theory Recursive

imports Abacus Rec_Def Abacus_Hoare

begin

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]"

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

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]"

  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. 

*}

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

       let (fprog, fpara, fn) = rec_ci f 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 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))"

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] 

        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] 

  where

  "addition_inv (as, lm') m n p lm = 

        (let sn = lm ! n in

         let sm = lm ! m in

         lm ! p = 0 \<and>

             (if as = 0 then \<exists> x. x \<le> lm ! m \<and> lm' = lm[m := x,

                                    n := (sn + sm - x), p := (sm - x)]

             else if as = 1 then \<exists> x. x < lm ! m \<and> lm' = lm[m := x,

                            n := (sn + sm - x - 1), p := (sm - x - 1)]

             else if as = 2 then \<exists> x. x < lm ! m \<and> lm' = lm[m := x, 

                               n := (sn + sm - x), p := (sm - x - 1)]

             else if as = 3 then \<exists> x. x < lm ! m \<and> lm' = lm[m := x,

                                   n := (sn + sm - x), p := (sm - x)]

             else if as = 4 then \<exists> x. x \<le> lm ! m \<and> lm' = lm[m := x,

                                       n := (sn + sm), p := (sm - x)] 

             else if as = 5 then \<exists> x. x < lm ! m \<and> lm' = lm[m := x, 

                                  n := (sn + sm), p := (sm - x - 1)] 

             else if as = 6 then \<exists> x. x < lm ! m \<and> lm' =

                     lm[m := Suc x, n := (sn + sm), p := (sm - x - 1)]

             else if as = 7 then lm' = lm[m := sm, n := (sn + sm)]

             else False))"

fun addition_stage1 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"

  where

  "addition_stage1 (as, lm) m p = 

          (if as = 0 \<or> as = 1 \<or> as = 2 \<or> as = 3 then 2 

           else if as = 4 \<or> as = 5 \<or> as = 6 then 1

           else 0)"

fun addition_stage2 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow>  nat \<Rightarrow> nat"

  where

  "addition_stage2 (as, lm) m p = 

              (if 0 \<le> as \<and> as \<le> 3 then lm ! m

               else if 4 \<le> as \<and> as \<le> 6 then lm ! p

               else 0)"

fun addition_stage3 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"

  where

  "addition_stage3 (as, lm) m p = 

             (if as = 1 then 4  

              else if as = 2 then 3 

              else if as = 3 then 2

              else if as = 0 then 1 

              else if as = 5 then 2

              else if as = 6 then 1 

              else if as = 4 then 0 

              else 0)"

  where

  "addition_measure ((as, lm), m, p) =

     (addition_stage1 (as, lm) m p, 

      addition_stage2 (as, lm) m p,

      addition_stage3 (as, lm) m p)"

  where "addition_LE \<equiv> (inv_image lex_triple addition_measure)"

lemma [simp]: "wf addition_LE"

declare addition_inv.simps[simp del]

lemma addition_inv_init: 

  "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow>

                                   addition_inv (0, lm) m n p lm"

apply(simp add: addition_inv.simps Let_def)

apply(rule_tac x = "lm ! m" in exI, simp)

done

lemma [simp]: "abc_fetch 0 (addition m n p) = Some (Dec m 4)"

by(simp add: abc_fetch.simps addition.simps)

lemma [simp]: "abc_fetch (Suc 0) (addition m n p) = Some (Inc n)"

by(simp add: abc_fetch.simps addition.simps)

lemma [simp]: "abc_fetch 2 (addition m n p) = Some (Inc p)"

by(simp add: abc_fetch.simps addition.simps)

lemma [simp]: "abc_fetch 3 (addition m n p) = Some (Goto 0)"

by(simp add: abc_fetch.simps addition.simps)

lemma [simp]: "abc_fetch 4 (addition m n p) = Some (Dec p 7)"

by(simp add: abc_fetch.simps addition.simps)

lemma [simp]: "abc_fetch 5 (addition m n p) = Some (Inc m)"

by(simp add: abc_fetch.simps addition.simps)

lemma [simp]: "abc_fetch 6 (addition m n p) = Some (Goto 4)"

by(simp add: abc_fetch.simps addition.simps)

lemma [simp]:

  "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x \<le> lm ! m; 0 < x\<rbrakk>

 \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m - x, 

                    p := lm ! m - x, m := x - Suc 0] =

                 lm[m := xa, n := lm ! n + lm ! m - Suc xa,

                    p := lm ! m - Suc xa]"

apply(case_tac x, simp, simp)

apply(rule_tac x = nat in exI, simp add: list_update_swap 

                                         list_update_overwrite)

done

lemma [simp]:

  "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>

   \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m - Suc x,

                      p := lm ! m - Suc x, n := lm ! n + lm ! m - x]

                 = lm[m := xa, n := lm ! n + lm ! m - xa, 

                      p := lm ! m - Suc xa]"

apply(rule_tac x = x in exI, 

      simp add: list_update_swap list_update_overwrite)

done

lemma [simp]: 

  "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>

   \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m - x, 

                          p := lm ! m - Suc x, p := lm ! m - x]

                 = lm[m := xa, n := lm ! n + lm ! m - xa, 

                          p := lm ! m - xa]"

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

done

lemma [simp]: 

  "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = (0::nat); m < p; n < p; x < lm ! m\<rbrakk>

  \<Longrightarrow> \<exists>xa\<le>lm ! m. lm[m := x, n := lm ! n + lm ! m - x,

                                   p := lm ! m - x] = 

                  lm[m := xa, n := lm ! n + lm ! m - xa, 

                                   p := lm ! m - xa]"

apply(rule_tac x = x in exI, simp)

done

lemma [simp]: 

  "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p;

    x \<le> lm ! m; lm ! m \<noteq> x\<rbrakk>

  \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m, 

                       p := lm ! m - x, p := lm ! m - Suc x] 

               = lm[m := xa, n := lm ! n + lm ! m, 

                       p := lm ! m - Suc xa]"

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

done

lemma [simp]:

  "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>

  \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m,

                             p := lm ! m - Suc x, m := Suc x]

                = lm[m := Suc xa, n := lm ! n + lm ! m, 

                             p := lm ! m - Suc xa]"

apply(rule_tac x = x in exI, 

     simp add: list_update_swap list_update_overwrite)

done

lemma [simp]: 

  "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x < lm ! m\<rbrakk>

  \<Longrightarrow> \<exists>xa\<le>lm ! m. lm[m := Suc x, n := lm ! n + lm ! m, 

                             p := lm ! m - Suc x] 

               = lm[m := xa, n := lm ! n + lm ! m, p := lm ! m - xa]"

apply(rule_tac x = "Suc x" in exI, simp)

done

lemma abc_steps_zero: "abc_steps_l asm ap 0 = asm"

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

done

declare Let_def[simp]

lemma addition_halt_lemma: 

  "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow>

  \<forall>na. \<not> (\<lambda>(as, lm') (m, p). as = 7) 

        (abc_steps_l (0, lm) (addition m n p) na) (m, p) \<and> 

  addition_inv (abc_steps_l (0, lm) (addition m n p) na) m n p lm 

\<longrightarrow> addition_inv (abc_steps_l (0, lm) (addition m n p) 

                                 (Suc na)) m n p lm 

  \<and> ((abc_steps_l (0, lm) (addition m n p) (Suc na), m, p), 

     abc_steps_l (0, lm) (addition m n p) na, m, p) \<in> addition_LE"

apply(rule allI, rule impI, simp add: abc_step_red2)

apply(case_tac "(abc_steps_l (0, lm) (addition m n p) na)", simp)

apply(auto split:if_splits simp add: addition_inv.simps

                                 abc_steps_zero)

apply(simp_all add: addition.simps abc_steps_l.simps)

apply(auto simp add: addition_LE_def lex_triple_def lex_pair_def 

                     abc_step_l.simps addition_inv.simps 

                     abc_lm_v.simps abc_lm_s.simps nth_append

                split: if_splits)

apply(rule_tac [!] x = x in exI, simp_all add: list_update_overwrite Suc_diff_Suc)

by (metis list_update_overwrite list_update_swap nat_neq_iff)

lemma  addition_correct': 

  "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow> 

  \<exists> stp. (\<lambda> (as, lm'). as = 7 \<and> addition_inv (as, lm') m n p lm) 

                        (abc_steps_l (0, lm) (addition m n p) stp)"

apply(insert halt_lemma2[of addition_LE

  "\<lambda> ((as, lm'), m, p). addition_inv (as, lm') m n p lm"

  "\<lambda> stp. (abc_steps_l (0, lm) (addition m n p) stp, m, p)"

  "\<lambda> ((as, lm'), m, p). as = 7"], 

  simp add: abc_steps_zero addition_inv_init)

apply(drule_tac addition_halt_lemma, simp, simp, simp,

      simp, erule_tac exE)

apply(rule_tac x = na in exI, 

      case_tac "(abc_steps_l (0, lm) (addition m n p) na)", auto)

done

lemma length_addition[simp]: "length (addition a b c) = 7"

by(auto simp: addition.simps)

lemma addition_correct:

  "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk>

   \<Longrightarrow> {\<lambda> a. a = lm} (addition m n p) {\<lambda> nl. addition_inv (7, nl) m n p lm}"

using assms

proof(rule_tac abc_Hoare_haltI, simp)

  fix lma

  assume "m \<noteq> n" "m < p \<and> n < p" "p < length lm" "lm ! p = 0"

  then have "\<exists> stp. (\<lambda> (as, lm'). as = 7 \<and> addition_inv (as, lm') m n p lm) 

                        (abc_steps_l (0, lm) (addition m n p) stp)"

    by(rule_tac addition_correct', auto simp: addition_inv.simps)

  thus "\<exists>na. abc_final (abc_steps_l (0, lm) (addition m n p) na) (addition m n p) \<and>

                  (\<lambda>nl. addition_inv (7, nl) m n p lm) abc_holds_for abc_steps_l (0, lm) (addition m n p) na"

    apply(erule_tac exE)

    apply(rule_tac x = stp in exI)

    apply(auto)

    done

qed

lemma compile_s_correct':

proof(rule_tac abc_Hoare_plus_halt)

    by(rule_tac addition_correct, auto simp: numeral_2_eq_2)

next

    by(rule_tac abc_Hoare_haltI, rule_tac x = 1 in exI, auto simp: addition_inv.simps 

      abc_steps_l.simps abc_step_l.simps abc_fetch.simps numeral_2_eq_2 abc_lm_s.simps abc_lm_v.simps)

qed

lemma abc_comp_commute: "(A [+] B) [+] C = A [+] (B [+] C)"

apply(auto simp: abc_comp.simps abc_shift.simps)

apply(case_tac x, auto)

done

lemma compile_z_correct: 

  {\<lambda>nl. nl = n # 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = n # r # 0 \<up> (fp - Suc arity) @ anything}"

apply(rule_tac abc_Hoare_haltI)

apply(rule_tac x = 1 in exI)

apply(auto simp: abc_steps_l.simps rec_ci.simps rec_ci_z_def 

done

lemma compile_s_correct: 

  {\<lambda>nl. nl = n # 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = n # r # 0 \<up> (fp - Suc arity) @ anything}"

done

lemma compile_id_correct':

  assumes "n < length args" 

  shows "{\<lambda>nl. nl = args @ 0 \<up> 2 @ anything} addition n (length args) (Suc (length args))

proof -

  have "{\<lambda>nl. nl = args @ 0 \<up> 2 @ anything} addition n (length args) (Suc (length args))

  {\<lambda>nl. addition_inv (7, nl) n (length args) (Suc (length args)) (args @ 0 \<up> 2 @ anything)}"

    using assms

    by(rule_tac addition_correct, auto simp: numeral_2_eq_2 nth_append)

  thus "?thesis"

    using assms

      nth_append numeral_2_eq_2 list_update_append)

qed

lemma compile_id_correct: 

       \<Longrightarrow> {\<lambda>nl. nl = xs @ 0 \<up> (fp - arity) @ anything} ap {\<lambda>nl. nl = xs @ r # 0 \<up> (fp - Suc arity) @ anything}"

apply(auto simp: rec_ci.simps rec_ci_id.simps compile_id_correct')

done

lemma cn_merge_gs_tl_app: 

  "cn_merge_gs (gs @ [g]) pstr = 

        cn_merge_gs gs pstr [+] cn_merge_gs [g] (pstr + length gs)"

apply(induct gs arbitrary: pstr, simp add: cn_merge_gs.simps, auto)

apply(simp add: abc_comp_commute)

done

lemma footprint_ge: 

  "rec_ci a = (p, arity, fp) \<Longrightarrow> arity < fp"

apply(induct a)

apply(auto simp: rec_ci.simps)

apply(case_tac "rec_ci a", simp)

apply(case_tac "rec_ci a1", case_tac "rec_ci a2", auto)

apply(case_tac "rec_ci a", auto)

done

lemma param_pattern: 

apply(auto simp: rec_ci.simps)

apply(case_tac "rec_ci f", simp)

apply(case_tac "rec_ci f", case_tac "rec_ci g", simp)

apply(case_tac "rec_ci f", case_tac "rec_ci gs", simp)

done

lemma replicate_merge_anywhere: 

  "x\<up>a @ x\<up>b @ ys = x\<up>(a+b) @ ys"

by(simp add:replicate_add)

fun mv_box_inv :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"

  where

  "mv_box_inv (as, lm) m n initlm = 

         (let plus = initlm ! m + initlm ! n in

           length initlm > max m n \<and> m \<noteq> n \<and> 

              (if as = 0 then \<exists> k l. lm = initlm[m := k, n := l] \<and> 

                    k + l = plus \<and> k \<le> initlm ! m 

              else if as = 1 then \<exists> k l. lm = initlm[m := k, n := l]

                             \<and> k + l + 1 = plus \<and> k < initlm ! m 

              else if as = 2 then \<exists> k l. lm = initlm[m := k, n := l] 

                              \<and> k + l = plus \<and> k \<le> initlm ! m

              else if as = 3 then lm = initlm[m := 0, n := plus]

              else False))"

fun mv_box_stage1 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat"

  where

  "mv_box_stage1 (as, lm) m  = 

            (if as = 3 then 0 

             else 1)"

fun mv_box_stage2 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat"

  where

  "mv_box_stage2 (as, lm) m = (lm ! m)"

fun mv_box_stage3 :: "nat \<times> nat list \<Rightarrow> nat \<Rightarrow> nat"

  where

  "mv_box_stage3 (as, lm) m = (if as = 1 then 3 

                                else if as = 2 then 2

                                else if as = 0 then 1 

                                else 0)"

fun mv_box_measure :: "((nat \<times> nat list) \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat)"

  where

  "mv_box_measure ((as, lm), m) = 

     (mv_box_stage1 (as, lm) m, mv_box_stage2 (as, lm) m,

      mv_box_stage3 (as, lm) m)"

definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"

  where

  "lex_pair = less_than <*lex*> less_than"

definition lex_triple :: 

 "((nat \<times> (nat \<times> nat)) \<times> (nat \<times> (nat \<times> nat))) set"

  where

  "lex_triple \<equiv> less_than <*lex*> lex_pair"

definition mv_box_LE :: 

 "(((nat \<times> nat list) \<times> nat) \<times> ((nat \<times> nat list) \<times> nat)) set"

  where 

  "mv_box_LE \<equiv> (inv_image lex_triple mv_box_measure)"

lemma wf_lex_triple: "wf lex_triple"

  by (auto intro:wf_lex_prod simp:lex_triple_def lex_pair_def)

lemma wf_mv_box_le[intro]: "wf mv_box_LE"

by(auto intro:wf_inv_image wf_lex_triple simp: mv_box_LE_def)

declare mv_box_inv.simps[simp del]

lemma mv_box_inv_init:  

"\<lbrakk>m < length initlm; n < length initlm; m \<noteq> n\<rbrakk> \<Longrightarrow> 

  mv_box_inv (0, initlm) m n initlm"

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

apply(rule_tac x = "initlm ! m" in exI, 

      rule_tac x = "initlm ! n" in exI, simp)

done

lemma [simp]: "abc_fetch 0 (mv_box m n) = Some (Dec m 3)"

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

done

lemma [simp]: "abc_fetch (Suc 0) (mv_box m n) =

               Some (Inc n)"

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

done

lemma [simp]: "abc_fetch 2 (mv_box m n) = Some (Goto 0)"

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

done

lemma [simp]: "abc_fetch 3 (mv_box m n) = None"

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

done

lemma replicate_Suc_iff_anywhere: "x # x\<up>b @ ys = x\<up>(Suc b) @ ys"

by simp

lemma [simp]: 

  "\<lbrakk>m \<noteq> n; m < length initlm; n < length initlm;

    k + l = initlm ! m + initlm ! n; k \<le> initlm ! m; 0 < k\<rbrakk>

 \<Longrightarrow> \<exists>ka la. initlm[m := k, n := l, m := k - Suc 0] = 

     initlm[m := ka, n := la] \<and>