/seL4-l4v-10.1.1/seL4/src/arch/x86/machine/ |
H A D | breakpoint.c | 121 * @param rw Access trigger condition (read/write). 125 convertTypeAndAccessToArch(uint16_t bp_num, word_t type, word_t rw) argument 133 type = (rw == seL4_BreakOnWrite) 156 * @param rw[out] Converted output access trigger value. 159 word_t type, rw; member in struct:__anon237 189 ret.rw = seL4_BreakOnRead; 193 ret.rw = seL4_BreakOnWrite; 198 ret.rw = seL4_BreakOnReadWrite; 420 * @param rw Access type that should trigger the BP (read/write). 424 uint16_t bp_num, word_t vaddr, word_t types, word_t size, word_t rw) 423 setBreakpoint(tcb_t *t, uint16_t bp_num, word_t vaddr, word_t types, word_t size, word_t rw) argument [all...] |
/seL4-l4v-10.1.1/HOL4/src/floating-point/ |
H A D | lift_ieeeScript.sml | 30 rw [float_less_than_def, float_compare_def, float_is_finite_def, 32 \\ rw [] 38 rw [float_less_equal_def, float_compare_def, float_is_finite_def, 40 \\ rw [realTheory.REAL_LT_IMP_LE, 47 rw [float_greater_than_def, float_compare_def, float_is_finite_def, 49 \\ rw [realLib.REAL_ARITH ``a < b : real ==> ~(a > b)``, 57 rw [float_greater_equal_def, float_compare_def, float_is_finite_def, 59 \\ rw [realLib.REAL_ARITH ``a < b : real ==> ~(a >= b)``, 67 rw [float_equal_def, float_compare_def, float_is_finite_def, 69 \\ rw [realLi [all...] |
H A D | binary_ieeeScript.sml | 631 rw [realTheory.REAL_LE_DIV, realTheory.REAL_LT_IMP_LE]) 635 rw [realTheory.REAL_EQ_LDIV_EQ]) 679 >- (`(n = 1) \/ (n = 2)` by decide_tac \\ rw []) 701 rw [DECIDE ``0 < a /\ a <> 1 ==> 2n <= a``]) 719 \\ rw [realTheory.pow] 920 \\ rw [float_value_def] 953 rw [float_plus_infinity_def, float_minus_infinity_def, 995 rw [float_component_equality, float_components, two_mod_not_one, sign_neq, 1008 rw [float_plus_infinity_def, float_minus_infinity_def, 1019 rw [float_plus_zero_de [all...] |
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/cbv-lc/ |
H A D | typesScript.sml | 85 rw [sn_v_term_fun_def, type_size_def]); 97 ho_match_mp_tac type_ind >> rw [] 99 >- (rw [sn_e_def, sn_v_def] 103 >> (rw [sem_def] 106 >- (rw [sn_e_def, sn_v_def] 139 >- (first_x_assum mp_tac >> rw [sn_e_def, sn_v_def] 144 >> rw [sem_def, dec_clock_def]));
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | stateScript.sml | 75 rw [NEXT_REL_def, FUN_EQ_THM]) 195 rw [SPLIT_def, STATE_def, SELECT_STATE_def, FRAME_STATE_def, 198 \\ rw [pred_setTheory.EXTENSION] 201 \\ rw [] 203 eq_tac \\ rw [], 247 rw [R_STATE_SEMANTICS]) 289 rw [relationTheory.PreOrder, relationTheory.reflexive_def, 339 rw [SEP_EQ_def, pred_setTheory.EXTENSION, boolTheory.IN_DEF]) 363 \\ rw [] 376 rw [fun2set_de [all...] |
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/ |
H A D | waaSimplScript.sml | 109 rw[SET_EQ_SUBSET, SUBSET_DEF] >> rpt strip_tac >> fs[alterA_lang_def] 160 >- (fs[] >> rw[] 204 >> rw[run_restr_V_def, DECIDE ``i + 1 = SUC i``] 410 rw[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> fs[alterA_lang_def] 540 (* Induct_on `n` >> rw[SET_EQ_SUBSET, SUBSET_DEF] >> rpt strip_tac *) 560 (* rw[SET_EQ_SUBSET] >> rpt strip_tac >> fs[reachable_def, replaceBy_def] *) 620 (* >- (rw[ITSET_THM] >> fs[MEMBER_NOT_EMPTY] *) 625 (* >- (rw[] >> metis_tac[]) *) 671 (* >- (fs[replace_ord_def] >> rw[] >> fs[] *) 734 (* >> rw[] *) [all...] |
H A D | concrwaa2gbaScript.sml | 36 >> fs[MEM_EQUAL_SET] >> rw[] 58 >- (Cases_on `y` >> fs[] >> rw[] >> rename[`MEM (f,f_trns) acc`] 139 >> Cases_on `y` >> fs[] >> rw[] 168 >> rw[] 244 >> rw[] >> rename[`(��,sucs) ��� aa_red.trans n.frml`] 252 >> `a ��� ��` by rw[] 263 >> rw[] 352 >> rw[] >> fs[MEM_SUBSET_SET_TO_LIST] 366 >> rw[] >> fs[findNode_def] 378 >> fs[] >> simp[acc_cond_concr_def] >> rw[] [all...] |
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/ |
H A D | NTpropertiesScript.sml | 59 rw[] >| [ 62 rw[] >> first_x_assum (qspecl_then [`p`, `l' ++ r ++ s0`, `t`] mp_tac), 176 strip_tac >- (rw[] >> Cases_on`pt` >> fs[]) >> 184 rw[] >> res_tac >> rw[]); 195 strip_tac >- (rw[] >> Cases_on`pt` >> fs[]) >> 213 strip_tac >- (rw[] >> Cases_on`pt` >> fs[]) >> 288 ho_match_mp_tac relationTheory.RTC_INDUCT >> rw[] >> 292 listTheory.APPEND_EQ_SING] >> rw[] >> 295 rw[] >> [all...] |
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/for/ |
H A D | for_ndScript.sml | 99 rw [type_e_def, SUBSET_DEF] >> 102 rw [EXTENSION] >> 108 rw [type_t_def, SUBSET_DEF] >> 111 rw [EXTENSION] >>
|
H A D | for_compileScript.sml | 50 \\ rw [phase1_def,Loop_def] 87 \\ rw [sem_t_def_with_stop,sem_e_def,Once sem_t_Loop] 100 \\ rw [sem_t_def_with_stop,sem_e_def,Once sem_t_Loop] 235 simp[FLOOKUP_DEF, FAPPLY_FUPDATE_THM] >> rw[]) 237 simp[sem_e_def, comp_exp_def, sem_t_def] >> rw[] >> 240 simp[FLOOKUP_DEF, FAPPLY_FUPDATE_THM] >> rw[]) 268 dsimp[] >> rw[] 281 rw[] >> fs[sem_e_break, exp_max_def, MAX_LESS] >> 288 simp[] >> strip_tac >> simp[store_var_def] >> rw[] >> 289 fs[SUBMAP_DEF, FAPPLY_FUPDATE_THM, FLOOKUP_DEF] >> rw[] >> f 613 local val rw = srw_tac[] val fs = fsrw_tac[] val rfs = rev_full_simp_tac(srw_ss()) in value 995 val rw = srw_tac[] val fs = fsrw_tac[] value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/generic_finite_graphs/ |
H A D | gfgScript.sml | 69 rw[]); 82 >> rw[] >> fs[] 88 >> Cases_on `MEM (e',n) followers_old` >> rw[] >> fs[MEM] 105 >> rw[] >> fs[INSERT_DEF,SET_EQ_SUBSET,SUBSET_DEF]
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/prog/ |
H A D | arm_progScript.sml | 146 rw [alignmentTheory.aligned_extract] 201 \\ rw [arm_WORD_MEMORY_def] 214 \\ rw [arm_BE_WORD_MEMORY_def] 249 rw [set_sepTheory.STAR_def, set_sepTheory.SPLIT_def, 286 \\ rw [stateTheory.UNION_STAR, arm_instr_star, set_sepTheory.SEP_CLAUSES, 321 \\ rw [stateTheory.UNION_STAR, arm_instr_star, set_sepTheory.SEP_CLAUSES, 345 rw [arm_instr_def, pred_setTheory.DISJOINT_DEF] 358 rw [arm_instr_def, pred_setTheory.DISJOINT_DEF] 367 rw [pred_setTheory.DISJOINT_DEF, lem]
|
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | indexedListsScript.sml | 14 fun rw thl = SRW_TAC[] thl function 149 strip_tac >> rw[] >> pop_assum mp_tac >> 163 rw[arithmeticTheory.ADD1, arithmeticTheory.ZERO_LESS_ADD]); 169 Cases_on `n` >> simp[findi_def] >> rw[arithmeticTheory.ADD1] >> 175 Induct_on`l` >> rw[findi_def] >> simp[DECIDE ``1 + x = SUC x``]); 197 Induct >> simp[delN_def] >> rw[] 199 `?i0. i = SUC i0` by (Cases_on `i` >> fs[]) >> rw[] >> 297 ho_match_mp_tac MAP2i_ind >> rw[arithmeticTheory.MIN_DEF]); 303 HO_MATCH_MP_TAC MAP2i_ind >> rw[] >> Cases_on���n��� >> fs[]);
|
H A D | numposrepScript.sml | 169 val rw = SRW_TAC[ARITH_ss] value 190 rw[] THEN fs[LAST_DEF] THEN 216 simp[dropWhile_def,REVERSE_SNOC] >> rw[] >> 217 rw[] >> rw[l2n_SNOC_0] >> rw[SNOC_APPEND]) 226 Q_TAC SUFF_TAC`x = PRE (LENGTH (REVERSE y))` >- rw[] >>
|
/seL4-l4v-10.1.1/HOL4/src/float/ |
H A D | floatScript.sml | 94 \\ rw [Isnan, Infinity, Isnormal, Isdenormal, Iszero, 115 rw [Isnan, Infinity, Isnormal, Isdenormal, Iszero, 182 \\ rw [] 194 rw [Plus_infinity, Minus_infinity, feq, float_eq, fcompare] 233 `!a. (a == a) = ~Isnan a`, rw [float_eq, feq, fcompare, Isnan]) 258 \\ rw [] 261 >- (qexists_tac `a` \\ rw [] \\ simp []) 263 \\ rw [] 276 rw [closest] 299 rw [EXTENSIO [all...] |
/seL4-l4v-10.1.1/HOL4/examples/logic/ |
H A D | foltypesScript.sml | 152 rw[IMP_def, GLAM_NIL_EQ, form_ABS_pseudo11, IMP_formP]); 318 rw[listTheory.LIST_REL_EL_EQN] >> 325 qx_gen_tac `i` >> rw[] >> ONCE_REWRITE_TAC [EQ_SYM_EQ] >> 328 rw[] >> qpat_x_assum `���n. n < LENGTH uns ��� PP ��� QQ` mp_tac >> 335 rw[EXTENSION, IN_GFVl] >> metis_tac[]); 339 rw[EQ_IMP_THM] >> rw[formP_form_REP] >> qexists_tac `form_ABS g` >> 340 rw[form_repabs_pseudo_id]); 379 rw[] >> match_mp_tac term_repabs_pseudo_id >> 385 rw[REL_de [all...] |
/seL4-l4v-10.1.1/HOL4/examples/countchars/ |
H A D | countcharsScript.sml | 45 rw[] >> 69 dsimp[FUN_FMAP_DEF, FAPPLY_FUPDATE_THM] >> rw[] >> fs[] >>
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/prog/ |
H A D | arm8_progScript.sml | 186 \\ rw [arm8_WORD_MEMORY_def] 215 \\ rw [arm8_DWORD_MEMORY_def] 248 rw [set_sepTheory.STAR_def, set_sepTheory.SPLIT_def, 290 \\ rw [stateTheory.UNION_STAR, arm_instr_star, set_sepTheory.SEP_CLAUSES, 326 \\ rw [stateTheory.UNION_STAR, arm_instr_star, set_sepTheory.SEP_CLAUSES, 350 rw [arm8_instr_def, pred_setTheory.DISJOINT_DEF] 363 rw [arm8_instr_def, pred_setTheory.DISJOINT_DEF] 372 rw [pred_setTheory.DISJOINT_DEF, lem]
|
/seL4-l4v-10.1.1/HOL4/examples/computability/ |
H A D | recursivefnsScript.sml | 76 simp[minimise_def] >> DEEP_INTRO_TAC optionTheory.some_intro >> rw[] 78 SELECT_ELIM_TAC >> rw[] >> 112 >- (qid_spec_tac`xs` >> Induct_on `n` >> simp[proj_def] >> rw[] >> 137 Induct_on ���recfn��� >> rw[] >> rename [���gs ��� []���] >> 151 ������h t. l = h::t��� by (Cases_on ���l��� >> fs[]) >> rw[] >> fs[] >>
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | tailrecScript.sml | 101 \\ ho_match_mp_tac TAILREC_PRE_INDUCT \\ rw [] 115 \\ ho_match_mp_tac SHORT_TAILREC_PRE_INDUCT \\ rw [] 116 \\ Cases_on `f x` \\ fs [] \\ rw []
|
/seL4-l4v-10.1.1/HOL4/src/finite_map/ |
H A D | finite_mapScript.sml | 2227 rw[fmap_rel_def,optionTheory.OPTREL_def,FLOOKUP_DEF,EXTENSION] >> 2234 rw[fmap_rel_OPTREL_FLOOKUP,optionTheory.OPTREL_def] >> 2235 first_x_assum(qspec_then`k`mp_tac) >> rw[]); 2316 rw[o_f_FAPPLY]); 2350 Induct >- rw[FUPDATE_LIST_THM] >> 2351 Cases >> rw[FUPDATE_LIST_THM] >> 2356 Induct >> rw[] >> 2358 rw[FUPDATE_LIST_THM] >> 2364 rw[FUPDATE_LIST_APPEND] >> 2368 rw[FUPDATE_LIST_TH [all...] |
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/more_theories/ |
H A D | ordNotationSemanticsScript.sml | 83 match_mp_tac ordlte_TRANS >> qexists_tac `omega` >> rw[] >> 84 match_mp_tac ordle_TRANS >> qexists_tac `omega ** <[e]> * &c` >> rw[] >> 131 `oless e1 e2 \/ oless e2 e1 \/ (e2 = e1)` by metis_tac[] >> rw[] >> 132 `oless t1 t2 \/ oless t2 t1 \/ (t2 = t1)` by metis_tac[] >> rw[] >> 188 >- (rw[] >> qexists_tac `c` >> simp[ordle_lteq]) >> 279 rw[add_nat1_disappears_kexp, osyntax_EQ_0] 302 by (rw[] >> match_mp_tac ordlte_TRANS >> 316 `omega ** e * c <= a` by rw[] >> 334 qexists_tac `Plus en cn tn` >> simp[] >> rw[] >- fs[] >> 341 pop_assum (fn th => RULE_ASSUM_TAC (REWRITE_RULE [th])) >> rw[] >> [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/prog/ |
H A D | m0_progScript.sml | 159 rw [set_sepTheory.STAR_def, set_sepTheory.SPLIT_def, m0_instr_def, 198 \\ rw [stateTheory.UNION_STAR, m0_instr_star, set_sepTheory.SEP_CLAUSES, 235 \\ rw [stateTheory.UNION_STAR, m0_instr_star, set_sepTheory.SEP_CLAUSES, 259 rw [m0_instr_def, data_to_thumb2_def, byte_lem, pred_setTheory.DISJOINT_DEF]
|
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsTools.sml | 505 fun crw_SINGLE_STEP_CONV (rw, turned) t = 507 val (l,r) = dest_eq rw; 511 if turned then mk_eq (r,l) else rw; 534 fun turn_eq rw = 535 let val (l,r) = dest_eq rw in mk_eq (r,l) end; 537 fun check_rw P rw = 538 case P rw of 540 | SOME false => SOME (rw,false) 541 | SOME true => SOME (turn_eq rw, true) 557 fun P v rw [all...] |
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | bitstringScript.sml | 133 \\ Induct_on `n` \\ rw [] 176 \\ rw [listTheory.EVERY_EL] \\ rw []) 200 rw [field_def, length_fixwidth]) 208 rw [length_bitify]) 281 by (rw [length_shiftr] \\ decide_tac) 296 arithmeticTheory.ADD1] \\ rw[]) 302 rw [field_def, shiftr_0]) 326 rw [v2w_def, wordsTheory.word_bit_def] 340 rw [wordsTheor [all...] |