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