src/HOL/Imperative_HOL/Ref.thy

--- a/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 02:29:05 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 11:38:03 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Ref.thy
+(*  Title:      HOL/Imperative_HOL/Ref.thy
     Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
 *)
 
@@ -135,77 +135,77 @@
 
 text {* Monad operations *}
 
-lemma execute_ref [simp, execute_simps]:
+lemma execute_ref [execute_simps]:
   "execute (ref v) h = Some (alloc v h)"
-  by (simp add: ref_def)
+  by (simp add: ref_def execute_simps)
 
-lemma success_refI [iff, success_intros]:
+lemma success_refI [success_intros]:
   "success (ref v) h"
-  by (auto simp add: ref_def)
+  by (auto intro: success_intros simp add: ref_def)
 
 lemma crel_refI [crel_intros]:
   assumes "(r, h') = alloc v h"
   shows "crel (ref v) h h' r"
-  by (rule crelI) (insert assms, simp)
+  by (rule crelI) (insert assms, simp add: execute_simps)
 
 lemma crel_refE [crel_elims]:
   assumes "crel (ref v) h h' r"
   obtains "Ref.get h' r = v" and "Ref.present h' r" and "\<not> Ref.present h r"
-  using assms by (rule crelE) simp
+  using assms by (rule crelE) (simp add: execute_simps)
 
-lemma execute_lookup [simp, execute_simps]:
+lemma execute_lookup [execute_simps]:
   "Heap_Monad.execute (lookup r) h = Some (get h r, h)"
-  by (simp add: lookup_def)
+  by (simp add: lookup_def execute_simps)
 
-lemma success_lookupI [iff, success_intros]:
+lemma success_lookupI [success_intros]:
   "success (lookup r) h"
-  by (auto simp add: lookup_def)
+  by (auto intro: success_intros  simp add: lookup_def)
 
 lemma crel_lookupI [crel_intros]:
   assumes "h' = h" "x = Ref.get h r"
   shows "crel (!r) h h' x"
-  by (rule crelI) (insert assms, simp)
+  by (rule crelI) (insert assms, simp add: execute_simps)
 
 lemma crel_lookupE [crel_elims]:
   assumes "crel (!r) h h' x"
   obtains "h' = h" "x = Ref.get h r"
-  using assms by (rule crelE) simp
+  using assms by (rule crelE) (simp add: execute_simps)
 
-lemma execute_update [simp, execute_simps]:
+lemma execute_update [execute_simps]:
   "Heap_Monad.execute (update r v) h = Some ((), set r v h)"
-  by (simp add: update_def)
+  by (simp add: update_def execute_simps)
 
-lemma success_updateI [iff, success_intros]:
+lemma success_updateI [success_intros]:
   "success (update r v) h"
-  by (auto simp add: update_def)
+  by (auto intro: success_intros  simp add: update_def)
 
 lemma crel_updateI [crel_intros]:
   assumes "h' = Ref.set r v h"
   shows "crel (r := v) h h' x"
-  by (rule crelI) (insert assms, simp)
+  by (rule crelI) (insert assms, simp add: execute_simps)
 
 lemma crel_updateE [crel_elims]:
   assumes "crel (r' := v) h h' r"
   obtains "h' = Ref.set r' v h"
-  using assms by (rule crelE) simp
+  using assms by (rule crelE) (simp add: execute_simps)
 
-lemma execute_change [simp, execute_simps]:
+lemma execute_change [execute_simps]:
   "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)"
-  by (simp add: change_def bind_def Let_def)
+  by (simp add: change_def bind_def Let_def execute_simps)
 
-lemma success_changeI [iff, success_intros]:
+lemma success_changeI [success_intros]:
   "success (change f r) h"
   by (auto intro!: success_intros crel_intros simp add: change_def)
 
 lemma crel_changeI [crel_intros]: 
   assumes "h' = Ref.set r (f (Ref.get h r)) h" "x = f (Ref.get h r)"
   shows "crel (Ref.change f r) h h' x"
-  by (rule crelI) (insert assms, simp)  
+  by (rule crelI) (insert assms, simp add: execute_simps)  
 
 lemma crel_changeE [crel_elims]:
   assumes "crel (Ref.change f r') h h' r"
   obtains "h' = Ref.set r' (f (Ref.get h r')) h" "r = f (Ref.get h r')"
-  using assms by (rule crelE) simp
+  using assms by (rule crelE) (simp add: execute_simps)
 
 lemma lookup_chain:
   "(!r \<guillemotright> f) = f"