simplified representation of monad type
authorhaftmann
Mon Jul 05 14:34:28 2010 +0200 (2010-07-05 ago)
changeset 3770970fafefbcc98
parent 37706 c63649d8d75b
child 37710 3f499df0751f
simplified representation of monad type
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/Linked_Lists.thy
src/HOL/Imperative_HOL/ex/SatChecker.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Mon Jul 05 10:42:27 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Mon Jul 05 14:34:28 2010 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4    [code del]: "nth a i = (do len \<leftarrow> length a;
     1.5                   (if i < len
     1.6                       then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h))
     1.7 -                     else raise (''array lookup: index out of range''))
     1.8 +                     else raise ''array lookup: index out of range'')
     1.9                done)"
    1.10  
    1.11  definition
    1.12 @@ -37,18 +37,12 @@
    1.13    [code del]: "upd i x a = (do len \<leftarrow> length a;
    1.14                        (if i < len
    1.15                             then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h))
    1.16 -                           else raise (''array update: index out of range''))
    1.17 +                           else raise ''array update: index out of range'')
    1.18                     done)" 
    1.19  
    1.20  lemma upd_return:
    1.21    "upd i x a \<guillemotright> return a = upd i x a"
    1.22 -proof (rule Heap_eqI)
    1.23 -  fix h
    1.24 -  obtain len h' where "Heap_Monad.execute (Array.length a) h = (len, h')"
    1.25 -    by (cases "Heap_Monad.execute (Array.length a) h")
    1.26 -  then show "Heap_Monad.execute (upd i x a \<guillemotright> return a) h = Heap_Monad.execute (upd i x a) h"
    1.27 -    by (auto simp add: upd_def bindM_def split: sum.split)
    1.28 -qed
    1.29 +  by (rule Heap_eqI) (simp add: upd_def bindM_def split: option.split) 
    1.30  
    1.31  
    1.32  subsection {* Derivates *}
    1.33 @@ -99,14 +93,11 @@
    1.34  
    1.35  lemma array_make [code]:
    1.36    "Array.new n x = make n (\<lambda>_. x)"
    1.37 -  by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def
    1.38 -    monad_simp array_of_list_replicate [symmetric]
    1.39 -    map_replicate_trivial replicate_append_same
    1.40 -    of_list_def)
    1.41 +  by (rule Heap_eqI) (simp add: make_def new_def array_of_list_replicate map_replicate_trivial of_list_def)
    1.42  
    1.43  lemma array_of_list_make [code]:
    1.44    "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
    1.45 -  unfolding make_def map_nth ..
    1.46 +  by (rule Heap_eqI) (simp add: make_def map_nth)
    1.47  
    1.48  
    1.49  subsection {* Code generator setup *}
    1.50 @@ -135,13 +126,11 @@
    1.51    by (simp add: make'_def o_def)
    1.52  
    1.53  definition length' where
    1.54 -  [code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat"
    1.55 +  [code del]: "length' a = Array.length a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))"
    1.56  hide_const (open) length'
    1.57  lemma [code]:
    1.58 -  "Array.length = Array.length' \<guillemotright>== liftM Code_Numeral.nat_of"
    1.59 -  by (simp add: length'_def monad_simp',
    1.60 -    simp add: liftM_def comp_def monad_simp,
    1.61 -    simp add: monad_simp')
    1.62 +  "Array.length a = Array.length' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))"
    1.63 +  by (simp add: length'_def)
    1.64  
    1.65  definition nth' where
    1.66    [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
    1.67 @@ -155,7 +144,7 @@
    1.68  hide_const (open) upd'
    1.69  lemma [code]:
    1.70    "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
    1.71 -  by (simp add: upd'_def monad_simp upd_return)
    1.72 +  by (simp add: upd'_def upd_return)
    1.73  
    1.74  
    1.75  subsubsection {* SML *}
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 05 10:42:27 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 05 14:34:28 2010 +0200
     2.3 @@ -12,16 +12,12 @@
     2.4  
     2.5  subsubsection {* Monad combinators *}
     2.6  
     2.7 -datatype exception = Exn
     2.8 -
     2.9  text {* Monadic heap actions either produce values
    2.10    and transform the heap, or fail *}
    2.11 -datatype 'a Heap = Heap "heap \<Rightarrow> ('a + exception) \<times> heap"
    2.12 +datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
    2.13  
    2.14 -primrec
    2.15 -  execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a + exception) \<times> heap" where
    2.16 -  "execute (Heap f) = f"
    2.17 -lemmas [code del] = execute.simps
    2.18 +primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where
    2.19 +  [code del]: "execute (Heap f) = f"
    2.20  
    2.21  lemma Heap_execute [simp]:
    2.22    "Heap (execute f) = f" by (cases f) simp_all
    2.23 @@ -34,58 +30,67 @@
    2.24    "(\<And>h. (\<lambda>x. execute (f x) h) = (\<lambda>y. execute (g y) h)) \<Longrightarrow> f = g"
    2.25      by (auto simp: expand_fun_eq intro: Heap_eqI)
    2.26  
    2.27 -lemma Heap_strip: "(\<And>f. PROP P f) \<equiv> (\<And>g. PROP P (Heap g))"
    2.28 -proof
    2.29 -  fix g :: "heap \<Rightarrow> ('a + exception) \<times> heap" 
    2.30 -  assume "\<And>f. PROP P f"
    2.31 -  then show "PROP P (Heap g)" .
    2.32 -next
    2.33 -  fix f :: "'a Heap" 
    2.34 -  assume assm: "\<And>g. PROP P (Heap g)"
    2.35 -  then have "PROP P (Heap (execute f))" .
    2.36 -  then show "PROP P f" by simp
    2.37 -qed
    2.38 -
    2.39 -definition
    2.40 -  heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
    2.41 -  [code del]: "heap f = Heap (\<lambda>h. apfst Inl (f h))"
    2.42 +definition heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
    2.43 +  [code del]: "heap f = Heap (Some \<circ> f)"
    2.44  
    2.45  lemma execute_heap [simp]:
    2.46 -  "execute (heap f) h = apfst Inl (f h)"
    2.47 +  "execute (heap f) = Some \<circ> f"
    2.48    by (simp add: heap_def)
    2.49  
    2.50 -definition
    2.51 -  bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
    2.52 -  [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
    2.53 -                  (Inl x, h') \<Rightarrow> execute (g x) h'
    2.54 -                | r \<Rightarrow> r)"
    2.55 -
    2.56 -notation
    2.57 -  bindM (infixl "\<guillemotright>=" 54)
    2.58 +lemma heap_cases [case_names succeed fail]:
    2.59 +  fixes f and h
    2.60 +  assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
    2.61 +  assumes fail: "execute f h = None \<Longrightarrow> P"
    2.62 +  shows P
    2.63 +  using assms by (cases "execute f h") auto
    2.64  
    2.65 -abbreviation
    2.66 -  chainM :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap"  (infixl ">>" 54) where
    2.67 -  "f >> g \<equiv> f >>= (\<lambda>_. g)"
    2.68 -
    2.69 -notation
    2.70 -  chainM (infixl "\<guillemotright>" 54)
    2.71 -
    2.72 -definition
    2.73 -  return :: "'a \<Rightarrow> 'a Heap" where
    2.74 +definition return :: "'a \<Rightarrow> 'a Heap" where
    2.75    [code del]: "return x = heap (Pair x)"
    2.76  
    2.77  lemma execute_return [simp]:
    2.78 -  "execute (return x) h = apfst Inl (x, h)"
    2.79 +  "execute (return x) = Some \<circ> Pair x"
    2.80    by (simp add: return_def)
    2.81  
    2.82 -definition
    2.83 -  raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
    2.84 -  [code del]: "raise s = Heap (Pair (Inr Exn))"
    2.85 +definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
    2.86 +  [code del]: "raise s = Heap (\<lambda>_. None)"
    2.87  
    2.88  lemma execute_raise [simp]:
    2.89 -  "execute (raise s) h = (Inr Exn, h)"
    2.90 +  "execute (raise s) = (\<lambda>_. None)"
    2.91    by (simp add: raise_def)
    2.92  
    2.93 +definition bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
    2.94 +  [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
    2.95 +                  Some (x, h') \<Rightarrow> execute (g x) h'
    2.96 +                | None \<Rightarrow> None)"
    2.97 +
    2.98 +notation bindM (infixl "\<guillemotright>=" 54)
    2.99 +
   2.100 +lemma execute_bind [simp]:
   2.101 +  "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
   2.102 +  "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
   2.103 +  by (simp_all add: bindM_def)
   2.104 +
   2.105 +lemma execute_bind_heap [simp]:
   2.106 +  "execute (heap f \<guillemotright>= g) h = execute (g (fst (f h))) (snd (f h))"
   2.107 +  by (simp add: bindM_def split_def)
   2.108 +  
   2.109 +lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
   2.110 +  by (rule Heap_eqI) simp
   2.111 +
   2.112 +lemma bind_return [simp]: "f \<guillemotright>= return = f"
   2.113 +  by (rule Heap_eqI) (simp add: bindM_def split: option.splits)
   2.114 +
   2.115 +lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
   2.116 +  by (rule Heap_eqI) (simp add: bindM_def split: option.splits)
   2.117 +
   2.118 +lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
   2.119 +  by (rule Heap_eqI) simp
   2.120 +
   2.121 +abbreviation chainM :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap"  (infixl ">>" 54) where
   2.122 +  "f >> g \<equiv> f >>= (\<lambda>_. g)"
   2.123 +
   2.124 +notation chainM (infixl "\<guillemotright>" 54)
   2.125 +
   2.126  
   2.127  subsubsection {* do-syntax *}
   2.128  
   2.129 @@ -170,88 +175,10 @@
   2.130  
   2.131  subsection {* Monad properties *}
   2.132  
   2.133 -subsubsection {* Monad laws *}
   2.134 -
   2.135 -lemma return_bind: "return x \<guillemotright>= f = f x"
   2.136 -  by (simp add: bindM_def return_def)
   2.137 -
   2.138 -lemma bind_return: "f \<guillemotright>= return = f"
   2.139 -proof (rule Heap_eqI)
   2.140 -  fix h
   2.141 -  show "execute (f \<guillemotright>= return) h = execute f h"
   2.142 -    by (auto simp add: bindM_def return_def split: sum.splits prod.splits)
   2.143 -qed
   2.144 -
   2.145 -lemma bind_bind: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
   2.146 -  by (rule Heap_eqI) (auto simp add: bindM_def split: split: sum.splits prod.splits)
   2.147 -
   2.148 -lemma bind_bind': "f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h x) = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= (\<lambda>y. return (x, y))) \<guillemotright>= (\<lambda>(x, y). h x y)"
   2.149 -  by (rule Heap_eqI) (auto simp add: bindM_def split: split: sum.splits prod.splits)
   2.150 -
   2.151 -lemma raise_bind: "raise e \<guillemotright>= f = raise e"
   2.152 -  by (simp add: raise_def bindM_def)
   2.153 -
   2.154 -
   2.155 -lemmas monad_simp = return_bind bind_return bind_bind raise_bind
   2.156 -
   2.157 -
   2.158  subsection {* Generic combinators *}
   2.159  
   2.160 -definition
   2.161 -  liftM :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap"
   2.162 -where
   2.163 -  "liftM f = return o f"
   2.164 -
   2.165 -definition
   2.166 -  compM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> ('b \<Rightarrow> 'c Heap) \<Rightarrow> 'a \<Rightarrow> 'c Heap" (infixl ">>==" 54)
   2.167 -where
   2.168 -  "(f >>== g) = (\<lambda>x. f x \<guillemotright>= g)"
   2.169 -
   2.170 -notation
   2.171 -  compM (infixl "\<guillemotright>==" 54)
   2.172 -
   2.173 -lemma liftM_collapse: "liftM f x = return (f x)"
   2.174 -  by (simp add: liftM_def)
   2.175 -
   2.176 -lemma liftM_compM: "liftM f \<guillemotright>== g = g o f"
   2.177 -  by (auto intro: Heap_eqI' simp add: expand_fun_eq liftM_def compM_def bindM_def)
   2.178 -
   2.179 -lemma compM_return: "f \<guillemotright>== return = f"
   2.180 -  by (simp add: compM_def monad_simp)
   2.181 -
   2.182 -lemma compM_compM: "(f \<guillemotright>== g) \<guillemotright>== h = f \<guillemotright>== (g \<guillemotright>== h)"
   2.183 -  by (simp add: compM_def monad_simp)
   2.184 -
   2.185 -lemma liftM_bind:
   2.186 -  "(\<lambda>x. liftM f x \<guillemotright>= liftM g) = liftM (\<lambda>x. g (f x))"
   2.187 -  by (rule Heap_eqI') (simp add: monad_simp liftM_def bindM_def)
   2.188 -
   2.189 -lemma liftM_comp:
   2.190 -  "liftM f o g = liftM (f o g)"
   2.191 -  by (rule Heap_eqI') (simp add: liftM_def)
   2.192 -
   2.193 -lemmas monad_simp' = monad_simp liftM_compM compM_return
   2.194 -  compM_compM liftM_bind liftM_comp
   2.195 -
   2.196 -primrec 
   2.197 -  mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap"
   2.198 -where
   2.199 -  "mapM f [] = return []"
   2.200 -  | "mapM f (x#xs) = do y \<leftarrow> f x;
   2.201 -                        ys \<leftarrow> mapM f xs;
   2.202 -                        return (y # ys)
   2.203 -                     done"
   2.204 -
   2.205 -primrec
   2.206 -  foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap"
   2.207 -where
   2.208 -  "foldM f [] s = return s"
   2.209 -  | "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs"
   2.210 -
   2.211 -definition
   2.212 -  assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap"
   2.213 -where
   2.214 -  "assert P x = (if P x then return x else raise (''assert''))"
   2.215 +definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where
   2.216 +  "assert P x = (if P x then return x else raise ''assert'')"
   2.217  
   2.218  lemma assert_cong [fundef_cong]:
   2.219    assumes "P = P'"
   2.220 @@ -259,28 +186,42 @@
   2.221    shows "(assert P x >>= f) = (assert P' x >>= f')"
   2.222    using assms by (auto simp add: assert_def return_bind raise_bind)
   2.223  
   2.224 +definition liftM :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where
   2.225 +  "liftM f = return o f"
   2.226 +
   2.227 +lemma liftM_collapse [simp]:
   2.228 +  "liftM f x = return (f x)"
   2.229 +  by (simp add: liftM_def)
   2.230 +
   2.231 +lemma bind_liftM:
   2.232 +  "(f \<guillemotright>= liftM g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
   2.233 +  by (simp add: liftM_def comp_def)
   2.234 +
   2.235 +primrec mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
   2.236 +  "mapM f [] = return []"
   2.237 +| "mapM f (x#xs) = do
   2.238 +     y \<leftarrow> f x;
   2.239 +     ys \<leftarrow> mapM f xs;
   2.240 +     return (y # ys)
   2.241 +   done"
   2.242 +
   2.243 +
   2.244  subsubsection {* A monadic combinator for simple recursive functions *}
   2.245  
   2.246  text {* Using a locale to fix arguments f and g of MREC *}
   2.247  
   2.248  locale mrec =
   2.249 -fixes
   2.250 -  f :: "'a => ('b + 'a) Heap"
   2.251 -  and g :: "'a => 'a => 'b => 'b Heap"
   2.252 +  fixes f :: "'a \<Rightarrow> ('b + 'a) Heap"
   2.253 +  and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b Heap"
   2.254  begin
   2.255  
   2.256 -function (default "\<lambda>(x,h). (Inr Exn, undefined)") 
   2.257 -  mrec 
   2.258 -where
   2.259 -  "mrec x h = 
   2.260 -   (case Heap_Monad.execute (f x) h of
   2.261 -     (Inl (Inl r), h') \<Rightarrow> (Inl r, h')
   2.262 -   | (Inl (Inr s), h') \<Rightarrow> 
   2.263 -          (case mrec s h' of
   2.264 -             (Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
   2.265 -           | (Inr e, h'') \<Rightarrow> (Inr e, h''))
   2.266 -   | (Inr e, h') \<Rightarrow> (Inr e, h')
   2.267 -   )"
   2.268 +function (default "\<lambda>(x, h). None") mrec :: "'a \<Rightarrow> heap \<Rightarrow> ('b \<times> heap) option" where
   2.269 +  "mrec x h = (case execute (f x) h of
   2.270 +     Some (Inl r, h') \<Rightarrow> Some (r, h')
   2.271 +   | Some (Inr s, h') \<Rightarrow> (case mrec s h' of
   2.272 +             Some (z, h'') \<Rightarrow> execute (g x s z) h''
   2.273 +           | None \<Rightarrow> None)
   2.274 +   | None \<Rightarrow> None)"
   2.275  by auto
   2.276  
   2.277  lemma graph_implies_dom:
   2.278 @@ -290,38 +231,37 @@
   2.279  apply (erule mrec_rel.cases)
   2.280  by simp
   2.281  
   2.282 -lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = (Inr Exn, undefined)"
   2.283 +lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = None"
   2.284    unfolding mrec_def 
   2.285    by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified])
   2.286  
   2.287  lemma mrec_di_reverse: 
   2.288    assumes "\<not> mrec_dom (x, h)"
   2.289    shows "
   2.290 -   (case Heap_Monad.execute (f x) h of
   2.291 -     (Inl (Inl r), h') \<Rightarrow> False
   2.292 -   | (Inl (Inr s), h') \<Rightarrow> \<not> mrec_dom (s, h')
   2.293 -   | (Inr e, h') \<Rightarrow> False
   2.294 +   (case execute (f x) h of
   2.295 +     Some (Inl r, h') \<Rightarrow> False
   2.296 +   | Some (Inr s, h') \<Rightarrow> \<not> mrec_dom (s, h')
   2.297 +   | None \<Rightarrow> False
   2.298     )" 
   2.299 -using assms
   2.300 -by (auto split:prod.splits sum.splits)
   2.301 - (erule notE, rule accpI, elim mrec_rel.cases, simp)+
   2.302 -
   2.303 +using assms apply (auto split: option.split sum.split)
   2.304 +apply (rule ccontr)
   2.305 +apply (erule notE, rule accpI, elim mrec_rel.cases, auto)+
   2.306 +done
   2.307  
   2.308  lemma mrec_rule:
   2.309    "mrec x h = 
   2.310 -   (case Heap_Monad.execute (f x) h of
   2.311 -     (Inl (Inl r), h') \<Rightarrow> (Inl r, h')
   2.312 -   | (Inl (Inr s), h') \<Rightarrow> 
   2.313 +   (case execute (f x) h of
   2.314 +     Some (Inl r, h') \<Rightarrow> Some (r, h')
   2.315 +   | Some (Inr s, h') \<Rightarrow> 
   2.316            (case mrec s h' of
   2.317 -             (Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
   2.318 -           | (Inr e, h'') \<Rightarrow> (Inr e, h''))
   2.319 -   | (Inr e, h') \<Rightarrow> (Inr e, h')
   2.320 +             Some (z, h'') \<Rightarrow> execute (g x s z) h''
   2.321 +           | None \<Rightarrow> None)
   2.322 +   | None \<Rightarrow> None
   2.323     )"
   2.324  apply (cases "mrec_dom (x,h)", simp)
   2.325  apply (frule mrec_default)
   2.326  apply (frule mrec_di_reverse, simp)
   2.327 -by (auto split: sum.split prod.split simp: mrec_default)
   2.328 -
   2.329 +by (auto split: sum.split option.split simp: mrec_default)
   2.330  
   2.331  definition
   2.332    "MREC x = Heap (mrec x)"
   2.333 @@ -340,32 +280,31 @@
   2.334    apply simp
   2.335    apply (rule ext)
   2.336    apply (unfold mrec_rule[of x])
   2.337 -  by (auto split:prod.splits sum.splits)
   2.338 -
   2.339 +  by (auto split: option.splits prod.splits sum.splits)
   2.340  
   2.341  lemma MREC_pinduct:
   2.342 -  assumes "Heap_Monad.execute (MREC x) h = (Inl r, h')"
   2.343 -  assumes non_rec_case: "\<And> x h h' r. Heap_Monad.execute (f x) h = (Inl (Inl r), h') \<Longrightarrow> P x h h' r"
   2.344 -  assumes rec_case: "\<And> x h h1 h2 h' s z r. Heap_Monad.execute (f x) h = (Inl (Inr s), h1) \<Longrightarrow> Heap_Monad.execute (MREC s) h1 = (Inl z, h2) \<Longrightarrow> P s h1 h2 z
   2.345 -    \<Longrightarrow> Heap_Monad.execute (g x s z) h2 = (Inl r, h') \<Longrightarrow> P x h h' r"
   2.346 +  assumes "execute (MREC x) h = Some (r, h')"
   2.347 +  assumes non_rec_case: "\<And> x h h' r. execute (f x) h = Some (Inl r, h') \<Longrightarrow> P x h h' r"
   2.348 +  assumes rec_case: "\<And> x h h1 h2 h' s z r. execute (f x) h = Some (Inr s, h1) \<Longrightarrow> execute (MREC s) h1 = Some (z, h2) \<Longrightarrow> P s h1 h2 z
   2.349 +    \<Longrightarrow> execute (g x s z) h2 = Some (r, h') \<Longrightarrow> P x h h' r"
   2.350    shows "P x h h' r"
   2.351  proof -
   2.352 -  from assms(1) have mrec: "mrec x h = (Inl r, h')"
   2.353 +  from assms(1) have mrec: "mrec x h = Some (r, h')"
   2.354      unfolding MREC_def execute.simps .
   2.355    from mrec have dom: "mrec_dom (x, h)"
   2.356      apply -
   2.357      apply (rule ccontr)
   2.358      apply (drule mrec_default) by auto
   2.359 -  from mrec have h'_r: "h' = (snd (mrec x h))" "r = (Sum_Type.Projl (fst (mrec x h)))"
   2.360 +  from mrec have h'_r: "h' = snd (the (mrec x h))" "r = fst (the (mrec x h))"
   2.361      by auto
   2.362 -  from mrec have "P x h (snd (mrec x h)) (Sum_Type.Projl (fst (mrec x h)))"
   2.363 +  from mrec have "P x h (snd (the (mrec x h))) (fst (the (mrec x h)))"
   2.364    proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom])
   2.365      case (1 x h)
   2.366 -    obtain rr h' where "mrec x h = (rr, h')" by fastsimp
   2.367 -    obtain fret h1 where exec_f: "Heap_Monad.execute (f x) h = (fret, h1)" by fastsimp
   2.368 +    obtain rr h' where "the (mrec x h) = (rr, h')" by fastsimp
   2.369      show ?case
   2.370 -    proof (cases fret)
   2.371 -      case (Inl a)
   2.372 +    proof (cases "execute (f x) h")
   2.373 +      case (Some result)
   2.374 +      then obtain a h1 where exec_f: "execute (f x) h = Some (a, h1)" by fastsimp
   2.375        note Inl' = this
   2.376        show ?thesis
   2.377        proof (cases a)
   2.378 @@ -375,23 +314,28 @@
   2.379        next
   2.380          case (Inr b)
   2.381          note Inr' = this
   2.382 -        obtain ret_mrec h2 where mrec_rec: "mrec b h1 = (ret_mrec, h2)" by fastsimp
   2.383 -        from this Inl 1(1) exec_f mrec show ?thesis
   2.384 -        proof (cases "ret_mrec")
   2.385 -          case (Inl aaa)
   2.386 -          from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2) [OF exec_f [symmetric] Inl' Inr', of "aaa" "h2"] 1(3)
   2.387 -            show ?thesis
   2.388 -              apply auto
   2.389 -              apply (rule rec_case)
   2.390 -              unfolding MREC_def by auto
   2.391 +        show ?thesis
   2.392 +        proof (cases "mrec b h1")
   2.393 +          case (Some result)
   2.394 +          then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastsimp
   2.395 +          moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
   2.396 +            apply (intro 1(2))
   2.397 +            apply (auto simp add: Inr Inl')
   2.398 +            done
   2.399 +          moreover note mrec mrec_rec exec_f Inl' Inr' 1(1) 1(3)
   2.400 +          ultimately show ?thesis
   2.401 +            apply auto
   2.402 +            apply (rule rec_case)
   2.403 +            apply auto
   2.404 +            unfolding MREC_def by auto
   2.405          next
   2.406 -          case (Inr b)
   2.407 -          from this Inl 1(1) exec_f mrec Inr' mrec_rec 1(3) show ?thesis by auto
   2.408 +          case None
   2.409 +          from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by auto
   2.410          qed
   2.411        qed
   2.412      next
   2.413 -      case (Inr b)
   2.414 -      from this 1(1) mrec exec_f 1(3) show ?thesis by simp
   2.415 +      case None
   2.416 +      from this 1(1) mrec 1(3) show ?thesis by simp
   2.417      qed
   2.418    qed
   2.419    from this h'_r show ?thesis by simp
   2.420 @@ -412,38 +356,29 @@
   2.421  
   2.422  subsubsection {* Logical intermediate layer *}
   2.423  
   2.424 -definition
   2.425 -  Fail :: "String.literal \<Rightarrow> exception"
   2.426 -where
   2.427 -  [code del]: "Fail s = Exn"
   2.428 +primrec raise' :: "String.literal \<Rightarrow> 'a Heap" where
   2.429 +  [code del, code_post]: "raise' (STR s) = raise s"
   2.430  
   2.431 -definition
   2.432 -  raise_exc :: "exception \<Rightarrow> 'a Heap"
   2.433 -where
   2.434 -  [code del]: "raise_exc e = raise []"
   2.435 +lemma raise_raise' [code_inline]:
   2.436 +  "raise s = raise' (STR s)"
   2.437 +  by simp
   2.438  
   2.439 -lemma raise_raise_exc [code, code_unfold]:
   2.440 -  "raise s = raise_exc (Fail (STR s))"
   2.441 -  unfolding Fail_def raise_exc_def raise_def ..
   2.442 +code_datatype raise' -- {* avoid @{const "Heap"} formally *}
   2.443  
   2.444 -hide_const (open) Fail raise_exc
   2.445 +hide_const (open) raise'
   2.446  
   2.447  
   2.448  subsubsection {* SML and OCaml *}
   2.449  
   2.450  code_type Heap (SML "unit/ ->/ _")
   2.451 -code_const Heap (SML "raise/ (Fail/ \"bare Heap\")")
   2.452  code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
   2.453  code_const return (SML "!(fn/ ()/ =>/ _)")
   2.454 -code_const "Heap_Monad.Fail" (SML "Fail")
   2.455 -code_const "Heap_Monad.raise_exc" (SML "!(fn/ ()/ =>/ raise/ _)")
   2.456 +code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)")
   2.457  
   2.458  code_type Heap (OCaml "_")
   2.459 -code_const Heap (OCaml "failwith/ \"bare Heap\"")
   2.460  code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
   2.461  code_const return (OCaml "!(fun/ ()/ ->/ _)")
   2.462 -code_const "Heap_Monad.Fail" (OCaml "Failure")
   2.463 -code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)")
   2.464 +code_const Heap_Monad.raise' (OCaml "failwith/ _")
   2.465  
   2.466  setup {*
   2.467  
   2.468 @@ -514,8 +449,6 @@
   2.469  
   2.470  *}
   2.471  
   2.472 -code_reserved OCaml Failure raise
   2.473 -
   2.474  
   2.475  subsubsection {* Haskell *}
   2.476  
   2.477 @@ -556,10 +489,8 @@
   2.478  text {* Monad *}
   2.479  
   2.480  code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
   2.481 -code_const Heap (Haskell "error/ \"bare Heap\"")
   2.482  code_monad "op \<guillemotright>=" Haskell
   2.483  code_const return (Haskell "return")
   2.484 -code_const "Heap_Monad.Fail" (Haskell "_")
   2.485 -code_const "Heap_Monad.raise_exc" (Haskell "error")
   2.486 +code_const Heap_Monad.raise' (Haskell "error/ _")
   2.487  
   2.488  end
     3.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Mon Jul 05 10:42:27 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Mon Jul 05 14:34:28 2010 +0200
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      HOL/Library/Ref.thy
     3.5 -    ID:         $Id$
     3.6      Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
     3.7  *)
     3.8  
     3.9 @@ -53,7 +52,7 @@
    3.10  
    3.11  lemma update_change [code]:
    3.12    "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()"
    3.13 -  by (auto simp add: monad_simp change_def lookup_chain)
    3.14 +  by (auto simp add: change_def lookup_chain)
    3.15  
    3.16  
    3.17  subsection {* Code generator setup *}
     4.1 --- a/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 05 10:42:27 2010 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 05 14:34:28 2010 +0200
     4.3 @@ -9,10 +9,10 @@
     4.4  
     4.5  definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool"
     4.6  where
     4.7 -  crel_def': "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = (Inl r, h')"
     4.8 +  crel_def': "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')"
     4.9  
    4.10  lemma crel_def: -- FIXME
    4.11 -  "crel c h h' r \<longleftrightarrow> (Inl r, h') = Heap_Monad.execute c h"
    4.12 +  "crel c h h' r \<longleftrightarrow> Some (r, h') = Heap_Monad.execute c h"
    4.13    unfolding crel_def' by auto
    4.14  
    4.15  lemma crel_deterministic: "\<lbrakk> crel f h h' a; crel f h h'' b \<rbrakk> \<Longrightarrow> (a = b) \<and> (h' = h'')"
    4.16 @@ -28,8 +28,7 @@
    4.17  lemma crelE[consumes 1]:
    4.18    assumes "crel (f >>= g) h h'' r'"
    4.19    obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
    4.20 -  using assms
    4.21 -  by (auto simp add: crel_def bindM_def Let_def prod_case_beta split_def Pair_fst_snd_eq split add: sum.split_asm)
    4.22 +  using assms by (auto simp add: crel_def bindM_def split: option.split_asm)
    4.23  
    4.24  lemma crelE'[consumes 1]:
    4.25    assumes "crel (f >> g) h h'' r'"
    4.26 @@ -86,8 +85,8 @@
    4.27  lemma crel_heap:
    4.28    assumes "crel (Heap_Monad.heap f) h h' r"
    4.29    obtains "h' = snd (f h)" "r = fst (f h)"
    4.30 -  using assms
    4.31 -  unfolding heap_def crel_def apfst_def split_def prod_fun_def by simp_all
    4.32 +  using assms by (cases "f h") (simp add: crel_def)
    4.33 +
    4.34  
    4.35  subsection {* Elimination rules for array commands *}
    4.36  
    4.37 @@ -369,11 +368,9 @@
    4.38  apply (cases f)
    4.39  apply simp
    4.40  apply (simp add: expand_fun_eq split_def)
    4.41 +apply (auto split: option.split)
    4.42 +apply (erule_tac x="x" in meta_allE)
    4.43  apply auto
    4.44 -apply (case_tac "fst (fun x)")
    4.45 -apply (simp_all add: Pair_fst_snd_eq)
    4.46 -apply (erule_tac x="x" in meta_allE)
    4.47 -apply fastsimp
    4.48  done
    4.49  
    4.50  section {* Introduction rules *}
    4.51 @@ -502,10 +499,10 @@
    4.52    shows "P x h h' r"
    4.53  proof (rule MREC_pinduct[OF assms(1)[unfolded crel_def, symmetric]])
    4.54    fix x h h1 h2 h' s z r
    4.55 -  assume "Heap_Monad.execute (f x) h = (Inl (Inr s), h1)"
    4.56 -    "Heap_Monad.execute (MREC f g s) h1 = (Inl z, h2)"
    4.57 +  assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)"
    4.58 +    "Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)"
    4.59      "P s h1 h2 z"
    4.60 -    "Heap_Monad.execute (g x s z) h2 = (Inl r, h')"
    4.61 +    "Heap_Monad.execute (g x s z) h2 = Some (r, h')"
    4.62    from assms(3)[unfolded crel_def, OF this(1)[symmetric] this(2)[symmetric] this(3) this(4)[symmetric]]
    4.63    show "P x h h' r" .
    4.64  next
    4.65 @@ -519,15 +516,15 @@
    4.66  
    4.67  definition noError :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool"
    4.68  where
    4.69 -  "noError c h \<longleftrightarrow> (\<exists>r h'. (Inl r, h') = Heap_Monad.execute c h)"
    4.70 +  "noError c h \<longleftrightarrow> (\<exists>r h'. Some (r, h') = Heap_Monad.execute c h)"
    4.71  
    4.72  lemma noError_def': -- FIXME
    4.73 -  "noError c h \<longleftrightarrow> (\<exists>r h'. Heap_Monad.execute c h = (Inl r, h'))"
    4.74 +  "noError c h \<longleftrightarrow> (\<exists>r h'. Heap_Monad.execute c h = Some (r, h'))"
    4.75    unfolding noError_def apply auto proof -
    4.76    fix r h'
    4.77 -  assume "(Inl r, h') = Heap_Monad.execute c h"
    4.78 -  then have "Heap_Monad.execute c h = (Inl r, h')" ..
    4.79 -  then show "\<exists>r h'. Heap_Monad.execute c h = (Inl r, h')" by blast
    4.80 +  assume "Some (r, h') = Heap_Monad.execute c h"
    4.81 +  then have "Heap_Monad.execute c h = Some (r, h')" ..
    4.82 +  then show "\<exists>r h'. Heap_Monad.execute c h = Some (r, h')" by blast
    4.83  qed
    4.84  
    4.85  subsection {* Introduction rules for basic monadic commands *}
    4.86 @@ -640,7 +637,7 @@
    4.87  (*TODO: move to HeapMonad *)
    4.88  lemma mapM_append:
    4.89    "mapM f (xs @ ys) = mapM f xs \<guillemotright>= (\<lambda>xs. mapM f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
    4.90 -  by (induct xs) (simp_all add: monad_simp)
    4.91 +  by (induct xs) simp_all
    4.92  
    4.93  lemma noError_freeze:
    4.94    shows "noError (freeze a) h"
     5.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Jul 05 10:42:27 2010 +0200
     5.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Jul 05 14:34:28 2010 +0200
     5.3 @@ -56,7 +56,7 @@
     5.4                              return (x#xs)
     5.5                           done"
     5.6  unfolding traverse_def
     5.7 -by (auto simp: traverse_def monad_simp MREC_rule)
     5.8 +by (auto simp: traverse_def MREC_rule)
     5.9  
    5.10  
    5.11  section {* Proving correctness with relational abstraction *}
    5.12 @@ -531,7 +531,7 @@
    5.13    done"
    5.14    unfolding rev'_def MREC_rule[of _ _ "(q, p)"] unfolding rev'_def[symmetric]
    5.15  thm arg_cong2
    5.16 -  by (auto simp add: monad_simp expand_fun_eq intro: arg_cong2[where f = "op \<guillemotright>="] split: node.split)
    5.17 +  by (auto simp add: expand_fun_eq intro: arg_cong2[where f = "op \<guillemotright>="] split: node.split)
    5.18  
    5.19  fun rev :: "('a:: heap) node \<Rightarrow> 'a node Heap" 
    5.20  where
     6.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Jul 05 10:42:27 2010 +0200
     6.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Jul 05 14:34:28 2010 +0200
     6.3 @@ -402,6 +402,12 @@
     6.4           res_thm' l cli clj
     6.5        done))"
     6.6  
     6.7 +primrec
     6.8 +  foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap"
     6.9 +where
    6.10 +  "foldM f [] s = return s"
    6.11 +  | "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs"
    6.12 +
    6.13  fun doProofStep2 :: "Clause option array \<Rightarrow> ProofStep \<Rightarrow> Clause list \<Rightarrow> Clause list Heap"
    6.14  where
    6.15    "doProofStep2 a (Conflict saveTo (i, rs)) rcs =