--- 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) +