pervasive success combinator
authorhaftmann
Fri Jul 09 16:58:44 2010 +0200 (2010-07-09)
changeset 37758bf86a65403a8
parent 37756 59caa6180fff
child 37759 00ff97087ab5
pervasive success combinator
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Imperative_HOL/Relational.thy
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Fri Jul 09 10:08:10 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Fri Jul 09 16:58:44 2010 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4    [code del]: "make n f = Heap_Monad.heap (array (map f [0 ..< n]))"
     1.5  
     1.6  definition len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
     1.7 -  [code del]: "len a = Heap_Monad.heap (\<lambda>h. (length a h, h))"
     1.8 +  [code del]: "len a = Heap_Monad.tap (\<lambda>h. length a h)"
     1.9  
    1.10  definition nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" where
    1.11    [code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length a h)
    1.12 @@ -75,7 +75,7 @@
    1.13      (\<lambda>h. (get_array a h ! i, change a i x h))"
    1.14  
    1.15  definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where
    1.16 -  [code del]: "freeze a = Heap_Monad.heap (\<lambda>h. (get_array a h, h))"
    1.17 +  [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)"
    1.18  
    1.19  
    1.20  subsection {* Properties *}
    1.21 @@ -83,6 +83,8 @@
    1.22  text {* FIXME: Does there exist a "canonical" array axiomatisation in
    1.23  the literature?  *}
    1.24  
    1.25 +text {* Primitives *}
    1.26 +
    1.27  lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
    1.28    and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
    1.29    unfolding noteq_arrs_def by auto
    1.30 @@ -153,50 +155,89 @@
    1.31    "array_present a (change b i v h) = array_present a h"
    1.32    by (simp add: change_def array_present_def set_array_def get_array_def)
    1.33  
    1.34 -lemma execute_new [simp]:
    1.35 -  "Heap_Monad.execute (new n x) h = Some (array (replicate n x) h)"
    1.36 +
    1.37 +text {* Monad operations *}
    1.38 +
    1.39 +lemma execute_new [simp, execute_simps]:
    1.40 +  "execute (new n x) h = Some (array (replicate n x) h)"
    1.41 +  by (simp add: new_def)
    1.42 +
    1.43 +lemma success_newI [iff, success_intros]:
    1.44 +  "success (new n x) h"
    1.45    by (simp add: new_def)
    1.46  
    1.47 -lemma execute_of_list [simp]:
    1.48 -  "Heap_Monad.execute (of_list xs) h = Some (array xs h)"
    1.49 +lemma execute_of_list [simp, execute_simps]:
    1.50 +  "execute (of_list xs) h = Some (array xs h)"
    1.51 +  by (simp add: of_list_def)
    1.52 +
    1.53 +lemma success_of_listI [iff, success_intros]:
    1.54 +  "success (of_list xs) h"
    1.55    by (simp add: of_list_def)
    1.56  
    1.57 -lemma execute_make [simp]:
    1.58 -  "Heap_Monad.execute (make n f) h = Some (array (map f [0 ..< n]) h)"
    1.59 +lemma execute_make [simp, execute_simps]:
    1.60 +  "execute (make n f) h = Some (array (map f [0 ..< n]) h)"
    1.61    by (simp add: make_def)
    1.62  
    1.63 -lemma execute_len [simp]:
    1.64 -  "Heap_Monad.execute (len a) h = Some (length a h, h)"
    1.65 +lemma success_makeI [iff, success_intros]:
    1.66 +  "success (make n f) h"
    1.67 +  by (simp add: make_def)
    1.68 +
    1.69 +lemma execute_len [simp, execute_simps]:
    1.70 +  "execute (len a) h = Some (length a h, h)"
    1.71 +  by (simp add: len_def)
    1.72 +
    1.73 +lemma success_lenI [iff, success_intros]:
    1.74 +  "success (len a) h"
    1.75    by (simp add: len_def)
    1.76  
    1.77 -lemma execute_nth [simp]:
    1.78 +lemma execute_nth [execute_simps]:
    1.79    "i < length a h \<Longrightarrow>
    1.80 -    Heap_Monad.execute (nth a i) h = Some (get_array a h ! i, h)"
    1.81 -  "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
    1.82 -  by (simp_all add: nth_def)
    1.83 +    execute (nth a i) h = Some (get_array a h ! i, h)"
    1.84 +  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
    1.85 +  by (simp_all add: nth_def execute_simps)
    1.86 +
    1.87 +lemma success_nthI [success_intros]:
    1.88 +  "i < length a h \<Longrightarrow> success (nth a i) h"
    1.89 +  by (auto intro: success_intros simp add: nth_def)
    1.90  
    1.91 -lemma execute_upd [simp]:
    1.92 +lemma execute_upd [execute_simps]:
    1.93    "i < length a h \<Longrightarrow>
    1.94 -    Heap_Monad.execute (upd i x a) h = Some (a, change a i x h)"
    1.95 -  "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
    1.96 -  by (simp_all add: upd_def)
    1.97 +    execute (upd i x a) h = Some (a, change a i x h)"
    1.98 +  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
    1.99 +  by (simp_all add: upd_def execute_simps)
   1.100  
   1.101 -lemma execute_map_entry [simp]:
   1.102 +lemma success_updI [success_intros]:
   1.103 +  "i < length a h \<Longrightarrow> success (upd i x a) h"
   1.104 +  by (auto intro: success_intros simp add: upd_def)
   1.105 +
   1.106 +lemma execute_map_entry [execute_simps]:
   1.107    "i < length a h \<Longrightarrow>
   1.108 -   Heap_Monad.execute (map_entry i f a) h =
   1.109 +   execute (map_entry i f a) h =
   1.110        Some (a, change a i (f (get_array a h ! i)) h)"
   1.111 -  "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
   1.112 -  by (simp_all add: map_entry_def)
   1.113 +  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
   1.114 +  by (simp_all add: map_entry_def execute_simps)
   1.115  
   1.116 -lemma execute_swap [simp]:
   1.117 +lemma success_map_entryI [success_intros]:
   1.118 +  "i < length a h \<Longrightarrow> success (map_entry i f a) h"
   1.119 +  by (auto intro: success_intros simp add: map_entry_def)
   1.120 +
   1.121 +lemma execute_swap [execute_simps]:
   1.122    "i < length a h \<Longrightarrow>
   1.123 -   Heap_Monad.execute (swap i x a) h =
   1.124 +   execute (swap i x a) h =
   1.125        Some (get_array a h ! i, change a i x h)"
   1.126 -  "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
   1.127 -  by (simp_all add: swap_def)
   1.128 +  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
   1.129 +  by (simp_all add: swap_def execute_simps)
   1.130 +
   1.131 +lemma success_swapI [success_intros]:
   1.132 +  "i < length a h \<Longrightarrow> success (swap i x a) h"
   1.133 +  by (auto intro: success_intros simp add: swap_def)
   1.134  
   1.135 -lemma execute_freeze [simp]:
   1.136 -  "Heap_Monad.execute (freeze a) h = Some (get_array a h, h)"
   1.137 +lemma execute_freeze [simp, execute_simps]:
   1.138 +  "execute (freeze a) h = Some (get_array a h, h)"
   1.139 +  by (simp add: freeze_def)
   1.140 +
   1.141 +lemma success_freezeI [iff, success_intros]:
   1.142 +  "success (freeze a) h"
   1.143    by (simp add: freeze_def)
   1.144  
   1.145  lemma upd_return:
   1.146 @@ -265,7 +306,7 @@
   1.147       x \<leftarrow> nth a i;
   1.148       upd i (f x) a
   1.149     done)"
   1.150 -  by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def)
   1.151 +  by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps)
   1.152  
   1.153  lemma [code]:
   1.154    "swap i x a = (do
   1.155 @@ -273,7 +314,7 @@
   1.156       upd i x a;
   1.157       return y
   1.158     done)"
   1.159 -  by (rule Heap_eqI) (simp add: bind_def guard_def swap_def)
   1.160 +  by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps)
   1.161  
   1.162  lemma [code]:
   1.163    "freeze a = (do
   1.164 @@ -288,18 +329,18 @@
   1.165       [0..<length a h] =
   1.166         List.map (List.nth (get_array a h)) [0..<length a h]"
   1.167      by simp
   1.168 -  have "Heap_Monad.execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h =
   1.169 +  have "execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h =
   1.170      Some (get_array a h, h)"
   1.171      apply (subst execute_fold_map_unchanged_heap)
   1.172      apply (simp_all add: nth_def guard_def *)
   1.173      apply (simp add: length_def map_nth)
   1.174      done
   1.175 -  then have "Heap_Monad.execute (do
   1.176 +  then have "execute (do
   1.177        n \<leftarrow> len a;
   1.178        Heap_Monad.fold_map (Array.nth a) [0..<n]
   1.179      done) h = Some (get_array a h, h)"
   1.180      by (auto intro: execute_eq_SomeI)
   1.181 -  then show "Heap_Monad.execute (freeze a) h = Heap_Monad.execute (do
   1.182 +  then show "execute (freeze a) h = execute (do
   1.183        n \<leftarrow> len a;
   1.184        Heap_Monad.fold_map (Array.nth a) [0..<n]
   1.185      done) h" by simp
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 09 10:08:10 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 09 16:58:44 2010 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  
     2.5  subsection {* The monad *}
     2.6  
     2.7 -subsubsection {* Monad combinators *}
     2.8 +subsubsection {* Monad construction *}
     2.9  
    2.10  text {* Monadic heap actions either produce values
    2.11    and transform the heap, or fail *}
    2.12 @@ -19,6 +19,13 @@
    2.13  primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where
    2.14    [code del]: "execute (Heap f) = f"
    2.15  
    2.16 +lemma Heap_cases [case_names succeed fail]:
    2.17 +  fixes f and h
    2.18 +  assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
    2.19 +  assumes fail: "execute f h = None \<Longrightarrow> P"
    2.20 +  shows P
    2.21 +  using assms by (cases "execute f h") auto
    2.22 +
    2.23  lemma Heap_execute [simp]:
    2.24    "Heap (execute f) = f" by (cases f) simp_all
    2.25  
    2.26 @@ -26,43 +33,98 @@
    2.27    "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
    2.28      by (cases f, cases g) (auto simp: expand_fun_eq)
    2.29  
    2.30 -lemma Heap_eqI':
    2.31 -  "(\<And>h. (\<lambda>x. execute (f x) h) = (\<lambda>y. execute (g y) h)) \<Longrightarrow> f = g"
    2.32 -    by (auto simp: expand_fun_eq intro: Heap_eqI)
    2.33 +ML {* structure Execute_Simps = Named_Thms(
    2.34 +  val name = "execute_simps"
    2.35 +  val description = "simplification rules for execute"
    2.36 +) *}
    2.37 +
    2.38 +setup Execute_Simps.setup
    2.39 +
    2.40 +lemma execute_Let [simp, execute_simps]:
    2.41 +  "execute (let x = t in f x) = (let x = t in execute (f x))"
    2.42 +  by (simp add: Let_def)
    2.43 +
    2.44 +
    2.45 +subsubsection {* Specialised lifters *}
    2.46 +
    2.47 +definition tap :: "(heap \<Rightarrow> 'a) \<Rightarrow> 'a Heap" where
    2.48 +  [code del]: "tap f = Heap (\<lambda>h. Some (f h, h))"
    2.49 +
    2.50 +lemma execute_tap [simp, execute_simps]:
    2.51 +  "execute (tap f) h = Some (f h, h)"
    2.52 +  by (simp add: tap_def)
    2.53  
    2.54  definition heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
    2.55    [code del]: "heap f = Heap (Some \<circ> f)"
    2.56  
    2.57 -lemma execute_heap [simp]:
    2.58 +lemma execute_heap [simp, execute_simps]:
    2.59    "execute (heap f) = Some \<circ> f"
    2.60    by (simp add: heap_def)
    2.61  
    2.62  definition guard :: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
    2.63    [code del]: "guard P f = Heap (\<lambda>h. if P h then Some (f h) else None)"
    2.64  
    2.65 -lemma execute_guard [simp]:
    2.66 +lemma execute_guard [execute_simps]:
    2.67    "\<not> P h \<Longrightarrow> execute (guard P f) h = None"
    2.68    "P h \<Longrightarrow> execute (guard P f) h = Some (f h)"
    2.69    by (simp_all add: guard_def)
    2.70  
    2.71 -lemma heap_cases [case_names succeed fail]:
    2.72 -  fixes f and h
    2.73 -  assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
    2.74 -  assumes fail: "execute f h = None \<Longrightarrow> P"
    2.75 -  shows P
    2.76 -  using assms by (cases "execute f h") auto
    2.77 +
    2.78 +subsubsection {* Predicate classifying successful computations *}
    2.79 +
    2.80 +definition success :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool" where
    2.81 +  "success f h \<longleftrightarrow> execute f h \<noteq> None"
    2.82 +
    2.83 +lemma successI:
    2.84 +  "execute f h \<noteq> None \<Longrightarrow> success f h"
    2.85 +  by (simp add: success_def)
    2.86 +
    2.87 +lemma successE:
    2.88 +  assumes "success f h"
    2.89 +  obtains r h' where "execute f h = Some (r, h')"
    2.90 +  using assms by (auto simp add: success_def)
    2.91 +
    2.92 +ML {* structure Success_Intros = Named_Thms(
    2.93 +  val name = "success_intros"
    2.94 +  val description = "introduction rules for success"
    2.95 +) *}
    2.96 +
    2.97 +setup Success_Intros.setup
    2.98 +
    2.99 +lemma success_tapI [iff, success_intros]:
   2.100 +  "success (tap f) h"
   2.101 +  by (rule successI) simp
   2.102 +
   2.103 +lemma success_heapI [iff, success_intros]:
   2.104 +  "success (heap f) h"
   2.105 +  by (rule successI) simp
   2.106 +
   2.107 +lemma success_guardI [success_intros]:
   2.108 +  "P h \<Longrightarrow> success (guard P f) h"
   2.109 +  by (rule successI) (simp add: execute_guard)
   2.110 +
   2.111 +lemma success_LetI [success_intros]:
   2.112 +  "x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h"
   2.113 +  by (simp add: Let_def)
   2.114 +
   2.115 +
   2.116 +subsubsection {* Monad combinators *}
   2.117  
   2.118  definition return :: "'a \<Rightarrow> 'a Heap" where
   2.119    [code del]: "return x = heap (Pair x)"
   2.120  
   2.121 -lemma execute_return [simp]:
   2.122 +lemma execute_return [simp, execute_simps]:
   2.123    "execute (return x) = Some \<circ> Pair x"
   2.124    by (simp add: return_def)
   2.125  
   2.126 +lemma success_returnI [iff, success_intros]:
   2.127 +  "success (return x) h"
   2.128 +  by (rule successI) simp
   2.129 +
   2.130  definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
   2.131    [code del]: "raise s = Heap (\<lambda>_. None)"
   2.132  
   2.133 -lemma execute_raise [simp]:
   2.134 +lemma execute_raise [simp, execute_simps]:
   2.135    "execute (raise s) = (\<lambda>_. None)"
   2.136    by (simp add: raise_def)
   2.137  
   2.138 @@ -73,14 +135,18 @@
   2.139  
   2.140  notation bind (infixl "\<guillemotright>=" 54)
   2.141  
   2.142 -lemma execute_bind [simp]:
   2.143 +lemma execute_bind [execute_simps]:
   2.144    "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
   2.145    "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
   2.146    by (simp_all add: bind_def)
   2.147  
   2.148 -lemma execute_bind_heap [simp]:
   2.149 -  "execute (heap f \<guillemotright>= g) h = execute (g (fst (f h))) (snd (f h))"
   2.150 -  by (simp add: bind_def split_def)
   2.151 +lemma success_bindI [success_intros]:
   2.152 +  "success f h \<Longrightarrow> success (g (fst (the (execute f h)))) (snd (the (execute f h))) \<Longrightarrow> success (f \<guillemotright>= g) h"
   2.153 +  by (auto intro!: successI elim!: successE simp add: bind_def)
   2.154 +
   2.155 +lemma execute_bind_successI [execute_simps]:
   2.156 +  "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
   2.157 +  by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
   2.158    
   2.159  lemma execute_eq_SomeI:
   2.160    assumes "Heap_Monad.execute f h = Some (x, h')"
   2.161 @@ -89,7 +155,7 @@
   2.162    using assms by (simp add: bind_def)
   2.163  
   2.164  lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
   2.165 -  by (rule Heap_eqI) simp
   2.166 +  by (rule Heap_eqI) (simp add: execute_bind)
   2.167  
   2.168  lemma bind_return [simp]: "f \<guillemotright>= return = f"
   2.169    by (rule Heap_eqI) (simp add: bind_def split: option.splits)
   2.170 @@ -98,7 +164,7 @@
   2.171    by (rule Heap_eqI) (simp add: bind_def split: option.splits)
   2.172  
   2.173  lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
   2.174 -  by (rule Heap_eqI) simp
   2.175 +  by (rule Heap_eqI) (simp add: execute_bind)
   2.176  
   2.177  abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap"  (infixl ">>" 54) where
   2.178    "f >> g \<equiv> f >>= (\<lambda>_. g)"
   2.179 @@ -187,24 +253,31 @@
   2.180  *}
   2.181  
   2.182  
   2.183 -subsection {* Monad properties *}
   2.184 +subsection {* Generic combinators *}
   2.185  
   2.186 -subsection {* Generic combinators *}
   2.187 +subsubsection {* Assertions *}
   2.188  
   2.189  definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where
   2.190    "assert P x = (if P x then return x else raise ''assert'')"
   2.191  
   2.192 -lemma execute_assert [simp]:
   2.193 +lemma execute_assert [execute_simps]:
   2.194    "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
   2.195    "\<not> P x \<Longrightarrow> execute (assert P x) h = None"
   2.196    by (simp_all add: assert_def)
   2.197  
   2.198 +lemma success_assertI [success_intros]:
   2.199 +  "P x \<Longrightarrow> success (assert P x) h"
   2.200 +  by (rule successI) (simp add: execute_assert)
   2.201 +
   2.202  lemma assert_cong [fundef_cong]:
   2.203    assumes "P = P'"
   2.204    assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
   2.205    shows "(assert P x >>= f) = (assert P' x >>= f')"
   2.206    by (rule Heap_eqI) (insert assms, simp add: assert_def)
   2.207  
   2.208 +
   2.209 +subsubsection {* Plain lifting *}
   2.210 +
   2.211  definition lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where
   2.212    "lift f = return o f"
   2.213  
   2.214 @@ -216,6 +289,9 @@
   2.215    "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
   2.216    by (simp add: lift_def comp_def)
   2.217  
   2.218 +
   2.219 +subsubsection {* Iteration -- warning: this is rarely useful! *}
   2.220 +
   2.221  primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
   2.222    "fold_map f [] = return []"
   2.223  | "fold_map f (x # xs) = do
   2.224 @@ -228,7 +304,7 @@
   2.225    "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
   2.226    by (induct xs) simp_all
   2.227  
   2.228 -lemma execute_fold_map_unchanged_heap:
   2.229 +lemma execute_fold_map_unchanged_heap [execute_simps]:
   2.230    assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)"
   2.231    shows "execute (fold_map f xs) h =
   2.232      Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
   2.233 @@ -527,6 +603,6 @@
   2.234  code_const return (Haskell "return")
   2.235  code_const Heap_Monad.raise' (Haskell "error/ _")
   2.236  
   2.237 -hide_const (open) Heap heap guard execute raise' fold_map
   2.238 +hide_const (open) Heap heap guard raise' fold_map
   2.239  
   2.240  end
     3.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 09 10:08:10 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 09 16:58:44 2010 +0200
     3.3 @@ -42,7 +42,7 @@
     3.4    [code del]: "ref v = Heap_Monad.heap (alloc v)"
     3.5  
     3.6  definition lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where
     3.7 -  [code del]: "lookup r = Heap_Monad.heap (\<lambda>h. (get h r, h))"
     3.8 +  [code del]: "lookup r = Heap_Monad.tap (\<lambda>h. get h r)"
     3.9  
    3.10  definition update :: "'a ref \<Rightarrow> 'a\<Colon>heap \<Rightarrow> unit Heap" ("_ := _" 62) where
    3.11    [code del]: "update r v = Heap_Monad.heap (\<lambda>h. ((), set r v h))"
    3.12 @@ -58,6 +58,8 @@
    3.13  
    3.14  subsection {* Properties *}
    3.15  
    3.16 +text {* Primitives *}
    3.17 +
    3.18  lemma noteq_sym: "r =!= s \<Longrightarrow> s =!= r"
    3.19    and unequal [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" -- "same types!"
    3.20    by (auto simp add: noteq_def)
    3.21 @@ -126,26 +128,44 @@
    3.22    "present h r \<Longrightarrow> \<not> present h r' \<Longrightarrow> r =!= r'"
    3.23    by (auto simp add: noteq_def present_def)
    3.24  
    3.25 -lemma execute_ref [simp]:
    3.26 -  "Heap_Monad.execute (ref v) h = Some (alloc v h)"
    3.27 +
    3.28 +text {* Monad operations *}
    3.29 +
    3.30 +lemma execute_ref [simp, execute_simps]:
    3.31 +  "execute (ref v) h = Some (alloc v h)"
    3.32    by (simp add: ref_def)
    3.33  
    3.34 -lemma execute_lookup [simp]:
    3.35 +lemma success_refI [iff, success_intros]:
    3.36 +  "success (ref v) h"
    3.37 +  by (auto simp add: ref_def)
    3.38 +
    3.39 +lemma execute_lookup [simp, execute_simps]:
    3.40    "Heap_Monad.execute (lookup r) h = Some (get h r, h)"
    3.41    by (simp add: lookup_def)
    3.42  
    3.43 -lemma execute_update [simp]:
    3.44 +lemma success_lookupI [iff, success_intros]:
    3.45 +  "success (lookup r) h"
    3.46 +  by (auto simp add: lookup_def)
    3.47 +
    3.48 +lemma execute_update [simp, execute_simps]:
    3.49    "Heap_Monad.execute (update r v) h = Some ((), set r v h)"
    3.50    by (simp add: update_def)
    3.51  
    3.52 -lemma execute_change [simp]:
    3.53 +lemma success_updateI [iff, success_intros]:
    3.54 +  "success (update r v) h"
    3.55 +  by (auto simp add: update_def)
    3.56 +
    3.57 +lemma execute_change [simp, execute_simps]:
    3.58    "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)"
    3.59 -  by (cases "!r" h rule: heap_cases)
    3.60 -    (simp_all only: change_def execute_bind, auto simp add: Let_def)
    3.61 +  by (simp add: change_def bind_def Let_def)
    3.62 +
    3.63 +lemma success_changeI [iff, success_intros]:
    3.64 +  "success (change f r) h"
    3.65 +  by (auto intro!: success_intros simp add: change_def)
    3.66  
    3.67  lemma lookup_chain:
    3.68    "(!r \<guillemotright> f) = f"
    3.69 -  by (rule Heap_eqI) (simp add: lookup_def)
    3.70 +  by (rule Heap_eqI) (auto simp add: lookup_def execute_simps)
    3.71  
    3.72  lemma update_change [code]:
    3.73    "r := e = change (\<lambda>_. e) r \<guillemotright> return ()"
    3.74 @@ -233,4 +253,4 @@
    3.75  code_const Ref.lookup (Haskell "Heap.readSTRef")
    3.76  code_const Ref.update (Haskell "Heap.writeSTRef")
    3.77  
    3.78 -end
    3.79 \ No newline at end of file
    3.80 +end
     4.1 --- a/src/HOL/Imperative_HOL/Relational.thy	Fri Jul 09 10:08:10 2010 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/Relational.thy	Fri Jul 09 16:58:44 2010 +0200
     4.3 @@ -23,6 +23,11 @@
     4.4  text {* For all commands, we define simple elimination rules. *}
     4.5  (* FIXME: consumes 1 necessary ?? *)
     4.6  
     4.7 +lemma crel_tap:
     4.8 +  assumes "crel (Heap_Monad.tap f) h h' r"
     4.9 +  obtains "h' = h" "r = f h"
    4.10 +  using assms by (simp add: crel_def)
    4.11 +
    4.12  lemma crel_heap:
    4.13    assumes "crel (Heap_Monad.heap f) h h' r"
    4.14    obtains "h' = snd (f h)" "r = fst (f h)"
    4.15 @@ -31,7 +36,7 @@
    4.16  lemma crel_guard:
    4.17    assumes "crel (Heap_Monad.guard P f) h h' r"
    4.18    obtains "h' = snd (f h)" "r = fst (f h)" "P h"
    4.19 -  using assms by (cases "f h", cases "P h") (simp_all add: crel_def)
    4.20 +  using assms by (cases "f h", cases "P h") (simp_all add: crel_def execute_simps)
    4.21  
    4.22  
    4.23  subsection {* Elimination rules for basic monadic commands *}
    4.24 @@ -121,7 +126,7 @@
    4.25    assumes "crel (len a) h h' r"
    4.26    obtains "h = h'" "r = Array.length a h'"
    4.27    using assms unfolding Array.len_def
    4.28 -  by (elim crel_heap) simp
    4.29 +  by (elim crel_tap) simp
    4.30  
    4.31  lemma crel_nth[consumes 1]:
    4.32    assumes "crel (nth a i) h h' r"
    4.33 @@ -184,7 +189,7 @@
    4.34    assumes "crel (Array.freeze a) h h' xs"
    4.35    obtains "h = h'" "xs = get_array a h"
    4.36    using assms unfolding freeze_def
    4.37 -  by (elim crel_heap) simp
    4.38 +  by (elim crel_tap) simp
    4.39  
    4.40  lemma crel_fold_map_map_entry_remains:
    4.41    assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
    4.42 @@ -314,23 +319,20 @@
    4.43  lemma crel_lookup:
    4.44    assumes "crel (!r') h h' r"
    4.45    obtains "h = h'" "r = Ref.get h r'"
    4.46 -using assms
    4.47 -unfolding Ref.lookup_def
    4.48 -by (auto elim: crel_heap)
    4.49 +  using assms unfolding Ref.lookup_def
    4.50 +  by (auto elim: crel_tap)
    4.51  
    4.52  lemma crel_update:
    4.53    assumes "crel (r' := v) h h' r"
    4.54    obtains "h' = Ref.set r' v h" "r = ()"
    4.55 -using assms
    4.56 -unfolding Ref.update_def
    4.57 -by (auto elim: crel_heap)
    4.58 +  using assms unfolding Ref.update_def
    4.59 +  by (auto elim: crel_heap)
    4.60  
    4.61  lemma crel_change:
    4.62    assumes "crel (Ref.change f r') h h' r"
    4.63    obtains "h' = Ref.set r' (f (Ref.get h r')) h" "r = f (Ref.get h r')"
    4.64 -using assms
    4.65 -unfolding Ref.change_def Let_def
    4.66 -by (auto elim!: crelE crel_lookup crel_update crel_return)
    4.67 +  using assms unfolding Ref.change_def Let_def
    4.68 +  by (auto elim!: crelE crel_lookup crel_update crel_return)
    4.69  
    4.70  subsection {* Elimination rules for the assert command *}
    4.71  
    4.72 @@ -388,6 +390,11 @@
    4.73  using assms
    4.74  by (auto split: option.split)
    4.75  
    4.76 +lemma crel_tapI:
    4.77 +  assumes "h' = h" "r = f h"
    4.78 +  shows "crel (Heap_Monad.tap f) h h' r"
    4.79 +  using assms by (simp add: crel_def)
    4.80 +
    4.81  lemma crel_heapI:
    4.82    shows "crel (Heap_Monad.heap f) h (snd (f h)) (fst (f h))"
    4.83    by (simp add: crel_def apfst_def split_def prod_fun_def)
    4.84 @@ -401,7 +408,7 @@
    4.85  lemma crel_guardI:
    4.86    assumes "P h" "h' = snd (f h)" "r = fst (f h)"
    4.87    shows "crel (Heap_Monad.guard P f) h h' r"
    4.88 -  using assms by (simp add: crel_def)
    4.89 +  using assms by (simp add: crel_def execute_simps)
    4.90  
    4.91  lemma crelI2:
    4.92    assumes "\<exists>h' rs'. crel f h h' rs' \<and> (\<exists>h'' rs. crel (g rs') h' h'' rs)"
    4.93 @@ -418,8 +425,7 @@
    4.94  
    4.95  lemma crel_lengthI:
    4.96    shows "crel (Array.len a) h h (Array.length a h)"
    4.97 -  unfolding len_def
    4.98 -  by (rule crel_heapI') auto
    4.99 +  unfolding len_def by (rule crel_tapI) simp_all
   4.100  
   4.101  (* thm crel_newI for Array.new is missing *)
   4.102  
   4.103 @@ -449,7 +455,7 @@
   4.104  
   4.105  lemma crel_lookupI:
   4.106    shows "crel (!r) h h (Ref.get h r)"
   4.107 -  unfolding lookup_def by (auto intro!: crel_heapI')
   4.108 +  unfolding lookup_def by (auto intro!: crel_tapI)
   4.109  
   4.110  lemma crel_updateI:
   4.111    shows "crel (r := v) h (Ref.set r v h) ()"
   4.112 @@ -457,7 +463,7 @@
   4.113  
   4.114  lemma crel_changeI: 
   4.115    shows "crel (Ref.change f r) h (Ref.set r (f (Ref.get h r)) h) (f (Ref.get h r))"
   4.116 -unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
   4.117 +  unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
   4.118  
   4.119  subsubsection {* Introduction rules for the assert command *}
   4.120  
   4.121 @@ -487,173 +493,26 @@
   4.122  next
   4.123  qed (auto simp add: assms(2)[unfolded crel_def])
   4.124  
   4.125 -section {* Definition of the noError predicate *}
   4.126  
   4.127 -text {* We add a simple definitional setting for crel intro rules
   4.128 -  where we only would like to show that the computation does not result in a exception for heap h,
   4.129 -  but we do not care about statements about the resulting heap and return value.*}
   4.130 -
   4.131 -definition noError :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool"
   4.132 -where
   4.133 -  "noError c h \<longleftrightarrow> (\<exists>r h'. Some (r, h') = Heap_Monad.execute c h)"
   4.134 -
   4.135 -lemma noError_def': -- FIXME
   4.136 -  "noError c h \<longleftrightarrow> (\<exists>r h'. Heap_Monad.execute c h = Some (r, h'))"
   4.137 -  unfolding noError_def apply auto proof -
   4.138 -  fix r h'
   4.139 -  assume "Some (r, h') = Heap_Monad.execute c h"
   4.140 -  then have "Heap_Monad.execute c h = Some (r, h')" ..
   4.141 -  then show "\<exists>r h'. Heap_Monad.execute c h = Some (r, h')" by blast
   4.142 -qed
   4.143 -
   4.144 -subsection {* Introduction rules for basic monadic commands *}
   4.145 -
   4.146 -lemma noErrorI:
   4.147 -  assumes "noError f h"
   4.148 -  assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError (g r) h'"
   4.149 -  shows "noError (f \<guillemotright>= g) h"
   4.150 -  using assms
   4.151 -  by (auto simp add: noError_def' crel_def' bind_def)
   4.152 -
   4.153 -lemma noErrorI':
   4.154 -  assumes "noError f h"
   4.155 -  assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError g h'"
   4.156 -  shows "noError (f \<guillemotright> g) h"
   4.157 -  using assms
   4.158 -  by (auto simp add: noError_def' crel_def' bind_def)
   4.159 -
   4.160 -lemma noErrorI2:
   4.161 -"\<lbrakk>crel f h h' r ; noError f h; noError (g r) h'\<rbrakk>
   4.162 -\<Longrightarrow> noError (f \<guillemotright>= g) h"
   4.163 -by (auto simp add: noError_def' crel_def' bind_def)
   4.164 -
   4.165 -lemma noError_return: 
   4.166 -  shows "noError (return x) h"
   4.167 -  unfolding noError_def return_def
   4.168 -  by auto
   4.169 -
   4.170 -lemma noError_if:
   4.171 -  assumes "c \<Longrightarrow> noError t h" "\<not> c \<Longrightarrow> noError e h"
   4.172 -  shows "noError (if c then t else e) h"
   4.173 -  using assms
   4.174 -  unfolding noError_def
   4.175 -  by auto
   4.176 -
   4.177 -lemma noError_option_case:
   4.178 -  assumes "\<And>y. x = Some y \<Longrightarrow> noError (s y) h"
   4.179 -  assumes "noError n h"
   4.180 -  shows "noError (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h"
   4.181 -using assms
   4.182 -by (auto split: option.split)
   4.183 -
   4.184 -lemma noError_fold_map: 
   4.185 -assumes "\<forall>x \<in> set xs. noError (f x) h \<and> crel (f x) h h (r x)" 
   4.186 -shows "noError (Heap_Monad.fold_map f xs) h"
   4.187 -using assms
   4.188 -proof (induct xs)
   4.189 -  case Nil
   4.190 -  thus ?case
   4.191 -    unfolding fold_map.simps by (intro noError_return)
   4.192 -next
   4.193 -  case (Cons x xs)
   4.194 -  thus ?case
   4.195 -    unfolding fold_map.simps
   4.196 -    by (auto intro: noErrorI2[of "f x"] noErrorI noError_return)
   4.197 -qed
   4.198 -
   4.199 -lemma noError_heap [simp]:
   4.200 -  "noError (Heap_Monad.heap f) h"
   4.201 -  by (simp add: noError_def')
   4.202 -
   4.203 -lemma noError_guard [simp]:
   4.204 -  "P h \<Longrightarrow> noError (Heap_Monad.guard P f) h"
   4.205 -  by (simp add: noError_def')
   4.206 -
   4.207 -subsection {* Introduction rules for array commands *}
   4.208 -
   4.209 -lemma noError_length:
   4.210 -  shows "noError (Array.len a) h"
   4.211 -  by (simp add: len_def)
   4.212 -
   4.213 -lemma noError_new:
   4.214 -  shows "noError (Array.new n v) h"
   4.215 -  by (simp add: Array.new_def)
   4.216 -
   4.217 -lemma noError_upd:
   4.218 -  assumes "i < Array.length a h"
   4.219 -  shows "noError (Array.upd i v a) h"
   4.220 -  using assms by (simp add: upd_def)
   4.221 -
   4.222 -lemma noError_nth:
   4.223 -  assumes "i < Array.length a h"
   4.224 -  shows "noError (Array.nth a i) h"
   4.225 -  using assms by (simp add: nth_def)
   4.226 -
   4.227 -lemma noError_of_list:
   4.228 -  "noError (of_list ls) h"
   4.229 -  by (simp add: of_list_def)
   4.230 -
   4.231 -lemma noError_map_entry:
   4.232 -  assumes "i < Array.length a h"
   4.233 -  shows "noError (map_entry i f a) h"
   4.234 -  using assms by (simp add: map_entry_def)
   4.235 -
   4.236 -lemma noError_swap:
   4.237 -  assumes "i < Array.length a h"
   4.238 -  shows "noError (swap i x a) h"
   4.239 -  using assms by (simp add: swap_def)
   4.240 -
   4.241 -lemma noError_make:
   4.242 -  "noError (make n f) h"
   4.243 -  by (simp add: make_def)
   4.244 -
   4.245 -lemma noError_freeze:
   4.246 -  "noError (freeze a) h"
   4.247 -  by (simp add: freeze_def)
   4.248 -
   4.249 -lemma noError_fold_map_map_entry:
   4.250 +lemma success_fold_map_map_entry:
   4.251    assumes "n \<le> Array.length a h"
   4.252 -  shows "noError (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
   4.253 +  shows "success (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
   4.254  using assms
   4.255  proof (induct n arbitrary: h)
   4.256    case 0
   4.257 -  thus ?case by (auto intro: noError_return)
   4.258 +  thus ?case by (auto intro: success_returnI)
   4.259  next
   4.260    case (Suc n)
   4.261 -  from Suc.prems have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
   4.262 +  from Suc.prems have "[Array.length a h - Suc n..<Array.length a h] =
   4.263 +    (Array.length a h - Suc n) # [Array.length a h - n..<Array.length a h]"
   4.264      by (simp add: upt_conv_Cons')
   4.265 -  with Suc.hyps[of "(Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h)"] Suc.prems show ?case
   4.266 -    by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
   4.267 +  with Suc.hyps [of "(Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h)"] Suc.prems show ?case apply -
   4.268 +    apply (auto simp add: execute_simps intro!: successI success_returnI success_map_entryI elim: crel_map_entry)
   4.269 +    apply (subst execute_bind) apply (auto simp add: execute_simps)
   4.270 +    done
   4.271  qed
   4.272  
   4.273  
   4.274 -subsection {* Introduction rules for the reference commands *}
   4.275 -
   4.276 -lemma noError_Ref_new:
   4.277 -  shows "noError (ref v) h"
   4.278 -  by (simp add: Ref.ref_def)
   4.279 -
   4.280 -lemma noError_lookup:
   4.281 -  shows "noError (!r) h"
   4.282 -  by (simp add: lookup_def)
   4.283 -
   4.284 -lemma noError_update:
   4.285 -  shows "noError (r := v) h"
   4.286 -  by (simp add: update_def)
   4.287 -
   4.288 -lemma noError_change:
   4.289 -  shows "noError (Ref.change f r) h"
   4.290 -  by (simp add: change_def)
   4.291 -    (auto intro!: noErrorI2 noError_lookup noError_update noError_return crel_lookupI crel_updateI simp add: Let_def)
   4.292 -
   4.293 -subsection {* Introduction rules for the assert command *}
   4.294 -
   4.295 -lemma noError_assert:
   4.296 -  assumes "P x"
   4.297 -  shows "noError (assert P x) h"
   4.298 -  using assms unfolding assert_def
   4.299 -  by (auto intro: noError_if noError_return)
   4.300 -
   4.301  section {* Cumulative lemmas *}
   4.302  
   4.303  lemmas crel_elim_all =
   4.304 @@ -668,10 +527,5 @@
   4.305    (* crel_Ref_newI *) crel_lookupI crel_updateI crel_changeI
   4.306    crel_assert
   4.307  
   4.308 -lemmas noError_intro_all = 
   4.309 -  noErrorI noErrorI' noError_return noError_if noError_option_case
   4.310 -  noError_length noError_new noError_nth noError_upd noError_of_list noError_map_entry noError_swap noError_make noError_freeze
   4.311 -  noError_Ref_new noError_lookup noError_update noError_change
   4.312 -  noError_assert
   4.313  
   4.314  end
   4.315 \ No newline at end of file
     5.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Jul 09 10:08:10 2010 +0200
     5.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Jul 09 16:58:44 2010 +0200
     5.3 @@ -575,23 +575,35 @@
     5.4  text {* We have proved that quicksort sorts (if no exceptions occur).
     5.5  We will now show that exceptions do not occur. *}
     5.6  
     5.7 -lemma noError_part1: 
     5.8 +lemma success_part1I: 
     5.9    assumes "l < Array.length a h" "r < Array.length a h"
    5.10 -  shows "noError (part1 a l r p) h"
    5.11 +  shows "success (part1 a l r p) h"
    5.12    using assms
    5.13  proof (induct a l r p arbitrary: h rule: part1.induct)
    5.14    case (1 a l r p)
    5.15    thus ?case
    5.16      unfolding part1.simps [of a l r] swap_def
    5.17 -    by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return)
    5.18 +    by (auto simp add: execute_simps intro!: success_intros elim!: crelE crel_upd crel_nth crel_return)
    5.19  qed
    5.20  
    5.21 -lemma noError_partition:
    5.22 +lemma success_ifI: (*FIXME move*)
    5.23 +  assumes "c \<Longrightarrow> success t h" "\<not> c \<Longrightarrow> success e h"
    5.24 +  shows "success (if c then t else e) h"
    5.25 +  using assms
    5.26 +  unfolding success_def
    5.27 +  by auto
    5.28 +
    5.29 +lemma success_bindI' [success_intros]: (*FIXME move*)
    5.30 +  assumes "success f h"
    5.31 +  assumes "\<And>h' r. crel f h h' r \<Longrightarrow> success (g r) h'"
    5.32 +  shows "success (f \<guillemotright>= g) h"
    5.33 +  using assms by (auto intro!: successI elim!: successE simp add: bind_def crel_def success_def) blast
    5.34 +
    5.35 +lemma success_partitionI:
    5.36    assumes "l < r" "l < Array.length a h" "r < Array.length a h"
    5.37 -  shows "noError (partition a l r) h"
    5.38 -using assms
    5.39 -unfolding partition.simps swap_def
    5.40 -apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return)
    5.41 +  shows "success (partition a l r) h"
    5.42 +using assms unfolding partition.simps swap_def
    5.43 +apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: crelE crel_upd crel_nth crel_return simp add:)
    5.44  apply (frule part_length_remains)
    5.45  apply (frule part_returns_index_in_bounds)
    5.46  apply auto
    5.47 @@ -602,15 +614,15 @@
    5.48  apply auto
    5.49  done
    5.50  
    5.51 -lemma noError_quicksort:
    5.52 +lemma success_quicksortI:
    5.53    assumes "l < Array.length a h" "r < Array.length a h"
    5.54 -  shows "noError (quicksort a l r) h"
    5.55 +  shows "success (quicksort a l r) h"
    5.56  using assms
    5.57  proof (induct a l r arbitrary: h rule: quicksort.induct)
    5.58    case (1 a l ri h)
    5.59    thus ?case
    5.60      unfolding quicksort.simps [of a l ri]
    5.61 -    apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition)
    5.62 +    apply (auto intro!: success_ifI success_bindI' success_returnI success_nthI success_updI success_assertI success_partitionI)
    5.63      apply (frule partition_returns_index_in_bounds)
    5.64      apply auto
    5.65      apply (frule partition_returns_index_in_bounds)
    5.66 @@ -620,7 +632,7 @@
    5.67      apply (erule disjE)
    5.68      apply auto
    5.69      unfolding quicksort.simps [of a "Suc ri" ri]
    5.70 -    apply (auto intro!: noError_if noError_return)
    5.71 +    apply (auto intro!: success_ifI success_returnI)
    5.72      done
    5.73  qed
    5.74