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

diff -r 192672a6fff4 -r dcbf7888a070 thys/Hoare_gen.thy
--- a/thys/Hoare_gen.thy	Fri Mar 21 15:10:13 2014 +0000
+++ b/thys/Hoare_gen.thy	Mon Mar 24 11:39:39 2014 +0000
@@ -7,6 +7,7 @@
   "../Separation_Algebra/Sep_Tactics"
 begin
 
+
 definition 
   pasrt :: "bool \<Rightarrow> 'a::sep_algebra \<Rightarrow> bool" ("<_>" [72] 71)
 where "pasrt b = (\<lambda> s . s = 0 \<and> b)"
@@ -60,10 +61,10 @@
   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 \<and>* c \<and>* r) (recse s) \<longrightarrow> (\<exists>k. ((q \<and>* c \<and>* r) (recse (run (Suc k) s)))))"
+      \<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 \<and>* c \<and>* r) (recse s) \<Longrightarrow> (\<exists>k. ((q \<and>* c \<and>* r) (recse (run (Suc k) s))))"
+  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
   unfolding Hoare_gen_def
@@ -123,11 +124,12 @@
   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)
-  from h[unfolded Hoare_gen_def, rule_format, OF this]
+  with h[unfolded Hoare_gen_def]
   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)
+    by (blast elim!: sep_conjE intro!: sep_conjI)
 qed
 
+(* FIXME: generic section ? *)
 lemma code_extension: 
   assumes "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
   shows "\<lbrace>p\<rbrace> c \<and>* e \<lbrace>q\<rbrace>"
@@ -154,12 +156,12 @@
   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>)"
+  "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>)"
 
 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)))"
+                   \<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
 proof
@@ -301,6 +303,7 @@
   using h1 h2
 by (smt IHoare_def sep_exec.composition)
 
+(* FIXME: generic section *)
 lemma pre_condI: 
   assumes h: "cond \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" 
   shows "\<lbrace><cond> \<and>* p\<rbrace> c \<lbrace>q\<rbrace>"
@@ -314,14 +317,15 @@
 qed
 
 lemma I_pre_condI: 
-  assumes h: "cond \<Longrightarrow> I.\<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" 
-  shows "I.\<lbrace><cond> \<and>* P\<rbrace> c \<lbrace>Q\<rbrace>"
+  assumes h: "cond \<Longrightarrow> I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>" 
+  shows "I. \<lbrace><cond> \<and>* P\<rbrace> c \<lbrace>Q\<rbrace>"
   using h
 by (smt IHoareI condD cond_true_eq2 sep.mult_commute)
 
+(* FIXME: generic section *)
 lemma code_condI: 
   assumes h: "b \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"
-  shows "\<lbrace>p\<rbrace> <b>**c \<lbrace>q\<rbrace>"
+  shows "\<lbrace>p\<rbrace> <b> \<and>* c \<lbrace>q\<rbrace>"
 proof(induct rule: HoareI)
   case (Pre r s)
   hence h1: "b" "(p \<and>* c \<and>* r) (recse s)"
@@ -335,14 +339,15 @@
 
 lemma I_code_condI: 
   assumes h: "b \<Longrightarrow> I. \<lbrace>P\<rbrace> c \<lbrace>Q\<rbrace>"
-  shows "I.\<lbrace>P\<rbrace> <b>**c \<lbrace>Q\<rbrace>"
+  shows "I. \<lbrace>P\<rbrace> <b> \<and>* c \<lbrace>Q\<rbrace>"
   using h
 by (smt IHoareI condD cond_true_eq2 sep.mult_commute sep_conj_cond1)
 
+(* FIXME: generic section *)
 lemma precond_exI: 
   assumes h:"\<And>x. \<lbrace>p x\<rbrace> c \<lbrace>q\<rbrace>"
   shows "\<lbrace>EXS x. p x\<rbrace> c \<lbrace>q\<rbrace>"
-proof(induct rule:HoareI)
+proof(induct rule: HoareI)
   case (Pre r s)
   then obtain x where "(p x \<and>* c \<and>* r) (recse s)"
     by (unfold pred_ex_def, auto elim!:sep_conjE intro!:sep_conjI)
@@ -352,7 +357,7 @@
 
 lemma I_precond_exI: 
   assumes h:"\<And>x. I. \<lbrace>P x\<rbrace> c \<lbrace>Q\<rbrace>"
-  shows "I.\<lbrace>EXS x. P x\<rbrace> c \<lbrace>Q\<rbrace>"
+  shows "I. \<lbrace>EXS x. P x\<rbrace> c \<lbrace>Q\<rbrace>"
 proof(induct rule:IHoareI)
   case (IPre s' s r cnf)
   then obtain x
@@ -366,14 +371,13 @@
     by (auto simp:sep_conj_ac)
 qed
 
+(* FIXME: generic section *)
 lemma hoare_sep_false: 
-     "\<lbrace>sep_false\<rbrace> c
-      \<lbrace>q\<rbrace>" 
+     "\<lbrace>sep_false\<rbrace> c \<lbrace>q\<rbrace>" 
   by(unfold Hoare_gen_def, clarify, simp)
 
 lemma I_hoare_sep_false:
-  "I. \<lbrace>sep_false\<rbrace> c
-      \<lbrace>Q\<rbrace>"
+  "I. \<lbrace>sep_false\<rbrace> c \<lbrace>Q\<rbrace>"
 by (smt IHoareI condD)
 
 end
@@ -391,18 +395,9 @@
 
 instance
   apply(default)
-  apply(simp add:set_ins_def)
-  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
-  apply (metis inf_commute)
-  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
-  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
-  apply (metis sup_commute)
-  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
-  apply (metis (lifting) Un_assoc)
-  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
-  apply (metis (lifting) Int_Un_distrib Un_empty inf_sup_distrib1 sup_eq_bot_iff)
-  apply(simp add:sep_disj_set_def plus_set_def set_zero_def)
-  by (metis (lifting) Int_Un_distrib Int_Un_distrib2 sup_eq_bot_iff)
+  apply(auto simp: set_ins_def)
+done
+
 end
 
 section {* A big operator of infinite separation conjunction *}