# HG changeset patch # User wenzelm # Date 1441543909 -7200 # Node ID 7beed856816cff21c0da62233e565d123cc150a8 # Parent a39e9c46a7722e193bfaa4525bd51ba97626a2e0 removed obsolete theory Legacy_Mrec; diff -r a39e9c46a772 -r 7beed856816c NEWS --- a/NEWS Sun Sep 06 13:37:18 2015 +0200 +++ b/NEWS Sun Sep 06 14:51:49 2015 +0200 @@ -282,6 +282,8 @@ * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef' command. Minor INCOMPATIBILITY, use 'function' instead. +* Imperative_HOL: obsolete theory Legacy_Mrec has been removed. + *** ML *** diff -r a39e9c46a772 -r 7beed856816c src/HOL/Imperative_HOL/Imperative_HOL_ex.thy --- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Sun Sep 06 13:37:18 2015 +0200 +++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Sun Sep 06 14:51:49 2015 +0200 @@ -8,7 +8,6 @@ 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 a39e9c46a772 -r 7beed856816c src/HOL/Imperative_HOL/Legacy_Mrec.thy --- a/src/HOL/Imperative_HOL/Legacy_Mrec.thy Sun Sep 06 13:37:18 2015 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,169 +0,0 @@ -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 mrec_rec 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