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 empty :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"

    31   where

    32   "empty 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 

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

    75   where

    76   "mv_boxes ab bb 0 = []" |

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

    78   (bb + n)"

    79 

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

    81   where

    82   "empty_boxes 0 = []" |

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

    84 

    85 fun cn_merge_gs ::

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

    87   where

    88   "cn_merge_gs [] p = []" |

    89   "cn_merge_gs (g # gs) p = 

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

    91          gprog [+] empty gpara p [+] cn_merge_gs gs (Suc p))"

    92 

    93 

    94 text {*

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

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

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

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

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

   100 *}

   101 

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

   103   where

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

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

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

   107   "rec_ci (Cn n f gs) = 

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

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

   110        let pstr = 

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

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

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

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

   115             empty fpara pstr [+] empty_boxes (length gs) [+] 

   116              empty pstr n [+] mv_boxes qstr 0 n, n,  qstr + n))" |

   117   "rec_ci (Pr n f g) = 

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

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

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

   121           let e = length gprog + 7 in 

   122            (empty n p [+] fprog [+] empty n (Suc n) [+] 

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

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

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

   126              Suc n, p + 1))" |

   127   "rec_ci (Mn n f) =

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

   129           let len = length (fprog) in 

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

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

   132   by pat_completeness auto

   133 termination 

   134 proof

   135 term size

   136   show "wf (measure size)" by auto

   137 next

   138   fix n f gs x

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

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

   141     by(induct gs, auto)

   142 next

   143   fix n f g

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

   145 next

   146   fix n f g x xa y xb ya

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

   148 next

   149   fix n f

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

   151 qed

   152 

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

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

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

   156         empty.simps[simp del] addition.simps[simp del]

   157   

   158 thm rec_calc_rel.induct

   159 

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

   161         abc_step_l.simps[simp del] 

   162 

   163 lemma abc_steps_add: 

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

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

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

   167 proof -

   168   fix m n as lm

   169   assume ind: 

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

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

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

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

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

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

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

   177     apply(simp add: abc_steps_l.simps)

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

   179           simp add: abc_steps_l.simps)

   180     done

   181 qed

   182 

   183 (*lemmas: rec_ci and rec_calc_rel*)

   184 

   185 lemma rec_calc_inj_case_z: 

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

   187 apply(auto elim: calc_z_reverse)

   188 done

   189 

   190 lemma  rec_calc_inj_case_s: 

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

   192 apply(auto elim: calc_s_reverse)

   193 done

   194 

   195 lemma rec_calc_inj_case_id:

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

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

   198 apply(auto elim: calc_id_reverse)

   199 done

   200 

   201 lemma rec_calc_inj_case_mn:

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

   203            \<Longrightarrow> x = y" 

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

   205   shows "x = y"

   206   apply(insert h)

   207   apply(elim  calc_mn_reverse)

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

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

   210 proof -

   211   fix v va

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

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

   214     "0 < v"

   215   thus "False"

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

   217     done

   218 next

   219   fix v va

   220   assume 

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

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

   223   thus "x = y"

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

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

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

   227     done

   228 qed 

   229 

   230 lemma rec_calc_inj_case_pr: 

   231   assumes f_ind: 

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

   233   and g_ind:

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

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

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

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

   238   shows "x = y"

   239   apply(case_tac "rec_ci f")

   240 proof -

   241   fix a b c

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

   243   hence ng_ind: 

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

   245     \<Longrightarrow> xc = yb"

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

   247     done

   248   from h show "x = y"

   249     apply(erule_tac calc_pr_reverse, erule_tac calc_pr_reverse)

   250     apply(erule f_ind, simp, simp)

   251     apply(erule_tac calc_pr_reverse, simp, simp)

   252   proof -

   253     fix la ya ry laa yaa rya

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

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

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

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

   258     from k2 have "ry = rya"

   259       apply(induct ya arbitrary: ry rya)

   260       apply(erule_tac calc_pr_reverse, 

   261         erule_tac calc_pr_reverse, simp)

   262       apply(erule f_ind, simp, simp, simp)

   263       apply(erule_tac calc_pr_reverse, simp)

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

   265     proof -

   266       fix ya ry rya l y ryb laa yb ryc

   267       assume ind:

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

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

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

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

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

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

   274       from j show "ry = rya"

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

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

   277 	done

   278     qed 

   279     from k1 and this show "x = y"

   280       apply(simp)

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

   282       done

   283   qed  

   284 qed

   285 

   286 lemma Suc_nth_part_eq:

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

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

   289 apply(rule allI, rule impI)

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

   291 done

   292 

   293 

   294 lemma list_eq_intro:  

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

   296   \<Longrightarrow> xs = ys"

   297 apply(induct xs arbitrary: ys, simp)

   298 apply(case_tac ys, simp, simp)

   299 proof -

   300   fix a xs ys aa list

   301   assume ind: 

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

   303     \<Longrightarrow> xs = ys"

   304     and h: "length xs = length list" 

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

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

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

   308     apply(frule Suc_nth_part_eq, simp)

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

   310     done

   311 qed

   312 

   313 lemma rec_calc_inj_case_cn: 

   314   assumes ind: 

   315   "\<And>x l xa y.

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

   317   \<Longrightarrow> xa = y"

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

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

   320   shows "x = y"

   321   apply(insert h, elim  calc_cn_reverse)

   322   apply(subgoal_tac "rs = rsa")

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

   324         simp, simp, simp)

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

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

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

   328   done

   329 

   330 lemma rec_calc_inj:

   331   "\<lbrakk>rec_calc_rel f l x; 

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

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

   334 apply(simp add: rec_calc_inj_case_z)

   335 apply(simp add: rec_calc_inj_case_s)

   336 apply(simp add: rec_calc_inj_case_id, simp)

   337 apply(erule rec_calc_inj_case_cn,simp, simp)

   338 apply(erule rec_calc_inj_case_pr, auto)

   339 apply(erule rec_calc_inj_case_mn, auto)

   340 done

   341 

   342 

   343 lemma calc_rel_reverse_ind_step_ex: 

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

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

   346 apply(erule calc_pr_reverse, simp, simp)

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

   348 done

   349 

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

   351 by arith

   352 

   353 lemma calc_pr_para_not_null: 

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

   355 apply(erule calc_pr_reverse, simp, simp)

   356 done

   357 

   358 lemma calc_pr_less_ex: 

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

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

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

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

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

   364 apply(simp add: calc_pr_para_not_null)

   365 done

   366 

   367 lemma calc_pr_zero_ex:

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

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

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

   371       erule_tac exE, simp)

   372 apply(erule_tac calc_pr_reverse, simp)

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

   374 done

   375 

   376 

   377 lemma abc_steps_ind: 

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

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

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

   381 done

   382 

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

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

   385 done

   386 

   387 lemma abc_append_nth: 

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

   389        (ap [+] bp) ! n =

   390          (if n < length ap then ap ! n 

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

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

   393 done

   394 

   395 lemma abc_state_keep:  

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

   397 apply(induct stp, simp add: abc_steps_zero)

   398 apply(simp add: abc_steps_ind)

   399 apply(simp add: abc_steps_zero)

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

   401 done

   402 

   403 lemma abc_halt_equal: 

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

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

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

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

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

   409       simp, simp add: abc_steps_zero)

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

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

   412       simp)

   413 done  

   414 

   415 lemma abc_halt_point_ex: 

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

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

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

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

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

   421 apply(erule_tac exE)

   422 proof -

   423   fix stp

   424   assume "bs = length bp" 

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

   426          "bp \<noteq> []"

   427   thus 

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

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

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

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

   432   proof -

   433     fix stpa

   434     assume ind: 

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

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

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

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

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

   440            "bp \<noteq> []"

   441     from h show 

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

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

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

   445             case_tac "a = length bp")

   446       apply(insert ind, simp)

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

   448       apply(rule_tac abc_halt_equal, simp, simp)

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

   450       apply(simp add: abc_steps_zero)

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

   452                              abc_fetch.simps abc_step_l.simps)

   453       done

   454   qed

   455 qed  

   456 

   457 

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

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

   460 apply(induct ab, simp, simp)

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

   462 done

   463 

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

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

   466 done

   467 

   468 

   469 lemma abc_append_length[simp]:  

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

   471 apply(simp add: abc_append.simps)

   472 done

   473 

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

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

   476 apply(induct cs, simp, simp)

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

   478 done

   479 

   480 lemma abc_halt_point_step[simp]: 

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

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

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

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

   485 apply(case_tac "bp ! a", 

   486                       auto simp: abc_steps_l.simps abc_step_l.simps)

   487 done

   488 

   489 lemma abc_step_state_in:

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

   491   \<Longrightarrow> a < length bp"

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

   493 apply(rule_tac classical, 

   494       simp add: abc_step_l.simps abc_steps_l.simps)

   495 done

   496 

   497 

   498 lemma abc_append_state_in_exc: 

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

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

   501                                              (length ap + bs, l)"

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

   503 proof -

   504   fix stpa bs l

   505   assume ind: 

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

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

   508                                                 (length ap + bs, l)"

   509     and h: "bs < length bp" 

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

   511   from h show 

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

   513                                                 (length ap + bs, l)"

   514     apply(simp add: abc_steps_ind)

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

   516   proof -

   517     fix a b

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

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

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

   521       apply(simp add: abc_step_state_in)

   522       done

   523     from h and g and k1 show 

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

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

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

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

   528                       abc_append_nth)

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

   530                                  abc_steps_l.simps abc_step_l.simps)

   531       done

   532   qed

   533 qed

   534 

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

   536 apply(induct stp, simp add: abc_steps_zero)

   537 apply(simp add: abc_steps_ind)

   538 apply(simp add: abc_steps_zero abc_steps_l.simps 

   539                 abc_fetch.simps abc_step_l.simps)

   540 done

   541 

   542 lemma abc_append_exc1:

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

   544     bs = length bp; 

   545     as = length ap\<rbrakk>

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

   547                                                  = (as + bs, lm')"

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

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

   550 apply(frule_tac abc_halt_point_ex, simp, simp,

   551       erule_tac exE, erule_tac exE) 

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

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

   554       simp add: abc_steps_ind)

   555 apply(subgoal_tac 

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

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

   558 apply(simp add: abc_steps_zero)

   559 apply(rule_tac abc_append_state_in_exc, simp, simp)

   560 done

   561 

   562 lemma abc_append_exc3: 

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

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

   565 apply(erule_tac exE)

   566 proof -

   567   fix stp

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

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

   570   proof(induct stp arbitrary: bs bm)

   571     fix bs bm

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

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

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

   575       done

   576   next

   577     fix stp bs bm

   578     assume ind: 

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

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

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

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

   583     from g show 

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

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

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

   587     proof -

   588       fix a b

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

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

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

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

   593       thus "?thesis"

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

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

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

   597       proof -

   598 	fix stp

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

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

   601                                               = (bs + length ap, bm)"

   602 	  apply(simp add: abc_steps_l.simps abc_steps_zero

   603                           abc_fetch.simps split: if_splits)

   604 	  apply(case_tac "bp ! a", 

   605                 simp_all add: abc_inst_shift.simps abc_append_nth

   606                    abc_steps_l.simps abc_steps_zero abc_step_l.simps)

   607 	  apply(auto)

   608 	  done

   609       qed

   610     qed

   611   qed

   612 qed

   613 

   614 lemma abc_add_equal:

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

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

   617     a < length ap\<rbrakk>

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

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

   620 apply(simp add: abc_steps_ind)

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

   622 proof -

   623   fix astp a b aa ba

   624   assume ind: 

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

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

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

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

   629                                                             = (a, b)"

   630         "a < length ap" 

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

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

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

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

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

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

   637                      nth_append abc_steps_zero)

   638     apply(rule abc_step_state_in, auto)

   639     done

   640 qed

   641 

   642 

   643 lemma abc_add_exc1: 

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

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

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

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

   648 apply(drule_tac abc_halt_point_ex, simp, simp)

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

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

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

   652 apply(simp add: abc_steps_l.simps abc_steps_zero 

   653                 abc_fetch.simps nth_append)

   654 done

   655 

   656 declare abc_shift.simps[simp del] 

   657 

   658 lemma abc_append_exc2: 

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

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

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

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

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

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

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

   666       simp, auto)

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

   668 apply(simp add: abc_append.simps)

   669 done

   670 lemma exp_length[simp]: "length (a\<^bsup>b\<^esup>) = b"

   671 by(simp add: exponent_def)

   672 lemma exponent_add_iff: "a\<^bsup>b\<^esup> @ a\<^bsup>c \<^esup>@ xs = a\<^bsup>b + c \<^esup>@ xs"

   673 apply(auto simp: exponent_def replicate_add)

   674 done

   675 lemma exponent_cons_iff: "a # a\<^bsup>c \<^esup>@ xs = a\<^bsup>Suc c \<^esup>@ xs"

   676 apply(auto simp: exponent_def replicate_add)

   677 done

   678 

   679 

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

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

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

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

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

   685                 abc_step_l.simps abc_lm_v.simps abc_lm_s.simps 

   686                 nth_append list_update_append)

   687 done

   688 

   689 lemma [simp]: 

   690   "length lm = n \<Longrightarrow> 

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

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

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

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

   695                 abc_step_l.simps abc_lm_v.simps abc_lm_s.simps 

   696                 nth_append list_update_append)

   697 done

   698 

   699 lemma pr_cycle_part_middle_inv: 

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

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

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

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

   704 proof -

   705   assume h: "length lm = n"

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

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

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

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

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

   711                     abc_lm_v.simps abc_lm_s.simps nth_append 

   712                     list_update_append abc_fetch.simps)

   713     done

   714   from h have k2: 

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

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

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

   718     apply(induct y)

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

   720           erule_tac exE)

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

   722           simp only: abc_steps_add, simp)

   723     done      

   724   from k1 and k2 show 

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

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

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

   728     apply(erule_tac exE, erule_tac exE)

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

   730     done

   731 qed

   732 

   733 lemma [simp]: 

   734   "length lm = Suc n \<Longrightarrow> 

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

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

   737                     (Suc (Suc (Suc 0))))

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

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

   740          abc_lm_v.simps list_update_append nth_append abc_lm_s.simps)

   741 done

   742 

   743 lemma switch_para_inv:

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

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

   746          "ss = length ap" 

   747          "length lm = Suc n"

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

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

   750 apply(induct y arbitrary: x)

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

   752   simp add: bp_def empty.simps abc_steps_l.simps 

   753             abc_fetch.simps h abc_step_l.simps 

   754             abc_lm_v.simps list_update_append nth_append

   755             abc_lm_s.simps)

   756 proof -

   757   fix y x

   758   assume ind: 

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

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

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

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

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

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

   765           simp only: abc_steps_add bp_def h)

   766     apply(simp add: h)

   767     done

   768 qed

   769 

   770 lemma [simp]:

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

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

   773                                          Suc (Suc (Suc 0)))))"

   774 apply(arith)

   775 done

   776 

   777 lemma [simp]: 

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

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

   780 apply(arith)

   781 done

   782 

   783 lemma [simp]: 

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

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

   786 apply(arith)

   787 done

   788 

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

   790 apply(auto)

   791 done

   792 

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

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

   795 apply(simp add: rec_ci.simps)

   796 apply(case_tac "rec_ci f", simp)

   797 apply(case_tac "rec_ci g", simp)

   798 apply(arith)

   799 done

   800 

   801 (*

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

   803 apply(erule calc_pr_reverse, simp, simp)

   804 done

   805 *)

   806 

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

   808                   \<Longrightarrow> rs_pos = Suc n"

   809 apply(simp add: rec_ci.simps)

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

   811 done

   812 

   813 lemma [intro]:  

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

   815   \<Longrightarrow> length lm = rs_pos"

   816 apply(simp add: rec_ci.simps rec_ci_z_def)

   817 apply(erule_tac calc_z_reverse, simp)

   818 done

   819 

   820 lemma [intro]: 

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

   822   \<Longrightarrow> length lm = rs_pos"

   823 apply(simp add: rec_ci.simps rec_ci_s_def)

   824 apply(erule_tac calc_s_reverse, simp)

   825 done

   826 

   827 lemma [intro]: 

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

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

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

   831 apply(erule_tac calc_id_reverse, simp)

   832 done

   833 

   834 lemma [intro]: 

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

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

   837 apply(erule_tac calc_cn_reverse, simp)

   838 apply(simp add: rec_ci.simps)

   839 apply(case_tac "rec_ci f",  simp)

   840 done

   841 

   842 lemma [intro]:

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

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

   845 apply(erule_tac  calc_pr_reverse, simp)

   846 apply(drule_tac ci_pr_para_eq, simp, simp)

   847 apply(drule_tac ci_pr_para_eq, simp)

   848 done

   849 

   850 lemma [intro]: 

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

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

   853 apply(erule_tac calc_mn_reverse)

   854 apply(simp add: rec_ci.simps)

   855 apply(case_tac "rec_ci f",  simp)

   856 done

   857 

   858 lemma para_pattern: 

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

   860   \<Longrightarrow> length lm = rs_pos"

   861 apply(case_tac f, auto)

   862 done

   863 

   864 lemma ci_pr_g_paras:

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

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

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

   868     aa = Suc rs_pos "

   869 apply(erule calc_pr_reverse, simp)

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

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

   872 apply(simp add: ci_pr_para_eq)

   873 apply(erule para_pattern, simp)

   874 done

   875 

   876 lemma ci_pr_g_md_less: 

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

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

   879 apply(simp add: rec_ci.simps)

   880 apply(case_tac "rec_ci f",  auto)

   881 done

   882 

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

   884   by(simp add: rec_ci.simps)

   885 

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

   887   by(simp add: rec_ci.simps)

   888 

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

   890   by(simp add: rec_ci.simps)

   891 

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

   893 apply(simp add: rec_ci.simps)

   894 apply(case_tac "rec_ci f",  simp)

   895 done

   896 

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

   898 apply(simp add: rec_ci.simps)

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

   900 

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

   902 apply(simp add: rec_ci.simps)

   903 apply(case_tac "rec_ci f", simp)

   904 apply(arith)

   905 done

   906 

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

   908 apply(case_tac f, auto)

   909 done

   910 

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

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

   913 done

   914 

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

   916 by(simp add: rec_ci.simps rec_ci_z_def)

   917 

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

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

   920 

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

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

   923 

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

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

   926 apply(simp add: abc_shift.simps empty.simps)

   927 done

   928 

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

   930 apply(simp add: rec_ci.simps)

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

   932 by(auto)

   933 

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

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

   936 done

   937 

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

   939 by(case_tac g, auto)

   940 

   941 lemma calc_pr_g_def:

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

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

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

   945 apply(erule_tac calc_pr_reverse, simp, simp)

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

   947 apply(erule_tac rec_calc_inj, auto)

   948 done

   949 

   950 lemma ci_pr_md_def: 

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

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

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

   954 by(simp add: rec_ci.simps)

   955 

   956 lemma  ci_pr_f_paras: 

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

   958     rec_calc_rel (Pr n f g) lm rs;

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

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

   961       erule_tac exE)

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

   963       simp, simp)

   964 apply(drule_tac para_pattern, simp)

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

   966 apply(erule_tac calc_pr_reverse, simp, simp)

   967 apply(erule calc_pr_zero_ex)

   968 done

   969 

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

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

   972 apply(case_tac "rec_ci g")

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

   974 done

   975 

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

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

   978 apply(case_tac "rec_ci f")

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

   980 done 

   981 

   982 lemma rec_calc_rel_def0: 

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

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

   985   apply(rule_tac calc_pr_zero, simp)

   986 apply(erule_tac calc_pr_reverse, simp, simp, simp)

   987 done

   988 

   989 lemma [simp]:  "length (empty m n) = 3"

   990 by (auto simp: empty.simps)

   991 (*

   992 lemma

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

   994   rec_calc_rel (Pr n f g) lm rs;

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

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

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

   998 apply(simp add: rec_ci.simps)

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

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

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

  1002 apply(auto simp: abc_append_commute)

  1003 done

  1004 

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

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

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

  1008 apply(simp add: rec_ci.simps)

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

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

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

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

  1013 apply(simp add: abc_append_commute)

  1014 done

  1015 *)

  1016 

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

  1018     \<Longrightarrow> rs_pos = Suc n"

  1019 apply(simp add: ci_pr_para_eq)

  1020 done

  1021 

  1022 

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

  1024     \<Longrightarrow> length lm = Suc n"

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

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

  1027 done

  1028 

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

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

  1031 apply arith

  1032 done

  1033 

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

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

  1036 apply(simp add: rec_ci.simps)

  1037 done

  1038 

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

  1040        butlast lm @ (last lm - xa) # (rsa::nat) # 0 # 0\<^bsup>a_md - Suc (Suc (Suc rs_pos))\<^esup> @ xa # suf_lm =

  1041        butlast lm @ (last lm - xa) # rsa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm"

  1042 apply(simp add: exp_ind_def[THEN sym])

  1043 done

  1044 

  1045 lemma pr_cycle_part_ind: 

  1046   assumes g_ind: 

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

  1048   \<exists>stp. abc_steps_l (0, lm @ 0\<^bsup>ba - aa\<^esup> @ suf_lm) a stp = 

  1049                     (length a, lm @ rs # 0\<^bsup>ba - Suc aa\<^esup> @ suf_lm)"

  1050   and ap_def: 

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

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

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

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

  1055          "rec_calc_rel (Pr n f g) 

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

  1057          "Suc xa \<le> last lm" 

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

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

  1060          "lm \<noteq> []"

  1061   shows 

  1062   "\<exists>stp. abc_steps_l 

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

  1064                0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ Suc xa # suf_lm) ap stp =

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

  1066                  # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm)"

  1067 proof -

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

  1069     rsxa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ Suc xa # suf_lm) ap stp =

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

  1071                            0\<^bsup>a_md - Suc (Suc (Suc rs_pos))\<^esup> @ xa # suf_lm)"

  1072     apply(simp add: ap_def, rule_tac abc_add_exc1)

  1073     apply(rule_tac as = "Suc 0" and 

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

  1075       rsxa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm" in abc_append_exc2,

  1076       auto)

  1077   proof -

  1078     show 

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

  1080                    # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ Suc xa # suf_lm) 

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

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

  1083              rsxa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm)"

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

  1085           simp add: abc_steps_l.simps abc_step_l.simps

  1086                      abc_fetch.simps)

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

  1088                               a_md > Suc (Suc rs_pos)")

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

  1090       apply(insert nth_append[of 

  1091                  "(last lm - Suc xa) # rsxa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup>" 

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

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

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

  1095                                            0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup>" 

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

  1097       apply(case_tac a_md, simp, simp)

  1098       apply(insert h, simp)

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

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

  1101       done

  1102   next

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

  1104            rsxa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm) (a [+] 

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

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

  1107                           0\<^bsup>a_md - Suc (Suc (Suc rs_pos))\<^esup> @ xa # suf_lm)"

  1108       apply(rule_tac as = "length a" and

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

  1110                      0\<^bsup>a_md - Suc (Suc (Suc rs_pos))\<^esup> @ xa # suf_lm" 

  1111         in abc_append_exc2, simp_all)

  1112     proof -

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

  1114 	apply(insert h)

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

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

  1117 	apply(drule_tac ci_pr_md_ge_g, auto)

  1118 	apply(erule_tac ci_ad_ge_paras)

  1119 	done

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

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

  1122 	apply(rule_tac  calc_pr_g_def, simp, simp)

  1123 	done

  1124       from j1 and j2 show 

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

  1126                 rsxa # 0\<^bsup>a_md - Suc (Suc rs_pos)\<^esup> @ xa # suf_lm) a astp =

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

  1128                          # 0\<^bsup>a_md - Suc (Suc (Suc rs_pos))\<^esup> @ xa # suf_lm)"

  1129 	apply(insert g_ind[of

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

  1131           "0\<^bsup>a_md - ba - Suc 0 \<^esup> @ xa # suf_lm"], simp, auto)

  1132 	apply(simp add: exponent_add_iff)

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

  1134 	done

  1135     next