--- a/thys/turing_basic.thy Fri Jan 18 13:56:35 2013 +0000
+++ b/thys/turing_basic.thy Fri Jan 18 23:59:33 2013 +0000
@@ -176,9 +176,10 @@
type_synonym assert = "tape \<Rightarrow> bool"
-definition assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100)
- where
- "assert_imp P Q = (\<forall>l r. P (l, r) \<longrightarrow> Q (l, r))"
+definition
+ assert_imp :: "assert \<Rightarrow> assert \<Rightarrow> bool" ("_ \<mapsto> _" [0, 0] 100)
+where
+ "P \<mapsto> Q = (\<forall>l r. P (l, r) \<longrightarrow> Q (l, r))"
lemma holds_for_imp:
assumes "P holds_for c"
@@ -186,17 +187,6 @@
shows "Q holds_for c"
using assms unfolding assert_imp_def by (case_tac c, auto)
-lemma test:
- assumes "is_final (steps (1, (l, r)) p n1)"
- and "is_final (steps (1, (l, r)) p n2)"
- shows "Q holds_for (steps (1, (l, r)) p n1) \<longleftrightarrow> Q holds_for (steps (1, (l, r)) p n2)"
-proof -
- obtain n3 where "n1 = n2 + n3 \<or> n2 = n1 + n3"
- by (metis le_iff_add nat_le_linear)
- with assms show "Q holds_for (steps (1, (l, r)) p n1) \<longleftrightarrow> Q holds_for (steps (1, (l, r)) p n2)"
- by(case_tac p) (auto)
-qed
-
definition
Hoare :: "assert \<Rightarrow> tprog \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" 50)
where
@@ -208,11 +198,6 @@
shows "{P} p {Q}"
unfolding Hoare_def using assms by auto
-text {*
-{P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2
------------------------------------
- {P1} A |+| B {Q2}
-*}
lemma step_0 [simp]:
shows "step (0, (l, r)) p = (0, (l, r))"
@@ -504,6 +489,14 @@
apply(auto)
done
+
+text {*
+ {P1} A {Q1} {P2} B {Q2} Q1 \<mapsto> P2
+ -----------------------------------
+ {P1} A |+| B {Q2}
+*}
+
+
lemma Hoare_plus_halt:
assumes aimpb: "Q1 \<mapsto> P2"
and A_wf : "tm_wf (A, 0)"
@@ -514,27 +507,27 @@
proof(rule HoareI)
fix l r
assume h: "P1 (l, r)"
- then obtain n1 where a: "is_final (steps (1, l, r) (A, 0) n1)" and b: "Q1 holds_for (steps (1, l, r) (A, 0) n1)"
+ then obtain n1
+ where "is_final (steps (1, l, r) (A, 0) n1)" and "Q1 holds_for (steps (1, l, r) (A, 0) n1)"
using A_halt unfolding Hoare_def by auto
then obtain l' r' where "steps (1, l, r) (A, 0) n1 = (0, l', r')" and c: "Q1 holds_for (0, l', r')"
- by(case_tac "steps (1, l, r) (A, 0) n1", auto)
+ by(case_tac "steps (1, l, r) (A, 0) n1") (auto)
then obtain stpa where d: "steps (1, l, r) (A |+| B, 0) stpa = (Suc (length A div 2), l', r')"
- using A_wf
- by(rule_tac t_merge_pre_halt_same, auto)
+ 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)
- from this have "P2 (l', r')" by auto
- from this obtain n2 where e: "is_final (steps (1, l', r') (B, 0) n2)" and f: "Q2 holds_for (steps (1, l', r') (B, 0) n2)"
- using B_halt unfolding Hoare_def
- by auto
+ by (rule holds_for_imp)
+ then have "P2 (l', r')" by auto
+ then obtain n2
+ where "is_final (steps (1, l', r') (B, 0) n2)" and "Q2 holds_for (steps (1, l', r') (B, 0) n2)"
+ using B_halt unfolding Hoare_def by auto
then obtain l'' r'' where "steps (1, l', r') (B, 0) n2 = (0, l'', r'')" and g: "Q2 holds_for (0, l'', r'')"
- by(case_tac "steps (1, l', r') (B, 0) n2", auto)
- from this have "steps (Suc (length A div 2), l', r') (A |+| B, 0) n2
- = (0, l'', r'')"
- apply(rule_tac t_merge_second_halt_same, auto simp: A_wf B_wf)
- done
- thus "\<exists>n. is_final (steps (1, l, r) (A |+| B, 0) n) \<and> Q2 holds_for (steps (1, l, r) (A |+| B, 0) n)"
- using d g
+ by (case_tac "steps (1, l', r') (B, 0) n2", auto)
+ then have "steps (Suc (length A div 2), l', r') (A |+| B, 0) n2 = (0, l'', r'')"
+ by (rule_tac t_merge_second_halt_same) (auto simp: A_wf B_wf)
+ ultimately show
+ "\<exists>n. is_final (steps (1, l, r) (A |+| B, 0) n) \<and> Q2 holds_for (steps (1, l, r) (A |+| B, 0) n)"
+ using g
apply(rule_tac x = "stpa + n2" in exI)
apply(simp add: steps_add)
done