--- 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
--- a/src/HOL/Imperative_HOL/Relational.thy Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Imperative_HOL/Relational.thy Wed Mar 31 16:44:41 2010 +0200
@@ -469,7 +469,7 @@
(* thm crel_mapI is missing *)
-subsection {* Introduction rules for reference commands *}
+subsubsection {* Introduction rules for reference commands *}
lemma crel_lookupI:
shows "crel (!ref) h h (get_ref ref h)"
@@ -483,7 +483,7 @@
shows "crel (Ref.change f ref) h (set_ref ref (f (get_ref ref h)) h) (f (get_ref ref h))"
unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
-subsection {* Introduction rules for the assert command *}
+subsubsection {* Introduction rules for the assert command *}
lemma crel_assertI:
assumes "P x"
@@ -492,7 +492,26 @@
unfolding assert_def
by (auto intro!: crel_ifI crel_returnI crel_raiseI)
-section {* Defintion of the noError predicate *}
+subsection {* Induction rule for the MREC combinator *}
+
+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, symmetric]])
+ fix x h h1 h2 h' s z r
+ assume "Heap_Monad.execute (f x) h = (Inl (Inr s), h1)"
+ "Heap_Monad.execute (MREC f g s) h1 = (Inl z, h2)"
+ "P s h1 h2 z"
+ "Heap_Monad.execute (g x s z) h2 = (Inl r, h')"
+ from assms(3)[unfolded crel_def, OF this(1)[symmetric] this(2)[symmetric] this(3) this(4)[symmetric]]
+ show "P x h h' r" .
+next
+qed (auto simp add: assms(2)[unfolded crel_def])
+
+section {* Definition of the noError predicate *}
text {* We add a simple definitional setting for crel intro rules
where we only would like to show that the computation does not result in a exception for heap h,