--- a/thys/uncomputable.thy Wed Jan 23 12:25:24 2013 +0100
+++ b/thys/uncomputable.thy Wed Jan 23 15:06:32 2013 +0100
@@ -1075,14 +1075,18 @@
definition haltP :: "tprog \<Rightarrow> nat list \<Rightarrow> bool"
where
- "haltP t lm = (\<exists>n a b c. steps (Suc 0, [], <lm>) t n = (0, Bk\<up>a, Oc\<up>b @ Bk\<up>c))"
+ "haltP p lm = (\<exists>n a b c. steps (Suc 0, [], <lm>) p n = (0, Bk\<up>a, Oc\<up>b @ Bk\<up>c))"
+
-lemma [intro]: "tm_wf (tcopy, 0)"
+abbreviation
+ "haltP0 p lm \<equiv> haltP (p, 0) lm"
+
+lemma [intro, simp]: "tm_wf0 tcopy"
by(auto simp: tcopy_def)
-lemma [intro]: "tm_wf (dither, 0)"
-apply(auto simp: tm_wf.simps dither_def)
-done
+lemma [intro, simp]: "tm_wf0 dither"
+by (auto simp: tm_wf.simps dither_def)
+
text {*
The following lemma shows the meaning of @{text "tinres"} with respect to
@@ -1246,127 +1250,49 @@
qed
qed
-(*
-lemma haltP_weaking:
- "haltP (tcontra H) (code (tcontra H)) \<Longrightarrow>
- \<exists>stp. isS0 (steps (Suc 0, [], Oc\<^bsup>code (tcontra H)\<^esup>)
- ((tcopy |+| H) |+| dither) stp)"
- apply(simp add: haltP_def, auto)
- apply(rule_tac x = n in exI, simp add: isS0_def tcontra_def)
- done
-*)
-
definition tcontra :: "instr list \<Rightarrow> instr list"
where
- "tcontra h \<equiv> ((tcopy |+| h) |+| dither)"
+ "tcontra h \<equiv> (tcopy |+| h) |+| dither"
declare replicate_Suc[simp del]
-lemma uh_h: "\<not> haltP (tcontra H, 0) [code (tcontra H)]
- \<Longrightarrow> haltP (tcontra H, 0) [code (tcontra H)]"
-proof(simp only: tcontra_def)
- let ?tcontr = "(tcopy |+| H) |+| dither"
- let ?cn = "Suc (code ?tcontr)"
- let ?P1 = "\<lambda> (l, r). (l = [] \<and> (r::cell list) = Oc\<up>(?cn))"
- let ?Q1 = "\<lambda> (l, r). (l = [Bk] \<and> r = Oc\<up>?cn @ Bk # Oc\<up>?cn)"
- 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, Oc]"
- let ?P3 = ?Q2
- let ?Q3 = ?P3
- assume h: "\<not> haltP (?tcontr, 0) [code ?tcontr]"
- have "{?P1} ?tcontr {?Q3}"
- proof(rule_tac Hoare_plus_halt, auto)
- show "?Q2 \<mapsto> ?P3"
- apply(simp add: assert_imp_def)
- done
- next
- show "{?P1} (tcopy|+|H) {?Q2}"
- proof(rule_tac Hoare_plus_halt, auto)
- show "?Q1 \<mapsto> ?P2"
- apply(simp add: assert_imp_def)
- done
- next
- show "{?P1} tcopy {?Q1}"
- proof -
- have g: "{inv_init1 ?cn} tcopy {inv_end0 ?cn}"
- by(rule_tac tcopy_correct1, simp)
- thus "?thesis"
- proof(rule_tac Hoare_weak)
- show "{inv_init1 ?cn} tcopy
- {inv_end0 ?cn} " using g by simp
- next
- show "?P1 \<mapsto> inv_init1 (?cn)"
- apply(simp add: inv_init1.simps assert_imp_def)
- done
- next
- show "inv_end0 ?cn \<mapsto> ?Q1"
- apply(simp add: assert_imp_def inv_end0.simps)
- done
- qed
- qed
- next
- show "{?P2} H {?Q2}"
- using Hoare_def nh_newcase[of ?tcontr "[code ?tcontr]" 1] h
- apply(auto)
- apply(rule_tac x = na in exI)
- apply(simp add: replicate_Suc tape_of_nl_abv)
- done
- qed
- next
- show "{?P3} dither {?Q3}"
- using Hoare_def
- proof(auto)
- fix nd
- show "\<exists>n. is_final (steps (Suc 0, Bk \<up> nd, [Oc, Oc]) (dither, 0) n) \<and>
- (\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc])
- holds_for steps (Suc 0, Bk \<up> nd, [Oc, Oc]) (dither, 0) n"
- using dither_halt_rs[of nd]
- apply(auto)
- apply(rule_tac x = stp in exI, simp)
- done
- qed
- qed
- thus "False"
- using h
- apply(auto simp: haltP_def Hoare_def)
- apply(erule_tac x = n in allE)
- 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 replicate_Suc tape_of_nl_abv)
- apply(erule_tac x = 0 in allE, simp)
- done
-qed
-
-
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 h_uh:
- assumes "haltP (tcontra H, 0) [code (tcontra H)]"
- shows "\<not> haltP (tcontra H, 0) [code (tcontra H)]"
-proof -
- (* code of tcontra *)
+
+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)]"
+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]"
+ def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
(*
{P1} tcopy {P2} {P2} H {P3}
----------------------------
- {P1} (tcopy |+| H) {P3} {P3} dither loops
+ {P1} (tcopy |+| H) {P3} {P3} dither {P3}
------------------------------------------------
- {P1} (tcontra H) loops
+ {P1} (tcontra H) {P3}
*)
- have tm1_wf: "tm_wf0 tcopy" by auto
- have tm2_wf: "tm_wf0 (tcopy |+| H)" by auto
+ have H_wf: "tm_wf0 (tcopy |+| H)" by auto
(* {P1} (tcopy |+| H) {P3} *)
have first: "{P1} (tcopy |+| H) {P3}"
@@ -1385,14 +1311,95 @@
show "{P1} tcopy {P2}" by (rule Hoare_weak)
next
case B_halt
- show "{P2} H {P3}"
- using Hoare_def h_newcase[of "tcontra H" "[code_tcontra]" 1] assms
- unfolding tcontra_def P2_def P3_def code_tcontra_def
+ 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 Hoare_def
apply(auto)
- apply(rule_tac x = na in exI)
- apply(simp add: replicate_Suc tape_of_nl_abv)
+ apply(rule_tac x = n in exI)
+ apply(simp add: replicate_Suc)
done
- qed (simp add: tm1_wf)
+ qed (simp)
+
+ (* {P3} dither {P3} *)
+ have second: "{P3} dither {P3}" unfolding P3_def
+ by (rule dither_halts)
+
+ (* {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"
+ unfolding P1_def P3_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)]"
+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]>)"
+ def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
+
+ (*
+ {P1} tcopy {P2} {P2} H {P3}
+ ----------------------------
+ {P1} (tcopy |+| H) {P3} {P3} dither loops
+ ------------------------------------------------
+ {P1} (tcontra H) loops
+ *)
+
+ have H_wf: "tm_wf0 (tcopy |+| H)" by auto
+
+ (* {P1} (tcopy |+| H) {P3} *)
+ have first: "{P1} (tcopy |+| H) {P3}"
+ 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
+ by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
+ ultimately
+ show "{P1} tcopy {P2}" by (rule Hoare_weak)
+ 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 H" "[code_tcontra]" 1, OF assms', folded code_tcontra_def]
+ by (auto)
+ 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)
+ done
+ qed (simp)
(* {P3} dither loops *)
have second: "{P3} dither \<up>" unfolding P3_def
@@ -1400,16 +1407,15 @@
(* {P1} tcontra loops *)
have "{P1} (tcontra H) \<up>" unfolding tcontra_def
- by (rule Hoare_plus_unhalt_simple[OF first second tm2_wf])
-
- then show "\<not> haltP (tcontra H, 0) [code_tcontra]"
- using assms
- unfolding tcontra_def code_tcontra_def
- apply(auto simp: haltP_def Hoare_unhalt_def P1_def)
- apply(erule_tac x = n in allE)
- apply(case_tac "steps (Suc 0, [], <[code ((tcopy |+| H) |+| dither)]>) (tcontra H, 0) n")
- apply(simp add: tape_of_nl_abv tcontra_def code_tcontra_def tape_of_nat_abv)
- done
+ by (rule Hoare_plus_unhalt_simple[OF first second H_wf])
+
+ with assms have "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