summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/IsarRef/Thy/HOL_Specific.thy

changeset 40171 | 1fa547166a1d |

parent 40170 | 751121d5ca35 |

child 40245 | 59f011c1877a |

1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Oct 26 12:19:01 2010 +0200 1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Oct 26 12:19:01 2010 +0200 1.3 @@ -548,6 +548,71 @@ 1.4 \end{description} 1.5 *} 1.6 1.7 +subsection {* Functions with explicit partiality *} 1.8 + 1.9 +text {* 1.10 + \begin{matharray}{rcl} 1.11 + @{command_def (HOL) "partial_function"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ 1.12 + @{attribute_def (HOL) "partial_function_mono"} & : & @{text attribute} \\ 1.13 + \end{matharray} 1.14 + 1.15 + \begin{rail} 1.16 + 'partial_function' target? '(' mode ')' fixes \\ 'where' thmdecl? prop 1.17 + \end{rail} 1.18 + 1.19 + \begin{description} 1.20 + 1.21 + \item @{command (HOL) "partial_function"} defines recursive 1.22 + functions based on fixpoints in complete partial orders. No 1.23 + termination proof is required from the user or constructed 1.24 + internally. Instead, the possibility of non-termination is modelled 1.25 + explicitly in the result type, which contains an explicit bottom 1.26 + element. 1.27 + 1.28 + Pattern matching and mutual recursion are currently not supported. 1.29 + Thus, the specification consists of a single function described by a 1.30 + single recursive equation. 1.31 + 1.32 + There are no fixed syntactic restrictions on the body of the 1.33 + function, but the induced functional must be provably monotonic 1.34 + wrt.\ the underlying order. The monotonicitity proof is performed 1.35 + internally, and the definition is rejected when it fails. The proof 1.36 + can be influenced by declaring hints using the 1.37 + @{attribute (HOL) partial_function_mono} attribute. 1.38 + 1.39 + The mandatory @{text mode} argument specifies the mode of operation 1.40 + of the command, which directly corresponds to a complete partial 1.41 + order on the result type. By default, the following modes are 1.42 + defined: 1.43 + 1.44 + \begin{description} 1.45 + \item @{text option} defines functions that map into the @{type 1.46 + option} type. Here, the value @{term None} is used to model a 1.47 + non-terminating computation. Monotonicity requires that if @{term 1.48 + None} is returned by a recursive call, then the overall result 1.49 + must also be @{term None}. This is best achieved through the use of 1.50 + the monadic operator @{const "Option.bind"}. 1.51 + 1.52 + \item @{text tailrec} defines functions with an arbitrary result 1.53 + type and uses the slightly degenerated partial order where @{term 1.54 + "undefined"} is the bottom element. Now, monotonicity requires that 1.55 + if @{term undefined} is returned by a recursive call, then the 1.56 + overall result must also be @{term undefined}. In practice, this is 1.57 + only satisfied when each recursive call is a tail call, whose result 1.58 + is directly returned. Thus, this mode of operation allows the 1.59 + definition of arbitrary tail-recursive functions. 1.60 + \end{description} 1.61 + 1.62 + Experienced users may define new modes by instantiating the locale 1.63 + @{const "partial_function_definitions"} appropriately. 1.64 + 1.65 + \item @{attribute (HOL) partial_function_mono} declares rules for 1.66 + use in the internal monononicity proofs of partial function 1.67 + definitions. 1.68 + 1.69 + \end{description} 1.70 + 1.71 +*} 1.72 1.73 subsection {* Old-style recursive function definitions (TFL) *} 1.74