/seL4-l4v-10.1.1/l4v/tools/haskell-translator/ |
H A D | make_spec.sh | 38 SPEC=$(find_dir "spec/design") 54 SKEL="$SPEC/skel" 55 MSKEL="$SPEC/m-skel" 57 MACH="$SPEC/../machine" 62 echo "(this script may have found the wrong spec $SPEC)" 104 mkdir -p "$SPEC/${arch}" 116 echo "$SKEL/${arch}/$NAME --> $SPEC/${arch}/$NAME" 145 for thy in $SPECNONARCH/${ARCHES[0]}/*.thy; do rsync -c "$thy" "$SPEC/"; done 147 echo Built from git repo at $L4CAP by $USER > $SPEC/version 148 echo >> $SPEC/versio [all...] |
/seL4-l4v-10.1.1/HOL4/tools/Holmake/tests/gh604/base/ |
H A D | base1Script.sml | 6 SPEC ���p:bool��� AND_CLAUSES);
|
H A D | base2Script.sml | 6 SPEC ���q:bool��� AND_CLAUSES);
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | progScript.sml | 34 SPEC ((to_set,next,instr,less,allow):('a,'b,'c)processor) p c q = 61 ``!x. RUN x p q = SPEC x p {} q``, 67 ``!x p c q. SPEC x p c q ==> !r. SPEC x (p * r) c (q * r)``, 74 ``!x c q. SPEC x SEP_F c q``, 81 ``!x p c q. SPEC x p c q ==> !r. SEP_IMP r p ==> SPEC x r c q``, 89 ``!x p c q. SPEC x p c q ==> !r. SEP_IMP q r ==> SPEC x p c r``, 101 ``!x p c q. SPEC [all...] |
/seL4-l4v-10.1.1/HOL4/src/num/reduce/src/ |
H A D | Boolconv.sml | 48 else let val xn' = dest_neg xn in SPEC xn c3 end 68 in if xn = T then SPEC yn c1 else 69 if yn = T then SPEC xn c2 else 70 if xn = F then SPEC yn c3 else 71 if yn = F then SPEC xn c4 else 72 if xn = yn then SPEC xn c5 else 76 (SPEC xn c5) 97 in if xn = T then SPEC yn c1 else 98 if yn = T then SPEC xn c2 else 99 if xn = F then SPEC y [all...] |
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/ |
H A D | mk_T.ml | 54 let th1 = EQ_MP (RIGHT_BETA(AP_THM(SPEC p L_AX )w)) (ASSUME "L ^p ^w") 56 let th2 = GEN w (DISCH "L ^p ^w" (MP (SPEC w th1) (SPEC w R_REFL))) 58 let th3 = AP_THM (SPEC "L ^p" (SPEC p imp_AX)) w 59 and th4 = RIGHT_BETA(AP_THM(SPEC "L ^p" (SPEC "not ^p" or_AX))w)
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/computer/ |
H A D | proof3.ml | 74 (SPECL [(tm i);(tm n)] (SPEC "ready:num->bool" NEXT_INC_INTERVAL_LEMMA)) 79 (SPECL [(tm 0);(tm n);"t2:num"] (SPEC "ready:num->bool" NEXT_IDENTITY_LEMMA)) 85 (SPEC (tm (n - 1))(SPEC "ready:num->bool" NEXT_INC_LEMMA)) 92 let th1 = (SUBS [SPEC (tm 0) ADD1] (SPEC (tm 0) LESS_SUC_REFL)) in 93 let th2 = (SUBS [SPEC (tm 1) ADD1] (SPEC (tm 1) LESS_SUC_REFL)) in 97 let th1 = (SUBS [SPEC (tm 0) ADD1] (SPEC (t [all...] |
H A D | proof1.ml | 93 let th1 = SPEC "t1:num" COMPUTER_IMP_ready in 99 let th7 = SPEC "(ready (t1:num)):bool" F_IMP in 102 MP (SPEC "mpc (t1:num) = ^tm" lemma1) th9;; 141 (SPEC "(mpc (t1:num)):word5" word5_CASES);; 145 let th3 = SPEC "t1:num" COMPUTER_IMP_idle;; 151 let th9 = SPEC "(idle (t1:num)):bool" F_IMP;; 154 let th12 = MP (SPEC "mpc (t1:num) = #00101" lemma1) th11;; 166 let th3 = SPEC "t1:num" COMPUTER_IMP_idle;; 172 let th9 = SPEC "(idle (t1:num)):bool" F_IMP;; 175 let th12 = MP (SPEC "mp [all...] |
H A D | proof6.ml | 82 let th1 = MP (SPECL ["0";"n:num"] LESS_SUC_IMP) (SPEC "n:num" LESS_0);; 92 let th1 = MP (SPEC "ready:num->bool" LEAST) (ASSUME "?t:num. ready t");; 96 let th5 = CHOOSE ("t:num",(SPEC "t1:num" infinitely_ready)) th4;; 106 let th4 = CONJUNCT2 (CONJUNCT2 (CONJUNCT2 (SPEC "~b2" EQ_CLAUSES)));; 109 let th7 = CONJUNCT1 (CONJUNCT2 (CONJUNCT2 (SPEC "~b3" OR_CLAUSES)));; 116 let th1 = SPEC "t:num" num_CASES;; 120 let th5 = SYM (CONJUNCT2 (CONJUNCT2 (CONJUNCT2 (SPEC "n = 0" EQ_CLAUSES))));; 134 let th1 = SPEC "(abs m ready):num" infinitely_ready;; 135 let th2 = SPEC (mk_abs ("t2:num",(snd (dest_exists (concl th1))))) LEAST;; 217 expand (PURE_REWRITE_TAC [SYM (SPEC " [all...] |
/seL4-l4v-10.1.1/HOL4/src/HolSat/vector_def_CNF/ |
H A D | defCNFScript.sml | 64 Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `n`) THEN 90 MP_TAC (Q.SPEC `n` th) THEN 91 MP_TAC (Q.SPEC `x` th) THEN 92 MP_TAC (Q.SPEC `x'` th)) THEN 96 MP_TAC (Q.SPEC `n` th) THEN 97 MP_TAC (Q.SPEC `x` th)) THEN 101 MP_TAC (Q.SPEC `n` th) THEN 102 MP_TAC (Q.SPEC `x` th)) THEN 106 MP_TAC (Q.SPEC `n` th)) THEN 133 Q.PAT_X_ASSUM `!v:num->bool. A v` (MP_TAC o Q.SPEC ` [all...] |
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/tamarack2/ |
H A D | mod.ml | 61 (STRIP_ASSUME_TAC o (SPEC "(k * m) + n")) EXISTS_MOD THEN 72 (CONJUNCT2 (SPEC "m * 1" (GEN "m" ADD_CLAUSES))))) THEN 83 (REWRITE_RULE [MULT_CLAUSES;ADD_CLAUSES]) o (SPEC "0")) MOD_THM);; 89 HOL_IMP_RES_THEN (STRIP_ASSUME_TAC o (SPEC "n")) EXISTS_MOD);; 97 (\thm. SUBST_OCCS_TAC [[2],CONJUNCT1 thm])) o (SPEC "n")) 108 (SPEC "n * m" (GEN "m" (CONJUNCT1 (CONJUNCT2 ADD_CLAUSES))))) THEN 115 HOL_IMP_RES_THEN (ASSUME_TAC o (SPEC "n")) MOD_LESS_THM THEN 116 HOL_IMP_RES_THEN (ASSUME_TAC o (SPEC "0")) MOD_THM THEN 126 (\thm. SUBST_OCCS_TAC [[1],CONJUNCT1 thm])) o (SPEC "n")) 132 REWRITE_TAC [MATCH_MP MOD_THM (SPEC " [all...] |
H A D | wop.ml | 28 (BETA_RULE (SPEC "\n. P n ==> (?n. P n /\ (!m. m < n ==> ~P m))" 38 (SPEC "!m. m < n ==> ~(P m)" EXCLUDED_MIDDLE)) THENL [
|
H A D | div.ml | 61 (STRIP_ASSUME_TAC o (SPEC "(k * m) + n")) EXISTS_DIV THEN 71 (SPEC "n")) EXISTS_DIV THEN 79 (DISJ_CASES_TAC o (REWRITE_RULE [LESS_OR_EQ]) o (SPEC "n")) 102 (SPEC "n")) EXISTS_DIV THEN 107 (SPEC "p")) EXISTS_DIV THEN 121 ASSUME_TAC (SPEC "(p Div m) * m" LESS_EQ_REFL) THEN
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/mos-count/ |
H A D | regn.ml | 90 let w1t0 = REWRITE_RULE [ASSUME "phiA ^t0 = Hi"] (SPEC t0 w1thm);; 93 [ASSUME "phiA ^t1 = Lo";val_not_eq_ax] (SPEC t1 w1thm);; 96 [ASSUME "phiA ^t2 = Lo";val_not_eq_ax] (SPEC t2 w1thm);; 97 let w2t1 = REWRITE_RULE [SUC_SUB1;w1t1;w1t0] (SPEC t1 w2thm);; 98 let w2t2 = REWRITE_RULE [SUC_SUB1;w1t2;w1t1] (SPEC t2 w2thm);; 99 let w3t2 = REWRITE_RULE [SUC_SUB1;w2t2;w2t1] (SPEC t2 w3thm);; 100 let w3t2 = REWRITE_RULE [SUC_SUB1;w2t2;w2t1] (SPEC t2 w3thm);; 101 let w4t2 = REWRITE_RULE [ASSUME "phiB ^t2 = Hi";w3t2] (SPEC t2 w4thm);; 104 [ASSUME "phiB ^t3 = Lo";val_not_eq_ax] (SPEC t3 w4thm);; 107 [ASSUME "phiB ^t4 = Lo";val_not_eq_ax] (SPEC t [all...] |
H A D | tempabs.ml | 54 PURE_REWRITE_TAC [Next;SYM (SPEC "t" ADD1)] THEN 67 PURE_REWRITE_TAC [Next;SYM (SPEC "t" ADD1)] THEN 84 DISJ_CASES_TAC (SPEC "t2 = t3" EXCLUDED_MIDDLE) THENL 86 DISJ_CASES_TAC (SPEC "t2 < t3" EXCLUDED_MIDDLE) THENL 90 let th1 = SPEC "t" (PURE_REWRITE_RULE [Inf] (ASSUME "Inf g"));; 110 let th3 = SPEC "t" (PURE_REWRITE_RULE [Inf] (ASSUME "Inf g"));; 143 (SELECT_RULE (SPEC "n" (ASSUME "!n. ?t. IsTimeOf n g t")))));; 150 DISJ_CASES_TAC (SPEC "n" num_CASES) THENL 154 (SPEC "0" (ASSUME "!n. IsTimeOf n g (TimeOf g n)"))); 161 (SPEC "SU [all...] |
/seL4-l4v-10.1.1/HOL4/examples/ind_def/ |
H A D | opsemScript.sml | 180 `SPEC P c Q = !s1 s2. P s1 /\ EVAL c s1 s2 ==> Q s2`; 189 ``!P. SPEC P Skip P``, 199 SPEC (\s. P (s |+ (v,neval e s))) (Assign v e) P``, 209 SPEC P c1 Q /\ SPEC Q c2 R ==> SPEC P (Seq c1 c2) R``, 219 SPEC (\s. P(s) /\ beval b s) c1 Q /\ 220 SPEC (\s. P(s) /\ ~beval b s) c2 Q ==> SPEC P (Cond b c1 c2) Q``, 241 ``!P b c. SPEC (\ [all...] |
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/ |
H A D | PFset_conv.sml | 51 fun itfn ith x th = SPEC x (MP (SPEC (rand(concl th)) ith) th) 95 (EQF_INTRO (SPEC ``x:'a`` pred_setTheory.NOT_IN_EMPTY)) 99 val F_OR = el 3 (CONJUNCTS (SPEC gv OR_CLAUSES)) 100 val OR_T = el 2 (CONJUNCTS (SPEC gv OR_CLAUSES)) 103 val thm = SPEC S' (SPEC y ith) 169 val thm = SPEC S' (SPEC y ith) 213 val thm = SPEC [all...] |
/seL4-l4v-10.1.1/HOL4/src/bool/ |
H A D | boolScript.sml | 346 val th = SPEC (rator cmb) (INST_TYPE tysubst ETA_AX) 353 val th1 = SPEC Bvar th 385 fun FALSITY_CONV tm = DISCH F (SPEC tm (EQ_MP F_DEF (ASSUME F))) 415 (* SPEC could be built here. *) 427 let val th0 = SPEC t BOOL_CASES_AX 429 val th2 = SPEC (subst[(x|->t)] P) th1 in 465 MP (MP (SPEC conseq (SPEC ant IMP_ANTISYM_AX)) th1) th2 475 fun CONTR tm th = MP (SPEC tm FALSITY) th 499 fun SPECL tm_list th = rev_itlist SPEC tm_lis [all...] |
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
H A D | MMU_SetupScript.sml | 33 (CONJ (SPEC ``guest1_min_adr:word32`` inequal_by_inequalities_gtu_lem) 34 (CONJ (SPEC ``guest1_max_adr:word32`` inequal_by_inequalities_gtu_lem) 35 (CONJ (SPEC ``guest1_min_adr:word32`` inequal_by_inequalities_ltu_lem) 36 (CONJ (SPEC ``guest1_max_adr:word32`` inequal_by_inequalities_ltu_lem) 37 (CONJ (SPEC ``guest2_min_adr:word32`` inequal_by_inequalities_gtu_lem) 38 (CONJ (SPEC ``guest2_max_adr:word32`` inequal_by_inequalities_gtu_lem) 39 (CONJ (SPEC ``guest2_min_adr:word32`` inequal_by_inequalities_ltu_lem) 40 (CONJ (SPEC ``guest2_max_adr:word32`` inequal_by_inequalities_ltu_lem) 41 (CONJ (SPEC ``guest1_min_adr:word32`` inequal_by_inequalities_gt_lem) 42 (CONJ (SPEC ``guest1_max_ad [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/dff/ |
H A D | tempabsScript.sml | 82 val wop_spec = SPEC lam WOP 167 (SPEC ``t:num`` num_CASES) THENL 182 [POP_ASSUM (STRIP_ASSUME_TAC o SPEC ``t:num``) THEN 185 POP_ASSUM (STRIP_ASSUME_TAC o SPEC ``SUC t``) THENL 252 (REPEAT_TCL STRIP_THM_THEN) SUBST1_TAC (SPEC ``n:num`` num_CASES) THEN 342 (ASSUME_TAC o SELECT_RULE o (SPEC ``SUC n``)) Istimeof_thm4 THEN 360 DISCH_THEN (STRIP_ASSUME_TAC o SPEC ``n:num``) THEN 371 DISCH_THEN (STRIP_ASSUME_TAC o SPEC ``n:num``) THEN 382 STRIP_ASSUME_TAC (SPEC ``n:num`` num_CASES) THEN 405 (STRIP_THM_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1 o SPEC `` [all...] |
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | numposrepLib.sml | 19 fun l2n_pow2 i = rule (Thm.SPEC (f i) thm) 20 fun n2l_pow2 i = rule (Thm.SPEC (f i) n2l_pow2_compute)
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | Thm_convs.sml | 60 val OR_F_CONV = REWR_CONV (el 3 (CONJUNCTS (SPEC (���x:bool���) OR_CLAUSES))); 99 SPEC (���n:num���) (arithmeticTheory.SUC_ONE_ADD)] 107 (SUBS [SPEC (���m:num���) (arithmeticTheory.SUC_ONE_ADD)] 116 (SUBS [SPEC (���m:num���) (arithmeticTheory.SUC_ONE_ADD)] 124 (SUBS [SPEC (���n:num���) (arithmeticTheory.SUC_ONE_ADD)] 131 (SUBS [SPEC (���m:num���) (arithmeticTheory.SUC_ONE_ADD), 132 SPEC (���n:num���) (arithmeticTheory.SUC_ONE_ADD)] 149 (SPEC ���b:num���
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/cantor/ |
H A D | Cantor.ml | 5 let Th2 = SPEC "\x. ~((FN:*->*->bool) x x)" Th1;;
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | normalFormsScript.sml | 17 val A1 = SPEC (Term `\x. ^f x = ^g x`) LEFT_EXISTS_IMP_THM 18 val A2 = SPEC (Term `^f = ^g`) A1 24 val A8 = SPEC (Term `\g x. (^f x = g x) ==> (^f = g)`) A7 37 SPEC (Term `\f x. !(g:'a->'b). (f (x g) = g (x g)) ==> (f = g)`) A15
|
/seL4-l4v-10.1.1/HOL4/src/rational/ |
H A D | intExtensionLib.sml | 39 MATCH_MP_TAC (SPEC term1 INT_SGN_CASES) THEN REPEAT CONJ_TAC THEN STRIP_TAC
|