--- a/thys/Hoare_gen.thy	Tue Mar 25 11:20:36 2014 +0000
+++ b/thys/Hoare_gen.thy	Thu Mar 27 11:50:37 2014 +0000
@@ -129,7 +129,6 @@
     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>"
@@ -151,6 +150,52 @@
 using assms
 by (auto intro: sequencing code_extension code_extension1)
 
+lemma pre_condI: 
+  assumes h: "cond \<Longrightarrow> \<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>" 
+  shows "\<lbrace><cond> \<and>* p\<rbrace> c \<lbrace>q\<rbrace>"
+proof(induct rule:HoareI)
+  case (Pre r s)
+  hence "cond" "(p \<and>* c \<and>* r) (recse s)"
+    apply (metis pasrt_def sep_conjD)
+    by (smt Pre.hyps pasrt_def sep_add_zero sep_conj_commute sep_conj_def)
+  from h[OF this(1), unfolded Hoare_gen_def, rule_format, OF this(2)]
+  show ?case .
+qed
+
+lemma code_condI: 
+  assumes h: "b \<Longrightarrow> \<lbrace>p\<rbrace> 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)"
+    apply (metis condD sep_conjD sep_conj_assoc)
+    by (smt Pre.hyps condD sep_conj_impl)
+  from h[OF h1(1), unfolded Hoare_gen_def, rule_format, OF h1(2)]
+  and h1(1)
+  show ?case
+    by (metis (full_types) cond_true_eq1)
+qed
+
+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)
+  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)
+  from h[of x, unfolded Hoare_gen_def, rule_format, OF this]  
+  show ?case .
+qed
+
+lemma hoare_sep_false: 
+  "\<lbrace>sep_false\<rbrace> c \<lbrace>q\<rbrace>" 
+  by(unfold Hoare_gen_def, clarify, simp)
+
+
+lemma pred_exI: 
+  assumes "(P(x) \<and>* r) s"
+  shows "((EXS x. P(x)) \<and>* r) s"
+  by (metis assms pred_ex_def sep_globalise)
 
 definition
   IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" 
@@ -303,57 +348,18 @@
   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>"
-proof(induct rule:HoareI)
-  case (Pre r s)
-  hence "cond" "(p \<and>* c \<and>* r) (recse s)"
-    apply (metis pasrt_def sep_conjD)
-    by (smt Pre.hyps pasrt_def sep_add_zero sep_conj_commute sep_conj_def)
-  from h[OF this(1), unfolded Hoare_gen_def, rule_format, OF this(2)]
-  show ?case .
-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>"
   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> \<and>* c \<lbrace>q\<rbrace>"
-proof(induct rule: HoareI)
-  case (Pre r s)
-  hence h1: "b" "(p \<and>* c \<and>* r) (recse s)"
-    apply (metis condD sep_conjD sep_conj_assoc)
-    by (smt Pre.hyps condD sep_conj_impl)
-  from h[OF h1(1), unfolded Hoare_gen_def, rule_format, OF h1(2)]
-  and h1(1)
-  show ?case
-    by (metis (full_types) cond_true_eq1)
-qed
-
 lemma I_code_condI: 
   assumes h: "b \<Longrightarrow> I. \<lbrace>P\<rbrace> 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)
-  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)
-  from h[of x, unfolded Hoare_gen_def, rule_format, OF this]  
-  show ?case .
-qed
 
 lemma I_precond_exI: 
   assumes h:"\<And>x. I. \<lbrace>P x\<rbrace> c \<lbrace>Q\<rbrace>"
@@ -371,11 +377,6 @@
     by (auto simp:sep_conj_ac)
 qed
 
-(* FIXME: generic section *)
-lemma hoare_sep_false: 
-     "\<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>"
 by (smt IHoareI condD)