# HG changeset patch # User krauss # Date 1377030242 -7200 # Node ID ae863ed9f64fc6b0b830da3e4f74e8775a82dbd0 # Parent 186535065f5c776d54076c31e93f257f8202ec41# Parent d81211f61a1b4e6bb07c8b8c19f23acd0b328383 merged diff -r d81211f61a1b -r ae863ed9f64f NEWS --- a/NEWS Tue Aug 20 17:39:08 2013 +0200 +++ b/NEWS Tue Aug 20 22:24:02 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 d81211f61a1b -r ae863ed9f64f src/Doc/Functions/Functions.thy --- a/src/Doc/Functions/Functions.thy Tue Aug 20 17:39:08 2013 +0200 +++ b/src/Doc/Functions/Functions.thy Tue Aug 20 22:24:02 2013 +0200 @@ -87,7 +87,7 @@ Isabelle provides customized induction rules for recursive functions. These rules follow the recursive structure of the - definition. Here is the rule @{text sep.induct} arising from the + definition. Here is the rule @{thm [source] sep.induct} arising from the above definition of @{const sep}: @{thm [display] sep.induct} @@ -387,7 +387,7 @@ text {* When functions are mutually recursive, proving properties about them - generally requires simultaneous induction. The induction rule @{text "even_odd.induct"} + generally requires simultaneous induction. The induction rule @{thm [source] "even_odd.induct"} generated from the above definition reflects this. Let us prove something about @{const even} and @{const odd}: @@ -507,7 +507,7 @@ can be simplified to @{term "F"} with the original equations, a (manual) case split on @{term "x"} is now necessary. - \item The splitting also concerns the induction rule @{text + \item The splitting also concerns the induction rule @{thm [source] "And.induct"}. Instead of five premises it now has seven, which means that our induction proofs will have more cases. @@ -730,11 +730,11 @@ text {* \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.psimps}\end{minipage} - \hfill(@{text "findzero.psimps"}) + \hfill(@{thm [source] "findzero.psimps"}) \vspace{1em} \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.pinduct}\end{minipage} - \hfill(@{text "findzero.pinduct"}) + \hfill(@{thm [source] "findzero.pinduct"}) *} text {* @@ -854,10 +854,10 @@ Since our function increases its argument at recursive calls, we need an induction principle which works \qt{backwards}. We will use - @{text inc_induct}, which allows to do induction from a fixed number + @{thm [source] inc_induct}, which allows to do induction from a fixed number \qt{downwards}: - \begin{center}@{thm inc_induct}\hfill(@{text "inc_induct"})\end{center} + \begin{center}@{thm inc_induct}\hfill(@{thm [source] "inc_induct"})\end{center} Figure \ref{findzero_term} gives a detailed Isar proof of the fact that @{text findzero} terminates if there is a zero which is greater @@ -936,7 +936,7 @@ findzero_rel}, which was also created internally by the function package. @{const findzero_rel} is just a normal inductive predicate, so we can inspect its definition by - looking at the introduction rules @{text findzero_rel.intros}. + looking at the introduction rules @{thm [source] findzero_rel.intros}. In our case there is just a single rule: @{thm[display] findzero_rel.intros} @@ -955,9 +955,10 @@ Since the domain predicate is just an abbreviation, you can use lemmas for @{const accp} and @{const findzero_rel} directly. Some - lemmas which are occasionally useful are @{text accpI}, @{text + lemmas which are occasionally useful are @{thm [source] accpI}, @{thm [source] accp_downward}, and of course the introduction and elimination rules - for the recursion relation @{text "findzero.intros"} and @{text "findzero.cases"}. + for the recursion relation @{thm [source] "findzero_rel.intros"} and @{thm + [source] "findzero_rel.cases"}. *} section {* Nested recursion *} @@ -1158,7 +1159,7 @@ congruence rule that specifies left-to-right evaluation order: \vspace{1ex} - \noindent @{thm disj_cong}\hfill(@{text "disj_cong"}) + \noindent @{thm disj_cong}\hfill(@{thm [source] "disj_cong"}) \vspace{1ex} Now the definition works without problems. Note how the termination diff -r d81211f61a1b -r ae863ed9f64f src/HOL/Imperative_HOL/Imperative_HOL.thy --- a/src/HOL/Imperative_HOL/Imperative_HOL.thy Tue Aug 20 17:39:08 2013 +0200 +++ b/src/HOL/Imperative_HOL/Imperative_HOL.thy Tue Aug 20 22:24:02 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 d81211f61a1b -r ae863ed9f64f src/HOL/Imperative_HOL/Imperative_HOL_ex.thy --- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Tue Aug 20 17:39:08 2013 +0200 +++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Tue Aug 20 22:24:02 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 d81211f61a1b -r ae863ed9f64f 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 22:24:02 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 d81211f61a1b -r ae863ed9f64f src/HOL/Imperative_HOL/Mrec.thy --- a/src/HOL/Imperative_HOL/Mrec.thy Tue Aug 20 17:39:08 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 diff -r d81211f61a1b -r ae863ed9f64f src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Tue Aug 20 17:39:08 2013 +0200 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Tue Aug 20 22:24:02 2013 +0200 @@ -664,20 +664,22 @@ subsection {* Definition of merge function *} -definition merge' :: "(('a::{heap, ord}) node ref * ('a::{heap, ord})) * ('a::{heap, ord}) node ref * ('a::{heap, ord}) node ref \ ('a::{heap, ord}) node ref Heap" +partial_function (heap) merge :: "('a::{heap, ord}) node ref \ 'a node ref \ 'a node ref Heap" where -"merge' = MREC (\(_, p, q). do { v \ !p; w \ !q; - (case v of Empty \ return (Inl q) +[code]: "merge p q = (do { v \ !p; w \ !q; + (case v of Empty \ return q | Node valp np \ - (case w of Empty \ return (Inl p) + (case w of Empty \ return p | Node valq nq \ - if (valp \ valq) then - return (Inr ((p, valp), np, q)) - else - return (Inr ((q, valq), p, nq)))) }) - (\ _ ((n, v), _, _) r. do { n := Node v r; return n })" + if (valp \ valq) then do { + npq \ merge np q; + p := Node valp npq; + return p } + else do { + pnq \ merge p nq; + q := Node valq pnq; + return q }))})" -definition merge where "merge p q = merge' (undefined, p, q)" lemma if_return: "(if P then return x else return y) = return (if P then x else y)" by auto @@ -693,45 +695,6 @@ lemma sum_distrib: "sum_case fl fr (case x of Empty \ y | Node v n \ (z v n)) = (case x of Empty \ sum_case fl fr y | Node v n \ sum_case fl fr (z v n))" by (cases x) auto -lemma merge: "merge' (x, p, q) = merge p q" -unfolding merge'_def merge_def -apply (simp add: MREC_rule) done -term "Ref.change" -lemma merge_simps [code]: -shows "merge p q = -do { v \ !p; - w \ !q; - (case v of node.Empty \ return q - | Node valp np \ - case w of node.Empty \ return p - | Node valq nq \ - if valp \ valq then do { r \ merge np q; - p := (Node valp r); - return p - } - else do { r \ merge p nq; - q := (Node valq r); - return q - }) -}" -proof - - {fix v x y - have case_return: "(case v of Empty \ return x | Node v n \ return (y v n)) = return (case v of Empty \ x | Node v n \ y v n)" by (cases v) auto - } note case_return = this -show ?thesis -unfolding merge_def[of p q] merge'_def -apply (simp add: MREC_rule[of _ _ "(undefined, p, q)"]) -unfolding bind_bind return_bind -unfolding merge'_def[symmetric] -unfolding if_return case_return bind_bind return_bind sum_distrib sum.cases -unfolding if_distrib[symmetric, where f="Inr"] -unfolding sum.cases -unfolding if_distrib -unfolding split_beta fst_conv snd_conv -unfolding if_distrib_App redundant_if merge -.. -qed - subsection {* Induction refinement by applying the abstraction function to our induct rule *} text {* From our original induction rule Lmerge.induct, we derive a new rule with our list_of' predicate *} @@ -800,13 +763,13 @@ proof (induct arbitrary: h' r rule: merge_induct2[OF assms(1) assms(2)]) case (1 ys p q) from 1(3-4) have "h = h' \ r = q" - unfolding merge_simps[of p q] + unfolding merge.simps[of p q] by (auto elim!: effect_lookupE effect_bindE effect_returnE) with assms(4)[OF 1(1) 1(2) 1(3)] show ?case by simp next case (2 x xs' p q pn) from 2(3-5) have "h = h' \ r = p" - unfolding merge_simps[of p q] + unfolding merge.simps[of p q] by (auto elim!: effect_lookupE effect_bindE effect_returnE) with assms(5)[OF 2(1-4)] show ?case by simp next @@ -814,7 +777,7 @@ from 3(3-5) 3(7) obtain h1 r1 where 1: "effect (merge pn q) h h1 r1" and 2: "h' = Ref.set p (Node x r1) h1 \ r = p" - unfolding merge_simps[of p q] + unfolding merge.simps[of p q] by (auto elim!: effect_lookupE effect_bindE effect_returnE effect_ifE effect_updateE) from 3(6)[OF 1] assms(6) [OF 3(1-5)] 1 2 show ?case by simp next @@ -822,7 +785,7 @@ from 4(3-5) 4(7) obtain h1 r1 where 1: "effect (merge p qn) h h1 r1" and 2: "h' = Ref.set q (Node y r1) h1 \ r = q" - unfolding merge_simps[of p q] + unfolding merge.simps[of p q] by (auto elim!: effect_lookupE effect_bindE effect_returnE effect_ifE effect_updateE) from 4(6)[OF 1] assms(7) [OF 4(1-5)] 1 2 show ?case by simp qed