Searched refs:f2 (Results 101 - 125 of 315) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A DmuSyntaxScript.sml161 (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 DcommonTools.sml191 (* 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 DratScript.sml39 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 DjbUtils.sml121 list_xmerge [[``f1:frac``,``f2:frac``],[``f2:frac``,``f3:frac``]];
H A DratLib.sml35 * 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 DNormalize.sml186 | (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 DNormalize.sml186 | (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 DLTLScript.sml73 (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 Dind_typeScript.sml124 ``!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 Dpkg-test.lisp8 (defun f2 (x) function
/seL4-l4v-10.1.1/HOL4/examples/elliptic/swsep/
H A Dexamples.sml101 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 Dselftest.sml31 (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 Dm1_factorialScript.sml53 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 DMiniTLHexSolitaireScript.sml222 (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 Daix.S61 .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 Drefined_format.sml106 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 DunifDefScript.sml156 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 DfoltypesScript.sml143 ``^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 DILTheory.sig203 |- (!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 DrulesScript.sml321 `!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 DStrongLawsScript.sml1824 (?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 Dzfset_catScript.sml895 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 DquotientScript.sml734 !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 Dquotient_listScript.sml253 !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 Ddecidable_separationLogicLib.sml161 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...]

Completed in 239 milliseconds

1234567891011>>