summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 02 Jun 2008 23:11:51 +0200 | |

changeset 27045 | 4e7ecec1b685 |

parent 27044 | c4eaa7140532 |

child 27046 | 51c2635dd89c |

moved (ax_)specification to end;

--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Jun 02 23:11:24 2008 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Jun 02 23:11:51 2008 +0200 @@ -614,55 +614,6 @@ *} -section {* Definition by specification \label{sec:hol-specification} *} - -text {* - \begin{matharray}{rcl} - @{command_def (HOL) "specification"} & : & \isartrans{theory}{proof(prove)} \\ - @{command_def (HOL) "ax_specification"} & : & \isartrans{theory}{proof(prove)} \\ - \end{matharray} - - \begin{rail} - ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +) - ; - decl: ((name ':')? term '(' 'overloaded' ')'?) - \end{rail} - - \begin{descr} - - \item [@{command (HOL) "specification"}~@{text "decls \<phi>"}] sets up a - goal stating the existence of terms with the properties specified to - hold for the constants given in @{text decls}. After finishing the - proof, the theory will be augmented with definitions for the given - constants, as well as with theorems stating the properties for these - constants. - - \item [@{command (HOL) "ax_specification"}~@{text "decls \<phi>"}] sets - up a goal stating the existence of terms with the properties - specified to hold for the constants given in @{text decls}. After - finishing the proof, the theory will be augmented with axioms - expressing the properties given in the first place. - - \item [@{text decl}] declares a constant to be defined by the - specification given. The definition for the constant @{text c} is - bound to the name @{text c_def} unless a theorem name is given in - the declaration. Overloaded constants should be declared as such. - - \end{descr} - - Whether to use @{command (HOL) "specification"} or @{command (HOL) - "ax_specification"} is to some extent a matter of style. @{command - (HOL) "specification"} introduces no new axioms, and so by - construction cannot introduce inconsistencies, whereas @{command - (HOL) "ax_specification"} does introduce axioms, but only after the - user has explicitly proven it to be safe. A practical issue must be - considered, though: After introducing two constants with the same - properties using @{command (HOL) "specification"}, one can prove - that the two constants are, in fact, equal. If this might be a - problem, one should use @{command (HOL) "ax_specification"}. -*} - - section {* Inductive and coinductive definitions \label{sec:hol-inductive} *} text {* @@ -1139,4 +1090,53 @@ \end{descr} *} + +section {* Definition by specification \label{sec:hol-specification} *} + +text {* + \begin{matharray}{rcl} + @{command_def (HOL) "specification"} & : & \isartrans{theory}{proof(prove)} \\ + @{command_def (HOL) "ax_specification"} & : & \isartrans{theory}{proof(prove)} \\ + \end{matharray} + + \begin{rail} + ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +) + ; + decl: ((name ':')? term '(' 'overloaded' ')'?) + \end{rail} + + \begin{descr} + + \item [@{command (HOL) "specification"}~@{text "decls \<phi>"}] sets up a + goal stating the existence of terms with the properties specified to + hold for the constants given in @{text decls}. After finishing the + proof, the theory will be augmented with definitions for the given + constants, as well as with theorems stating the properties for these + constants. + + \item [@{command (HOL) "ax_specification"}~@{text "decls \<phi>"}] sets + up a goal stating the existence of terms with the properties + specified to hold for the constants given in @{text decls}. After + finishing the proof, the theory will be augmented with axioms + expressing the properties given in the first place. + + \item [@{text decl}] declares a constant to be defined by the + specification given. The definition for the constant @{text c} is + bound to the name @{text c_def} unless a theorem name is given in + the declaration. Overloaded constants should be declared as such. + + \end{descr} + + Whether to use @{command (HOL) "specification"} or @{command (HOL) + "ax_specification"} is to some extent a matter of style. @{command + (HOL) "specification"} introduces no new axioms, and so by + construction cannot introduce inconsistencies, whereas @{command + (HOL) "ax_specification"} does introduce axioms, but only after the + user has explicitly proven it to be safe. A practical issue must be + considered, though: After introducing two constants with the same + properties using @{command (HOL) "specification"}, one can prove + that the two constants are, in fact, equal. If this might be a + problem, one should use @{command (HOL) "ax_specification"}. +*} + end