Searched refs:rw (Results 51 - 75 of 182) sorted by relevance

12345678

/seL4-l4v-10.1.1/seL4/src/arch/x86/machine/
H A Dbreakpoint.c121 * @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 Dlift_ieeeScript.sml30 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 Dbinary_ieeeScript.sml631 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 DtypesScript.sml85 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 DstateScript.sml75 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 DwaaSimplScript.sml109 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 Dconcrwaa2gbaScript.sml36 >> 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 DNTpropertiesScript.sml59 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 Dfor_ndScript.sml99 rw [type_e_def, SUBSET_DEF] >>
102 rw [EXTENSION] >>
108 rw [type_t_def, SUBSET_DEF] >>
111 rw [EXTENSION] >>
H A Dfor_compileScript.sml50 \\ 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 DgfgScript.sml69 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 Darm_progScript.sml146 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 DindexedListsScript.sml14 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 DnumposrepScript.sml169 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 DfloatScript.sml94 \\ 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 DfoltypesScript.sml152 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 DcountcharsScript.sml45 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 Darm8_progScript.sml186 \\ 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 DrecursivefnsScript.sml76 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 DtailrecScript.sml101 \\ 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 Dfinite_mapScript.sml2227 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 DordNotationSemanticsScript.sml83 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 Dm0_progScript.sml159 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 DquantHeuristicsTools.sml505 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 DbitstringScript.sml133 \\ 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...]

Completed in 296 milliseconds

12345678