src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 36057 ca6610908ae9
parent 35423 6ef9525a5727
child 36078 59f6773a7d1d
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Mar 31 16:44:41 2010 +0200
@@ -270,15 +270,23 @@
   using assms by (auto simp add: assert_def return_bind raise_bind)
 
 subsubsection {* A monadic combinator for simple recursive functions *}
- 
-function (default "\<lambda>(f,g,x,h). (Inr Exn, undefined)") 
+
+text {* Using a locale to fix arguments f and g of MREC *}
+
+locale mrec =
+fixes
+  f :: "'a => ('b + 'a) Heap"
+  and g :: "'a => 'a => 'b => 'b Heap"
+begin
+
+function (default "\<lambda>(x,h). (Inr Exn, undefined)") 
   mrec 
 where
-  "mrec f g x h = 
+  "mrec x h = 
    (case Heap_Monad.execute (f x) h of
      (Inl (Inl r), h') \<Rightarrow> (Inl r, h')
    | (Inl (Inr s), h') \<Rightarrow> 
-          (case mrec f g s h' of
+          (case mrec s h' of
              (Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
            | (Inr e, h'') \<Rightarrow> (Inr e, h''))
    | (Inr e, h') \<Rightarrow> (Inr e, h')
@@ -292,17 +300,17 @@
 apply (erule mrec_rel.cases)
 by simp
 
-lemma f_default: "\<not> mrec_dom (f, g, x, h) \<Longrightarrow> mrec f g x h = (Inr Exn, undefined)"
+lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec 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])
+  by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified])
 
-lemma f_di_reverse: 
-  assumes "\<not> mrec_dom (f, g, x, h)"
+lemma mrec_di_reverse: 
+  assumes "\<not> mrec_dom (x, h)"
   shows "
    (case Heap_Monad.execute (f x) h of
-     (Inl (Inl r), h') \<Rightarrow> mrecalse
-   | (Inl (Inr s), h') \<Rightarrow> \<not> mrec_dom (f, g, s, h')
-   | (Inr e, h') \<Rightarrow> mrecalse
+     (Inl (Inl r), h') \<Rightarrow> False
+   | (Inl (Inr s), h') \<Rightarrow> \<not> mrec_dom (s, h')
+   | (Inr e, h') \<Rightarrow> False
    )" 
 using assms
 by (auto split:prod.splits sum.splits)
@@ -310,40 +318,103 @@
 
 
 lemma mrec_rule:
-  "mrec f g x h = 
+  "mrec x h = 
    (case Heap_Monad.execute (f x) h of
      (Inl (Inl r), h') \<Rightarrow> (Inl r, h')
    | (Inl (Inr s), h') \<Rightarrow> 
-          (case mrec f g s h' of
+          (case mrec s h' of
              (Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
            | (Inr e, h'') \<Rightarrow> (Inr e, h''))
    | (Inr e, h') \<Rightarrow> (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)
+apply (cases "mrec_dom (x,h)", simp)
+apply (frule mrec_default)
+apply (frule mrec_di_reverse, simp)
+by (auto split: sum.split prod.split simp: mrec_default)
 
 
 definition
-  "MREC f g x = Heap (mrec f g x)"
+  "MREC x = Heap (mrec x)"
 
 lemma MREC_rule:
-  "MREC f g x = 
+  "MREC x = 
   (do y \<leftarrow> f x;
                 (case y of 
                 Inl r \<Rightarrow> return r
               | Inr s \<Rightarrow> 
-                do z \<leftarrow> MREC f g s ;
+                do z \<leftarrow> MREC 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])
+  apply (unfold mrec_rule[of x])
   by (auto split:prod.splits sum.splits)
 
+
+lemma MREC_pinduct:
+  assumes "Heap_Monad.execute (MREC x) h = (Inl r, h')"
+  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"
+  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
+    \<Longrightarrow> Heap_Monad.execute (g x s z) h2 = (Inl r, h') \<Longrightarrow> P x h h' r"
+  shows "P x h h' r"
+proof -
+  from assms(1) have mrec: "mrec x h = (Inl 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 (mrec x h))" "r = (Sum_Type.Projl (fst (mrec x h)))"
+    by auto
+  from mrec have "P x h (snd (mrec x h)) (Sum_Type.Projl (fst (mrec x h)))"
+  proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom])
+    case (1 x h)
+    obtain rr h' where "mrec x h = (rr, h')" by fastsimp
+    obtain fret h1 where exec_f: "Heap_Monad.execute (f x) h = (fret, h1)" by fastsimp
+    show ?case
+    proof (cases fret)
+      case (Inl a)
+      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
+        obtain ret_mrec h2 where mrec_rec: "mrec b h1 = (ret_mrec, h2)" by fastsimp
+        from this Inl 1(1) exec_f mrec show ?thesis
+        proof (cases "ret_mrec")
+          case (Inl aaa)
+          from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2)[OF exec_f Inl' Inr', of "aaa" "h2"] 1(3)
+            show ?thesis
+              apply auto
+              apply (rule rec_case)
+              unfolding MREC_def by auto
+        next
+          case (Inr b)
+          from this Inl 1(1) exec_f mrec Inr' mrec_rec 1(3) show ?thesis by auto
+        qed
+      qed
+    next
+      case (Inr b)
+      from this 1(1) mrec exec_f 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
+
 hide (open) const heap execute