# HG changeset patch
# User krauss
# Date 1288088342 -7200
# Node ID 97b69fef52291d9957e1e336f2441d385908d6e4
# Parent  0ffdd6baec03de13e5a11e0b22863db245184585
use partial_function instead of MREC combinator; curried rev'

diff -r 0ffdd6baec03 -r 97b69fef5229 src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Oct 26 12:19:02 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Oct 26 12:19:02 2010 +0200
@@ -37,17 +37,14 @@
                                    }"
 
 
-text {* define traverse using the MREC combinator *}
-
-definition
-  traverse :: "'a\<Colon>heap node \<Rightarrow> 'a list Heap"
+partial_function (heap) traverse :: "'a\<Colon>heap node \<Rightarrow> 'a list Heap"
 where
-[code del]: "traverse = MREC (\<lambda>n. case n of Empty \<Rightarrow> return (Inl [])
-                                | Node x r \<Rightarrow> do { tl \<leftarrow> Ref.lookup r;
-                                                  return (Inr tl) })
-                   (\<lambda>n tl xs. case n of Empty \<Rightarrow> undefined
-                                      | Node x r \<Rightarrow> return (x # xs))"
-
+  [code del]: "traverse l =
+    (case l of Empty \<Rightarrow> return []
+     | Node x r \<Rightarrow> do { tl \<leftarrow> Ref.lookup r;
+                              xs \<leftarrow> traverse tl;
+                              return (x#xs)
+                         })"
 
 lemma traverse_simps[code, simp]:
   "traverse Empty      = return []"
@@ -55,8 +52,7 @@
                               xs \<leftarrow> traverse tl;
                               return (x#xs)
                          }"
-unfolding traverse_def
-by (auto simp: traverse_def MREC_rule)
+by (simp_all add: traverse.simps[of "Empty"] traverse.simps[of "Node x r"])
 
 
 section {* Proving correctness with relational abstraction *}
@@ -528,16 +524,9 @@
 
 subsection {* Definition of in-place reversal *}
 
-definition rev' :: "(('a::heap) node ref \<times> 'a node ref) \<Rightarrow> 'a node ref Heap"
-where "rev' = MREC (\<lambda>(q, p). do { v \<leftarrow> !p; (case v of Empty \<Rightarrow> (return (Inl q))
-                            | Node x next \<Rightarrow> do {
-                                    p := Node x q;
-                                    return (Inr (p, next))
-                                  })})
-             (\<lambda>x s z. return z)"
-
-lemma rev'_simps [code]:
-  "rev' (q, p) =
+partial_function (heap) rev' :: "('a::heap) node ref \<Rightarrow> 'a node ref \<Rightarrow> 'a node ref Heap"
+where
+  [code]: "rev' q p =
    do {
      v \<leftarrow> !p;
      (case v of
@@ -545,22 +534,19 @@
       | Node x next \<Rightarrow>
         do {
           p := Node x q;
-          rev' (p, next)
+          rev' p next
         })
-  }"
-  unfolding rev'_def MREC_rule[of _ _ "(q, p)"] unfolding rev'_def[symmetric]
-thm arg_cong2
-  by (auto simp add: fun_eq_iff intro: arg_cong2[where f = bind] split: node.split)
-
+    }"
+  
 primrec rev :: "('a:: heap) node \<Rightarrow> 'a node Heap" 
 where
   "rev Empty = return Empty"
-| "rev (Node x n) = do { q \<leftarrow> ref Empty; p \<leftarrow> ref (Node x n); v \<leftarrow> rev' (q, p); !v }"
+| "rev (Node x n) = do { q \<leftarrow> ref Empty; p \<leftarrow> ref (Node x n); v \<leftarrow> rev' q p; !v }"
 
 subsection {* Correctness Proof *}
 
 lemma rev'_invariant:
-  assumes "crel (rev' (q, p)) h h' v"
+  assumes "crel (rev' q p) h h' v"
   assumes "list_of' h q qs"
   assumes "list_of' h p ps"
   assumes "\<forall>qrs prs. refs_of' h q qrs \<and> refs_of' h p prs \<longrightarrow> set prs \<inter> set qrs = {}"
@@ -569,7 +555,7 @@
 proof (induct ps arbitrary: qs p q h)
   case Nil
   thus ?case
-    unfolding rev'_simps[of q p] list_of'_def
+    unfolding rev'.simps[of q p] list_of'_def
     by (auto elim!: crel_bindE crel_lookupE crel_returnE)
 next
   case (Cons x xs)
@@ -579,8 +565,8 @@
     (*and "ref_present ref h"*)
     and list_of'_ref: "list_of' h ref xs"
     unfolding list_of'_def by (cases "Ref.get h p", auto)
-  from p_is_Node Cons(2) have crel_rev': "crel (rev' (p, ref)) (Ref.set p (Node x q) h) h' v"
-    by (auto simp add: rev'_simps [of q p] elim!: crel_bindE crel_lookupE crel_updateE)
+  from p_is_Node Cons(2) have crel_rev': "crel (rev' p ref) (Ref.set p (Node x q) h) h' v"
+    by (auto simp add: rev'.simps [of q p] elim!: crel_bindE crel_lookupE crel_updateE)
   from Cons(3) obtain qrs where qrs_def: "refs_of' h q qrs" by (elim list_of'_refs_of')
   from Cons(4) obtain prs where prs_def: "refs_of' h p prs" by (elim list_of'_refs_of')
   from qrs_def prs_def Cons(5) have distinct_pointers: "set qrs \<inter> set prs = {}" by fastsimp
@@ -627,7 +613,7 @@
   with crel_rev obtain p q h1 h2 h3 v where
     init: "crel (ref Empty) h h1 q"
     "crel (ref (Node x ps)) h1 h2 p"
-    and crel_rev':"crel (rev' (q, p)) h2 h3 v"
+    and crel_rev':"crel (rev' q p) h2 h3 v"
     and lookup: "crel (!v) h3 h' r'"
     using rev.simps
     by (auto elim!: crel_bindE)