Searched refs:f2 (Results 201 - 225 of 315) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/official-semantics/
H A DModelLemmasScript.sml1365 `O_OR(f1,f2) = O_NOT(O_AND(O_NOT f1, O_NOT f2))`;
1370 ``O_SEM M (O_OR (f1,f2)) s = O_SEM M f1 s \/ O_SEM M f2 s``,
1375 `O_IMP(f1,f2) = O_OR(O_NOT f1, f2)`;
1380 ``O_SEM M (O_IMP (f1,f2)) s = O_SEM M f1 s ==> O_SEM M f2 s``,
1386 `O_IFF(f1,f2) = O_AND(O_IMP(f1, f2), O_IM
[all...]
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/
H A DseparationLogicScript.sml1611 (PRODUCT_SEPARATION_COMBINATOR (f1:'a bin_option_function) (f2:'b bin_option_function) NONE _ = NONE) /\
1612 (PRODUCT_SEPARATION_COMBINATOR f1 f2 _ NONE = NONE) /\
1613 (PRODUCT_SEPARATION_COMBINATOR f1 f2 (SOME (x1,x2)) (SOME (y1,y2)) =
1615 let z2 = f2 (SOME x2) (SOME y2) in
1623 ``(PRODUCT_SEPARATION_COMBINATOR f1 f2 X NONE = NONE) /\
1624 (PRODUCT_SEPARATION_COMBINATOR f1 f2 NONE X = NONE) /\
1625 (PRODUCT_SEPARATION_COMBINATOR f1 f2 (SOME x) (SOME y) =
1627 let z2 = f2 (SOME (SND x)) (SOME (SND y)) in
1632 ((PRODUCT_SEPARATION_COMBINATOR f1 f2 (SOME x) (SOME y) = SOME z) =
1634 (f2 (SOM
[all...]
/seL4-l4v-10.1.1/HOL4/src/integer/
H A DOmegaMLShadow.sml117 combine_real_factoids i f1 f2
122 strictly negative in f2. The combination may produce a factoid where
128 fun combine_real_factoids i f1 f2 =
129 case (f1, f2) of
305 fun combine_dfactoids em i ((f1, d1), (f2, d2)) =
307 DARK => (combine_dark_factoids i f1 f2, d1)
308 | _ => (combine_real_factoids i f1 f2, REAL_COMBIN(i, d1, d2))
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibOmega.sml154 combine_real_factoids i f1 f2
159 strictly negative in f2. The combination may produce a factoid where
165 fun combine_real_factoids i f1 f2 =
166 case (f1, f2) of
343 fun combine_dfactoids em i ((f1, d1), (f2, d2)) =
345 DARK => (combine_dark_factoids i f1 f2, d1)
346 | _ => (combine_real_factoids i f1 f2, REAL_COMBIN(i, d1, d2))
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/more_theories/
H A DcardinalScript.sml222 (Q.X_CHOOSE_THEN `f2` assume_tac)) >>
224 qexists_tac `\(x,y). (f1 x, f2 y)` >>
360 `(?f1. BIJ f1 A M) /\ (?f2. BIJ f2 B M)` by metis_tac[cardeq_def] >>
364 qexists_tac `\x. if x IN A then (T,f1 x) else (F,f2 x)` >>
373 `?b. b IN B /\ (f2 b = m)` by metis_tac [BIJ_DEF, SURJ_DEF] >>
386 rr = {((s1:'a set,f1),(s2,f2)) | (s1,f1) IN A /\ (s2,f2) IN A /\ s1 SUBSET s2 /\
387 !x. x IN s1 ==> (f1 x = f2 x)}
397 map_every qx_gen_tac [`s1`, `f1`, `s2`, `f2`] >>
[all...]
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/executable-semantics/
H A DExecuteSemanticsScript.sml96 * Executable semantics of [f1 U f2]
97 * w |= [f1 U f2]
99 * |w| > 0 And (w |= f2 Or (w |= f1 And w^1 |= [f1 U f2]))
104 ``UF_SEM w (F_UNTIL(f1,f2)) =
107 (UF_SEM w f2
109 (UF_SEM w f1 /\ UF_SEM (RESTN w 1) (F_UNTIL(f1,f2))))``,
119 Cases_on `UF_SEM (FINITE l) f2`
151 Cases_on `UF_SEM (INFINITE f) f2`
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/
H A DpegScript.sml223 (subexprs (tok t f2) = { tok t f2 }) ���
266 (choice e1 e2 f2 ��� Gexprs G ��� e1 ��� Gexprs G ��� e2 ��� Gexprs G) ���
/seL4-l4v-10.1.1/HOL4/src/Boolify/src/
H A DEncodeScript.sml261 ``!l1 l2 f1 f2.
262 (l1=l2) /\ (!x. MEM x l2 ==> (f1 x = f2 x))
264 (encode_list f1 l1 = encode_list f2 l2)``,
/seL4-l4v-10.1.1/HOL4/examples/logic/
H A DPropLogicScript.sml35 (`!f1 f2 s. (!x. x IN s ==> (f1 x = f2 x)) ==> (IMAGE f1 s = IMAGE f2 s)`,
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/
H A DbuechiAScript.sml141 >> qabbrev_tac `f2 = ��(m,n,b). f m n b`
142 >> `FINITE {f2 x | x ��� T1 }`
143 suffices_by (qunabbrev_tac `f2` >> rpt strip_tac
H A DconcrRepScript.sml801 (addFrmlToGraph g (U f1 f2) =
802 if MEM (U f1 f2) (MAP ((��l. l.frml) ��� SND) (toAList g.nodeInfo))
804 else addNode <| frml := (U f1 f2); is_final := T
816 >- (Cases_on `?f1 f2. f = U f1 f2`
819 >> Cases_on `���y. U f1 f2 = (SND y).frml
823 >> qexists_tac `(g.next,<|frml := U f1 f2;
930 ==> (SORTED (��f1 f2. (FST f2).edge_grp <= (FST f1).edge_grp) fls
954 (��(f1:�� edgeLabelAA # num) (f2
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/
H A DonestepScript.sml495 `!f1 f2 f3 imm1 imm2 abs1 abs2.
496 CORRECT f1 f2 imm1 abs1 /\ CORRECT f2 f3 imm2 abs2 ==>
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/
H A Dlisp_parseScript.sml1770 (Q.ABBREV_TAC `f2 = (r4 + 0x4w =+ 0x3w)
1775 SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by
1782 \\ Q.UNABBREV_TAC `f2`
1796 (Q.ABBREV_TAC `f2 = (r7 =+ r4) ((r4 =+ 0x1Bw) ((r4 + 0x4w =+ r5 + 0x8w)
1802 SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5 + 8w`,`r7`,`r8`])
1815 \\ Q.UNABBREV_TAC `f2`
1860 \\ Q.ABBREV_TAC `f2 = (r4 + 0x4w =+ r8) ((r4 =+ r7) f)`
1865 SEP_FILL (b,d) * p) (fun2set (f2,df))` suffices_by (STRIP_TAC THEN Q.PAT_X_ASSUM `!xx yy zz. bbb` (MP_TAC o Q.SPECL [`r4 - 8w`,`r5`,`3w`,`r4`])
1871 \\ Q.UNABBREV_TAC `f2`
1900 (Q.ABBREV_TAC `f2
[all...]
H A Dlisp_printScript.sml135 \\ Q.ABBREV_TAC `f2 = (r7 =+ x) ((r6 =+ h) f)`
137 one_list (r7 + 0x1w) ys r7i) (fun2set (f2,df))` by
138 (REWRITE_TAC [WORD_SUB_ADD] \\ Q.UNABBREV_TAC `f2` \\ SEP_WRITE_TAC)
895 \\ Q.ABBREV_TAC `f2 = (r7 =+ w2w (0x27w:word32)) f`
901 (fun2set (f2,df))` by
902 (Q.UNABBREV_TAC `f2`
924 Q.SPECL [`T`,`p * one (r7,0x27w)`,`w1`,`w2`,`r3n`,`r7+1w`,`r8`,`h`,`f2`,`q * fr`,`c`])
1001 \\ Q.ABBREV_TAC `f2 = if b then (r7 =+ 0x28w) f else f`
1008 one_space r72 (LENGTH (s1++s3++s2++p2)) c) (fun2set (f2,df))` by
1010 \\ Q.UNABBREV_TAC `p2` \\ Q.UNABBREV_TAC `f2`
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/
H A DdevScript.sml577 SAFE_DEV f2 (start_f,q,done_f,out) /\
607 DEV f2 (start_f,q,done_f,out) /\
735 DEV f2 (start_f,q,done_f,out) /\
831 DEV f2 (start_f,q,done_f,out) /\
855 DEV f2 (start_f,q,done_f,out) /\ DEV f3 (start_g,q,done_g,data_g)
1162 TOTAL (f1,f2,f3) /\
1167 DEV f2 (start_f,q,done_f,out) /\
1418 `TOTAL (f1,f2,f3) /\
1419 REC (DEV f1) (DEV f2) (DEV f3) (load,inp,done,out) ==>
1420 DEV (TAILREC f1 f2 f
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/
H A DMenu.sml439 val (f2, id) = value
445 val flags = List.foldl Word32.orb 0w0 [f1,f2,f3]
462 val (f2, id) = value
467 val flags = List.foldl Word32.orb 0w0 [f1,f2,f3]
/seL4-l4v-10.1.1/HOL4/src/datatype/record/
H A DRecordType.sml396 fun create_goal((s1, f1),(s2, f2)) = let
398 val (g_t, _) = dom_rng (type_of f2)
402 mk_eq(list_mk_comb(inst s2 f1, [f, list_mk_comb(f2, [g, var])]),
403 list_mk_comb(inst s1 f2, [g, list_mk_comb(f1, [f, var])]))
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A DdecompScript.sml22 (AP_EXT (f1 /\ f2) = (AP_EXT f1) /\ (AP_EXT f2)) /\
23 (AP_EXT (f1 \/ f2) = (AP_EXT f1) \/ (AP_EXT f2)) /\
H A DmuCheck.sml379 fun get_abthms mf f1 f2 cch =
380 let (*FIXME: don't do the extra work if f1 and f2 are the same *)
387 val cab2 = #8(get_cache_entry mf2 f2)
405 | muCheck_aux (args as (msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muAnd(cch,(f1,f2))) =
407 val (abthm,abthnm,mf1,mf2,cab1,cab1nm,cab2,cab2nm) = get_abthms mf f1 f2 cch
408 val tb = cache_get cch ie (BinExp (args,(seth,sel,state,ie)) bdd.And (snd(strip_comb(mf))) vm (f1,f2) dp abthm)
411 (List.nth(msp,3)))) dp [f1,f2] mf seth sel state
413 | muCheck_aux (args as (msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muOr(cch,(f1,f2))) =
415 val (abthm,abthnm,mf1,mf2,cab1,cab1nm,cab2,cab2nm) = get_abthms mf f1 f2 cch
416 val tb = cache_get cch ie (BinExp (args,(seth,sel,state,ie)) bdd.Or (snd(strip_comb(mf))) vm (f1,f2) d
[all...]
/seL4-l4v-10.1.1/HOL4/src/probability/
H A DlebesgueScript.sml2688 ("integrable_add",``!m f1 f2. measure_space m /\ integrable m f1 /\ integrable m f2
2689 ==> integrable m (\x. f1 x + f2 x)``,
2691 >> `(\x. f1 x + f2 x) IN measurable (m_space m, measurable_sets m) Borel`
2694 >> Q.EXISTS_TAC `f2`
2699 >> Q.EXISTS_TAC `(\x. fn_plus f1 x + fn_plus f2 x)`
2703 >> Q.EXISTS_TAC `(\x. fn_minus f1 x + fn_minus f2 x)`
2749 ("integrable_sub",``!m f1 f2. measure_space m /\ integrable m f1 /\ integrable m f2
2750 ==> integrable m (\x. f1 x - f2
[all...]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/
H A Dimproved_gcScript.sml674 ?h2 f2. gc_inv (h1,roots1,h2,f2) (b,i,j2,e,b2,e2,m2,z UNION (D1(CUT(j,j2)m2))) /\ j <= j2 /\
677 (!a. ~(f a = a) ==> (f2 a = f a)) /\
678 (!a. a IN ADDR_SET [x2] ==> ~(f2 a = a)) /\
679 ([x2] = ADDR_MAP f2 [x]) /\ full_heap j j2 m2``,
859 `h2`,`f2`,`m3`,`j3`,`xs4`,`j4`,`m4`])
875 \\ `f2 (f2 n) = n` by FULL_SIMP_TAC std_ss [gc_inv_def,FUN_EQ_THM,abs_gc_inv_def,LET_DEF]
/seL4-l4v-10.1.1/HOL4/examples/Crypto/SHA-1/
H A DSHA1Script.sml206 val f2_def = Define `f2(a,b,c) = (a ?? b ?? c) + C2 : word32`;
250 let (hbar2,wlist2) = Round (Helper f2) 0 hbar1 wlist1 in
/seL4-l4v-10.1.1/graph-refine/
H A Dtrace_refute.py385 f2 = get_body_addrs_fun (addr)
386 if should_avoid_fun (f2) or has_complex_loop (f2):
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/
H A DtranslationsLib.sml1137 fun psl_equivalent2ks_fair_emptyness fast f1 f2 =
1140 val (eval_thm2, cs_free_thm2, ltl_thm2, _) = prepare_psl_term f2;
1142 val to_ltl_thm = ISPECL [f1, f2] PSL_TO_LTL___UF_EQUIVALENT;
1158 fun psl_equivalent2ks_fair_emptyness___num mode fast f1 f2 =
1161 val (eval_thm2, cs_free_thm2, ltl_thm2, _) = prepare_psl_term f2;
1163 val to_ltl_thm = ISPECL [f1, f2] PSL_TO_LTL___UF_EQUIVALENT;
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/model/
H A Driscv.sml7038 val f2 = FPRS rs2 value
7040 case FP32.compare(f1,f2) of
7043 | IEEEReal.GREATER => f2
7045 if ((FP32_IsSignalingNan f1) orelse (FP32_IsSignalingNan f2)) orelse
7046 ((f1 = RV32_CanonicalNan) andalso (f2 = RV32_CanonicalNan))
7048 else if f1 = RV32_CanonicalNan then f2 else f1
7056 val f2 = FPRS rs2 value
7058 case FP32.compare(f1,f2) of
7059 IEEEReal.LESS => f2
7060 | IEEEReal.EQUAL => f2
7250 val f2 = FPRS rs2 value
7259 val f2 = FPRS rs2 value
7268 val f2 = FPRS rs2 value
7285 val f2 = FPRS rs2 value
7319 val f2 = FPRS rs2 value
7353 val f2 = FPRS rs2 value
7528 val f2 = FPRD rs2 value
7546 val f2 = FPRD rs2 value
7750 val f2 = FPRD rs2 value
7759 val f2 = FPRD rs2 value
7768 val f2 = FPRD rs2 value
7785 val f2 = FPRD rs2 value
7819 val f2 = FPRD rs2 value
7853 val f2 = FPRD rs2 value
[all...]

Completed in 219 milliseconds

1234567891011>>