theorem collections do not contain default rules any longer
authorhaftmann
Tue Jul 13 11:38:03 2010 +0200 (2010-07-13)
changeset 3778730dc3abf4a58
parent 37786 4eb98849c5c0
child 37788 261c61fabc98
theorem collections do not contain default rules any longer
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Mrec.thy
src/HOL/Imperative_HOL/Ref.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 02:29:05 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 11:38:03 2010 +0200
     1.3 @@ -166,80 +166,80 @@
     1.4  
     1.5  text {* Monad operations *}
     1.6  
     1.7 -lemma execute_new [simp, execute_simps]:
     1.8 +lemma execute_new [execute_simps]:
     1.9    "execute (new n x) h = Some (array (replicate n x) h)"
    1.10 -  by (simp add: new_def)
    1.11 +  by (simp add: new_def execute_simps)
    1.12  
    1.13 -lemma success_newI [iff, success_intros]:
    1.14 +lemma success_newI [success_intros]:
    1.15    "success (new n x) h"
    1.16 -  by (simp add: new_def)
    1.17 +  by (auto intro: success_intros simp add: new_def)
    1.18  
    1.19  lemma crel_newI [crel_intros]:
    1.20    assumes "(a, h') = array (replicate n x) h"
    1.21    shows "crel (new n x) h h' a"
    1.22 -  by (rule crelI) (simp add: assms)
    1.23 +  by (rule crelI) (simp add: assms execute_simps)
    1.24  
    1.25  lemma crel_newE [crel_elims]:
    1.26    assumes "crel (new n x) h h' r"
    1.27    obtains "r = fst (array (replicate n x) h)" "h' = snd (array (replicate n x) h)" 
    1.28      "get_array r h' = replicate n x" "array_present r h'" "\<not> array_present r h"
    1.29 -  using assms by (rule crelE) (simp add: get_array_init_array_list)
    1.30 +  using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
    1.31  
    1.32 -lemma execute_of_list [simp, execute_simps]:
    1.33 +lemma execute_of_list [execute_simps]:
    1.34    "execute (of_list xs) h = Some (array xs h)"
    1.35 -  by (simp add: of_list_def)
    1.36 +  by (simp add: of_list_def execute_simps)
    1.37  
    1.38 -lemma success_of_listI [iff, success_intros]:
    1.39 +lemma success_of_listI [success_intros]:
    1.40    "success (of_list xs) h"
    1.41 -  by (simp add: of_list_def)
    1.42 +  by (auto intro: success_intros simp add: of_list_def)
    1.43  
    1.44  lemma crel_of_listI [crel_intros]:
    1.45    assumes "(a, h') = array xs h"
    1.46    shows "crel (of_list xs) h h' a"
    1.47 -  by (rule crelI) (simp add: assms)
    1.48 +  by (rule crelI) (simp add: assms execute_simps)
    1.49  
    1.50  lemma crel_of_listE [crel_elims]:
    1.51    assumes "crel (of_list xs) h h' r"
    1.52    obtains "r = fst (array xs h)" "h' = snd (array xs h)" 
    1.53      "get_array r h' = xs" "array_present r h'" "\<not> array_present r h"
    1.54 -  using assms by (rule crelE) (simp add: get_array_init_array_list)
    1.55 +  using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
    1.56  
    1.57 -lemma execute_make [simp, execute_simps]:
    1.58 +lemma execute_make [execute_simps]:
    1.59    "execute (make n f) h = Some (array (map f [0 ..< n]) h)"
    1.60 -  by (simp add: make_def)
    1.61 +  by (simp add: make_def execute_simps)
    1.62  
    1.63 -lemma success_makeI [iff, success_intros]:
    1.64 +lemma success_makeI [success_intros]:
    1.65    "success (make n f) h"
    1.66 -  by (simp add: make_def)
    1.67 +  by (auto intro: success_intros simp add: make_def)
    1.68  
    1.69  lemma crel_makeI [crel_intros]:
    1.70    assumes "(a, h') = array (map f [0 ..< n]) h"
    1.71    shows "crel (make n f) h h' a"
    1.72 -  by (rule crelI) (simp add: assms)
    1.73 +  by (rule crelI) (simp add: assms execute_simps)
    1.74  
    1.75  lemma crel_makeE [crel_elims]:
    1.76    assumes "crel (make n f) h h' r"
    1.77    obtains "r = fst (array (map f [0 ..< n]) h)" "h' = snd (array (map f [0 ..< n]) h)" 
    1.78      "get_array r h' = map f [0 ..< n]" "array_present r h'" "\<not> array_present r h"
    1.79 -  using assms by (rule crelE) (simp add: get_array_init_array_list)
    1.80 +  using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps)
    1.81  
    1.82 -lemma execute_len [simp, execute_simps]:
    1.83 +lemma execute_len [execute_simps]:
    1.84    "execute (len a) h = Some (length a h, h)"
    1.85 -  by (simp add: len_def)
    1.86 +  by (simp add: len_def execute_simps)
    1.87  
    1.88 -lemma success_lenI [iff, success_intros]:
    1.89 +lemma success_lenI [success_intros]:
    1.90    "success (len a) h"
    1.91 -  by (simp add: len_def)
    1.92 +  by (auto intro: success_intros simp add: len_def)
    1.93  
    1.94  lemma crel_lengthI [crel_intros]:
    1.95    assumes "h' = h" "r = length a h"
    1.96    shows "crel (len a) h h' r"
    1.97 -  by (rule crelI) (simp add: assms)
    1.98 +  by (rule crelI) (simp add: assms execute_simps)
    1.99  
   1.100  lemma crel_lengthE [crel_elims]:
   1.101    assumes "crel (len a) h h' r"
   1.102    obtains "r = length a h'" "h' = h" 
   1.103 -  using assms by (rule crelE) simp
   1.104 +  using assms by (rule crelE) (simp add: execute_simps)
   1.105  
   1.106  lemma execute_nth [execute_simps]:
   1.107    "i < length a h \<Longrightarrow>
   1.108 @@ -327,13 +327,13 @@
   1.109    using assms by (rule crelE)
   1.110      (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.111  
   1.112 -lemma execute_freeze [simp, execute_simps]:
   1.113 +lemma execute_freeze [execute_simps]:
   1.114    "execute (freeze a) h = Some (get_array a h, h)"
   1.115 -  by (simp add: freeze_def)
   1.116 +  by (simp add: freeze_def execute_simps)
   1.117  
   1.118 -lemma success_freezeI [iff, success_intros]:
   1.119 +lemma success_freezeI [success_intros]:
   1.120    "success (freeze a) h"
   1.121 -  by (simp add: freeze_def)
   1.122 +  by (auto intro: success_intros simp add: freeze_def)
   1.123  
   1.124  lemma crel_freezeI [crel_intros]:
   1.125    assumes "h' = h" "r = get_array a h"
   1.126 @@ -343,19 +343,19 @@
   1.127  lemma crel_freezeE [crel_elims]:
   1.128    assumes "crel (freeze a) h h' r"
   1.129    obtains "h' = h" "r = get_array a h"
   1.130 -  using assms by (rule crelE) simp
   1.131 +  using assms by (rule crelE) (simp add: execute_simps)
   1.132  
   1.133  lemma upd_return:
   1.134    "upd i x a \<guillemotright> return a = upd i x a"
   1.135 -  by (rule Heap_eqI) (simp add: bind_def guard_def upd_def)
   1.136 +  by (rule Heap_eqI) (simp add: bind_def guard_def upd_def execute_simps)
   1.137  
   1.138  lemma array_make:
   1.139    "new n x = make n (\<lambda>_. x)"
   1.140 -  by (rule Heap_eqI) (simp add: map_replicate_trivial)
   1.141 +  by (rule Heap_eqI) (simp add: map_replicate_trivial execute_simps)
   1.142  
   1.143  lemma array_of_list_make:
   1.144    "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
   1.145 -  by (rule Heap_eqI) (simp add: map_nth)
   1.146 +  by (rule Heap_eqI) (simp add: map_nth execute_simps)
   1.147  
   1.148  hide_const (open) new
   1.149  
   1.150 @@ -444,11 +444,11 @@
   1.151        n \<leftarrow> len a;
   1.152        Heap_Monad.fold_map (Array.nth a) [0..<n]
   1.153      done) h = Some (get_array a h, h)"
   1.154 -    by (auto intro: execute_bind_eq_SomeI)
   1.155 +    by (auto intro: execute_bind_eq_SomeI simp add: execute_simps)
   1.156    then show "execute (freeze a) h = execute (do
   1.157        n \<leftarrow> len a;
   1.158        Heap_Monad.fold_map (Array.nth a) [0..<n]
   1.159 -    done) h" by simp
   1.160 +    done) h" by (simp add: execute_simps)
   1.161  qed
   1.162  
   1.163  hide_const (open) new' of_list' make' len' nth' upd'
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 13 02:29:05 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 13 11:38:03 2010 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/Library/Heap_Monad.thy
     2.5 +(*  Title:      HOL/Imperative_HOL/Heap_Monad.thy
     2.6      Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
     2.7  *)
     2.8  
     2.9 @@ -40,7 +40,7 @@
    2.10  
    2.11  setup Execute_Simps.setup
    2.12  
    2.13 -lemma execute_Let [simp, execute_simps]:
    2.14 +lemma execute_Let [execute_simps]:
    2.15    "execute (let x = t in f x) = (let x = t in execute (f x))"
    2.16    by (simp add: Let_def)
    2.17  
    2.18 @@ -50,14 +50,14 @@
    2.19  definition tap :: "(heap \<Rightarrow> 'a) \<Rightarrow> 'a Heap" where
    2.20    [code del]: "tap f = Heap (\<lambda>h. Some (f h, h))"
    2.21  
    2.22 -lemma execute_tap [simp, execute_simps]:
    2.23 +lemma execute_tap [execute_simps]:
    2.24    "execute (tap f) h = Some (f h, h)"
    2.25    by (simp add: tap_def)
    2.26  
    2.27  definition heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
    2.28    [code del]: "heap f = Heap (Some \<circ> f)"
    2.29  
    2.30 -lemma execute_heap [simp, execute_simps]:
    2.31 +lemma execute_heap [execute_simps]:
    2.32    "execute (heap f) = Some \<circ> f"
    2.33    by (simp add: heap_def)
    2.34  
    2.35 @@ -93,13 +93,13 @@
    2.36  
    2.37  setup Success_Intros.setup
    2.38  
    2.39 -lemma success_tapI [iff, success_intros]:
    2.40 +lemma success_tapI [success_intros]:
    2.41    "success (tap f) h"
    2.42 -  by (rule successI) simp
    2.43 +  by (rule successI) (simp add: execute_simps)
    2.44  
    2.45 -lemma success_heapI [iff, success_intros]:
    2.46 +lemma success_heapI [success_intros]:
    2.47    "success (heap f) h"
    2.48 -  by (rule successI) simp
    2.49 +  by (rule successI) (simp add: execute_simps)
    2.50  
    2.51  lemma success_guardI [success_intros]:
    2.52    "P h \<Longrightarrow> success (guard P f) h"
    2.53 @@ -196,22 +196,22 @@
    2.54  lemma crel_tapI [crel_intros]:
    2.55    assumes "h' = h" "r = f h"
    2.56    shows "crel (tap f) h h' r"
    2.57 -  by (rule crelI) (simp add: assms)
    2.58 +  by (rule crelI) (simp add: assms execute_simps)
    2.59  
    2.60  lemma crel_tapE [crel_elims]:
    2.61    assumes "crel (tap f) h h' r"
    2.62    obtains "h' = h" and "r = f h"
    2.63 -  using assms by (rule crelE) auto
    2.64 +  using assms by (rule crelE) (auto simp add: execute_simps)
    2.65  
    2.66  lemma crel_heapI [crel_intros]:
    2.67    assumes "h' = snd (f h)" "r = fst (f h)"
    2.68    shows "crel (heap f) h h' r"
    2.69 -  by (rule crelI) (simp add: assms)
    2.70 +  by (rule crelI) (simp add: assms execute_simps)
    2.71  
    2.72  lemma crel_heapE [crel_elims]:
    2.73    assumes "crel (heap f) h h' r"
    2.74    obtains "h' = snd (f h)" and "r = fst (f h)"
    2.75 -  using assms by (rule crelE) simp
    2.76 +  using assms by (rule crelE) (simp add: execute_simps)
    2.77  
    2.78  lemma crel_guardI [crel_intros]:
    2.79    assumes "P h" "h' = snd (f h)" "r = fst (f h)"
    2.80 @@ -230,34 +230,34 @@
    2.81  definition return :: "'a \<Rightarrow> 'a Heap" where
    2.82    [code del]: "return x = heap (Pair x)"
    2.83  
    2.84 -lemma execute_return [simp, execute_simps]:
    2.85 +lemma execute_return [execute_simps]:
    2.86    "execute (return x) = Some \<circ> Pair x"
    2.87 -  by (simp add: return_def)
    2.88 +  by (simp add: return_def execute_simps)
    2.89  
    2.90 -lemma success_returnI [iff, success_intros]:
    2.91 +lemma success_returnI [success_intros]:
    2.92    "success (return x) h"
    2.93 -  by (rule successI) simp
    2.94 +  by (rule successI) (simp add: execute_simps)
    2.95  
    2.96  lemma crel_returnI [crel_intros]:
    2.97    "h = h' \<Longrightarrow> crel (return x) h h' x"
    2.98 -  by (rule crelI) simp
    2.99 +  by (rule crelI) (simp add: execute_simps)
   2.100  
   2.101  lemma crel_returnE [crel_elims]:
   2.102    assumes "crel (return x) h h' r"
   2.103    obtains "r = x" "h' = h"
   2.104 -  using assms by (rule crelE) simp
   2.105 +  using assms by (rule crelE) (simp add: execute_simps)
   2.106  
   2.107  definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
   2.108    [code del]: "raise s = Heap (\<lambda>_. None)"
   2.109  
   2.110 -lemma execute_raise [simp, execute_simps]:
   2.111 +lemma execute_raise [execute_simps]:
   2.112    "execute (raise s) = (\<lambda>_. None)"
   2.113    by (simp add: raise_def)
   2.114  
   2.115  lemma crel_raiseE [crel_elims]:
   2.116    assumes "crel (raise x) h h' r"
   2.117    obtains "False"
   2.118 -  using assms by (rule crelE) (simp add: success_def)
   2.119 +  using assms by (rule crelE) (simp add: success_def execute_simps)
   2.120  
   2.121  definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
   2.122    [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
   2.123 @@ -303,16 +303,16 @@
   2.124    using assms by (simp add: bind_def)
   2.125  
   2.126  lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
   2.127 -  by (rule Heap_eqI) (simp add: execute_bind)
   2.128 +  by (rule Heap_eqI) (simp add: execute_bind execute_simps)
   2.129  
   2.130  lemma bind_return [simp]: "f \<guillemotright>= return = f"
   2.131 -  by (rule Heap_eqI) (simp add: bind_def split: option.splits)
   2.132 +  by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
   2.133  
   2.134  lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
   2.135 -  by (rule Heap_eqI) (simp add: bind_def split: option.splits)
   2.136 +  by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
   2.137  
   2.138  lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
   2.139 -  by (rule Heap_eqI) (simp add: execute_bind)
   2.140 +  by (rule Heap_eqI) (simp add: execute_simps)
   2.141  
   2.142  abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap"  (infixl ">>" 54) where
   2.143    "f >> g \<equiv> f >>= (\<lambda>_. g)"
   2.144 @@ -411,7 +411,7 @@
   2.145  lemma execute_assert [execute_simps]:
   2.146    "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
   2.147    "\<not> P x \<Longrightarrow> execute (assert P x) h = None"
   2.148 -  by (simp_all add: assert_def)
   2.149 +  by (simp_all add: assert_def execute_simps)
   2.150  
   2.151  lemma success_assertI [success_intros]:
   2.152    "P x \<Longrightarrow> success (assert P x) h"
   2.153 @@ -466,14 +466,14 @@
   2.154    shows "execute (fold_map f xs) h =
   2.155      Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
   2.156  using assms proof (induct xs)
   2.157 -  case Nil show ?case by simp
   2.158 +  case Nil show ?case by (simp add: execute_simps)
   2.159  next
   2.160    case (Cons x xs)
   2.161    from Cons.prems obtain y
   2.162      where y: "execute (f x) h = Some (y, h)" by auto
   2.163    moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h =
   2.164      Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto
   2.165 -  ultimately show ?case by (simp, simp only: execute_bind(1), simp)
   2.166 +  ultimately show ?case by (simp, simp only: execute_bind(1), simp add: execute_simps)
   2.167  qed
   2.168  
   2.169  subsection {* Code generator setup *}
     3.1 --- a/src/HOL/Imperative_HOL/Mrec.thy	Tue Jul 13 02:29:05 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Mrec.thy	Tue Jul 13 11:38:03 2010 +0200
     3.3 @@ -76,7 +76,7 @@
     3.4    apply simp
     3.5    apply (rule ext)
     3.6    apply (unfold mrec_rule[of x])
     3.7 -  by (auto split: option.splits prod.splits sum.splits)
     3.8 +  by (auto simp add: execute_simps split: option.splits prod.splits sum.splits)
     3.9  
    3.10  lemma MREC_pinduct:
    3.11    assumes "execute (MREC x) h = Some (r, h')"
     4.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 02:29:05 2010 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 11:38:03 2010 +0200
     4.3 @@ -1,4 +1,4 @@
     4.4 -(*  Title:      HOL/Library/Ref.thy
     4.5 +(*  Title:      HOL/Imperative_HOL/Ref.thy
     4.6      Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
     4.7  *)
     4.8  
     4.9 @@ -135,77 +135,77 @@
    4.10  
    4.11  text {* Monad operations *}
    4.12  
    4.13 -lemma execute_ref [simp, execute_simps]:
    4.14 +lemma execute_ref [execute_simps]:
    4.15    "execute (ref v) h = Some (alloc v h)"
    4.16 -  by (simp add: ref_def)
    4.17 +  by (simp add: ref_def execute_simps)
    4.18  
    4.19 -lemma success_refI [iff, success_intros]:
    4.20 +lemma success_refI [success_intros]:
    4.21    "success (ref v) h"
    4.22 -  by (auto simp add: ref_def)
    4.23 +  by (auto intro: success_intros simp add: ref_def)
    4.24  
    4.25  lemma crel_refI [crel_intros]:
    4.26    assumes "(r, h') = alloc v h"
    4.27    shows "crel (ref v) h h' r"
    4.28 -  by (rule crelI) (insert assms, simp)
    4.29 +  by (rule crelI) (insert assms, simp add: execute_simps)
    4.30  
    4.31  lemma crel_refE [crel_elims]:
    4.32    assumes "crel (ref v) h h' r"
    4.33    obtains "Ref.get h' r = v" and "Ref.present h' r" and "\<not> Ref.present h r"
    4.34 -  using assms by (rule crelE) simp
    4.35 +  using assms by (rule crelE) (simp add: execute_simps)
    4.36  
    4.37 -lemma execute_lookup [simp, execute_simps]:
    4.38 +lemma execute_lookup [execute_simps]:
    4.39    "Heap_Monad.execute (lookup r) h = Some (get h r, h)"
    4.40 -  by (simp add: lookup_def)
    4.41 +  by (simp add: lookup_def execute_simps)
    4.42  
    4.43 -lemma success_lookupI [iff, success_intros]:
    4.44 +lemma success_lookupI [success_intros]:
    4.45    "success (lookup r) h"
    4.46 -  by (auto simp add: lookup_def)
    4.47 +  by (auto intro: success_intros  simp add: lookup_def)
    4.48  
    4.49  lemma crel_lookupI [crel_intros]:
    4.50    assumes "h' = h" "x = Ref.get h r"
    4.51    shows "crel (!r) h h' x"
    4.52 -  by (rule crelI) (insert assms, simp)
    4.53 +  by (rule crelI) (insert assms, simp add: execute_simps)
    4.54  
    4.55  lemma crel_lookupE [crel_elims]:
    4.56    assumes "crel (!r) h h' x"
    4.57    obtains "h' = h" "x = Ref.get h r"
    4.58 -  using assms by (rule crelE) simp
    4.59 +  using assms by (rule crelE) (simp add: execute_simps)
    4.60  
    4.61 -lemma execute_update [simp, execute_simps]:
    4.62 +lemma execute_update [execute_simps]:
    4.63    "Heap_Monad.execute (update r v) h = Some ((), set r v h)"
    4.64 -  by (simp add: update_def)
    4.65 +  by (simp add: update_def execute_simps)
    4.66  
    4.67 -lemma success_updateI [iff, success_intros]:
    4.68 +lemma success_updateI [success_intros]:
    4.69    "success (update r v) h"
    4.70 -  by (auto simp add: update_def)
    4.71 +  by (auto intro: success_intros  simp add: update_def)
    4.72  
    4.73  lemma crel_updateI [crel_intros]:
    4.74    assumes "h' = Ref.set r v h"
    4.75    shows "crel (r := v) h h' x"
    4.76 -  by (rule crelI) (insert assms, simp)
    4.77 +  by (rule crelI) (insert assms, simp add: execute_simps)
    4.78  
    4.79  lemma crel_updateE [crel_elims]:
    4.80    assumes "crel (r' := v) h h' r"
    4.81    obtains "h' = Ref.set r' v h"
    4.82 -  using assms by (rule crelE) simp
    4.83 +  using assms by (rule crelE) (simp add: execute_simps)
    4.84  
    4.85 -lemma execute_change [simp, execute_simps]:
    4.86 +lemma execute_change [execute_simps]:
    4.87    "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)"
    4.88 -  by (simp add: change_def bind_def Let_def)
    4.89 +  by (simp add: change_def bind_def Let_def execute_simps)
    4.90  
    4.91 -lemma success_changeI [iff, success_intros]:
    4.92 +lemma success_changeI [success_intros]:
    4.93    "success (change f r) h"
    4.94    by (auto intro!: success_intros crel_intros simp add: change_def)
    4.95  
    4.96  lemma crel_changeI [crel_intros]: 
    4.97    assumes "h' = Ref.set r (f (Ref.get h r)) h" "x = f (Ref.get h r)"
    4.98    shows "crel (Ref.change f r) h h' x"
    4.99 -  by (rule crelI) (insert assms, simp)  
   4.100 +  by (rule crelI) (insert assms, simp add: execute_simps)  
   4.101  
   4.102  lemma crel_changeE [crel_elims]:
   4.103    assumes "crel (Ref.change f r') h h' r"
   4.104    obtains "h' = Ref.set r' (f (Ref.get h r')) h" "r = f (Ref.get h r')"
   4.105 -  using assms by (rule crelE) simp
   4.106 +  using assms by (rule crelE) (simp add: execute_simps)
   4.107  
   4.108  lemma lookup_chain:
   4.109    "(!r \<guillemotright> f) = f"