# HG changeset patch # User Christian Urban # Date 1358865536 0 # Node ID 7edbd5657702a19f31cf7892517ac726a4890ef2 # Parent c8ff97d9f8da0a8c9db38721ab091cacfa777b9d updated files diff -r c8ff97d9f8da -r 7edbd5657702 Paper/Paper.thy --- a/Paper/Paper.thy Sun Jan 20 16:01:16 2013 +0000 +++ b/Paper/Paper.thy Tue Jan 22 14:38:56 2013 +0000 @@ -1,6 +1,6 @@ (*<*) theory Paper -imports "../thys/uncomputable" +imports "../thys/recursive" begin (* @@ -66,7 +66,7 @@ The only satisfying way out of this problem in a theorem prover based on classical logic is to formalise a theory of computability. Norrish -provided such a formalisation for the HOL4. He choose +provided such a formalisation for the HOL. He choose the $\lambda$-calculus as the starting point for his formalisation of computability theory, because of its ``simplicity'' \cite[Page 297]{Norrish11}. Part of his formalisation is a clever infrastructure @@ -90,13 +90,13 @@ of register machines) and recursive functions. To see the difficulties involved with this work, one has to understand that Turing machine programs can be completely \emph{unstructured}, behaving -similar to Basic's infamous goto \cite{Dijkstra68}. This precludes in the +similar Basic programs involving the infamous goto \cite{Dijkstra68}. This precludes in the general case a compositional Hoare-style reasoning about Turing -programs. We provide such Hoare-rules for when it is possible to +programs. We provide such Hoare-rules for when it \emph{is} possible to reason in a compositional manner (which is fortunately quite often), but also tackle the more complicated case when we translate abacus programs into -Turing programs. This aspect of reasoning about computability theory -is usually completely left out in the informal literature, e.g.~\cite{Boolos87}. +Turing programs. These difficulties when reasoning about computability theory +are usually completely left out in the informal literature, e.g.~\cite{Boolos87}. %To see the difficulties %involved with this work, one has to understand that interactive diff -r c8ff97d9f8da -r 7edbd5657702 Paper/ROOT.ML --- a/Paper/ROOT.ML Sun Jan 20 16:01:16 2013 +0000 +++ b/Paper/ROOT.ML Tue Jan 22 14:38:56 2013 +0000 @@ -1,7 +1,9 @@ no_document -use_thys ["../thys/turing_basic", +use_thys ["../thys/turing_basic"(*, "../thys/turing_hoare", - "../thys/uncomputable"(*, - "../thys/abacus"*)]; + "../thys/uncomputable", + "../thys/abacus", + "../thys/rec_def", + "../thys/recursive"*)]; use_thys ["Paper"] diff -r c8ff97d9f8da -r 7edbd5657702 ROOT.ML --- a/ROOT.ML Sun Jan 20 16:01:16 2013 +0000 +++ b/ROOT.ML Tue Jan 22 14:38:56 2013 +0000 @@ -12,10 +12,9 @@ *) no_document -use_thys ["turing_basic", - "uncomputable", - "abacus", - "rec_def", - "recursive", - "UF", - "UTM"] +use_thys ["thys/turing_basic"(*, + "thys/truing_hoare", + "thys/uncomputable", + "thys/abacus", + "thys/rec_def", + "thys/recursive"*)] diff -r c8ff97d9f8da -r 7edbd5657702 paper.pdf Binary file paper.pdf has changed diff -r c8ff97d9f8da -r 7edbd5657702 thys/abacus.thy --- a/thys/abacus.thy Sun Jan 20 16:01:16 2013 +0000 +++ b/thys/abacus.thy Tue Jan 22 14:38:56 2013 +0000 @@ -4950,7 +4950,7 @@ by(case_tac "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp", auto) then have "is_final (steps (s'', l'', r'') (tp @ shift (mopup n) off, 0) diff)" - by(auto intro: is_final_steps) + by(auto intro: after_is_final) then have "is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stpa)" using e by(simp add: steps_add f) diff -r c8ff97d9f8da -r 7edbd5657702 thys/turing_basic.thy --- a/thys/turing_basic.thy Sun Jan 20 16:01:16 2013 +0000 +++ b/thys/turing_basic.thy Tue Jan 22 14:38:56 2013 +0000 @@ -114,12 +114,26 @@ shows "is_final (s, tp) = (s = 0)" by (case_tac tp) (auto) -lemma is_final_steps: - assumes "is_final (s, l, r)" - shows "is_final (steps (s, l, r) (p, off) n)" +lemma after_is_final: + assumes "is_final c" + shows "is_final (steps c p n)" using assms -by (induct n) (auto) +apply(induct n) +apply(case_tac [!] c) +apply(auto) +done +lemma not_is_final: + assumes a: "\ is_final (steps c p n1)" + and b: "n2 \ n1" + shows "\ is_final (steps c p n2)" +proof (rule notI) + obtain n3 where eq: "n1 = n2 + n3" using b by (metis le_iff_add) + assume "is_final (steps c p n2)" + then have "is_final (steps c p n1)" unfolding eq + by (simp add: after_is_final) + with a show "False" by simp +qed (* if the machine is in the halting state, there must have been a state just before the halting state *) @@ -212,7 +226,7 @@ shows "length (A |+| B) = length A + length B" by auto -lemma tm_comp_step_aux: +lemma tm_comp_step: assumes unfinal: "\ is_final (step0 c A)" shows "step0 c (A |+| B) = step0 c A" proof - @@ -228,7 +242,7 @@ then show "step0 c (A |+| B) = step0 c A" by (simp add: eq) qed -lemma tm_comp_step: +lemma tm_comp_steps: assumes "\ is_final (steps0 c A n)" shows "steps0 c (A |+| B) n = steps0 c A n" using assms @@ -247,7 +261,7 @@ have "steps0 c (A |+| B) (Suc n) = step0 (steps0 c (A |+| B) n) (A |+| B)" by (simp only: step_red) also have "... = step0 (steps0 c A n) (A |+| B)" by (simp only: ih[OF fin2]) - also have "... = step0 (steps0 c A n) A" by (simp only: tm_comp_step_aux[OF fin1]) + also have "... = step0 (steps0 c A n) A" by (simp only: tm_comp_step[OF fin1]) finally show "steps0 c (A |+| B) (Suc n) = steps0 c A (Suc n)" by (simp only: step_red) qed @@ -319,7 +333,7 @@ obtain stp' where fin: "\ is_final (steps0 (1, tp) A stp')" and h: "steps0 (1, tp) A (Suc stp') = (0, tp')" using before_final[OF a_ht] by blast from fin have h1:"steps0 (1, tp) (A |+| B) stp' = steps0 (1, tp) A stp'" - by (rule tm_comp_step) + by (rule tm_comp_steps) from h have h2: "step0 (steps0 (1, tp) A stp') A = (0, tp')" by (simp only: step_red) diff -r c8ff97d9f8da -r 7edbd5657702 thys/turing_hoare.thy --- a/thys/turing_hoare.thy Sun Jan 20 16:01:16 2013 +0000 +++ b/thys/turing_hoare.thy Tue Jan 22 14:38:56 2013 +0000 @@ -2,11 +2,6 @@ imports turing_basic begin -declare step.simps[simp del] -declare steps.simps[simp del] -declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] -declare tm_wf.simps[simp del] - type_synonym assert = "tape \ bool" @@ -20,9 +15,35 @@ where "P holds_for (s, l, r) = P (l, r)" +(* halting case *) +definition + Hoare :: "assert \ tprog0 \ assert \ bool" ("({(1_)}/ (_)/ {(1_)})" [50, 49] 50) +where + "{P} p {Q} \ + (\tp. P tp \ (\n. is_final (steps0 (1, tp) p n) \ Q holds_for (steps0 (1, tp) p n)))" + +(* not halting case *) +definition + Hoare_unhalt :: "assert \ tprog0 \ bool" ("({(1_)}/ (_)) \" [50, 49] 50) +where + "{P} p \ \ (\tp. P tp \ (\ n . \ (is_final (steps0 (1, tp) 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 Hoare_unhalt_I: + assumes "\l r n. P (l, r) \ \ is_final (steps0 (1, (l, r)) p n)" + shows "{P} p \" +unfolding Hoare_unhalt_def +using assms by auto + lemma is_final_holds[simp]: assumes "is_final c" - shows "Q holds_for (steps c (p, off) n) = Q holds_for c" + shows "Q holds_for (steps c p n) = Q holds_for c" using assms apply(induct n) apply(auto) @@ -30,24 +51,6 @@ 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 A, B well-formed @@ -57,118 +60,103 @@ lemma Hoare_plus_halt: - assumes aimpb: "Q1 \ P2" + assumes a_imp: "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 tm_comp_pre_halt_same) (auto) + then obtain n1 l' r' + where "is_final (steps0 (1, l, r) A n1)" + and a1: "Q1 holds_for (steps0 (1, l, r) A n1)" + and a2: "steps0 (1, l, r) A n1 = (0, l', r')" + using A_halt unfolding Hoare_def + by (metis is_final_eq surj_pair) + then obtain n2 + where "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')" + using A_wf by (rule_tac tm_comp_pre_halt_same) 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) + from a1 a2 a_imp have "P2 (l', r')" by (simp add: assert_imp_def) + then obtain n3 l'' r'' + where "is_final (steps0 (1, l', r') B n3)" + and b1: "Q2 holds_for (steps0 (1, l', r') B n3)" + and b2: "steps0 (1, l', r') B n3 = (0, l'', r'')" + using B_halt unfolding Hoare_def + by (metis is_final_eq surj_pair) + then have "steps0 (Suc (length A div 2), l', r') (A |+| B) n3 = (0, l'', r'')" + using A_wf by (rule_tac t_merge_second_halt_same) 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 + using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp) 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 +text {* + {P1} A {Q1} {P2} B loops Q1 \ P2 A well-formed + ------------------------------------------------------ + {P1} A |+| B loops +*} lemma Hoare_plus_unhalt: - fixes A B :: tprog0 - assumes aimpb: "Q1 \ P2" + assumes a_imp: "Q1 \ P2" and A_wf : "tm_wf (A, 0)" - and B_wf : "tm_wf (B, 0)" (* probably not needed *) and A_halt : "{P1} A {Q1}" - and B_uhalt : "{P2} B" - shows "{P1} (A |+| B)" + and B_uhalt : "{P2} B \" + shows "{P1} (A |+| B) \" proof(rule_tac Hoare_unhalt_I) - fix l r + fix n 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 tm_comp_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 + then obtain n1 l' r' + where a: "is_final (steps0 (1, l, r) A n1)" + and b: "Q1 holds_for (steps0 (1, l, r) A n1)" + and c: "steps0 (1, l, r) A n1 = (0, l', r')" + using A_halt unfolding Hoare_def + by (metis is_final_eq surj_pair) + then obtain n2 where eq: "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')" + using A_wf by (rule_tac tm_comp_pre_halt_same) + then show "\ is_final (steps0 (1, l, r) (A |+| B) n)" + proof(cases "n2 \ n") + case True + from b c a_imp have "P2 (l', r')" by (simp add: assert_imp_def) + then have "\ n. \ is_final (steps0 (1, l', r') B n) " + using B_uhalt unfolding Hoare_unhalt_def by simp + then have "\ is_final (steps0 (Suc 0, l', r') B (n - n2))" by auto + then obtain s'' l'' r'' + where "steps0 (Suc 0, l', r') B (n - n2) = (s'', l'', r'')" + and "\ is_final (s'', l'', r'')" by (metis surj_pair) + then have "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - n2) = (s''+ length A div 2, l'', r'')" + using A_wf by (auto dest: t_merge_second_same simp del: steps.simps) + then have "\ is_final (steps0 (1, l, r) (A |+| B) (n2 + (n - n2)))" + using A_wf by (simp only: steps_add eq) (simp add: tm_wf.simps) + then show "\ is_final (steps0 (1, l, r) (A |+| B) n)" + using `n2 \ n` by simp + next + case False + then obtain n3 where "n = n2 - n3" + by (metis diff_le_self le_imp_diff_is_add nat_add_commute nat_le_linear) + moreover + with eq show "\ is_final (steps0 (1, l, r) (A |+| B) n)" + by (simp add: not_is_final[where ?n1.0="n2"]) 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]) +by (metis holds_for.simps surj_pair) + + +declare step.simps[simp del] +declare steps.simps[simp del] +declare tm_comp.simps [simp del] adjust.simps[simp del] shift.simps[simp del] +declare tm_wf.simps[simp del] + + end \ No newline at end of file diff -r c8ff97d9f8da -r 7edbd5657702 thys/uncomputable.thy --- a/thys/uncomputable.thy Sun Jan 20 16:01:16 2013 +0000 +++ b/thys/uncomputable.thy Tue Jan 22 14:38:56 2013 +0000 @@ -996,8 +996,6 @@ next show "tm_wf (tcopy_init |+| tcopy_loop, 0)" by auto next - show "tm_wf (tcopy_end, 0)" by auto -next assume "0 < x" thus "{inv_init1 x} (tcopy_init |+| tcopy_loop) {inv_loop0 x}" proof(rule_tac Hoare_plus_halt) @@ -1008,8 +1006,6 @@ next show "tm_wf (tcopy_init, 0)" by auto next - show "tm_wf (tcopy_loop, 0)" by auto - next assume "0 < x" thus "{inv_init1 x} tcopy_init {inv_init0 x}" by(erule_tac init_correct) @@ -1345,7 +1341,7 @@ let ?Q2 = "\(l, r). (\nd. l = Bk \ nd) \ r = [Oc]" let ?P3 = ?Q2 assume h: "haltP (?tcontr, 0) [code ?tcontr]" - have "{?P1} ?tcontr" + have "{?P1} ?tcontr \" proof(rule_tac Hoare_plus_unhalt, auto) show "?Q2 \ ?P3" apply(simp add: assert_imp_def) @@ -1384,7 +1380,7 @@ done qed next - show "{?P3} dither" + show "{?P3} dither \" using Hoare_unhalt_def proof(auto) fix nd n