(* Title: thys/Recursive.thy

   Author: Jian Xu, Xingyuan Zhang, and Christian Urban

*)

header {* Translating Recursive Functions into Abacus Machines *}

theory Recursive

imports Rec_Def Abacus

begin

text {*

  Some auxilliary Abacus machines used to construct the result Abacus machines.

*}

text {*

  @{text "get_paras_num recf"} returns the arity of recursive function @{text "recf"}.

*}

fun get_paras_num :: "recf \<Rightarrow> nat"

  where

  "get_paras_num z = 1" |

  "get_paras_num s = 1" |

  "get_paras_num (id m n) = m" |

  "get_paras_num (Cn n f gs) = n" |

  "get_paras_num (Pr n f g) = Suc n"  |

  "get_paras_num (Mn n f) = n"  

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 xs n = map (\<lambda> x. abc_inst_shift x n) xs" 

fun abc_append :: "abc_inst list \<Rightarrow> abc_inst list \<Rightarrow> 

                           abc_inst list" (infixl "[+]" 60)

  where

  "abc_append al bl = (let al_len = length al in 

                           al @ abc_shift bl al_len)"

text {* The compilation of @{text "z"}-operator. *}

definition rec_ci_z :: "abc_inst list"

  where

  "rec_ci_z \<equiv> [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])"

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 0 = []" |

  "mv_boxes ab bb (Suc n) = mv_boxes ab bb n [+] mv_box (ab + n) (bb + n)"

fun empty_boxes :: "nat \<Rightarrow> abc_inst list"

  where

  "empty_boxes 0 = []" |

  "empty_boxes (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))"

text {*

  The compiler of recursive functions, where @{text "rec_ci recf"} return 

  @{text "(ap, arity, fp)"}, where @{text "ap"} is the Abacus program, @{text "arity"} is the 

  arity of the recursive function @{text "recf"}, 

  @{text "fp"} is the amount of memory which is going to be

  used by @{text "ap"} for its execution. 

*}

function 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 (\<lambda> g. rec_ci g) (f # gs) in

       let (fprog, fpara, fn) = hd cied_gs in 

       let pstr = 

        Max (set (Suc n # fn # (map (\<lambda> (aprog, p, n). n) cied_gs))) in

       let qstr = pstr + Suc (length gs) in 

       (cn_merge_gs (tl 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 = Max (set ([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))"

  by pat_completeness auto

termination 

proof

  show "wf (measure size)" by auto

next

  fix n f gs x

  assume "(x::recf) \<in> set (f # gs)" 

  thus "(x, Cn n f gs) \<in> measure size"

    by(induct gs, auto)

next

  fix n f g

  show "(f, Pr n f g) \<in> measure size" by auto

next

  fix n f g x xa y xb ya

  show "(g, Pr n f g) \<in> measure size" by auto

next

  fix n f

  show "(f, Mn n f) \<in> measure size" by auto

qed

declare rec_ci.simps [simp del] rec_ci_s_def[simp del] 

        rec_ci_z_def[simp del] rec_ci_id.simps[simp del]

        mv_boxes.simps[simp del] abc_append.simps[simp del]

        mv_box.simps[simp del] addition.simps[simp del]

declare abc_steps_l.simps[simp del] abc_fetch.simps[simp del] 

        abc_step_l.simps[simp del] 

lemma abc_steps_add: 

  "abc_steps_l (as, lm) ap (m + n) = 

         abc_steps_l (abc_steps_l (as, lm) ap m) ap n"

apply(induct m arbitrary: n as lm, simp add: abc_steps_l.simps)

proof -

  fix m n as lm

  assume ind: 

    "\<And>n as lm. abc_steps_l (as, lm) ap (m + n) = 

                   abc_steps_l (abc_steps_l (as, lm) ap m) ap n"

  show "abc_steps_l (as, lm) ap (Suc m + n) = 

             abc_steps_l (abc_steps_l (as, lm) ap (Suc m)) ap n"

    apply(insert ind[of as lm "Suc n"], simp)

    apply(insert ind[of as lm "Suc 0"], simp add: abc_steps_l.simps)

    apply(case_tac "(abc_steps_l (as, lm) ap m)", simp)

    apply(simp add: abc_steps_l.simps)

    apply(case_tac "abc_step_l (a, b) (abc_fetch a ap)", 

          simp add: abc_steps_l.simps)

    done

qed

(*lemmas: rec_ci and rec_calc_rel*)

lemma rec_calc_inj_case_z: 

  "\<lbrakk>rec_calc_rel z l x; rec_calc_rel z l y\<rbrakk> \<Longrightarrow> x = y"

apply(auto elim: calc_z_reverse)

done

lemma  rec_calc_inj_case_s: 

  "\<lbrakk>rec_calc_rel s l x; rec_calc_rel s l y\<rbrakk> \<Longrightarrow> x = y"

apply(auto elim: calc_s_reverse)

done

lemma rec_calc_inj_case_id:

  "\<lbrakk>rec_calc_rel (recf.id nat1 nat2) l x;

    rec_calc_rel (recf.id nat1 nat2) l y\<rbrakk> \<Longrightarrow> x = y"

apply(auto elim: calc_id_reverse)

done

lemma rec_calc_inj_case_mn:

  assumes ind: "\<And> l x y. \<lbrakk>rec_calc_rel f l x; rec_calc_rel f l y\<rbrakk> 

           \<Longrightarrow> x = y" 

  and h: "rec_calc_rel (Mn n f) l x" "rec_calc_rel (Mn n f) l y"

  shows "x = y"

  apply(insert h)

  apply(elim  calc_mn_reverse)

  apply(case_tac "x > y", simp)

  apply(erule_tac x = "y" in allE, auto)

proof -

  fix v va

  assume "rec_calc_rel f (l @ [y]) 0" 

    "rec_calc_rel f (l @ [y]) v"  

    "0 < v"

  thus "False"

    apply(insert ind[of "l @ [y]" 0 v], simp)

    done

next

  fix v va

  assume 

    "rec_calc_rel f (l @ [x]) 0" 

    "\<forall>x<y. \<exists>v. rec_calc_rel f (l @ [x]) v \<and> 0 < v" "\<not> y < x"

  thus "x = y"

    apply(erule_tac x = "x" in allE)

    apply(case_tac "x = y", auto)

    apply(drule_tac y = v in ind, simp, simp)

    done

qed 

lemma rec_calc_inj_case_pr: 

  assumes f_ind: 

  "\<And>l x y. \<lbrakk>rec_calc_rel f l x; rec_calc_rel f l y\<rbrakk> \<Longrightarrow> x = y"

  and g_ind:

  "\<And>x xa y xb ya l xc yb. 

  \<lbrakk>x = rec_ci f; (xa, y) = x; (xb, ya) = y; 

  rec_calc_rel g l xc; rec_calc_rel g l yb\<rbrakk> \<Longrightarrow> xc = yb"

  and h: "rec_calc_rel (Pr n f g) l x" "rec_calc_rel (Pr n f g) l y"  

  shows "x = y"

  apply(case_tac "rec_ci f")

proof -

  fix a b c

  assume "rec_ci f = (a, b, c)"

  hence ng_ind: 

    "\<And> l xc yb. \<lbrakk>rec_calc_rel g l xc; rec_calc_rel g l yb\<rbrakk>

    \<Longrightarrow> xc = yb"

    apply(insert g_ind[of "(a, b, c)" "a" "(b, c)" b c], simp)

    done

  from h show "x = y"

    apply(erule_tac calc_pr_reverse, erule_tac calc_pr_reverse)

    apply(erule f_ind, simp, simp)

    apply(erule_tac calc_pr_reverse, simp, simp)

  proof -

    fix la ya ry laa yaa rya

    assume k1:  "rec_calc_rel g (la @ [ya, ry]) x" 

      "rec_calc_rel g (la @ [ya, rya]) y"

      and k2: "rec_calc_rel (Pr (length la) f g) (la @ [ya]) ry"

              "rec_calc_rel (Pr (length la) f g) (la @ [ya]) rya"

    from k2 have "ry = rya"

      apply(induct ya arbitrary: ry rya)

      apply(erule_tac calc_pr_reverse, 

        erule_tac calc_pr_reverse, simp)

      apply(erule f_ind, simp, simp, simp)

      apply(erule_tac calc_pr_reverse, simp)

      apply(erule_tac rSucy = rya in calc_pr_reverse, simp, simp)

    proof -

      fix ya ry rya l y ryb laa yb ryc

      assume ind:

        "\<And>ry rya. \<lbrakk>rec_calc_rel (Pr (length l) f g) (l @ [y]) ry; 

                   rec_calc_rel (Pr (length l) f g) (l @ [y]) rya\<rbrakk> \<Longrightarrow> ry = rya"

        and j: "rec_calc_rel (Pr (length l) f g) (l @ [y]) ryb"

        "rec_calc_rel g (l @ [y, ryb]) ry" 

        "rec_calc_rel (Pr (length l) f g) (l @ [y]) ryc" 

        "rec_calc_rel g (l @ [y, ryc]) rya"

      from j show "ry = rya"

	apply(insert ind[of ryb ryc], simp)

	apply(insert ng_ind[of "l @ [y, ryc]" ry rya], simp)

	done

    qed 

    from k1 and this show "x = y"

      apply(simp)

      apply(insert ng_ind[of "la @ [ya, rya]" x y], simp)

      done

  qed  

qed

lemma Suc_nth_part_eq:

  "\<forall>k<Suc (length list). (a # xs) ! k = (aa # list) ! k

       \<Longrightarrow> \<forall>k<(length list). (xs) ! k = (list) ! k"

apply(rule allI, rule impI)

apply(erule_tac x = "Suc k" in allE, simp)

done

lemma list_eq_intro:  

  "\<lbrakk>length xs = length ys; \<forall> k < length xs. xs ! k = ys ! k\<rbrakk> 

  \<Longrightarrow> xs = ys"

apply(induct xs arbitrary: ys, simp)

apply(case_tac ys, simp, simp)

proof -

  fix a xs ys aa list

  assume ind: 

    "\<And>ys. \<lbrakk>length list = length ys; \<forall>k<length ys. xs ! k = ys ! k\<rbrakk>

    \<Longrightarrow> xs = ys"

    and h: "length xs = length list" 

    "\<forall>k<Suc (length list). (a # xs) ! k = (aa # list) ! k"

  from h show "a = aa \<and> xs = list"

    apply(insert ind[of list], simp)

    apply(frule Suc_nth_part_eq, simp)

    apply(erule_tac x = "0" in allE, simp)

    done

qed

lemma rec_calc_inj_case_cn: 

  assumes ind: 

  "\<And>x l xa y.

  \<lbrakk>x = f \<or> x \<in> set gs; rec_calc_rel x l xa; rec_calc_rel x l y\<rbrakk>

  \<Longrightarrow> xa = y"

  and h: "rec_calc_rel (Cn n f gs) l x" 

         "rec_calc_rel (Cn n f gs) l y"

  shows "x = y"

  apply(insert h, elim  calc_cn_reverse)

  apply(subgoal_tac "rs = rsa")

  apply(rule_tac x = f and l = rsa and xa = x and y = y in ind, 

        simp, simp, simp)

  apply(intro list_eq_intro, simp, rule allI, rule impI)

  apply(erule_tac x = k in allE, rule_tac x = k in allE, simp, simp)

  apply(rule_tac x = "gs ! k" in ind, simp, simp, simp)

  done

lemma rec_calc_inj:

  "\<lbrakk>rec_calc_rel f l x; 

    rec_calc_rel f l y\<rbrakk> \<Longrightarrow> x = y"

apply(induct f arbitrary: l x y rule: rec_ci.induct)

apply(simp add: rec_calc_inj_case_z)

apply(simp add: rec_calc_inj_case_s)

apply(simp add: rec_calc_inj_case_id, simp)

apply(erule rec_calc_inj_case_cn,simp, simp)

apply(erule rec_calc_inj_case_pr, auto)

apply(erule rec_calc_inj_case_mn, auto)

done

lemma calc_rel_reverse_ind_step_ex: 

  "\<lbrakk>rec_calc_rel (Pr n f g) (lm @ [Suc x]) rs\<rbrakk> 

  \<Longrightarrow> \<exists> rs. rec_calc_rel (Pr n f g) (lm @ [x]) rs"

apply(erule calc_pr_reverse, simp, simp)

apply(rule_tac x = rk in exI, simp)

done

lemma [simp]: "Suc x \<le> y \<Longrightarrow> Suc (y - Suc x) = y - x"

by arith

lemma calc_pr_para_not_null: 

  "rec_calc_rel (Pr n f g) lm rs \<Longrightarrow> lm \<noteq> []"

apply(erule calc_pr_reverse, simp, simp)

done

lemma calc_pr_less_ex: 

 "\<lbrakk>rec_calc_rel (Pr n f g) lm rs; x \<le> last lm\<rbrakk> \<Longrightarrow> 

 \<exists>rs. rec_calc_rel (Pr n f g) (butlast lm @ [last lm - x]) rs"

apply(subgoal_tac "lm \<noteq> []")

apply(induct x, rule_tac x = rs in exI, simp, simp, erule exE)

apply(rule_tac rs = xa in calc_rel_reverse_ind_step_ex, simp)

apply(simp add: calc_pr_para_not_null)

done

lemma calc_pr_zero_ex:

  "rec_calc_rel (Pr n f g) lm rs \<Longrightarrow> 

             \<exists>rs. rec_calc_rel f (butlast lm) rs"

apply(drule_tac x = "last lm" in calc_pr_less_ex, simp,

      erule_tac exE, simp)

apply(erule_tac calc_pr_reverse, simp)

apply(rule_tac x = rs in exI, simp, simp)

done

lemma abc_steps_ind: 

  "abc_steps_l (as, am) ap (Suc stp) =

          abc_steps_l (abc_steps_l (as, am) ap stp) ap (Suc 0)"

apply(insert abc_steps_add[of as am ap stp "Suc 0"], simp)

done

lemma abc_steps_zero: "abc_steps_l asm ap 0 = asm"

apply(case_tac asm, simp add: abc_steps_l.simps)

done

lemma abc_append_nth: 

  "n < length ap + length bp \<Longrightarrow> 

       (ap [+] bp) ! n =

         (if n < length ap then ap ! n 

          else abc_inst_shift (bp ! (n - length ap)) (length ap))"

apply(simp add: abc_append.simps nth_append map_nth split: if_splits)

done

lemma abc_state_keep:  

  "as \<ge> length bp \<Longrightarrow> abc_steps_l (as, lm) bp stp = (as, lm)"

apply(induct stp, simp add: abc_steps_zero)

apply(simp add: abc_steps_ind)

apply(simp add: abc_steps_zero)

apply(simp add: abc_steps_l.simps abc_fetch.simps abc_step_l.simps)

done

lemma abc_halt_equal: 

  "\<lbrakk>abc_steps_l (0, lm) bp stpa = (length bp, lm1); 

    abc_steps_l (0, lm) bp stpb = (length bp, lm2)\<rbrakk> \<Longrightarrow> lm1 = lm2"

apply(case_tac "stpa - stpb > 0")

apply(insert abc_steps_add[of 0 lm bp stpb "stpa - stpb"], simp)

apply(insert abc_state_keep[of bp "length bp" lm2 "stpa - stpb"], 

      simp, simp add: abc_steps_zero)

apply(insert abc_steps_add[of 0 lm bp stpa "stpb - stpa"], simp)

apply(insert abc_state_keep[of bp "length bp" lm1 "stpb - stpa"], 

      simp)

done  

lemma abc_halt_point_ex: 

  "\<lbrakk>\<exists>stp. abc_steps_l (0, lm) bp stp = (bs, lm');

    bs = length bp; bp \<noteq> []\<rbrakk> 

  \<Longrightarrow> \<exists> stp. (\<lambda> (s, l). s < bs \<and> 

              (abc_steps_l (s, l) bp (Suc 0)) = (bs, lm')) 

      (abc_steps_l (0, lm) bp stp) "

apply(erule_tac exE)

proof -

  fix stp

  assume "bs = length bp" 

         "abc_steps_l (0, lm) bp stp = (bs, lm')" 

         "bp \<noteq> []"

  thus 

    "\<exists>stp. (\<lambda>(s, l). s < bs \<and> 

      abc_steps_l (s, l) bp (Suc 0) = (bs, lm')) 

                       (abc_steps_l (0, lm) bp stp)"

    apply(induct stp, simp add: abc_steps_zero, simp)

  proof -

    fix stpa

    assume ind: 

     "abc_steps_l (0, lm) bp stpa = (length bp, lm')

       \<Longrightarrow> \<exists>stp. (\<lambda>(s, l). s < length bp  \<and> abc_steps_l (s, l) bp 

             (Suc 0) = (length bp, lm')) (abc_steps_l (0, lm) bp stp)"

    and h: "abc_steps_l (0, lm) bp (Suc stpa) = (length bp, lm')" 

           "abc_steps_l (0, lm) bp stp = (length bp, lm')" 

           "bp \<noteq> []"

    from h show 

      "\<exists>stp. (\<lambda>(s, l). s < length bp \<and> abc_steps_l (s, l) bp (Suc 0)

                    = (length bp, lm')) (abc_steps_l (0, lm) bp stp)"

      apply(case_tac "abc_steps_l (0, lm) bp stpa", 

            case_tac "a = length bp")

      apply(insert ind, simp)

      apply(subgoal_tac "b = lm'", simp)

      apply(rule_tac abc_halt_equal, simp, simp)

      apply(rule_tac x = stpa in exI, simp add: abc_steps_ind)

      apply(simp add: abc_steps_zero)

      apply(rule classical, simp add: abc_steps_l.simps 

                             abc_fetch.simps abc_step_l.simps)

      done

  qed

qed  

lemma abc_append_empty_r[simp]: "[] [+] ab = ab"

apply(simp add: abc_append.simps abc_inst_shift.simps)

apply(induct ab, simp, simp)

apply(case_tac a, simp_all add: abc_inst_shift.simps)

done

lemma abc_append_empty_l[simp]:  "ab [+] [] = ab"

apply(simp add: abc_append.simps abc_inst_shift.simps)

done

lemma abc_append_length[simp]:  

  "length (ap [+] bp) = length ap + length bp"

apply(simp add: abc_append.simps)

done

declare Let_def[simp]

lemma abc_append_commute: "as [+] bs [+] cs = as [+] (bs [+] cs)"

apply(simp add: abc_append.simps abc_shift.simps abc_inst_shift.simps)

apply(induct cs, simp, simp)

apply(case_tac a, auto simp: abc_inst_shift.simps Let_def)

done

lemma abc_halt_point_step[simp]: 

  "\<lbrakk>a < length bp; abc_steps_l (a, b) bp (Suc 0) = (length bp, lm')\<rbrakk>

  \<Longrightarrow> abc_steps_l (length ap + a, b) (ap [+] bp [+] cp) (Suc 0) = 

                                        (length ap + length bp, lm')"

apply(simp add: abc_steps_l.simps abc_fetch.simps abc_append_nth)

apply(case_tac "bp ! a", 

                      auto simp: abc_steps_l.simps abc_step_l.simps)

done

lemma abc_step_state_in:

  "\<lbrakk>bs < length bp;  abc_steps_l (a, b) bp (Suc 0) = (bs, l)\<rbrakk>

  \<Longrightarrow> a < length bp"

apply(simp add: abc_steps_l.simps abc_fetch.simps)

apply(rule_tac classical, 

      simp add: abc_step_l.simps abc_steps_l.simps)

done

lemma abc_append_state_in_exc: 

  "\<lbrakk>bs < length bp; abc_steps_l (0, lm) bp stpa = (bs, l)\<rbrakk>

 \<Longrightarrow> abc_steps_l (length ap, lm) (ap [+] bp [+] cp) stpa = 

                                             (length ap + bs, l)"

apply(induct stpa arbitrary: bs l, simp add: abc_steps_zero)

proof -

  fix stpa bs l

  assume ind: 

    "\<And>bs l. \<lbrakk>bs < length bp; abc_steps_l (0, lm) bp stpa = (bs, l)\<rbrakk>

    \<Longrightarrow> abc_steps_l (length ap, lm) (ap [+] bp [+] cp) stpa = 

                                                (length ap + bs, l)"

    and h: "bs < length bp" 

           "abc_steps_l (0, lm) bp (Suc stpa) = (bs, l)"

  from h show 

    "abc_steps_l (length ap, lm) (ap [+] bp [+] cp) (Suc stpa) = 

                                                (length ap + bs, l)"

    apply(simp add: abc_steps_ind)

    apply(case_tac "(abc_steps_l (0, lm) bp stpa)", simp)

  proof -

    fix a b

    assume g: "abc_steps_l (0, lm) bp stpa = (a, b)" 

              "abc_steps_l (a, b) bp (Suc 0) = (bs, l)"

    from h and g have k1: "a < length bp"

      apply(simp add: abc_step_state_in)

      done

    from h and g and k1 show 

   "abc_steps_l (abc_steps_l (length ap, lm) (ap [+] bp [+] cp) stpa) 

              (ap [+] bp [+] cp) (Suc 0) = (length ap + bs, l)"

      apply(insert ind[of a b], simp)

      apply(simp add: abc_steps_l.simps abc_fetch.simps 

                      abc_append_nth)

      apply(case_tac "bp ! a", auto simp: 

                                 abc_steps_l.simps abc_step_l.simps)

      done

  qed

qed