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