# HG changeset patch
# User haftmann
# Date 1279013883 -7200
# Node ID 30dc3abf4a58eef0828a2e680e16bf277c54325f
# Parent  4eb98849c5c059ee800596481cb73b181f3f8ce9
theorem collections do not contain default rules any longer

diff -r 4eb98849c5c0 -r 30dc3abf4a58 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 02:29:05 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 11:38:03 2010 +0200
@@ -166,80 +166,80 @@
 
 text {* Monad operations *}
 
-lemma execute_new [simp, execute_simps]:
+lemma execute_new [execute_simps]:
   "execute (new n x) h = Some (array (replicate n x) h)"
-  by (simp add: new_def)
+  by (simp add: new_def execute_simps)
 
-lemma success_newI [iff, success_intros]:
+lemma success_newI [success_intros]:
   "success (new n x) h"
-  by (simp add: new_def)
+  by (auto intro: success_intros simp add: new_def)
 
 lemma crel_newI [crel_intros]:
   assumes "(a, h') = array (replicate n x) h"
   shows "crel (new n x) h h' a"
-  by (rule crelI) (simp add: assms)
+  by (rule crelI) (simp add: assms execute_simps)
 
 lemma crel_newE [crel_elims]:
   assumes "crel (new n x) h h' r"
   obtains "r = fst (array (replicate n x) h)" "h' = snd (array (replicate n x) h)" 
     "get_array r h' = replicate n x" "array_present r h'" "\<not> array_present r h"
-  using assms by (rule crelE) (simp add: get_array_init_array_list)
+  using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
 
-lemma execute_of_list [simp, execute_simps]:
+lemma execute_of_list [execute_simps]:
   "execute (of_list xs) h = Some (array xs h)"
-  by (simp add: of_list_def)
+  by (simp add: of_list_def execute_simps)
 
-lemma success_of_listI [iff, success_intros]:
+lemma success_of_listI [success_intros]:
   "success (of_list xs) h"
-  by (simp add: of_list_def)
+  by (auto intro: success_intros simp add: of_list_def)
 
 lemma crel_of_listI [crel_intros]:
   assumes "(a, h') = array xs h"
   shows "crel (of_list xs) h h' a"
-  by (rule crelI) (simp add: assms)
+  by (rule crelI) (simp add: assms execute_simps)
 
 lemma crel_of_listE [crel_elims]:
   assumes "crel (of_list xs) h h' r"
   obtains "r = fst (array xs h)" "h' = snd (array xs h)" 
     "get_array r h' = xs" "array_present r h'" "\<not> array_present r h"
-  using assms by (rule crelE) (simp add: get_array_init_array_list)
+  using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
 
-lemma execute_make [simp, execute_simps]:
+lemma execute_make [execute_simps]:
   "execute (make n f) h = Some (array (map f [0 ..< n]) h)"
-  by (simp add: make_def)
+  by (simp add: make_def execute_simps)
 
-lemma success_makeI [iff, success_intros]:
+lemma success_makeI [success_intros]:
   "success (make n f) h"
-  by (simp add: make_def)
+  by (auto intro: success_intros simp add: make_def)
 
 lemma crel_makeI [crel_intros]:
   assumes "(a, h') = array (map f [0 ..< n]) h"
   shows "crel (make n f) h h' a"
-  by (rule crelI) (simp add: assms)
+  by (rule crelI) (simp add: assms execute_simps)
 
 lemma crel_makeE [crel_elims]:
   assumes "crel (make n f) h h' r"
   obtains "r = fst (array (map f [0 ..< n]) h)" "h' = snd (array (map f [0 ..< n]) h)" 
     "get_array r h' = map f [0 ..< n]" "array_present r h'" "\<not> array_present r h"
-  using assms by (rule crelE) (simp add: get_array_init_array_list)
+  using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
 
-lemma execute_len [simp, execute_simps]:
+lemma execute_len [execute_simps]:
   "execute (len a) h = Some (length a h, h)"
-  by (simp add: len_def)
+  by (simp add: len_def execute_simps)
 
-lemma success_lenI [iff, success_intros]:
+lemma success_lenI [success_intros]:
   "success (len a) h"
-  by (simp add: len_def)
+  by (auto intro: success_intros simp add: len_def)
 
 lemma crel_lengthI [crel_intros]:
   assumes "h' = h" "r = length a h"
   shows "crel (len a) h h' r"
-  by (rule crelI) (simp add: assms)
+  by (rule crelI) (simp add: assms execute_simps)
 
 lemma crel_lengthE [crel_elims]:
   assumes "crel (len a) h h' r"
   obtains "r = length a h'" "h' = h" 
-  using assms by (rule crelE) simp
+  using assms by (rule crelE) (simp add: execute_simps)
 
 lemma execute_nth [execute_simps]:
   "i < length a h \<Longrightarrow>
@@ -327,13 +327,13 @@
   using assms by (rule crelE)
     (erule successE, cases "i < length a h", simp_all add: execute_simps)
 
-lemma execute_freeze [simp, execute_simps]:
+lemma execute_freeze [execute_simps]:
   "execute (freeze a) h = Some (get_array a h, h)"
-  by (simp add: freeze_def)
+  by (simp add: freeze_def execute_simps)
 
-lemma success_freezeI [iff, success_intros]:
+lemma success_freezeI [success_intros]:
   "success (freeze a) h"
-  by (simp add: freeze_def)
+  by (auto intro: success_intros simp add: freeze_def)
 
 lemma crel_freezeI [crel_intros]:
   assumes "h' = h" "r = get_array a h"
@@ -343,19 +343,19 @@
 lemma crel_freezeE [crel_elims]:
   assumes "crel (freeze a) h h' r"
   obtains "h' = h" "r = get_array a h"
-  using assms by (rule crelE) simp
+  using assms by (rule crelE) (simp add: execute_simps)
 
 lemma upd_return:
   "upd i x a \<guillemotright> return a = upd i x a"
-  by (rule Heap_eqI) (simp add: bind_def guard_def upd_def)
+  by (rule Heap_eqI) (simp add: bind_def guard_def upd_def execute_simps)
 
 lemma array_make:
   "new n x = make n (\<lambda>_. x)"
-  by (rule Heap_eqI) (simp add: map_replicate_trivial)
+  by (rule Heap_eqI) (simp add: map_replicate_trivial execute_simps)
 
 lemma array_of_list_make:
   "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
-  by (rule Heap_eqI) (simp add: map_nth)
+  by (rule Heap_eqI) (simp add: map_nth execute_simps)
 
 hide_const (open) new
 
@@ -444,11 +444,11 @@
       n \<leftarrow> len a;
       Heap_Monad.fold_map (Array.nth a) [0..<n]
     done) h = Some (get_array a h, h)"
-    by (auto intro: execute_bind_eq_SomeI)
+    by (auto intro: execute_bind_eq_SomeI simp add: execute_simps)
   then show "execute (freeze a) h = execute (do
       n \<leftarrow> len a;
       Heap_Monad.fold_map (Array.nth a) [0..<n]
-    done) h" by simp
+    done) h" by (simp add: execute_simps)
 qed
 
 hide_const (open) new' of_list' make' len' nth' upd'
diff -r 4eb98849c5c0 -r 30dc3abf4a58 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 13 02:29:05 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 13 11:38:03 2010 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Heap_Monad.thy
+(*  Title:      HOL/Imperative_HOL/Heap_Monad.thy
     Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
 *)
 
@@ -40,7 +40,7 @@
 
 setup Execute_Simps.setup
 
-lemma execute_Let [simp, execute_simps]:
+lemma execute_Let [execute_simps]:
   "execute (let x = t in f x) = (let x = t in execute (f x))"
   by (simp add: Let_def)
 
@@ -50,14 +50,14 @@
 definition tap :: "(heap \<Rightarrow> 'a) \<Rightarrow> 'a Heap" where
   [code del]: "tap f = Heap (\<lambda>h. Some (f h, h))"
 
-lemma execute_tap [simp, execute_simps]:
+lemma execute_tap [execute_simps]:
   "execute (tap f) h = Some (f h, h)"
   by (simp add: tap_def)
 
 definition heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
   [code del]: "heap f = Heap (Some \<circ> f)"
 
-lemma execute_heap [simp, execute_simps]:
+lemma execute_heap [execute_simps]:
   "execute (heap f) = Some \<circ> f"
   by (simp add: heap_def)
 
@@ -93,13 +93,13 @@
 
 setup Success_Intros.setup
 
-lemma success_tapI [iff, success_intros]:
+lemma success_tapI [success_intros]:
   "success (tap f) h"
-  by (rule successI) simp
+  by (rule successI) (simp add: execute_simps)
 
-lemma success_heapI [iff, success_intros]:
+lemma success_heapI [success_intros]:
   "success (heap f) h"
-  by (rule successI) simp
+  by (rule successI) (simp add: execute_simps)
 
 lemma success_guardI [success_intros]:
   "P h \<Longrightarrow> success (guard P f) h"
@@ -196,22 +196,22 @@
 lemma crel_tapI [crel_intros]:
   assumes "h' = h" "r = f h"
   shows "crel (tap f) h h' r"
-  by (rule crelI) (simp add: assms)
+  by (rule crelI) (simp add: assms execute_simps)
 
 lemma crel_tapE [crel_elims]:
   assumes "crel (tap f) h h' r"
   obtains "h' = h" and "r = f h"
-  using assms by (rule crelE) auto
+  using assms by (rule crelE) (auto simp add: execute_simps)
 
 lemma crel_heapI [crel_intros]:
   assumes "h' = snd (f h)" "r = fst (f h)"
   shows "crel (heap f) h h' r"
-  by (rule crelI) (simp add: assms)
+  by (rule crelI) (simp add: assms execute_simps)
 
 lemma crel_heapE [crel_elims]:
   assumes "crel (heap f) h h' r"
   obtains "h' = snd (f h)" and "r = fst (f h)"
-  using assms by (rule crelE) simp
+  using assms by (rule crelE) (simp add: execute_simps)
 
 lemma crel_guardI [crel_intros]:
   assumes "P h" "h' = snd (f h)" "r = fst (f h)"
@@ -230,34 +230,34 @@
 definition return :: "'a \<Rightarrow> 'a Heap" where
   [code del]: "return x = heap (Pair x)"
 
-lemma execute_return [simp, execute_simps]:
+lemma execute_return [execute_simps]:
   "execute (return x) = Some \<circ> Pair x"
-  by (simp add: return_def)
+  by (simp add: return_def execute_simps)
 
-lemma success_returnI [iff, success_intros]:
+lemma success_returnI [success_intros]:
   "success (return x) h"
-  by (rule successI) simp
+  by (rule successI) (simp add: execute_simps)
 
 lemma crel_returnI [crel_intros]:
   "h = h' \<Longrightarrow> crel (return x) h h' x"
-  by (rule crelI) simp
+  by (rule crelI) (simp add: execute_simps)
 
 lemma crel_returnE [crel_elims]:
   assumes "crel (return x) h h' r"
   obtains "r = x" "h' = h"
-  using assms by (rule crelE) simp
+  using assms by (rule crelE) (simp add: execute_simps)
 
 definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
   [code del]: "raise s = Heap (\<lambda>_. None)"
 
-lemma execute_raise [simp, execute_simps]:
+lemma execute_raise [execute_simps]:
   "execute (raise s) = (\<lambda>_. None)"
   by (simp add: raise_def)
 
 lemma crel_raiseE [crel_elims]:
   assumes "crel (raise x) h h' r"
   obtains "False"
-  using assms by (rule crelE) (simp add: success_def)
+  using assms by (rule crelE) (simp add: success_def execute_simps)
 
 definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
   [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
@@ -303,16 +303,16 @@
   using assms by (simp add: bind_def)
 
 lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
-  by (rule Heap_eqI) (simp add: execute_bind)
+  by (rule Heap_eqI) (simp add: execute_bind execute_simps)
 
 lemma bind_return [simp]: "f \<guillemotright>= return = f"
-  by (rule Heap_eqI) (simp add: bind_def split: option.splits)
+  by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
 
 lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
-  by (rule Heap_eqI) (simp add: bind_def split: option.splits)
+  by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
 
 lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
-  by (rule Heap_eqI) (simp add: execute_bind)
+  by (rule Heap_eqI) (simp add: execute_simps)
 
 abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap"  (infixl ">>" 54) where
   "f >> g \<equiv> f >>= (\<lambda>_. g)"
@@ -411,7 +411,7 @@
 lemma execute_assert [execute_simps]:
   "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
   "\<not> P x \<Longrightarrow> execute (assert P x) h = None"
-  by (simp_all add: assert_def)
+  by (simp_all add: assert_def execute_simps)
 
 lemma success_assertI [success_intros]:
   "P x \<Longrightarrow> success (assert P x) h"
@@ -466,14 +466,14 @@
   shows "execute (fold_map f xs) h =
     Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
 using assms proof (induct xs)
-  case Nil show ?case by simp
+  case Nil show ?case by (simp add: execute_simps)
 next
   case (Cons x xs)
   from Cons.prems obtain y
     where y: "execute (f x) h = Some (y, h)" by auto
   moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h =
     Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto
-  ultimately show ?case by (simp, simp only: execute_bind(1), simp)
+  ultimately show ?case by (simp, simp only: execute_bind(1), simp add: execute_simps)
 qed
 
 subsection {* Code generator setup *}
diff -r 4eb98849c5c0 -r 30dc3abf4a58 src/HOL/Imperative_HOL/Mrec.thy
--- a/src/HOL/Imperative_HOL/Mrec.thy	Tue Jul 13 02:29:05 2010 +0200
+++ b/src/HOL/Imperative_HOL/Mrec.thy	Tue Jul 13 11:38:03 2010 +0200
@@ -76,7 +76,7 @@
   apply simp
   apply (rule ext)
   apply (unfold mrec_rule[of x])
-  by (auto split: option.splits prod.splits sum.splits)
+  by (auto simp add: execute_simps split: option.splits prod.splits sum.splits)
 
 lemma MREC_pinduct:
   assumes "execute (MREC x) h = Some (r, h')"
diff -r 4eb98849c5c0 -r 30dc3abf4a58 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"