src/HOL/Imperative_HOL/ex/Linked_Lists.thy

 | "Lmerge [] ys = ys"
 | "Lmerge xs [] = xs"
 
 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 })"
-
-definition merge where "merge p q = merge' (undefined, p, q)"
+                       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 }))})"
+
 
 lemma if_return: "(if P then return x else return y) = return (if P then x else y)"
 by auto
 
 lemma if_distrib_App: "(if P then f else g) x = (if P then f x else g x)"

 
 
 
 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 *}
 

 shows "P p q h h' r xs ys"
 using assms(3)
 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
   case (3 x xs' y ys' p q pn qn)
   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
   case (4 x xs' y ys' p q pn qn)
   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