# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1395663355 0
# Node ID b88fc9da19702a65fa245e2c64b0896d019018cf
# Parent  dcbf7888a070164af9282555193cd36b5c45ef16
small modifications

diff -r dcbf7888a070 -r b88fc9da1970 thys/Hoare_tm.thy
--- a/thys/Hoare_tm.thy	Mon Mar 24 11:39:39 2014 +0000
+++ b/thys/Hoare_tm.thy	Mon Mar 24 12:15:55 2014 +0000
@@ -12,21 +12,6 @@
   Pretty.block (Pretty.commas (map (Syntax.pretty_term ctxt) trms))
 *}
 
-lemma int_add_C :"x + (y::int) = y + x"
-  by simp
-
-lemma int_add_A : "(x + y) + z = x + (y + (z::int))"
-  by simp
-
-lemma int_add_LC: "x + (y + (z::int)) = y + (x + z)"
-  by simp
-
-lemmas int_add_ac = int_add_A int_add_C int_add_LC
-
-method_setup prune = 
-  {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} 
-  "pruning parameters"
-
 ML {*
 structure StepRules = Named_Thms
   (val name = @{binding "step"}
@@ -43,6 +28,22 @@
 
 setup {* FwdRules.setup *}
 
+method_setup prune = 
+  {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} 
+  "pruning parameters"
+
+lemma int_add_C :"x + (y::int) = y + x"
+  by simp
+
+lemma int_add_A : "(x + y) + z = x + (y + (z::int))"
+  by simp
+
+lemma int_add_LC: "x + (y + (z::int)) = y + (x + z)"
+  by simp
+
+lemmas int_add_ac = int_add_A int_add_C int_add_LC
+
+
 section {* Operational Semantics of TM *}
 
 datatype taction = W0 | W1 | L | R
@@ -55,11 +56,13 @@
 
 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)"
 
-fun next_tape :: "taction \<Rightarrow> (int \<times>  (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times>  (int \<rightharpoonup> Block))"
-where "next_tape W0 (pos, m) = (pos, m(pos \<mapsto> Bk))" |
-      "next_tape W1 (pos, m) = (pos, m(pos \<mapsto> Oc))" |
-      "next_tape L  (pos, m) = (pos - 1, m)" |
-      "next_tape R  (pos, m) = (pos + 1, m)"
+fun 
+  next_tape :: "taction \<Rightarrow> (int \<times>  (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times>  (int \<rightharpoonup> Block))"
+where 
+  "next_tape W0 (pos, m) = (pos, m(pos \<mapsto> Bk))" |
+  "next_tape W1 (pos, m) = (pos, m(pos \<mapsto> Oc))" |
+  "next_tape L  (pos, m) = (pos - 1, m)" |
+  "next_tape R  (pos, m) = (pos + 1, m)"
 
 fun tstep :: "tconf \<Rightarrow> tconf"
   where "tstep (faults, prog, pc, pos, m) = 
@@ -88,7 +91,7 @@
                           s =  (faults, prog, pc, pos, m) \<longrightarrow>
                           prog pc  = None \<longrightarrow> P (faults + 1, prog, pc, pos, m))
                    )"
-  by (case_tac s, auto split:option.splits Block.splits)
+  by (cases s) (auto split: option.splits Block.splits)
 
 datatype tresource = 
     TM int Block
@@ -111,6 +114,8 @@
 
 interpretation tm: sep_exec tstep trset_of .
 
+
+
 section {* Assembly language for TMs and its program logic *}
 
 subsection {* The assembly language *}
@@ -520,18 +525,24 @@
   show ?thesis by auto
 qed
 
+
 subsection {* Basic assertions for TM *}
 
+(* ones between tape position i and j *)
 function ones :: "int \<Rightarrow> int \<Rightarrow> tassert" where
-  "ones i j = (if j < i then <(i = j + 1)> else
-                (one i) ** ones (i + 1) j)"
+  "ones i j = (if j < i then <(i = j + 1)> 
+               else (one i) \<and>* ones (i + 1) j)"
 by auto
-termination by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") auto
-
-lemma ones_base_simp: "j < i \<Longrightarrow> ones i j = <(i = j + 1)>"
+
+termination 
+  by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") auto
+
+lemma ones_base_simp: 
+  "j < i \<Longrightarrow> ones i j = <(i = j + 1)>"
   by simp
 
-lemma ones_step_simp: "\<not> j < i \<Longrightarrow> ones i j =  ((one i) ** ones (i + 1) j)"
+lemma ones_step_simp: 
+  "\<not> j < i \<Longrightarrow> ones i j =  ((one i) \<and>* ones (i + 1) j)"
   by simp
 
 lemmas ones_simps = ones_base_simp ones_step_simp
@@ -539,9 +550,8 @@
 declare ones.simps [simp del] ones_simps [simp]
 
 lemma ones_induct [case_names Base Step]:
-  fixes P i j
   assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)"
-  and h2: "\<And> i j. \<lbrakk>\<not> j < i; P (i + 1) j (ones (i + 1) j)\<rbrakk> \<Longrightarrow> P i j ((one i) ** ones (i + 1) j)"
+  and h2: "\<And> i j. \<lbrakk>\<not> j < i; P (i + 1) j (ones (i + 1) j)\<rbrakk> \<Longrightarrow> P i j ((one i) \<and>* ones (i + 1) j)"
   shows "P i j (ones i j)"
 proof(induct i j rule:ones.induct)
   fix i j 
@@ -560,8 +570,8 @@
 qed
 
 function ones' ::  "int \<Rightarrow> int \<Rightarrow> tassert" where
-  "ones' i j = (if j < i then <(i = j + 1)> else
-                ones' i (j - 1) ** one j)"
+  "ones' i j = (if j < i then <(i = j + 1)> 
+                else ones' i (j - 1) \<and>* one j)"
 by auto
 termination by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") auto
 
@@ -584,7 +594,6 @@
 qed
 
 lemma ones_rev_induct [case_names Base Step]:
-  fixes P i j
   assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)"
   and h2: "\<And> i j. \<lbrakk>\<not> j < i; P i (j - 1) (ones i (j - 1))\<rbrakk> \<Longrightarrow> P i j ((ones i (j - 1)) ** one j)"
   shows "P i j (ones i j)"
@@ -622,7 +631,6 @@
 lemmas zeros_simps [simp] = zeros_base_simp zeros_step_simp
 
 lemma zeros_induct [case_names Base Step]:
-  fixes P i j
   assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)"
   and h2: "\<And> i j. \<lbrakk>\<not> j < i; P (i + 1) j (zeros (i + 1) j)\<rbrakk> \<Longrightarrow> 
                                    P i j ((zero i) ** zeros (i + 1) j)"
@@ -643,7 +651,7 @@
   qed
 qed
 
-lemma zeros_rev: "\<not> j < i \<Longrightarrow> (zeros i j) = ((zeros i (j - 1)) ** zero j)"
+lemma zeros_rev: "\<not> j < i \<Longrightarrow> (zeros i j) = ((zeros i (j - 1)) \<and>* zero j)"
 proof(induct i j rule:zeros_induct)
   case (Base i j)
   thus ?case by auto
@@ -660,7 +668,6 @@
 qed
 
 lemma zeros_rev_induct [case_names Base Step]:
-  fixes P i j
   assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)"
   and h2: "\<And> i j. \<lbrakk>\<not> j < i; P i (j - 1) (zeros i (j - 1))\<rbrakk> \<Longrightarrow> 
                        P i j ((zeros i (j - 1)) ** zero j)"
@@ -682,7 +689,7 @@
   qed
 qed
 
-definition "rep i j k = ((ones i (i + (int k))) ** <(j = i + int k)>)"
+definition "rep i j k = ((ones i (i + (int k))) \<and>* <(j = i + int k)>)"
 
 fun reps :: "int \<Rightarrow> int \<Rightarrow> nat list\<Rightarrow> tassert"
   where
@@ -892,6 +899,7 @@
   qed
 qed
 
+
 subsection {* A theory of list extension *}
 
 definition "list_ext n xs = xs @ replicate ((Suc n) - length xs) 0"
@@ -925,6 +933,7 @@
 lemma nth_app: "length xs \<le> a \<Longrightarrow> (xs @ ys)!a = ys!(a - length xs)"
   by (metis not_less nth_append)
 
+(* FIXME in Hoare_gen? *)
 lemma pred_exI: 
   assumes "(P(x) \<and>* r) s"
   shows "((EXS x. P(x)) \<and>* r) s"
diff -r dcbf7888a070 -r b88fc9da1970 thys/My_block.thy
--- a/thys/My_block.thy	Mon Mar 24 11:39:39 2014 +0000
+++ b/thys/My_block.thy	Mon Mar 24 12:15:55 2014 +0000
@@ -7,11 +7,16 @@
 begin
 
 ML {*
-  val my_block = Proof.assert_backward #> Proof.enter_forward #> Proof.begin_block
+  val my_block = 
+    Proof.assert_backward 
+    #> Proof.enter_forward 
+    #> Proof.begin_block
 *}
 
 ML {*
-  val my_block_end = Proof.end_block #> Proof.enter_backward
+  val my_block_end = 
+    Proof.end_block 
+    #> Proof.enter_backward
 *}
 
 ML {*
@@ -23,7 +28,10 @@
 
 ML {*
   fun my_note x = 
-     Proof.assert_backward #> Proof.enter_forward #> Proof.note_thmss_cmd x #> Proof.enter_backward
+    Proof.assert_backward 
+    #> Proof.enter_forward 
+    #> Proof.note_thmss_cmd x 
+    #> Proof.enter_backward
 *}
 
 ML {*