src/HOL/Imperative_HOL/Heap_Monad.thy

     where y: "execute (f x) h = Some (y, h)" by auto
   moreover from Cons.prems Cons.hyps have "execute (fold_map f xs) h =
     Some (map (\<lambda>x. fst (the (execute (f x) h))) xs, h)" by auto
   ultimately show ?case by (simp, simp only: execute_bind(1), simp)
 qed
-
-
-subsubsection {* A monadic combinator for simple recursive functions *}
-
-text {* Using a locale to fix arguments f and g of MREC *}
-
-locale mrec =
-  fixes f :: "'a \<Rightarrow> ('b + 'a) Heap"
-  and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b Heap"
-begin
-
-function (default "\<lambda>(x, h). None") mrec :: "'a \<Rightarrow> heap \<Rightarrow> ('b \<times> heap) option" where
-  "mrec x h = (case execute (f x) h of
-     Some (Inl r, h') \<Rightarrow> Some (r, h')
-   | Some (Inr s, h') \<Rightarrow> (case mrec s h' of
-             Some (z, h'') \<Rightarrow> execute (g x s z) h''
-           | None \<Rightarrow> None)
-   | None \<Rightarrow> None)"
-by auto
-
-lemma graph_implies_dom:
-  "mrec_graph x y \<Longrightarrow> mrec_dom x"
-apply (induct rule:mrec_graph.induct) 
-apply (rule accpI)
-apply (erule mrec_rel.cases)
-by simp
-
-lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = None"
-  unfolding mrec_def 
-  by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified])
-
-lemma mrec_di_reverse: 
-  assumes "\<not> mrec_dom (x, h)"
-  shows "
-   (case execute (f x) h of
-     Some (Inl r, h') \<Rightarrow> False
-   | Some (Inr s, h') \<Rightarrow> \<not> mrec_dom (s, h')
-   | None \<Rightarrow> False
-   )" 
-using assms apply (auto split: option.split sum.split)
-apply (rule ccontr)
-apply (erule notE, rule accpI, elim mrec_rel.cases, auto)+
-done
-
-lemma mrec_rule:
-  "mrec x h = 
-   (case execute (f x) h of
-     Some (Inl r, h') \<Rightarrow> Some (r, h')
-   | Some (Inr s, h') \<Rightarrow> 
-          (case mrec s h' of
-             Some (z, h'') \<Rightarrow> execute (g x s z) h''
-           | None \<Rightarrow> None)
-   | None \<Rightarrow> None
-   )"
-apply (cases "mrec_dom (x,h)", simp)
-apply (frule mrec_default)
-apply (frule mrec_di_reverse, simp)
-by (auto split: sum.split option.split simp: mrec_default)
-
-definition
-  "MREC x = Heap (mrec x)"
-
-lemma MREC_rule:
-  "MREC x = 
-  (do y \<leftarrow> f x;
-                (case y of 
-                Inl r \<Rightarrow> return r
-              | Inr s \<Rightarrow> 
-                do z \<leftarrow> MREC s ;
-                   g x s z
-                done) done)"
-  unfolding MREC_def
-  unfolding bind_def return_def
-  apply simp
-  apply (rule ext)
-  apply (unfold mrec_rule[of x])
-  by (auto split: option.splits prod.splits sum.splits)
-
-lemma MREC_pinduct:
-  assumes "execute (MREC x) h = Some (r, h')"
-  assumes non_rec_case: "\<And> x h h' r. execute (f x) h = Some (Inl r, h') \<Longrightarrow> P x h h' r"
-  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
-    \<Longrightarrow> execute (g x s z) h2 = Some (r, h') \<Longrightarrow> P x h h' r"
-  shows "P x h h' r"
-proof -
-  from assms(1) have mrec: "mrec x h = Some (r, h')"
-    unfolding MREC_def execute.simps .
-  from mrec have dom: "mrec_dom (x, h)"
-    apply -
-    apply (rule ccontr)
-    apply (drule mrec_default) by auto
-  from mrec have h'_r: "h' = snd (the (mrec x h))" "r = fst (the (mrec x h))"
-    by auto
-  from mrec have "P x h (snd (the (mrec x h))) (fst (the (mrec x h)))"
-  proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom])
-    case (1 x h)
-    obtain rr h' where "the (mrec x h) = (rr, h')" by fastsimp
-    show ?case
-    proof (cases "execute (f x) h")
-      case (Some result)
-      then obtain a h1 where exec_f: "execute (f x) h = Some (a, h1)" by fastsimp
-      note Inl' = this
-      show ?thesis
-      proof (cases a)
-        case (Inl aa)
-        from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis
-          by auto
-      next
-        case (Inr b)
-        note Inr' = this
-        show ?thesis
-        proof (cases "mrec b h1")
-          case (Some result)
-          then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastsimp
-          moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
-            apply (intro 1(2))
-            apply (auto simp add: Inr Inl')
-            done
-          moreover note mrec mrec_rec exec_f Inl' Inr' 1(1) 1(3)
-          ultimately show ?thesis
-            apply auto
-            apply (rule rec_case)
-            apply auto
-            unfolding MREC_def by auto
-        next
-          case None
-          from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by auto
-        qed
-      qed
-    next
-      case None
-      from this 1(1) mrec 1(3) show ?thesis by simp
-    qed
-  qed
-  from this h'_r show ?thesis by simp
-qed
-
-end
-
-text {* Providing global versions of the constant and the theorems *}
-
-abbreviation "MREC == mrec.MREC"
-lemmas MREC_rule = mrec.MREC_rule
-lemmas MREC_pinduct = mrec.MREC_pinduct
-
 
 subsection {* Code generator setup *}
 
 subsubsection {* Logical intermediate layer *}