Searched refs:rw (Results 1 - 25 of 182) sorted by relevance

12345678

/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/small-step/
H A Dpath_auxScript.sml32 rw [] >>
37 rw [] >>
41 rw [] >>
50 rw []);
55 rw [] >>
60 rw [tail_take]);
68 rw [] >>
70 rw [] >>
71 rw [Once path_bisimulation] >>
73 rw [] >>
460 local val rw = srw_tac[] val fs = fsrw_tac[] in value
[all...]
H A Dsimple_traceScript.sml13 rw [] >>
20 rw [] >>
26 rw [some_def]);
30 rw [some_def] >>
56 rw [] >>
62 rw []
65 rw [check_trace_def])
68 rw [LAST_DEF] >>
71 rw [] >>
73 rw [LAST_DE
[all...]
H A DoracleSemScript.sml18 rw [lfilter_map_def] >>
97 rw [] >>
114 rw [small_chain_def, lprefix_chain_def, LPREFIX_def] >>
115 rw [from_toList] >>
124 rw [] >>
134 rw [] >>
146 rw [fbs_chain_def, lprefix_chain_def, LPREFIX_def] >>
147 rw [from_toList] >>
166 rw [] >>
168 rw [small_chain_de
[all...]
/seL4-l4v-10.1.1/HOL4/examples/set-theory/vbg/
H A DordinalScript.sml33 rw[iseg_def, SUBSET_def, SPEC0] >- metis_tac [] >>
51 rw[woclass_def, totalR_def, poc_def, LE_ANTISYM]
75 rw[ordle_def])
82 rw[woclass_def, EQ_IMP_THM]
84 rw[totalR_def, poc_def]
88 by (rw[Once EXTENSION] >> metis_tac [SET_def]) >>
94 by rw[Once EXTENSION, EXISTS_OR_THM] >>
100 by rw[Once EXTENSION, EXISTS_OR_THM] >>
106 rw[ordinal_def, transitive_def])
112 rw[ordinal_de
[all...]
H A DvbgnatsScript.sml36 rw [Nats_def, SPEC0, inductive_def]);
41 rw [Nats_def, SPEC0, inductive_def, vSUC_def]);
82 qx_gen_tac `n` >> rw [Nats_def] >>
87 qsuff_tac `vSUC e = y` >- rw[] >>
88 rw [vSUC_def, Once EXTENSION] >> metis_tac [SET_def]);
93 rw [SPEC0, SUBSET_def, Inductives_def, Nats_SET, EMPTY_IN_Nats,
99 rw[Inductives_def, SUBSET_def] >>
128 rw [transitive_def] >> metis_tac [SUBSET_def]);
133 ho_match_mp_tac nat_induction >> conj_tac >> rw[transitive_def] >>
140 ho_match_mp_tac nat_induction >> rw[vSUC_de
[all...]
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/
H A DsimpleSexpParseScript.sml12 Induct \\ simp[listTheory.DROP_def] \\ rw[]);
28 Induct \\ rw[EQ_IMP_THM] \\ rw[]
39 rw[n2s_def,rich_listTheory.EVERY_REVERSE,listTheory.EVERY_MAP]
48 rw[num_to_dec_string_def,EVERY_isDigit_n2s]);
52 rw[n2s_def,listTheory.NULL_EQ]
59 rw[num_to_dec_string_def,n2s_not_null]);
73 simp[stringTheory.isDigit_def] \\ rw[]
92 \\ rw[] \\ simp[GSYM isDigit_UNHEX_alt,isDigit_ORD_MOD_10]);
97 rw[num_to_dec_string_de
[all...]
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/cbv-lc/
H A DoptScript.sml18 rw [FUNPOW]);
22 rw [FUN_EQ_THM]);
26 rw [] >>
28 rw [prim_recTheory.WF_LESS]);
41 rw [] >>
98 rw [is_val_def, sem_def] >>
106 rw [is_val_def, shift_def]);
113 rw [] >>
125 rw [] >>
130 rw [res_rel_r
[all...]
H A DlogrelScript.sml54 rw [] >>
56 rw [] >>
78 rw [] >>
136 rw [] >>
139 rw [] >>
152 rw [] >>
163 rw [LIST_REL_EL_EQN] >>
171 rw [LIST_REL_EL_EQN] >>
179 rw [exp_rel_def] >>
180 rw [exec_rel_r
200 local val rw = srw_tac[] val fs = fsrw_tac[] in value
419 local val rw = srw_tac[] val fs = fsrw_tac[] in value
[all...]
H A DcbvScript.sml67 rw [state_component_equality]);
77 rw [check_clock_def, state_component_equality]);
122 rw[] >> fsrw_tac[ARITH_ss][]);
146 rw[Once sem_def] >>
156 `F` suffices_by rw[] >>
163 rw[] >>
165 rw[] >> fs[] >>
181 rw [sem_def, state_component_equality] >>
182 rw [] >>
196 rw [] >>
[all...]
/seL4-l4v-10.1.1/HOL4/examples/balanced_bst/
H A DosetScript.sml61 rw [empty_thm, good_oset_def, oempty_def]);
65 rw [singleton_thm, good_oset_def, osingleton_def]);
69 rw [oinsert_def, good_oset_def] >>
74 rw [good_oset_def, odelete_def] >>
79 rw [good_oset_def, ounion_def] >>
90 rw [] >>
92 by (rw [good_cmp_def, LAMBDA_PROD, FORALL_PROD] >>
95 rw [ocompare_def, good_cmp_def] >>
101 rw [] >>
107 rw [oset_de
[all...]
H A Dbalanced_mapScript.sml24 by (rw [GSPEC_AND, LE_LT1] >>
27 rw [GSYM count_def]) >>
102 rw [] >>
104 rw [] >>
124 val rw = srw_tac [ARITH_ss]; value
158 rw [MIN_DEF] >>
166 rw [DISJOINT_DEF, FCARD_DEF] >>
176 rw [DISJOINT_DEF] >>
181 rw [FCARD_DEF, FDOM_DRESTRICT]);
190 rw [CARD_INSER
[all...]
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/
H A Dvec_mapScript.sml40 >> rw [alist_to_vec_def]
42 >> rw []
44 >> Cases_on `n` >> rw [EL_CONS] >> fs []
45 >- (FIRST_X_ASSUM match_mp_tac >> rw []
49 >- (FIRST_X_ASSUM match_mp_tac >> rw []
53 >- (ntac 2 (pop_assum mp_tac) >> rw []
55 >> `MEM (max ��� SUC cur) (MAP FST l)` by (rw[MEM_MAP] >> metis_tac[FST])
58 >- (FIRST_X_ASSUM match_mp_tac >> rw []
62 >- (FIRST_X_ASSUM match_mp_tac >> rw []
76 rw [] >>
[all...]
H A Dregexp_compilerScript.sml196 Cases >> rw[Once Brz_def])
212 >- (rw[] >> rw[Once Brz_def,LET_THM]
215 >- rw [Brz_def]
216 >- (rw [Once Brz_def] >> metis_tac [])
218 >> rw[LET_THM]
287 >> rw [Once Brz_def]);
299 >> rw [Once Brz_def,LET_THM]);
333 >- rw [Once Brz_def]
337 >- rw []
[all...]
H A Dregexp_parserScript.sml91 rw[charset_char_def,uncharset_char_def]
96 \\ rw[stringTheory.CHR_ORD]);
165 \\ rpt(rw[Once wfpeg_cases]));
169 rw[Once wfpeg_cases] >- EVAL_TAC
170 \\ rw[wfpeg_BslashSpecial_applied]);
175 \\ ntac 2 (rw[Once wfpeg_cases]));
179 rw[Once wfpeg_cases] >- EVAL_TAC
180 \\ rw[wfpeg_CharSet_applied]);
185 \\ rpt(rw[Once wfpeg_cases]));
189 rw[Onc
[all...]
H A DregexpScript.sml213 >> rw [rsize_def]
232 rw [regexp_lang_def,Epsilon_def,charset_mem_empty,KSTAR_EMPTYSET,SET_EQ_THM]);
237 rw [regexp_lang_def,Empty_def,charset_mem_empty]);
242 rw [regexp_lang_epsilon,SET_EQ_THM]);
309 recInduct len_cmp_ind >> rw[len_cmp_def]);
315 recInduct len_cmp_ind >> rw[len_cmp_def]);
319 recInduct len_cmp_ind >> rw[len_cmp_def]);
326 recInduct len_cmp_ind >> rw[len_cmp_def]);
330 recInduct len_cmp_ind >> rw[len_cmp_def]);
478 >> rw[]
[all...]
H A Deq_cmp_bmapScript.sml81 Induct >> rw [invariant_def] >> metis_tac [insert_thm])
86 rw [bmap_of_def,invariant_insert_list]);
104 rw [] >> `good_cmp cmp` by metis_tac [eq_cmp_def]
105 >> rw [lookup_thm]
111 rw [insert_thm,lookup_thm,FLOOKUP_UPDATE]
120 rw [insert_thm,lookup_thm,FLOOKUP_UPDATE]
140 Induct >> rw [bmap_of_list_def] >> `good_cmp cmp` by metis_tac [eq_cmp_def]
142 >- (rw [Once lookup_insert_thm,invariant_insert_list,GSYM bmap_of_list_def]
150 Induct >> rw [bmap_of_list_def] >> `good_cmp cmp` by metis_tac [eq_cmp_def]
151 >- rw [lookup_de
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ind_def/
H A DclScript.sml41 rw[confluent_def] >>
51 rw[confluent_def, diamond_def]);
73 GEN_TAC >> STRIP_TAC >> Induct_on `RTC` >> rw[] >| [
142 rw[Sx_predn0, predn_rules, S_predn, EQ_IMP_THM]);
146 rw[characterise ``K # x``, predn_rules, K_predn, EQ_IMP_THM]);
152 rw[characterise ``K # x # y``, predn_rules, Kx_predn, EQ_IMP_THM]);
158 rw[characterise ``S # x # y``, predn_rules, EQ_IMP_THM,
166 rw[characterise ``S # w # x # y``, predn_rules, Sxy_predn, EQ_IMP_THM]);
175 rw[] >>
178 rw[] >| [
[all...]
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/for/
H A Dfor_nd_semScript.sml57 rw [state_component_equality]);
119 ho_match_mp_tac sem_e_ind >> rw [sem_e_def] >> ect >>
121 rw [] >> ect >> fs [] >>
122 ect >> fs [] >> rw []);
126 ho_match_mp_tac sem_e_ind >> rw [sem_e_def] >> ect >>
129 rw [] >> ect >> fs [] >>
130 ect >> fs [] >> rw [] >> metis_tac []);
134 ho_match_mp_tac sem_e_ind >> rw [sem_e_def] >> ect >>
136 rw [] >> ect >> fs [] >>
137 ect >> fs [] >> rw [] >> metis_ta
[all...]
H A Dfor_monadicScript.sml67 rw[FUN_EQ_THM] >> EVAL_TAC >>
72 EVAL_TAC >> rw[]);
82 rw[FUN_EQ_THM] >>
94 rw[FUN_EQ_THM] >>
107 rw[FUN_EQ_THM] >> EVAL_TAC);
114 rw[FUN_EQ_THM] >> EVAL_TAC);
118 rw[FUN_EQ_THM] >> EVAL_TAC);
123 rw[FUN_EQ_THM] >> EVAL_TAC >>
132 rw[FUN_EQ_THM] >> EVAL_TAC >>
154 rw[FUN_EQ_TH
[all...]
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibRewrite.sml66 fun update_waiting waiting rw =
68 val REWRS {order, known, rewrites, subterms, waiting = _} = rw
74 fun waiting_del i (rw as REWRS {waiting, ...}) =
75 update_waiting (S.delete (waiting,i)) rw;
121 fun rewrs_to_string rw = PP.pp_to_string (!LINE_LENGTH) pp_rewrs rw;
123 fun chatrewrs s rw =
124 chat (module ^ "." ^ s ^ ":\n" ^ rewrs_to_string rw ^ "\n");
145 fun add (i,th) (rw as REWRS {known, ...}) =
146 if Option.isSome (M.peek (known,i)) then rw els
155 val rw = REWRS {order = order, known = known, rewrites = rewrites, value
172 fun rw ((l,_),LtoR) tm = can (match l) tm function
215 val (rw,ort) = retrieve known j value
410 val (rw,changed) = reduce_acc (S.empty, S.empty, S.empty, rw) value
[all...]
/seL4-l4v-10.1.1/HOL4/examples/countable/
H A DcountableScript.sml10 rw[] >> Induct_on `l1` >>
11 rw[definition "count_list_aux_def"])
21 rw[] >> Cases_on `p1` >> fs[])
/seL4-l4v-10.1.1/HOL4/src/finite_map/
H A DalistScript.sml81 Cases >> rw[MEM_fmap_to_alist,FLOOKUP_DEF])
86 rw[MEM_fmap_to_alist_FLOOKUP])
92 rw[fmap_to_alist_def,SET_TO_LIST_CARD])
123 REWRITE_TAC[FLOOKUP_DEF] >> rw[])
128 gen_tac >> Induct >- rw[FUN_EQ_THM] >> Cases >> rw[FUN_EQ_THM] >> rw[])
148 Induct >- rw[FUNION_FEMPTY_1] >>
149 Cases >> rw[FUNION_FUPDATE_1])
165 rw[] >> Cases_o
[all...]
/seL4-l4v-10.1.1/HOL4/examples/
H A Deuclid.sml93 rw [divides_def] >> rw[]);
102 rw [LESS_EQ_EXISTS]
104 >> rw [FACT,ADD_CLAUSES]
114 >> rw [FACT,ADD_CLAUSES]
120 rw [LESS_EQ_EXISTS]
129 >> rw [] >|
130 [`m = n` by rw[] >>
133 `0 < n` by rw[] >>
135 >> rw [FAC
[all...]
/seL4-l4v-10.1.1/seL4/include/machine/
H A Ddebug.h42 word_t vaddr, word_t type, word_t size, word_t rw);
51 * @param rw[out] Access type (read/write) that will trigger thr breakpoint.
60 word_t vaddr, type, size, rw; member in struct:getBreakpointRet
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/ml/
H A DtypeSoundScript.sml51 rw[LIST_EQ_REWRITE,EL_LUPDATE] >> rw[])
59 simp[f_o_f_DEF] >> rw[] >> fs[])
143 rw [check_clock_def, state_component_equality]);
150 rw[dec_clock_def])
154 rw[dec_clock_def])
261 rw[] >> fsrw_tac[ARITH_ss][])
287 rw[Once sem_def] >>
297 `F` suffices_by rw[] >>
304 rw[] >>
[all...]

Completed in 105 milliseconds

12345678