--- 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) *}
--- 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%
--- 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
--- 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)
--- 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;
--- 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"
--- 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;