changeset 34051 1a82e2e29d67 parent 32069 6d28bbd33e2c child 35113 1a0c129bb2e0
```     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Dec 09 21:33:50 2009 +0100
1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Dec 10 11:58:26 2009 +0100
1.3 @@ -266,6 +266,81 @@
1.4    shows "(assert P x >>= f) = (assert P' x >>= f')"
1.5    using assms by (auto simp add: assert_def return_bind raise_bind)
1.6
1.7 +subsubsection {* A monadic combinator for simple recursive functions *}
1.8 +
1.9 +function (default "\<lambda>(f,g,x,h). (Inr Exn, undefined)")
1.10 +  mrec
1.11 +where
1.12 +  "mrec f g x h =
1.13 +   (case Heap_Monad.execute (f x) h of
1.14 +     (Inl (Inl r), h') \<Rightarrow> (Inl r, h')
1.15 +   | (Inl (Inr s), h') \<Rightarrow>
1.16 +          (case mrec f g s h' of
1.17 +             (Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
1.18 +           | (Inr e, h'') \<Rightarrow> (Inr e, h''))
1.19 +   | (Inr e, h') \<Rightarrow> (Inr e, h')
1.20 +   )"
1.21 +by auto
1.22 +
1.23 +lemma graph_implies_dom:
1.24 +	"mrec_graph x y \<Longrightarrow> mrec_dom x"
1.25 +apply (induct rule:mrec_graph.induct)
1.26 +apply (rule accpI)
1.27 +apply (erule mrec_rel.cases)
1.28 +by simp
1.29 +
1.30 +lemma f_default: "\<not> mrec_dom (f, g, x, h) \<Longrightarrow> mrec f g x h = (Inr Exn, undefined)"
1.31 +	unfolding mrec_def
1.32 +  by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(f, g, x, h)", simplified])
1.33 +
1.34 +lemma f_di_reverse:
1.35 +  assumes "\<not> mrec_dom (f, g, x, h)"
1.36 +  shows "
1.37 +   (case Heap_Monad.execute (f x) h of
1.38 +     (Inl (Inl r), h') \<Rightarrow> mrecalse
1.39 +   | (Inl (Inr s), h') \<Rightarrow> \<not> mrec_dom (f, g, s, h')
1.40 +   | (Inr e, h') \<Rightarrow> mrecalse
1.41 +   )"
1.42 +using assms
1.43 +by (auto split:prod.splits sum.splits)
1.44 + (erule notE, rule accpI, elim mrec_rel.cases, simp)+
1.45 +
1.46 +
1.47 +lemma mrec_rule:
1.48 +  "mrec f g x h =
1.49 +   (case Heap_Monad.execute (f x) h of
1.50 +     (Inl (Inl r), h') \<Rightarrow> (Inl r, h')
1.51 +   | (Inl (Inr s), h') \<Rightarrow>
1.52 +          (case mrec f g s h' of
1.53 +             (Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
1.54 +           | (Inr e, h'') \<Rightarrow> (Inr e, h''))
1.55 +   | (Inr e, h') \<Rightarrow> (Inr e, h')
1.56 +   )"
1.57 +apply (cases "mrec_dom (f,g,x,h)", simp)
1.58 +apply (frule f_default)
1.59 +apply (frule f_di_reverse, simp)
1.60 +by (auto split: sum.split prod.split simp: f_default)
1.61 +
1.62 +
1.63 +definition
1.64 +  "MREC f g x = Heap (mrec f g x)"
1.65 +
1.66 +lemma MREC_rule:
1.67 +  "MREC f g x =
1.68 +  (do y \<leftarrow> f x;
1.69 +                (case y of
1.70 +                Inl r \<Rightarrow> return r
1.71 +              | Inr s \<Rightarrow>
1.72 +                do z \<leftarrow> MREC f g s ;
1.73 +                   g x s z
1.74 +                done) done)"
1.75 +  unfolding MREC_def
1.76 +  unfolding bindM_def return_def
1.77 +  apply simp
1.78 +  apply (rule ext)
1.79 +  apply (unfold mrec_rule[of f g x])
1.80 +  by (auto split:prod.splits sum.splits)
1.81 +
1.82  hide (open) const heap execute
1.83
1.84
```