--- a/thys/uncomputable.thy Tue Jan 22 14:46:02 2013 +0000
+++ b/thys/uncomputable.thy Wed Jan 23 08:01:35 2013 +0100
@@ -9,6 +9,24 @@
imports Main turing_hoare
begin
+declare tm_comp.simps [simp del]
+declare adjust.simps[simp del]
+declare shift.simps[simp del]
+declare tm_wf.simps[simp del]
+declare step.simps[simp del]
+declare steps.simps[simp del]
+
+
+lemma numeral:
+ shows "1 = Suc 0"
+ and "2 = Suc 1"
+ and "3 = Suc 2"
+ and "4 = Suc 3"
+ and "5 = Suc 4"
+ and "6 = Suc 5" by arith+
+
+
+
text {*
The {\em Copying} TM, which duplicates its input.
*}
@@ -51,8 +69,6 @@
declare inv_init.simps[simp del]
-lemma numeral_4_eq_4: "4 = Suc 3"
-by arith
lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow>
\<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"
@@ -62,9 +78,9 @@
lemma inv_init_step:
"\<lbrakk>inv_init x cf; x > 0\<rbrakk>
\<Longrightarrow> inv_init x (step cf (tcopy_init, 0))"
+unfolding tcopy_init_def
apply(case_tac cf)
-apply(auto simp: inv_init.simps step.simps tcopy_init_def numeral_2_eq_2
- numeral_3_eq_3 numeral_4_eq_4 split: if_splits)
+apply(auto simp: inv_init.simps step.simps tcopy_init_def numeral split: if_splits)
apply(case_tac "hd c", auto simp: inv_init.simps)
apply(case_tac c, simp_all)
done
@@ -137,8 +153,8 @@
proof(simp)
assume "inv_init x (s, l, r)" "0 < s"
thus "(step (s, l, r) (tcopy_init, 0), s, l, r) \<in> init_LE"
- apply(auto simp: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral_2_eq_2
- numeral_3_eq_3 numeral_4_eq_4 split: if_splits)
+ apply(auto simp: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral
+ split: if_splits)
apply(case_tac r, auto, case_tac a, auto)
done
qed
@@ -254,9 +270,6 @@
apply(case_tac t, auto)
done
-lemma numeral_5_eq_5: "5 = Suc 4" by arith
-
-lemma numeral_6_eq_6: "6 = Suc (Suc 4)" by arith
lemma [simp]: "inv_loop1 x (b, []) = False"
by(simp add: inv_loop1.simps)
@@ -472,8 +485,7 @@
"\<lbrakk>inv_loop x cf; x > 0\<rbrakk>
\<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
apply(case_tac cf, case_tac c, case_tac [2] aa)
-apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral_2_eq_2
- numeral_3_eq_3 numeral_4_eq_4 numeral_5_eq_5 numeral_6_eq_6 split: if_splits)
+apply(auto simp: inv_loop.simps step.simps tcopy_loop_def numeral split: if_splits)
done
lemma inv_loop_steps:
@@ -648,8 +660,7 @@
using h
apply(case_tac r', case_tac [2] a)
apply(auto simp: inv_loop.simps step.simps tcopy_loop_def
- numeral_2_eq_2 numeral_3_eq_3 numeral_4_eq_4
- numeral_5_eq_5 numeral_6_eq_6 loop_LE_def lex_triple_def lex_pair_def split: if_splits)
+ numeral loop_LE_def lex_triple_def lex_pair_def split: if_splits)
done
thus "(steps (Suc 0, l, r) (tcopy_loop, 0) (Suc n),
steps (Suc 0, l, r) (tcopy_loop, 0) n) \<in> loop_LE"
@@ -862,8 +873,7 @@
inv_end x cf\<rbrakk>
\<Longrightarrow> inv_end x (step cf (tcopy_end, 0))"
apply(case_tac cf, case_tac c, case_tac [2] aa)
-apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral_2_eq_2
- numeral_3_eq_3 numeral_4_eq_4 numeral_5_eq_5 split: if_splits)
+apply(auto simp: inv_end.simps step.simps tcopy_end_def numeral split: if_splits)
done
lemma inv_end_steps:
@@ -937,8 +947,7 @@
hence "(step (s', l', r') (tcopy_end, 0), s', l', r') \<in> end_LE"
apply(case_tac r', case_tac [2] a)
apply(auto simp: inv_end.simps step.simps tcopy_end_def
- numeral_2_eq_2 numeral_3_eq_3 numeral_4_eq_4
- numeral_5_eq_5 numeral_6_eq_6 end_LE_def lex_triple_def lex_pair_def split: if_splits)
+ numeral end_LE_def lex_triple_def lex_pair_def split: if_splits)
done
thus "(steps (Suc 0, l, r) (tcopy_end, 0) (Suc n),
steps (Suc 0, l, r) (tcopy_end, 0) n) \<in> end_LE"
@@ -1037,7 +1046,7 @@
(0, Bk\<up>m, [Oc, Oc])"
apply(rule_tac x = "Suc (Suc (Suc 0))" in exI)
apply(simp add: dither_def steps.simps
- step.simps fetch.simps numeral_2_eq_2)
+ step.simps fetch.simps numeral)
done
lemma dither_unhalt_state:
@@ -1046,7 +1055,7 @@
(steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = (2, Oc # Bk\<up>m, []))"
apply(induct stp, simp add: steps.simps)
apply(simp add: step_red, auto)
- apply(auto simp: step.simps fetch.simps dither_def numeral_2_eq_2)
+ apply(auto simp: step.simps fetch.simps dither_def numeral)
done
lemma dither_unhalt_rs:
@@ -1324,14 +1333,17 @@
apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n")
apply(simp, auto)
apply(erule_tac x = nd in allE, erule_tac x = 2 in allE)
- apply(simp add: numeral_2_eq_2 replicate_Suc tape_of_nl_abv)
+ apply(simp add: numeral replicate_Suc tape_of_nl_abv)
apply(erule_tac x = 0 in allE, simp)
done
qed
-lemma h_uh: "haltP (tcontra H, 0) [code (tcontra H)]
- \<Longrightarrow> \<not> haltP (tcontra H, 0) [code (tcontra H)]"
+
+
+lemma h_uh:
+ assumes "haltP (tcontra H, 0) [code (tcontra H)]"
+ shows "\<not> haltP (tcontra H, 0) [code (tcontra H)]"
proof(simp only: tcontra_def)
let ?tcontr = "(tcopy |+| H) |+| dither"
let ?cn = "Suc (code ?tcontr)"
@@ -1340,7 +1352,6 @@
let ?P2 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)"
let ?Q2 = "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
let ?P3 = ?Q2
- assume h: "haltP (?tcontr, 0) [code ?tcontr]"
have "{?P1} ?tcontr \<up>"
proof(rule_tac Hoare_plus_unhalt, auto)
show "?Q2 \<mapsto> ?P3"
@@ -1373,7 +1384,8 @@
qed
next
show "{?P2} H {?Q2}"
- using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] h
+ using Hoare_def h_newcase[of ?tcontr "[code ?tcontr]" 1] assms
+ unfolding tcontra_def
apply(auto)
apply(rule_tac x = na in exI)
apply(simp add: replicate_Suc tape_of_nl_abv)
@@ -1390,8 +1402,9 @@
by simp
qed
qed
- thus "\<not> True"
- using h
+ thus "\<not> haltP ((tcopy |+| H) |+| dither, 0) [code ((tcopy |+| H) |+| dither)]"
+ using assms
+ unfolding tcontra_def
apply(auto simp: haltP_def Hoare_unhalt_def)
apply(erule_tac x = n in allE)
apply(case_tac "steps (Suc 0, [], Oc \<up> ?cn) (?tcontr, 0) n")
@@ -1399,6 +1412,7 @@
done
qed
+
text {*
@{text "False"} is finally derived.
*}
@@ -1406,6 +1420,7 @@
lemma false: "False"
using uh_h h_uh
by auto
+
end
end