# HG changeset patch # User Christian Urban # Date 1358606647 0 # Node ID cd4ef33c8fb1a4c88bc81230bd1a94f9fdfb3832 # Parent e7d845acb0a7e038c01b0a1c9cf7f6846014e238 added turing_hoare diff -r e7d845acb0a7 -r cd4ef33c8fb1 Paper/ROOT.ML --- a/Paper/ROOT.ML Sat Jan 19 14:29:56 2013 +0000 +++ b/Paper/ROOT.ML Sat Jan 19 14:44:07 2013 +0000 @@ -1,5 +1,6 @@ no_document use_thys ["../thys/turing_basic", + "../thys/turing_hoare", "../thys/uncomputable"(*, "../thys/abacus"*)]; diff -r e7d845acb0a7 -r cd4ef33c8fb1 paper.pdf Binary file paper.pdf has changed diff -r e7d845acb0a7 -r cd4ef33c8fb1 thys/turing_basic.thy --- a/thys/turing_basic.thy Sat Jan 19 14:29:56 2013 +0000 +++ b/thys/turing_basic.thy Sat Jan 19 14:44:07 2013 +0000 @@ -147,6 +147,14 @@ where "tm_comp p1 p2 = ((adjust p1) @ (shift p2 (length p1 div 2)))" +lemma step_0 [simp]: + shows "step (0, (l, r)) p = (0, (l, r))" +by (case_tac p, simp) + +lemma steps_0 [simp]: + shows "steps (0, (l, r)) p n = (0, (l, r))" +by (induct n) (simp_all) + fun is_final :: "config \ bool" where @@ -157,54 +165,7 @@ shows "is_final (steps (s, l, r) (p, off) n)" using assms by (induct n) (auto) -fun - holds_for :: "(tape \ bool) \ config \ bool" ("_ holds'_for _" [100, 99] 100) -where - "P holds_for (s, l, r) = P (l, r)" -lemma is_final_holds[simp]: - assumes "is_final c" - shows "Q holds_for (steps c (p, off) n) = Q holds_for c" -using assms -apply(induct n) -apply(auto) -apply(case_tac [!] c) -apply(auto) -done - -type_synonym assert = "tape \ bool" - -definition - assert_imp :: "assert \ assert \ bool" ("_ \ _" [0, 0] 100) -where - "P \ Q \ \l r. P (l, r) \ Q (l, r)" - -lemma holds_for_imp: - assumes "P holds_for c" - and "P \ Q" - shows "Q holds_for c" -using assms unfolding assert_imp_def -by (case_tac c) (auto) - -definition - Hoare :: "assert \ tprog0 \ assert \ bool" ("({(1_)}/ (_)/ {(1_)})" 50) -where - "{P} p {Q} \ - (\l r. P (l, r) \ (\n. is_final (steps0 (1, (l, r)) p n) \ Q holds_for (steps0 (1, (l, r)) p n)))" - -lemma HoareI: - assumes "\l r. P (l, r) \ \n. is_final (steps0 (1, (l, r)) p n) \ Q holds_for (steps0 (1, (l, r)) p n)" - shows "{P} p {Q}" -unfolding Hoare_def using assms by auto - - -lemma step_0 [simp]: - shows "step (0, (l, r)) p = (0, (l, r))" -by (case_tac p, simp) - -lemma steps_0 [simp]: - shows "steps (0, (l, r)) p n = (0, (l, r))" -by (induct n) (simp_all) (* if the machine is in the halting state, there must have been a state just before the halting state *) @@ -480,119 +441,6 @@ apply(auto) done - -text {* - {P1} A {Q1} {P2} B {Q2} Q1 \ P2 - ----------------------------------- - {P1} A |+| B {Q2} -*} - - -lemma Hoare_plus_halt: - assumes aimpb: "Q1 \ P2" - and A_wf : "tm_wf (A, 0)" - and B_wf : "tm_wf (B, 0)" - and A_halt : "{P1} A {Q1}" - and B_halt : "{P2} B {Q2}" - shows "{P1} A |+| B {Q2}" -proof(rule HoareI) - fix l r - assume h: "P1 (l, r)" - then obtain n1 - where "is_final (steps0 (1, l, r) A n1)" and "Q1 holds_for (steps0 (1, l, r) A n1)" - using A_halt unfolding Hoare_def by auto - then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" - by(case_tac "steps0 (1, l, r) A n1") (auto) - then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')" - using A_wf by(rule_tac t_merge_pre_halt_same) (auto) - moreover - from c aimpb have "P2 holds_for (0, l', r')" - by (rule holds_for_imp) - then have "P2 (l', r')" by auto - then obtain n2 - where "is_final (steps0 (1, l', r') B n2)" and "Q2 holds_for (steps0 (1, l', r') B n2)" - using B_halt unfolding Hoare_def by auto - then obtain l'' r'' where "steps0 (1, l', r') B n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')" - by (case_tac "steps0 (1, l', r') B n2", auto) - then have "steps0 (Suc (length A div 2), l', r') (A |+| B) n2 = (0, l'', r'')" - by (rule_tac t_merge_second_halt_same) (auto simp: A_wf B_wf) - ultimately show - "\n. is_final (steps0 (1, l, r) (A |+| B) n) \ Q2 holds_for (steps0 (1, l, r) (A |+| B) n)" - using g - apply(rule_tac x = "stpa + n2" in exI) - apply(simp add: steps_add) - done -qed - -definition - Hoare_unhalt :: "assert \ tprog0 \ bool" ("({(1_)}/ (_))" 50) -where - "{P} p \ - (\l r. P (l, r) \ (\ n . \ (is_final (steps0 (1, (l, r)) p n))))" - -lemma Hoare_unhalt_I: - assumes "\l r. P (l, r) \ \ n. \ is_final (steps0 (1, (l, r)) p n)" - shows "{P} p" -unfolding Hoare_unhalt_def using assms by auto - -lemma Hoare_plus_unhalt: - fixes A B :: tprog0 - assumes aimpb: "Q1 \ P2" - and A_wf : "tm_wf (A, 0)" - and B_wf : "tm_wf (B, 0)" - and A_halt : "{P1} A {Q1}" - and B_uhalt : "{P2} B" - shows "{P1} (A |+| B)" -proof(rule_tac Hoare_unhalt_I) - fix l r - assume h: "P1 (l, r)" - then obtain n1 where a: "is_final (steps0 (1, l, r) A n1)" and b: "Q1 holds_for (steps0 (1, l, r) A n1)" - using A_halt unfolding Hoare_def by auto - then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" - by(case_tac "steps0 (1, l, r) A n1", auto) - then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')" - using A_wf - by(rule_tac t_merge_pre_halt_same, auto) - from c aimpb have "P2 holds_for (0, l', r')" - by(rule holds_for_imp) - from this have "P2 (l', r')" by auto - from this have e: "\ n. \ is_final (steps0 (Suc 0, l', r') B n) " - using B_uhalt unfolding Hoare_unhalt_def - by auto - from e show "\n. \ is_final (steps0 (1, l, r) (A |+| B) n)" - proof(rule_tac allI, case_tac "n > stpa") - fix n - assume h2: "stpa < n" - hence "\ is_final (steps0 (Suc 0, l', r') B (n - stpa))" - using e - apply(erule_tac x = "n - stpa" in allE) by simp - then obtain s'' l'' r'' where f: "steps0 (Suc 0, l', r') B (n - stpa) = (s'', l'', r'')" and g: "s'' \ 0" - apply(case_tac "steps0 (Suc 0, l', r') B (n - stpa)", auto) - done - have k: "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - stpa) = (s''+ length A div 2, l'', r'') " - using A_wf B_wf f g - apply(drule_tac t_merge_second_same, auto) - done - show "\ is_final (steps0 (1, l, r) (A |+| B) n)" - proof - - have "\ is_final (steps0 (1, l, r) (A |+| B) (stpa + (n - stpa)))" - using d k A_wf - apply(simp only: steps_add d, simp add: tm_wf.simps) - done - thus "\ is_final (steps0 (1, l, r) (A |+| B) n)" - using h2 by simp - qed - next - fix n - assume h2: "\ stpa < n" - with d show "\ is_final (steps0 (1, l, r) (A |+| B) n)" - apply(auto) - apply(subgoal_tac "\ d. stpa = n + d", auto) - apply(case_tac "(steps0 (Suc 0, l, r) (A |+| B) n)", simp) - apply(rule_tac x = "stpa - n" in exI, simp) - done - qed -qed end diff -r e7d845acb0a7 -r cd4ef33c8fb1 thys/turing_hoare.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/thys/turing_hoare.thy Sat Jan 19 14:44:07 2013 +0000 @@ -0,0 +1,173 @@ +theory turing_hoare +imports turing_basic +begin + + + +type_synonym assert = "tape \ bool" + +definition + assert_imp :: "assert \ assert \ bool" ("_ \ _" [0, 0] 100) +where + "P \ Q \ \l r. P (l, r) \ Q (l, r)" + + + +fun + holds_for :: "(tape \ bool) \ config \ bool" ("_ holds'_for _" [100, 99] 100) +where + "P holds_for (s, l, r) = P (l, r)" + +lemma is_final_holds[simp]: + assumes "is_final c" + shows "Q holds_for (steps c (p, off) n) = Q holds_for c" +using assms +apply(induct n) +apply(auto) +apply(case_tac [!] c) +apply(auto) +done + +lemma holds_for_imp: + assumes "P holds_for c" + and "P \ Q" + shows "Q holds_for c" +using assms unfolding assert_imp_def +by (case_tac c) (auto) + +definition + Hoare :: "assert \ tprog0 \ assert \ bool" ("({(1_)}/ (_)/ {(1_)})" 50) +where + "{P} p {Q} \ + (\l r. P (l, r) \ (\n. is_final (steps0 (1, (l, r)) p n) \ Q holds_for (steps0 (1, (l, r)) p n)))" + +lemma HoareI: + assumes "\l r. P (l, r) \ \n. is_final (steps0 (1, (l, r)) p n) \ Q holds_for (steps0 (1, (l, r)) p n)" + shows "{P} p {Q}" +unfolding Hoare_def using assms by auto + + +text {* + {P1} A {Q1} {P2} B {Q2} Q1 \ P2 + ----------------------------------- + {P1} A |+| B {Q2} +*} + + +lemma Hoare_plus_halt: + assumes aimpb: "Q1 \ P2" + and A_wf : "tm_wf (A, 0)" + and B_wf : "tm_wf (B, 0)" + and A_halt : "{P1} A {Q1}" + and B_halt : "{P2} B {Q2}" + shows "{P1} A |+| B {Q2}" +proof(rule HoareI) + fix l r + assume h: "P1 (l, r)" + then obtain n1 + where "is_final (steps0 (1, l, r) A n1)" and "Q1 holds_for (steps0 (1, l, r) A n1)" + using A_halt unfolding Hoare_def by auto + then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" + by(case_tac "steps0 (1, l, r) A n1") (auto) + then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')" + using A_wf by(rule_tac t_merge_pre_halt_same) (auto) + moreover + from c aimpb have "P2 holds_for (0, l', r')" + by (rule holds_for_imp) + then have "P2 (l', r')" by auto + then obtain n2 + where "is_final (steps0 (1, l', r') B n2)" and "Q2 holds_for (steps0 (1, l', r') B n2)" + using B_halt unfolding Hoare_def by auto + then obtain l'' r'' where "steps0 (1, l', r') B n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')" + by (case_tac "steps0 (1, l', r') B n2", auto) + then have "steps0 (Suc (length A div 2), l', r') (A |+| B) n2 = (0, l'', r'')" + by (rule_tac t_merge_second_halt_same) (auto simp: A_wf B_wf) + ultimately show + "\n. is_final (steps0 (1, l, r) (A |+| B) n) \ Q2 holds_for (steps0 (1, l, r) (A |+| B) n)" + using g + apply(rule_tac x = "stpa + n2" in exI) + apply(simp add: steps_add) + done +qed + +definition + Hoare_unhalt :: "assert \ tprog0 \ bool" ("({(1_)}/ (_))" 50) +where + "{P} p \ + (\l r. P (l, r) \ (\ n . \ (is_final (steps0 (1, (l, r)) p n))))" + +lemma Hoare_unhalt_I: + assumes "\l r. P (l, r) \ \ n. \ is_final (steps0 (1, (l, r)) p n)" + shows "{P} p" +unfolding Hoare_unhalt_def using assms by auto + +lemma Hoare_plus_unhalt: + fixes A B :: tprog0 + assumes aimpb: "Q1 \ P2" + and A_wf : "tm_wf (A, 0)" + and B_wf : "tm_wf (B, 0)" + and A_halt : "{P1} A {Q1}" + and B_uhalt : "{P2} B" + shows "{P1} (A |+| B)" +proof(rule_tac Hoare_unhalt_I) + fix l r + assume h: "P1 (l, r)" + then obtain n1 where a: "is_final (steps0 (1, l, r) A n1)" and b: "Q1 holds_for (steps0 (1, l, r) A n1)" + using A_halt unfolding Hoare_def by auto + then obtain l' r' where "steps0 (1, l, r) A n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')" + by(case_tac "steps0 (1, l, r) A n1", auto) + then obtain stpa where d: "steps0 (1, l, r) (A |+| B) stpa = (Suc (length A div 2), l', r')" + using A_wf + by(rule_tac t_merge_pre_halt_same, auto) + from c aimpb have "P2 holds_for (0, l', r')" + by(rule holds_for_imp) + from this have "P2 (l', r')" by auto + from this have e: "\ n. \ is_final (steps0 (Suc 0, l', r') B n) " + using B_uhalt unfolding Hoare_unhalt_def + by auto + from e show "\n. \ is_final (steps0 (1, l, r) (A |+| B) n)" + proof(rule_tac allI, case_tac "n > stpa") + fix n + assume h2: "stpa < n" + hence "\ is_final (steps0 (Suc 0, l', r') B (n - stpa))" + using e + apply(erule_tac x = "n - stpa" in allE) by simp + then obtain s'' l'' r'' where f: "steps0 (Suc 0, l', r') B (n - stpa) = (s'', l'', r'')" and g: "s'' \ 0" + apply(case_tac "steps0 (Suc 0, l', r') B (n - stpa)", auto) + done + have k: "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - stpa) = (s''+ length A div 2, l'', r'') " + using A_wf B_wf f g + apply(drule_tac t_merge_second_same, auto) + done + show "\ is_final (steps0 (1, l, r) (A |+| B) n)" + proof - + have "\ is_final (steps0 (1, l, r) (A |+| B) (stpa + (n - stpa)))" + using d k A_wf + apply(simp only: steps_add d, simp add: tm_wf.simps) + done + thus "\ is_final (steps0 (1, l, r) (A |+| B) n)" + using h2 by simp + qed + next + fix n + assume h2: "\ stpa < n" + with d show "\ is_final (steps0 (1, l, r) (A |+| B) n)" + apply(auto) + apply(subgoal_tac "\ d. stpa = n + d", auto) + apply(case_tac "(steps0 (Suc 0, l, r) (A |+| B) n)", simp) + apply(rule_tac x = "stpa - n" in exI, simp) + done + qed +qed + +lemma Hoare_weak: + fixes p::tprog0 + assumes a: "{P} p {Q}" + and b: "P' \ P" + and c: "Q \ Q'" + shows "{P'} p {Q'}" +using assms +unfolding Hoare_def assert_imp_def +by (blast intro: holds_for_imp[simplified assert_imp_def]) + +end \ No newline at end of file diff -r e7d845acb0a7 -r cd4ef33c8fb1 thys/uncomputable.thy --- a/thys/uncomputable.thy Sat Jan 19 14:29:56 2013 +0000 +++ b/thys/uncomputable.thy Sat Jan 19 14:44:07 2013 +0000 @@ -6,7 +6,7 @@ header {* Undeciablity of the {\em Halting problem} *} theory uncomputable -imports Main turing_basic +imports Main turing_hoare begin text {* @@ -1143,15 +1143,6 @@ apply(drule_tac length_eq, simp) done -lemma Hoare_weak: - fixes p::tprog0 - assumes a: "{P} p {Q}" - and b: "P' \ P" - and c: "Q \ Q'" - shows "{P'} p {Q'}" -using assms -unfolding Hoare_def assert_imp_def -by (blast intro: holds_for_imp[simplified assert_imp_def]) text {* The following locale specifies that TM @{text "H"} can be used to solve