--- a/thys/uncomputable.thy Wed Jan 23 17:02:23 2013 +0100
+++ b/thys/uncomputable.thy Wed Jan 23 20:18:40 2013 +0100
@@ -25,8 +25,6 @@
and "5 = Suc 4"
and "6 = Suc 5" by arith+
-
-
text {*
The {\em Copying} TM, which duplicates its input.
*}
@@ -61,11 +59,11 @@
fun inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
- "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x )"
+ "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x)"
fun inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
- "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc\<up>j)"
+ "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc \<up> j)"
fun inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
@@ -77,14 +75,14 @@
fun inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
- "inv_init0 x (l, r) = ((x > Suc 0 \<and> l = Oc\<up>(x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or>
- (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))"
+ "inv_init0 x (l, r) = ((x > 1 \<and> l = Oc \<up> (x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or>
+ (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))"
fun inv_init :: "nat \<Rightarrow> config \<Rightarrow> bool"
where
- "inv_init x (s, l, r) = (
- if s = 0 then inv_init0 x (l, r)
- else if s = Suc 0 then inv_init1 x (l, r)
+ "inv_init x (s, l, r) =
+ (if s = 0 then inv_init0 x (l, r)
+ else if s = 1 then inv_init1 x (l, r)
else if s = 2 then inv_init2 x (l, r)
else if s = 3 then inv_init3 x (l, r)
else if s = 4 then inv_init4 x (l, r)
@@ -1077,6 +1075,13 @@
where
"dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "
+(* invariants of dither *)
+abbreviation
+ "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
+
+abbreviation
+ "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
+
lemma dither_unhalt_state:
"(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or>
(steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))"
@@ -1092,25 +1097,22 @@
by auto
lemma dither_loops:
- shows "{(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc])} dither \<up>"
+ shows "{dither_unhalt_inv} dither \<up>"
apply(rule Hoare_unhaltI)
using dither_unhalt_rs
apply(auto)
done
lemma dither_halt_rs:
- "\<exists>stp. steps0 (Suc 0, Bk \<up> m, [Oc, Oc]) dither stp = (0, Bk \<up> m, [Oc, Oc])"
+ "\<exists>stp. steps0 (1, Bk \<up> m, [Oc, Oc]) dither stp = (0, Bk \<up> m, [Oc, Oc])"
unfolding dither_def
apply(rule_tac x = "3" in exI)
apply(simp add: steps.simps step.simps fetch.simps numeral)
done
-definition
- "dither_halt_inv \<equiv> (\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc])"
lemma dither_halts:
shows "{dither_halt_inv} dither {dither_halt_inv}"
-unfolding dither_halt_inv_def
apply(rule HoareI)
using dither_halt_rs
apply(auto)
@@ -1218,33 +1220,29 @@
The TM @{text "H"} is the one which is assummed being able to solve the Halting problem.
*}
and H :: "instr list"
- assumes h_wf[intro]: "tm_wf (H, 0)"
+ assumes h_wf[intro]: "tm_wf0 H"
-- {*
The following two assumptions specifies that @{text "H"} does solve the Halting problem.
*}
and h_case:
- "\<And> M n. \<lbrakk>(haltP (M, 0) lm)\<rbrakk> \<Longrightarrow>
- \<exists> na nb. (steps (Suc 0, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))"
+ "\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [], <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
and nh_case:
- "\<And> M n. \<lbrakk>(\<not> haltP (M, 0) lm)\<rbrakk> \<Longrightarrow>
- \<exists> na nb. (steps (Suc 0, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
+ "\<And> M lm. (\<not> haltP0 M lm) \<Longrightarrow>
+ \<exists> na nb. (steps0 (1, [], <code M # lm>) H na = (0, Bk \<up> nb, [Oc, Oc]))"
begin
lemma h_newcase:
- "\<And> M n. haltP (M, 0) lm \<Longrightarrow>
- \<exists> na nb. (steps (Suc 0, Bk\<up>x , <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))"
+ "\<And> M lm. haltP0 M lm \<Longrightarrow> \<exists> na nb. (steps0 (1, Bk \<up> x , <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
proof -
- fix M n
+ fix M lm
assume "haltP (M, 0) lm"
- hence "\<exists> na nb. (steps (Suc 0, [], <code M # lm>) (H, 0) na
+ hence "\<exists> na nb. (steps (1, [], <code M # lm>) (H, 0) na
= (0, Bk\<up>nb, [Oc]))"
- apply(erule_tac h_case)
- done
+ by (rule h_case)
from this obtain na nb where
- cond1:"(steps (Suc 0, [], <code M # lm>) (H, 0) na
- = (0, Bk\<up>nb, [Oc]))" by blast
- thus "\<exists> na nb. (steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))"
- proof(rule_tac x = na in exI, case_tac "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
+ cond1:"(steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))" by blast
+ thus "\<exists> na nb. (steps (1, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))"
+ proof(rule_tac x = na in exI, case_tac "steps (1, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
fix a b c
assume cond2: "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
have "tinres (Bk\<up>nb) b \<and> [Oc] = c \<and> 0 = a"
@@ -1254,32 +1252,29 @@
apply(auto)
done
next
- show "(steps (Suc 0, [], <code M # lm>) (H, 0) na
+ show "(steps (1, [], <code M # lm>) (H, 0) na
= (0, Bk\<up>nb, [Oc]))"
- by(simp add: cond1)
+ by(simp add: cond1[simplified])
next
- show "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
- by(simp add: cond2)
+ show "steps (1, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
+ by(simp add: cond2[simplified])
qed
thus "a = 0 \<and> (\<exists>nb. b = (Bk\<up>nb)) \<and> c = [Oc]"
by(auto elim: tinres_ex1)
qed
qed
-lemma nh_newcase: "\<And> M n. \<lbrakk>\<not> (haltP (M, 0) lm)\<rbrakk> \<Longrightarrow>
- \<exists> na nb. (steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
+lemma nh_newcase:
+ "\<And> M lm. \<not> (haltP (M, 0) lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, Bk\<up>x, <code M # lm>) H na = (0, Bk\<up>nb, [Oc, Oc]))"
proof -
- fix M n
+ fix M lm
assume "\<not> haltP (M, 0) lm"
- hence "\<exists> na nb. (steps (Suc 0, [], <code M # lm>) (H, 0) na
- = (0, Bk\<up>nb, [Oc, Oc]))"
- apply(erule_tac nh_case)
- done
+ hence "\<exists> na nb. (steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
+ by (rule nh_case)
from this obtain na nb where
- cond1: "(steps (Suc 0, [], <code M # lm>) (H, 0) na
- = (0, Bk\<up>nb, [Oc, Oc]))" by blast
- thus "\<exists> na nb. (steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
- proof(rule_tac x = na in exI, case_tac "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
+ cond1: "(steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))" by blast
+ thus "\<exists> na nb. (steps (1, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
+ proof(rule_tac x = na in exI, case_tac "steps (1, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
fix a b c
assume cond2: "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
have "tinres (Bk\<up>nb) b \<and> [Oc, Oc] = c \<and> 0 = a"
@@ -1288,17 +1283,59 @@
apply(auto simp: tinres_def)
done
next
- show "(steps (Suc 0, [], <code M # lm>) (H, 0) na
- = (0, Bk\<up>nb, [Oc, Oc]))"
- by(simp add: cond1)
+ show "(steps (Suc 0, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
+ by(simp add: cond1[simplified])
next
show "steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (a, b, c)"
- by(simp add: cond2)
+ by(simp add: cond2[simplified])
qed
thus "a = 0 \<and> (\<exists>nb. b = Bk\<up>nb) \<and> c = [Oc, Oc]"
by(auto elim: tinres_ex1)
qed
qed
+
+
+(* invariants for H *)
+abbreviation
+ "pre_H_inv M n \<equiv> \<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code M, n]>)"
+
+abbreviation
+ "post_H_halt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
+
+abbreviation
+ "post_H_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
+
+
+lemma H_halt_inv:
+ assumes "\<not> haltP0 M [n]"
+ shows "{pre_H_inv M n} H {post_H_halt_inv}"
+proof -
+ obtain stp i
+ where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
+ using nh_newcase[of "M" "[n]" "1", OF assms] by auto
+ then show "{pre_H_inv M n} H {post_H_halt_inv}"
+ unfolding Hoare_def
+ apply(auto)
+ apply(rule_tac x = stp in exI)
+ apply(auto)
+ done
+qed
+
+lemma H_unhalt_inv:
+ assumes "haltP0 M [n]"
+ shows "{pre_H_inv M n} H {post_H_unhalt_inv}"
+proof -
+ obtain stp i
+ where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
+ using h_newcase[of "M" "[n]" "1", OF assms] by auto
+ then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
+ unfolding Hoare_def
+ apply(auto)
+ apply(rule_tac x = stp in exI)
+ apply(auto)
+ done
+qed
+
(* TM that produces the contradiction and its code *)
abbreviation
@@ -1314,7 +1351,7 @@
(* 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]>)"
- def P3 \<equiv> dither_halt_inv
+ def P3 \<equiv> "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
(*
{P1} tcopy {P2} {P2} H {P3}
@@ -1333,18 +1370,10 @@
show "{P1} tcopy {P2}" unfolding P1_def P2_def
by (rule tcopy_correct2)
next
- 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" "[code_tcontra]" 1, OF assms]
- by (auto)
- then show "{P2} H {P3}"
- unfolding P2_def P3_def dither_halt_inv_def
- unfolding Hoare_def
- apply(auto)
- apply(rule_tac x = n in exI)
- apply(simp)
- done
+ case B_halt (* of H *)
+ show "{P2} H {P3}"
+ unfolding P2_def P3_def
+ using assms by (rule H_halt_inv)
qed (simp)
(* {P3} dither {P3} *)
@@ -1356,7 +1385,7 @@
by (rule Hoare_plus_halt_simple[OF first second H_wf])
with assms show "False"
- unfolding P1_def P3_def dither_halt_inv_def
+ unfolding P1_def P3_def
unfolding haltP_def
unfolding Hoare_def
apply(auto)
@@ -1364,8 +1393,8 @@
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)
+ apply(simp add: numeral)
+ done
qed
(* asumme tcontra halts on its code *)
@@ -1395,18 +1424,10 @@
show "{P1} tcopy {P2}" unfolding P1_def P2_def
by (rule tcopy_correct2)
next
- 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" "[code_tcontra]" 1, OF assms]
- by (auto)
+ case B_halt (* of H *)
then show "{P2} H {P3}"
unfolding P2_def P3_def
- unfolding Hoare_def
- apply(auto)
- apply(rule_tac x = n in exI)
- apply(simp)
- done
+ using assms by (rule H_unhalt_inv)
qed (simp)
(* {P3} dither loops *)
@@ -1418,8 +1439,8 @@
by (rule Hoare_plus_unhalt_simple[OF first second H_wf])
with assms show "False"
+ unfolding P1_def
unfolding haltP_def
- unfolding P1_def
unfolding Hoare_unhalt_def
by (auto, metis is_final_eq)
qed