/seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/official-semantics/ |
H A D | SyntaxScript.sml | 56 | F_AND of fl # fl (* f1 and f2 *) 60 | F_UNTIL of fl # fl (* [f1 U f2] *) 72 | O_AND of obe # obe (* f1 and f2 *) 74 | O_EU of obe # obe (* E[f1 U f2] *)
|
H A D | UnclockedSemanticsScript.sml | 209 (UF_SEM v (F_AND(f1,f2)) = 210 UF_SEM v f1 /\ UF_SEM v f2) 235 (UF_SEM v (F_UNTIL(f1,f2)) = 237 UF_SEM (RESTN v k) f2 /\ !j :: (LESS k). UF_SEM (RESTN v j) f1) 271 (UF_SEM v (F_AND(f1,f2)) = 272 UF_SEM v f1 /\ UF_SEM v f2) 297 (UF_SEM v (F_UNTIL(f1,f2)) = 299 UF_SEM (RESTN v k) f2 /\ !j :: (LESS k). UF_SEM (RESTN v j) f1) 353 (O_SEM M (O_AND(f1,f2)) s = O_SEM M f1 s /\ O_SEM M f2 [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/ |
H A D | many2_win32.c | 13 float f2, 26 return ((f1/f2+f3/f4+f5/f6+f7/f8+f9/f10+f11/f12) * f13); 12 fastcall_many(float f1, float f2, float f3, float f4, float f5, float f6, float f7, float f8, float f9, float f10, float f11, float f12, float f13) argument
|
H A D | many_win32.c | 13 float f2, 26 return ((f1/f2+f3/f4+f5/f6+f7/f8+f9/f10+f11/f12) * f13); 12 stdcall_many(float f1, float f2, float f3, float f4, float f5, float f6, float f7, float f8, float f9, float f10, float f11, float f12, float f13) argument
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | jrhCore.sml | 27 val conjn_rwt = prove(``!f1 f2 x. eval_form f1 x /\ eval_form f2 x = 28 eval_form (Conjn f1 f2) x``, tac) 29 val disjn_rwt = prove(``!f1 f2 x. eval_form f1 x \/ eval_form f2 x = 30 eval_form (Disjn f1 f2) x``, tac) 58 (* i.e., c1 /\ c2 = eval_form f1 x /\ eval_form f2 x *) 190 ``(eval_form (neginf (Conjn f1 f2)) x = eval_form (neginf f1) x /\ 191 eval_form (neginf f2) x) /\ 192 (eval_form (neginf (Disjn f1 f2)) [all...] |
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | indexedListsScript.sml | 67 ``!l1 l2 f1 f2. 68 l1 = l2 /\ (!x n. MEM x l2 ==> f1 n x = f2 n x) ==> 69 MAPi f1 l1 = MAPi f2 l2``, 74 ``l1 = l2 ==> (!x n. (x = EL n l2) ==> n < LENGTH l2 ==> f1 n x = f2 n x) ==> 75 MAPi f1 l1 = MAPi f2 l2``, 76 map_every qid_spec_tac [`f1`, `f2`, `l2`] >> Induct_on `l1` >> 108 ``(!m. m < n ==> f1 m = f2 m) ==> GENLIST f1 n = GENLIST f2 n``, 109 map_every qid_spec_tac [`f1`, `f2`] >> Induct_on `n` >> 135 (!n e a. n < LENGTH l2 ==> MEM e l2 ==> f1 n e a = f2 [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | ANF.sml | 106 (`!f1 f2 f3. Seq (Par f1 f2) f3 = \x. let v = f2 x in f3 (f1 x,v)`, 110 (`!f2 f3. Seq (Par (\x.x) f2) f3 = \x. let v = f2 x in f3 (x,v)`, 141 val f2 = mk_pabs(args,t2) value 143 val th2 = PBETA_CONV (mk_comb(f2,args)) 144 val th3 = ISPECL [f1,f2] Par_def 145 val ptm = mk_pabs(args, mk_pair(mk_comb(f1,args),mk_comb(f2,arg 168 val f2 = mk_pabs(args,t2) value 199 val f2 = mk_pabs(args,M) value 219 val f2 = mk_pabs(args,t2) value 365 val f2 = mk_pabs(args,rand t2) value [all...] |
H A D | cpsScript.sml | 15 `Seq (f1:'a->'b) (f2:'b->'c) = \x. f2(f1 x)`; 19 `Par f1 f2 = \x. (f1 x, f2 x)`; 23 `Ite f1 f2 f3 = \x. if f1 x then f2 x else f3 x`; 27 `Rec (x:'a) = if f1 x then f2 x else Rec (f3 x)`; 304 ``!f f1 f2 f3. 305 (!x:'a. f x = if f1(x) then f2(x) else f(f3 x)) 307 ==> (f:'a->'b = Rec f1 f2 f [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | ANF.sml | 106 (`!f1 f2 f3. Seq (Par f1 f2) f3 = \x. let v = f2 x in f3 (f1 x,v)`, 110 (`!f2 f3. Seq (Par (\x.x) f2) f3 = \x. let v = f2 x in f3 (x,v)`, 141 val f2 = mk_pabs(args,t2) value 143 val th2 = PBETA_CONV (mk_comb(f2,args)) 144 val th3 = ISPECL [f1,f2] Par_def 145 val ptm = mk_pabs(args, mk_pair(mk_comb(f1,args),mk_comb(f2,arg 168 val f2 = mk_pabs(args,t2) value 199 val f2 = mk_pabs(args,M) value 219 val f2 = mk_pabs(args,t2) value 365 val f2 = mk_pabs(args,rand t2) value [all...] |
H A D | cpsScript.sml | 15 `Seq (f1:'a->'b) (f2:'b->'c) = \x. f2(f1 x)`; 19 `Par f1 f2 = \x. (f1 x, f2 x)`; 23 `Ite f1 f2 f3 = \x. if f1 x then f2 x else f3 x`; 27 `Rec (x:'a) = if f1 x then f2 x else Rec (f3 x)`; 304 ``!f f1 f2 f3. 305 (!x:'a. f x = if f1(x) then f2(x) else f(f3 x)) 307 ==> (f:'a->'b = Rec f1 f2 f [all...] |
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/ |
H A D | formParseScript.sml | 163 ������s1 s2 f1 f2 top1 top2. 164 (s1 = s2) ��� (���s. LENGTH s < LENGTH s1 ��� (f1 s = f2 s)) ��� 166 (parseFGX f1 top1 s1 = parseFGX f2 top2 s2)���, 175 rename [���option_CASE (f2 s')���, ���f1 _ = f2 _���] >> 176 reverse (Cases_on ���f2 s'���) >> simp[UNIT_DEF] 177 >- (rename [���f2 s' = SOME p���] >> Cases_on ���p��� >> simp[]) >> 185 >- (rename [���option_CASE (f2 s2)���, ���f1 _ = f2 _���] >> Cases_on ���f2 s [all...] |
/seL4-l4v-10.1.1/HOL4/src/finite_map/ |
H A D | finite_mapScript.sml | 498 (`!x y (f1:('a,'b)fmap) f2. 499 (f1 = f2) ==> 500 ((\f.FUPDATE f (x,y)) f1 = (\f. FUPDATE f (x,y)) f2)`, 745 ``!f1 f2 s1 s2. 746 (DRESTRICT f1 s1 = DRESTRICT f2 s2) = 747 (DRESTRICT f1 s1 SUBMAP f2 /\ DRESTRICT f2 s2 SUBMAP f1 /\ 748 (s1 INTER FDOM f1 = s2 INTER FDOM f2))``, 886 ``!f1 f2 m. DISJOINT (FDOM f1) (FDOM f2) [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | nestedCases.sml | 37 `num_case b f2 z = 39 else let v = destruct_suc z in f2 v`,
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | ParseDatatype_dtype.sml | 19 fun pr (f1,f2) (a,b) = "(" ^ f1 a ^ "," ^ f2 b ^ ")"
|
/seL4-l4v-10.1.1/l4v/tools/autocorres/tests/examples/ |
H A D | heap_wrap.c | 32 void f2(struct thing *t) { function
|
/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/ |
H A D | arrays.c | 21 i10 *f2(void) function
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | ctlScript.sml | 61 | C_AND of ctl # ctl (* f1 \wedge f2 *) 63 | C_EU of ctl # ctl (* E[f1 U f2] *) 343 (C_SEM M (C_AND(f1,f2)) s = C_SEM M f1 s /\ C_SEM M f2 s) /\ 345 (C_SEM M (C_EU(f1,f2)) s = CEU M (C_SEM M f1, C_SEM M f2) s) /\ 360 val C_AU_def = Define `C_AU ((f1: 'prop ctl),(f2: 'prop ctl)) = C_AND(C_NOT(C_EU(C_NOT f2,C_AND(C_NOT f1,C_NOT f2))),C_NOT(C_EG(C_NOT f2)))`; [all...] |
/seL4-l4v-10.1.1/HOL4/src/boss/theory_tests/ |
H A D | github112Script.sml | 6 val f2_def = Define `(f2 x y = case (x, y) of (0, _) => SOME 1 | _ => NONE)`
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | cpsScript.sml | 15 `Seq (f1:'a->'b) (f2:'b->'c) = \x. f2(f1 x)`; 19 `Par f1 f2 = \x. (f1 x, f2 x)`; 23 `Ite f1 f2 f3 = \x. if f1 x then f2 x else f3 x`; 27 `Rec (x:'a) = if f1 x then f2 x else Rec (f3 x)`; 304 ``!f f1 f2 f3. 305 (!x:'a. f x = if f1(x) then f2(x) else f(f3 x)) 307 ==> (f:'a->'b = Rec f1 f2 f [all...] |
H A D | ANF.sml | 106 (`!f1 f2 f3. Seq (Par f1 f2) f3 = \x. let v = f2 x in f3 (f1 x,v)`, 110 (`!f2 f3. Seq (Par (\x.x) f2) f3 = \x. let v = f2 x in f3 (x,v)`, 141 val f2 = mk_pabs(args,t2) value 143 val th2 = PBETA_CONV (mk_comb(f2,args)) 144 val th3 = ISPECL [f1,f2] Par_def 145 val ptm = mk_pabs(args, mk_pair(mk_comb(f1,args),mk_comb(f2,arg 168 val f2 = mk_pabs(args,t2) value 199 val f2 = mk_pabs(args,M) value 219 val f2 = mk_pabs(args,t2) value 365 val f2 = mk_pabs(args,rand t2) value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | rltlScript.sml | 39 | RLTL_AND of rltl # rltl (* f1 and f2 *) 41 | RLTL_SUNTIL of rltl # rltl (* [f1 U f2] *) 58 [`P`,`\(f,b). P f`,`\(f1,f2). P f1 /\ P f2`] 70 (RLTL_SEM_TIME t v a r (RLTL_AND (f1,f2)) = 71 RLTL_SEM_TIME t v a r f1 /\ RLTL_SEM_TIME t v a r f2) 76 (RLTL_SEM_TIME t v a r (RLTL_SUNTIL(f1,f2)) = 77 ?k. (k >= t) /\ (RLTL_SEM_TIME k v a r f2) /\ (!j. (t <= j /\ j < k) ==> (RLTL_SEM_TIME j v a r f1))) 109 `RLTL_OR(f1,f2) = RLTL_NOT (RLTL_AND((RLTL_NOT f1),(RLTL_NOT f2)))`; [all...] |
/seL4-l4v-10.1.1/HOL4/examples/category/ |
H A D | YonedaScript.sml | 61 `(TypedGraphFun (t2,t3) f2) o (TypedGraphFun (t1,t2) f1) -:ens_cat U = 62 (TypedGraphFun (t4,t3) f1) o (TypedGraphFun (t1,t4) f2) -:ens_cat U` >> 65 (���x. x ��� t2 ��� f2 x ��� t3) ��� 66 (���x. x ��� t1 ��� f2 x ��� t4)` by ( 89 srw_tac [][Abbr`f1`,Abbr`f2`] >> 383 qmatch_abbrev_tac `(f1 o f2 -:ens_cat (homs c) = f3 o f4 -:ens_cat (homs c)) ��� X` >> 384 `IsTypedFun f2` by ( 385 srw_tac [][Abbr`f2`] >> 412 `f2 ���> f1 -:ens_cat (homs c)` by ( 413 fsrw_tac [][Abbr`f2`,hom_de [all...] |
/seL4-l4v-10.1.1/HOL4/examples/real-to-float/ |
H A D | daisyScript.sml | 42 (eval_F c env (Add f1 f2) = c.add (eval_F c env f1) (eval_F c env f2)) /\ 43 (eval_F c env (Div f1 f2) = c.div (eval_F c env f1) (eval_F c env f2))` 46 (eval_C c env (LessEq f1 f2) = c.less_eq (eval_F c env f1) (eval_F c env f2))` 190 (f_str (Add f1 f2) = "(" ++ f_str f1 ++ " + " ++ f_str f2 ++ ")") /\ 194 (c_str (LessEq f1 f2) = "(" ++ f_str f1 ++ " <= " ++ f_str f2 [all...] |
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
H A D | inference_rulesScript.sml | 445 THEN Cases_on `f2 a b` 446 THEN Cases_on `f2 a' b'` 482 ``! f1 f2 k k' invr23 uf uy. 486 (preserve_relation_mmu_abs f2 (assert_mode k) (assert_mode k') uf uy) ==> 487 (preserve_relation_mmu (f1 >>= (f2)) (assert_mode k) invr23 uf uy) 495 ``! f1 f2 k k' uf uy. 498 (preserve_relation_mmu_abs f2 (assert_mode k') (assert_mode k') uf uy) ==> 499 (preserve_relation_mmu (f1 >>= (f2)) (assert_mode k) (assert_mode k') uf uy) 506 ``! f1 f2 k k' comb_inv uf uy. 510 (preserve_relation_mmu_abs f2 (assert_mod [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/common/ |
H A D | decoderScript.sml | 114 (((DT >> f1) ++ (DF >> f2)) (g,F::b) = f2 (g,b)) /\ 115 (((DF >> f2) ++ (DT >> f1)) (g,F::b) = f2 (g,b)) /\ 116 (((DT >> f1) ++ (DF >> f2)) (g,T::b) = f1 (g,b)) /\ 117 (((DF >> f2) ++ (DT >> f1)) (g,T::b) = f1 (g,b)) /\
|