--- a/thys/Recursive.thy Mon Feb 11 00:08:54 2013 +0000
+++ b/thys/Recursive.thy Mon Feb 11 08:31:48 2013 +0000
@@ -2,9 +2,7 @@
imports Rec_Def Abacus
begin
-section {*
- Compiling from recursive functions to Abacus machines
- *}
+section {* Compiling from recursive functions to Abacus machines *}
text {*
Some auxilliary Abacus machines used to construct the result Abacus machines.
@@ -24,8 +22,7 @@
fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"
where
- "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7,
- Inc m, Goto 4]"
+ "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]"
fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
where
@@ -47,25 +44,18 @@
"abc_append al bl = (let al_len = length al in
al @ abc_shift bl al_len)"
-text {*
- The compilation of @{text "z"}-operator.
-*}
+text {* The compilation of @{text "z"}-operator. *}
definition rec_ci_z :: "abc_inst list"
where
"rec_ci_z \<equiv> [Goto 1]"
-text {*
- The compilation of @{text "s"}-operator.
-*}
+text {* The compilation of @{text "s"}-operator. *}
definition rec_ci_s :: "abc_inst list"
where
"rec_ci_s \<equiv> (addition 0 1 2 [+] [Inc 1])"
-text {*
- The compilation of @{text "id i j"}-operator
-*}
-
+text {* The compilation of @{text "id i j"}-operator *}
fun rec_ci_id :: "nat \<Rightarrow> nat \<Rightarrow> abc_inst list"
where
"rec_ci_id i j = addition j i (i + 1)"
@@ -73,8 +63,7 @@
fun mv_boxes :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list"
where
"mv_boxes ab bb 0 = []" |
- "mv_boxes ab bb (Suc n) = mv_boxes ab bb n [+] mv_box (ab + n)
- (bb + n)"
+ "mv_boxes ab bb (Suc n) = mv_boxes ab bb n [+] mv_box (ab + n) (bb + n)"
fun empty_boxes :: "nat \<Rightarrow> abc_inst list"
where
@@ -94,7 +83,7 @@
The compiler of recursive functions, where @{text "rec_ci recf"} return
@{text "(ap, arity, fp)"}, where @{text "ap"} is the Abacus program, @{text "arity"} is the
arity of the recursive function @{text "recf"},
-@{text "fp"} is the amount of memory which is going to be
+ @{text "fp"} is the amount of memory which is going to be
used by @{text "ap"} for its execution.
*}
@@ -127,11 +116,10 @@
(let (fprog, fpara, fn) = rec_ci f in
let len = length (fprog) in
(fprog @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),
- Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn) )"
+ Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn))"
by pat_completeness auto
termination
proof
-term size
show "wf (measure size)" by auto
next
fix n f gs x
@@ -154,8 +142,6 @@
mv_boxes.simps[simp del] abc_append.simps[simp del]
mv_box.simps[simp del] addition.simps[simp del]
-thm rec_calc_rel.induct
-
declare abc_steps_l.simps[simp del] abc_fetch.simps[simp del]
abc_step_l.simps[simp del]
@@ -797,12 +783,6 @@
apply(arith)
done
-(*
-lemma pr_para_ge_suc0: "rec_calc_rel (Pr n f g) lm xs \<Longrightarrow> 0 < n"
-apply(erule calc_pr_reverse, simp, simp)
-done
-*)
-
lemma ci_pr_para_eq: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md)
\<Longrightarrow> rs_pos = Suc n"
apply(simp add: rec_ci.simps)
@@ -1443,7 +1423,6 @@
\<exists> stp. (\<lambda> (as, lm). as = 3 \<and>
mv_box_inv (as, lm) m n initlm)
(abc_steps_l (0::nat, initlm) (mv_box m n) stp)"
-thm halt_lemma2
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)"
@@ -1539,12 +1518,6 @@
apply(arith)
done
-thm nth_replicate
-(*
-lemma exp_nth[simp]: "n < m \<Longrightarrow> a\<up>m ! n = a"
-apply(sim)
-done
-*)
lemma [simp]: "length lm = n \<and> rs_pos = n \<and> 0 < n \<Longrightarrow>
lm[n - Suc 0 := 0::nat] = butlast lm @ [0]"
apply(auto)
@@ -1938,8 +1911,6 @@
done
qed
-thm rec_calc_rel.induct
-
lemma eq_switch: "x = y \<Longrightarrow> y = x"
by simp
@@ -1956,14 +1927,7 @@
"rec_ci (Mn n f) = (aprog, rs_pos, a_md) \<Longrightarrow> rs_pos = n"
apply(case_tac "rec_ci f", simp add: rec_ci.simps)
done
-(*
-lemma [simp]: "\<lbrakk>rec_ci f = (a, aa, ba); rec_ci (Mn n f) = (aprog, rs_pos, a_md); rec_calc_rel (Mn n f) lm rs\<rbrakk> \<Longrightarrow> aa = Suc rs_pos"
-apply(rule_tac calc_mn_reverse, simp)
-apply(insert para_pattern [of f a aa ba "lm @ [rs]" 0], simp)
-apply(subgoal_tac "rs_pos = length lm", simp)
-apply(drule_tac ci_mn_para_eq, simp)
-done
-*)
+
lemma [simp]: "rec_ci f = (a, aa, ba) \<Longrightarrow> aa < ba"
apply(simp add: ci_ad_ge_paras)
done
@@ -2057,7 +2021,6 @@
((nat \<times> nat list) \<times> nat \<times> nat)) set"
where "mn_LE \<equiv> (inv_image lex_triple mn_measure)"
-thm halt_lemma2
lemma wf_mn_le[intro]: "wf mn_LE"
by(auto intro:wf_inv_image wf_lex_triple simp: mn_LE_def)
@@ -2078,7 +2041,6 @@
apply(erule_tac rec_ci_not_null)
done
-thm rec_ci.simps
lemma [simp]:
"\<lbrakk>rec_ci f = (a, aa, ba);
rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk>
@@ -2189,14 +2151,6 @@
Suc (a_md - Suc (Suc rs_pos)) = a_md - Suc rs_pos"
by arith
-term rec_ci
-(*
-lemma [simp]: "\<lbrakk>rec_ci (Mn n f) = (aprog, rs_pos, a_md); rec_calc_rel (Mn n f) lm rs\<rbrakk> \<Longrightarrow> Suc rs_pos < a_md"
-apply(case_tac "rec_ci f")
-apply(subgoal_tac "c > b \<and> b = Suc rs_pos \<and> a_md \<ge> c")
-apply(arith, auto)
-done
-*)
lemma mn_ind_step:
assumes ind:
"\<And>aprog a_md rs_pos rs suf_lm lm.
@@ -2212,7 +2166,6 @@
"aa = Suc rs_pos"
shows "\<exists>stp. abc_steps_l (0, lm @ x # 0\<up>(a_md - Suc rs_pos) @ suf_lm)
aprog stp = (0, lm @ Suc x # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
-thm abc_add_exc1
proof -
have k1:
"\<exists> stp. abc_steps_l (0, lm @ x # 0\<up>(a_md - Suc (rs_pos)) @ suf_lm)
@@ -2349,7 +2302,6 @@
from h and ind have k1:
"\<exists>stp. abc_steps_l (0, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)
aprog stp = (length a, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
- thm mn_calc_f
apply(insert mn_calc_f[of f a aa ba n aprog
rs_pos a_md lm rs 0 suf_lm], simp)
apply(subgoal_tac "aa = Suc n", simp add: exponent_cons_iff)
@@ -2397,7 +2349,6 @@
hence k1:
"\<exists>stp. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm) aprog
stp = (0, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
- thm mn_ind_steps
apply(auto intro: mn_ind_steps ind)
done
from h have k2:
@@ -2502,8 +2453,6 @@
apply(rule_tac x = "lm ! m" in exI, simp)
done
-thm addition.simps
-
lemma [simp]: "abc_fetch 0 (addition m n p) = Some (Dec m 4)"
by(simp add: abc_fetch.simps addition.simps)
@@ -2845,7 +2794,6 @@
(\<lambda>(ap, pos, n). length ap) (rec_ci a) + (3 + 3 * length list),
lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm)"
apply(simp add: cn_merge_gs_tl_app)
- thm abc_append_exc2
apply(rule_tac as =
"(\<Sum>(ap, pos, n)\<leftarrow>map rec_ci list. length ap) + 3 * length list"
and bm = "lm @ 0\<up>(pstr - n) @ butlast ys @
@@ -3036,22 +2984,6 @@
"lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4"], simp)
done
qed
-(*
-lemma [simp]: "\<lbrakk>Suc n \<le> aa - ba;
- ba < aa;
- length lm2 = aa - Suc (ba + n)\<rbrakk>
- \<Longrightarrow> ((0::nat) # lm2 @ 0\<up>n @ last lm3 # lm4) ! (aa - ba)
- = last lm3"
-proof -
- assume h: "Suc n \<le> aa - ba"
- and g: " ba < aa" "length lm2 = aa - Suc (ba + n)"
- from h and g have k: "aa - ba = Suc (length lm2 + n)"
- by arith
- thus "((0::nat) # lm2 @ 0\<up>n @ last lm3 # lm4) ! (aa - ba) = last lm3"
- apply(simp, simp add: nth_append)
- done
-qed
-*)
lemma [simp]: "\<lbrakk>Suc n \<le> aa - ba; ba < aa; length lm1 = ba;
length lm2 = aa - Suc (ba + n); length lm3 = Suc n\<rbrakk>
@@ -3152,7 +3084,6 @@
0\<up>(a_md - pstr - length ys) @ suf_lm)
(mv_boxes 0 (pstr + Suc (length ys)) n) stp
= (3 * n, 0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
-thm mv_boxes_ex
apply(insert mv_boxes_ex[of n "pstr + Suc (length ys)" 0 "[]" "lm"
"0\<up>(pstr - n) @ ys @ [0]" "0\<up>(a_md - pstr - length ys - n - Suc 0) @ suf_lm"], simp)
apply(erule_tac exE, rule_tac x = stp in exI,
@@ -3361,7 +3292,6 @@
\<exists>stp. abc_steps_l (0, 0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @
suf_lm) (mv_boxes pstr 0 (length ys)) stp =
(3 * length ys, ys @ 0\<up>pstr @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
-thm mv_boxes_ex2
apply(insert mv_boxes_ex2[of "length ys" "pstr" 0 "[]"
"0\<up>(pstr - length ys)" "ys"
"0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm"],
@@ -3431,7 +3361,6 @@
"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))))"
- thm rec_ci.simps
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) +
@@ -3473,8 +3402,6 @@
qed
qed
-thm rec_ci.simps
-
lemma calc_f_prog_ex:
"\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md);
rec_ci f = (a, aa, ba);
@@ -3647,7 +3574,6 @@
ys @ 0\<up>(pstr - length ys) @ rs # 0\<up>length ys @ lm @
0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)"
proof -
- thm rec_ci.simps
from h and pdef have k1:
"\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and>
length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) +
@@ -3927,7 +3853,6 @@
lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)
aprog stp = (ss + 3 * n, lm @ rs # 0\<up>(a_md - Suc n) @ suf_lm)"
proof -
- thm rec_ci.simps
from h and pdef and starts have k1:
"\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and>
bp = mv_boxes (pstr + Suc (length gs)) (0::nat) n"
@@ -3996,13 +3921,11 @@
apply(rule_tac a = a and aa = b and ba = c in cn_calc_gs)
apply(rule_tac ind, auto)
done
- thm rec_ci.simps
from g have k2:
"\<exists> stp. abc_steps_l (?gs_len + 3 * length gs, lm @
0\<up>(?pstr - n) @ ys @ 0\<up>(a_md - ?pstr - length ys) @ suf_lm) aprog stp =
(?gs_len + 3 * length gs + 3 * n, 0\<up>?pstr @ ys @ 0 # lm @
0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm)"
- thm save_paras
apply(erule_tac ba = c in save_paras, auto intro: ci_cn_para_eq)
done
from g have k3:
@@ -4022,7 +3945,6 @@
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)
done
-thm rec_ci.simps
from g h have k5:
"\<exists> stp. abc_steps_l (?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)
@@ -4207,7 +4129,6 @@
"p = ap [+] bp [+] cp"
have "\<exists> stp. (abc_steps_l (0, am) p stp) = (length ap, lm)"
using h
- thm abc_add_exc1
apply(simp add: abc_append.simps)
apply(rule_tac abc_add_exc1, auto)
done
@@ -4267,7 +4188,6 @@
"rec_ci rf = (aprog, rs_pos, a_md)"
"rec_ci f = (aprog', rs_pos', a_md')"
"\<forall>y. \<exists>rs. rec_calc_rel f (lm @ [y]) rs \<and> rs \<noteq> 0" "length lm = n"
- thm mn_ind_step
have "\<exists>stpa \<ge> stp. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm) aprog stpa
= (0, lm @ stp # 0\<up>(a_md - Suc rs_pos) @ suf_lm)"
proof(induct stp, auto)
@@ -4441,7 +4361,6 @@
apply(rule_tac A = "set (take i gs)" in subsetD,
simp add: set_take_subset, simp)
done
- thm cn_merge_gs.simps
from this obtain stpa where g2:
"abc_steps_l (0, lm @ 0\<up>(a_md - n) @ suflm)
(cn_merge_gs (map rec_ci ?ggs) ?pstr) stpa =
@@ -4510,7 +4429,6 @@
apply(rule_tac Max_ge, simp, simp)
apply(rule_tac disjI2)
using h2
- thm rev_image_eqI
apply(rule_tac x = "gs!i" in rev_image_eqI, simp, simp)
done
next
@@ -4770,8 +4688,6 @@
assume h: "rec_calc_rel recf args r"
"abc_steps_l (0, args) ap stp = (length ap, lm')"
"abc_list_crsp lm' (args @ r # 0\<up>m)"
- thm abc_append_exc2
- thm abc_lm_s.simps
have "\<exists>stp. abc_steps_l (0, args) (ap [+]
(dummy_abc (length args))) stp = (length ap + 3,
abc_lm_s lm' (length args) (abc_lm_v lm' (length args)))"