--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Imperative_HOL/Mrec.thy Mon Jul 12 16:19:15 2010 +0200
@@ -0,0 +1,165 @@
+theory Mrec
+imports Heap_Monad
+begin
+
+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_Monad.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
+
+lemma MREC_induct:
+ assumes "crel (MREC f g x) h h' r"
+ assumes "\<And> x h h' r. crel (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
+ assumes "\<And> x h h1 h2 h' s z r. crel (f x) h h1 (Inr s) \<Longrightarrow> crel (MREC f g s) h1 h2 z \<Longrightarrow> P s h1 h2 z
+ \<Longrightarrow> crel (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
+ shows "P x h h' r"
+proof (rule MREC_pinduct[OF assms(1) [unfolded crel_def]])
+ fix x h h1 h2 h' s z r
+ assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)"
+ "Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)"
+ "P s h1 h2 z"
+ "Heap_Monad.execute (g x s z) h2 = Some (r, h')"
+ from assms(3) [unfolded crel_def, OF this(1) this(2) this(3) this(4)]
+ show "P x h h' r" .
+next
+qed (auto simp add: assms(2)[unfolded crel_def])
+
+end