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

doc-src/IsarRef/Thy/HOL_Specific.thy

changeset 27045 | 4e7ecec1b685 |

parent 27041 | 22dcf2fc0aa2 |

child 27103 | d8549f4d900b |

1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Jun 02 23:11:24 2008 +0200 1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Jun 02 23:11:51 2008 +0200 1.3 @@ -614,55 +614,6 @@ 1.4 *} 1.5 1.6 1.7 -section {* Definition by specification \label{sec:hol-specification} *} 1.8 - 1.9 -text {* 1.10 - \begin{matharray}{rcl} 1.11 - @{command_def (HOL) "specification"} & : & \isartrans{theory}{proof(prove)} \\ 1.12 - @{command_def (HOL) "ax_specification"} & : & \isartrans{theory}{proof(prove)} \\ 1.13 - \end{matharray} 1.14 - 1.15 - \begin{rail} 1.16 - ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +) 1.17 - ; 1.18 - decl: ((name ':')? term '(' 'overloaded' ')'?) 1.19 - \end{rail} 1.20 - 1.21 - \begin{descr} 1.22 - 1.23 - \item [@{command (HOL) "specification"}~@{text "decls \<phi>"}] sets up a 1.24 - goal stating the existence of terms with the properties specified to 1.25 - hold for the constants given in @{text decls}. After finishing the 1.26 - proof, the theory will be augmented with definitions for the given 1.27 - constants, as well as with theorems stating the properties for these 1.28 - constants. 1.29 - 1.30 - \item [@{command (HOL) "ax_specification"}~@{text "decls \<phi>"}] sets 1.31 - up a goal stating the existence of terms with the properties 1.32 - specified to hold for the constants given in @{text decls}. After 1.33 - finishing the proof, the theory will be augmented with axioms 1.34 - expressing the properties given in the first place. 1.35 - 1.36 - \item [@{text decl}] declares a constant to be defined by the 1.37 - specification given. The definition for the constant @{text c} is 1.38 - bound to the name @{text c_def} unless a theorem name is given in 1.39 - the declaration. Overloaded constants should be declared as such. 1.40 - 1.41 - \end{descr} 1.42 - 1.43 - Whether to use @{command (HOL) "specification"} or @{command (HOL) 1.44 - "ax_specification"} is to some extent a matter of style. @{command 1.45 - (HOL) "specification"} introduces no new axioms, and so by 1.46 - construction cannot introduce inconsistencies, whereas @{command 1.47 - (HOL) "ax_specification"} does introduce axioms, but only after the 1.48 - user has explicitly proven it to be safe. A practical issue must be 1.49 - considered, though: After introducing two constants with the same 1.50 - properties using @{command (HOL) "specification"}, one can prove 1.51 - that the two constants are, in fact, equal. If this might be a 1.52 - problem, one should use @{command (HOL) "ax_specification"}. 1.53 -*} 1.54 - 1.55 - 1.56 section {* Inductive and coinductive definitions \label{sec:hol-inductive} *} 1.57 1.58 text {* 1.59 @@ -1139,4 +1090,53 @@ 1.60 \end{descr} 1.61 *} 1.62 1.63 + 1.64 +section {* Definition by specification \label{sec:hol-specification} *} 1.65 + 1.66 +text {* 1.67 + \begin{matharray}{rcl} 1.68 + @{command_def (HOL) "specification"} & : & \isartrans{theory}{proof(prove)} \\ 1.69 + @{command_def (HOL) "ax_specification"} & : & \isartrans{theory}{proof(prove)} \\ 1.70 + \end{matharray} 1.71 + 1.72 + \begin{rail} 1.73 + ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +) 1.74 + ; 1.75 + decl: ((name ':')? term '(' 'overloaded' ')'?) 1.76 + \end{rail} 1.77 + 1.78 + \begin{descr} 1.79 + 1.80 + \item [@{command (HOL) "specification"}~@{text "decls \<phi>"}] sets up a 1.81 + goal stating the existence of terms with the properties specified to 1.82 + hold for the constants given in @{text decls}. After finishing the 1.83 + proof, the theory will be augmented with definitions for the given 1.84 + constants, as well as with theorems stating the properties for these 1.85 + constants. 1.86 + 1.87 + \item [@{command (HOL) "ax_specification"}~@{text "decls \<phi>"}] sets 1.88 + up a goal stating the existence of terms with the properties 1.89 + specified to hold for the constants given in @{text decls}. After 1.90 + finishing the proof, the theory will be augmented with axioms 1.91 + expressing the properties given in the first place. 1.92 + 1.93 + \item [@{text decl}] declares a constant to be defined by the 1.94 + specification given. The definition for the constant @{text c} is 1.95 + bound to the name @{text c_def} unless a theorem name is given in 1.96 + the declaration. Overloaded constants should be declared as such. 1.97 + 1.98 + \end{descr} 1.99 + 1.100 + Whether to use @{command (HOL) "specification"} or @{command (HOL) 1.101 + "ax_specification"} is to some extent a matter of style. @{command 1.102 + (HOL) "specification"} introduces no new axioms, and so by 1.103 + construction cannot introduce inconsistencies, whereas @{command 1.104 + (HOL) "ax_specification"} does introduce axioms, but only after the 1.105 + user has explicitly proven it to be safe. A practical issue must be 1.106 + considered, though: After introducing two constants with the same 1.107 + properties using @{command (HOL) "specification"}, one can prove 1.108 + that the two constants are, in fact, equal. If this might be a 1.109 + problem, one should use @{command (HOL) "ax_specification"}. 1.110 +*} 1.111 + 1.112 end