| /seL4-l4v-master/HOL4/src/q/ |
| H A D | selftest.sml | 83 [([a1,a2,a3], c)] =>
85 val _ = aconvdie "assumption #1" a1 expected_mat1a1
101 [([a1, a2], c)] =>
104 val _ = aconvdie "assumption #1" a1 expected_mat2a1
164 [([a1, a2], c)] => (aconvdie "assumption #1" a1 expected_a1;
179 [([a1, a2, a3], c)] =>
180 (aconvdie "assumption #1" a1 expected_a1;
|
| /seL4-l4v-master/HOL4/examples/unification/triangular/nominal/ |
| H A D | dis_setScript.sml | 28 (pnomsl ((a1,a2)::t) = a1::a2::pnomsl t)
|
| H A D | ntermScript.sml | 19 (Ctermeq (CNom a1) (CNom a2) = (a1 = a2)) ���
21 (Ctermeq (CTie a1 t1) (CTie a2 t2) <=> (a1 = a2) ��� Ctermeq t1 t2) ���
53 `���t1 t2 a1 a2. (a1 = a2) ��� Ctermeq t1 t2 ��� Ctermeq (CTie a1 t1) (CTie a2 t2)`,
|
| H A D | nunifPropsScript.sml | 48 (a1 ��� a2 ��� fresh fcs a1 t2 ���
49 equiv fcs t1 (apply_pi [(a1,a2)] t2) ���
50 equiv fcs (Tie a1 t1) (Tie a2 t2)) ���
79 Q.PAT_X_ASSUM `a ��� a1` ASSUME_TAC THEN
82 POP_ASSUM (Q.SPEC_THEN `REVERSE [(a1,a2)]` MP_TAC) THEN
119 `equiv fe (apply_pi [(a2,a1)] (apply_pi [(a1,a2)] t2)) (apply_pi [(a2,a1)] t1)`
123 Q.EXISTS_TAC `[(a1,a
[all...] |
| H A D | nunifDefScript.sml | 107 of (Nom a1, Nom a2) => if a1 = a2 then SOME (s,fe) else NONE
114 | (Tie a1 t1, Tie a2 t2) =>
115 if a1 = a2 then ntunify (s,fe) t1 t2
116 else do fcs <- term_fcs a1 (nwalk* s t2);
117 ntunify (s, fe UNION fcs) t1 (apply_pi [(a1,a2)] t2)
248 `nwfs s /\ (nwalk s t1 = Tie a1 t1a) ==>
283 (nwalk s t1 = Tie a1 t1a) ���
306 (nwalk (FST p) t1 = Tie a1 t1a) ���
557 (nwalk s t1 = Tie a1 t1
[all...] |
| /seL4-l4v-master/HOL4/examples/dev/AES/curried/ |
| H A D | word8Script.sml | 211 `BYTE_COMPARE (BYTE a7 a6 a5 a4 a3 a2 a1 a0)
225 (case BIT_COMPARE a1 b1
248 `(BYTE a b c d e f g h) XOR8 (BYTE a1 b1 c1 d1 e1 f1 g1 h1) =
249 BYTE (a XOR a1) (b XOR b1) (c XOR c1) (d XOR d1)
257 `(BYTE a b c d e f g h) AND8 (BYTE a1 b1 c1 d1 e1 f1 g1 h1) =
258 BYTE (a /\ a1) (b /\ b1) (c /\ c1) (d /\ d1)
|
| H A D | aesScript.sml | 32 `?a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11.
33 x = (a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11)`
137 `(a,b,c,d) XOR8x4 (a1,b1,c1,d1) = (a # a1, b # b1, c # c1, d # d1)`;
|
| /seL4-l4v-master/HOL4/examples/dev/sw2/ |
| H A D | refine.sml | 135 let val (t,a1,a2) = dest_cond tm
136 in case (is_const a1 orelse is_word_literal a1,
138 of (true,true) => MK_COND tm (letify a1) (letify a2)
139 | (true,false) => MK_COND tm (letify a1) (REFL a2)
140 | (false,true) => MK_COND tm (REFL a1) (letify a2)
|
| /seL4-l4v-master/HOL4/src/monad/ |
| H A D | parmonadsyntax.sml | 70 val (v1,a1) = clean_action arg1
74 APP(loc1, APP(loc2, IDENT(loc3, s), a1), a2))
119 | APP(l,a1,a2) => APP(l,clean_do a1, clean_do a2)
209 | SOME (a1, a2) => let
224 (pr_action (prec,l,prec) (SOME v1, a1) >>
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/mips/step/ |
| H A D | mips_stepScript.sml | 272 `!a0: word8 a1: word8 a2: word8 a3: word8 a4: word8 a5: word8 a6: word8
274 let w = a7 @@ a6 @@ a5 @@ a4 @@ a3 @@ a2 @@ a1 @@ a0
277 ((15 >< 0) w = (a1 @@ a0) : word16) /\
278 ((23 >< 0) w = (a2 @@ a1 @@ a0) : word24) /\
279 ((31 >< 0) w = (a3 @@ a2 @@ a1 @@ a0) : word32) /\
280 ((39 >< 0) w = (a4 @@ a3 @@ a2 @@ a1 @@ a0) : 40 word) /\
281 ((47 >< 0) w = (a5 @@ a4 @@ a3 @@ a2 @@ a1 @@ a0) : word48) /\
282 ((55 >< 0) w = (a6 @@ a5 @@ a4 @@ a3 @@ a2 @@ a1 @@ a0) : 56 word) /\
288 ((31 >< 8) w = (a3 @@ a2 @@ a1) : word24) /\
291 ((63 >< 8) w = (a7 @@ a6 @@ a5 @@ a4 @@ a3 @@ a2 @@ a1)
[all...] |
| /seL4-l4v-master/HOL4/examples/ |
| H A D | taut.sml | 149 `(car1 = a1 /\ b1) /\
152 (som1 = ~(a1 = b1)) /\
153 (cout1 = b1 /\ a1)
154 ==> (som1 = ~(~a1 /\ ~b1 \/ a1 /\ b1)) /\
4322 `(car1 = a1 /\ b1) /\
4329 (som1 = ~(a1 = b1)) /\
4330 (cout1 = b1 /\ a1) /\
4333 ==> (som1 = ~(~a1 /\ ~b1 \/ a1 /\ b
[all...] |
| /seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
| H A D | lisp_printScript.sml | 954 \\ `?a1 a2. t = Dot a1 a2` by FULL_SIMP_TAC std_ss [isDot_thm,SExp_11]
966 \\ Q.ABBREV_TAC `s1 = sexp2string_aux (a1,T)`
994 \\ Q.PAT_X_ASSUM `t = Dot a1 a2` (K ALL_TAC)
1022 \\ STRIP_ASSUME_TAC (Q.SPECL [`LDEPTH a1`,`LDEPTH a2`,`r8+16w`] stack_slots_MAX)
1025 one (r8 + 0xCw,h (r3+4w)) * stack_slots (r8 + 0x10w) (LDEPTH a1))
1028 \\ `lisp_tree a1 (h r3,d,h2) sym` by
1048 (ASSUME_TAC o RW [] o Q.SPEC `T` o RW [] o Q.SPEC `a1` o
1049 RW [DECIDE ``m < SUC (m + n):num``] o Q.SPEC `LSIZE a1`) th end)
1062 \\ Q.ABBREV_TAC `s1 = sexp2string_aux (a1,
[all...] |
| /seL4-l4v-master/HOL4/src/quotient/src/ |
| H A D | quotient_optionScript.sml | 243 !a1 a2 f1 f2.
244 (R1 ===> R2) f1 f2 /\ (OPTION_REL R1) a1 a2 ==>
245 (OPTION_REL R2) (OPTION_MAP f1 a1) (OPTION_MAP f2 a2)���),
|
| /seL4-l4v-master/HOL4/examples/CCS/ |
| H A D | CongruenceScript.sml | 364 (!a1 a2 e1 e2.
366 ==> GCONTEXT (\t. sum (prefix a1 (e1 t)) (* GCONTEXT4 *)
417 Know `CONTEXT (\t. (prefix a1 (e1 t)))`
423 Know `CONTEXT (\t. (\t. (prefix a1 (e1 t))) t + (\t. (prefix a2 (e2 t))) t)`
1195 (!a1 a2 e1 e2.
1196 GSEQ e1 /\ GSEQ e2 ==> GSEQ (\t. sum (prefix a1 (e1 t)) (* GSEQ4 *)
1218 qpat_x_assum `CONTEXT e1` (ASSUME_TAC o (Q.SPEC `a1`) o (MATCH_MP CONTEXT3)) \\
1220 MP_TAC (Q.SPECL [`\t. (prefix a1 (e1 t))`, `\t. (prefix a2 (e2 t))`] CONTEXT4) \\
1342 Cases_on `a1` >> Cases_on `a2` >| (* 4 sub-goals here *)
1484 POP_ASSUM (MP_TAC o (Q.SPEC `a1`)) \\
[all...] |
| /seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/ |
| H A D | combin.tex | 122 |- \(\forall\)a0 a1.
123 a0 --> a1 \(\Leftrightarrow\)
124 (\(\exists\)x y f. (a0 = f # x) \(\land\) (a1 = f # y) \(\land\) x --> y) \(\lor\)
125 (\(\exists\)f g x. (a0 = f # x) \(\land\) (a1 = g # x) \(\land\) f --> g) \(\lor\)
126 (\(\exists\)y. a0 = K # a1 # y) \(\lor\)
127 \(\exists\)f g x. (a0 = S # f # g # x) \(\land\) (a1 = f # x # (g # x))
206 |- \(\forall\)R a0 a1. RTC R a0 a1 \(\Leftrightarrow\) (a1 = a0) \(\lor\)
207 \(\exists\)y. R a0 y \(\land\) RTC R y a1
[all...] |
| /seL4-l4v-master/l4v/tools/c-parser/standalone-parser/ |
| H A D | basics.sml | 27 fun pair_compare (acmp, bcmp) ((a1, b1), (a2, b2)) =
28 case acmp(a1, a2) of
|
| /seL4-l4v-master/HOL4/examples/computability/kolmog/ |
| H A D | plain_kolmog_inequalitiesScript.sml | 715 ������a1 i1 b1. p1 = pair a1 (pair i1 b1)���
718 qabbrev_tac ���N1 = LENGTH (pair a1 (pair i1 b1))��� >>
723 qabbrev_tac���ARG = pair (n2bl N1) (pair (n2bl SIb_i) (pair a1 (pair i1 b1) ++ pair i2 b2))��� >>
729 ���LENGTH (pair a1 (pair i1 b1)) ��� LENGTH (pair (n2bl y) (pair (n2bl (print_index ��� nblfst_i)) []))���
731 ���2 * LENGTH a1 + (LENGTH b1 + (2 * LENGTH i1 + 2)) + 10 ���
733 ���2 * ��� (2 * LENGTH a1 + (LENGTH b1 + (2 * LENGTH i1 + 2))) + 5 <= 2 * LENGTH a1 + (LENGTH b1 + (2 * LENGTH i1 + 2)) + 10 ��� 2 * ��� y + (2 * ��� (print_index ��� nblfst_i) + 2) + 10 <= 2 * ��� y + (3 * ��� (print_index ��� nblfst_i) + 23)��� suffices_by metis_tac[LESS_EQ_TRANS] >> rw[] >>
734 ���2 * ��� (2 * LENGTH a1 + (LENGTH b1 + (2 * LENGTH i1 + 2))) + 5 ���
735 2 * LENGTH a1
[all...] |
| /seL4-l4v-master/HOL4/src/quotient/examples/sigma/ |
| H A D | liftScript.sml | 606 (!a0 a1 a0' a1'.
607 ALPHA_obj (INVOKE1 a0 a1) (INVOKE1 a0' a1') =
608 ALPHA_obj a0 a0' /\ (a1 = a1')) /\
609 (!a0 a1 a2 a0' a1' a2'.
610 ALPHA_obj (UPDATE1 a0 a1 a2) (UPDATE1 a0' a1' a
[all...] |
| /seL4-l4v-master/HOL4/examples/dev/AES/tupled/ |
| H A D | aesScript.sml | 33 `?a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11.
34 x = (a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11)`
138 `(a,b,c,d) XOR8x4 (a1,b1,c1,d1) = (a # a1, b # b1, c # c1, d # d1)`;
|
| /seL4-l4v-master/HOL4/examples/dev/AES/word8/ |
| H A D | aesScript.sml | 33 `?a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11.
34 x = (a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11)`
146 `(a,b,c,d) XOR8x4 (a1,b1,c1,d1) = (a ?? a1, b ?? b1, c ?? c1, d ?? d1)`;
|
| /seL4-l4v-master/HOL4/src/pred_set/src/ |
| H A D | pred_setLib.sml | 23 of (c,[a1,a2]) =>
|
| /seL4-l4v-master/HOL4/examples/Crypto/AES/ |
| H A D | aesScript.sml | 33 `?a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11.
34 x = (a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11)`
146 `(a,b,c,d) XOR8x4 (a1,b1,c1,d1) = (a ?? a1, b ?? b1, c ?? c1, d ?? d1)`;
|
| /seL4-l4v-master/isabelle/src/Pure/Isar/ |
| H A D | outer_syntax.scala | 97 val a1 = Symbol.decode(a)
100 List((a1, b1), (a2, b1))
|
| /seL4-l4v-master/l4v/isabelle/src/Pure/Isar/ |
| H A D | outer_syntax.scala | 97 val a1 = Symbol.decode(a)
100 List((a1, b1), (a2, b1))
|
| /seL4-l4v-master/HOL4/src/quantHeuristics/ |
| H A D | quantHeuristicsLibParameters.sml | 146 val t = ``(\ (a1, a2, a3). P a1 a2 a3) (x:('a # 'b # 'c))``
175 val t = ``!x. a /\ (\ (a1, t3, a2). P a1 a2 t3) x /\ b x``
|