# HG changeset patch # User Christian Urban # Date 1358949992 -3600 # Node ID 0349fa7f5595736daee86fc8fa1d185639c5cc2d # Parent 5c74f6b38a63cd5fdcb002cbe5689b649644d06d also polished uh_h proof diff -r 5c74f6b38a63 -r 0349fa7f5595 thys/uncomputable.thy --- 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 \ nat list \ bool" where - "haltP t lm = (\n a b c. steps (Suc 0, [], ) t n = (0, Bk\a, Oc\b @ Bk\c))" + "haltP p lm = (\n a b c. steps (Suc 0, [], ) p n = (0, Bk\a, Oc\b @ Bk\c))" + -lemma [intro]: "tm_wf (tcopy, 0)" +abbreviation + "haltP0 p lm \ 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)) \ - \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 \ instr list" where - "tcontra h \ ((tcopy |+| h) |+| dither)" + "tcontra h \ (tcopy |+| h) |+| dither" declare replicate_Suc[simp del] -lemma uh_h: "\ haltP (tcontra H, 0) [code (tcontra H)] - \ haltP (tcontra H, 0) [code (tcontra H)]" -proof(simp only: tcontra_def) - let ?tcontr = "(tcopy |+| H) |+| dither" - let ?cn = "Suc (code ?tcontr)" - let ?P1 = "\ (l, r). (l = [] \ (r::cell list) = Oc\(?cn))" - let ?Q1 = "\ (l, r). (l = [Bk] \ r = Oc\?cn @ Bk # Oc\?cn)" - let ?P2 = "\ (l, r). (l = [Bk] \ r = Oc\?cn @ Bk # Oc\?cn)" - let ?Q2 = "\(l, r). (\nd. l = Bk \ nd) \ r = [Oc, Oc]" - let ?P3 = ?Q2 - let ?Q3 = ?P3 - assume h: "\ haltP (?tcontr, 0) [code ?tcontr]" - have "{?P1} ?tcontr {?Q3}" - proof(rule_tac Hoare_plus_halt, auto) - show "?Q2 \ ?P3" - apply(simp add: assert_imp_def) - done - next - show "{?P1} (tcopy|+|H) {?Q2}" - proof(rule_tac Hoare_plus_halt, auto) - show "?Q1 \ ?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 \ inv_init1 (?cn)" - apply(simp add: inv_init1.simps assert_imp_def) - done - next - show "inv_end0 ?cn \ ?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 "\n. is_final (steps (Suc 0, Bk \ nd, [Oc, Oc]) (dither, 0) n) \ - (\(l, r). (\nd. l = Bk \ nd) \ r = [Oc, Oc]) - holds_for steps (Suc 0, Bk \ 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 \ ?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 "{(\(l, r). (\nd. l = Bk \ nd) \ r = [Oc])} dither \" apply(rule Hoare_unhaltI) apply(auto intro!: dither_unhalt_rs) done - -lemma h_uh: - assumes "haltP (tcontra H, 0) [code (tcontra H)]" - shows "\ haltP (tcontra H, 0) [code (tcontra H)]" -proof - - (* code of tcontra *) + +lemma dither_halts: + shows + "{(\(l, r). (\nd. l = Bk \ nd) \ r = [Oc, Oc])} dither {(\(l, r). (\nd. l = Bk \ nd) \ 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 "\ haltP0 (tcontra H) [code (tcontra H)]" + shows "haltP0 (tcontra H) [code (tcontra H)]" +proof - + (* code of tcontra *) def code_tcontra \ "(code (tcontra H))" + have assms': "\ haltP0 (tcontra H) [code_tcontra]" + using assms by (simp add: code_tcontra_def) (* invariants *) def P1 \ "\(l::cell list, r::cell list). (l = [] \ r = <[code_tcontra]>)" def P2 \ "\(l::cell list, r::cell list). (l = [Bk] \ r = <[code_tcontra, code_tcontra]>)" - def P3 \ "\(l::cell list, r::cell list). (\nd. l = Bk \ nd) \ r = [Oc]" + def P3 \ "\(l::cell list, r::cell list). (\nd. l = Bk \ nd) \ 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 \ 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \ 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 "\ haltP0 (tcontra H) [code (tcontra H)]" +proof - + (* code of tcontra *) + def code_tcontra \ "(code (tcontra H))" + have assms': "haltP0 (tcontra H) [code_tcontra]" + using assms by (simp add: code_tcontra_def) + + (* invariants *) + def P1 \ "\(l::cell list, r::cell list). (l = [] \ r = <[code_tcontra]>)" + def P2 \ "\(l::cell list, r::cell list). (l = [Bk] \ r = <[code_tcontra, code_tcontra]>)" + def P3 \ "\(l::cell list, r::cell list). (\nd. l = Bk \ nd) \ 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 \ 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) \ 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 \ 1, <[code_tcontra, code_tcontra]>) H n = (0, Bk \ 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 \" unfolding P3_def @@ -1400,16 +1407,15 @@ (* {P1} tcontra loops *) have "{P1} (tcontra H) \" unfolding tcontra_def - by (rule Hoare_plus_unhalt_simple[OF first second tm2_wf]) - - then show "\ 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 "\ haltP0 (tcontra H) [code_tcontra]" + by blast qed