tm: comparison thys/uncomputable.thy

equal deleted inserted replaced

-:0349fa7f5595
+:4a3cd7d70ec2
 text {*
 The {\em Dithering} TM, when the input is @{text "1"}, it will loop forever, otherwise, it will
 terminate.
 *}
 definition dither :: "instr list"
 where
 "dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "
-lemma dither_halt_rs:
-"\<exists> stp. steps (Suc 0, Bk\<up>m, [Oc, Oc]) (dither, 0) stp =
-(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)
-done
 lemma dither_unhalt_state:
-"(steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp =
+"(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or>
-(Suc 0, Bk\<up>m, [Oc])) \<or>
+(steps0 (1, Bk \<up> m, [Oc]) dither stp = (2, Oc # Bk \<up> m, []))"
-(steps (Suc 0, Bk\<up>m, [Oc]) (dither, 0) stp = (2, Oc # Bk\<up>m, []))"
+apply(induct stp)
-apply(induct stp, simp add: steps.simps)
+apply(simp add: steps.simps)
-apply(simp add: step_red, auto)
+apply(simp add: step_red)
 apply(auto simp: step.simps fetch.simps dither_def numeral)
 done
 lemma dither_unhalt_rs:
-"\<not> is_final (steps (Suc 0, Bk\<up>m, [Oc]) (dither,0) stp)"
+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>"
+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])"
+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)
 section {*
 The final diagnal arguments to show the undecidability of Halting problem.
 *}
 thus "a = 0 \<and> (\<exists>nb. b =  Bk\<up>nb) \<and> c = [Oc, Oc]"
 by(auto elim: tinres_ex1)
 qed
 qed
+(* TM that produces the contradiction *)
 definition tcontra :: "instr list \<Rightarrow> instr list"
 where
 "tcontra h \<equiv> (tcopy |+| h) |+| dither"
-declare replicate_Suc[simp del]
-lemma dither_loops:
-shows "{(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc])} dither \<up>"
-apply(rule Hoare_unhaltI)
-apply(auto intro!: dither_unhalt_rs)
-done
-lemma dither_halts:
-shows
-"{(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc])} dither {(\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc])}"
-apply(rule HoareI)
-using dither_halt_rs
-apply(auto)
-by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
 lemma uh_h:
 assumes "\<not> haltP0 (tcontra H) [code (tcontra H)]"
-shows "haltP0 (tcontra H) [code (tcontra H)]"
+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]>)"
-def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
+def P3 \<equiv> dither_halt_inv
 (*
 {P1} tcopy {P2}  {P2} H {P3}
 ----------------------------
 {P1} (tcopy |+| H) {P3}     {P3} dither {P3}
 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]
 by (auto)
 then show "{P2} H {P3}"
-unfolding P2_def P3_def
+unfolding P2_def P3_def dither_halt_inv_def
 unfolding Hoare_def
 apply(auto)
 apply(rule_tac x = n in exI)
-apply(simp add: replicate_Suc)
+apply(simp)
 done
 qed (simp)
 (* {P3} dither {P3} *)
 have second: "{P3} dither {P3}" unfolding P3_def
 (* {P1} tcontra {P3} *)
 have "{P1} (tcontra H) {P3}" unfolding tcontra_def
 by (rule Hoare_plus_halt_simple[OF first second H_wf])
-with assms' have "False"
+with assms' show "False"
-unfolding P1_def P3_def code_tcontra_def
+unfolding P1_def P3_def dither_halt_inv_def code_tcontra_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(simp, auto)
 apply(erule_tac x = 2 in allE, erule_tac x = 0 in allE)
 apply(simp)
 by (smt replicate_0 replicate_Suc)
-then show "haltP0 (tcontra H) [code (tcontra H)]"
-by blast
 qed
 lemma h_uh:
 assumes "haltP0 (tcontra H) [code (tcontra H)]"
-shows "\<not> haltP0 (tcontra H) [code (tcontra H)]"
+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)
 then show "{P2} H {P3}"
 unfolding P2_def P3_def
 unfolding Hoare_def
 apply(auto)
 apply(rule_tac x = n in exI)
-apply(simp add: replicate_Suc)
+apply(simp)
 done
 qed (simp)
 (* {P3} dither loops *)
 have second: "{P3} dither \<up>" unfolding P3_def
 (* {P1} tcontra loops *)
 have "{P1} (tcontra H) \<up>" unfolding tcontra_def
 by (rule Hoare_plus_unhalt_simple[OF first second H_wf])
-with assms have "False"
+with assms show "False"
 unfolding haltP_def
 unfolding P1_def code_tcontra_def
 unfolding Hoare_unhalt_def
 by (auto, metis is_final_eq)
-then show "\<not> haltP0 (tcontra H) [code_tcontra]"
-by blast
 qed
 text {*
 @{text "False"} can finally derived.
 *}
 lemma false: "False"
-using uh_h h_uh
+using uh_h h_uh by auto
-by auto
 end
+declare replicate_Suc[simp del]
 end

changeset 66	4a3cd7d70ec2
parent 65	0349fa7f5595
child 67	140489a4020e