# HG changeset patch # User bulwahn # Date 1270046681 -7200 # Node ID ca6610908ae93f1ce54c1e48d1708c963a1d0cdc # Parent 0c128c2c310d3735d2cd53076a57ae8a8d52d5c6 adding MREC induction rule in Imperative HOL diff -r 0c128c2c310d -r ca6610908ae9 src/HOL/Imperative_HOL/Heap_Monad.thy --- 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 "\(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 "\(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') \ (Inl r, h') | (Inl (Inr s), h') \ - (case mrec f g s h' of + (case mrec 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') @@ -292,17 +300,17 @@ apply (erule mrec_rel.cases) by simp -lemma f_default: "\ mrec_dom (f, g, x, h) \ mrec f g x h = (Inr Exn, undefined)" +lemma mrec_default: "\ mrec_dom (x, h) \ 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 "\ mrec_dom (f, g, x, h)" +lemma mrec_di_reverse: + assumes "\ mrec_dom (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 + (Inl (Inl r), h') \ False + | (Inl (Inr s), h') \ \ mrec_dom (s, h') + | (Inr e, h') \ 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') \ (Inl r, h') | (Inl (Inr s), h') \ - (case mrec f g s h' of + (case mrec 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) +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 \ f x; (case y of Inl r \ return r | Inr s \ - do z \ MREC f g s ; + do z \ 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: "\ x h h' r. Heap_Monad.execute (f x) h = (Inl (Inl r), h') \ P x h h' r" + assumes rec_case: "\ x h h1 h2 h' s z r. Heap_Monad.execute (f x) h = (Inl (Inr s), h1) \ Heap_Monad.execute (MREC s) h1 = (Inl z, h2) \ P s h1 h2 z + \ Heap_Monad.execute (g x s z) h2 = (Inl r, h') \ 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 diff -r 0c128c2c310d -r ca6610908ae9 src/HOL/Imperative_HOL/Relational.thy --- 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 "\ x h h' r. crel (f x) h h' (Inl r) \ P x h h' r" + assumes "\ x h h1 h2 h' s z r. crel (f x) h h1 (Inr s) \ crel (MREC f g s) h1 h2 z \ P s h1 h2 z + \ crel (g x s z) h2 h' r \ 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,