| /seL4-l4v-10.1.1/HOL4/src/coretypes/ |
| H A D | sumScript.sml | 190 REPEAT STRIP_TAC THEN STRIP_ASSUME_TAC (SPEC ���s:('a,'b)sum��� A_ONTO) THEN
359 STRIP_ASSUME_TAC (SPEC ���x:('a,'b)sum��� sum_CASES) THEN
366 STRIP_ASSUME_TAC (SPEC ���x:('a,'b)sum��� sum_CASES) THEN
374 STRIP_ASSUME_TAC (SPEC ���x:('a,'b)sum��� sum_CASES) THEN
|
| /seL4-l4v-10.1.1/HOL4/src/prekernel/ |
| H A D | FinalThm-sig.sml | 62 val SPEC : term -> thm -> thm value
|
| /seL4-l4v-10.1.1/HOL4/src/simp/src/ |
| H A D | Opening.sig | 10 * fun refl x = SPEC x thm;
|
| /seL4-l4v-10.1.1/HOL4/examples/lambda/barendregt/ |
| H A D | takahashiScript.sml | 96 |> Q.SPEC `��M N. P M N ��� M =��=> N`
|
| /seL4-l4v-10.1.1/HOL4/examples/lambda/typing/ |
| H A D | contextlistsScript.sml | 105 val PERM_RULES = LIST_CONJ [Q.SPEC `[]` PERM_REFL,
|
| /seL4-l4v-10.1.1/HOL4/examples/logic/ |
| H A D | foltypesScript.sml | 297 |> Q.SPEC `��n t0 x. (n = 0) ��� Q t0 x`
346 |> Q.SPEC `��n t0 x. (n = 1) ��� Q t0 x`
389 fof_ind |> Q.SPEC `��f x. Q f` |> Q.SPEC `��x. X` |> SIMP_RULE (srw_ss()) []
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
| H A D | priv_constraints_spsrScript.sml | 367 THEN ASSUME_TAC (SPEC ``s:arm_state`` read_cpsr_fixed_lem)
495 SPEC ``27w:word5`` constT_sfc_ut_thm]
587 IMP_RES_TAC (SPEC r' (
593 (fn thm => ASSUME_TAC (SPEC ``s:arm_state`` thm))
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | GraphLangScript.sml | 205 (* representation in ARM SPEC *)
247 (* representation in M0 SPEC *)
357 | ARM arm_c => SPEC ARM_MODEL (arm_STATE s * arm_PC n) arm_c
359 | M0 m0_c => SPEC M0_MODEL (m0_STATE s * m0_PC n) m0_c
1297 ``SPEC ARM_MODEL (arm_assert_for ((NextNode i,st,name)::t)) code
1301 ``SPEC M0_MODEL (m0_assert_for ((NextNode i,st,name)::t)) code
1341 SPEC ^model_tm (^assert_for_tm s1) code (^assert_for_tm s2)``,
1581 \\ ASSUME_TAC (DIVISION |> Q.SPEC `2` |> SIMP_RULE std_ss []
1582 |> GSYM |> Q.SPEC `n`)
1598 \\ ASSUME_TAC (DIVISION |> Q.SPEC `
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/ |
| H A D | alphaScript.sml | 914 (map (fn tm => MP_TAC (SPEC_ALL (SPEC tm ALPHA1_height_induct_LEMMA)))
933 THEN STRIP_ASSUME_TAC (SPEC x th)
1031 THEN POP_ASSUM (MP_TAC o SPEC ���y:var���)
1032 THEN POP_ASSUM (MP_TAC o SPEC ���v:var���)
1039 THEN POP_ASSUM (MP_TAC o SPEC ���y:var���)
1040 THEN POP_ASSUM (MP_TAC o SPEC ���v:var���)
1232 THEN DISCH_THEN (MP_TAC o SPEC ���FV_obj1 (SUB1 s x)���)
1234 THEN POP_ASSUM (MP_TAC o SPEC ���x:var���)
1374 THEN POP_ASSUM (STRIP_ASSUME_TAC o SPEC ���FV_obj1 (SUB1 s x')���)
1376 [ POP_ASSUM (STRIP_ASSUME_TAC o SPEC ���
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | CooperCore.sml | 264 SPEC y (MATCH_MP INT_DIVIDES_RMUL ldel_divides)
276 SPEC y (MATCH_MP INT_DIVIDES_RMUL ldel_divides)
360 val delta_ok = CONJ zero_lt_delta (SPEC delta_tm INT_LE_REFL)
583 SYM (SPEC e elim_neg_ones)
646 val disj2_exm = SPEC disj2 EXCLUDED_MIDDLE
786 val e_eq_e11 = SYM (SPEC e elim_minus_ones)
960 val e_eq_11 = SYM (SPEC e elim_neg_ones)
1071 SPEC change_by_dmultiples with u, and MP with zero_lt_u to get
1074 val Fx0_less_ud = MP (SPEC u change_by_dmultiples) zero_lt_u
1075 (* SPEC choose_lemm
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/probability/ |
| H A D | probabilityScript.sml | 256 Q.SPEC `(p_space p, events p)`) ALGEBRA_INTER
263 Q.SPEC `(p_space p, events p)`) ALGEBRA_EMPTY
270 Q.SPEC `(p_space p, events p)`) ALGEBRA_SPACE
278 Q.SPEC `(p_space p, events p)`) ALGEBRA_UNION
301 Q.SPEC `(p_space p, events p)`) ALGEBRA_DIFF
309 Q.SPEC `(p_space p, events p)`) ALGEBRA_COMPL
317 Q.SPEC `(p_space p, events p)`) SIGMA_ALGEBRA_COUNTABLE_UNION
613 (prob p s = SIGMA (\x. prob p {x}) s)` (MP_TAC o GSYM o Q.SPEC `p`)
641 >> (MATCH_MP_TAC o UNDISCH o Q.SPEC `s`) REAL_SUM_IMAGE_FINITE_SAME
868 (MP_TAC o Q.SPEC `(\
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/CCS/ |
| H A D | StrongLawsScript.sml | 136 (SPEC ``E :('a, 'b) CCS`` STRONG_SUM_IDENT_R)));
191 (SPEC ``E :('a, 'b) CCS``
196 (SPEC ``E' :('a, 'b) CCS``
198 (SPEC ``E :('a, 'b) CCS`` STRONG_SUM_IDEMP)))))));
210 (SPEC ``E' :('a, 'b) CCS``
212 (SPEC ``E'' :('a, 'b) CCS``
215 (SPEC ``E' :('a, 'b) CCS``
344 (SPEC ``E :('a, 'b) CCS`` STRONG_PAR_IDENT_R)));
606 (CONJ (SPEC ``tau :'b Action``
609 (SPEC ``
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
| H A D | lisp_opsScript.sml | 78 val th = SPEC f (MATCH_MP SPEC_FRAME th)
82 val th = SPEC x (MATCH_MP SPEC_FRAME th)
83 val th = SPEC post_tm (MATCH_MP SPEC_WEAKEN th)
125 val th = SPEC (mk_cond_star(pre_tm,pre)) th
301 val th = RW [Q.SPEC `n2w n` WORD_AND_COMM] th
471 val lisp_inv_0 = (DISCH_ALL o SIMP_RULE std_ss [] o Q.SPEC `0` o UNDISCH) lisp_inv_Val
472 val lisp_inv_1 = (DISCH_ALL o SIMP_RULE std_ss [] o Q.SPEC `1` o UNDISCH) lisp_inv_Val
1071 val th = RW [Q.SPEC `f y` SEP_HIDE_def] th
1073 val th = SPEC (mk_var("r5",``:word32``)) th
1086 val th = SPEC (mk_va
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/ |
| H A D | dpll.sml | 76 Unsat (DISJ_CASES (SPEC v BOOL_CASES_AX) l_false r_false)
122 spec (SPEC (f (#1 (dest_forall (concl th)))) th)
|
| /seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
| H A D | eq_cmp_bmapScript.sml | 222 >> STRIP_ASSUME_TAC (SPEC ``k:'a->bool`` SET_CASES)
224 >- (STRIP_ASSUME_TAC (SPEC ``t:'a->bool`` SET_CASES)
|
| H A D | regexpLib.sml | 147 (SPEC regexp_tm Brzozowski_partial_eval_conseq)
151 val dfa_thm1 = SPEC stm dfa_thm
|
| /seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/for/ |
| H A D | for_compileScript.sml | 182 (FIRST_X_ASSUM (MP_TAC o Q.SPEC `r'`)
183 \\ FIRST_X_ASSUM (MP_TAC o Q.SPEC `s`)
186 \\ FIRST_X_ASSUM (MP_TAC o Q.SPEC `s'`) \\ fs []
451 \\ REPEAT (FIRST_X_ASSUM (MP_TAC o Q.SPEC `c:num`))
859 \\ FIRST_X_ASSUM (MP_TAC o Q.SPEC `c`) \\ fs [])
861 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `c`)
864 \\ POP_ASSUM (MP_TAC o Q.SPEC `a_state (phase3 0 0 t) c`)
871 \\ POP_ASSUM (MP_TAC o Q.SPEC `a_state (phase3 0 0 t) c`)
|
| /seL4-l4v-10.1.1/HOL4/examples/imperative/ |
| H A D | reflectOnFailure.sml | 182 REWRITE_TAC [BETA_RULE (SPEC P (INST_TYPE [alpha |-> ``:'a->num``,beta |-> ``:'a->num``]
203 SPEC P (INST_TYPE [ alpha |-> type_of((hd(#1(Pxy))))] parameterizeSPrime)
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Tactic.sml | 71 fun resolve th th' = MP (MP (SPEC (concl th) F_IMP) th') th
301 ([(asl, mk_forall (x, subst [t |-> x] w))], sing (SPEC t))
306 ([(asl, mk_forall (x, w))], sing (SPEC x))
457 val (ct, cf) = CONJ_PAIR (SPEC rarm (SPEC larm inst))
465 (SPEC cond EXCLUDED_MIDDLE)
499 fun BOOL_CASES_TAC p = STRUCT_CASES_TAC (SPEC p BOOL_CASES_AX)
557 fun ASM_CASES_TAC t = DISJ_CASES_TAC (SPEC t EXCLUDED_MIDDLE)
|
| /seL4-l4v-10.1.1/HOL4/src/list/src/ |
| H A D | numposrepScript.sml | 263 REWRITE_RULE [DECIDE ``1 < 2``] o Q.SPEC `2`) EXP_BASE_LT_MONO
284 (Q.SPEC `1` (Thm.CONJUNCT2 l2n_pow2_compute))
|
| /seL4-l4v-10.1.1/HOL4/src/n-bit/ |
| H A D | alignmentScript.sml | 253 |> Q.SPEC p
255 val th2 = th1 |> Q.SPEC `0w` |> SIMP_RULE (srw_ss()) [aligned_0]
|
| /seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
| H A D | Sub_and_cond.sml | 89 (SPEC n arithmeticTheory.LESS_EQ_REFL))
98 SUB_LEFT_EQ |> SPEC numSyntax.zero_tm
|
| /seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/ |
| H A D | Logging.sml | 46 |f (SPEC_prf _) = "SPEC"
250 (* Attribution: ideas (and code) for reconstructing DISCH, SPEC, GEN, etc.
290 val th2 = SPEC x (ASSUME tm)
295 val th2 = SPEC Q (UNDISCH(fst(EQ_IMP_RULE th1)))
324 val th3 = SPEC R (EQ_MP th2 (ASSUME (mk_disj(P,Q))))
555 | Specialize_prf (t,th) => log_thm (SPEC t th)
611 val th5 = MP th4 (SPEC F FALSITY)
613 val _ = log_thm (DISJ_CASES (SPEC tm BOOL_CASES_AX) th2 th6)
|
| /seL4-l4v-10.1.1/HOL4/src/ring/src/ |
| H A D | abstraction.sml | 117 (nsub,SPEC v (GEN (inst ti x) th))
167 foldl (fn ({redex,residue},th) => SPEC residue (GEN redex th))
|
| /seL4-l4v-10.1.1/HOL4/src/search/ |
| H A D | bftScript.sml | 170 >> POP_ASSUM (MP_TAC o Q.SPEC `x`)
203 POP_ASSUM (MP_TAC o Q.SPEC `x`) THEN RW_TAC list_ss [] THEN
|