theory Test1

imports "../thys/Uncomputable"

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) = ([Goto 1], 1, 2)"

apply(tactic {*

  timing_wrapper (asm_full_simp_tac @{simpset} 1)

*})

done

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

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