--- 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 ***
--- 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
--- 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
--- 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,
--- /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 \<Rightarrow> ('b + 'a) Heap"
+ and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b Heap"
+begin
+
+function (default "\<lambda>(x, h). None") mrec :: "'a \<Rightarrow> heap \<Rightarrow> ('b \<times> heap) option" where
+ "mrec x h = (case execute (f x) h of
+ Some (Inl r, h') \<Rightarrow> Some (r, h')
+ | Some (Inr s, h') \<Rightarrow> (case mrec s h' of
+ Some (z, h'') \<Rightarrow> execute (g x s z) h''
+ | None \<Rightarrow> None)
+ | None \<Rightarrow> None)"
+by auto
+
+lemma graph_implies_dom:
+ "mrec_graph x y \<Longrightarrow> mrec_dom x"
+apply (induct rule:mrec_graph.induct)
+apply (rule accpI)
+apply (erule mrec_rel.cases)
+by simp
+
+lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> 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 "\<not> mrec_dom (x, h)"
+ shows "
+ (case execute (f x) h of
+ Some (Inl r, h') \<Rightarrow> False
+ | Some (Inr s, h') \<Rightarrow> \<not> mrec_dom (s, h')
+ | None \<Rightarrow> 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') \<Rightarrow> Some (r, h')
+ | Some (Inr s, h') \<Rightarrow>
+ (case mrec s h' of
+ Some (z, h'') \<Rightarrow> execute (g x s z) h''
+ | None \<Rightarrow> None)
+ | None \<Rightarrow> 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 \<leftarrow> f x;
+ (case y of
+ Inl r \<Rightarrow> return r
+ | Inr s \<Rightarrow>
+ do { z \<leftarrow> 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: "\<And> x h h' r. execute (f x) h = Some (Inl r, h') \<Longrightarrow> P x h h' r"
+ assumes rec_case: "\<And> x h h1 h2 h' s z r. execute (f x) h = Some (Inr s, h1) \<Longrightarrow> execute (MREC s) h1 = Some (z, h2) \<Longrightarrow> P s h1 h2 z
+ \<Longrightarrow> execute (g x s z) h2 = Some (r, h') \<Longrightarrow> 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 "\<And> x h h' r. effect (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
+ assumes "\<And> x h h1 h2 h' s z r. effect (f x) h h1 (Inr s) \<Longrightarrow> effect (MREC f g s) h1 h2 z \<Longrightarrow> P s h1 h2 z
+ \<Longrightarrow> effect (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 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
--- 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 \<Rightarrow> ('b + 'a) Heap"
- and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b Heap"
-begin
-
-function (default "\<lambda>(x, h). None") mrec :: "'a \<Rightarrow> heap \<Rightarrow> ('b \<times> heap) option" where
- "mrec x h = (case execute (f x) h of
- Some (Inl r, h') \<Rightarrow> Some (r, h')
- | Some (Inr s, h') \<Rightarrow> (case mrec s h' of
- Some (z, h'') \<Rightarrow> execute (g x s z) h''
- | None \<Rightarrow> None)
- | None \<Rightarrow> None)"
-by auto
-
-lemma graph_implies_dom:
- "mrec_graph x y \<Longrightarrow> mrec_dom x"
-apply (induct rule:mrec_graph.induct)
-apply (rule accpI)
-apply (erule mrec_rel.cases)
-by simp
-
-lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> 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 "\<not> mrec_dom (x, h)"
- shows "
- (case execute (f x) h of
- Some (Inl r, h') \<Rightarrow> False
- | Some (Inr s, h') \<Rightarrow> \<not> mrec_dom (s, h')
- | None \<Rightarrow> 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') \<Rightarrow> Some (r, h')
- | Some (Inr s, h') \<Rightarrow>
- (case mrec s h' of
- Some (z, h'') \<Rightarrow> execute (g x s z) h''
- | None \<Rightarrow> None)
- | None \<Rightarrow> 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 \<leftarrow> f x;
- (case y of
- Inl r \<Rightarrow> return r
- | Inr s \<Rightarrow>
- do { z \<leftarrow> 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: "\<And> x h h' r. execute (f x) h = Some (Inl r, h') \<Longrightarrow> P x h h' r"
- assumes rec_case: "\<And> x h h1 h2 h' s z r. execute (f x) h = Some (Inr s, h1) \<Longrightarrow> execute (MREC s) h1 = Some (z, h2) \<Longrightarrow> P s h1 h2 z
- \<Longrightarrow> execute (g x s z) h2 = Some (r, h') \<Longrightarrow> 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 "\<And> x h h' r. effect (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
- assumes "\<And> x h h1 h2 h' s z r. effect (f x) h h1 (Inr s) \<Longrightarrow> effect (MREC f g s) h1 h2 z \<Longrightarrow> P s h1 h2 z
- \<Longrightarrow> effect (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 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
--- 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 \<Rightarrow> ('a::{heap, ord}) node ref Heap"
+partial_function (heap) merge :: "('a::{heap, ord}) node ref \<Rightarrow> 'a node ref \<Rightarrow> 'a node ref Heap"
where
-"merge' = MREC (\<lambda>(_, p, q). do { v \<leftarrow> !p; w \<leftarrow> !q;
- (case v of Empty \<Rightarrow> return (Inl q)
+[code]: "merge p q = (do { v \<leftarrow> !p; w \<leftarrow> !q;
+ (case v of Empty \<Rightarrow> return q
| Node valp np \<Rightarrow>
- (case w of Empty \<Rightarrow> return (Inl p)
+ (case w of Empty \<Rightarrow> return p
| Node valq nq \<Rightarrow>
- if (valp \<le> valq) then
- return (Inr ((p, valp), np, q))
- else
- return (Inr ((q, valq), p, nq)))) })
- (\<lambda> _ ((n, v), _, _) r. do { n := Node v r; return n })"
+ if (valp \<le> valq) then do {
+ npq \<leftarrow> merge np q;
+ p := Node valp npq;
+ return p }
+ else do {
+ pnq \<leftarrow> 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 \<Rightarrow> y | Node v n \<Rightarrow> (z v n)) = (case x of Empty \<Rightarrow> sum_case fl fr y | Node v n \<Rightarrow> 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 \<leftarrow> !p;
- w \<leftarrow> !q;
- (case v of node.Empty \<Rightarrow> return q
- | Node valp np \<Rightarrow>
- case w of node.Empty \<Rightarrow> return p
- | Node valq nq \<Rightarrow>
- if valp \<le> valq then do { r \<leftarrow> merge np q;
- p := (Node valp r);
- return p
- }
- else do { r \<leftarrow> merge p nq;
- q := (Node valq r);
- return q
- })
-}"
-proof -
- {fix v x y
- have case_return: "(case v of Empty \<Rightarrow> return x | Node v n \<Rightarrow> return (y v n)) = return (case v of Empty \<Rightarrow> x | Node v n \<Rightarrow> 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' \<and> 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' \<and> 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 \<and> 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 \<and> 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