1open HolKernel boolLib bossLib lcsymtacs Parse; 2open integerTheory stringTheory alistTheory listTheory llistTheory pred_setTheory relationTheory; 3open pairTheory optionTheory finite_mapTheory arithmeticTheory; 4 5val _ = set_trace "Goalstack.print_goal_at_top" 0; 6val _ = ParseExtras.temp_tight_equality(); 7 8val _ = new_theory "simple_trace"; 9 10val hd_drop_last_take = Q.store_thm ("hd_drop_last_take", 11`!l n. 0 < n ��� n ��� LENGTH l ��� HD (DROP (n - 1) l) = LAST (TAKE n l)`, 12 Induct_on `l` >> 13 rw [] >> 14 fs [] 15 >- ( 16 `n = 1` by decide_tac >> 17 fs []) >> 18 first_x_assum (qspec_then `n - 1` mp_tac) >> 19 simp [] >> 20 rw [] >> 21 Cases_on `l` >> 22 fs []); 23 24val some_no_choice = Q.store_thm ("some_no_choice", 25`!f. (some x. f x) = NONE ��� ��?x. f x`, 26 rw [some_def]); 27 28val some_exists_determ = Q.store_thm ("some_exists_determ", 29`!f. (!x y. f x ��� f y ��� x = y) ��� ((some x. f x) = SOME a ��� f a)`, 30 rw [some_def] >> 31 metis_tac []); 32 33val monotone_def = Define ` 34 monotone (f : num -> num) ��� 35 !x y. x ��� y ��� f x ��� f y`; 36 37val unbounded_def = Define ` 38 unbounded (f : num -> num) ��� 39 !x. ?y. x < f y`; 40 41 42 43val check_trace_def = Define ` 44 (check_trace step [] ��� T) ��� 45 (check_trace step [s] ��� T) ��� 46 (check_trace step (s1::s2::tr) ��� 47 step s1 = SOME s2 ��� 48 check_trace step (s2::tr))`; 49 50val check_trace_ind = fetch "-" "check_trace_ind"; 51 52val check_trace_thm = Q.store_thm ("check_trace_thm", 53`!step s1 s2. 54 (��s1 s2. step s1 = SOME s2)^* s1 s2 ��� 55 ?tr. tr ��� [] ��� HD tr = s1 ��� LAST tr = s2 ��� check_trace step tr`, 56 rw [] >> 57 eq_tac 58 >- ( 59 qspec_tac (`s2`,`s2`) >> 60 qspec_tac (`s1`,`s1`) >> 61 ho_match_mp_tac RTC_INDUCT >> 62 rw [] 63 >- ( 64 qexists_tac `[s1]` >> 65 rw [check_trace_def]) 66 >- ( 67 qexists_tac `s1::tr` >> 68 rw [LAST_DEF] >> 69 Cases_on `tr` >> 70 fs [check_trace_def])) >> 71 rw [] >> 72 Induct_on `tr` >> 73 rw [LAST_DEF] >> 74 fs [] >> 75 Cases_on `tr` >> 76 fs [check_trace_def] >> 77 rw [Once RTC_CASES1]); 78 79val check_trace_append = Q.store_thm ("check_trace_append", 80`!tr1 tr2. 81 check_trace step (tr1 ++ tr2) ��� 82 if tr1 = [] then 83 check_trace step tr2 84 else if tr2 = [] then 85 check_trace step tr1 86 else 87 check_trace step tr1 ��� check_trace step tr2 ��� step (LAST tr1) = SOME (HD tr2)`, 88 Induct >> 89 rw [] >> 90 Cases_on `tr1` >> 91 rw [check_trace_def] 92 >- ( 93 Cases_on `tr2` >> 94 fs [check_trace_def] >> 95 metis_tac []) >> 96 Cases_on `t` >> 97 fs [check_trace_def] >> 98 metis_tac []); 99 100val step_rel_determ = Q.store_thm ("step_rel_determ", 101`!s s1. 102 (��s1 s2. step s1 = SOME s2)^* s s1 ��� 103 !s2. step s1 = NONE ��� (��s1 s2. step s1 = SOME s2)^* s s2 ��� step s2 = NONE 104 ��� 105 s1 = s2`, 106 ho_match_mp_tac RTC_INDUCT >> 107 rw [] 108 >- ( 109 fs [Once RTC_CASES1] >> 110 fs []) >> 111 rw [] >> 112 first_x_assum match_mp_tac >> 113 rw [] >> 114 qpat_assum `r^* s s2` (assume_tac o SIMP_RULE (srw_ss()) [Once RTC_CASES1]) >> 115 fs [] >> 116 rw [] >> 117 fs [] >> 118 rw []); 119 120val trace_extends = Q.store_thm ("trace_extends", 121`!tr tr'. 122 tr ��� [] ��� tr' ��� [] ��� 123 HD tr = HD tr' ��� 124 LENGTH tr < LENGTH tr' ��� 125 check_trace step tr ��� 126 check_trace step tr' 127 ��� 128 step (LAST tr) ��� NONE`, 129 Induct_on `tr` >> 130 rw [] >> 131 Cases_on `tr'` >> 132 fs [] >> 133 Cases_on `tr` >> 134 fs [] 135 >- ( 136 Cases_on `t` >> 137 fs [check_trace_def]) 138 >- ( 139 Cases_on `t` >> 140 fs [check_trace_def] >> 141 rw [] >> 142 first_x_assum (qspec_then `h'::t''` assume_tac) >> 143 fs [])); 144 145val check_trace_append2 = Q.store_thm ("check_trace_append2", 146`���f ls ls'. 147 check_trace f ls ��� 148 check_trace f ls' ��� 149 f (LAST ls) = SOME (HD ls') ��� 150 check_trace f (ls++ls')`, 151 ho_match_mp_tac check_trace_ind>>rw[]>>fs[check_trace_def]>> 152 Cases_on`ls'`>>fs[check_trace_def]) 153 154val check_trace_drop = Q.store_thm ("check_trace_drop", 155`!tr n. 156 check_trace step tr ��� 157 n ��� LENGTH tr 158 ��� 159 check_trace step (DROP n tr)`, 160 Induct_on `n` >> 161 rw [] >> 162 Cases_on `tr` >> 163 fs [] >> 164 first_x_assum (qspec_then `t` match_mp_tac) >> 165 rw [] >> 166 Cases_on `t` >> 167 fs [check_trace_def]); 168 169val check_trace_twice_take = Q.store_thm ("check_trace_twice_take", 170`!tr tr'. 171 tr ��� [] ��� tr' ��� [] ��� 172 HD tr = HD tr' ��� 173 LENGTH tr ��� LENGTH tr' ��� 174 check_trace step tr ��� 175 check_trace step tr' 176 ��� 177 TAKE (LENGTH tr) tr' = tr`, 178 Induct_on `tr` >> 179 simp [] >> 180 gen_tac >> 181 Cases_on `tr'` >> 182 fs [] >> 183 DISCH_TAC >> 184 Cases_on `tr` >> 185 Cases_on `t` >> 186 fs [check_trace_def] >> 187 fs [] >> 188 rw [] >> 189 first_x_assum (qspec_then `h'::t''` strip_assume_tac) >> 190 rfs []); 191 192val check_trace_twice_take = Q.store_thm ("check_trace_twice_suff", 193`!tr tr'. 194 tr ��� [] ��� tr' ��� [] ��� 195 HD tr = HD tr' ��� 196 LENGTH tr ��� LENGTH tr' ��� 197 check_trace step tr ��� 198 check_trace step tr' 199 ��� 200 HD (DROP (LENGTH tr - 1) tr') = (LAST tr) `, 201 rw [] >> 202 `TAKE (LENGTH tr) tr' = tr` by metis_tac [check_trace_twice_take] >> 203 fs [] >> 204 `0 < LENGTH tr ��� LENGTH tr ��� LENGTH tr'` by (rw [] >> Cases_on `tr` >> fs [] >> decide_tac) >> 205 metis_tac [hd_drop_last_take]); 206 207val _ = export_theory (); 208