--- a/thys/uncomputable.thy Wed Jan 23 15:33:26 2013 +0100
+++ b/thys/uncomputable.thy Wed Jan 23 15:42:47 2013 +0100
@@ -1269,21 +1269,17 @@
qed
qed
-(* TM that produces the contradiction *)
-definition tcontra :: "instr list \<Rightarrow> instr list"
- where
- "tcontra h \<equiv> (tcopy |+| h) |+| dither"
+(* TM that produces the contradiction and its code *)
+abbreviation
+ "tcontra \<equiv> (tcopy |+| H) |+| dither"
+abbreviation
+ "code_tcontra \<equiv> code tcontra"
-
-lemma uh_h:
- assumes "\<not> haltP0 (tcontra H) [code (tcontra H)]"
+(* assume tcontra does not halt on its code *)
+lemma tcontra_unhalt:
+ assumes "\<not> haltP0 tcontra [code tcontra]"
shows "False"
proof -
- (* code of tcontra *)
- def code_tcontra \<equiv> "(code (tcontra H))"
- have assms': "\<not> haltP0 (tcontra H) [code_tcontra]"
- using assms by (simp add: code_tcontra_def)
-
(* invariants *)
def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)"
def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)"
@@ -1294,7 +1290,7 @@
----------------------------
{P1} (tcopy |+| H) {P3} {P3} dither {P3}
------------------------------------------------
- {P1} (tcontra H) {P3}
+ {P1} tcontra {P3}
*)
have H_wf: "tm_wf0 (tcopy |+| H)" by auto
@@ -1304,13 +1300,12 @@
proof (induct rule: Hoare_plus_halt_simple)
case A_halt (* of tcopy *)
have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}"
- unfolding code_tcontra_def
by (rule tcopy_correct1) (simp)
moreover
have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def
by (simp add: assert_imp_def tape_of_nl_abv)
moreover
- have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def code_tcontra_def
+ have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def
by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
ultimately
show "{P1} tcopy {P2}" by (rule Hoare_weak)
@@ -1318,7 +1313,7 @@
case B_halt
obtain n i
where "steps0 (1, Bk \<up> 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \<up> i, [Oc, Oc])"
- using nh_newcase[of "tcontra H" "[code_tcontra]" 1, OF assms', folded code_tcontra_def]
+ using nh_newcase[of "tcontra" "[code_tcontra]" 1, OF assms]
by (auto)
then show "{P2} H {P3}"
unfolding P2_def P3_def dither_halt_inv_def
@@ -1334,31 +1329,27 @@
by (rule dither_halts)
(* {P1} tcontra {P3} *)
- have "{P1} (tcontra H) {P3}" unfolding tcontra_def
+ have "{P1} tcontra {P3}"
by (rule Hoare_plus_halt_simple[OF first second H_wf])
- with assms' show "False"
- unfolding P1_def P3_def dither_halt_inv_def code_tcontra_def
+ with assms show "False"
+ unfolding P1_def P3_def dither_halt_inv_def
unfolding haltP_def
unfolding Hoare_def
apply(auto)
apply(erule_tac x = n in allE)
- apply(case_tac "steps0 (Suc 0, [], <[code (tcontra H)]>) (tcontra H) n")
+ apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n")
apply(simp, auto)
apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE)
apply(simp)
by (smt replicate_0 replicate_Suc)
qed
-lemma h_uh:
- assumes "haltP0 (tcontra H) [code (tcontra H)]"
+(* asumme tcontra halts on its code *)
+lemma tcontra_halt:
+ assumes "haltP0 tcontra [code tcontra]"
shows "False"
proof -
- (* code of tcontra *)
- def code_tcontra \<equiv> "(code (tcontra H))"
- have assms': "haltP0 (tcontra H) [code_tcontra]"
- using assms by (simp add: code_tcontra_def)
-
(* invariants *)
def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)"
def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)"
@@ -1369,7 +1360,7 @@
----------------------------
{P1} (tcopy |+| H) {P3} {P3} dither loops
------------------------------------------------
- {P1} (tcontra H) loops
+ {P1} tcontra loops
*)
have H_wf: "tm_wf0 (tcopy |+| H)" by auto
@@ -1379,13 +1370,12 @@
proof (induct rule: Hoare_plus_halt_simple)
case A_halt (* of tcopy *)
have "{inv_init1 (Suc code_tcontra)} tcopy {inv_end0 (Suc code_tcontra)}"
- unfolding code_tcontra_def
by (rule tcopy_correct1) (simp)
moreover
have "P1 \<mapsto> inv_init1 (Suc code_tcontra)" unfolding P1_def
by (simp add: assert_imp_def tape_of_nl_abv)
moreover
- have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def code_tcontra_def
+ have "inv_end0 (Suc code_tcontra) \<mapsto> P2" unfolding P2_def
by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
ultimately
show "{P1} tcopy {P2}" by (rule Hoare_weak)
@@ -1393,7 +1383,7 @@
case B_halt
obtain n i
where "steps0 (1, Bk \<up> 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \<up> i, [Oc])"
- using h_newcase[of "tcontra H" "[code_tcontra]" 1, OF assms', folded code_tcontra_def]
+ using h_newcase[of "tcontra" "[code_tcontra]" 1, OF assms]
by (auto)
then show "{P2} H {P3}"
unfolding P2_def P3_def
@@ -1409,25 +1399,23 @@
by (rule dither_loops)
(* {P1} tcontra loops *)
- have "{P1} (tcontra H) \<up>" unfolding tcontra_def
+ have "{P1} tcontra \<up>"
by (rule Hoare_plus_unhalt_simple[OF first second H_wf])
with assms show "False"
unfolding haltP_def
- unfolding P1_def code_tcontra_def
+ unfolding P1_def
unfolding Hoare_unhalt_def
by (auto, metis is_final_eq)
qed
-
-
-
text {*
@{text "False"} can finally derived.
*}
lemma false: "False"
-using uh_h h_uh by auto
+using tcontra_halt tcontra_unhalt
+by auto
end