# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1358553573 0
# Node ID 6725c9c026f61d8f171fbc728834a38ab88ee3fe
# Parent  816e84ca16d641e5a98fe872141d8dde1be79d95
slight update

diff -r 816e84ca16d6 -r 6725c9c026f6 paper.pdf
Binary file paper.pdf has changed
diff -r 816e84ca16d6 -r 6725c9c026f6 thys/turing_basic.thy
--- 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