--- a/thys/Recursive.thy Thu Feb 14 12:11:40 2013 +0000
+++ b/thys/Recursive.thy Fri Feb 15 07:42:47 2013 +0000
@@ -1146,8 +1146,8 @@
[Inc (rs_pos - Suc 0), Dec rs_pos 3, Goto (Suc 0)])) @
[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]"
apply(simp add: rec_ci.simps)
-apply(rule_tac x = "Recursive.mv_box n (max (Suc (Suc (Suc n)))
- (max bc ba)) [+] ab [+] Recursive.mv_box n (Suc n)" in exI,
+apply(rule_tac x = "mv_box n (max (Suc (Suc (Suc n)))
+ (max bc ba)) [+] ab [+] mv_box n (Suc n)" in exI,
simp)
apply(auto simp add: abc_append_commute numeral_3_eq_3)
done
@@ -1357,20 +1357,20 @@
rule_tac x = "initlm ! n" in exI, simp)
done
-lemma [simp]: "abc_fetch 0 (Recursive.mv_box m n) = Some (Dec m 3)"
+lemma [simp]: "abc_fetch 0 (mv_box m n) = Some (Dec m 3)"
apply(simp add: mv_box.simps abc_fetch.simps)
done
-lemma [simp]: "abc_fetch (Suc 0) (Recursive.mv_box m n) =
+lemma [simp]: "abc_fetch (Suc 0) (mv_box m n) =
Some (Inc n)"
apply(simp add: mv_box.simps abc_fetch.simps)
done
-lemma [simp]: "abc_fetch 2 (Recursive.mv_box m n) = Some (Goto 0)"
+lemma [simp]: "abc_fetch 2 (mv_box m n) = Some (Goto 0)"
apply(simp add: mv_box.simps abc_fetch.simps)
done
-lemma [simp]: "abc_fetch 3 (Recursive.mv_box m n) = None"
+lemma [simp]: "abc_fetch 3 (mv_box m n) = None"
apply(simp add: mv_box.simps abc_fetch.simps)
done
@@ -1405,15 +1405,15 @@
lemma [simp]:
"\<lbrakk>length initlm > max m n; m \<noteq> n\<rbrakk> \<Longrightarrow>
\<forall>na. \<not> (\<lambda>(as, lm) m. as = 3)
- (abc_steps_l (0, initlm) (Recursive.mv_box m n) na) m \<and>
+ (abc_steps_l (0, initlm) (mv_box m n) na) m \<and>
mv_box_inv (abc_steps_l (0, initlm)
- (Recursive.mv_box m n) na) m n initlm \<longrightarrow>
+ (mv_box m n) na) m n initlm \<longrightarrow>
mv_box_inv (abc_steps_l (0, initlm)
- (Recursive.mv_box m n) (Suc na)) m n initlm \<and>
- ((abc_steps_l (0, initlm) (Recursive.mv_box m n) (Suc na), m),
- abc_steps_l (0, initlm) (Recursive.mv_box m n) na, m) \<in> mv_box_LE"
+ (mv_box m n) (Suc na)) m n initlm \<and>
+ ((abc_steps_l (0, initlm) (mv_box m n) (Suc na), m),
+ abc_steps_l (0, initlm) (mv_box m n) na, m) \<in> mv_box_LE"
apply(rule allI, rule impI, simp add: abc_steps_ind)
-apply(case_tac "(abc_steps_l (0, initlm) (Recursive.mv_box m n) na)",
+apply(case_tac "(abc_steps_l (0, initlm) (mv_box m n) na)",
simp)
apply(auto split:if_splits simp add:abc_steps_l.simps mv_box_inv.simps)
apply(auto simp add: mv_box_LE_def lex_triple_def lex_pair_def
@@ -1430,14 +1430,14 @@
(abc_steps_l (0::nat, initlm) (mv_box m n) stp)"
apply(insert halt_lemma2[of mv_box_LE
"\<lambda> ((as, lm), m). mv_box_inv (as, lm) m n initlm"
- "\<lambda> stp. (abc_steps_l (0, initlm) (Recursive.mv_box m n) stp, m)"
+ "\<lambda> stp. (abc_steps_l (0, initlm) (mv_box m n) stp, m)"
"\<lambda> ((as, lm), m). as = (3::nat)"
])
apply(insert wf_mv_box_le)
apply(simp add: mv_box_inv_init abc_steps_zero)
apply(erule_tac exE)
apply(rule_tac x = na in exI)
-apply(case_tac "(abc_steps_l (0, initlm) (Recursive.mv_box m n) na)",
+apply(case_tac "(abc_steps_l (0, initlm) (mv_box m n) na)",
simp, auto)
done
@@ -1454,7 +1454,7 @@
= (3, (lm[n := (lm ! m + lm ! n)])[m := 0::nat])"
apply(drule mv_box_inv_halt, simp, erule_tac exE)
apply(rule_tac x = stp in exI)
-apply(case_tac "abc_steps_l (0, lm) (Recursive.mv_box m n) stp",
+apply(case_tac "abc_steps_l (0, lm) (mv_box m n) stp",
simp)
apply(erule_tac mv_box_halt_cond, auto)
done
@@ -1510,7 +1510,7 @@
\<Longrightarrow> \<exists>ap bp. aprog = ap [+] bp \<and>
ap = mv_box n (max (Suc (Suc (Suc n))) (max bc ba))"
apply(simp add: rec_ci.simps)
-apply(rule_tac x = "(ab [+] (Recursive.mv_box n (Suc n) [+]
+apply(rule_tac x = "(ab [+] (mv_box n (Suc n) [+]
([Dec (max (n + 3) (max bc ba)) (length a + 7)]
[+] (a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])) @
[Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]))" in exI, auto)
@@ -1615,10 +1615,10 @@
lemma pr_prog_ex[simp]: "\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_ci g = (a, aa, ba); rec_ci f = (ab, ac, bc)\<rbrakk>
- \<Longrightarrow> \<exists>cp. aprog = Recursive.mv_box n (max (n + 3)
+ \<Longrightarrow> \<exists>cp. aprog = mv_box n (max (n + 3)
(max bc ba)) [+] cp"
apply(simp add: rec_ci.simps)
-apply(rule_tac x = "(ab [+] (Recursive.mv_box n (Suc n) [+]
+apply(rule_tac x = "(ab [+] (mv_box n (Suc n) [+]
([Dec (max (n + 3) (max bc ba)) (length a + 7)]
[+] (a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)]))
@ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]))" in exI)
@@ -1639,7 +1639,7 @@
apply(case_tac "rec_ci g", simp add: rec_ci.simps)
apply(rule_tac x = "mv_box n
(max (n + 3) (max bc c))" in exI, simp)
-apply(rule_tac x = "Recursive.mv_box n (Suc n) [+]
+apply(rule_tac x = "mv_box n (Suc n) [+]
([Dec (max (n + 3) (max bc c)) (length a + 7)]
[+] a [+] [Inc n, Dec (Suc n) 3, Goto (Suc 0)])
@ [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length a + 4)]" in exI,
@@ -1651,10 +1651,10 @@
"\<lbrakk>rec_ci (Pr n f g) = (aprog, rs_pos, a_md);
rec_ci g = (a, aa, ba);
rec_ci f = (ab, ac, bc)\<rbrakk> \<Longrightarrow>
- \<exists>ap. (\<exists>cp. aprog = ap [+] Recursive.mv_box n (Suc n) [+] cp)
+ \<exists>ap. (\<exists>cp. aprog = ap [+] mv_box n (Suc n) [+] cp)
\<and> length ap = 3 + length ab"
apply(simp add: rec_ci.simps)
-apply(rule_tac x = "Recursive.mv_box n (max (n + 3)
+apply(rule_tac x = "mv_box n (max (n + 3)
(max bc ba)) [+] ab" in exI, simp)
apply(rule_tac x = "([Dec (max (n + 3) (max bc ba))
(length a + 7)] [+] a [+]
@@ -1673,9 +1673,9 @@
Goto (length a + 4)] [+] cp) \<and>
length ap = 6 + length ab"
apply(simp add: rec_ci.simps)
-apply(rule_tac x = "Recursive.mv_box n
+apply(rule_tac x = "mv_box n
(max (n + 3) (max bc ba)) [+] ab [+]
- Recursive.mv_box n (Suc n)" in exI, simp)
+ mv_box n (Suc n)" in exI, simp)
apply(rule_tac x = "[]" in exI, auto)
apply(simp add: abc_append_commute)
done
@@ -1751,7 +1751,7 @@
apply(erule_tac exE, erule_tac exE, simp)
apply(subgoal_tac
"\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm)
- ([] [+] Recursive.mv_box n
+ ([] [+] mv_box n
(max (n + 3) (max bc ba)) [+] cp) stp =
(0 + 3, butlast lm @ 0 # 0\<up>(a_md - Suc rs_pos) @
last lm # suf_lm)", simp)
@@ -1817,21 +1817,21 @@
0\<up>(a_md - rs_pos - 2) @ last lm # suf_lm)"
proof -
from h have "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
- length ap = 3 + length ab \<and> bp = Recursive.mv_box n (Suc n)"
+ length ap = 3 + length ab \<and> bp = mv_box n (Suc n)"
by auto
thus "?thesis"
proof(erule_tac exE, erule_tac exE, erule_tac exE,
erule_tac exE)
fix ap cp bp apa
assume "aprog = ap [+] bp [+] cp \<and> length ap = 3 +
- length ab \<and> bp = Recursive.mv_box n (Suc n)"
+ length ab \<and> bp = mv_box n (Suc n)"
thus "?thesis"
apply(simp del: abc_append_commute)
apply(subgoal_tac
"\<exists>stp. abc_steps_l (3 + length ab,
butlast lm @ rsa # 0\<up>(a_md - Suc rs_pos) @
last lm # suf_lm) (ap [+]
- Recursive.mv_box n (Suc n) [+] cp) stp =
+ mv_box n (Suc n) [+] cp) stp =
((3 + length ab) + 3, butlast lm @ 0 # rsa #
0\<up>(a_md - Suc (Suc rs_pos)) @ last lm # suf_lm)", simp)
apply(rule_tac abc_append_exc1, simp_all)
@@ -2811,7 +2811,7 @@
from h show
"\<exists>bstp. abc_steps_l (0, lm @ 0\<up>(pstr - n) @ butlast ys @
0\<up>(a_md - (pstr + length list)) @ suf_lm)
- ((\<lambda>(gprog, gpara, gn). gprog [+] Recursive.mv_box gpara
+ ((\<lambda>(gprog, gpara, gn). gprog [+] mv_box gpara
(pstr + length list)) (rec_ci a)) bstp =
((\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3,
lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm)"
@@ -2850,7 +2850,7 @@
from h and this show
"\<exists>bstp. abc_steps_l (0, lm @ ys ! length list #
0\<up>(pstr - Suc n) @ butlast ys @ 0\<up>(a_md - (pstr + length list)) @ suf_lm)
- (Recursive.mv_box b (pstr + length list)) bstp =
+ (mv_box b (pstr + length list)) bstp =
(3, lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm)"
apply(insert mv_box_ex [of b "pstr + length list"
"lm @ ys ! length list # 0\<up>(pstr - Suc n) @ butlast ys @
@@ -2862,7 +2862,7 @@
done
next
fix aa b c
- show "3 = length (Recursive.mv_box b (pstr + length list))"
+ show "3 = length (mv_box b (pstr + length list))"
by simp
next
fix aa b aaa ba
@@ -2875,7 +2875,7 @@
next
show "(\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3 =
length ((\<lambda>(gprog, gpara, gn). gprog [+]
- Recursive.mv_box gpara (pstr + length list)) (rec_ci a))"
+ mv_box gpara (pstr + length list)) (rec_ci a))"
by(case_tac "rec_ci a", simp)
next
show "listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) list) +
@@ -2884,7 +2884,7 @@
((\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3)" by simp
next
show "(\<lambda>(gprog, gpara, gn). gprog [+]
- Recursive.mv_box gpara (pstr + length list)) (rec_ci a) \<noteq> []"
+ mv_box gpara (pstr + length list)) (rec_ci a) \<noteq> []"
by(case_tac "rec_ci a",
simp add: abc_append.simps abc_shift.simps)
qed
@@ -2983,7 +2983,7 @@
"length (lm3::nat list) = ba - Suc (aa + n)"
thus " \<exists>bstp. abc_steps_l (0, lm1 @ 0\<up>n @ last lm2 # lm3 @
butlast lm2 @ 0 # lm4)
- (Recursive.mv_box (aa + n) (ba + n)) bstp
+ (mv_box (aa + n) (ba + n)) bstp
= (3, lm1 @ 0 # 0\<up>n @ lm3 @ lm2 @ lm4)"
apply(insert mv_box_ex[of "aa + n" "ba + n"
"lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4"], simp)
@@ -3065,7 +3065,7 @@
thus
"\<exists>bstp. abc_steps_l (0, lm1 @ butlast lm3 @ 0 # lm2 @ 0\<up>n @
last lm3 # lm4)
- (Recursive.mv_box (aa + n) (ba + n)) bstp =
+ (mv_box (aa + n) (ba + n)) bstp =
(3, lm1 @ lm3 @ lm2 @ 0 # 0\<up>n @ lm4)"
apply(insert mv_box_ex[of "aa + n" "ba + n" "lm1 @ butlast lm3 @
0 # lm2 @ 0\<up>n @ last lm3 # lm4"], simp)
@@ -3133,9 +3133,9 @@
simp add: cn_merge_gs_len)
apply(rule_tac x =
"mv_boxes (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))
- 0 (length gs) [+] a [+]Recursive.mv_box aa (max (Suc n)
+ 0 (length gs) [+] a [+]mv_box aa (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
- empty_boxes (length gs) [+] Recursive.mv_box (max (Suc n)
+ empty_boxes (length gs) [+] mv_box (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
mv_boxes (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci)
` set gs))) + length gs)) 0 n" in exI, auto)
@@ -3218,9 +3218,9 @@
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n [+]
mv_boxes (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
- a [+] Recursive.mv_box aa (max (Suc n)
+ a [+] mv_box aa (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
- empty_boxes (length gs) [+] Recursive.mv_box (max (Suc n)
+ empty_boxes (length gs) [+] mv_box (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
mv_boxes (Suc (max (Suc n) (Max
(insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n"
@@ -3332,9 +3332,9 @@
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n" in exI,
simp add: cn_merge_gs_len)
apply(rule_tac x = "a [+]
- Recursive.mv_box aa (max (Suc n) (Max (insert ba
+ mv_box aa (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
- empty_boxes (length gs) [+] Recursive.mv_box
+ empty_boxes (length gs) [+] mv_box
(max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n
[+] mv_boxes (Suc (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI,
@@ -3423,9 +3423,9 @@
mv_boxes (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs)" in exI,
simp add: cn_merge_gs_len)
-apply(rule_tac x = "Recursive.mv_box aa (max (Suc n) (Max (insert ba
+apply(rule_tac x = "mv_box aa (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
- empty_boxes (length gs) [+] Recursive.mv_box (max (Suc n) (
+ empty_boxes (length gs) [+] mv_box (max (Suc n) (
Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
mv_boxes (Suc (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI,
@@ -3523,7 +3523,7 @@
"\<lbrakk>pstr > length ys\<rbrakk>
\<Longrightarrow> \<exists>stp. abc_steps_l (0, ys @ rs # 0\<up>pstr @ lm @
0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)
- (Recursive.mv_box (length ys) pstr) stp =
+ (mv_box (length ys) pstr) stp =
(3, ys @ 0\<up>(pstr - (length ys)) @ rs #
0\<up>length ys @ lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
apply(insert mv_box_ex[of "length ys" pstr
@@ -3552,7 +3552,7 @@
in exI, simp add: cn_merge_gs_len)
apply(rule_tac x =
"empty_boxes (length gs) [+]
- Recursive.mv_box (max (Suc n) (Max (insert ba
+ mv_box (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
mv_boxes (Suc (max (Suc n) (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))
+ length gs)) 0 n" in exI,
@@ -3599,7 +3599,7 @@
fix ap bp apa cp
assume "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 \<and> bp = Recursive.mv_box (length ys) pstr"
+ 3 * n + length a \<and> bp = mv_box (length ys) pstr"
thus"?thesis"
apply(simp, rule_tac abc_append_exc1, simp_all)
apply(rule_tac save_rs', insert h)
@@ -3674,10 +3674,10 @@
(insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n
[+] mv_boxes (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
- a [+] Recursive.mv_box aa (max (Suc n)
+ a [+] mv_box aa (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))))"
in exI, simp add: cn_merge_gs_len)
-apply(rule_tac x = " Recursive.mv_box (max (Suc n) (Max (insert ba
+apply(rule_tac x = " mv_box (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
mv_boxes (Suc (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI,
@@ -3755,7 +3755,7 @@
\<circ> rec_ci) ` set gs))) + length gs)) n [+]
mv_boxes (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
- a [+] Recursive.mv_box aa (max (Suc n)
+ a [+] mv_box aa (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
empty_boxes (length gs)" in exI, simp add: cn_merge_gs_len)
apply(rule_tac x = "mv_boxes (Suc (max (Suc n)
@@ -3798,7 +3798,7 @@
proof (erule_tac exE, erule_tac exE, erule_tac exE, erule_tac exE)
fix ap bp apa cp
assume "aprog = ap [+] bp [+] cp \<and> length ap = ss \<and>
- bp = Recursive.mv_box pstr n"
+ bp = mv_box pstr n"
thus"?thesis"
apply(simp, rule_tac abc_append_exc1, simp_all add: starts h)
apply(insert mv_box_ex[of pstr n "0\<up>pstr @ rs # 0\<up>length gs @
@@ -3834,10 +3834,10 @@
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))
+ length gs)) n [+] mv_boxes (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
- a [+] Recursive.mv_box aa (max (Suc n)
+ a [+] mv_box aa (max (Suc n)
(Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
empty_boxes (length gs) [+]
- Recursive.mv_box (max (Suc n) (Max (insert ba
+ mv_box (max (Suc n) (Max (insert ba
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n" in exI, simp add: cn_merge_gs_len)
apply(rule_tac x = "[]" in exI, auto simp: abc_append_commute)
done
@@ -4383,9 +4383,9 @@
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) +
length gs)) n [+] mv_boxes (max (Suc n) (Max (insert c
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) 0 (length gs) [+]
- a [+] Recursive.mv_box b (max (Suc n)
+ a [+] mv_box b (max (Suc n)
(Max (insert c (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) [+]
- empty_boxes (length gs) [+] Recursive.mv_box (max (Suc n)
+ empty_boxes (length gs) [+] mv_box (max (Suc n)
(Max (insert c (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs)))) n [+]
mv_boxes (Suc (max (Suc n) (Max (insert c
(((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI)