--- a/thys/Abacus.thy Mon Feb 11 00:08:54 2013 +0000
+++ b/thys/Abacus.thy Mon Feb 11 08:31:48 2013 +0000
@@ -227,7 +227,6 @@
@{text "start_of layout n"} looks out the starting state of @{text "n"}-th
TM in the finall TM.
*}
-thm listsum_def
fun start_of :: "nat list \<Rightarrow> nat \<Rightarrow> nat"
where
@@ -877,7 +876,6 @@
from a b have c: "steps0 (s + off, l, r) (A @ shift B off) stp = (s'' + off, l'', r'')"
by(erule_tac ind, simp)
from c b h a k assms show "?case"
- thm tm_append_second_step_eq
apply(simp add: step_red) by(rule tm_append_second_step_eq, simp_all)
qed
@@ -902,7 +900,6 @@
and even: "length A mod 2 = 0"
shows "steps (Suc off, l, r) (A @ shift B off, 0) stp = (0, l', r')"
proof -
- thm before_final
have "\<exists>n. \<not> is_final (steps0 (1, l, r) B n) \<and> steps0 (1, l, r) B (Suc n) = (0, l', r')"
using exec by(rule_tac before_final, simp)
then obtain n where a:
@@ -1508,7 +1505,6 @@
and P: "P = (\<lambda> ((s, l, r), n). s = Suc (2 * n))"
and Q: "Q = (\<lambda> ((s, l, r), n). findnth_inv ly n (as, lm) (s, l, r) ires)"
shows "\<exists> stp. P (f stp) \<and> Q (f stp)"
-thm halt_lemma2
proof(rule_tac LE = findnth_LE in halt_lemma2)
show "wf findnth_LE" by(intro wf_findnth_LE)
next
@@ -2101,7 +2097,6 @@
shows "\<exists> stp k. steps (Suc 0, l, r) (findnth n @ shift tinc_b (2 * n), 0) stp
= (2*n + 10, Bk # Bk # ires, <lma> @ Bk\<up>k) \<and> stp > 0"
proof -
- thm tm_append_steps
have "\<exists> stp l' r'. steps (Suc 0, l, r) (findnth n, 0) stp = (Suc (2 * n), l', r')
\<and> inv_locate_a (as, lm) (n, l', r') ires"
using assms
@@ -2349,7 +2344,6 @@
lemma start_of_less_2:
"start_of ly e \<le> start_of ly (Suc e)"
-thm take_Suc
apply(case_tac "e < length ly")
apply(auto simp: start_of.simps take_Suc take_Suc_conv_app_nth)
done
@@ -3234,7 +3228,6 @@
from this obtain stpa la ra where a:
"steps (start_of ly as + 2 * n, l, r) (?P, ?off) stpa = (Suc (start_of ly as) + 2*n, la, ra)
\<and> inv_locate_b (as, lm) (n, la, ra) ires" by blast
- term dec_inv_1
have "\<exists> stp lb rb. steps (Suc (start_of ly as) + 2 * n, la, ra) (?P, ?off) stp = (start_of ly e, lb, rb)
\<and> dec_inv_1 ly n e (as, lm) (start_of ly e, lb, rb) ires"
using assms a
@@ -3714,7 +3707,6 @@
text{*The tp @ [(Nop, 0), (Nop, 0)] is nomoral turing machines, so we can use Hoare_plus when composing with Mop machine*}
-thm layout_of.simps
lemma layout_id_cons: "layout_of (ap @ [p]) = layout_of ap @ [length_of p]"
apply(simp add: layout_of.simps)
done
@@ -3722,11 +3714,6 @@
lemma [simp]: "length (layout_of xs) = length xs"
by(simp add: layout_of.simps)
-thm tms_of.simps
-term ci
-thm tms_of.simps
-thm tpairs_of.simps
-
lemma [simp]:
"map (start_of (layout_of xs @ [length_of x])) [0..<length xs] = (map (start_of (layout_of xs)) [0..<length xs])"
apply(auto)
@@ -4495,7 +4482,6 @@
done
declare mopup_inv.simps[simp del]
-term mopup_inv
lemma [simp]:
"\<lbrakk>0 < q; q \<le> n\<rbrakk> \<Longrightarrow>
@@ -4534,7 +4520,6 @@
apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto)
done
then have "mopup_inv (a, b, c) lm n ires"
- thm mopup_inv_steps
using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na]
apply(simp)
done
@@ -4641,7 +4626,6 @@
then have b: "steps (Suc 0 + off, Bk # Bk # ires, <am> @ Bk \<up> k) (tp @ shift (mopup n) off, 0) stpb
= (0, Bk\<up>i @ Bk # Bk # ires, Oc # Oc\<up> rs @ Bk\<up>j)"
using assms wf_mopup
- thm tm_append_second_halt_eq
apply(drule_tac tm_append_second_halt_eq, auto)
done
from a b show "?thesis"
--- a/thys/Rec_Def.thy Mon Feb 11 00:08:54 2013 +0000
+++ b/thys/Rec_Def.thy Mon Feb 11 08:31:48 2013 +0000
@@ -2,42 +2,26 @@
imports Main
begin
-section {*
- Recursive functions
-*}
-
-text {*
- Datatype of recursive operators.
-*}
+section {* Recursive functions *}
datatype recf =
- -- {* The zero function, which always resturns @{text "0"} as result. *}
- z |
- -- {* The successor function, which increments its arguments. *}
- s |
- -- {*
- The projection function, where @{text "id i j"} returns the @{text "j"}-th
- argment out of the @{text "i"} arguments.
- *}
+ z | s |
+ -- {* The projection function, where @{text "id i j"} returns the @{text "j"}-th
+ argment out of the @{text "i"} arguments. *}
id nat nat |
- -- {*
- The compostion operator, where "@{text "Cn n f [g1; g2; \<dots> ;gm]"}
+ -- {* The compostion operator, where "@{text "Cn n f [g1; g2; \<dots> ;gm]"}
computes @{text "f (g1(x1, x2, \<dots>, xn), g2(x1, x2, \<dots>, xn), \<dots> ,
- gm(x1, x2, \<dots> , xn))"} for input argments @{text "x1, \<dots>, xn"}.
- *}
+ gm(x1, x2, \<dots> , xn))"} for input argments @{text "x1, \<dots>, xn"}. *}
Cn nat recf "recf list" |
--- {*
- The primitive resursive operator, where @{text "Pr n f g"} computes:
+ -- {* The primitive resursive operator, where @{text "Pr n f g"} computes:
@{text "Pr n f g (x1, x2, \<dots>, xn-1, 0) = f(x1, \<dots>, xn-1)"}
and @{text "Pr n f g (x1, x2, \<dots>, xn-1, k') = g(x1, x2, \<dots>, xn-1, k,
- Pr n f g (x1, \<dots>, xn-1, k))"}.
+ Pr n f g (x1, \<dots>, xn-1, k))"}.
*}
Pr nat recf recf |
--- {*
- The minimization operator, where @{text "Mn n f (x1, x2, \<dots> , xn)"}
+ -- {* The minimization operator, where @{text "Mn n f (x1, x2, \<dots> , xn)"}
computes the first i such that @{text "f (x1, \<dots>, xn, i) = 0"} and for all
- @{text "j"}, @{text "f (x1, x2, \<dots>, xn, j) > 0"}.
- *}
+ @{text "j"}, @{text "f (x1, x2, \<dots>, xn, j) > 0"}. *}
Mn nat recf
text {*
@@ -72,8 +56,7 @@
\<forall> i < r. (\<exists> ri. rec_calc_rel f (args@[i]) ri \<and> ri \<noteq> 0)\<rbrakk>
\<Longrightarrow> rec_calc_rel (Mn n f) args r"
-inductive_cases calc_pr_reverse:
- "rec_calc_rel (Pr n f g) (lm) rSucy"
+inductive_cases calc_pr_reverse: "rec_calc_rel (Pr n f g) (lm) rSucy"
inductive_cases calc_z_reverse: "rec_calc_rel z lm x"
--- 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)))"
--- a/thys/UF.thy Mon Feb 11 00:08:54 2013 +0000
+++ b/thys/UF.thy Mon Feb 11 08:31:48 2013 +0000
@@ -14,10 +14,6 @@
subsection {* The construction of component functions *}
text {*
- This section constructs a set of component functions used to construct @{text "rec_F"}.
- *}
-
-text {*
The recursive function used to do arithmatic addition.
*}
definition rec_add :: "recf"
@@ -2428,7 +2424,6 @@
Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 2) [recf.id 3 0]],
Cn 3 rec_eq [recf.id 3 2, Cn 3 (constn 3) [recf.id 3 0]],
Cn 3 rec_less [Cn 3 (constn 3) [recf.id 3 0], recf.id 3 2]]"
- thm embranch_lemma
have k1: "rec_exec (rec_embranch (zip ?rgs ?rrs)) [p, r, a]
= Embranch (zip (map rec_exec ?rgs) (map (\<lambda>r args. 0 < rec_exec r args) ?rrs)) [p, r, a]"
apply(rule_tac embranch_lemma )
@@ -2644,8 +2639,6 @@
where
"rght c = lo c (Pi 2)"
-thm Prime.simps
-
fun inpt :: "nat \<Rightarrow> nat list \<Rightarrow> nat"
where
"inpt m xs = trpl 0 1 (strt xs)"
@@ -3103,7 +3096,6 @@
apply(rule_tac calc_pr_zero, simp)
using ind1[of "rec_exec (Pr n f g) (butlast xs @ [0])"]
apply(simp add: rec_exec.simps, simp, simp, simp)
- thm calc_pr_ind
apply(rule_tac rk = "rec_exec (Pr n f g)
(butlast xs@[last xs - Suc 0])" in calc_pr_ind)
using ind2[of "rec_exec (Pr n f g)
@@ -3540,7 +3532,6 @@
subsection {* Relating interperter functions to the execution of TMs *}
lemma [simp]: "bl2wc [] = 0" by(simp add: bl2wc.simps bl2nat.simps)
-term trpl
lemma [simp]: "\<lbrakk>fetch tp 0 b = (nact, ns)\<rbrakk> \<Longrightarrow> action_map nact = 4"
apply(simp add: fetch.simps)
@@ -3586,7 +3577,6 @@
apply(simp)
done
-term set_of
lemma prime_coprime: "\<lbrakk>Prime x; Prime y; x\<noteq>y\<rbrakk> \<Longrightarrow> coprime x y"
proof(simp only: Prime.simps coprime_nat, auto simp: dvd_def,
rule_tac classical, simp)
--- a/thys/UTM.thy Mon Feb 11 00:08:54 2013 +0000
+++ b/thys/UTM.thy Mon Feb 11 08:31:48 2013 +0000
@@ -5,17 +5,27 @@
section {* Wang coding of input arguments *}
text {*
- The direct compilation of the universal function @{text "rec_F"} can not give us UTM, because @{text "rec_F"} is of arity 2,
- where the first argument represents the Godel coding of the TM being simulated and the second argument represents the right number (in Wang's coding) of the TM tape.
- (Notice, left number is always @{text "0"} at the very beginning). However, UTM needs to simulate the execution of any TM which may
- very well take many input arguments. Therefore, a initialization TM needs to run before the TM compiled from @{text "rec_F"}, and the sequential
- composition of these two TMs will give rise to the UTM we are seeking. The purpose of this initialization TM is to transform the multiple
- input arguments of the TM being simulated into Wang's coding, so that it can be consumed by the TM compiled from @{text "rec_F"} as the second
- argument.
-
- However, this initialization TM (named @{text "t_wcode"}) can not be constructed by compiling from any resurve function, because every recursive
- function takes a fixed number of input arguments, while @{text "t_wcode"} needs to take varying number of arguments and tranform them into
- Wang's coding. Therefore, this section give a direct construction of @{text "t_wcode"} with just some parts being obtained from recursive functions.
+ The direct compilation of the universal function @{text "rec_F"} can
+ not give us UTM, because @{text "rec_F"} is of arity 2, where the
+ first argument represents the Godel coding of the TM being simulated
+ and the second argument represents the right number (in Wang's
+ coding) of the TM tape. (Notice, left number is always @{text "0"}
+ at the very beginning). However, UTM needs to simulate the execution
+ of any TM which may very well take many input arguments. Therefore,
+ a initialization TM needs to run before the TM compiled from @{text
+ "rec_F"}, and the sequential composition of these two TMs will give
+ rise to the UTM we are seeking. The purpose of this initialization
+ TM is to transform the multiple input arguments of the TM being
+ simulated into Wang's coding, so that it can be consumed by the TM
+ compiled from @{text "rec_F"} as the second argument.
+
+ However, this initialization TM (named @{text "t_wcode"}) can not be
+ constructed by compiling from any resurve function, because every
+ recursive function takes a fixed number of input arguments, while
+ @{text "t_wcode"} needs to take varying number of arguments and
+ tranform them into Wang's coding. Therefore, this section give a
+ direct construction of @{text "t_wcode"} with just some parts being
+ obtained from recursive functions.
\newlength{\basewidth}
\settowidth{\basewidth}{xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx}
@@ -71,10 +81,22 @@
\caption{The output of TM $prepare$} \label{prepare_output}
\end{figure}
-As shown in Figure \ref{prepare_input}, the input of $prepare$ is the same as the the input
-of UTM, where $m$ is the Godel coding of the TM being interpreted and $a_1$ through $a_n$ are the $n$ input arguments of the TM under interpretation. The purpose of $purpose$ is to transform this initial tape layout to the one shown in Figure \ref{prepare_output},
-which is convenient for the generation of Wang's codding of $a_1, \ldots, a_n$. The coding procedure starts from $a_n$ and ends after $a_1$ is encoded. The coding result is stored in an accumulator at the end of the tape (initially represented by the $1$ two blanks right to $a_n$ in Figure \ref{prepare_output}). In Figure \ref{prepare_output}, arguments $a_1, \ldots, a_n$ are separated by two blanks on both ends with the rest so that movement conditions can be implemented conveniently in subsequent TMs, because, by convention,
-two consecutive blanks are usually used to signal the end or start of a large chunk of data. The diagram of $prepare$ is given in Figure \ref{prepare_diag}.
+As shown in Figure \ref{prepare_input}, the input of $prepare$ is the
+same as the the input of UTM, where $m$ is the Godel coding of the TM
+being interpreted and $a_1$ through $a_n$ are the $n$ input arguments
+of the TM under interpretation. The purpose of $purpose$ is to
+transform this initial tape layout to the one shown in Figure
+\ref{prepare_output}, which is convenient for the generation of Wang's
+codding of $a_1, \ldots, a_n$. The coding procedure starts from $a_n$
+and ends after $a_1$ is encoded. The coding result is stored in an
+accumulator at the end of the tape (initially represented by the $1$
+two blanks right to $a_n$ in Figure \ref{prepare_output}). In Figure
+\ref{prepare_output}, arguments $a_1, \ldots, a_n$ are separated by
+two blanks on both ends with the rest so that movement conditions can
+be implemented conveniently in subsequent TMs, because, by convention,
+two consecutive blanks are usually used to signal the end or start of
+a large chunk of data. The diagram of $prepare$ is given in Figure
+\ref{prepare_diag}.
\begin{figure}[h!]
@@ -840,7 +862,6 @@
lemma wf_wcode_double_case_le[intro]: "wf wcode_double_case_le"
by(auto intro:wf_inv_image simp: wcode_double_case_le_def )
-term fetch
lemma [simp]: "fetch t_wcode_main (Suc 0) Bk = (L, Suc 0)"
apply(simp add: t_wcode_main_def t_wcode_main_first_part_def
@@ -1326,7 +1347,7 @@
(Suc (length ap div 2), l', r')"
proof -
have "\<exists> stp. \<not> is_final (steps0 (1, l, r) ap stp) \<and> (steps0 (1, l, r) ap (Suc stp) = (0, l', r'))"
- thm before_final using exec
+ using exec
by(erule_tac before_final)
then obtain stpa where a:
"\<not> is_final (steps0 (1, l, r) ap stpa) \<and> (steps0 (1, l, r) ap (Suc stpa) = (0, l', r'))" ..
@@ -1377,7 +1398,6 @@
hence "\<exists> stp. steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n))
(adjust t_twice_compile) stp
= (Suc (length t_twice_compile div 2), Bk\<up>(ln) @ Bk # Bk # ires, Oc\<up>(Suc (2 * rs)) @ Bk\<up>(rn))"
- thm adjust_halt_eq
apply(rule_tac stp = stp in adjust_halt_eq)
apply(simp add: t_twice_compile_def, auto)
done
@@ -3310,15 +3330,6 @@
apply(simp add:tm_wf.simps t_wcode_prepare_def)
done
-(*
-lemma t_correct_termi: "t_correct tp \<Longrightarrow>
- list_all (\<lambda>(acn, st). (st \<le> Suc (length tp div 2))) (change_termi_state tp)"
-apply(auto simp: t_correct.simps List.list_all_length)
-apply(erule_tac x = n in allE, simp)
-apply(case_tac "tp!n", auto simp: change_termi_state.simps split: if_splits)
-done
-*)
-
lemma t_correct_shift:
"list_all (\<lambda>(acn, st). (st \<le> y)) tp \<Longrightarrow>
list_all (\<lambda>(acn, st). (st \<le> y + off)) (shift tp off) "
@@ -3326,20 +3337,6 @@
apply(erule_tac x = n in allE, simp add: length_shift)
apply(case_tac "tp!n", auto simp: shift.simps)
done
-(*
-lemma [intro]:
- "t_correct (tm_of abc_twice @ tMp (Suc 0)
- (start_of twice_ly (length abc_twice) - Suc 0))"
-apply(rule_tac t_compiled_correct, simp_all)
-apply(simp add: twice_ly_def)
-done
-
-lemma [intro]: "t_correct (tm_of abc_fourtimes @ tMp (Suc 0)
- (start_of fourtimes_ly (length abc_fourtimes) - Suc 0))"
-apply(rule_tac t_compiled_correct, simp_all)
-apply(simp add: fourtimes_ly_def)
-done
-*)
lemma [intro]: "(28 + (length t_twice_compile + length t_fourtimes_compile)) mod 2 = 0"
apply(auto simp: t_twice_compile_def t_fourtimes_compile_def)
@@ -3664,7 +3661,6 @@
apply(simp only: fetch.simps t_wcode_adjust_def nth_of.simps numeral_5_eq_5, auto)
done
-thm numeral_6_eq_6
lemma [simp]: "fetch t_wcode_adjust 6 Oc = (R, 7)"
apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_6_eq_6)
done
@@ -4665,112 +4661,6 @@
where
"UTM_pre = t_wcode |+| t_utm"
-(*
-lemma F_abc_halt_eq:
- "\<lbrakk>Turing.t_correct tp;
- length lm = k;
- steps (Suc 0, Bk\<up>(l), <lm>) tp stp = (0, Bk\<up>(m), Oc\<up>(rs)@Bk\<up>(n));
- rs > 0\<rbrakk>
- \<Longrightarrow> \<exists> stp m. abc_steps_l (0, [code tp, bl2wc (<lm>)]) (F_aprog) stp =
- (length (F_aprog), code tp # bl2wc (<lm>) # (rs - 1) # 0\<up>(m))"
-apply(drule_tac F_t_halt_eq, simp, simp, simp)
-apply(case_tac "rec_ci rec_F")
-apply(frule_tac abc_append_dummy_complie, simp, simp, erule_tac exE,
- erule_tac exE)
-apply(rule_tac x = stp in exI, rule_tac x = m in exI)
-apply(simp add: F_aprog_def dummy_abc_def)
-done
-
-lemma F_abc_utm_halt_eq:
- "\<lbrakk>rs > 0;
- abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog stp =
- (length F_aprog, code tp # bl2wc (<lm>) # (rs - 1) # 0\<up>(m))\<rbrakk>
- \<Longrightarrow> \<exists>stp m n.(steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp =
- (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n)))"
- thm abacus_turing_eq_halt
- using abacus_turing_eq_halt
- [of "layout_of F_aprog" "F_aprog" "F_tprog" "length (F_aprog)"
- "[code tp, bl2wc (<lm>)]" stp "code tp # bl2wc (<lm>) # (rs - 1) # 0\<up>(m)" "Suc (Suc 0)"
- "start_of (layout_of (F_aprog)) (length (F_aprog))" "[]" 0]
-apply(simp add: F_tprog_def t_utm_def abc_lm_v.simps nth_append)
-apply(erule_tac exE)+
-apply(rule_tac x = stpa in exI, rule_tac x = "Suc (Suc ma)" in exI,
- rule_tac x = l in exI, simp add: exp_ind)
-done
-
-declare tape_of_nl_abv_cons[simp del]
-
-lemma t_utm_halt_eq':
- "\<lbrakk>Turing.t_correct tp;
- 0 < rs;
- steps (Suc 0, Bk\<up>(l), <lm::nat list>) tp stp = (0, Bk\<up>(m), Oc\<up>(rs)@Bk\<up>(n))\<rbrakk>
- \<Longrightarrow> \<exists>stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stp =
- (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))"
-apply(drule_tac l = l in F_abc_halt_eq, simp, simp, simp)
-apply(erule_tac exE, erule_tac exE)
-apply(rule_tac F_abc_utm_halt_eq, simp_all)
-done
-*)
-(*
-lemma [simp]: "tinres xs (xs @ Bk\<up>(i))"
-apply(auto simp: tinres_def)
-done
-
-lemma [elim]: "\<lbrakk>rs > 0; Oc\<up>(rs) @ Bk\<up>(na) = c @ Bk\<up>(n)\<rbrakk>
- \<Longrightarrow> \<exists>n. c = Oc\<up>(rs) @ Bk\<up>(n)"
-apply(case_tac "na > n")
-apply(subgoal_tac "\<exists> d. na = d + n", auto simp: exp_add)
-apply(rule_tac x = "na - n" in exI, simp)
-apply(subgoal_tac "\<exists> d. n = d + na", auto simp: exp_add)
-apply(case_tac rs, simp_all add: exp_ind, case_tac d,
- simp_all add: exp_ind)
-apply(rule_tac x = "n - na" in exI, simp)
-done
-*)
-(*
-lemma t_utm_halt_eq'':
- "\<lbrakk>Turing.t_correct tp;
- 0 < rs;
- steps (Suc 0, Bk\<up>(l), <lm::nat list>) tp stp = (0, Bk\<up>(m), Oc\<up>(rs)@Bk\<up>(n))\<rbrakk>
- \<Longrightarrow> \<exists>stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stp =
- (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))"
-apply(drule_tac t_utm_halt_eq', simp_all)
-apply(erule_tac exE)+
-proof -
- fix stpa ma na
- assume "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stpa = (0, Bk\<up>(ma), Oc\<up>(rs) @ Bk\<up>(na))"
- and gr: "rs > 0"
- thus "\<exists>stp m n. steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stp = (0, Bk\<up>(m), Oc\<up>(rs) @ Bk\<up>(n))"
- apply(rule_tac x = stpa in exI, rule_tac x = ma in exI, simp)
- proof(case_tac "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stpa", simp)
- fix a b c
- assume "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]>) t_utm stpa = (0, Bk\<up>(ma), Oc\<up>(rs) @ Bk\<up>(na))"
- "steps (Suc 0, [Bk, Bk], <[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)) t_utm stpa = (a, b, c)"
- thus " a = 0 \<and> b = Bk\<up>(ma) \<and> (\<exists>n. c = Oc\<up>(rs) @ Bk\<up>(n))"
- using tinres_steps2[of "<[code tp, bl2wc (<lm>)]>" "<[code tp, bl2wc (<lm>)]> @ Bk\<up>(i)"
- "Suc 0" " [Bk, Bk]" t_utm stpa 0 "Bk\<up>(ma)" "Oc\<up>(rs) @ Bk\<up>(na)" a b c]
- apply(simp)
- using gr
- apply(simp only: tinres_def, auto)
- apply(rule_tac x = "na + n" in exI, simp add: exp_add)
- done
- qed
-qed
-
-lemma [simp]: "tinres [Bk, Bk] [Bk]"
-apply(auto simp: tinres_def)
-done
-
-lemma [elim]: "Bk\<up>(ma) = b @ Bk\<up>(n) \<Longrightarrow> \<exists>m. b = Bk\<up>(m)"
-apply(subgoal_tac "ma = length b + n")
-apply(rule_tac x = "ma - n" in exI, simp add: exp_add)
-apply(drule_tac length_equal)
-apply(simp)
-done
-*)
-
-
-
lemma tinres_step1:
"\<lbrakk>tinres l l'; step (ss, l, r) (t, 0) = (sa, la, ra);
step (ss, l', r) (t, 0) = (sb, lb, rb)\<rbrakk>
@@ -5083,15 +4973,6 @@
apply(rule_tac nonstop_t_uhalt_eq, simp_all)
done
-(*
-lemma [simp]:
- "\<forall>j<Suc k. Ex (rec_calc_rel (get_fstn_args (Suc k) (Suc k) ! j)
- (code tp # lm))"
-apply(auto simp: get_fstn_args_nth)
-apply(rule_tac x = "(code tp # lm) ! j" in exI)
-apply(rule_tac calc_id, simp_all)
-done
-*)
declare ci_cn_para_eq[simp]
lemma F_aprog_uhalt:
@@ -5180,7 +5061,6 @@
\<Longrightarrow> \<forall> stp. case abc_steps_l (0, [code tp, bl2wc (<lm>)]) F_aprog
stp of (ss, e) \<Rightarrow> ss < length F_aprog"
apply(case_tac "rec_ci rec_F", simp add: F_aprog_def)
-thm uabc_uhalt'
apply(drule_tac ap = a and pos = b and md = c in uabc_uhalt', simp_all)
proof -
fix a b c