Lines Matching refs:ok
29 (!s a fns ok.
30 MR_ev (Const s,a,ctxt:context_type,fns,ok) (s,ok))
32 (!x (a: string |-> SExp) fns ok.
34 MR_ev (Var x,a,ctxt,fns,ok) (FAPPLY a x,ok))
36 (!a fns ok s ok1.
37 MR_ev (Const (Sym "NIL"),a,ctxt,fns,ok) (s,ok1) ==>
38 MR_ev (Or [],a,ctxt,fns,ok) (s,ok1))
40 (!a fns s1 t ts ok.
41 MR_ev (t,a,ctxt,fns,ok) (s1,ok1) /\ isTrue s1 ==>
42 MR_ev (Or (t::ts),a,ctxt,fns,ok) (s1,ok1))
44 (!a fns s1 s2 t ts ok ok2.
45 MR_ev (t,a,ctxt,fns,ok) (s1,ok1) /\ ~(isTrue s1) /\
47 MR_ev (Or (t::ts),a,ctxt,fns,ok) (s2,ok2))
50 MR_ev (e1,a,ctxt,fns,ok) (s1,ok1) /\ ~isTrue s1 /\
53 MR_ev (If e1 e2 e3,a,ctxt,fns,ok) (s,ok2))
56 MR_ev (e1,a,ctxt,fns,ok) (s1,ok1) /\ isTrue s1 /\
59 MR_ev (If e1 e2 e3,a,ctxt,fns,ok) (s,ok2))
62 MR_evl (ys,a,ctxt,fns,ok) (sl,ok1) /\ (LENGTH xs = LENGTH ys) /\
65 MR_ev (LamApp xs e ys,a,ctxt,fns,ok) (x,ok2))
68 MR_evl (el,a,ctxt,fns,ok) (args,ok1) /\
71 MR_ev (App fc el,a,ctxt,fns,ok) (x,ok2))
76 MR_ap (PrimitiveFun fc,args,a,ctxt,fns,ok) (f args,ok))
82 MR_ev (exp,VarBind params args,ctxt,fns,ok) (x,ok2)
84 MR_ap (Fun fc,args,a,ctxt,fns,ok) (x,ok2))
92 MR_ap (Fun fc,args,a,ctxt,fns,ok) (sem args,F))
94 (!x a ctxt fns ok.
95 MR_ap (Fun "NOT",[x],a,ctxt,fns,ok) (not x,ok))
97 (!x a ctxt fns ok.
98 MR_ap (Fun "RANK",[x],a,ctxt,fns,ok) (rank x,ok))
100 (!x a ctxt fns ok.
101 MR_ap (Fun "ORDP",[x],a,ctxt,fns,ok) (ordp x,ok))
103 (!x y a ctxt fns ok.
104 MR_ap (Fun "ORD<",[x;y],a,ctxt,fns,ok) (ord_ x y,ok))
109 MR_ev (exp,VarBind params args,ctxt,fns,ok) (x,ok2)
111 MR_ap (Funcall,Sym fname::args,a,ctxt,fns,ok) (x,ok2))
114 MR_evl ([],a,ctxt,fns,ok) ([],ok))
117 MR_ev (e,a,ctxt,fns,ok) (s,ok1) /\
120 MR_evl (e::el,a,ctxt,fns,ok) (s::sl,ok2))
125 MR_ev (App (PrimitiveFun opCAR) [e],a,ctxt,fns,ok) (s,ok1) ==>
126 MR_ev (First e,a,ctxt,fns,ok) (s,ok1))
129 MR_ev (First (App (PrimitiveFun opCDR) [e]),a,ctxt,fns,ok) (s,ok1) ==>
130 MR_ev (Second e,a,ctxt,fns,ok) (s,ok1))
133 MR_ev (Second (App (PrimitiveFun opCDR) [e]),a,ctxt,fns,ok) (s,ok1) ==>
134 MR_ev (Third e,a,ctxt,fns,ok) (s,ok1))
137 MR_ev (Third (App (PrimitiveFun opCDR) [e]),a,ctxt,fns,ok) (s,ok1) ==>
138 MR_ev (Fourth e,a,ctxt,fns,ok) (s,ok1))
141 MR_ev (Fourth (App (PrimitiveFun opCDR) [e]),a,ctxt,fns,ok) (s,ok1) ==>
142 MR_ev (Fifth e,a,ctxt,fns,ok) (s,ok1))
145 MR_ev (LamApp (MAP FST zs) x (MAP SND zs),a,ctxt,fns,ok) (s,ok1) ==>
146 MR_ev (Let zs x,a,ctxt,fns,ok) (s,ok1))
149 MR_ev (x,a,ctxt,fns,ok) (s,ok1) ==>
150 MR_ev (LetStar [] x,a,ctxt,fns,ok) (s,ok1))
153 MR_ev (Let [z] (LetStar zs x),a,ctxt,fns,ok) (s,ok1) ==>
154 MR_ev (LetStar (z::zs) x,a,ctxt,fns,ok) (s,ok1))
157 MR_ev (Const (Sym "NIL"),a,ctxt,fns,ok) (s,ok1) ==>
158 MR_ev (Cond [],a,ctxt,fns,ok) (s,ok1))
161 MR_ev (If x1 x2 (Cond qs),a,ctxt,fns,ok) (s,ok1) ==>
162 MR_ev (Cond ((x1,x2)::qs),a,ctxt,fns,ok) (s,ok1))
165 MR_ev (Const (Sym "T"),a,ctxt,fns,ok) (s,ok1) ==>
166 MR_ev (And [],a,ctxt,fns,ok) (s,ok1))
169 MR_ev (Const (Sym "NIL"),a,ctxt,fns,ok) (s,ok1) ==>
170 MR_ev (List [],a,ctxt,fns,ok) (s,ok1))
173 MR_ev (t,a,ctxt,fns,ok) (s,ok1) ==>
174 MR_ev (And [t],a,ctxt,fns,ok) (s,ok1))
177 MR_ev (If t1 (And (t2::ts)) (Const (Sym "NIL")),a,ctxt,fns,ok) (s,ok1) ==>
178 MR_ev (And (t1::t2::ts),a,ctxt,fns,ok) (s,ok1))
181 MR_ev (App (PrimitiveFun opCONS) [t;List ts],a,ctxt,fns,ok) (s,ok1) ==>
182 MR_ev (List (t::ts),a,ctxt,fns,ok) (s,ok1))
185 MR_ev (App Define [Const (Sym fname); Const (list2sexp (MAP Sym ps)); Const body],a,ctxt,fns,ok) (s,ok1) ==>
186 MR_ev (Defun fname ps body,a,ctxt,fns,ok) (s,ok1))`;
204 !f args a ctxt fns ok res ok1 res2 ok2 ok3.
205 (x = (f,args,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\
208 !xs a ctxt fns ok res ok1 res2 ok2 ok3.
209 (x = (xs,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\
212 !x1 a ctxt fns ok res ok1 res2 ok2 ok3.
213 (x = (x1,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\
235 !f args a ctxt fns ok res ok1 res2 ok2 ok3.
236 (x = (f,args,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\
237 MR_ap (f,args,a,ctxt,fns,ok) (res2,ok2) ==> (res = res2) /\ (ok1 = ok2)`
239 !xs a ctxt fns ok res ok1 res2 ok2 ok3.
240 (x = (xs,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\
241 MR_evl (xs,a,ctxt,fns,ok) (res2,ok2) ==> (res = res2) /\ (ok1 = ok2)`
243 !x1 a ctxt fns ok res ok1 res2 ok2 ok3.
244 (x = (x1,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\
245 MR_ev (x1,a,ctxt,fns,ok) (res2,ok2) ==> (res = res2) /\ (ok1 = ok2)`
269 !f args a ctxt fns ok res ok1.
270 (x = (f,args,a,ctxt \\ name,fns,ok)) /\ (y = (res,ok1)) ==>
271 MR_ap (f,args,a,ctxt,fns,ok) (res,ok1)`
273 !xs a ctxt fns ok res ok1 res2 ok2 ok3.
274 (x = (xs,a,ctxt \\ name,fns,ok)) /\ (y = (res,ok1)) ==>
275 MR_evl (xs,a,ctxt,fns,ok) (res,ok1)`
277 !x1 a ctxt fns ok res ok1 res2 ok2 ok3.
278 (x = (x1,a,ctxt \\ name,fns,ok)) /\ (y = (res,ok1)) ==>
279 MR_ev (x1,a,ctxt,fns,ok) (res,ok1)`
308 !f args a ctxt fns ok res ok1.
309 (x = (f,args,a,ctxt,fns,ok)) /\ (y = (res,ok1)) ==>
310 MR_ap (f,args,a,ctxt,add_def fns d,ok) (res,ok1)`
312 !xs a ctxt fns ok res ok1 res2 ok2 ok3.
313 (x = (xs,a,ctxt,fns,ok)) /\ (y = (res,ok1)) ==>
314 MR_evl (xs,a,ctxt,add_def fns d,ok) (res,ok1)`
316 !x1 a ctxt fns ok res ok1 res2 ok2 ok3.
317 (x = (x1,a,ctxt,fns,ok)) /\ (y = (res,ok1)) ==>
318 MR_ev (x1,a,ctxt,add_def fns d,ok) (res,ok1)`
337 !f args a ctxt fns ok res ok1 z.
338 (x = (f,args,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\
339 MR_ap (f,args,a,ctxt,fns,ok) z ==> (z = (res,ok1))`
341 !xs a ctxt fns ok res ok1 z.
342 (x = (xs,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\
343 MR_evl (xs,a,ctxt,fns,ok) z ==> (z = (res,ok1))`
345 !x1 a ctxt fns ok res ok1 z.
346 (x = (x1,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\
347 MR_ev (x1,a,ctxt,fns,ok) z ==> (z = (res,ok1))`
368 !f args a ctxt fns ok res ok1 z.
369 (x = (f,args,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ ok1 ==> ok`
371 !xs a ctxt fns ok res ok1 z.
372 (x = (xs,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ ok1 ==> ok`
374 !x1 a ctxt fns ok res ok1 z.
375 (x = (x1,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ ok1 ==> ok`
407 ``!xs ys ok ok1. MR_evl (xs,a,ctxt,fns,ok) (ys,ok1) ==> (LENGTH xs = LENGTH ys)``,
418 !f args a ctxt fns ok res ok1 io q1 q2.
419 (x = (f,args,a,fns,io,ok)) /\ (y = (res,q1,q2,ok1)) /\ ok1 ==> ok`
421 !xs a ctxt fns ok res ok1 io q1 q2.
422 (x = (xs,a,fns,io,ok)) /\ (y = (res,q1,q2,ok1)) /\ ok1 ==> ok`
424 !x1 a ctxt fns ok res ok1 io q1 q2.
425 (x = (x1,a,fns,io,ok)) /\ (y = (res,q1,q2,ok1)) /\ ok1 ==> ok`
442 !f args a ctxt fns ok res ok1 io.
443 (x = (f,args,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ core_assum fns ==>
445 R_ap (f,args,a,fns,io,ok) (res,fns,io ++ io1,ok1)`
447 !xs a ctxt fns ok res ok1 io.
448 (x = (xs,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ core_assum fns ==>
450 R_evl (xs,a,fns,io,ok) (res,fns,io ++ io1,ok1)`
452 !x1 a ctxt fns ok res ok1 io.
453 (x = (x1,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ core_assum fns ==>
455 R_ev (x1,a,fns,io,ok) (res,fns,io ++ io1,ok1)`
661 !f args a ctxt fns ok res ok1 z.
662 (x = (f,args,a,ctxt,fns,ok)) /\ (y = (res,ok1)) ==>
663 MR_ap (f,args,a,ctxt,fns,ok) (res,ok1)`
665 !xs a b ctxt fns ok res ok1 z n v.
666 (x = (xs,a,ctxt,fns,ok)) /\ (y = (res,ok1)) ==>
669 MR_evl (xs,b,ctxt,fns,ok) (res,ok1)`
671 !x1 a b ctxt fns ok res ok1 z n v.
672 (x = (x1,a,ctxt,fns,ok)) /\ (y = (res,ok1)) ==>
675 MR_ev (x1,b,ctxt,fns,ok) (res,ok1)`
688 \\ `MR_evl (ys,b,ctxt,fns,ok) (sl,ok1)` by METIS_TAC []
906 ``MR_ev (App (PrimitiveFun opCAR) [x],a,ctxt,fns,ok) (s,ok2) =
907 ?res. MR_ev (x,a,ctxt,fns,ok) (res,ok2) /\ (s = CAR res)``,
913 ``MR_ev (App (PrimitiveFun opCDR) [x],a,ctxt,fns,ok) (s,ok2) =
914 ?res. MR_ev (x,a,ctxt,fns,ok) (res,ok2) /\ (s = CDR res)``,
921 ``MR_ev (First x,a,ctxt,fns,ok) (s,ok2)``
925 ``MR_ev (Second x,a,ctxt,fns,ok) (s,ok2)``
929 ``MR_ev (Third x,a,ctxt,fns,ok) (s,ok2)``
933 ``MR_ev (Fourth x,a,ctxt,fns,ok) (s,ok2)``
937 ``MR_ev (Fifth x,a,ctxt,fns,ok) (s,ok2)``
940 ``(!res ok2 ok a.
942 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==>
943 MR_ev (x,a,ctxt,fns,ok) (res,ok2)) /\
945 MR_ev (term2term (First x),a,ctxt,fns,ok) (res,ok2) ==>
946 MR_ev (First x,a,ctxt,fns,ok) (res,ok2)``,
952 ``(!res ok2 ok a.
954 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==>
955 MR_ev (x,a,ctxt,fns,ok) (res,ok2)) /\
957 MR_ev (term2term (Second x),a,ctxt,fns,ok) (res,ok2) ==>
958 MR_ev (Second x,a,ctxt,fns,ok) (res,ok2)``,
964 ``(!res ok2 ok a.
966 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==>
967 MR_ev (x,a,ctxt,fns,ok) (res,ok2)) /\
969 MR_ev (term2term (Third x),a,ctxt,fns,ok) (res,ok2) ==>
970 MR_ev (Third x,a,ctxt,fns,ok) (res,ok2)``,
976 ``(!res ok2 ok a.
978 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==>
979 MR_ev (x,a,ctxt,fns,ok) (res,ok2)) /\
981 MR_ev (term2term (Fourth x),a,ctxt,fns,ok) (res,ok2) ==>
982 MR_ev (Fourth x,a,ctxt,fns,ok) (res,ok2)``,
988 ``(!res ok2 ok a.
990 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==>
991 MR_ev (x,a,ctxt,fns,ok) (res,ok2)) /\
993 MR_ev (term2term (Fifth x),a,ctxt,fns,ok) (res,ok2) ==>
994 MR_ev (Fifth x,a,ctxt,fns,ok) (res,ok2)``,
1001 MR_evl (MAP Var vs ++ ys,a,ctxt,fns,ok) (sl,ok1) ==>
1004 MR_evl (ys,a,ctxt,fns,ok) (sl2,ok1)``,
1030 !res ok2 ok a.
1032 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==>
1033 MR_ev (x,a,ctxt,fns,ok) (res,ok2)) /\
1034 (!res ok2 ok a.
1036 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==>
1037 MR_ev (x,a,ctxt,fns,ok) (res,ok2)) /\
1039 MR_ev (term2term (Let ts x),a,ctxt,fns,ok) (res,ok2) ==>
1040 MR_ev (Let ts x,a,ctxt,fns,ok) (res,ok2)``,
1083 \\ Q.SPEC_TAC (`ok`,`ok`) \\ Q.SPEC_TAC (`ok1`,`ok1`)
1200 ``!xs res ok ok2 a.
1203 !res' ok2' ok' a'.
1204 MR_ev (term2term x,a',ctxt,fns,ok') (res',ok2') ==>
1205 MR_ev (x,a',ctxt,fns,ok') (res',ok2')) /\
1207 MR_ev (term2term (Or xs),a,ctxt,fns,ok) (res,ok2) ==>
1208 MR_ev (Or xs,a,ctxt,fns,ok) (res,ok2)``,
1238 \\ `MR_ev (h',a,ctxt,fns,ok) (res,ok1)` by METIS_TAC []
1281 ``!x res ok2 ok a.
1283 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==>
1284 MR_ev (x,a,ctxt,fns,ok) (res,ok2)``,
1303 \\ Q.SPEC_TAC (`args`,`args`) \\ Q.SPEC_TAC (`ok`,`ok`)
1318 \\ Q.SPEC_TAC (`sl`,`sl`) \\ Q.SPEC_TAC (`ok`,`ok`)
1498 !name params body sem args ok.
1501 ?ok2. MR_ap (Fun name,args,ARB,ctxt,k,ok) (sem args,ok2) /\
1505 ``MR_ap (Fun fc,args,a,ctxt \\ name,k,ok) (sem args,ok2) ==>
1506 MR_ap (Fun fc,args,a,ctxt,k,ok) (sem args,ok2)``,
2134 |> Q.SPEC `\(exp,a,ctxt) result. !ok env.
2146 ?ok2. MR_ev (t2term exp,env,ctxt,k,ok) (result,ok2) /\
2148 |> Q.SPEC `\(f,args,ctxt) result. !ok env.
2160 ?ok2. MR_ap (f2func f,args,ARB,ctxt,k,ok) (result,ok2) /\
2162 |> Q.SPEC `\(exp,a,ctxt) result. !ok env.
2174 ?ok2. MR_evl (MAP t2term exp,env,ctxt,k,ok) (result,ok2) /\
2196 \\ `?ok2. MR_ev (t2term e1,env,ctxt,k,ok) (s1,ok2) /\
2209 \\ `?ok2. MR_ev (t2term e1,env,ctxt,k,ok) (s1,ok2) /\
2225 \\ Q.PAT_X_ASSUM `!ok:bool. bbb` MP_TAC
2226 \\ Q.PAT_X_ASSUM `!ok:bool. bbb` (MP_TAC o Q.SPECL [`ok`,`env`])
2267 \\ Q.PAT_X_ASSUM `!ok env. bb ==> bbb` (MP_TAC o Q.SPECL [`ok`,`env`])
2270 \\ Q.PAT_X_ASSUM `!ok. ?ok2. bbb` (STRIP_ASSUME_TAC o Q.SPEC `ok2`)
2293 (Q.EXISTS_TAC `ok` \\ REVERSE STRIP_TAC THEN1
2322 \\ STRIP_TAC \\ POP_ASSUM (MP_TAC o Q.SPECL [`args`,`ok`])
2341 \\ Q.PAT_X_ASSUM `!ok env. bbb` (MP_TAC o Q.SPECL [`ok`,`VarBind params args`])
2385 \\ Q.PAT_X_ASSUM `!xx yy. bbb ==> bbbb` (MP_TAC o Q.SPECL [`ok`,`env`])