# HG changeset patch # User krauss # Date 1376991593 -7200 # Node ID 186535065f5c776d54076c31e93f257f8202ec41 # Parent d84c8de81edf48d44517678b44bf03bb77b3d489 renamed theory Mrec to Legacy_Mrec, no longer included by default diff -r d84c8de81edf -r 186535065f5c NEWS --- a/NEWS Tue Aug 20 11:21:49 2013 +0200 +++ b/NEWS Tue Aug 20 11:39:53 2013 +0200 @@ -312,6 +312,10 @@ "ALL x1 ... xn. Prop x1 ... xn". Simple examples are in src/HOL/Spec_Check/Examples.thy. +* Imperative HOL: The MREC combinator is considered legacy and no longer +included by default. INCOMPATIBILITY, use partial_function instead, or import +theory Legacy_Mrec as a fallback. + *** HOL-Algebra *** diff -r d84c8de81edf -r 186535065f5c src/HOL/Imperative_HOL/Imperative_HOL.thy --- a/src/HOL/Imperative_HOL/Imperative_HOL.thy Tue Aug 20 11:21:49 2013 +0200 +++ b/src/HOL/Imperative_HOL/Imperative_HOL.thy Tue Aug 20 11:39:53 2013 +0200 @@ -5,7 +5,7 @@ header {* Entry point into monadic imperative HOL *} theory Imperative_HOL -imports Array Ref Mrec +imports Array Ref begin end diff -r d84c8de81edf -r 186535065f5c src/HOL/Imperative_HOL/Imperative_HOL_ex.thy --- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Tue Aug 20 11:21:49 2013 +0200 +++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Tue Aug 20 11:39:53 2013 +0200 @@ -8,6 +8,7 @@ theory Imperative_HOL_ex imports Imperative_HOL Overview "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker" + Legacy_Mrec begin definition "everything = (Array.new, Array.of_list, Array.make, Array.len, Array.nth, diff -r d84c8de81edf -r 186535065f5c src/HOL/Imperative_HOL/Legacy_Mrec.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Imperative_HOL/Legacy_Mrec.thy Tue Aug 20 11:39:53 2013 +0200 @@ -0,0 +1,169 @@ +theory Legacy_Mrec +imports Heap_Monad +begin + +subsubsection {* A monadic combinator for simple recursive functions *} + +text {* + NOTE: The use of this obsolete combinator is discouraged. Instead, use the + @{text "partal_function (heap)"} command. +*} + +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). None") mrec :: "'a \ heap \ ('b \ heap) option" where + "mrec x h = (case execute (f x) h of + Some (Inl r, h') \ Some (r, h') + | Some (Inr s, h') \ (case mrec s h' of + Some (z, h'') \ execute (g x s z) h'' + | None \ None) + | None \ None)" +by auto + +lemma graph_implies_dom: + "mrec_graph x y \ mrec_dom x" +apply (induct rule:mrec_graph.induct) +apply (rule accpI) +apply (erule mrec_rel.cases) +by simp + +lemma mrec_default: "\ mrec_dom (x, h) \ 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 "\ mrec_dom (x, h)" + shows " + (case execute (f x) h of + Some (Inl r, h') \ False + | Some (Inr s, h') \ \ mrec_dom (s, h') + | None \ 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') \ Some (r, h') + | Some (Inr s, h') \ + (case mrec s h' of + Some (z, h'') \ execute (g x s z) h'' + | None \ None) + | None \ None + )" +apply (cases "mrec_dom (x,h)", simp add: mrec.psimps) +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 \ f x; + (case y of + Inl r \ return r + | Inr s \ + do { z \ MREC s ; + g x s z })}" + unfolding MREC_def + unfolding bind_def return_def + apply simp + apply (rule ext) + apply (unfold mrec_rule[of x]) + by (auto simp add: execute_simps split: option.splits prod.splits sum.splits) + +lemma MREC_pinduct: + assumes "execute (MREC x) h = Some (r, h')" + assumes non_rec_case: "\ x h h' r. execute (f x) h = Some (Inl r, h') \ P x h h' r" + assumes rec_case: "\ x h h1 h2 h' s z r. execute (f x) h = Some (Inr s, h1) \ execute (MREC s) h1 = Some (z, h2) \ P s h1 h2 z + \ execute (g x s z) h2 = Some (r, h') \ 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 fastforce + 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 fastforce + 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 simp: mrec.psimps) + 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 fastforce + 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 simp: mrec.psimps) + next + case None + from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by (auto simp: mrec.psimps) + qed + qed + next + case None + from this 1(1) mrec 1(3) show ?thesis by (simp add: mrec.psimps) + 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 "effect (MREC f g x) h h' r" + assumes "\ x h h' r. effect (f x) h h' (Inl r) \ P x h h' r" + assumes "\ x h h1 h2 h' s z r. effect (f x) h h1 (Inr s) \ effect (MREC f g s) h1 h2 z \ P s h1 h2 z + \ effect (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 effect_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 effect_def, OF this(1) this(2) this(3) this(4)] + show "P x h h' r" . +next +qed (auto simp add: assms(2)[unfolded effect_def]) + +end diff -r d84c8de81edf -r 186535065f5c src/HOL/Imperative_HOL/Mrec.thy --- a/src/HOL/Imperative_HOL/Mrec.thy Tue Aug 20 11:21:49 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,164 +0,0 @@ -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 \ ('b + 'a) Heap" - and g :: "'a \ 'a \ 'b \ 'b Heap" -begin - -function (default "\(x, h). None") mrec :: "'a \ heap \ ('b \ heap) option" where - "mrec x h = (case execute (f x) h of - Some (Inl r, h') \ Some (r, h') - | Some (Inr s, h') \ (case mrec s h' of - Some (z, h'') \ execute (g x s z) h'' - | None \ None) - | None \ None)" -by auto - -lemma graph_implies_dom: - "mrec_graph x y \ mrec_dom x" -apply (induct rule:mrec_graph.induct) -apply (rule accpI) -apply (erule mrec_rel.cases) -by simp - -lemma mrec_default: "\ mrec_dom (x, h) \ 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 "\ mrec_dom (x, h)" - shows " - (case execute (f x) h of - Some (Inl r, h') \ False - | Some (Inr s, h') \ \ mrec_dom (s, h') - | None \ 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') \ Some (r, h') - | Some (Inr s, h') \ - (case mrec s h' of - Some (z, h'') \ execute (g x s z) h'' - | None \ None) - | None \ None - )" -apply (cases "mrec_dom (x,h)", simp add: mrec.psimps) -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 \ f x; - (case y of - Inl r \ return r - | Inr s \ - do { z \ MREC s ; - g x s z })}" - unfolding MREC_def - unfolding bind_def return_def - apply simp - apply (rule ext) - apply (unfold mrec_rule[of x]) - by (auto simp add: execute_simps split: option.splits prod.splits sum.splits) - -lemma MREC_pinduct: - assumes "execute (MREC x) h = Some (r, h')" - assumes non_rec_case: "\ x h h' r. execute (f x) h = Some (Inl r, h') \ P x h h' r" - assumes rec_case: "\ x h h1 h2 h' s z r. execute (f x) h = Some (Inr s, h1) \ execute (MREC s) h1 = Some (z, h2) \ P s h1 h2 z - \ execute (g x s z) h2 = Some (r, h') \ 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 fastforce - 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 fastforce - 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 simp: mrec.psimps) - 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 fastforce - 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 simp: mrec.psimps) - next - case None - from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by (auto simp: mrec.psimps) - qed - qed - next - case None - from this 1(1) mrec 1(3) show ?thesis by (simp add: mrec.psimps) - 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 "effect (MREC f g x) h h' r" - assumes "\ x h h' r. effect (f x) h h' (Inl r) \ P x h h' r" - assumes "\ x h h1 h2 h' s z r. effect (f x) h h1 (Inr s) \ effect (MREC f g s) h1 h2 z \ P s h1 h2 z - \ effect (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 effect_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 effect_def, OF this(1) this(2) this(3) this(4)] - show "P x h h' r" . -next -qed (auto simp add: assms(2)[unfolded effect_def]) - -end