1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_semantics";
2
3open stringTheory finite_mapTheory pred_setTheory listTheory sumTheory;
4open optionTheory arithmeticTheory relationTheory;
5
6open lisp_sexpTheory lisp_parseTheory;
7
8infix \\
9val op \\ = op THEN;
10
11
12(* abstract syntax of well-formed Lisp prorams *)
13
14val _ = Hol_datatype `
15  func = PrimitiveFun of lisp_primitive_op
16       | Define | Print | Error | Funcall | Fun of string`;
17
18val _ = Hol_datatype `
19  term = Const of SExp
20       | Var of string
21       | App of func => term list
22       | If of term => term => term
23       | LamApp of string list => term => term list
24       (* only macros below *)
25       | Let of (string # term) list => term
26       | LetStar of (string # term) list => term
27       | Cond of (term # term) list
28       | Or of term list | And of term list
29       | First of term | Second of term | Third of term
30       | Fourth of term | Fifth of term | List of term list
31       | Defun of string => string list => SExp`;
32
33val term_11 = fetch "-" "term_11";
34val term_distinct = fetch "-" "term_distinct";
35val term_size_def = fetch "-" "term_size_def";
36val func_11 = fetch "-" "func_11";
37
38
39(* reading a program, i.e. term, from an s-expression -- sexp2term *)
40
41val list2sexp_def = Define `
42  (list2sexp [] = Sym "NIL") /\
43  (list2sexp (x::xs) = Dot x (list2sexp xs))`;
44
45val sym2prim_def = Define `
46  sym2prim s =
47    if s = "CONS" then SOME opCONS else
48    if s = "EQUAL" then SOME opEQUAL else
49    if s = "<" then SOME opLESS else
50    if s = "SYMBOL-<" then SOME opSYMBOL_LESS else
51    if s = "+" then SOME opADD else
52    if s = "-" then SOME opSUB else
53    if s = "CONSP" then SOME opCONSP else
54    if s = "NATP" then SOME opNATP else
55    if s = "SYMBOLP" then SOME opSYMBOLP else
56    if s = "CAR" then SOME opCAR else
57    if s = "CDR" then SOME opCDR else NONE`;
58
59val sexp2list_def = Define `
60  (sexp2list (Val n) = []) /\
61  (sexp2list (Sym s) = []) /\
62  (sexp2list (Dot x y) = x::sexp2list y)`;
63
64val IMP_isDot = prove(
65  ``!x. ~isVal x /\ ~isSym x ==> isDot x``,
66  Cases \\ EVAL_TAC);
67
68val MEM_sexp2list_LSIZE = prove(
69  ``!b a. MEM a (sexp2list b) ==> LSIZE a < LSIZE b``,
70  Induct \\ SIMP_TAC std_ss [sexp2list_def,MEM,LSIZE_def] \\ REPEAT STRIP_TAC
71  \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC \\ DECIDE_TAC);
72
73val LSIZE_CAR_LESS = prove(
74  ``!x m. LSIZE x < m ==> LSIZE (CAR x) < m``,
75  Cases \\ SIMP_TAC std_ss [CAR_def,LSIZE_def] \\ DECIDE_TAC);
76
77val LSIZE_CDR_LESS = prove(
78  ``!x m. LSIZE x < m ==> LSIZE (CDR x) < m``,
79  Cases \\ SIMP_TAC std_ss [CDR_def,LSIZE_def] \\ DECIDE_TAC);
80
81val sexp2term_def = tDefine "sexp2term" `
82  sexp2term x = if x = Sym "T" then Const x else
83                if x = Sym "NIL" then Const x else
84                if isVal x then Const x else
85                if isSym x then Var (getSym x) else
86                let x1 = CAR x in
87                let x2 = CAR (CDR x) in
88                let x3 = CAR (CDR (CDR x)) in
89                let x4 = CAR (CDR (CDR (CDR x))) in
90                if x1 = Sym "QUOTE" then Const x2 else
91                if x1 = Sym "IF" then
92                  If (sexp2term x2) (sexp2term x3) (sexp2term x4) else
93                if ~(sym2prim (getSym x1) = NONE) then
94                  App (PrimitiveFun (THE (sym2prim (getSym x1))))
95                    (MAP sexp2term (sexp2list (CDR x))) else
96                if x1 = Sym "FIRST" then First (sexp2term x2) else
97                if x1 = Sym "SECOND" then Second (sexp2term x2) else
98                if x1 = Sym "THIRD" then Third (sexp2term x2) else
99                if x1 = Sym "FOURTH" then Fourth (sexp2term x2) else
100                if x1 = Sym "FIFTH" then Fifth (sexp2term x2) else
101                if x1 = Sym "OR" then Or (MAP sexp2term (sexp2list (CDR x))) else
102                if x1 = Sym "AND" then And (MAP sexp2term (sexp2list (CDR x))) else
103                if x1 = Sym "LIST" then List (MAP sexp2term (sexp2list (CDR x))) else
104                if x1 = Sym "DEFUN" then
105                  Defun (getSym x2) (MAP getSym (sexp2list x3)) x4 else
106                if x1 = Sym "COND" then
107                  Cond (MAP (\y. (sexp2term (CAR y), sexp2term (CAR (CDR y))))
108                            (sexp2list (CDR x))) else
109                if x1 = Sym "LET" then
110                  Let (MAP (\y. (getSym (CAR y), sexp2term (CAR (CDR y))))
111                           (sexp2list x2)) (sexp2term x3) else
112                if x1 = Sym "LET*" then
113                  LetStar (MAP (\y. (getSym (CAR y), sexp2term (CAR (CDR y))))
114                               (sexp2list x2)) (sexp2term x3) else
115                if CAR x1 = Sym "LAMBDA" then
116                  let y2 = CAR (CDR x1) in
117                  let y3 = CAR (CDR (CDR x1)) in
118                    LamApp (MAP getSym (sexp2list y2)) (sexp2term y3)
119                           (MAP sexp2term (sexp2list (CDR x))) else
120                if x1 = Sym "DEFINE" then
121                  App Define (MAP sexp2term (sexp2list (CDR x))) else
122                if x1 = Sym "ERROR" then
123                  App Error (MAP sexp2term (sexp2list (CDR x))) else
124                if x1 = Sym "FUNCALL" then
125                  App Funcall (MAP sexp2term (sexp2list (CDR x))) else
126                if x1 = Sym "PRINT" then
127                  App Print (MAP sexp2term (sexp2list (CDR x)))
128                else (* user-defined fun *)
129                  App (Fun (getSym x1))
130                    (MAP sexp2term (sexp2list (CDR x)))`
131 (WF_REL_TAC `measure LSIZE`
132  \\ REPEAT STRIP_TAC \\ IMP_RES_TAC IMP_isDot
133  \\ FULL_SIMP_TAC std_ss [isDot_thm,LSIZE_def,CDR_def,CAR_def]
134  \\ IMP_RES_TAC MEM_sexp2list_LSIZE
135  \\ POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [CDR_def]
136  \\ REPEAT STRIP_TAC
137  \\ REPEAT (MATCH_MP_TAC LSIZE_CAR_LESS)
138  \\ REPEAT (MATCH_MP_TAC LSIZE_CDR_LESS) \\ REPEAT DECIDE_TAC
139  \\ Cases_on `b` \\ FULL_SIMP_TAC std_ss [CAR_def,LSIZE_def] \\ DECIDE_TAC);
140
141
142(* a structural operational semantics *)
143
144val EVAL_DATA_OP_def = Define `
145  (EVAL_DATA_OP opCONS = ((\xs. LISP_CONS (EL 0 xs) (EL 1 xs)), 2)) /\
146  (EVAL_DATA_OP opEQUAL = ((\xs. LISP_EQUAL (EL 0 xs) (EL 1 xs)), 2)) /\
147  (EVAL_DATA_OP opLESS = ((\xs. LISP_LESS (EL 0 xs) (EL 1 xs)), 2)) /\
148  (EVAL_DATA_OP opSYMBOL_LESS = ((\xs. LISP_SYMBOL_LESS (EL 0 xs) (EL 1 xs)), 2)) /\
149  (EVAL_DATA_OP opADD = ((\xs. LISP_ADD (EL 0 xs) (EL 1 xs)), 2)) /\
150  (EVAL_DATA_OP opSUB = ((\xs. LISP_SUB (EL 0 xs) (EL 1 xs)), 2)) /\
151  (EVAL_DATA_OP opCONSP = ((\xs. LISP_CONSP (EL 0 xs)), 1)) /\
152  (EVAL_DATA_OP opNATP = ((\xs. LISP_NUMBERP (EL 0 xs)), 1)) /\
153  (EVAL_DATA_OP opSYMBOLP = ((\xs. LISP_SYMBOLP (EL 0 xs)), 1)) /\
154  (EVAL_DATA_OP opCAR = ((\xs. CAR (EL 0 xs)), 1)) /\
155  (EVAL_DATA_OP opCDR = ((\xs. CDR (EL 0 xs)), (1:num)))`;
156
157val VarBindAux_def = Define `
158  (VarBindAux [] args = FEMPTY) /\
159  (VarBindAux (p::ps) [] = FEMPTY) /\
160  (VarBindAux (p::ps) (a::as) = (VarBindAux ps as) |+ (p,a))`;
161
162val VarBind_def = Define `
163  VarBind params args = VarBindAux (REVERSE params) (REVERSE args)`;
164
165val add_def_def = Define `
166  add_def fns x = FUNION fns (FEMPTY |+ x)`;
167
168val (R_ev_rules,R_ev_ind,R_ev_cases) = Hol_reln `
169 (!s a fns io ok.
170    R_ev (Const s, a,fns,io,ok) (s,fns,io,ok))
171  /\
172  (!x (a: string |-> SExp) fns io ok.
173    x IN FDOM a ==>
174    R_ev (Var x,a,fns,io,ok) (a ' x,fns,io,ok))
175  /\
176  (!a fns io ok s fns1 io1 ok1.
177    R_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==>
178    R_ev (Or [],a,fns,io,ok) (s,fns1,io1,ok1))
179  /\
180  (!a fns io s1 fns1 io1 t ts ok.
181    R_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ isTrue s1 ==>
182    R_ev (Or (t::ts),a,fns,io,ok) (s1,fns1,io1,ok1))
183  /\
184  (!a fns io s1 fns1 io1 s2 fns2 io2 t ts ok ok2.
185    R_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ ~(isTrue s1) /\
186    R_ev (Or ts,a,fns1,io1,ok1) (s2,fns2,io2,ok2) ==>
187    R_ev (Or (t::ts),a,fns,io,ok) (s2,fns2,io2,ok2))
188  /\
189  (!e1 e2 e3 s1 s a ok1 ok2.
190    R_ev (e1,a,fns,io,ok) (s1,fns1,io1,ok1) /\ ~isTrue s1 /\
191    R_ev (e3,a,fns1,io1,ok1) (s,fns2,io2,ok2)
192    ==>
193    R_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2))
194  /\
195  (!e1 e2 e3 s1 s a ok1 ok2.
196    R_ev (e1,a,fns,io,ok) (s1,fns1,io1,ok1) /\ isTrue s1 /\
197    R_ev (e2,a,fns1,io1,ok1) (s,fns2,io2,ok2)
198    ==>
199    R_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2))
200  /\
201  (!e xs ys fns a ok1 ok2.
202    R_evl (ys,a,fns,io,ok) (sl,fns1,io1,ok1) /\ (LENGTH xs = LENGTH ys) /\
203    R_ev (e,FUNION (VarBind xs sl) a,fns1,io1,ok1) (x,fns2,io2,ok2)
204    ==>
205    R_ev (LamApp xs e ys,a,fns,io,ok) (x,fns2,io2,ok2))
206  /\
207  (!el args a fc fns x ok1 ok2.
208    R_evl (el,a,fns,io,ok) (args,fns1,io1,ok1) /\
209    R_ap (fc,args,a,fns1,io1,ok1) (x,fns2,io2,ok2)
210    ==>
211    R_ev (App fc el,a,fns,io,ok) (x,fns2,io2,ok2))
212  /\
213  (!fc args a fns f.
214    (EVAL_DATA_OP fc = (f,LENGTH args))
215    ==>
216    R_ap (PrimitiveFun fc,args,a,fns,io,ok) (f args,fns,io,ok))
217  /\
218  (!args a fc fns params exp x ok2.
219    fc IN FDOM fns /\
220    (fns ' fc = (params,exp)) /\ (LENGTH params = LENGTH args) /\
221    R_ev (exp,VarBind params args,fns,io,ok) (x,fns2,io2,ok2)
222    ==>
223    R_ap (Fun fc,args,a,fns,io:string,ok) (x,fns2,io2,ok2))
224  /\
225  (!args a fns io.
226    R_ap (Print,args,a,fns,io,ok) (Sym "NIL",fns,
227          io ++ sexp2string (list2sexp (Sym "PRINT"::args)) ++ "\n",ok))
228  /\
229  (!a fns fc formals body.
230    R_ap (Define,[fc; formals; body],a,fns,io,ok)
231         (Sym "NIL",add_def fns (getSym fc,MAP getSym (sexp2list formals),sexp2term body),
232          io,ok /\ ~(getSym fc IN FDOM fns)))
233  /\
234  (!args a fns io anything.
235    R_ap (Error,args,a,fns,io,ok) (anything,fns,
236          io ++ sexp2string (list2sexp (Sym "ERROR"::args)) ++ "\n",F))
237  /\
238  (!args params a fname fns x ok2.
239    fname IN FDOM fns /\
240    (fns ' fname = (params,exp)) /\ (LENGTH params = LENGTH args) /\
241    R_ev (exp,VarBind params args,fns,io,ok) (x,fns2,io2,ok2)
242    ==>
243    R_ap (Funcall,Sym fname::args,a,fns,io,ok) (x,fns2,io2,ok2))
244  /\ (* give short-cut semantics for failure states *)
245  (!f args a fns io res.
246    f IN FDOM fns /\
247    (fns ' f = (params,exp)) /\ (LENGTH params = LENGTH args) ==>
248    R_ap (Fun f,args,a,fns,io,F) (res,fns,io,F))
249  /\ (* give short-cut semantics for failure states *)
250  (!args a fns io res.
251    R_ap (Funcall,args,a,fns,io,F) (res,fns,io,F))
252  /\
253  (!a.
254    R_evl ([],a,fns,io,ok) ([],fns,io,ok))
255  /\
256  (!e el s sl a ok1 ok2.
257    R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1) /\
258    R_evl (el,a,fns1,io1,ok1) (sl,fns2,io2,ok2)
259    ==>
260    R_evl (e::el,a,fns,io,ok) (s::sl,fns2,io2,ok2))
261
262  /\ (* semantics of macros below *)
263
264  (!e a fns io s fns1 io1 ok1.
265    R_ev (App (PrimitiveFun opCAR) [e],a,fns,io,ok) (s,fns1,io1,ok1) ==>
266    R_ev (First e,a,fns,io,ok) (s,fns1,io1,ok1))
267  /\
268  (!e a fns io s fns1 io1 ok1.
269    R_ev (First (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==>
270    R_ev (Second e,a,fns,io,ok) (s,fns1,io1,ok1))
271  /\
272  (!e a fns io s fns1 io1 ok1.
273    R_ev (Second (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==>
274    R_ev (Third e,a,fns,io,ok) (s,fns1,io1,ok1))
275  /\
276  (!e a fns io s fns1 io1 ok1.
277    R_ev (Third (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==>
278    R_ev (Fourth e,a,fns,io,ok) (s,fns1,io1,ok1))
279  /\
280  (!e a fns io s fns1 io1 ok1.
281    R_ev (Fourth (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==>
282    R_ev (Fifth e,a,fns,io,ok) (s,fns1,io1,ok1))
283  /\
284  (!zs x a fns io s fns1 io1 ok1.
285    R_ev (LamApp (MAP FST zs) x (MAP SND zs),a,fns,io,ok) (s,fns1,io1,ok1) ==>
286    R_ev (Let zs x,a,fns,io,ok) (s,fns1,io1,ok1))
287  /\
288  (!x a fns io s fns1 io1 ok1.
289    R_ev (x,a,fns,io,ok) (s,fns1,io1,ok1) ==>
290    R_ev (LetStar [] x,a,fns,io,ok) (s,fns1,io1,ok1))
291  /\
292  (!z zs x a fns io s fns1 io1 ok1.
293    R_ev (Let [z] (LetStar zs x),a,fns,io,ok) (s,fns1,io1,ok1) ==>
294    R_ev (LetStar (z::zs) x,a,fns,io,ok) (s,fns1,io1,ok1))
295  /\
296  (!a fns io s fns1 io1 ok1.
297    R_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==>
298    R_ev (Cond [],a,fns,io,ok) (s,fns1,io1,ok1))
299  /\
300  (!x1 x2 qs a fns io s fns1 io1 ok1.
301    R_ev (If x1 x2 (Cond qs),a,fns,io,ok) (s,fns1,io1,ok1) ==>
302    R_ev (Cond ((x1,x2)::qs),a,fns,io,ok) (s,fns1,io1,ok1))
303  /\
304  (!a fns io s fns1 io1 ok1.
305    R_ev (Const (Sym "T"),a,fns,io,ok) (s,fns1,io1,ok1) ==>
306    R_ev (And [],a,fns,io,ok) (s,fns1,io1,ok1))
307  /\
308  (!a fns io s fns1 io1 ok1.
309    R_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==>
310    R_ev (List [],a,fns,io,ok) (s,fns1,io1,ok1))
311  /\
312  (!a fns io s fns1 io1 ok1.
313    R_ev (t,a,fns,io,ok) (s,fns1,io1,ok1) ==>
314    R_ev (And [t],a,fns,io,ok) (s,fns1,io1,ok1))
315  /\
316  (!a fns io s fns1 io1 ok1.
317    R_ev (If t1 (And (t2::ts)) (Const (Sym "NIL")),a,fns,io,ok) (s,fns1,io1,ok1) ==>
318    R_ev (And (t1::t2::ts),a,fns,io,ok) (s,fns1,io1,ok1))
319  /\
320  (!a fns io s fns1 io1 ok1.
321    R_ev (App (PrimitiveFun opCONS) [t;List ts],a,fns,io,ok) (s,fns1,io1,ok1) ==>
322    R_ev (List (t::ts),a,fns,io,ok) (s,fns1,io1,ok1))
323  /\
324  (!fname ps body a fns io s fns1 io1 ok1.
325    R_ev (App Define [Const (Sym fname); Const (list2sexp (MAP Sym ps)); Const body],a,fns,io,ok) (s,fns1,io1,ok1) ==>
326    R_ev (Defun fname ps body,a,fns,io,ok) (s,fns1,io1,ok1))`;
327
328val R_evl_LENGTH = save_thm("R_evl_LENGTH",
329  R_ev_ind
330  |> Q.SPECL [`\x y. T`,`\x y. (LENGTH (FST x) = LENGTH (FST y))`,`\x y. T`]
331  |> SIMP_RULE std_ss [LENGTH]);
332
333
334(* semantics of the read-eval-print loop *)
335
336val (R_exec_rules,R_exec_ind,R_exec_cases) = Hol_reln `
337 (!input fns io rest.
338    (is_eof input = (T,rest)) ==>
339    R_exec (input,fns,io) (io,T))
340  /\
341 (!input fns io input2 exp rest s fns2 io2 ok2 io3 ok3.
342    (is_eof input = (F,input2)) /\
343    (sexp_parse_stream input2 = (exp,rest)) /\
344    R_ev (sexp2term exp,FEMPTY,fns,io,T) (s,fns2,io2,ok2) /\
345    R_exec (rest,fns2,io2 ++ sexp2string s ++ "\n") (io3,ok3) ==>
346    R_exec (input,fns,io) (io3,ok2 /\ ok3))`;
347
348
349(* theorems about the semantics *)
350
351val R_ev_induct = IndDefLib.derive_strong_induction(R_ev_rules,R_ev_ind);
352
353val PULL_FORALL_IMP = METIS_PROVE [] ``(p ==> !x. q x) = !x. p ==> q x``;
354
355val R_ev_OK = prove(
356  ``(!x y. R_ap x y ==> SND (SND (SND y)) ==> (SND (SND (SND (SND (SND x)))))) /\
357    (!x y. R_evl x y ==> SND (SND (SND y)) ==> (SND (SND (SND (SND (x)))))) /\
358    (!x y. R_ev x y ==> SND (SND (SND y)) ==> (SND (SND (SND (SND (x))))))``,
359  HO_MATCH_MP_TAC R_ev_ind \\ SIMP_TAC std_ss [pairTheory.FORALL_PROD,LET_DEF]);
360
361val R_ev_T_11_lemma = prove(
362  ``(!x y. R_ap x y ==> !z. SND (SND (SND y)) /\ R_ap x z ==> (y = z)) /\
363    (!x y. R_evl x y ==> !z. SND (SND (SND y)) /\ R_evl x z ==> (y = z)) /\
364    (!x y. R_ev x y ==> !z. SND (SND (SND y)) /\ R_ev x z ==> (y = z))``,
365  HO_MATCH_MP_TAC R_ev_induct \\ SIMP_TAC std_ss []
366  \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []
367  \\ POP_ASSUM MP_TAC \\ ONCE_REWRITE_TAC [R_ev_cases] \\ SIMP_TAC (srw_ss()) []
368  \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ RES_TAC
369  \\ IMP_RES_TAC R_ev_OK \\ FULL_SIMP_TAC std_ss [listTheory.CONS_11]
370  \\ RES_TAC \\ FULL_SIMP_TAC std_ss [])
371  |> SIMP_RULE std_ss [pairTheory.FORALL_PROD,PULL_FORALL_IMP];
372
373val R_ev_T_11 = store_thm("R_ev_T_11",
374  ``!x y. R_ev x (res,k,io,T) /\ R_ev x y ==> (y = (res,k,io,T))``,
375  FULL_SIMP_TAC std_ss [pairTheory.FORALL_PROD] \\ REPEAT STRIP_TAC
376  \\ IMP_RES_TAC R_ev_T_11_lemma \\ FULL_SIMP_TAC std_ss []);
377
378val R_ap_T_11 = store_thm("R_ap_T_11",
379  ``!x y. R_ap x (res,k,io,T) /\ R_ap x y ==> (y = (res,k,io,T))``,
380  FULL_SIMP_TAC std_ss [pairTheory.FORALL_PROD] \\ REPEAT STRIP_TAC
381  \\ IMP_RES_TAC R_ev_T_11_lemma \\ FULL_SIMP_TAC std_ss []);
382
383val R_ap_F_11 = store_thm("R_ap_F_11",
384  ``R_ap x (res,k,io,F) /\ R_ap x (res2,k2,io2,b) ==> ~b``,
385  REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []
386  \\ IMP_RES_TAC R_ap_T_11 \\ FULL_SIMP_TAC std_ss []);
387
388Theorem R_ev_T_cases:
389  (R_ev (x,env,k,io,ok) (r,k',io',T) ���
390     R_ev (x,env,k,io,T) (r,k',io',T) /\ ok) /\
391  (R_evl (xs,env,k,io,ok) (rs,k',io',T) ���
392     R_evl (xs,env,k,io,T) (rs,k',io',T) /\ ok) /\
393  (R_ap (f,args,env,k,io,ok) (r,k',io',T) ���
394     R_ap (f,args,env,k,io,T) (r,k',io',T) /\ ok)
395Proof REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC
396      \\ IMP_RES_TAC R_ev_OK \\ FULL_SIMP_TAC std_ss []
397QED
398
399
400val _ = export_theory();
401