diff -r 995eb45bbadc -r 545fef826fa9 thys/Hoare_gen.thy
--- a/thys/Hoare_gen.thy	Thu Mar 13 20:06:29 2014 +0000
+++ b/thys/Hoare_gen.thy	Wed Mar 19 00:00:28 2014 +0000
@@ -7,17 +7,25 @@
   "../Separation_Algebra/Sep_Tactics"
 begin
 
-definition pasrt :: "bool \<Rightarrow> (('a::sep_algebra) \<Rightarrow> bool)" ("<_>" [72] 71)
+definition 
+  pasrt :: "bool \<Rightarrow> 'a::sep_algebra \<Rightarrow> bool" ("<_>" [72] 71)
 where "pasrt b = (\<lambda> s . s = 0 \<and> b)"
 
-lemma sep_conj_cond1: "(p \<and>* <cond> \<and>* q) = (<cond> \<and>* p \<and>* q)"
-  by(simp add: sep_conj_ac)
+
+(* smae 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)
 
-lemma sep_conj_cond2: "(p \<and>* <cond>) = (<cond> \<and>* p)"
-  by(simp add: sep_conj_ac)
+(* same as sep.mult.commute *)
+lemma sep_conj_cond2: 
+  "(p \<and>* <cond>) = (<cond> \<and>* p)"
+  by(rule sep.mult.commute)
 
-lemma sep_conj_cond3: "((<cond> \<and>* p) \<and>* r) = (<cond> \<and>* p \<and>* r)"
-  by (metis sep.mult_assoc)
+(* same as sep.mult_assoc *)
+lemma sep_conj_cond3: 
+  "((<cond> \<and>* p) \<and>* r) = (<cond> \<and>* p \<and>* r)"
+  by (rule sep.mult_assoc)
 
 lemmas sep_conj_cond = sep_conj_cond1 sep_conj_cond2 sep_conj_cond3
 
@@ -33,7 +41,7 @@
 lemma cond_true_eq2: "(p \<and>* <True>) = p"
   by simp
 
-lemma condD: "(<b> ** r) s \<Longrightarrow> b \<and> r s" 
+lemma condD: "(<b> \<and>* r) s \<Longrightarrow> b \<and> r s" 
 by (unfold sep_conj_def pasrt_def, auto)
 
 locale sep_exec = 
@@ -44,73 +52,60 @@
 definition "run n = step ^^ n"
 
 lemma run_add: "run (n1 + n2) s = run n1 (run n2 s)"
-  apply (unfold run_def)
-  by (metis funpow_add o_apply)
+  unfolding run_def
+  by (simp add: funpow_add)
 
+(* separation Hoare tripple *)
 definition
-  Hoare_gen :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" 
-                  ("(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50)
+  Hoare_gen :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"  ("(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)
 where
-  "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace> \<equiv> 
-      (\<forall> s r. (p**c**r) (recse s) \<longrightarrow> (\<exists> k. ((q ** c ** r) (recse (run (Suc k) s)))))"
+  "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace> \<equiv> 
+      (\<forall>s r. (p \<and>* c \<and>* r) (recse s) \<longrightarrow> (\<exists>k. ((q \<and>* c \<and>* r) (recse (run (Suc k) s)))))"
 
 lemma HoareI [case_names Pre]: 
-  assumes h: "\<And> r s. (p**c**r) (recse s) \<Longrightarrow> (\<exists> k. ((q ** c ** r) (recse (run (Suc k) s))))"
-  shows "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
+  assumes h: "\<And> r s. (p \<and>* c \<and>* r) (recse s) \<Longrightarrow> (\<exists>k. ((q \<and>* c \<and>* r) (recse (run (Suc k) s))))"
+  shows "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
   using h
-  by (unfold Hoare_gen_def, auto)
+  unfolding Hoare_gen_def
+  by simp
 
 lemma frame_rule: 
-  assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
-  shows "\<lbrace> p ** r \<rbrace> c \<lbrace> q ** r \<rbrace>"
-proof(induct rule: HoareI)
-  case (Pre r' s')
-  hence "(p \<and>* c \<and>* r \<and>* r') (recse s')" by (auto simp:sep_conj_ac)
-  from h[unfolded Hoare_gen_def, rule_format, OF this]
-  show ?case
-    by (metis sep_conj_assoc sep_conj_left_commute)
-qed
+  assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
+  shows "\<lbrace>p \<and>* r\<rbrace> c \<lbrace>q \<and>* r\<rbrace>"
+using assms
+unfolding Hoare_gen_def
+by (metis sep_conj_assoc sep_conj_left_commute)
 
 lemma sequencing: 
   assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
   and h2: "\<lbrace>q\<rbrace> c \<lbrace>r\<rbrace>"
   shows "\<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>"
-proof(induct rule:HoareI)
+proof(induct rule: HoareI)
   case (Pre r' s')
-  from h1[unfolded Hoare_gen_def, rule_format, OF Pre]
+  have "(p \<and>* c \<and>* r') (recse s')" by fact
+  with h1[unfolded Hoare_gen_def]
   obtain k1 where "(q \<and>* c \<and>* r') (recse (run (Suc k1) s'))" by auto
-  from h2[unfolded Hoare_gen_def, rule_format, OF this]
+  with h2[unfolded Hoare_gen_def]
   obtain k2 where "(r \<and>* c \<and>* r') (recse (run (Suc k2) (run (Suc k1) s')))" by auto
-  thus ?case
-    apply (rule_tac x = "Suc (k1 + k2)" in exI)
-    by (metis add_Suc_right nat_add_commute sep_exec.run_add)
+  thus "\<exists>k. (r \<and>* c \<and>* r') (recse (run (Suc k) s'))"
+    by (auto simp add: run_add[symmetric])
 qed
 
 lemma pre_stren: 
   assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
-  and h2:  "\<And>s. r s \<Longrightarrow> p s"
+  and h2: "\<And>s. r s \<Longrightarrow> p s"
   shows "\<lbrace>r\<rbrace> c \<lbrace>q\<rbrace>"
-proof(induct rule:HoareI)
-  case (Pre r' s')
-  with h2
-  have "(p \<and>* c \<and>* r') (recse s')"
-    by (metis sep_conj_impl1)
-  from h1[unfolded Hoare_gen_def, rule_format, OF this]
-  show ?case .
-qed
+using assms
+unfolding Hoare_gen_def
+by (metis sep_globalise)
 
 lemma post_weaken: 
   assumes h1: "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
     and h2: "\<And> s. q s \<Longrightarrow> r s"
   shows "\<lbrace>p\<rbrace> c \<lbrace>r\<rbrace>"
-proof(induct rule:HoareI)
-  case (Pre r' s')
-  from h1[unfolded Hoare_gen_def, rule_format, OF this]
-  obtain k where "(q \<and>* c \<and>* r') (recse (run (Suc k) s'))" by blast
-  with h2
-  show ?case
-    by (metis sep_conj_impl1)
-qed
+using assms
+unfolding Hoare_gen_def
+by (metis sep_globalise)
 
 lemma hoare_adjust:
   assumes h1: "\<lbrace>p1\<rbrace> c \<lbrace>q1\<rbrace>"
@@ -118,65 +113,55 @@
   and h3: "\<And>s. q1 s \<Longrightarrow> q s"
   shows "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
   using h1 h2 h3 post_weaken pre_stren
-  by (metis)
+  by (blast)
 
 lemma code_exI: 
   assumes h: "\<And> k. \<lbrace>p\<rbrace> c(k) \<lbrace>q\<rbrace>"
   shows "\<lbrace>p\<rbrace> EXS k. c(k) \<lbrace>q\<rbrace>"
-proof(unfold pred_ex_def, induct rule:HoareI)
+unfolding pred_ex_def
+proof(induct rule:HoareI)
   case (Pre r' s')
   then obtain k where "(p \<and>* (\<lambda> s. c k s) \<and>* r') (recse s')"
-    by (auto elim!:sep_conjE intro!:sep_conjI)
+    by (auto elim!: sep_conjE intro!: sep_conjI)
   from h[unfolded Hoare_gen_def, rule_format, OF this]
-  show ?case
-   by (auto elim!:sep_conjE intro!:sep_conjI)
+  show "\<exists>k. (q \<and>* (\<lambda>s. \<exists>x. c x s) \<and>* r') (recse (run (Suc k) s'))"
+    by (auto elim!: sep_conjE intro!: sep_conjI)
 qed
 
 lemma code_extension: 
-  assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
-  shows "\<lbrace> p \<rbrace> c ** e \<lbrace> q \<rbrace>"
-proof(induct rule:HoareI)
-  case (Pre r' s')
-  hence "(p \<and>* c \<and>* e \<and>* r') (recse s')" by (auto simp:sep_conj_ac)
-  from h[unfolded Hoare_gen_def, rule_format, OF this]
-  show ?case
-    by (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)
-qed
+  assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
+  shows "\<lbrace>p\<rbrace> c \<and>* e \<lbrace>q\<rbrace>"
+using assms
+unfolding Hoare_gen_def
+by (metis sep_conj_assoc)
 
 lemma code_extension1: 
-  assumes h: "\<lbrace> p \<rbrace> c \<lbrace> q \<rbrace>"
-  shows "\<lbrace> p \<rbrace> e ** c \<lbrace> q \<rbrace>"
-  by (metis code_extension h sep.mult_commute)
+  assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
+  shows "\<lbrace>p\<rbrace> e \<and>* c \<lbrace>q\<rbrace>"
+using assms
+unfolding Hoare_gen_def
+by (metis sep_conj_commute sep_conj_left_commute)
 
 lemma composition: 
   assumes h1: "\<lbrace>p\<rbrace> c1 \<lbrace>q\<rbrace>"
     and h2: "\<lbrace>q\<rbrace> c2 \<lbrace>r\<rbrace>"
-  shows "\<lbrace>p\<rbrace> c1 ** c2 \<lbrace>r\<rbrace>"
-proof(induct rule:HoareI)
-  case (Pre r' s')
-  hence "(p \<and>* c1 \<and>* c2 \<and>* r') (recse s')" by (auto simp:sep_conj_ac)
-  from h1[unfolded Hoare_gen_def, rule_format, OF this]
-  obtain k1 where "(q \<and>* c2 \<and>* c1 \<and>* r') (recse (run (Suc k1) s'))" 
-    by (auto simp:sep_conj_ac)
-  from h2[unfolded Hoare_gen_def, rule_format, OF this, folded run_add]
-  show ?case
-    by (auto elim!:sep_conjE intro!:sep_conjI simp:sep_conj_ac)
-qed
+  shows "\<lbrace>p\<rbrace> c1 \<and>* c2 \<lbrace>r\<rbrace>"
+using assms
+by (auto intro: sequencing code_extension code_extension1)
 
 
 definition
-  IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 
-                ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" 
-                  ("(1_).(\<lbrace>(1_)\<rbrace> / (_)/ \<lbrace>(1_)\<rbrace>)" 50)
+  IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" 
+             ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)
 where
   "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace> = (\<forall>s'. \<lbrace> EXS s. <P s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace> c 
-                         \<lbrace> EXS s. <Q s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace>)"
+                        \<lbrace> EXS s. <Q s> \<and>* <(s ## s')> \<and>* I(s + s')\<rbrace>)"
 
 lemma IHoareI [case_names IPre]: 
   assumes h: "\<And>s' s r cnf .  (<P s> \<and>* <(s ## s')> \<and>* I(s + s') \<and>* c \<and>* r) (recse cnf) \<Longrightarrow> 
                    (\<exists>k t. (<Q t> \<and>* <(t ## s')>  \<and>* I(t + s') \<and>* c \<and>* r) (recse (run (Suc k) cnf)))"
   shows "I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"
-  unfolding IHoare_def
+unfolding IHoare_def
 proof
   fix s'
   show " \<lbrace>EXS s. <P s> \<and>* <(s ## s')> \<and>* I (s + s')\<rbrace>  c