--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Tests/Test1.thy Fri Mar 01 11:16:30 2013 +0000
@@ -0,0 +1,216 @@
+theory Test1
+imports Main
+begin
+
+ML {*
+fun timing_wrapper tac st =
+let
+ val t_start = Timing.start ();
+ val res = tac st;
+ val t_end = Timing.result t_start;
+in
+ (tracing (Timing.message t_end); res)
+end
+*}
+
+
+datatype abc_inst =
+ Inc nat
+ | Dec nat nat
+ | Goto nat
+
+type_synonym abc_prog = "abc_inst list"
+
+datatype recf =
+ z
+| s
+| id nat nat --"Projection"
+| Cn nat recf "recf list" --"Composition"
+| Pr nat recf recf --"Primitive recursion"
+| Mn nat recf --"Minimisation"
+
+
+
+fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
+ where
+ "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]"
+
+fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
+ where
+ "mv_box m n = [Dec m 3, Inc n, Goto 0]"
+
+fun abc_inst_shift :: "abc_inst \<Rightarrow> nat \<Rightarrow> abc_inst"
+ where
+ "abc_inst_shift (Inc m) n = Inc m" |
+ "abc_inst_shift (Dec m e) n = Dec m (e + n)" |
+ "abc_inst_shift (Goto m) n = Goto (m + n)"
+
+fun abc_shift :: "abc_inst list \<Rightarrow> nat \<Rightarrow> abc_inst list"
+ where
+ "abc_shift [] n = []"
+| "abc_shift (x#xs) n = (abc_inst_shift x n) # (abc_shift xs n)"
+
+fun abc_append :: "abc_inst list \<Rightarrow> abc_inst list \<Rightarrow> abc_inst list" (infixl "[+]" 60)
+ where
+ "abc_append al bl = al @ abc_shift bl (length al)"
+
+lemma [simp]:
+ "length (pa [+] pb) = length pa + length pb"
+by (induct pb) (auto)
+
+
+text {* The compilation of @{text "z"}-operator. *}
+definition rec_ci_z :: "abc_inst list"
+ where
+ [simp]: "rec_ci_z = [Goto 1]"
+
+
+text {* The compilation of @{text "s"}-operator. *}
+definition rec_ci_s :: "abc_inst list"
+ where
+ "rec_ci_s \<equiv> (addition 0 1 2 [+] [Inc 1])"
+
+lemma [simp]:
+ "rec_ci_s = [Dec 0 4, Inc 1, Inc 2, Goto 0, Dec 2 7, Inc 0, Goto 4, Inc 1] "
+by (simp add: rec_ci_s_def)
+
+text {* The compilation of @{text "id i j"}-operator *}
+fun rec_ci_id :: "nat \<Rightarrow> nat \<Rightarrow> abc_inst list"
+ where
+ "rec_ci_id i j = addition j i (i + 1)"
+
+fun mv_boxes :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list"
+ where
+ "mv_boxes ab bb n = (case n of
+ 0 => []
+ | Suc n => mv_boxes ab bb n [+] mv_box (ab + n) (bb + n))"
+
+fun empty_boxes :: "nat \<Rightarrow> abc_inst list"
+ where
+ "empty_boxes n = (case n of
+ 0 => []
+ | Suc n => empty_boxes n [+] [Dec n 2, Goto 0])"
+
+fun cn_merge_gs ::
+ "(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list"
+ where
+ "cn_merge_gs [] p = []" |
+ "cn_merge_gs (g # gs) p =
+ (let (gprog, gpara, gn) = g in
+ gprog [+] mv_box gpara p [+] cn_merge_gs gs (Suc p))"
+
+fun list_max :: "nat list \<Rightarrow> nat"
+ where
+ "list_max [] = 0"
+| "list_max (x#xs) = (let y = list_max xs in
+ if (y < x) then x else y)"
+
+fun rec_ci :: "recf \<Rightarrow> abc_inst list \<times> nat \<times> nat"
+ where
+ "rec_ci z = (rec_ci_z, 1, 2)" |
+ "rec_ci s = (rec_ci_s, 1, 3)" |
+ "rec_ci (id m n) = (rec_ci_id m n, m, m + 2)" |
+ "rec_ci (Cn n f gs) =
+ (let cied_gs = map rec_ci gs in
+ let (fprog, fpara, fn) = rec_ci f in
+ let pstr = list_max (Suc n # fn # (map (\<lambda> (aprog, p, n). n) cied_gs)) in
+ let qstr = pstr + Suc (length gs) in
+ (cn_merge_gs cied_gs pstr [+] mv_boxes 0 qstr n [+]
+ mv_boxes pstr 0 (length gs) [+] fprog [+]
+ mv_box fpara pstr [+] empty_boxes (length gs) [+]
+ mv_box pstr n [+] mv_boxes qstr 0 n, n, qstr + n))" |
+ "rec_ci (Pr n f g) =
+ (let (fprog, fpara, fn) = rec_ci f in
+ let (gprog, gpara, gn) = rec_ci g in
+ let p = list_max [n + 3, fn, gn] in
+ let e = length gprog + 7 in
+ (mv_box n p [+] fprog [+] mv_box n (Suc n) [+]
+ (([Dec p e] [+] gprog [+]
+ [Inc n, Dec (Suc n) 3, Goto 1]) @
+ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gprog + 4)]),
+ Suc n, p + 1))" |
+ "rec_ci (Mn n f) =
+ (let (fprog, fpara, fn) = rec_ci f in
+ let len = length (fprog) in
+ (fprog @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),
+ Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn))"
+
+definition rec_add :: "recf"
+ where
+ [simp]: "rec_add \<equiv> Pr 1 (id 1 0) (Cn 3 s [id 3 2])"
+
+fun constn :: "nat \<Rightarrow> recf" where
+ "constn n = (case n of
+ 0 => z |
+ Suc n => Cn 1 s [constn n])"
+
+ML {*
+fun dest_suc_trm @{term "Suc 0"} = raise TERM ("Suc 0", [])
+ | dest_suc_trm @{term "Suc (Suc 0)"} = 2
+ | dest_suc_trm (@{term "Suc"} $ t) = 1 + dest_suc_trm t
+ | dest_suc_trm t = snd (HOLogic.dest_number t)
+
+fun get_thm ctxt (t, n) =
+let
+ val num = HOLogic.mk_number @{typ "nat"} n
+ val goal = Logic.mk_equals (t, num)
+ val num_ss = HOL_ss addsimps @{thms semiring_norm}
+in
+ Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))
+end
+
+fun nat_number_simproc ss ctrm =
+let
+ val trm = term_of ctrm
+ val ctxt = Simplifier.the_context ss
+in
+ SOME (get_thm ctxt (trm, dest_suc_trm trm))
+ handle TERM _ => NONE
+end
+*}
+
+simproc_setup nat_number ("Suc n") = {* K nat_number_simproc*}
+
+declare Nat.One_nat_def[simp del]
+
+lemma [simp]:
+ shows "nat_case g f (1::nat) = f (0::nat)"
+by (metis One_nat_def nat_case_Suc)
+
+lemma
+ "rec_ci (constn 0) = XXX"
+apply(tactic {*
+ timing_wrapper (asm_full_simp_tac @{simpset} 1)
+*})
+oops
+
+lemma
+ "rec_ci (constn 10) = XXX"
+apply(tactic {*
+ timing_wrapper (asm_full_simp_tac @{simpset} 1)
+*})
+oops
+
+lemma
+ "rec_ci (constn 3) = XXX"
+apply(tactic {*
+ timing_wrapper (asm_full_simp_tac @{simpset} 1)
+*})
+oops
+
+lemma
+ "rec_ci (rec_add) = XXX"
+apply(simp del: abc_append.simps)
+apply(simp)
+oops
+
+definition rec_mult :: "recf"
+ where
+ [simp]: "rec_mult = Pr 1 z (Cn 3 rec_add [id 3 0, id 3 2])"
+
+lemma
+ "rec_ci (rec_mult) = XXX"
+apply(simp)
+oops
+
+end
\ No newline at end of file