/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/ |
H A D | waaSimplScript.sml | 342 reachRelFromSet (ALTER_A f f0 f1 f2 f3) (BIGUNION f2)` 352 >> `���x. (oneStep (ALTER_A f f0 f1 f2 f3))^* x s ��� ���s. x ��� s ��� s ��� f2` 355 >- (`oneStep (ALTER_A f f0 f1 f2 f3) s s'` by ( 392 >> rename [���reachRel (ALTER_A f f0 f1 f2 f3) b s���, ���b ��� s1���, ���s1 ��� f2���, 395 >- (`oneStep (ALTER_A f f0 f1 f2 f3) s x` by ( 450 ��� q ��� reachRelFromSet (ALTER_A f f0 f1 f2 f3) (BIGUNION f2)` [all...] |
H A D | concrltl2waaScript.sml | 13 ��� (tempDNF_concr (DISJ f1 f2) = (tempDNF_concr f1) ++ (tempDNF_concr f2)) 14 ��� (tempDNF_concr (CONJ f1 f2) = 16 let tDNF2 = tempDNF_concr f2 in 19 ��� (tempDNF_concr (U f1 f2) = [[U f1 f2]]) 20 ��� (tempDNF_concr (R f1 f2) = [[R f1 f2]])`; 123 ��� (props_concr (DISJ f1 f2) = props_concr f1 ++ props_concr f2) [all...] |
H A D | gbaSimplScript.sml | 224 >- (rename [���reachableFromGBA (GBA f f0 f1 f2 f3) x s���, ���x ��� f0���] 226 >> `stepGBA (GBA f f0 f1 f2 f3) s d` suffices_by metis_tac[RTC_CASES2] 340 e ��� reachableFromSetGBA (GBA f' f0 f1 f2 f3) f0}) 341 ��� T' ��� f2` suffices_by metis_tac[] 458 (* >> Cases_on `equivalentStates f2 f1 x y` *) 527 (* >- (qabbrev_tac `aut = GBA f f0 f1 f2 f3` *) 533 (* >- (qabbrev_tac `aut = GBA f f0 f1 f2 f3` *) 543 (* >> Cases_on `���q'. q' ��� f ��� q' ��� q ��� equivalentStates f2 f1 q' q` *)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/ |
H A D | arm_improved_gcScript.sml | 351 ?f2. arm_move_pre (r1,ref_heap_addr x,ref_addr j,df,f) /\ 352 (arm_move (r1,ref_heap_addr x,ref_addr j,df,f) = (r1,ref_addr j2,df,f2)) /\ 353 (one (r1,ref_heap_addr x2) * ref_mem m2 ij je * ref_mem m2 b2 e2 * p) (fun2set (f2,df)) /\ 503 ?f2 h3 f3. 505 (arm_move_list (r1,ref_addr j,n2w (LENGTH xs),df,f) = (r1 + n2w (4 * LENGTH xs),ref_addr j2,df,f2)) /\ 506 (ref_mem m2 ij je * ref_mem m2 b2 e2 * one_list r1 (MAP ref_heap_addr ys) * p) (fun2set (f2,df)) /\ 556 ?f2 h3 f3. 558 (arm_move_roots (r1,ref_addr j,df,f) = (ref_addr j2,df,f2)) /\ 559 (ref_mem m2 ij je * ref_mem m2 b2 e2 * one_list_roots r1 ys * p) (fun2set (f2,df)) /\ 615 ?f2 [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/just-in-time/ |
H A D | jit_codegenScript.sml | 278 \\ Q.ABBREV_TAC `f2 = (r1 =+ n2w y) f` 279 \\ `(x * one (r1,n2w y)) (fun2set (f2,df))` by 280 (Q.UNABBREV_TAC `f2` \\ SEP_WRITE_TAC) 466 \\ Q.ABBREV_TAC `f2 = (a + 0x4w =+ n2w (w2n c)) ((a =+ 0xE9w) f)` 470 one (a + 0x4w,n2w (w2n (c:word7)))) (fun2set (f2,df))` by 471 (Q.UNABBREV_TAC `f2` \\ SEP_WRITE_TAC) 476 `b2`,`f2`,`df`,`a+4w`,`r4`,`r3`]) x86_addr_thm 489 \\ Q.PAT_ABBREV_TAC `f2 = (a + 0x7w =+ (n2w (w2n (c:word7))):word8) ff` 495 one (a + 0x7w,n2w (w2n (c:word7)))) (fun2set (f2,df))` by 496 (Q.UNABBREV_TAC `f2` \\ SEP_WRITE_TA [all...] |
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | KeyMap.sml | 569 fun treeMerge f1 f2 fb tree1 tree2 = 571 E => treeMapPartial f2 tree2 575 | T node2 => nodeMerge f1 f2 fb node1 node2 577 and nodeMerge f1 f2 fb node1 node2 = 583 val left = treeMerge f1 f2 fb l left 584 and right = treeMerge f1 f2 fb r right 588 NONE => f2 (key,value) 605 fun treeUnion f f2 tree1 tree2 = 611 | T node2 => nodeUnion f f2 node1 node2 613 and nodeUnion f f2 node 1184 fun f2 kv = f (kv,kv) function [all...] |
H A D | Map.sml | 561 fun treeMerge compareKey f1 f2 fb tree1 tree2 = 563 E => treeMapPartial f2 tree2 567 | T node2 => nodeMerge compareKey f1 f2 fb node1 node2 569 and nodeMerge compareKey f1 f2 fb node1 node2 = 575 val left = treeMerge compareKey f1 f2 fb l left 576 and right = treeMerge compareKey f1 f2 fb r right 580 NONE => f2 (key,value) 597 fun treeUnion compareKey f f2 tree1 tree2 = 603 | T node2 => nodeUnion compareKey f f2 node1 node2 605 and nodeUnion compareKey f f2 node 1176 fun f2 kv = f (kv,kv) function [all...] |
H A D | TermNet.sml | 35 | (Fn f1, Fn f2) => fnCmp f1 f2 qs 45 fun compareFnQterm (f1,f2) = fnCmp f1 f2 []; 50 fun equalFnQterm f1 f2 = compareFnQterm (f1,f2) = EQUAL;
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | KeyMap.sml | 569 fun treeMerge f1 f2 fb tree1 tree2 = 571 E => treeMapPartial f2 tree2 575 | T node2 => nodeMerge f1 f2 fb node1 node2 577 and nodeMerge f1 f2 fb node1 node2 = 583 val left = treeMerge f1 f2 fb l left 584 and right = treeMerge f1 f2 fb r right 588 NONE => f2 (key,value) 605 fun treeUnion f f2 tree1 tree2 = 611 | T node2 => nodeUnion f f2 node1 node2 613 and nodeUnion f f2 node 1184 fun f2 kv = f (kv,kv) function [all...] |
H A D | Map.sml | 561 fun treeMerge compareKey f1 f2 fb tree1 tree2 = 563 E => treeMapPartial f2 tree2 567 | T node2 => nodeMerge compareKey f1 f2 fb node1 node2 569 and nodeMerge compareKey f1 f2 fb node1 node2 = 575 val left = treeMerge compareKey f1 f2 fb l left 576 and right = treeMerge compareKey f1 f2 fb r right 580 NONE => f2 (key,value) 597 fun treeUnion compareKey f f2 tree1 tree2 = 603 | T node2 => nodeUnion compareKey f f2 node1 node2 605 and nodeUnion compareKey f f2 node 1176 fun f2 kv = f (kv,kv) function [all...] |
H A D | TermNet.sml | 35 | (Fn f1, Fn f2) => fnCmp f1 f2 qs 45 fun compareFnQterm (f1,f2) = fnCmp f1 f2 []; 50 fun equalFnQterm f1 f2 = compareFnQterm (f1,f2) = EQUAL;
|
/seL4-l4v-10.1.1/HOL4/examples/dev/ |
H A D | composeScript.sml | 438 (* TOTAL(f1,f2,f3) checks the termination for *) 439 (* TAILREC f1 f2 f3 = \x. if (f1 x) then (f2 x) else TAILREC f1 f2 f3 (f3 x) *) 444 `TOTAL(f1,f2,f3) = 448 TotalDefn.DefineSchema `TAILREC x = if f1 x then f2 x else TAILREC (f3 x)`; 451 (`!f1 f2 f3 x. 453 (TAILREC f1 f2 f3 x = if f1 x then f2 x else TAILREC f1 f2 f [all...] |
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | optionScript.sml | 360 ``!opt1 opt2 f1 f2. 361 (opt1 = opt2) /\ (!x. (opt2 = SOME x) ==> (f1 x = f2 x)) ==> 362 (OPTION_MAP f1 opt1 = OPTION_MAP f2 opt2)``, 408 ``!x1 x2 y1 y2 f1 f2. 410 (!x y. (x2 = SOME x) /\ (y2 = SOME y) ==> (f1 x y = f2 x y)) ==> 411 (OPTION_MAP2 f1 x1 y1 = OPTION_MAP2 f2 x2 y2)``, 468 `!o1 o2 f1 f2. 469 (o1:'a option = o2) /\ (!x. (o2 = SOME x) ==> (f1 x = f2 x)) ==> 470 (OPTION_BIND o1 f1 = OPTION_BIND o2 f2)`,
|
/seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
H A D | quotient_pred_setScript.sml | 184 !f1 f2. 185 (R1 ===> (R2 ### $=)) f1 f2 ==> 186 (R2 ===> $=) (GSPECR R1 R2 f1) (GSPECR R1 R2 f2)���), 919 !f1 f2 s1 s2. 920 (R1 ===> R2) f1 f2 /\ (R1 ===> $=) s1 s2 ==> 921 (R2 ===> $=) (IMAGER R1 R2 f1 s1) (IMAGER R1 R2 f2 s2)���), 947 !f1 f2 s1 s2. 948 (R1 ===> R2) f1 f2 /\ (R1 ===> $=) s1 s2 ==> 949 (R2 ===> $=) (IMAGE f1 s1) (IMAGE f2 s2)���),
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/powerpc/ |
H A D | darwin.S | 153 lfd f2, -SAVE_REGS_SIZE-(12*FPR_SIZE)(r28) 228 stfd f2, -SAVE_REGS_SIZE-(12*FPR_SIZE)(r28) 262 stfd f2,FPR_SIZE(r30)
|
H A D | linux64_closure.S | 127 stfd %f2, -104+(1*8)(%r1) 209 lfd %f2, RETVAL+8(%r1) 288 lfs %f2, RETVAL+4(%r1) 293 lfd %f2, RETVAL+8(%r1)
|
H A D | darwin_closure.S | 160 stfd f2, (FP_SAVE_BASE + FPR_SIZE )(r1) 252 lfd f2,8(r5) 427 lfd f2, (FP_SAVE_BASE + FPR_SIZE )(r1)
|
/seL4-l4v-10.1.1/HOL4/examples/computability/register/ |
H A D | regScript.sml | 96 ``!prog pc args f1 f2. 98 isExecution prog pc args f2 ==> (f1=f2)``, 735 qmatch_abbrev_tac `Q ei f1 ��� Q ei f2` >> 736 qsuff_tac `f1 = f2` >> srw_tac [][] >> 737 srw_tac [][Abbr`f2`, Abbr`f1`, saferead_update, 922 qmatch_abbrev_tac `Q ei f1 ==> Q ei f2` >> 923 qsuff_tac `f1 = f2` >- srw_tac [][] >> 924 srw_tac [ARITH_ss][Abbr`f1`, Abbr`f2`, FUN_EQ_THM, 941 qpat_x_assum `QQ (bi + 3) f2` mp_ta [all...] |
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/ |
H A D | psl_to_rltlScript.sml | 96 (PSL_TO_RLTL (F_AND(f1,f2)) = RLTL_AND(PSL_TO_RLTL f1,PSL_TO_RLTL f2)) 100 (PSL_TO_RLTL (F_UNTIL(f1,f2)) = RLTL_SUNTIL(PSL_TO_RLTL f1,PSL_TO_RLTL f2)) 991 ``!f1 f2. F_CLOCK_SERE_FREE f1 ==> F_CLOCK_SERE_FREE f2 ==> 992 (UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f1 f2 = 993 LTL_IS_CONTRADICTION (LTL_NOT (LTL_EQUIV(PSL_TO_LTL f1, PSL_TO_LTL f2))))``, 997 `F_CLOCK_SERE_FREE (F_NOT (F_IFF (f1,f2)))` by 1074 (FUTURE_LTL_TO_PSL (LTL_AND(f1,f2)) [all...] |
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Ho_Net.sml | 46 | (FVnet f1, FVnet f2) => pair_compare (String.compare, Int.compare) 47 (f1, f2)
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | omega_automatonScript.sml | 63 [`P`,`\(f1,f2). P f1 /\ P f2`]
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/s390/ |
H A D | sysv.S | 70 ld %f2,40(%r11) 126 std %f2,72(%r15) 271 ld %f2,56(%r11) 328 std %f2,136(%r15)
|
/seL4-l4v-10.1.1/HOL4/examples/lambda/other-models/ |
H A D | diagsScript.sml | 146 (evalform (f1 /\ f2) R <=> evalform f1 R /\ evalform f2 R) /\ 214 (f1:('a,'b,'c)diaform) ==> f2 <=> ~(f1 /\ ~f2)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | rulesScript.sml | 322 `!ir1 ir2 pre_p1 post_p1 post_p2 stk_f in_f1 f1 f2 out_f1 out_f2. 324 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) 326 PSPEC (SC ir1 ir2) (pre_p1,post_p2) stk_f (in_f1,f2 o f1,out_f2)`, 334 `!cond ir_t ir_f pre_p post_p stk_f cond_f in_f f1 f2 out_f. 337 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) 339 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)`, 519 `!ir1 ir2 pre_p1 post_p1 post_p2 stk vi1 f1 vo1 f2 vo2. 521 VSPEC ir1 (pre_p1,post_p1) stk (vi1,f1,vo1) /\ VSPEC ir2 (post_p1,post_p2) stk (vo1,f2,vo2) 523 VSPEC (SC ir1 ir2) (pre_p1,post_p2) stk (vi1,f2 o f1,vo2)`, 530 `!cond ir_t ir_f pre_p post_p stk cond_f iv f1 f2 o [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/test/ |
H A D | test.sml | 12 `f2 ((y,z),(k0,k1,k2,k3),sum) = 22 |- f2 ((y,z),(k0,k1,k2,k3),sum) = 55 |- f2 =
|