# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1395409760 0
# Node ID 6c722e960f2ed86aa066cd0e226b51a25942bf59
# Parent  ceb0bdc9989367c7be4a582254fe770b37352b4f
minor changes

diff -r ceb0bdc99893 -r 6c722e960f2e Separation_Algebra/Separation_Algebra.thy
--- a/Separation_Algebra/Separation_Algebra.thy	Fri Mar 21 21:40:51 2014 +0800
+++ b/Separation_Algebra/Separation_Algebra.thy	Fri Mar 21 13:49:20 2014 +0000
@@ -35,7 +35,7 @@
   pred_K :: "'b \<Rightarrow> 'a \<Rightarrow> 'b" ("\<langle>_\<rangle>") where
   "\<langle>f\<rangle> \<equiv> \<lambda>s. f"
 
-(* abbreviation *)
+(* was an abbreviation *)
   definition pred_ex :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "EXS " 10) where
   "EXS x. P x \<equiv> \<lambda>s. \<exists>x. P x s"
 
@@ -216,7 +216,6 @@
   then obtain x y z where "P x" and "Q y" and "R z"
                       and "x ## y" and "x ## z" and "y ## z" and "x ## y + z"
                       and "h = x + y + z"
-    thm sep_disj_addD
     by (fastforce elim!: sep_conjE simp: sep_add_ac dest: sep_disj_addD)
   thus "?lhs h"
     by (metis sep_conj_def sep_disj_addI1)
diff -r ceb0bdc99893 -r 6c722e960f2e thys/Hoare_gen.thy
--- a/thys/Hoare_gen.thy	Fri Mar 21 21:40:51 2014 +0800
+++ b/thys/Hoare_gen.thy	Fri Mar 21 13:49:20 2014 +0000
@@ -12,7 +12,7 @@
 where "pasrt b = (\<lambda> s . s = 0 \<and> b)"
 
 
-(* smae as sep.mult.left_commute *)
+(* same as sep.mult.left_commute *)
 lemma sep_conj_cond1: 
   "(p \<and>* <cond> \<and>* q) = (<cond> \<and>* p \<and>* q)"
   by (rule sep.mult.left_commute)
@@ -289,15 +289,15 @@
 by (smt IHoare_def code_exI)
 
 lemma I_code_extension: 
-  assumes h: "I. \<lbrace> P \<rbrace> c \<lbrace> Q \<rbrace>"
-  shows "I. \<lbrace> P \<rbrace> c ** e \<lbrace> Q \<rbrace>"
+  assumes h: "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"
+  shows "I. \<lbrace>P\<rbrace> c \<and>* e \<lbrace>Q\<rbrace>"
   using h
   by (smt IHoare_def sep_exec.code_extension)
 
 lemma I_composition: 
   assumes h1: "I. \<lbrace>P\<rbrace> c1 \<lbrace>Q\<rbrace>"
     and h2: "I. \<lbrace>Q\<rbrace> c2 \<lbrace>R\<rbrace>"
-  shows "I. \<lbrace>P\<rbrace> c1 ** c2 \<lbrace>R\<rbrace>"
+  shows "I. \<lbrace>P\<rbrace> c1 \<and>* c2 \<lbrace>R\<rbrace>"
   using h1 h2
 by (smt IHoare_def sep_exec.composition)
 
diff -r ceb0bdc99893 -r 6c722e960f2e thys/Hoare_tm.thy
--- a/thys/Hoare_tm.thy	Fri Mar 21 21:40:51 2014 +0800
+++ b/thys/Hoare_tm.thy	Fri Mar 21 13:49:20 2014 +0000
@@ -1,5 +1,5 @@
 header {* 
-  Separation logic for TM
+  Separation logic for Turing Machines
 *}
 
 theory Hoare_tm
@@ -23,8 +23,9 @@
 
 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"
+method_setup prune = 
+  {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} 
+  "pruning parameters"
 
 ML {*
 structure StepRules = Named_Thms
@@ -110,7 +111,7 @@
 
 interpretation tm: sep_exec tstep trset_of .
 
-section {* Assembly language and its program logic *}
+section {* Assembly language for TMs and its program logic *}
 
 subsection {* The assembly language *}
 
@@ -118,7 +119,7 @@
    TInstr tm_inst
  | TLabel nat
  | TSeq tpg tpg
- | TLocal "(nat \<Rightarrow> tpg)"
+ | TLocal "nat \<Rightarrow> tpg"
 
 notation TLocal (binder "TL " 10)
 
@@ -132,14 +133,12 @@
 
 type_synonym tassert = "tresource set \<Rightarrow> bool"
 
-abbreviation t_hoare :: 
-  "tassert \<Rightarrow> tassert  \<Rightarrow> tassert \<Rightarrow> bool" ("(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50)
-  where "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace> == sep_exec.Hoare_gen tstep trset_of p c q"
+abbreviation t_hoare :: "tassert \<Rightarrow> tassert  \<Rightarrow> tassert \<Rightarrow> bool" ("(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)
+  where "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace> == sep_exec.Hoare_gen tstep trset_of p c q"
 
 abbreviation it_hoare ::
-  "(('a::sep_algebra) \<Rightarrow> tresource set \<Rightarrow> bool) \<Rightarrow> 
-      ('a \<Rightarrow> bool) \<Rightarrow> (tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-  ("(1_).(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50)
+  "('a::sep_algebra \<Rightarrow> tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> (tresource set \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+      ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)
 where "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> == sep_exec.IHoare tstep trset_of I P c Q"
 
 (*
@@ -147,7 +146,8 @@
   "tpg_len (TInstr ai) = 1" |
   "tpg_len (TSeq p1 p2) = tpg_len p1 + tpg_len " |
   "tpg_len (TLocal fp) = tpg_len (fp 0)" |
-  "tpg_len (TLabel l) = 0" *)
+  "tpg_len (TLabel l) = 0" 
+*)
 
 primrec tassemble_to :: "tpg \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> tassert" 
   where 
@@ -165,7 +165,7 @@
 
 lemma EXS_intro: 
   assumes h: "(P x) s"
-  shows "((EXS x. P(x))) s"
+  shows "(EXS x. P(x)) s"
   by (smt h pred_ex_def sep_conj_impl)
 
 lemma EXS_elim: