src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 37787 30dc3abf4a58
parent 37772 026ed2fc15d4
child 37792 ba0bc31b90d7
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 13 02:29:05 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 13 11:38:03 2010 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Library/Heap_Monad.thy
     1.5 +(*  Title:      HOL/Imperative_HOL/Heap_Monad.thy
     1.6      Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
     1.7  *)
     1.8  
     1.9 @@ -40,7 +40,7 @@
    1.10  
    1.11  setup Execute_Simps.setup
    1.12  
    1.13 -lemma execute_Let [simp, execute_simps]:
    1.14 +lemma execute_Let [execute_simps]:
    1.15    "execute (let x = t in f x) = (let x = t in execute (f x))"
    1.16    by (simp add: Let_def)
    1.17  
    1.18 @@ -50,14 +50,14 @@
    1.19  definition tap :: "(heap \<Rightarrow> 'a) \<Rightarrow> 'a Heap" where
    1.20    [code del]: "tap f = Heap (\<lambda>h. Some (f h, h))"
    1.21  
    1.22 -lemma execute_tap [simp, execute_simps]:
    1.23 +lemma execute_tap [execute_simps]:
    1.24    "execute (tap f) h = Some (f h, h)"
    1.25    by (simp add: tap_def)
    1.26  
    1.27  definition heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
    1.28    [code del]: "heap f = Heap (Some \<circ> f)"
    1.29  
    1.30 -lemma execute_heap [simp, execute_simps]:
    1.31 +lemma execute_heap [execute_simps]:
    1.32    "execute (heap f) = Some \<circ> f"
    1.33    by (simp add: heap_def)
    1.34  
    1.35 @@ -93,13 +93,13 @@
    1.36  
    1.37  setup Success_Intros.setup
    1.38  
    1.39 -lemma success_tapI [iff, success_intros]:
    1.40 +lemma success_tapI [success_intros]:
    1.41    "success (tap f) h"
    1.42 -  by (rule successI) simp
    1.43 +  by (rule successI) (simp add: execute_simps)
    1.44  
    1.45 -lemma success_heapI [iff, success_intros]:
    1.46 +lemma success_heapI [success_intros]:
    1.47    "success (heap f) h"
    1.48 -  by (rule successI) simp
    1.49 +  by (rule successI) (simp add: execute_simps)
    1.50  
    1.51  lemma success_guardI [success_intros]:
    1.52    "P h \<Longrightarrow> success (guard P f) h"
    1.53 @@ -196,22 +196,22 @@
    1.54  lemma crel_tapI [crel_intros]:
    1.55    assumes "h' = h" "r = f h"
    1.56    shows "crel (tap f) h h' r"
    1.57 -  by (rule crelI) (simp add: assms)
    1.58 +  by (rule crelI) (simp add: assms execute_simps)
    1.59  
    1.60  lemma crel_tapE [crel_elims]:
    1.61    assumes "crel (tap f) h h' r"
    1.62    obtains "h' = h" and "r = f h"
    1.63 -  using assms by (rule crelE) auto
    1.64 +  using assms by (rule crelE) (auto simp add: execute_simps)
    1.65  
    1.66  lemma crel_heapI [crel_intros]:
    1.67    assumes "h' = snd (f h)" "r = fst (f h)"
    1.68    shows "crel (heap f) h h' r"
    1.69 -  by (rule crelI) (simp add: assms)
    1.70 +  by (rule crelI) (simp add: assms execute_simps)
    1.71  
    1.72  lemma crel_heapE [crel_elims]:
    1.73    assumes "crel (heap f) h h' r"
    1.74    obtains "h' = snd (f h)" and "r = fst (f h)"
    1.75 -  using assms by (rule crelE) simp
    1.76 +  using assms by (rule crelE) (simp add: execute_simps)
    1.77  
    1.78  lemma crel_guardI [crel_intros]:
    1.79    assumes "P h" "h' = snd (f h)" "r = fst (f h)"
    1.80 @@ -230,34 +230,34 @@
    1.81  definition return :: "'a \<Rightarrow> 'a Heap" where
    1.82    [code del]: "return x = heap (Pair x)"
    1.83  
    1.84 -lemma execute_return [simp, execute_simps]:
    1.85 +lemma execute_return [execute_simps]:
    1.86    "execute (return x) = Some \<circ> Pair x"
    1.87 -  by (simp add: return_def)
    1.88 +  by (simp add: return_def execute_simps)
    1.89  
    1.90 -lemma success_returnI [iff, success_intros]:
    1.91 +lemma success_returnI [success_intros]:
    1.92    "success (return x) h"
    1.93 -  by (rule successI) simp
    1.94 +  by (rule successI) (simp add: execute_simps)
    1.95  
    1.96  lemma crel_returnI [crel_intros]:
    1.97    "h = h' \<Longrightarrow> crel (return x) h h' x"
    1.98 -  by (rule crelI) simp
    1.99 +  by (rule crelI) (simp add: execute_simps)
   1.100  
   1.101  lemma crel_returnE [crel_elims]:
   1.102    assumes "crel (return x) h h' r"
   1.103    obtains "r = x" "h' = h"
   1.104 -  using assms by (rule crelE) simp
   1.105 +  using assms by (rule crelE) (simp add: execute_simps)
   1.106  
   1.107  definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
   1.108    [code del]: "raise s = Heap (\<lambda>_. None)"
   1.109  
   1.110 -lemma execute_raise [simp, execute_simps]:
   1.111 +lemma execute_raise [execute_simps]:
   1.112    "execute (raise s) = (\<lambda>_. None)"
   1.113    by (simp add: raise_def)
   1.114  
   1.115  lemma crel_raiseE [crel_elims]:
   1.116    assumes "crel (raise x) h h' r"
   1.117    obtains "False"
   1.118 -  using assms by (rule crelE) (simp add: success_def)
   1.119 +  using assms by (rule crelE) (simp add: success_def execute_simps)
   1.120  
   1.121  definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
   1.122    [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
   1.123 @@ -303,16 +303,16 @@
   1.124    using assms by (simp add: bind_def)
   1.125  
   1.126  lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
   1.127 -  by (rule Heap_eqI) (simp add: execute_bind)
   1.128 +  by (rule Heap_eqI) (simp add: execute_bind execute_simps)
   1.129  
   1.130  lemma bind_return [simp]: "f \<guillemotright>= return = f"
   1.131 -  by (rule Heap_eqI) (simp add: bind_def split: option.splits)
   1.132 +  by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
   1.133  
   1.134  lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
   1.135 -  by (rule Heap_eqI) (simp add: bind_def split: option.splits)
   1.136 +  by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
   1.137  
   1.138  lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
   1.139 -  by (rule Heap_eqI) (simp add: execute_bind)
   1.140 +  by (rule Heap_eqI) (simp add: execute_simps)
   1.141  
   1.142  abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap"  (infixl ">>" 54) where
   1.143    "f >> g \<equiv> f >>= (\<lambda>_. g)"
   1.144 @@ -411,7 +411,7 @@
   1.145  lemma execute_assert [execute_simps]:
   1.146    "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
   1.147    "\<not> P x \<Longrightarrow> execute (assert P x) h = None"
   1.148 -  by (simp_all add: assert_def)
   1.149 +  by (simp_all add: assert_def execute_simps)
   1.150  
   1.151  lemma success_assertI [success_intros]:
   1.152    "P x \<Longrightarrow> success (assert P x) h"
   1.153 @@ -466,14 +466,14 @@
   1.154    shows "execute (fold_map f xs) h =
   1.155      Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
   1.156  using assms proof (induct xs)
   1.157 -  case Nil show ?case by simp
   1.158 +  case Nil show ?case by (simp add: execute_simps)
   1.159  next
   1.160    case (Cons x xs)
   1.161    from Cons.prems obtain y
   1.162      where y: "execute (f x) h = Some (y, h)" by auto
   1.163    moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h =
   1.164      Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto
   1.165 -  ultimately show ?case by (simp, simp only: execute_bind(1), simp)
   1.166 +  ultimately show ?case by (simp, simp only: execute_bind(1), simp add: execute_simps)
   1.167  qed
   1.168  
   1.169  subsection {* Code generator setup *}