/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/small-step/ |
H A D | path_auxScript.sml | 32 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 D | simple_traceScript.sml | 13 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 D | oracleSemScript.sml | 18 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 D | ordinalScript.sml | 33 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 D | vbgnatsScript.sml | 36 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 D | simpleSexpParseScript.sml | 12 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 D | optScript.sml | 18 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 D | logrelScript.sml | 54 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 D | cbvScript.sml | 67 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 D | osetScript.sml | 61 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 D | balanced_mapScript.sml | 24 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 D | vec_mapScript.sml | 40 >> 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 D | regexp_compilerScript.sml | 196 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 D | regexp_parserScript.sml | 91 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 D | regexpScript.sml | 213 >> 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 D | eq_cmp_bmapScript.sml | 81 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 D | clScript.sml | 41 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 D | for_nd_semScript.sml | 57 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 D | for_monadicScript.sml | 67 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 D | mlibRewrite.sml | 66 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 D | countableScript.sml | 10 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 D | alistScript.sml | 81 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 D | euclid.sml | 93 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 D | debug.h | 42 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 D | typeSoundScript.sml | 51 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...] |