diff -r 3d2acb18f2f2 -r 1a82e2e29d67 src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Dec 09 21:33:50 2009 +0100 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Dec 10 11:58:26 2009 +0100 @@ -266,6 +266,81 @@ shows "(assert P x >>= f) = (assert P' x >>= f')" using assms by (auto simp add: assert_def return_bind raise_bind) +subsubsection {* A monadic combinator for simple recursive functions *} + +function (default "\(f,g,x,h). (Inr Exn, undefined)") + mrec +where + "mrec f g x h = + (case Heap_Monad.execute (f x) h of + (Inl (Inl r), h') \ (Inl r, h') + | (Inl (Inr s), h') \ + (case mrec f g s h' of + (Inl z, h'') \ Heap_Monad.execute (g x s z) h'' + | (Inr e, h'') \ (Inr e, h'')) + | (Inr e, h') \ (Inr e, h') + )" +by auto + +lemma graph_implies_dom: + "mrec_graph x y \ mrec_dom x" +apply (induct rule:mrec_graph.induct) +apply (rule accpI) +apply (erule mrec_rel.cases) +by simp + +lemma f_default: "\ mrec_dom (f, g, x, h) \ mrec f g x h = (Inr Exn, undefined)" + unfolding mrec_def + by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(f, g, x, h)", simplified]) + +lemma f_di_reverse: + assumes "\ mrec_dom (f, g, x, h)" + shows " + (case Heap_Monad.execute (f x) h of + (Inl (Inl r), h') \ mrecalse + | (Inl (Inr s), h') \ \ mrec_dom (f, g, s, h') + | (Inr e, h') \ mrecalse + )" +using assms +by (auto split:prod.splits sum.splits) + (erule notE, rule accpI, elim mrec_rel.cases, simp)+ + + +lemma mrec_rule: + "mrec f g x h = + (case Heap_Monad.execute (f x) h of + (Inl (Inl r), h') \ (Inl r, h') + | (Inl (Inr s), h') \ + (case mrec f g s h' of + (Inl z, h'') \ Heap_Monad.execute (g x s z) h'' + | (Inr e, h'') \ (Inr e, h'')) + | (Inr e, h') \ (Inr e, h') + )" +apply (cases "mrec_dom (f,g,x,h)", simp) +apply (frule f_default) +apply (frule f_di_reverse, simp) +by (auto split: sum.split prod.split simp: f_default) + + +definition + "MREC f g x = Heap (mrec f g x)" + +lemma MREC_rule: + "MREC f g x = + (do y \ f x; + (case y of + Inl r \ return r + | Inr s \ + do z \ MREC f g s ; + g x s z + done) done)" + unfolding MREC_def + unfolding bindM_def return_def + apply simp + apply (rule ext) + apply (unfold mrec_rule[of f g x]) + by (auto split:prod.splits sum.splits) + hide (open) const heap execute