/seL4-l4v-10.1.1/HOL4/src/enumfset/ |
H A D | comparisonScript.sml | 35 rw [good_cmp_def] >> 84 rw[TotOrd,good_cmp_thm] >> metis_tac[]) 107 rw[] >> 144 rw [good_cmp_def] >> 152 rw [good_cmp_def] >> 231 rw [list_cmp_def] >> 232 rw [list_cmp_def] >> 234 rw []); 244 rw [option_cmp_def] >> 245 rw [option_cmp_de [all...] |
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/small-step/ |
H A D | determSemScript.sml | 90 local val rw = srw_tac[] val fs = fsrw_tac[] in value 107 rw [small_sem_def, fbs_sem_def] >> 120 rw [] >> 123 rw [] >> 131 rw [] >> 134 rw [] >> 159 rw [check_result_def] >> 165 rw [check_result_def] >> 197 rw [] 200 rw [] >> [all...] |
H A D | for_osmallScript.sml | 17 rw [some_def]); 21 rw[some_def,SELECT_THM]>> 263 ho_match_mp_tac step_e_strongind>>rw[]>>fs[FORALL_PROD] 264 >- (rw[conjs_def]>>fs[Once step_e_cases]>>rfs[]) 265 >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[])) 266 >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[])) 267 >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[])) 268 >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[])) 271 (pop_assum mp_tac>>simp[Once step_e_cases]>>rw[]>> 281 ho_match_mp_tac step_t_strongind >>rw[] 640 local val rw = srw_tac[] val fs = fsrw_tac[] in value 874 local val rw = srw_tac[] val fs = fsrw_tac[] in value [all...] |
H A D | forSmallScript.sml | 19 rw [some_def]); 197 ho_match_mp_tac step_e_strongind>>rw[]>>fs[FORALL_PROD] 203 (pop_assum mp_tac>>simp[Once step_e_cases]>>rw[] 211 (pop_assum mp_tac>>simp[Once step_e_cases]>>rw[] 221 (pop_assum mp_tac >> simp[Once step_e_cases]>>rw[] 232 ho_match_mp_tac step_t_strongind >>rw[] 240 simp[Once step_t_cases]>>fs[FORALL_PROD]>>rw[] 265 simp[Once step_t_cases]>>rw[] 279 rw[]>> 286 rw[]>>f 637 local val rw = srw_tac[] val fs = fsrw_tac[] in value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/computability/turing/ |
H A D | turing_machine_primeqScript.sml | 60 simp[NUM_TO_ACT_def] >> rw[FULL_DECODE_TM_def,FULL_ENCODE_TM_def] 61 >- (rw[UPDATE_ACT_S_TM_def] >> EVAL_TAC) >> 62 rw[ENCODE_TM_TAPE_def] 63 >- (rw[UPDATE_ACT_S_TM_def] >> rw[DECODE_TM_TAPE_def] >> 65 >- (rw[UPDATE_ACT_S_TM_def] >> rw[DECODE_TM_TAPE_def] >> 85 rw[FULL_DECODE_TM_def] >> rw[FULL_ENCODE_TM_def] 86 >- (rw[UPDATE_ACT_S_TM_de [all...] |
H A D | turing_machineScript.sml | 121 (WF_REL_TAC `$<` >> rw[] >> fs[ODD_EXISTS] >> 139 completeInduct_on `n` >> Cases_on `n` >- EVAL_TAC >> rw[DECODE_def] 140 >- (rw[ENCODE_def] 143 >> `ENCODE (DECODE (n' DIV 2)) = n' DIV 2` by fs[] >> rw[] 148 >> rw[]) 149 >> rw[ENCODE_def] 157 Induct_on `n` >- EVAL_TAC >> fs[] >> rw[DECODE_def] ); 248 rpt strip_tac >> rw[UPDATE_ACT_S_TM_def] ); 253 rpt strip_tac >> rw[UPDATE_ACT_S_TM_def] ); 258 rw[DECODE_de [all...] |
/seL4-l4v-10.1.1/HOL4/examples/misc/ |
H A D | balancedParensScript.sml | 16 `S []`, rw[Once S_cases]); 27 `T []`, rw[Once T_cases]) 51 rw[] >> fs[] >- ( 68 rw[APPEND_EQ_APPEND,APPEND_EQ_CONS] >> fs[] >> 74 asm_simp_tac std_ss [REPLICATE_GENLIST] >> rw[] >> fs[]
|
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/for/ |
H A D | forScript.sml | 71 rw [state_component_equality]); 104 Induct_on `e` >> rw [sem_e_def] >> ect >> 105 fs [] >> rw [] >> metis_tac []); 109 Induct_on `e` >> rw [sem_e_def] >> ect >> 110 fs [SUBSET_DEF] >> rw [] >> metis_tac []); 114 Induct_on `e` >> rw [sem_e_def] >> ect >> 115 fs [] >> rw [] >> metis_tac []); 126 rw [dec_clock_def]); 167 \\ rw [] 176 rw [Onc 1017 local val rw = srw_tac[] val fs = fsrw_tac[] in value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/ |
H A D | wordScript.sml | 16 rw[] >> Cases_on `w` 39 rw[word_range_def] >> metis_tac[word_range_def]
|
H A D | concrRepScript.sml | 345 (* >- (rw[] *) 367 (* rw[]) *) 450 (* >> `neg1 = []` by fs[MEM_SUBSET_SET_TO_LIST] >> rw[] *) 498 >> rw[FOLDR_LEMM5] 628 by (fs[MEM_MAP] >> qexists_tac `y` >> Cases_on `y` >> fs[] >> rw[]) 686 >> `id = id2` by (rw[] >> metis_tac[]) 687 >> rw[] >> metis_tac[MEM_toAList,SOME_11] 731 >> rw[] >> metis_tac[MEM_toAList,SOME_11] 763 >> fs[MEM_toAList,domain_lookup] >> rw[] 817 >- (fs[addFrmlToGraph_def] >> rw[] [all...] |
H A D | formParseScript.sml | 76 rw[EQ_IMP_THM] 77 >- (rw[] >> 79 Cases_on ���px��� >> fs[] >> rw[] >> 82 simp[] >> rw[] >> Cases_on ���px��� >> simp[] >> metis_tac[]); 89 Induct_on ���s��� >> simp[token_def, TypeBase.case_eq_of ``:bool``] >> rw[] >> 90 rw[EQ_IMP_THM] 96 >- (simp[] >> Cases_on ���px��� >> fs[] >> rw[] >> metis_tac[]) 97 >- (���px = []��� by (Cases_on ���px��� >> fs[] >> rw[] >> fs[]) >> 107 >- (rw[EQ_IMP_THM] 109 ������pt. px = c :: pt��� by (Cases_on ���px��� >> fs[] >> rw[] >> f [all...] |
H A D | generalHelpersScript.sml | 36 >> rw[ADD_SUC] 165 >- (rw[] >> metis_tac[FUNPOW, FUNPOW_SUC]) 196 rpt strip_tac >> fs[d_conj_def] >> rw[SET_EQ_SUBSET] 279 (* rw[] >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac *) 289 (* rw[] >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac *) 328 (* >- (rw[] *) 341 (* rw[] >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac *) 354 (* >- (rw[] >> ) *) 410 >> fs[d_conj_def] >> rw[] 420 >> qunabbrev_tac `f_a2` >> qunabbrev_tac `f_e2` >> rw[] >> f [all...] |
H A D | concrGBArepScript.sml | 102 >> fs[cE_equiv_def] >> rw[MEM_EQUAL_SET,LIST_TO_SET_FILTER] 134 >- (rw[] >> fs[] >> Cases_on `s = []` >> fs[] 145 >> rw[] 150 >- (fs[MEM_GENLIST] >> rw[] >> fs[] 173 >> rw[] 193 >> rw[FOLDR_CONCR_EDGE] 201 >> rpt strip_tac >> simp[d_conj_concr_def] >> rw[FOLDR_LEMM4] 224 >> rw[] 285 >- (qunabbrev_tac `s` >> rw[] >> simp[d_conj_set_def,ITSET_THM] 329 >> rw[FOLDR_CONCR_EDG [all...] |
H A D | buechiAScript.sml | 51 rw[EQ_IMP_THM] >> fs[isAcceptingGBARunFor_def] 251 (* >> rw[] >> metis_tac[] *) 293 (* >> rw[] >> metis_tac[] *) 305 (* >> rw[] *) 327 (* >- (rw[] >> first_assum (qspec_then `0` mp_tac) >> simp[] *) 331 (* >- (Cases_on `SUC k = i` >> fs[] >> rw[] *) 344 (* >> rw[] *) 350 (* >- (Cases_on `SUC k = i` >> fs[] >> rw[] *) 353 (* >- (Cases_on `SUC k = i` >> fs[] >> rw[] *) 382 (* >- (`B = 0` by simp[] >> rw[] *) [all...] |
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/more_theories/ |
H A D | wellorderScript.sml | 38 rw[wellfounded_def, WF_DEF, SPECIFICATION]); 50 rw[wellorder_def, wellfounded_def, linear_order_def, transitive_def, 56 rw[wellorder_def, wellfounded_def, strict_def, reflexive_def, 66 rw[SUBSET_DEF,rrestrict_def] >> rw[]); 71 rw[wellfounded_def] >> 101 rw[elsOf_def, range_def, domain_def, strict_def] >> metis_tac[]); 106 rw[elsOf_def, range_def, domain_def] >> metis_tac[]); 140 rw[strict_def]); 187 rw[transitive_de [all...] |
/seL4-l4v-10.1.1/HOL4/examples/set-theory/vbg/ |
H A D | vbgsetScript.sml | 260 rw [INTER_def]); 269 ] >> rw[SUBSET_def]); 497 rw[SUBSET_def]); 538 >- (rw[bad_def] >> 540 rw[] >> Cases_on `���e. f 0 = {e}` >> fs[] >> 542 >- (DISJ1_TAC >> rw[Once EXTENSION]) >> 544 first_x_assum (qspec_then `e` mp_tac) >> rw[] >> 547 CONV_TAC CONTRAPOS_CONV >> rw[] >> 558 rw[SUBSET_def]) >> 561 by (rw[Abb [all...] |
/seL4-l4v-10.1.1/HOL4/examples/finite-test-set/ |
H A D | finite_test_setScript.sml | 66 \\ rw[] \\ res_tac \\ rw[]); 85 (WF_REL_TAC`measure (LENGTH o FST o FST)` \\ rw[]); 108 \\ rw[val_form_def,Goldbach_statement_def] 142 Induct \\ rw[mk_test_inst_def] \\ rw[]); 147 \\ rw[mk_test_inst_def] 155 Induct \\ rw[mk_test_inst_def] 160 \\ rw[DROP_APPEND,DROP_LENGTH_NIL_rwt] ) 162 \\ Cases_on`q` \\ rw[] [all...] |
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Rewrite.sml | 49 fun updateWaiting rw waiting = 51 val Rewrite {order, known, redexes, subterms, waiting = _} = rw 58 fun deleteWaiting (rw as Rewrite {waiting,...}) id = 59 updateWaiting rw (IntSet.delete waiting id); 190 fun add (rw as Rewrite {known,...}) (id,eqn) = 191 if IntMap.inDomain id known then rw 194 val Rewrite {order,redexes,subterms,waiting, ...} = rw 204 val rw = value 209 val () = Print.trace pp "Rewrite.add: result" rw 212 rw 515 val rw = value 537 val rw = value 628 val rw = deleteWaiting rw id value 673 val rw = List.foldl addEqn (new order) (enumerate ths) value [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Rewrite.sml | 49 fun updateWaiting rw waiting = 51 val Rewrite {order, known, redexes, subterms, waiting = _} = rw 58 fun deleteWaiting (rw as Rewrite {waiting,...}) id = 59 updateWaiting rw (IntSet.delete waiting id); 190 fun add (rw as Rewrite {known,...}) (id,eqn) = 191 if IntMap.inDomain id known then rw 194 val Rewrite {order,redexes,subterms,waiting, ...} = rw 204 val rw = value 209 val () = Print.trace pp "Rewrite.add: result" rw 212 rw 515 val rw = value 537 val rw = value 628 val rw = deleteWaiting rw id value 673 val rw = List.foldl addEqn (new order) (enumerate ths) value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/ |
H A D | grammarScript.sml | 52 rw[definition "parsetree_size_def"] >- decide_tac >> 177 rw[derive_def] >> metis_tac [APPEND_ASSOC]); 181 rw[derive_def] >> metis_tac [APPEND_ASSOC]); 194 rw[derive_def, APPEND_EQ_CONS]); 201 ho_match_mp_tac relationTheory.RTC_INDUCT >> rw[] >> 207 ho_match_mp_tac relationTheory.RTC_INDUCT >> rw[] >> 228 ho_match_mp_tac ptree_ind >> rw[] >> Cases_on`pt` >> fs[] >> 229 match_mp_tac RTC1 >> qexists_tac `MAP ptree_head l` >> rw[] >> 230 qpat_x_assum `SS ��� G.rules ' s` (K ALL_TAC) >> Induct_on `l` >> rw[] >> 242 reverse eq_tac >- (rw[] >> r [all...] |
/seL4-l4v-10.1.1/HOL4/examples/countable/ |
H A D | countable_initScript.sml | 11 rw[count_num2_def] >> 12 SELECT_ELIM_TAC >> rw[] >> 28 rw[INJ_DEF,count_num_aux_def]) 36 rw[INJ_DEF,count_char_aux_def,stringTheory.ORD_11]);
|
/seL4-l4v-10.1.1/HOL4/examples/computability/turingMachines/ |
H A D | register_machineScript.sml | 54 `FUNPOW f 2 a = FUNPOW f (SUC (SUC 0)) a` by fs[] >> rw[FUNPOW_SUC]) 58 `FUNPOW f 3 a = FUNPOW f (SUC (SUC (SUC 0))) a` by fs[] >> rw[FUNPOW_SUC]) 67 Induct_on `reg_val rm.regs n` >> rw[] 89 rw[FUNPOW_TWO] 91 by fs[is_halted_def] >> simp[step_def] >> rw[is_halted_def] >> simp[upd_reg_def,FLOOKUP_DEF]) 100 strip_tac >> rw[] 102 >- (Cases_on `args` >> rw[] >> simp[run_reg_def,initial_reg_def,zerof_inst_def,Clear_def]>> 103 Induct_on `h` >>rw[] >>simp[MULT_SUC] >> rw[FUNPOW_ADD,FUNPOW_THREE] >>
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/acl2/ |
H A D | m1_progLib.sml | 84 fun rw (FUN_LET (x,y,t)) = FUN_LET (x, y, rw t) function 85 | rw (FUN_IF (x,t1,t2)) = FUN_IF (x, rw t1, rw t2) 86 | rw (FUN_COND (x,t)) = FUN_COND (x, rw t) 87 | rw (FUN_VAL tm) = 90 val tm3 = ftree2tm (rw (tm2ftree tm2))
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/prog/ |
H A D | riscv_progScript.sml | 92 rw [alignmentTheory.aligned_extract] 99 rw [alignmentTheory.aligned_extract] 108 rw [alignmentTheory.aligned_extract] 120 rw [stateTheory.FRAME_STATE_def, stateTheory.SELECT_STATE_def, 123 \\ rw [] 125 \\ rw [combinTheory.APPLY_UPDATE_THM, riscv_proj_def]
|
/seL4-l4v-10.1.1/HOL4/src/patricia/ |
H A D | sptreeScript.sml | 113 Cases_on `t` >> rw[Once insert_def]); 120 simp[Once insert_def] >> rw[wf_def, insert_notEmpty] >> fs[wf_def]); 135 Induct >> rw[wf_def, delete_def, mk_BN_thm, mk_BS_thm] >> 136 rw[wf_def] >> rw[] >> fs[] >> metis_tac[]); 142 simp[Once insert_def] >> rw[lookup_def]); 156 rw[] >> markerLib.RM_ALL_ABBREVS_TAC >> 172 simp[Once insert_def] >> rw[lookup_def] >> simp[] >| [ 237 rw[optcase_lemma]); 336 rw[optcase_lemm [all...] |