diff -r 514809bb7ce4 -r e55c8e5da49f thys/Recursive.thy
--- a/thys/Recursive.thy	Thu Feb 28 12:37:33 2013 +0000
+++ b/thys/Recursive.thy	Thu Feb 28 15:21:43 2013 +0000
@@ -3101,7 +3101,7 @@
   "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); 
     rec_ci f = (a, aa, ba); 
     pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
-                                    (map rec_ci (f # gs))))\<rbrakk>
+                                    (map rec_ci (gs))))\<rbrakk>
     \<Longrightarrow> \<exists>ap bp cp. 
       aprog = ap [+] bp [+] cp \<and>
       length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
@@ -3130,7 +3130,7 @@
     length lm = n;
     rec_ci f = (a, aa, ba);
     pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
-                                          (map rec_ci (f # gs))))\<rbrakk>
+                                          (map rec_ci (gs))))\<rbrakk>
   \<Longrightarrow> \<exists>stp. abc_steps_l ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
           3 * length gs, lm @ 0\<up>(pstr - n) @ ys @
                  0\<up>(a_md - pstr - length ys) @ suf_lm) aprog stp = 
@@ -3146,7 +3146,7 @@
     "length lm = n"    
     "rec_ci f = (a, aa, ba)"
     and g: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
-                                        (map rec_ci (f # gs))))"
+                                        (map rec_ci (gs))))"
   from h and g have k1: 
     "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> 
     length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
@@ -3190,7 +3190,7 @@
   "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); 
     rec_ci f = (a, aa, ba);
     Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
-                         (map rec_ci (f # gs)))) = pstr\<rbrakk>
+                         (map rec_ci (gs)))) = pstr\<rbrakk>
    \<Longrightarrow> \<exists>ap bp. aprog = ap [+] bp \<and> 
                  ap = cn_merge_gs (map rec_ci gs) pstr"
 apply(simp add: rec_ci.simps)
@@ -3222,7 +3222,7 @@
           "length lm = n" 
           "rec_ci f = (a, aa, ba)" 
           "Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
-                               (map rec_ci (f # gs)))) = pstr"
+                               (map rec_ci (gs)))) = pstr"
   shows  
   "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp =
   ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3 * length gs, 
@@ -3287,7 +3287,7 @@
   "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
   rec_calc_rel f ys rs; rec_ci f = (a, aa, ba);
   pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
-               (map rec_ci (f # gs))))\<rbrakk>
+               (map rec_ci (gs))))\<rbrakk>
   \<Longrightarrow> length ys < pstr"
 apply(subgoal_tac "length ys = aa", simp)
 apply(subgoal_tac "aa < ba \<and> ba \<le> pstr", 
@@ -3301,7 +3301,7 @@
   "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); 
    rec_ci f = (a, aa, ba);
    Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
-  (map rec_ci (f # gs)))) = pstr\<rbrakk>
+  (map rec_ci (gs)))) = pstr\<rbrakk>
   \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> 
   length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
            3 *length gs + 3 * n \<and> bp = mv_boxes pstr 0 (length gs)"
@@ -3330,7 +3330,7 @@
         length ys = aa;
         rec_ci f = (a, aa, ba);
         pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
-                                    (map rec_ci (f # gs))))\<rbrakk>
+                                    (map rec_ci (gs))))\<rbrakk>
 \<Longrightarrow> \<exists>stp. abc_steps_l ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
                                                3 * length gs + 3 * n,
         0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp =
@@ -3345,7 +3345,7 @@
     "length ys = length gs"  "length lm = n"    
     "rec_ci f = (a, aa, ba)"
     and g: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
-                                         (map rec_ci (f # gs))))"
+                                         (map rec_ci (gs))))"
   from h and g have k1:
     "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = 
     (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
@@ -3391,7 +3391,7 @@
   "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
     rec_ci f = (a, aa, ba);
     Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
-                   (map rec_ci (f # gs)))) = pstr\<rbrakk>
+                   (map rec_ci (gs)))) = pstr\<rbrakk>
    \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
   length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
                                 6 *length gs + 3 * n \<and> bp = a"
@@ -3413,13 +3413,11 @@
 done
 
 lemma calc_cn_f:
-  assumes ind:
-  "\<And>x aprog a_md rs_pos rs suf_lm lm.
-  \<lbrakk>x \<in> set (f # gs);
-  rec_ci x = (aprog, rs_pos, a_md); 
-  rec_calc_rel x lm rs\<rbrakk>
-  \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp =
-  (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
+  assumes ind: 
+  "\<And>x ap fp arity r anything args.
+    \<lbrakk>x = map rec_ci gs; rec_ci f = (ap, arity, fp); rec_calc_rel f args r\<rbrakk>
+    \<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0 \<up> (fp - arity) @ anything) ap stp =
+    (length ap, args @ [r] @ 0 \<up> (fp - arity - 1) @ anything)"  
   and h: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
   "rec_calc_rel (Cn n f gs) lm rs"
   "length ys = length gs"
@@ -3427,7 +3425,7 @@
   "length lm = n"
   "rec_ci f = (a, aa, ba)" 
   and p: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
-                                (map rec_ci (f # gs))))"
+                                (map rec_ci (gs))))"
   shows "\<exists>stp. abc_steps_l   
   ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 3 * n,
   ys @ 0\<up>pstr @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp =
@@ -3449,7 +3447,8 @@
       6 * length gs + 3 * n \<and> bp = a"
     from h and this show "?thesis"
       apply(simp, rule_tac abc_append_exc1, simp_all)
-      apply(insert ind[of f "a" aa ba ys rs 
+      thm ind
+      apply(insert ind[of "map rec_ci gs" a aa ba ys rs 
         "0\<up>(pstr - ba + length gs) @ 0 # lm @ 
         0\<up>(a_md - Suc (pstr + length gs + n)) @ suf_lm"], simp)
       apply(subgoal_tac "ba > aa \<and> aa = length gs\<and> pstr \<ge> ba", simp)
@@ -3464,14 +3463,13 @@
       done
   qed
 qed
-(*
+
 lemma [simp]: 
   "\<lbrakk>pstr + length ys + n \<le> a_md; ys \<noteq> []\<rbrakk> \<Longrightarrow> 
                           pstr < a_md + length suf_lm"
 apply(case_tac "length ys", simp)
 apply(arith)
 done
-*)
 
 lemma [simp]: 
   "pstr > length ys 
@@ -3516,7 +3514,7 @@
   "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
   rec_ci f = (a, aa, ba);
   Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
-                        (map rec_ci (f # gs)))) = pstr\<rbrakk>
+                        (map rec_ci (gs)))) = pstr\<rbrakk>
   \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
   length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
               6 *length gs + 3 * n + length a
@@ -3549,7 +3547,7 @@
   "rec_ci f = (a, aa, ba)"  
   "length lm = n"
   and pdef: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
-                                            (map rec_ci (f # gs))))"
+                                            (map rec_ci (gs))))"
   shows "\<exists>stp. abc_steps_l
            ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs
           + 3 * n + length a, ys @ rs # 0\<up>pstr @ lm @
@@ -3643,7 +3641,7 @@
   "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
   rec_ci f = (a, aa, ba); 
   Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
-                    (map rec_ci (f # gs)))) = pstr\<rbrakk>
+                    (map rec_ci (gs)))) = pstr\<rbrakk>
   \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> 
   length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
   6 *length gs + 3 * n + length a + 3 \<and> bp = empty_boxes (length gs)"
@@ -3673,7 +3671,7 @@
   "rec_calc_rel f ys rs" 
   "rec_ci f = (a, aa, ba)" 
   and pdef: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
-                                             (map rec_ci (f # gs))))"
+                                             (map rec_ci (gs))))"
   and starts: "ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
                               6 * length gs + 3 * n + length a + 3"
   shows "\<exists>stp. abc_steps_l
@@ -3723,7 +3721,7 @@
   "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
   rec_ci f = (a, aa, ba);
   Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
-  (map rec_ci (f # gs)))) = pstr;
+  (map rec_ci (gs)))) = pstr;
   ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
   8 * length gs + 3 * n + length a + 3\<rbrakk>
   \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> 
@@ -3761,7 +3759,7 @@
   "rec_calc_rel f ys rs" 
   "rec_ci f = (a, aa, ba)" 
   and pdef: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
-                                        (map rec_ci (f # gs))))"
+                                        (map rec_ci (gs))))"
   and starts: "ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
                               8 * length gs + 3 * n + length a + 3" 
   shows "\<exists>stp. abc_steps_l
@@ -3802,7 +3800,7 @@
   "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); 
   rec_ci f = (a, aa, ba);
   Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n)
-                          (map rec_ci (f # gs)))) = pstr;
+                          (map rec_ci (gs)))) = pstr;
   ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
                          8 * length gs + 3 * n + length a + 6\<rbrakk>
   \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> 
@@ -3831,7 +3829,7 @@
   "rec_ci f = (a, aa, ba)"
   and pdef: 
   "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) 
-                         (map rec_ci (f # gs))))"
+                         (map rec_ci (gs))))"
   and starts: "ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 
                               8 * length gs + 3 * n + length a + 6" 
   shows "\<exists>stp. abc_steps_l (ss, 0\<up>n @ rs # 0\<up>(pstr - n+ length ys) @
@@ -3874,13 +3872,18 @@
 done
 
 lemma  cn_case: 
-  assumes ind:
+  assumes ind1:
   "\<And>x aprog a_md rs_pos rs suf_lm lm.
-  \<lbrakk>x \<in> set (f # gs);
+  \<lbrakk>x \<in> set gs;
   rec_ci x = (aprog, rs_pos, a_md);
   rec_calc_rel x lm rs\<rbrakk>
   \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = 
                (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)"
+  and ind2: 
+  "\<And>x ap fp arity r anything args.
+    \<lbrakk>x = map rec_ci gs; rec_ci f = (ap, arity, fp); rec_calc_rel f args r\<rbrakk>
+    \<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0 \<up> (fp - arity) @ anything) ap stp =
+    (length ap, args @ [r] @ 0 \<up> (fp - arity - 1) @ anything)"
   and h: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
          "rec_calc_rel (Cn n f gs) lm rs"
   shows "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp 
@@ -3889,7 +3892,7 @@
 proof -
   fix a b c ys
   let ?pstr = "Max (set (Suc n # c # (map (\<lambda>(aprog, p, n). n) 
-                                         (map rec_ci (f # gs)))))"  
+                                         (map rec_ci (gs)))))"  
   let ?gs_len = "listsum (map (\<lambda> (ap, pos, n). length ap) 
                                                 (map rec_ci (gs)))"
   assume g: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)"
@@ -3904,7 +3907,7 @@
     (?gs_len + 3 * length gs, lm @ 0\<up>(?pstr - n) @ ys @
                                0\<up>(a_md - ?pstr - length ys) @ suf_lm)"	
     apply(rule_tac a = a and aa = b and ba = c in cn_calc_gs)
-    apply(rule_tac ind, auto)
+    apply(rule_tac ind1, auto)
     done  
   from g have k2: 
     "\<exists> stp. abc_steps_l (?gs_len + 3 * length gs,  lm @ 
@@ -3928,7 +3931,7 @@
     ys @ 0\<up>?pstr @ 0 # lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm) aprog stp =
     (?gs_len + 6 * length gs + 3 * n + length a, 
    ys @ rs # 0\<up>?pstr  @ lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm)"
-    apply(rule_tac ba = c in calc_cn_f, rule_tac ind, auto)
+    apply(rule_tac ba = c in calc_cn_f, rule_tac ind2, auto)
     done
   from g h have k5:
     "\<exists> stp. abc_steps_l (?gs_len + 6 * length gs + 3 * n + length a,
@@ -4061,18 +4064,25 @@
     by(erule_tac id_case)
 next
   fix n f gs ap fp arity r anything args
-  assume ind: "\<And>x ap fp arity r anything args.
-    \<lbrakk>x \<in> set (f # gs); 
+  assume ind1: "\<And>x ap fp arity r anything args.
+    \<lbrakk>x \<in> set gs; 
     rec_ci x = (ap, arity, fp); 
     rec_calc_rel x args r\<rbrakk>
     \<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) ap stp =
     (length ap, args @ [r] @ 0\<up>(fp - arity - 1) @ anything)"
+  and ind2: 
+    "\<And>x ap fp arity r anything args.
+    \<lbrakk>x = map rec_ci gs; rec_ci f = (ap, arity, fp); rec_calc_rel f args r\<rbrakk>
+    \<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0 \<up> (fp - arity) @ anything) ap stp =
+    (length ap, args @ [r] @ 0 \<up> (fp - arity - 1) @ anything)"
   and h: "rec_ci (Cn n f gs) = (ap, arity, fp)" 
     "rec_calc_rel (Cn n f gs) args r"
   from h show
     "\<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) 
        ap stp = (length ap, args @ [r] @ 0\<up>(fp - arity - 1) @ anything)"
-    apply(rule_tac cn_case, rule_tac ind, auto)
+    apply(rule_tac cn_case)
+    apply(rule_tac ind1, simp, simp, simp)
+    apply(rule_tac ind2, auto)    
     done
 next
   fix n f ap fp arity r anything args
@@ -4325,7 +4335,7 @@
     "(length ys = i \<and> (\<forall> k < i. rec_calc_rel (?ggs ! k)
                         lm (ys ! k)))" ..
   let ?pstr = "Max (set (Suc n # c # map (\<lambda>(aprog, p, n). n)
-    (map rec_ci (f # gs))))"
+    (map rec_ci (gs))))"
   have "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - n) @ suflm) 
     (cn_merge_gs (map rec_ci ?ggs) ?pstr) stp =
     (listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) ?ggs) +