# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1362314682 0
# Node ID 1d6a0fd9f7f488ff04ba851cdafa0f1878d55442
# Parent  5e2e576fac7cc190398c2fb991831bd95bb17dde
added factorial as an example

diff -r 5e2e576fac7c -r 1d6a0fd9f7f4 Tests/Test1.thy
--- a/Tests/Test1.thy	Sun Mar 03 00:18:13 2013 +0000
+++ b/Tests/Test1.thy	Sun Mar 03 12:44:42 2013 +0000
@@ -1,5 +1,5 @@
 theory Test1
-imports Main
+imports "../thys/Uncomputable"
 begin
 
 ML {*
@@ -178,11 +178,11 @@
 by (metis One_nat_def nat_case_Suc)
 
 lemma 
-  "rec_ci (constn 0) = XXX"
+  "rec_ci (constn 0) = ([Goto 1], 1, 2)"
 apply(tactic {*
   timing_wrapper (asm_full_simp_tac @{simpset} 1)
 *})
-oops
+done
 
 lemma 
   "rec_ci (constn 10) = XXX"
@@ -213,4 +213,24 @@
 apply(simp)
 oops
 
+fun mopup_a :: "nat \<Rightarrow> instr list"
+  where
+  "mopup_a 0 = []" |
+  "mopup_a (Suc n) = mopup_a n @ 
+       [(R, 2*n + 3), (W0, 2*n + 2), (R, 2*n + 1), (W1, 2*n + 2)]"
+
+definition mopup_b :: "instr list"
+  where
+  "mopup_b \<equiv> [(R, 2), (R, 1), (L, 5), (W0, 3), (R, 4), (W0, 3),
+            (R, 2), (W0, 3), (L, 5), (L, 6), (R, 0), (L, 6)]"
+
+fun mopup :: "nat \<Rightarrow> instr list"
+  where 
+  "mopup n = mopup_a n @ shift mopup_b (2*n)"
+
+
+lemma
+  "tcopy |+| mopup 0 = XXX"
+apply(simp add: tm_comp.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def mopup_b_def)
+apply(simp add: adjust.simps shift.simps)
 end
\ No newline at end of file