tm: comparison thys/uncomputable.thy

equal deleted inserted replaced

-:32ec97f94a07
+:2363eb91d9fd
 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.
 *}
 definition
 (* tcopy_init *)
 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
 "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc \<up> x \<and> tl r = [])"
 where
 "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc \<up> x \<and> r = [Bk, Oc]) \<or> (l = Oc \<up> (x - 1) \<and> r = [Oc, Bk, Oc])))"
 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>
+"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) = (
+"inv_init x (s, l, r) =
-if s = 0 then inv_init0 x (l, r)
+(if s = 0 then inv_init0 x (l, r)
-else if s = Suc 0 then inv_init1 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)
 else False)"
 definition dither :: "instr list"
 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, []))"
 apply(induct stp)
 apply(simp add: steps.simps)
 shows "\<not> is_final (steps0 (1, Bk \<up> m, [Oc]) dither stp)"
 using dither_unhalt_state[of m stp]
 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)
 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
 fixes code :: "instr list \<Rightarrow> nat"
 -- {*
 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>
+"\<And> M lm. (haltP0 M lm) \<Longrightarrow> \<exists> na nb. (steps0 (1, [], <code M # lm>) H na = (0, Bk \<up> nb, [Oc]))"
-\<exists> na nb. (steps (Suc 0, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))"
 and nh_case:
-"\<And> M n. \<lbrakk>(\<not> haltP (M, 0) lm)\<rbrakk> \<Longrightarrow>
+"\<And> M lm. (\<not> haltP0 M lm) \<Longrightarrow>
-\<exists> na nb. (steps (Suc 0, [],  <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
+\<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>
+"\<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]))"
-\<exists> na nb. (steps (Suc 0, Bk\<up>x , <code M # lm>) (H, 0) 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)
+by (rule h_case)
-done
 from this obtain na nb where
-cond1:"(steps (Suc 0, [], <code M # lm>) (H, 0) na
+cond1:"(steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc]))" by blast
-= (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]))"
-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 (1, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
-proof(rule_tac x = na in exI, case_tac "steps (Suc 0, 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"
 proof(rule_tac tinres_steps)
 show "tinres [] (Bk\<up>x)"
 apply(simp add: tinres_def)
 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)"
+show "steps (1, 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]"
 by(auto elim: tinres_ex1)
 qed
 qed
-lemma nh_newcase: "\<And> M n. \<lbrakk>\<not> (haltP (M, 0) lm)\<rbrakk> \<Longrightarrow>
+lemma nh_newcase:
-\<exists> na nb. (steps (Suc 0, Bk\<up>x, <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
+"\<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
+hence "\<exists> na nb. (steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
-= (0, Bk\<up>nb, [Oc, Oc]))"
+by (rule nh_case)
-apply(erule_tac nh_case)
-done
 from this obtain na nb where
-cond1: "(steps (Suc 0, [], <code M # lm>) (H, 0) na
+cond1: "(steps (1, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))" by blast
-= (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]))"
-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 (1, Bk\<up>x, <code M # lm>) (H, 0) na", simp)
-proof(rule_tac x = na in exI, case_tac "steps (Suc 0, 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"
 proof(rule_tac tinres_steps)
 show "tinres [] (Bk\<up>x)"
 apply(auto simp: tinres_def)
 done
 next
-show "(steps (Suc 0, [], <code M # lm>) (H, 0) na
+show "(steps (Suc 0, [], <code M # lm>) (H, 0) na = (0, Bk\<up>nb, [Oc, Oc]))"
-= (0, Bk\<up>nb, [Oc, Oc]))"
+by(simp add: cond1[simplified])
-by(simp add: cond1)
 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
 "tcontra \<equiv> (tcopy |+| H) |+| dither"
 abbreviation
 shows "False"
 proof -
 (* 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}
 ----------------------------
 {P1} (tcopy |+| H) {P3}     {P3} dither {P3}
 proof (cases rule: Hoare_plus_halt_simple)
 case A_halt (* of tcopy *)
 show "{P1} tcopy {P2}" unfolding P1_def P2_def
 by (rule tcopy_correct2)
 next
-case B_halt
+case B_halt (* of H *)
-obtain n i
+show "{P2} H {P3}"
-where "steps0 (1, Bk \<up> 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \<up> i, [Oc, Oc])"
+unfolding P2_def P3_def
-using nh_newcase[of "tcontra" "[code_tcontra]" 1, OF assms]
+using assms by (rule H_halt_inv)
-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
 qed (simp)
 (* {P3} dither {P3} *)
 have second: "{P3} dither {P3}" unfolding P3_def
 by (rule dither_halts)
 (* {P1} tcontra {P3} *)
 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
+unfolding P1_def P3_def
 unfolding haltP_def
 unfolding Hoare_def
 apply(auto)
 apply(erule_tac x = n in allE)
 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)
+apply(simp add: numeral)
-by (smt replicate_0 replicate_Suc)
+done
 qed
 (* asumme tcontra halts on its code *)
 lemma tcontra_halt:
 assumes "haltP0 tcontra [code tcontra]"
 proof (cases rule: Hoare_plus_halt_simple)
 case A_halt (* of tcopy *)
 show "{P1} tcopy {P2}" unfolding P1_def P2_def
 by (rule tcopy_correct2)
 next
-case B_halt
+case B_halt (* of H *)
-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)
 then show "{P2} H {P3}"
 unfolding P2_def P3_def
-unfolding Hoare_def
+using assms by (rule H_unhalt_inv)
-apply(auto)
-apply(rule_tac x = n in exI)
-apply(simp)
-done
 qed (simp)
 (* {P3} dither loops *)
 have second: "{P3} dither \<up>" unfolding P3_def
 by (rule dither_loops)
 (* {P1} tcontra loops *)
 have "{P1} tcontra \<up>"
 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
 text {*

changeset 70	2363eb91d9fd
parent 69	32ec97f94a07
child 71	8c7f10b3da7b