equal
deleted
inserted
replaced
1 theory Test1 |
1 theory Test1 |
2 imports Main |
2 imports "../thys/Uncomputable" |
3 begin |
3 begin |
4 |
4 |
5 ML {* |
5 ML {* |
6 fun timing_wrapper tac st = |
6 fun timing_wrapper tac st = |
7 let |
7 let |
176 lemma [simp]: |
176 lemma [simp]: |
177 shows "nat_case g f (1::nat) = f (0::nat)" |
177 shows "nat_case g f (1::nat) = f (0::nat)" |
178 by (metis One_nat_def nat_case_Suc) |
178 by (metis One_nat_def nat_case_Suc) |
179 |
179 |
180 lemma |
180 lemma |
181 "rec_ci (constn 0) = XXX" |
181 "rec_ci (constn 0) = ([Goto 1], 1, 2)" |
182 apply(tactic {* |
182 apply(tactic {* |
183 timing_wrapper (asm_full_simp_tac @{simpset} 1) |
183 timing_wrapper (asm_full_simp_tac @{simpset} 1) |
184 *}) |
184 *}) |
185 oops |
185 done |
186 |
186 |
187 lemma |
187 lemma |
188 "rec_ci (constn 10) = XXX" |
188 "rec_ci (constn 10) = XXX" |
189 apply(tactic {* |
189 apply(tactic {* |
190 timing_wrapper (asm_full_simp_tac @{simpset} 1) |
190 timing_wrapper (asm_full_simp_tac @{simpset} 1) |
211 lemma |
211 lemma |
212 "rec_ci (rec_mult) = XXX" |
212 "rec_ci (rec_mult) = XXX" |
213 apply(simp) |
213 apply(simp) |
214 oops |
214 oops |
215 |
215 |
216 end |
216 fun mopup_a :: "nat \<Rightarrow> instr list" |
|
217 where |
|
218 "mopup_a 0 = []" | |
|
219 "mopup_a (Suc n) = mopup_a n @ |
|
220 [(R, 2*n + 3), (W0, 2*n + 2), (R, 2*n + 1), (W1, 2*n + 2)]" |
|
221 |
|
222 definition mopup_b :: "instr list" |
|
223 where |
|
224 "mopup_b \<equiv> [(R, 2), (R, 1), (L, 5), (W0, 3), (R, 4), (W0, 3), |
|
225 (R, 2), (W0, 3), (L, 5), (L, 6), (R, 0), (L, 6)]" |
|
226 |
|
227 fun mopup :: "nat \<Rightarrow> instr list" |
|
228 where |
|
229 "mopup n = mopup_a n @ shift mopup_b (2*n)" |
|
230 |
|
231 |
|
232 lemma |
|
233 "tcopy |+| mopup 0 = XXX" |
|
234 apply(simp add: tm_comp.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def mopup_b_def) |
|
235 apply(simp add: adjust.simps shift.simps) |
|
236 end |