1 theory recursive

     2 imports Main rec_def abacus

     3 begin

     4 

     5 section {* 

     6   Compiling from recursive functions to Abacus machines

     7   *}

     8 

     9 text {*

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

    11 *}

    12 

    13 text {*

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

    15 *}

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

    17   where

    18   "get_paras_num z = 1" |

    19   "get_paras_num s = 1" |

    20   "get_paras_num (id m n) = m" |

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

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

    23   "get_paras_num (Mn n f) = n"  

    24 

    25 fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"

    26   where

    27   "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, 

    28                        Inc m, Goto 4]"

    29 

    30 fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"

    31   where

    32   "mv_box m n = [Dec m 3, Inc n, Goto 0]"

    33 

    34 fun abc_inst_shift :: "abc_inst \<Rightarrow> nat \<Rightarrow> abc_inst"

    35   where

    36   "abc_inst_shift (Inc m) n = Inc m" |

    37   "abc_inst_shift (Dec m e) n = Dec m (e + n)" |

    38   "abc_inst_shift (Goto m) n = Goto (m + n)"

    39 

    40 fun abc_shift :: "abc_inst list \<Rightarrow> nat \<Rightarrow> abc_inst list" 

    41   where

    42   "abc_shift xs n = map (\<lambda> x. abc_inst_shift x n) xs" 

    43 

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

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

    46   where

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

    48                            al @ abc_shift bl al_len)"

    49 

    50 text {*

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

    52 *}

    53 definition rec_ci_z :: "abc_inst list"

    54   where

    55   "rec_ci_z \<equiv> [Goto 1]"

    56 

    57 text {*

    58   The compilation of @{text "s"}-operator.

    59 *}

    60 definition rec_ci_s :: "abc_inst list"

    61   where

    62   "rec_ci_s \<equiv> (addition 0 1 2 [+] [Inc 1])"

    63 

    64 

    65 text {*

    66   The compilation of @{text "id i j"}-operator

    67 *}

    68 

    69 fun rec_ci_id :: "nat \<Rightarrow> nat \<Rightarrow> abc_inst list"

    70   where

    71   "rec_ci_id i j = addition j i (i + 1)"

    72 

    73 fun mv_boxes :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list"

    74   where

    75   "mv_boxes ab bb 0 = []" |

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

    77   (bb + n)"

    78 

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

    80   where

    81   "empty_boxes 0 = []" |

    82   "empty_boxes (Suc n) = empty_boxes n [+] [Dec n 2, Goto 0]"

    83 

    84 fun cn_merge_gs ::

    85   "(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list"

    86   where

    87   "cn_merge_gs [] p = []" |

    88   "cn_merge_gs (g # gs) p = 

    89       (let (gprog, gpara, gn) = g in 

    90          gprog [+] mv_box gpara p [+] cn_merge_gs gs (Suc p))"

    91 

    92 

    93 text {*

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

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

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

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

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

    99 *}

   100 

   101 function rec_ci :: "recf \<Rightarrow> abc_inst list \<times> nat \<times> nat"

   102   where

   103   "rec_ci z = (rec_ci_z, 1, 2)" |

   104   "rec_ci s = (rec_ci_s, 1, 3)" |

   105   "rec_ci (id m n) = (rec_ci_id m n, m, m + 2)" |

   106   "rec_ci (Cn n f gs) = 

   107       (let cied_gs = map (\<lambda> g. rec_ci g) (f # gs) in

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

   109        let pstr = 

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

   111        let qstr = pstr + Suc (length gs) in 

   112        (cn_merge_gs (tl cied_gs) pstr [+] mv_boxes 0 qstr n [+] 

   113           mv_boxes pstr 0 (length gs) [+] fprog [+] 

   114             mv_box fpara pstr [+] empty_boxes (length gs) [+] 

   115              mv_box pstr n [+] mv_boxes qstr 0 n, n,  qstr + n))" |

   116   "rec_ci (Pr n f g) = 

   117          (let (fprog, fpara, fn) = rec_ci f in 

   118           let (gprog, gpara, gn) = rec_ci g in 

   119           let p = Max (set ([n + 3, fn, gn])) in 

   120           let e = length gprog + 7 in 

   121            (mv_box n p [+] fprog [+] mv_box n (Suc n) [+] 

   122                (([Dec p e] [+] gprog [+] 

   123                  [Inc n, Dec (Suc n) 3, Goto 1]) @

   124                      [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gprog + 4)]),

   125              Suc n, p + 1))" |

   126   "rec_ci (Mn n f) =

   127          (let (fprog, fpara, fn) = rec_ci f in 

   128           let len = length (fprog) in 

   129             (fprog @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),

   130              Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn) )"

   131   by pat_completeness auto

   132 termination 

   133 proof

   134 term size

   135   show "wf (measure size)" by auto

   136 next

   137   fix n f gs x

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

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

   140     by(induct gs, auto)

   141 next

   142   fix n f g

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

   144 next

   145   fix n f g x xa y xb ya

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

   147 next

   148   fix n f

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

   150 qed

   151 

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

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

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

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

   156   

   157 thm rec_calc_rel.induct

   158 

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

   160         abc_step_l.simps[simp del] 

   161 

   162 lemma abc_steps_add: 

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

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

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

   166 proof -

   167   fix m n as lm

   168   assume ind: 

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

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

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

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

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

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

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

   176     apply(simp add: abc_steps_l.simps)

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

   178           simp add: abc_steps_l.simps)

   179     done

   180 qed

   181 

   182 (*lemmas: rec_ci and rec_calc_rel*)

   183 

   184 lemma rec_calc_inj_case_z: 

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

   186 apply(auto elim: calc_z_reverse)

   187 done

   188 

   189 lemma  rec_calc_inj_case_s: 

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

   191 apply(auto elim: calc_s_reverse)

   192 done

   193 

   194 lemma rec_calc_inj_case_id:

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

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

   197 apply(auto elim: calc_id_reverse)

   198 done

   199 

   200 lemma rec_calc_inj_case_mn:

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

   202            \<Longrightarrow> x = y" 

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

   204   shows "x = y"

   205   apply(insert h)

   206   apply(elim  calc_mn_reverse)

   207   apply(case_tac "x > y", simp)

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

   209 proof -

   210   fix v va

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

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

   213     "0 < v"

   214   thus "False"

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

   216     done

   217 next

   218   fix v va

   219   assume 

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

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

   222   thus "x = y"

   223     apply(erule_tac x = "x" in allE)

   224     apply(case_tac "x = y", auto)

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

   226     done

   227 qed 

   228 

   229 lemma rec_calc_inj_case_pr: 

   230   assumes f_ind: 

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

   232   and g_ind:

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

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

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

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

   237   shows "x = y"

   238   apply(case_tac "rec_ci f")

   239 proof -

   240   fix a b c

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

   242   hence ng_ind: 

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

   244     \<Longrightarrow> xc = yb"

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

   246     done

   247   from h show "x = y"

   248     apply(erule_tac calc_pr_reverse, erule_tac calc_pr_reverse)

   249     apply(erule f_ind, simp, simp)

   250     apply(erule_tac calc_pr_reverse, simp, simp)

   251   proof -

   252     fix la ya ry laa yaa rya

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

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

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

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

   257     from k2 have "ry = rya"

   258       apply(induct ya arbitrary: ry rya)

   259       apply(erule_tac calc_pr_reverse, 

   260         erule_tac calc_pr_reverse, simp)

   261       apply(erule f_ind, simp, simp, simp)

   262       apply(erule_tac calc_pr_reverse, simp)

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

   264     proof -

   265       fix ya ry rya l y ryb laa yb ryc

   266       assume ind:

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

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

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

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

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

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

   273       from j show "ry = rya"

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

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

   276 	done

   277     qed 

   278     from k1 and this show "x = y"

   279       apply(simp)

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

   281       done

   282   qed  

   283 qed

   284 

   285 lemma Suc_nth_part_eq:

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

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

   288 apply(rule allI, rule impI)

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

   290 done

   291 

   292 

   293 lemma list_eq_intro:  

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

   295   \<Longrightarrow> xs = ys"

   296 apply(induct xs arbitrary: ys, simp)

   297 apply(case_tac ys, simp, simp)

   298 proof -

   299   fix a xs ys aa list

   300   assume ind: 

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

   302     \<Longrightarrow> xs = ys"

   303     and h: "length xs = length list" 

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

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

   306     apply(insert ind[of list], simp)

   307     apply(frule Suc_nth_part_eq, simp)

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

   309     done

   310 qed

   311 

   312 lemma rec_calc_inj_case_cn: 

   313   assumes ind: 

   314   "\<And>x l xa y.

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

   316   \<Longrightarrow> xa = y"

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

   318          "rec_calc_rel (Cn n f gs) l y"

   319   shows "x = y"

   320   apply(insert h, elim  calc_cn_reverse)

   321   apply(subgoal_tac "rs = rsa")

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

   323         simp, simp, simp)

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

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

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

   327   done

   328 

   329 lemma rec_calc_inj:

   330   "\<lbrakk>rec_calc_rel f l x; 

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

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

   333 apply(simp add: rec_calc_inj_case_z)

   334 apply(simp add: rec_calc_inj_case_s)

   335 apply(simp add: rec_calc_inj_case_id, simp)

   336 apply(erule rec_calc_inj_case_cn,simp, simp)

   337 apply(erule rec_calc_inj_case_pr, auto)

   338 apply(erule rec_calc_inj_case_mn, auto)

   339 done

   340 

   341 

   342 lemma calc_rel_reverse_ind_step_ex: 

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

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

   345 apply(erule calc_pr_reverse, simp, simp)

   346 apply(rule_tac x = rk in exI, simp)

   347 done

   348 

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

   350 by arith

   351 

   352 lemma calc_pr_para_not_null: 

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

   354 apply(erule calc_pr_reverse, simp, simp)

   355 done

   356 

   357 lemma calc_pr_less_ex: 

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

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

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

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

   362 apply(rule_tac rs = xa in calc_rel_reverse_ind_step_ex, simp)

   363 apply(simp add: calc_pr_para_not_null)

   364 done

   365 

   366 lemma calc_pr_zero_ex:

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

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

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

   370       erule_tac exE, simp)

   371 apply(erule_tac calc_pr_reverse, simp)

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

   373 done

   374 

   375 

   376 lemma abc_steps_ind: 

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

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

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

   380 done

   381 

   382 lemma abc_steps_zero: "abc_steps_l asm ap 0 = asm"

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

   384 done

   385 

   386 lemma abc_append_nth: 

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

   388        (ap [+] bp) ! n =

   389          (if n < length ap then ap ! n 

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

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

   392 done

   393 

   394 lemma abc_state_keep:  

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

   396 apply(induct stp, simp add: abc_steps_zero)

   397 apply(simp add: abc_steps_ind)

   398 apply(simp add: abc_steps_zero)

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

   400 done

   401 

   402 lemma abc_halt_equal: 

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

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

   405 apply(case_tac "stpa - stpb > 0")

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

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

   408       simp, simp add: abc_steps_zero)

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

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

   411       simp)

   412 done  

   413 

   414 lemma abc_halt_point_ex: 

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

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

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

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

   419       (abc_steps_l (0, lm) bp stp) "

   420 apply(erule_tac exE)

   421 proof -

   422   fix stp

   423   assume "bs = length bp" 

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

   425          "bp \<noteq> []"

   426   thus 

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

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

   429                        (abc_steps_l (0, lm) bp stp)"

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

   431   proof -

   432     fix stpa

   433     assume ind: 

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

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

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

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

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

   439            "bp \<noteq> []"

   440     from h show 

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

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

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

   444             case_tac "a = length bp")

   445       apply(insert ind, simp)

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

   447       apply(rule_tac abc_halt_equal, simp, simp)

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

   449       apply(simp add: abc_steps_zero)

   450       apply(rule classical, simp add: abc_steps_l.simps 

   451                              abc_fetch.simps abc_step_l.simps)

   452       done

   453   qed

   454 qed  

   455 

   456 

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

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

   459 apply(induct ab, simp, simp)

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

   461 done

   462 

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

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

   465 done

   466 

   467 

   468 lemma abc_append_length[simp]:  

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

   470 apply(simp add: abc_append.simps)

   471 done

   472 

   473 declare Let_def[simp]

   474 

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

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

   477 apply(induct cs, simp, simp)

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

   479 done

   480 

   481 lemma abc_halt_point_step[simp]: 

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

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

   484                                         (length ap + length bp, lm')"

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

   486 apply(case_tac "bp ! a", 

   487                       auto simp: abc_steps_l.simps abc_step_l.simps)

   488 done

   489 

   490 lemma abc_step_state_in:

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

   492   \<Longrightarrow> a < length bp"

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

   494 apply(rule_tac classical, 

   495       simp add: abc_step_l.simps abc_steps_l.simps)

   496 done

   497 

   498 

   499 lemma abc_append_state_in_exc: 

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

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

   502                                              (length ap + bs, l)"

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

   504 proof -

   505   fix stpa bs l

   506   assume ind: 

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

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

   509                                                 (length ap + bs, l)"

   510     and h: "bs < length bp" 

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

   512   from h show 

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

   514                                                 (length ap + bs, l)"

   515     apply(simp add: abc_steps_ind)

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

   517   proof -

   518     fix a b

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

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

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

   522       apply(simp add: abc_step_state_in)

   523       done

   524     from h and g and k1 show 

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

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

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

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

   529                       abc_append_nth)

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

   531                                  abc_steps_l.simps abc_step_l.simps)

   532       done

   533   qed

   534 qed

   535 

   536 lemma [simp]: "abc_steps_l (0, am) [] stp = (0, am)"

   537 apply(induct stp, simp add: abc_steps_zero)

   538 apply(simp add: abc_steps_ind)

   539 apply(simp add: abc_steps_zero abc_steps_l.simps 

   540                 abc_fetch.simps abc_step_l.simps)

   541 done

   542 

   543 lemma abc_append_exc1:

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

   545     bs = length bp; 

   546     as = length ap\<rbrakk>

   547     \<Longrightarrow> \<exists> stp. abc_steps_l (as, lm) (ap [+] bp [+] cp) stp 

   548                                                  = (as + bs, lm')"

   549 apply(case_tac "bp = []", erule_tac exE, simp,

   550       rule_tac x = 0 in exI, simp add: abc_steps_zero)

   551 apply(frule_tac abc_halt_point_ex, simp, simp,

   552       erule_tac exE, erule_tac exE) 

   553 apply(rule_tac x = "stpa + Suc 0" in exI)

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

   555       simp add: abc_steps_ind)

   556 apply(subgoal_tac 

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

   558                                    = (length ap + a, b)", simp)

   559 apply(simp add: abc_steps_zero)

   560 apply(rule_tac abc_append_state_in_exc, simp, simp)

   561 done

   562 

   563 lemma abc_append_exc3: 

   564   "\<lbrakk>\<exists> stp. abc_steps_l (0, am) bp stp = (bs, bm); ss = length ap\<rbrakk>

   565    \<Longrightarrow>  \<exists> stp. abc_steps_l (ss, am) (ap [+] bp) stp = (bs + ss, bm)"

   566 apply(erule_tac exE)

   567 proof -

   568   fix stp

   569   assume h: "abc_steps_l (0, am) bp stp = (bs, bm)" "ss = length ap"

   570   thus " \<exists>stp. abc_steps_l (ss, am) (ap [+] bp) stp = (bs + ss, bm)"

   571   proof(induct stp arbitrary: bs bm)

   572     fix bs bm

   573     assume "abc_steps_l (0, am) bp 0 = (bs, bm)"

   574     thus "\<exists>stp. abc_steps_l (ss, am) (ap [+] bp) stp = (bs + ss, bm)"

   575       apply(rule_tac x = 0 in exI, simp add: abc_steps_l.simps)

   576       done

   577   next

   578     fix stp bs bm

   579     assume ind: 

   580       "\<And>bs bm. \<lbrakk>abc_steps_l (0, am) bp stp = (bs, bm);

   581                  ss = length ap\<rbrakk> \<Longrightarrow> 

   582           \<exists>stp. abc_steps_l (ss, am) (ap [+] bp) stp = (bs + ss, bm)"

   583     and g: "abc_steps_l (0, am) bp (Suc stp) = (bs, bm)"

   584     from g show 

   585       "\<exists>stp. abc_steps_l (ss, am) (ap [+] bp) stp = (bs + ss, bm)"

   586       apply(insert abc_steps_add[of 0 am bp stp "Suc 0"], simp)

   587       apply(case_tac "(abc_steps_l (0, am) bp stp)", simp)

   588     proof -

   589       fix a b

   590       assume "(bs, bm) = abc_steps_l (a, b) bp (Suc 0)" 

   591              "abc_steps_l (0, am) bp (Suc stp) = 

   592                        abc_steps_l (a, b) bp (Suc 0)" 

   593               "abc_steps_l (0, am) bp stp = (a, b)"

   594       thus "?thesis"

   595 	apply(insert ind[of a b], simp add: h, erule_tac exE)

   596 	apply(rule_tac x = "Suc stp" in exI)

   597 	apply(simp only: abc_steps_ind, simp add: abc_steps_zero)

   598       proof -

   599 	fix stp

   600 	assume "(bs, bm) = abc_steps_l (a, b) bp (Suc 0)"

   601 	thus "abc_steps_l (a + length ap, b) (ap [+] bp) (Suc 0)

   602                                               = (bs + length ap, bm)"

   603 	  apply(simp add: abc_steps_l.simps abc_steps_zero

   604                           abc_fetch.simps split: if_splits)

   605 	  apply(case_tac "bp ! a", 

   606                 simp_all add: abc_inst_shift.simps abc_append_nth

   607                    abc_steps_l.simps abc_steps_zero abc_step_l.simps)

   608 	  apply(auto)

   609 	  done

   610       qed

   611     qed

   612   qed

   613 qed

   614 

   615 lemma abc_add_equal:

   616   "\<lbrakk>ap \<noteq> []; 

   617     abc_steps_l (0, am) ap astp = (a, b);

   618     a < length ap\<rbrakk>

   619      \<Longrightarrow> (abc_steps_l (0, am) (ap @ bp) astp) = (a, b)"

   620 apply(induct astp arbitrary: a b, simp add: abc_steps_l.simps, simp)

   621 apply(simp add: abc_steps_ind)

   622 apply(case_tac "(abc_steps_l (0, am) ap astp)")

   623 proof -

   624   fix astp a b aa ba

   625   assume ind: 

   626     "\<And>a b. \<lbrakk>abc_steps_l (0, am) ap astp = (a, b); 

   627              a < length ap\<rbrakk> \<Longrightarrow> 

   628                   abc_steps_l (0, am) (ap @ bp) astp = (a, b)"

   629   and h: "abc_steps_l (abc_steps_l (0, am) ap astp) ap (Suc 0)

   630                                                             = (a, b)"

   631         "a < length ap" 

   632         "abc_steps_l (0, am) ap astp = (aa, ba)"

   633   from h show "abc_steps_l (abc_steps_l (0, am) (ap @ bp) astp)

   634                                         (ap @ bp) (Suc 0) = (a, b)"

   635     apply(insert ind[of aa ba], simp)

   636     apply(subgoal_tac "aa < length ap", simp)

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

   638                      nth_append abc_steps_zero)

   639     apply(rule abc_step_state_in, auto)

   640     done

   641 qed

   642 

   643 

   644 lemma abc_add_exc1: 

   645   "\<lbrakk>\<exists> astp. abc_steps_l (0, am) ap astp = (as, bm); as = length ap\<rbrakk>

   646   \<Longrightarrow> \<exists> stp. abc_steps_l (0, am) (ap @ bp) stp = (as, bm)"

   647 apply(case_tac "ap = []", simp, 

   648       rule_tac x = 0 in exI, simp add: abc_steps_zero)

   649 apply(drule_tac abc_halt_point_ex, simp, simp)

   650 apply(erule_tac exE, case_tac "(abc_steps_l (0, am) ap astp)", simp)

   651 apply(rule_tac x = "Suc astp" in exI, simp add: abc_steps_ind, auto)

   652 apply(frule_tac bp = bp in abc_add_equal, simp, simp, simp)

   653 apply(simp add: abc_steps_l.simps abc_steps_zero 

   654                 abc_fetch.simps nth_append)

   655 done

   656 

   657 declare abc_shift.simps[simp del] 

   658 

   659 lemma abc_append_exc2: 

   660   "\<lbrakk>\<exists> astp. abc_steps_l (0, am) ap astp = (as, bm); as = length ap; 

   661     \<exists> bstp. abc_steps_l (0, bm) bp bstp = (bs, bm'); bs = length bp;

   662     cs = as + bs; bp \<noteq> []\<rbrakk>

   663   \<Longrightarrow> \<exists> stp. abc_steps_l (0, am) (ap [+] bp) stp = (cs, bm')"

   664 apply(insert abc_append_exc1[of bm bp bs bm' as ap "[]"], simp)

   665 apply(drule_tac bp = "abc_shift bp (length ap)" in abc_add_exc1, simp)

   666 apply(subgoal_tac "ap @ abc_shift bp (length ap) = ap [+] bp", 

   667       simp, auto)

   668 apply(rule_tac x = "stpa + stp" in exI, simp add: abc_steps_add)

   669 apply(simp add: abc_append.simps)

   670 done

   671 lemma exponent_add_iff: "a\<up>b @ a\<up>c@ xs = a\<up>(b+c) @ xs"

   672 apply(auto simp: replicate_add)

   673 done

   674 

   675 lemma exponent_cons_iff: "a # a\<up>c @ xs = a\<up>(Suc c) @ xs"

   676 apply(auto simp: replicate_add)

   677 done

   678 

   679 lemma  [simp]: "length lm = n \<Longrightarrow>  

   680   abc_steps_l (Suc 0, lm @ Suc x # 0 # suf_lm) 

   681        [Inc n, Dec (Suc n) 3, Goto (Suc 0)] (Suc (Suc 0))

   682                                   = (3, lm @ Suc x # 0 # suf_lm)"

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

   684                 abc_step_l.simps abc_lm_v.simps abc_lm_s.simps 

   685                 nth_append list_update_append)

   686 done

   687 

   688 lemma [simp]: 

   689   "length lm = n \<Longrightarrow> 

   690   abc_steps_l (Suc 0, lm @ Suc x # Suc y # suf_lm) 

   691      [Inc n, Dec (Suc n) 3, Goto (Suc 0)] (Suc (Suc 0))

   692   = (Suc 0, lm @ Suc x # y # suf_lm)"

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

   694                 abc_step_l.simps abc_lm_v.simps abc_lm_s.simps 

   695                 nth_append list_update_append)

   696 done

   697 

   698 lemma pr_cycle_part_middle_inv: 

   699   "\<lbrakk>length lm = n\<rbrakk> \<Longrightarrow> 

   700   \<exists> stp. abc_steps_l (0, lm @ x # y # suf_lm) 

   701                          [Inc n, Dec (Suc n) 3, Goto (Suc 0)] stp 

   702   = (3, lm @ Suc x # 0 # suf_lm)"

   703 proof -

   704   assume h: "length lm = n"

   705   hence k1: "\<exists> stp. abc_steps_l (0, lm @ x # y # suf_lm) 

   706                            [Inc n, Dec (Suc n) 3, Goto (Suc 0)] stp 

   707     = (Suc 0, lm @ Suc x # y # suf_lm)"

   708     apply(rule_tac x = "Suc 0" in exI)

   709     apply(simp add: abc_steps_l.simps abc_step_l.simps 

   710                     abc_lm_v.simps abc_lm_s.simps nth_append 

   711                     list_update_append abc_fetch.simps)

   712     done

   713   from h have k2: 

   714     "\<exists> stp. abc_steps_l (Suc 0, lm @ Suc x # y # suf_lm)

   715                       [Inc n, Dec (Suc n) 3, Goto (Suc 0)] stp 

   716     = (3, lm @ Suc x # 0 # suf_lm)"

   717     apply(induct y)

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

   719           erule_tac exE)

   720     apply(rule_tac x = "Suc (Suc 0) + stp" in exI, 

   721           simp only: abc_steps_add, simp)

   722     done      

   723   from k1 and k2 show 

   724     "\<exists> stp. abc_steps_l (0, lm @ x # y # suf_lm) 

   725                        [Inc n, Dec (Suc n) 3, Goto (Suc 0)] stp 

   726     = (3, lm @ Suc x # 0 # suf_lm)"

   727     apply(erule_tac exE, erule_tac exE)

   728     apply(rule_tac x = "stp + stpa" in exI, simp add: abc_steps_add)

   729     done

   730 qed

   731 

   732 lemma [simp]: 

   733   "length lm = Suc n \<Longrightarrow> 

   734   (abc_steps_l (length ap, lm @ x # Suc y # suf_lm) 

   735            (ap @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length ap)]) 

   736                     (Suc (Suc (Suc 0))))

   737   = (length ap, lm @ Suc x # y # suf_lm)"

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

   739          abc_lm_v.simps list_update_append nth_append abc_lm_s.simps)

   740 done

   741 

   742 lemma switch_para_inv:

   743   assumes bp_def:"bp =  ap @ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto ss]"

   744   and h: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)" 

   745          "ss = length ap" 

   746          "length lm = Suc n"

   747   shows " \<exists>stp. abc_steps_l (ss, lm @ x # y # suf_lm) bp stp =

   748                                (0, lm @ (x + y) # 0 # suf_lm)"

   749 apply(induct y arbitrary: x)

   750 apply(rule_tac x = "Suc 0" in exI,

   751   simp add: bp_def mv_box.simps abc_steps_l.simps 

   752             abc_fetch.simps h abc_step_l.simps 

   753             abc_lm_v.simps list_update_append nth_append

   754             abc_lm_s.simps)

   755 proof -

   756   fix y x

   757   assume ind: 

   758     "\<And>x. \<exists>stp. abc_steps_l (ss, lm @ x # y # suf_lm) bp stp = 

   759                                      (0, lm @ (x + y) # 0 # suf_lm)"

   760   show "\<exists>stp. abc_steps_l (ss, lm @ x # Suc y # suf_lm) bp stp = 

   761                                   (0, lm @ (x + Suc y) # 0 # suf_lm)"

   762     apply(insert ind[of "Suc x"], erule_tac exE)

   763     apply(rule_tac x = "Suc (Suc (Suc 0)) + stp" in exI, 

   764           simp only: abc_steps_add bp_def h)

   765     apply(simp add: h)

   766     done

   767 qed

   768 

   769 lemma [simp]:

   770   "length lm = rs_pos \<and> Suc (Suc rs_pos) < a_md \<and> 0 < rs_pos \<Longrightarrow> 

   771       a_md - Suc 0 < Suc (Suc (Suc (a_md + length suf_lm - 

   772                                          Suc (Suc (Suc 0)))))"

   773 apply(arith)

   774 done

   775 

   776 lemma [simp]: 

   777   "Suc (Suc rs_pos) < a_md \<and> 0 < rs_pos \<Longrightarrow> 

   778                            \<not> a_md - Suc 0 < rs_pos - Suc 0"

   779 apply(arith)

   780 done

   781 

   782 lemma [simp]: 

   783   "Suc (Suc rs_pos) < a_md \<and> 0 < rs_pos \<Longrightarrow> 

   784            \<not> a_md - rs_pos < Suc (Suc (a_md - Suc (Suc rs_pos)))"

   785 apply(arith)

   786 done

   787 

   788 lemma butlast_append_last: "lm \<noteq> [] \<Longrightarrow> lm = butlast lm @ [last lm]"

   789 apply(auto)

   790 done

   791 

   792 lemma [simp]: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)

   793            \<Longrightarrow> (Suc (Suc rs_pos)) < a_md"

   794 apply(simp add: rec_ci.simps)

   795 apply(case_tac "rec_ci f", simp)

   796 apply(case_tac "rec_ci g", simp)

   797 apply(arith)

   798 done

   799 

   800 (*

   801 lemma pr_para_ge_suc0: "rec_calc_rel (Pr n f g) lm xs \<Longrightarrow> 0 < n"

   802 apply(erule calc_pr_reverse, simp, simp)

   803 done

   804 *)

   805 

   806 lemma ci_pr_para_eq: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)

   807                   \<Longrightarrow> rs_pos = Suc n"

   808 apply(simp add: rec_ci.simps)

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

   810 done

   811 

   812 lemma [intro]:  

   813   "\<lbrakk>rec_ci z = (aprog, rs_pos, a_md); rec_calc_rel z lm xs\<rbrakk>

   814   \<Longrightarrow> length lm = rs_pos"

   815 apply(simp add: rec_ci.simps rec_ci_z_def)

   816 apply(erule_tac calc_z_reverse, simp)

   817 done

   818 

   819 lemma [intro]: 

   820   "\<lbrakk>rec_ci s = (aprog, rs_pos, a_md); rec_calc_rel s lm xs\<rbrakk>

   821   \<Longrightarrow> length lm = rs_pos"

   822 apply(simp add: rec_ci.simps rec_ci_s_def)

   823 apply(erule_tac calc_s_reverse, simp)

   824 done

   825 

   826 lemma [intro]: 

   827   "\<lbrakk>rec_ci (recf.id nat1 nat2) = (aprog, rs_pos, a_md); 

   828     rec_calc_rel (recf.id nat1 nat2) lm xs\<rbrakk> \<Longrightarrow> length lm = rs_pos"

   829 apply(simp add: rec_ci.simps rec_ci_id.simps)

   830 apply(erule_tac calc_id_reverse, simp)

   831 done

   832 

   833 lemma [intro]: 

   834   "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); 

   835     rec_calc_rel (Cn n f gs) lm xs\<rbrakk> \<Longrightarrow> length lm = rs_pos"

   836 apply(erule_tac calc_cn_reverse, simp)

   837 apply(simp add: rec_ci.simps)

   838 apply(case_tac "rec_ci f",  simp)

   839 done

   840 

   841 lemma [intro]:

   842   "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); 

   843     rec_calc_rel (Pr n f g) lm xs\<rbrakk> \<Longrightarrow> length lm = rs_pos"

   844 apply(erule_tac  calc_pr_reverse, simp)

   845 apply(drule_tac ci_pr_para_eq, simp, simp)

   846 apply(drule_tac ci_pr_para_eq, simp)

   847 done

   848 

   849 lemma [intro]: 

   850   "\<lbrakk>rec_ci (Mn n f) = (aprog, rs_pos, a_md);

   851     rec_calc_rel (Mn n f) lm xs\<rbrakk> \<Longrightarrow> length lm = rs_pos"

   852 apply(erule_tac calc_mn_reverse)

   853 apply(simp add: rec_ci.simps)

   854 apply(case_tac "rec_ci f",  simp)

   855 done

   856 

   857 lemma para_pattern: 

   858   "\<lbrakk>rec_ci f = (aprog, rs_pos, a_md); rec_calc_rel f lm xs\<rbrakk>

   859   \<Longrightarrow> length lm = rs_pos"

   860 apply(case_tac f, auto)

   861 done

   862 

   863 lemma ci_pr_g_paras:

   864   "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);

   865     rec_ci g = (a, aa, ba);

   866     rec_calc_rel (Pr n f g) (lm @ [x]) rs; x > 0\<rbrakk> \<Longrightarrow> 

   867     aa = Suc rs_pos "

   868 apply(erule calc_pr_reverse, simp)

   869 apply(subgoal_tac "length (args @ [k, rk]) = aa", simp)

   870 apply(subgoal_tac "rs_pos = Suc n", simp)

   871 apply(simp add: ci_pr_para_eq)

   872 apply(erule para_pattern, simp)

   873 done

   874 

   875 lemma ci_pr_g_md_less: 

   876   "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); 

   877     rec_ci g = (a, aa, ba)\<rbrakk> \<Longrightarrow> ba < a_md"

   878 apply(simp add: rec_ci.simps)

   879 apply(case_tac "rec_ci f",  auto)

   880 done

   881 

   882 lemma [intro]: "rec_ci z = (ap, rp, ad) \<Longrightarrow> rp < ad"

   883   by(simp add: rec_ci.simps)

   884 

   885 lemma [intro]: "rec_ci s = (ap, rp, ad) \<Longrightarrow> rp < ad"

   886   by(simp add: rec_ci.simps)

   887 

   888 lemma [intro]: "rec_ci (recf.id nat1 nat2) = (ap, rp, ad) \<Longrightarrow> rp < ad"

   889   by(simp add: rec_ci.simps)

   890 

   891 lemma [intro]: "rec_ci (Cn n f gs) = (ap, rp, ad) \<Longrightarrow> rp < ad"

   892 apply(simp add: rec_ci.simps)

   893 apply(case_tac "rec_ci f",  simp)

   894 done

   895 

   896 lemma [intro]: "rec_ci (Pr n f g) = (ap, rp, ad) \<Longrightarrow> rp < ad"

   897 apply(simp add: rec_ci.simps)

   898 by(case_tac "rec_ci f", case_tac "rec_ci g",  auto)

   899 

   900 lemma [intro]: "rec_ci (Mn n f) = (ap, rp, ad) \<Longrightarrow> rp < ad"

   901 apply(simp add: rec_ci.simps)

   902 apply(case_tac "rec_ci f", simp)

   903 apply(arith)

   904 done

   905 

   906 lemma ci_ad_ge_paras: "rec_ci f = (ap, rp, ad) \<Longrightarrow> ad > rp"

   907 apply(case_tac f, auto)

   908 done

   909 

   910 lemma [elim]: "\<lbrakk>a [+] b = []; a \<noteq> [] \<or> b \<noteq> []\<rbrakk> \<Longrightarrow> RR"

   911 apply(auto simp: abc_append.simps abc_shift.simps)

   912 done

   913 

   914 lemma [intro]: "rec_ci z = ([], aa, ba) \<Longrightarrow> False"

   915 by(simp add: rec_ci.simps rec_ci_z_def)

   916 

   917 lemma [intro]: "rec_ci s = ([], aa, ba) \<Longrightarrow> False"

   918 by(auto simp: rec_ci.simps rec_ci_s_def addition.simps)

   919 

   920 lemma [intro]: "rec_ci (id m n) = ([], aa, ba) \<Longrightarrow> False"

   921 by(auto simp: rec_ci.simps rec_ci_id.simps addition.simps)

   922 

   923 lemma [intro]: "rec_ci (Cn n f gs) = ([], aa, ba) \<Longrightarrow> False"

   924 apply(case_tac "rec_ci f", auto simp: rec_ci.simps abc_append.simps)

   925 apply(simp add: abc_shift.simps mv_box.simps)

   926 done

   927 

   928 lemma [intro]: "rec_ci (Pr n f g) = ([], aa, ba) \<Longrightarrow> False"

   929 apply(simp add: rec_ci.simps)

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

   931 by(auto)

   932 

   933 lemma [intro]: "rec_ci (Mn n f) = ([], aa, ba) \<Longrightarrow> False"

   934 apply(case_tac "rec_ci f", auto simp: rec_ci.simps)

   935 done

   936 

   937 lemma rec_ci_not_null:  "rec_ci g = (a, aa, ba) \<Longrightarrow> a \<noteq> []"

   938 by(case_tac g, auto)

   939 

   940 lemma calc_pr_g_def:

   941  "\<lbrakk>rec_calc_rel (Pr rs_pos f g) (lm @ [Suc x]) rsa;

   942    rec_calc_rel (Pr rs_pos f g) (lm @ [x]) rsxa\<rbrakk>

   943  \<Longrightarrow> rec_calc_rel g (lm @ [x, rsxa]) rsa"

   944 apply(erule_tac calc_pr_reverse, simp, simp)

   945 apply(subgoal_tac "rsxa = rk", simp)

   946 apply(erule_tac rec_calc_inj, auto)

   947 done

   948 

   949 lemma ci_pr_md_def: 

   950   "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);

   951     rec_ci g = (a, aa, ba); rec_ci f = (ab, ac, bc)\<rbrakk>

   952   \<Longrightarrow> a_md = Suc (max (n + 3) (max bc ba))"

   953 by(simp add: rec_ci.simps)

   954 

   955 lemma  ci_pr_f_paras: 

   956   "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);

   957     rec_calc_rel (Pr n f g) lm rs;

   958     rec_ci f = (ab, ac, bc)\<rbrakk>  \<Longrightarrow> ac = rs_pos - Suc 0"

   959 apply(subgoal_tac "\<exists>rs. rec_calc_rel f (butlast lm) rs", 

   960       erule_tac exE)

   961 apply(drule_tac f = f and lm = "butlast lm" in para_pattern, 

   962       simp, simp)

   963 apply(drule_tac para_pattern, simp)

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

   965 apply(erule_tac calc_pr_reverse, simp, simp)

   966 apply(erule calc_pr_zero_ex)

   967 done

   968 

   969 lemma ci_pr_md_ge_f:  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);

   970         rec_ci f = (ab, ac, bc)\<rbrakk> \<Longrightarrow> Suc bc \<le> a_md"

   971 apply(case_tac "rec_ci g")

   972 apply(simp add: rec_ci.simps, auto)

   973 done

   974 

   975 lemma ci_pr_md_ge_g:  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);

   976         rec_ci g = (ab, ac, bc)\<rbrakk> \<Longrightarrow> bc < a_md"

   977 apply(case_tac "rec_ci f")

   978 apply(simp add: rec_ci.simps, auto)

   979 done 

   980 

   981 lemma rec_calc_rel_def0: 

   982   "\<lbrakk>rec_calc_rel (Pr n f g) lm rs; rec_calc_rel f (butlast lm) rsa\<rbrakk>

   983   \<Longrightarrow> rec_calc_rel (Pr n f g) (butlast lm @ [0]) rsa"

   984   apply(rule_tac calc_pr_zero, simp)

   985 apply(erule_tac calc_pr_reverse, simp, simp, simp)

   986 done

   987 

   988 lemma [simp]:  "length (mv_box m n) = 3"

   989 by (auto simp: mv_box.simps)

   990 (*

   991 lemma

   992   "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);

   993   rec_calc_rel (Pr n f g) lm rs;

   994   rec_ci g = (a, aa, ba);

   995   rec_ci f = (ab, ac, bc)\<rbrakk>

   996 \<Longrightarrow> \<exists>ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = 3 + length ab \<and> bp = recursive.mv_box (n - Suc 0) n 3"

   997 apply(simp add: rec_ci.simps)

   998 apply(rule_tac x = "recursive.mv_box (n - Suc 0) (max (Suc (Suc n)) (max bc ba)) 3 [+] ab" in exI, simp)

   999 apply(rule_tac x = "([Dec (max (Suc (Suc n)) (max bc ba)) (length a + 7)] [+] a [+] 

  1000   [Inc (n - Suc 0), Dec n 3, Goto (Suc 0)]) @ [Dec (Suc n) 0, Inc n, Goto (length a + 4)]" in exI, simp)

  1001 apply(auto simp: abc_append_commute)

  1002 done

  1003 

  1004 lemma  "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);

  1005         rec_ci g = (a, aa, ba); rec_ci f = (ab, ac, bc)\<rbrakk>

  1006     \<Longrightarrow> \<exists>ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = 3 \<and> bp = ab"

  1007 apply(simp add: rec_ci.simps)

  1008 apply(rule_tac x = "recursive.mv_box (n - Suc 0) (max (Suc (Suc n)) (max bc ba)) 3" in exI, simp)

  1009 apply(rule_tac x = "recursive.mv_box (n - Suc 0) n 3 [+]

  1010      ([Dec (max (Suc (Suc n)) (max bc ba)) (length a + 7)] [+] a 

  1011   [+] [Inc (n - Suc 0), Dec n 3, Goto (Suc 0)]) @ [Dec (Suc n) 0, Inc n, Goto (length a + 4)]" in exI, auto)

  1012 apply(simp add: abc_append_commute)

  1013 done

  1014 *)

  1015 

  1016 lemma [simp]: "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); rec_calc_rel (Pr n f g) lm rs\<rbrakk>

  1017     \<Longrightarrow> rs_pos = Suc n"

  1018 apply(simp add: ci_pr_para_eq)

  1019 done

  1020 

  1021 

  1022 lemma [simp]: "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md); rec_calc_rel (Pr n f g) lm rs\<rbrakk>

  1023     \<Longrightarrow> length lm = Suc n"

  1024 apply(subgoal_tac "rs_pos = Suc n", rule_tac para_pattern, simp, simp)

  1025 apply(case_tac "rec_ci f", case_tac "rec_ci g", simp add: rec_ci.simps)

  1026 done

  1027 

  1028 lemma [simp]: "rec_ci (Pr n f g) = (a, rs_pos, a_md) \<Longrightarrow> Suc (Suc n) < a_md"

  1029 apply(case_tac "rec_ci f", case_tac "rec_ci g", simp add: rec_ci.simps)

  1030 apply arith

  1031 done

  1032 

  1033 lemma [simp]: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md) \<Longrightarrow> 0 < rs_pos"

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

  1035 apply(simp add: rec_ci.simps)

  1036 done

  1037 

  1038 lemma [simp]: "Suc (Suc rs_pos) < a_md \<Longrightarrow> 

  1039        butlast lm @ (last lm - xa) # (rsa::nat) # 0 # 0\<up>(a_md - Suc (Suc (Suc rs_pos))) @ xa # suf_lm =

  1040        butlast lm @ (last lm - xa) # rsa # 0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm"

  1041 apply(simp add: replicate_Suc[THEN sym])

  1042 done

  1043 

  1044 lemma pr_cycle_part_ind: 

  1045   assumes g_ind: 

  1046   "\<And>lm rs suf_lm. rec_calc_rel g lm rs \<Longrightarrow> 

  1047   \<exists>stp. abc_steps_l (0, lm @ 0\<up>(ba - aa) @ suf_lm) a stp = 

  1048                     (length a, lm @ rs # 0\<up>(ba - Suc aa) @ suf_lm)"

  1049   and ap_def: 

  1050   "ap = ([Dec (a_md - Suc 0) (length a + 7)] [+]

  1051         (a [+] [Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)])) @

  1052          [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]"

  1053   and h: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)" 

  1054          "rec_calc_rel (Pr n f g) 

  1055                    (butlast lm @ [last lm - Suc xa]) rsxa" 

  1056          "Suc xa \<le> last lm" 

  1057          "rec_ci g = (a, aa, ba)"

  1058          "rec_calc_rel (Pr n f g) (butlast lm @ [last lm - xa]) rsa"

  1059          "lm \<noteq> []"

  1060   shows 

  1061   "\<exists>stp. abc_steps_l 

  1062      (0, butlast lm @ (last lm - Suc xa) # rsxa # 

  1063                0\<up>(a_md - Suc (Suc rs_pos)) @ Suc xa # suf_lm) ap stp =

  1064      (0, butlast lm @ (last lm - xa) # rsa

  1065                  # 0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm)"

  1066 proof -

  1067   have k1: "\<exists>stp. abc_steps_l (0, butlast lm @ (last lm - Suc xa) #

  1068     rsxa # 0\<up>(a_md - Suc (Suc rs_pos)) @ Suc xa # suf_lm) ap stp =

  1069          (length a + 4, butlast lm @ (last lm - xa) # 0 # rsa #

  1070                            0\<up>(a_md - Suc (Suc (Suc rs_pos))) @ xa # suf_lm)"

  1071     apply(simp add: ap_def, rule_tac abc_add_exc1)

  1072     apply(rule_tac as = "Suc 0" and 

  1073       bm = "butlast lm @ (last lm - Suc xa) # 

  1074       rsxa # 0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm" in abc_append_exc2,

  1075       auto)

  1076   proof -

  1077     show 

  1078       "\<exists>astp. abc_steps_l (0, butlast lm @ (last lm - Suc xa) # rsxa 

  1079                    # 0\<up>(a_md - Suc (Suc rs_pos)) @ Suc xa # suf_lm) 

  1080               [Dec (a_md - Suc 0)(length a + 7)] astp =

  1081       (Suc 0, butlast lm @ (last lm - Suc xa) # 

  1082              rsxa # 0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm)"

  1083       apply(rule_tac x = "Suc 0" in exI, 

  1084           simp add: abc_steps_l.simps abc_step_l.simps

  1085                      abc_fetch.simps)

  1086       apply(subgoal_tac "length lm = Suc n \<and> rs_pos = Suc n \<and>

  1087                               a_md > Suc (Suc rs_pos)")

  1088       apply(simp add: abc_lm_v.simps nth_append abc_lm_s.simps)

  1089       apply(insert nth_append[of 

  1090                  "(last lm - Suc xa) # rsxa # 0\<up>(a_md - Suc (Suc rs_pos))" 

  1091                  "Suc xa # suf_lm" "(a_md - rs_pos)"], simp)

  1092       apply(simp add: list_update_append del: list_update.simps)

  1093       apply(insert list_update_append[of "(last lm - Suc xa) # rsxa # 

  1094                                           0\<up>(a_md - Suc (Suc rs_pos))" 

  1095                     "Suc xa # suf_lm" "a_md - rs_pos" "xa"], simp)

  1096       apply(case_tac a_md, simp, simp)

  1097       apply(insert h, simp)

  1098       apply(insert para_pattern[of "Pr n f g" aprog rs_pos a_md 

  1099                     "(butlast lm @ [last lm - Suc xa])" rsxa], simp)

  1100       done

  1101   next

  1102     show "\<exists>bstp. abc_steps_l (0, butlast lm @ (last lm - Suc xa) # 

  1103            rsxa # 0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm) (a [+] 

  1104             [Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)]) bstp =

  1105          (3 + length a, butlast lm @ (last lm - xa) # 0 # rsa #

  1106                           0\<up>(a_md - Suc (Suc (Suc rs_pos))) @ xa # suf_lm)"

  1107       apply(rule_tac as = "length a" and

  1108                bm = "butlast lm @ (last lm - Suc xa) # rsxa # rsa #

  1109                      0\<up>(a_md - Suc (Suc (Suc rs_pos))) @ xa # suf_lm" 

  1110         in abc_append_exc2, simp_all)

  1111     proof -

  1112       from h have j1: "aa = Suc rs_pos \<and> a_md > ba \<and> ba > Suc rs_pos"

  1113 	apply(insert h)

  1114 	apply(insert ci_pr_g_paras[of n f g aprog rs_pos

  1115                  a_md a aa ba "butlast lm" "last lm - xa" rsa], simp)

  1116 	apply(drule_tac ci_pr_md_ge_g, auto)

  1117 	apply(erule_tac ci_ad_ge_paras)

  1118 	done

  1119       from h have j2: "rec_calc_rel g (butlast lm @ 

  1120                                   [last lm - Suc xa, rsxa]) rsa"

  1121 	apply(rule_tac  calc_pr_g_def, simp, simp)

  1122 	done

  1123       from j1 and j2 show 

  1124         "\<exists>astp. abc_steps_l (0, butlast lm @ (last lm - Suc xa) #

  1125                 rsxa # 0\<up>(a_md - Suc (Suc rs_pos)) @ xa # suf_lm) a astp =

  1126         (length a, butlast lm @ (last lm - Suc xa) # rsxa # rsa 

  1127                          # 0\<up>(a_md - Suc (Suc (Suc rs_pos))) @ xa # suf_lm)"

  1128 	apply(insert g_ind[of

  1129           "butlast lm @ (last lm - Suc xa) # [rsxa]" rsa 

  1130           "0\<up>(a_md - ba - Suc 0) @ xa # suf_lm"], simp, auto)

  1131 	apply(simp add: exponent_add_iff)

  1132 	apply(rule_tac x = stp in exI, simp add: numeral_3_eq_3)

  1133 	done

  1134     next

  1135       from h have j3: "length lm = rs_pos \<and> rs_pos > 0"