# HG changeset patch
# User blanchet
# Date 1288088619 -7200
# Node ID 7ecfa9beef91588074c2cefb476b9d5c352a96a3
# Parent  30482e17955bbbf246cda1a98c1f445646e61b46# Parent  00152d17855bc2efdae007aebbdb620b0764b77c
merged

diff -r 00152d17855b -r 7ecfa9beef91 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Oct 26 12:17:19 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Oct 26 12:23:39 2010 +0200
@@ -401,11 +401,9 @@
   \begin{rail}
     'primrec' target? fixes 'where' equations
     ;
-    equations: (thmdecl? prop + '|')
+    ('fun' | 'function') target? functionopts? fixes \\ 'where' equations
     ;
-    ('fun' | 'function') target? functionopts? fixes 'where' clauses
-    ;
-    clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
+    equations: (thmdecl? prop + '|')
     ;
     functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
     ;
@@ -550,6 +548,71 @@
   \end{description}
 *}
 
+subsection {* Functions with explicit partiality *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{command_def (HOL) "partial_function"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{attribute_def (HOL) "partial_function_mono"} & : & @{text attribute} \\
+  \end{matharray}
+
+  \begin{rail}
+    'partial_function' target? '(' mode ')' fixes \\ 'where' thmdecl? prop
+  \end{rail}
+
+  \begin{description}
+
+  \item @{command (HOL) "partial_function"} defines recursive
+  functions based on fixpoints in complete partial orders. No
+  termination proof is required from the user or constructed
+  internally. Instead, the possibility of non-termination is modelled
+  explicitly in the result type, which contains an explicit bottom
+  element.
+
+  Pattern matching and mutual recursion are currently not supported.
+  Thus, the specification consists of a single function described by a
+  single recursive equation.
+
+  There are no fixed syntactic restrictions on the body of the
+  function, but the induced functional must be provably monotonic
+  wrt.\ the underlying order.  The monotonicitity proof is performed
+  internally, and the definition is rejected when it fails. The proof
+  can be influenced by declaring hints using the
+  @{attribute (HOL) partial_function_mono} attribute.
+
+  The mandatory @{text mode} argument specifies the mode of operation
+  of the command, which directly corresponds to a complete partial
+  order on the result type. By default, the following modes are
+  defined: 
+
+  \begin{description}
+  \item @{text option} defines functions that map into the @{type
+  option} type. Here, the value @{term None} is used to model a
+  non-terminating computation. Monotonicity requires that if @{term
+  None} is returned by a recursive call, then the overall result
+  must also be @{term None}. This is best achieved through the use of
+  the monadic operator @{const "Option.bind"}.
+  
+  \item @{text tailrec} defines functions with an arbitrary result
+  type and uses the slightly degenerated partial order where @{term
+  "undefined"} is the bottom element.  Now, monotonicity requires that
+  if @{term undefined} is returned by a recursive call, then the
+  overall result must also be @{term undefined}. In practice, this is
+  only satisfied when each recursive call is a tail call, whose result
+  is directly returned. Thus, this mode of operation allows the
+  definition of arbitrary tail-recursive functions.
+  \end{description}
+
+  Experienced users may define new modes by instantiating the locale
+  @{const "partial_function_definitions"} appropriately.
+
+  \item @{attribute (HOL) partial_function_mono} declares rules for
+  use in the internal monononicity proofs of partial function
+  definitions.
+
+  \end{description}
+
+*}
 
 subsection {* Old-style recursive function definitions (TFL) *}
 
diff -r 00152d17855b -r 7ecfa9beef91 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Oct 26 12:17:19 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Oct 26 12:23:39 2010 +0200
@@ -411,11 +411,9 @@
   \begin{rail}
     'primrec' target? fixes 'where' equations
     ;
-    equations: (thmdecl? prop + '|')
+    ('fun' | 'function') target? functionopts? fixes \\ 'where' equations
     ;
-    ('fun' | 'function') target? functionopts? fixes 'where' clauses
-    ;
-    clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
+    equations: (thmdecl? prop + '|')
     ;
     functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
     ;
@@ -560,6 +558,71 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsubsection{Functions with explicit partiality%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{HOL}{command}{partial\_function}\hypertarget{command.HOL.partial-function}{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isacharunderscore}function}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
+    \indexdef{HOL}{attribute}{partial\_function\_mono}\hypertarget{attribute.HOL.partial-function-mono}{\hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isacharunderscore}function{\isacharunderscore}mono}}}} & : & \isa{attribute} \\
+  \end{matharray}
+
+  \begin{rail}
+    'partial_function' target? '(' mode ')' fixes \\ 'where' thmdecl? prop
+  \end{rail}
+
+  \begin{description}
+
+  \item \hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isacharunderscore}function}}}} defines recursive
+  functions based on fixpoints in complete partial orders. No
+  termination proof is required from the user or constructed
+  internally. Instead, the possibility of non-termination is modelled
+  explicitly in the result type, which contains an explicit bottom
+  element.
+
+  Pattern matching and mutual recursion are currently not supported.
+  Thus, the specification consists of a single function described by a
+  single recursive equation.
+
+  There are no fixed syntactic restrictions on the body of the
+  function, but the induced functional must be provably monotonic
+  wrt.\ the underlying order.  The monotonicitity proof is performed
+  internally, and the definition is rejected when it fails. The proof
+  can be influenced by declaring hints using the
+  \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isacharunderscore}function{\isacharunderscore}mono}}} attribute.
+
+  The mandatory \isa{mode} argument specifies the mode of operation
+  of the command, which directly corresponds to a complete partial
+  order on the result type. By default, the following modes are
+  defined: 
+
+  \begin{description}
+  \item \isa{option} defines functions that map into the \isa{option} type. Here, the value \isa{None} is used to model a
+  non-terminating computation. Monotonicity requires that if \isa{None} is returned by a recursive call, then the overall result
+  must also be \isa{None}. This is best achieved through the use of
+  the monadic operator \isa{{\isachardoublequote}Option{\isachardot}bind{\isachardoublequote}}.
+  
+  \item \isa{tailrec} defines functions with an arbitrary result
+  type and uses the slightly degenerated partial order where \isa{{\isachardoublequote}undefined{\isachardoublequote}} is the bottom element.  Now, monotonicity requires that
+  if \isa{undefined} is returned by a recursive call, then the
+  overall result must also be \isa{undefined}. In practice, this is
+  only satisfied when each recursive call is a tail call, whose result
+  is directly returned. Thus, this mode of operation allows the
+  definition of arbitrary tail-recursive functions.
+  \end{description}
+
+  Experienced users may define new modes by instantiating the locale
+  \isa{{\isachardoublequote}partial{\isacharunderscore}function{\isacharunderscore}definitions{\isachardoublequote}} appropriately.
+
+  \item \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isacharunderscore}function{\isacharunderscore}mono}}} declares rules for
+  use in the internal monononicity proofs of partial function
+  definitions.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsubsection{Old-style recursive function definitions (TFL)%
 }
 \isamarkuptrue%
diff -r 00152d17855b -r 7ecfa9beef91 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Oct 26 12:17:19 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Oct 26 12:23:39 2010 +0200
@@ -594,6 +594,75 @@
 *}
 
 
+section {* Partial function definition setup *}
+
+definition "Heap_ord = img_ord execute (fun_ord option_ord)"
+definition "Heap_lub = img_lub execute Heap (fun_lub (flat_lub None))"
+
+interpretation heap!:
+  partial_function_definitions Heap_ord Heap_lub
+unfolding Heap_ord_def Heap_lub_def
+apply (rule partial_function_image)
+apply (rule partial_function_lift)
+apply (rule flat_interpretation)
+by (auto intro: Heap_eqI)
+
+abbreviation "mono_Heap \<equiv> monotone (fun_ord Heap_ord) Heap_ord"
+
+lemma Heap_ordI:
+  assumes "\<And>h. execute x h = None \<or> execute x h = execute y h"
+  shows "Heap_ord x y"
+using assms unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def
+by blast
+
+lemma Heap_ordE:
+  assumes "Heap_ord x y"
+  obtains "execute x h = None" | "execute x h = execute y h"
+using assms unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def
+by atomize_elim blast
+
+
+lemma bind_mono[partial_function_mono]:
+assumes mf: "mono_Heap B" and mg: "\<And>y. mono_Heap (\<lambda>f. C y f)"
+shows "mono_Heap (\<lambda>f. B f \<guillemotright>= (\<lambda>y. C y f))"
+proof (rule monotoneI)
+  fix f g :: "'a \<Rightarrow> 'b Heap" assume fg: "fun_ord Heap_ord f g"
+  from mf
+  have 1: "Heap_ord (B f) (B g)" by (rule monotoneD) (rule fg)
+  from mg
+  have 2: "\<And>y'. Heap_ord (C y' f) (C y' g)" by (rule monotoneD) (rule fg)
+
+  have "Heap_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y. C y f))"
+    (is "Heap_ord ?L ?R")
+  proof (rule Heap_ordI)
+    fix h
+    from 1 show "execute ?L h = None \<or> execute ?L h = execute ?R h"
+      by (rule Heap_ordE[where h = h]) (auto simp: execute_bind_case)
+  qed
+  also
+  have "Heap_ord (B g \<guillemotright>= (\<lambda>y'. C y' f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))"
+    (is "Heap_ord ?L ?R")
+  proof (rule Heap_ordI)
+    fix h
+    show "execute ?L h = None \<or> execute ?L h = execute ?R h"
+    proof (cases "execute (B g) h")
+      case None
+      then have "execute ?L h = None" by (auto simp: execute_bind_case)
+      thus ?thesis ..
+    next
+      case Some
+      then obtain r h' where "execute (B g) h = Some (r, h')"
+        by (metis surjective_pairing)
+      then have "execute ?L h = execute (C r f) h'"
+        "execute ?R h = execute (C r g) h'"
+        by (auto simp: execute_bind_case)
+      with 2[of r] show ?thesis by (auto elim: Heap_ordE)
+    qed
+  qed
+  finally (heap.leq_trans)
+  show "Heap_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))" .
+qed
+
 hide_const (open) Heap heap guard raise' fold_map
 
 end
diff -r 00152d17855b -r 7ecfa9beef91 src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Oct 26 12:17:19 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Oct 26 12:23:39 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)
diff -r 00152d17855b -r 7ecfa9beef91 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Tue Oct 26 12:17:19 2010 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Oct 26 12:23:39 2010 +0200
@@ -218,7 +218,8 @@
     lthy'
     |> Local_Theory.note (eq_abinding, [rec_rule])
     |-> (fn (_, rec') =>
-      Local_Theory.note ((Binding.qualify true fname (Binding.name "rec"), []), rec'))
+      Spec_Rules.add Spec_Rules.Equational ([f], [rec'])
+      |> Local_Theory.note ((Binding.qualify true fname (Binding.name "simps"), []), rec'))
     |> snd
   end;
 
diff -r 00152d17855b -r 7ecfa9beef91 src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Tue Oct 26 12:17:19 2010 +0200
+++ b/src/HOL/ex/Fundefs.thy	Tue Oct 26 12:23:39 2010 +0200
@@ -222,7 +222,7 @@
      then do { ns \<leftarrow> collatz (n div 2); Some (n # ns) }
      else do { ns \<leftarrow> collatz (3 * n + 1);  Some (n # ns)})"
 
-declare collatz.rec[code]
+declare collatz.simps[code]
 value "collatz 23"
 
 
diff -r 00152d17855b -r 7ecfa9beef91 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Tue Oct 26 12:17:19 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Tue Oct 26 12:23:39 2010 +0200
@@ -480,9 +480,9 @@
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
     val (algebra', eqngr') = obtain false thy consts [t'];
-    val result = evaluator algebra' eqngr' vs' t';
   in
-    evaluator algebra' eqngr' vs' t'
+    t'
+    |> evaluator algebra' eqngr' vs'
     |> postproc (postprocess_term thy o resubst)
   end;