/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | muSyntaxScript.sml | 161 (SUBFORMULA g (f1 /\ f2) = (SUBFORMULA g f1) \/ (SUBFORMULA g f2) \/ (g = f1 /\ f2)) /\ 162 (SUBFORMULA g (f1 \/ f2) = (SUBFORMULA g f1) \/ (SUBFORMULA g f2) \/ (g = f1 \/ f2)) /\ 180 (IMF (f1 /\ f2) = (IMF f1) /\ (IMF f2)) /\ 181 (IMF (f1 \/ f2) = (IMF f1) /\ (IMF f2)) /\ [all...] |
H A D | commonTools.sml | 191 (* assume t=(c,f1,f2) is a nested conditional, return a list of all the conditions *) 192 fun depth_dest_cond_aux (c,f1,f2) = 194 val l2 = if (is_cond f2) then depth_dest_cond_aux (dest_cond f2) else [] 199 fun list_dest_cond_aux (c,f1,f2) = if is_cond f2 then (c,f1)::(list_dest_cond_aux (dest_cond f2)) else [(c,f1)] 204 fun gen_dest_cond_aux (c,f1,f2) = 206 val l2 = if (is_cond f2) then gen_dest_cond_aux (dest_cond f2) els [all...] |
/seL4-l4v-10.1.1/HOL4/src/rational/ |
H A D | ratScript.sml | 39 val rat_equiv_def = Define `rat_equiv f1 f2 = (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)`; 113 ``!f1 f2. rat_equiv f1 f2 = (rat_equiv f1 = rat_equiv f2)``, 265 ``!f1 f2. (abs_rat f1 = abs_rat f2) = rat_equiv f1 f2``, 289 * |- !f1 f2 [all...] |
H A D | jbUtils.sml | 121 list_xmerge [[``f1:frac``,``f2:frac``],[``f2:frac``,``f3:frac``]];
|
H A D | ratLib.sml | 35 * abs_rat f1 = abs_rat f2 37 * |- (abs_rat f1 = abs_rat f2) 38 * = (nmr f1 * dnm f2 = nmr f2 * dnm f1) : thm 46 val (rhc, f2) = dest_comb rhs; 48 UNDISCH_ALL (SPECL[f1,f2] RAT_EQ) 56 * A ?- abs_rat f1 = abs_rat f2 58 * A ?- nmr f1 * dnm f2 = nmr f2 * dnm f1 192 RAT_CALC_CONV ``rat_add (abs_rat(f1)) (abs_rat(f2))``; [all...] |
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Normalize.sml | 186 | (Exists (_,_,n1,f1), Exists (_,_,n2,f2)) => 189 | EQUAL => compare (f1,f2) 193 | (Forall (_,_,n1,f1), Forall (_,_,n2,f2)) => 196 | EQUAL => compare (f1,f2) 305 | And2 (True,f2) = f2 307 | And2 (f1,f2) = 315 case f2 of 317 | _ => (freeVars f2, count f2, singleto [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Normalize.sml | 186 | (Exists (_,_,n1,f1), Exists (_,_,n2,f2)) => 189 | EQUAL => compare (f1,f2) 193 | (Forall (_,_,n1,f1), Forall (_,_,n2,f2)) => 196 | EQUAL => compare (f1,f2) 305 | And2 (True,f2) = f2 307 | And2 (f1,f2) = 315 case f2 of 317 | _ => (freeVars f2, count f2, singleto [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/LTL/ |
H A D | LTLScript.sml | 73 (Formula Vars (AND f1 f2) = Formula Vars f1 /\ Formula Vars f2) 75 (Formula Vars (OR f1 f2) = Formula Vars f1 /\ Formula Vars f2) 83 (Formula Vars (UNTIL f1 f2) = Formula Vars f1 /\ Formula Vars f2) 85 (Formula Vars (WEAK_UNTIL f1 f2) = Formula Vars f1 /\ Formula Vars f2)`; 373 (SEM M p (AND f1 f2) = SEM M p f1 /\ SEM M p f2) [all...] |
/seL4-l4v-10.1.1/HOL4/src/datatype/ |
H A D | ind_typeScript.sml | 124 ``!f1 f2. (INJF f1 :num->'a->bool = INJF f2) = (f1 = f2)``, 138 Term`INJP f1 f2:num->'a->bool = 139 \n a. if NUMLEFT n then f1 (NUMRIGHT n) a else f2 (NUMRIGHT n) a`); 143 Term`!(f1:num->'a->bool) f1' f2 f2'. 144 (INJP f1 f2 = INJP f1' f2') = (f1 = f1') /\ (f2 [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/ |
H A D | pkg-test.lisp | 8 (defun f2 (x) function
|
/seL4-l4v-10.1.1/HOL4/examples/elliptic/swsep/ |
H A D | examples.sml | 101 val def2 = Define `f2 (x:word32) = x + f1(x) + 1w`; 102 val def3 = Define `f3 (x:word32) = f2(x) + 1w`;
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | selftest.sml | 31 (Hol_defn "f2") 32 `(f2 x y = case (x, y:'a) of (T, _) => T | _ => F)`
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/acl2/ |
H A D | m1_factorialScript.sml | 53 val f2 = el 2 (CONJUNCTS defs); value 61 val _ = sexp.print_acl2def out (sexp.defun (concl f2));
|
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/Solitaire/ |
H A D | MiniTLHexSolitaireScript.sml | 222 (Eval (AND f1 f2) R s = Eval f1 R s /\ Eval f2 R s) /\ 223 (Eval (OR f1 f2) R s = Eval f1 R s \/ Eval f2 R s) /\ 309 (aEval (aAND f1 f2) (R,L) s = aEval f1 (R,L) s /\ aEval f2 (R,L) s) /\ 310 (aEval (aOR f1 f2) (R,L) s = aEval f1 (R,L) s \/ aEval f2 (R,L) s) /\
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/powerpc/ |
H A D | aix.S | 61 .set f2,2 155 lfd f2,-32-(12*8)(r28) 200 stfd f2, 8(r30) 257 lfd f2,-16-(12*8)(r28)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/test/ |
H A D | refined_format.sml | 106 f2 (k0:word32,(k1:word32,k2:word32),k3:word32) = 110 f2 (k0 - 1w, (k3 - k2, k2 * k1), k0) 112 f2 (k0 - 1w, (k0,k1), k3 - k0)`; 117 |- f2 = 132 f2 (r0,(r1,r2),r3)) 141 f2 (r0,(r1,r2),r3))))) : thm
|
/seL4-l4v-10.1.1/HOL4/examples/unification/triangular/first-order/ |
H A D | unifDefScript.sml | 156 Q.ABBREV_TAC `f2 = \n. FST (SND (f n))` THEN 157 `!n. FST (SND (f n)) = f2 n` by SRW_TAC [][Abbr`f2`] THEN 163 `��n. allvars (f1 n) (f2 n) (f3 n)`] 181 (allvars (f1 n) (f2 n) (f3 n) = allvars (f1 m) (f2 m) (f3 m))` 185 allvars (f1 (f' m)) (f2 (f' m)) (f3 (f' m)) 187 allvars (f1 m) (f2 m) (f3 m)` 190 (allvars (f1 (f' m)) (f2 (f' m)) (f3 (f' m))) 191 (allvars (f1 m) (f2 [all...] |
/seL4-l4v-10.1.1/HOL4/examples/logic/ |
H A D | foltypesScript.sml | 143 ``^IMP_t f1 f2 = 144 ^form_ABS_t (GLAM ARB ftmIMP [] [^form_REP_t f1; ^form_REP_t f2])``); 146 ``^formP (GLAM v ftmIMP [] [^form_REP_t f1; ^form_REP_t f2])``, 150 ``^form_ABS_t (GLAM v ftmIMP [] [^form_REP_t f1; ^form_REP_t f2]) = 151 ^IMP_t f1 f2``, 368 (���f1 f2 x. (���x. P f1 x) ��� (���x. P f2 x) ��� P (IMP f1 f2) x) ��� 394 ``ALL v1 f1 = ALL v2 f2`` 398 |> GENL [``v1:string``, ``v2:string``, ``f1:form``, ``f2 [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | ILTheory.sig | 203 |- (!f f1 f2 f3 a. CTL_STRUCTURE_case f f1 f2 f3 (BLK a) = f a) /\ 204 (!f f1 f2 f3 a0 a1. CTL_STRUCTURE_case f f1 f2 f3 (SC a0 a1) = f1 a0 a1) /\ 205 (!f f1 f2 f3 a0 a1 a2. 206 CTL_STRUCTURE_case f f1 f2 f3 (CJ a0 a1 a2) = f2 a0 a1 a2) /\ 207 !f f1 f2 f3 a0 a1. CTL_STRUCTURE_case f f1 f2 f3 (TR a0 a1) = f3 a0 a1 430 |- (!f f1 f2 f [all...] |
H A D | rulesScript.sml | 321 `!ir1 ir2 pre_p1 post_p1 post_p2 stk_f in_f1 f1 f2 out_f1 out_f2. 323 PSPEC ir1 (pre_p1,post_p1) stk_f (in_f1,f1,out_f1) /\ PSPEC ir2 (post_p1,post_p2) stk_f (out_f1,f2,out_f2) 325 PSPEC (SC ir1 ir2) (pre_p1,post_p2) stk_f (in_f1,f2 o f1,out_f2)`, 333 `!cond ir_t ir_f pre_p post_p stk_f cond_f in_f f1 f2 out_f. 336 PSPEC ir_f (pre_p, post_p) stk_f (in_f,f2,out_f) /\ (!st. cond_f (in_f st) = eval_il_cond cond st) 338 PSPEC (CJ cond ir_t ir_f) (pre_p,post_p) stk_f (in_f, (\v.if cond_f v then f1 v else f2 v), out_f)`, 518 `!ir1 ir2 pre_p1 post_p1 post_p2 stk vi1 f1 vo1 f2 vo2. 520 VSPEC ir1 (pre_p1,post_p1) stk (vi1,f1,vo1) /\ VSPEC ir2 (post_p1,post_p2) stk (vo1,f2,vo2) 522 VSPEC (SC ir1 ir2) (pre_p1,post_p2) stk (vi1,f2 o f1,vo2)`, 529 `!cond ir_t ir_f pre_p post_p stk cond_f iv f1 f2 o [all...] |
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | StrongLawsScript.sml | 1824 (?f1 n1 f2 m2. 1826 (!j. j <= m2 ==> Is_Prefix(f2 j)) /\ 1827 (x = par (SIGMA f1 n1) (SIGMA f2 m2)) /\ 1831 (par (PREF_PROC (f1 i)) (SIGMA f2 m2))) n1) 1832 (SIGMA (\j. prefix (PREF_ACT(f2 j)) 1833 (par (SIGMA f1 n1) (PREF_PROC (f2 j)))) m2)) 1834 (ALL_SYNC f1 n1 f2 m2)))`` 1857 (REWRITE_RULE [ASSUME ``E = par (SIGMA f1 n1) (SIGMA f2 m2)``] 1885 (MATCH_MP (ASSUME ``!(j :num). j <= m2 ==> Is_Prefix (f2 j)``) 1888 (REWRITE_RULE [ASSUME ``(f2 [all...] |
/seL4-l4v-10.1.1/HOL4/examples/category/ |
H A D | zfset_catScript.sml | 895 qmatch_abbrev_tac `f1##(f2##gof) = (f1##(f2##g)) |o| (f1##(f2##f))` >> 896 `f1##(f2##gof) = (f1 ��� f2)##gof` by ( 899 `f1##(f2##g) = (f1 ��� f2)##g` by ( 902 `f1##(f2##f) = (f1 ��� f2)##f` by ( 906 Q.ISPECL_THEN [`f1 ��� f2`,`(f [all...] |
/seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
H A D | quotientScript.sml | 734 !f1 f2. 735 (R1 ===> R2) f1 f2 ==> 736 (R1 ===> R2) (\x. f1 x) (\y. f2 y)���), 766 !f1 f2. 767 (R1 ===> R2) f1 f2 ==> 769 (RES_ABSTRACT (respects R1) f2) 798 (���!REL1 (abs1:'a -> 'c) rep1 REL2 (abs2:'b -> 'd) rep2 f1 f2. 801 (REL1 ===> REL2) f1 f2 ==> 802 (REL1 ===> REL2) f1 ((abs1 --> rep2) ((rep1 --> abs2) f2))���), 1139 !f1 f2 [all...] |
H A D | quotient_listScript.sml | 253 !l1 l2 f1 f2. 254 (R1 ===> R2) f1 f2 /\ (LIST_REL R1) l1 l2 ==> 255 (LIST_REL R2) (MAP f1 l1) (MAP f2 l2)���), 587 !l1 l2 f1 f2 e1 e2. 588 (R1 ===> R2 ===> R1) f1 f2 /\ 590 R1 (FOLDL f1 e1 l1) (FOLDL f2 e2 l2)���), 628 !l1 l2 f1 f2 e1 e2. 629 (R1 ===> R2 ===> R2) f1 f2 /\ 631 R2 (FOLDR f1 e1 l1) (FOLDR f2 e2 l2)���),
|
/seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/src/ |
H A D | decidable_separationLogicLib.sml | 161 val sf = ``sf_bin_tree (f1,f2) e`` 171 val (f1,f2) = pairLib.dest_pair (el 1 args) 172 val _ = if f1 = f2 then (SMALLFOOT_ERR "NO SF_BIN_TREE!") else (); 174 (f1,f2, el 2 args, el 1 args) 179 val sf = ``sf_tree (f1::f2::l) e1 e2`` 181 val sf = ``sf_bin_tree (f1,f2) e`` 205 val (f1, f2, e, _) = dest_sf_bin_tree sf; 209 (sf, ([f1,f2], mk_list ([], type_of f1)), es, e) 219 val sf = ``sf_points_to e ((f1, e1)::(f2,e2)::l)`` 541 val t = ``LIST_DS_ENTAILS ([], [(e1,e2);(e9,e9)]) ((pf1::pf_equal e e::pf_true::pf2::pf_equal e' e'::pf3::l),(sf1::sf2::(sf_ls f e e) ::sf3::(sf_points_to e [(f, e)])::(sf_bin_tree (f1, f2) dse_ni 618 val (f2, p2) = get_pf_trival_filter pf; value 951 val (f2, p2) = get_hypothesis_filter cL pfL pfL'; value 1369 val f2 = mk_list (f2L, Type `:pointsto_cases`); value [all...] |