# HG changeset patch # User Christian Urban <christian dot urban at kcl dot ac dot uk> # Date 1358940324 -3600 # Node ID 5c74f6b38a63cd5fdcb002cbe5689b649644d06d # Parent 35fe8fe12e659d021b45be7a219d18c44e5272cb updated h_uh proof in uncomputable diff -r 35fe8fe12e65 -r 5c74f6b38a63 thys/turing_hoare.thy --- a/thys/turing_hoare.thy Wed Jan 23 08:01:35 2013 +0100 +++ b/thys/turing_hoare.thy Wed Jan 23 12:25:24 2013 +0100 @@ -35,7 +35,7 @@ unfolding Hoare_def using assms by auto -lemma Hoare_unhalt_I: +lemma Hoare_unhaltI: assumes "\<And>l r n. P (l, r) \<Longrightarrow> \<not> is_final (steps0 (1, (l, r)) p n)" shows "{P} p \<up>" unfolding Hoare_unhalt_def @@ -92,6 +92,15 @@ using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp) qed +lemma Hoare_plus_halt_simple [case_names A_halt B_halt A_wf]: + assumes A_halt : "{P1} A {P2}" + and B_halt : "{P2} B {P3}" + and A_wf : "tm_wf (A, 0)" + shows "{P1} A |+| B {P3}" +by (rule Hoare_plus_halt[OF A_halt B_halt _ A_wf]) + (simp add: assert_imp_def) + + text {* {P1} A {Q1} {P2} B loops Q1 \<mapsto> P2 A well-formed @@ -99,16 +108,13 @@ {P1} A |+| B loops *} - - - lemma Hoare_plus_unhalt: assumes A_halt: "{P1} A {Q1}" and B_uhalt: "{P2} B \<up>" and a_imp: "Q1 \<mapsto> P2" and A_wf : "tm_wf (A, 0)" shows "{P1} (A |+| B) \<up>" -proof(rule_tac Hoare_unhalt_I) +proof(rule_tac Hoare_unhaltI) fix n l r assume h: "P1 (l, r)" then obtain n1 l' r' @@ -145,6 +151,15 @@ qed qed +lemma Hoare_plus_unhalt_simple [case_names A_halt B_unhalt A_wf]: + assumes A_halt: "{P1} A {P2}" + and B_uhalt: "{P2} B \<up>" + and A_wf : "tm_wf (A, 0)" + shows "{P1} (A |+| B) \<up>" +by (rule Hoare_plus_unhalt[OF A_halt B_uhalt _ A_wf]) + (simp add: assert_imp_def) + + lemma Hoare_weak: assumes a: "{P} p {Q}" and b: "P' \<mapsto> P" diff -r 35fe8fe12e65 -r 5c74f6b38a63 thys/uncomputable.thy --- a/thys/uncomputable.thy Wed Jan 23 08:01:35 2013 +0100 +++ b/thys/uncomputable.thy Wed Jan 23 12:25:24 2013 +0100 @@ -1337,84 +1337,86 @@ 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(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]" - let ?P3 = ?Q2 - have "{?P1} ?tcontr \<up>" - proof(rule_tac Hoare_plus_unhalt, auto) - show "?Q2 \<mapsto> ?P3" - apply(simp add: assert_imp_def) - done +proof - + (* code of tcontra *) + def code_tcontra \<equiv> "(code (tcontra H))" + + (* 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 tm1_wf: "tm_wf0 tcopy" by auto + have tm2_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 - 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 h_newcase[of ?tcontr "[code ?tcontr]" 1] assms - unfolding tcontra_def - apply(auto) - apply(rule_tac x = na in exI) - apply(simp add: replicate_Suc tape_of_nl_abv) - done - qed - next - show "{?P3} dither \<up>" - using Hoare_unhalt_def - proof(auto) - fix nd n - assume "is_final (steps (Suc 0, Bk \<up> nd, [Oc]) (dither, 0) n)" - thus "False" - using dither_unhalt_rs[of nd n] - by simp - qed - qed - thus "\<not> haltP ((tcopy |+| H) |+| dither, 0) [code ((tcopy |+| H) |+| dither)]" + 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 + apply(auto) + apply(rule_tac x = na in exI) + apply(simp add: replicate_Suc tape_of_nl_abv) + done + qed (simp add: tm1_wf) + + (* {P3} dither loops *) + have second: "{P3} dither \<up>" unfolding P3_def + by (rule dither_loops) + + (* {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 - apply(auto simp: haltP_def Hoare_unhalt_def) + 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, [], Oc \<up> ?cn) (?tcontr, 0) n") - apply(simp add: tape_of_nl_abv) + 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 qed - + + + text {* - @{text "False"} is finally derived. + @{text "False"} can finally derived. *} lemma false: "False"