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