author | wenzelm |
Wed, 07 May 2008 13:38:15 +0200 | |
changeset 26845 | d86eb226ecba |
parent 26840 | ec46381f149d |
child 26852 | a31203f58b20 |
permissions | -rw-r--r-- |
wenzelm@26840 | 1 |
(* $Id$ *) |
wenzelm@26840 | 2 |
|
wenzelm@26840 | 3 |
theory ZF_Specific |
wenzelm@26840 | 4 |
imports ZF |
wenzelm@26840 | 5 |
begin |
wenzelm@26840 | 6 |
|
wenzelm@26845 | 7 |
chapter {* ZF specific elements *} |
wenzelm@26845 | 8 |
|
wenzelm@26845 | 9 |
section {* Type checking *} |
wenzelm@26845 | 10 |
|
wenzelm@26845 | 11 |
text {* |
wenzelm@26845 | 12 |
The ZF logic is essentially untyped, so the concept of ``type |
wenzelm@26845 | 13 |
checking'' is performed as logical reasoning about set-membership |
wenzelm@26845 | 14 |
statements. A special method assists users in this task; a version |
wenzelm@26845 | 15 |
of this is already declared as a ``solver'' in the standard |
wenzelm@26845 | 16 |
Simplifier setup. |
wenzelm@26845 | 17 |
|
wenzelm@26845 | 18 |
\begin{matharray}{rcl} |
wenzelm@26845 | 19 |
@{command_def (ZF) "print_tcset"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\ |
wenzelm@26845 | 20 |
@{method_def (ZF) typecheck} & : & \isarmeth \\ |
wenzelm@26845 | 21 |
@{attribute_def (ZF) TC} & : & \isaratt \\ |
wenzelm@26845 | 22 |
\end{matharray} |
wenzelm@26845 | 23 |
|
wenzelm@26845 | 24 |
\begin{rail} |
wenzelm@26845 | 25 |
'TC' (() | 'add' | 'del') |
wenzelm@26845 | 26 |
; |
wenzelm@26845 | 27 |
\end{rail} |
wenzelm@26845 | 28 |
|
wenzelm@26845 | 29 |
\begin{descr} |
wenzelm@26845 | 30 |
|
wenzelm@26845 | 31 |
\item [@{command (ZF) "print_tcset"}] prints the collection of |
wenzelm@26845 | 32 |
typechecking rules of the current context. |
wenzelm@26845 | 33 |
|
wenzelm@26845 | 34 |
\item [@{method (ZF) typecheck}] attempts to solve any pending |
wenzelm@26845 | 35 |
type-checking problems in subgoals. |
wenzelm@26845 | 36 |
|
wenzelm@26845 | 37 |
\item [@{attribute (ZF) TC}] adds or deletes type-checking rules |
wenzelm@26845 | 38 |
from the context. |
wenzelm@26845 | 39 |
|
wenzelm@26845 | 40 |
\end{descr} |
wenzelm@26845 | 41 |
*} |
wenzelm@26845 | 42 |
|
wenzelm@26845 | 43 |
|
wenzelm@26845 | 44 |
section {* (Co)Inductive sets and datatypes *} |
wenzelm@26845 | 45 |
|
wenzelm@26845 | 46 |
subsection {* Set definitions *} |
wenzelm@26845 | 47 |
|
wenzelm@26845 | 48 |
text {* |
wenzelm@26845 | 49 |
In ZF everything is a set. The generic inductive package also |
wenzelm@26845 | 50 |
provides a specific view for ``datatype'' specifications. |
wenzelm@26845 | 51 |
Coinductive definitions are available in both cases, too. |
wenzelm@26845 | 52 |
|
wenzelm@26845 | 53 |
\begin{matharray}{rcl} |
wenzelm@26845 | 54 |
@{command_def (ZF) "inductive"} & : & \isartrans{theory}{theory} \\ |
wenzelm@26845 | 55 |
@{command_def (ZF) "coinductive"} & : & \isartrans{theory}{theory} \\ |
wenzelm@26845 | 56 |
@{command_def (ZF) "datatype"} & : & \isartrans{theory}{theory} \\ |
wenzelm@26845 | 57 |
@{command_def (ZF) "codatatype"} & : & \isartrans{theory}{theory} \\ |
wenzelm@26845 | 58 |
\end{matharray} |
wenzelm@26845 | 59 |
|
wenzelm@26845 | 60 |
\begin{rail} |
wenzelm@26845 | 61 |
('inductive' | 'coinductive') domains intros hints |
wenzelm@26845 | 62 |
; |
wenzelm@26845 | 63 |
|
wenzelm@26845 | 64 |
domains: 'domains' (term + '+') ('<=' | subseteq) term |
wenzelm@26845 | 65 |
; |
wenzelm@26845 | 66 |
intros: 'intros' (thmdecl? prop +) |
wenzelm@26845 | 67 |
; |
wenzelm@26845 | 68 |
hints: monos? condefs? typeintros? typeelims? |
wenzelm@26845 | 69 |
; |
wenzelm@26845 | 70 |
monos: ('monos' thmrefs)? |
wenzelm@26845 | 71 |
; |
wenzelm@26845 | 72 |
condefs: ('con\_defs' thmrefs)? |
wenzelm@26845 | 73 |
; |
wenzelm@26845 | 74 |
typeintros: ('type\_intros' thmrefs)? |
wenzelm@26845 | 75 |
; |
wenzelm@26845 | 76 |
typeelims: ('type\_elims' thmrefs)? |
wenzelm@26845 | 77 |
; |
wenzelm@26845 | 78 |
\end{rail} |
wenzelm@26845 | 79 |
|
wenzelm@26845 | 80 |
In the following syntax specification @{text "monos"}, @{text |
wenzelm@26845 | 81 |
typeintros}, and @{text typeelims} are the same as above. |
wenzelm@26845 | 82 |
|
wenzelm@26845 | 83 |
\begin{rail} |
wenzelm@26845 | 84 |
('datatype' | 'codatatype') domain? (dtspec + 'and') hints |
wenzelm@26845 | 85 |
; |
wenzelm@26845 | 86 |
|
wenzelm@26845 | 87 |
domain: ('<=' | subseteq) term |
wenzelm@26845 | 88 |
; |
wenzelm@26845 | 89 |
dtspec: term '=' (con + '|') |
wenzelm@26845 | 90 |
; |
wenzelm@26845 | 91 |
con: name ('(' (term ',' +) ')')? |
wenzelm@26845 | 92 |
; |
wenzelm@26845 | 93 |
hints: monos? typeintros? typeelims? |
wenzelm@26845 | 94 |
; |
wenzelm@26845 | 95 |
\end{rail} |
wenzelm@26845 | 96 |
|
wenzelm@26845 | 97 |
See \cite{isabelle-ZF} for further information on inductive |
wenzelm@26845 | 98 |
definitions in ZF, but note that this covers the old-style theory |
wenzelm@26845 | 99 |
format. |
wenzelm@26845 | 100 |
*} |
wenzelm@26845 | 101 |
|
wenzelm@26845 | 102 |
|
wenzelm@26845 | 103 |
subsection {* Primitive recursive functions *} |
wenzelm@26845 | 104 |
|
wenzelm@26845 | 105 |
text {* |
wenzelm@26845 | 106 |
\begin{matharray}{rcl} |
wenzelm@26845 | 107 |
@{command_def (ZF) "primrec"} & : & \isartrans{theory}{theory} \\ |
wenzelm@26845 | 108 |
\end{matharray} |
wenzelm@26845 | 109 |
|
wenzelm@26845 | 110 |
\begin{rail} |
wenzelm@26845 | 111 |
'primrec' (thmdecl? prop +) |
wenzelm@26845 | 112 |
; |
wenzelm@26845 | 113 |
\end{rail} |
wenzelm@26845 | 114 |
*} |
wenzelm@26845 | 115 |
|
wenzelm@26845 | 116 |
|
wenzelm@26845 | 117 |
subsection {* Cases and induction: emulating tactic scripts *} |
wenzelm@26845 | 118 |
|
wenzelm@26845 | 119 |
text {* |
wenzelm@26845 | 120 |
The following important tactical tools of Isabelle/ZF have been |
wenzelm@26845 | 121 |
ported to Isar. These should not be used in proper proof texts. |
wenzelm@26845 | 122 |
|
wenzelm@26845 | 123 |
\begin{matharray}{rcl} |
wenzelm@26845 | 124 |
@{method_def (ZF) case_tac}@{text "\<^sup>*"} & : & \isarmeth \\ |
wenzelm@26845 | 125 |
@{method_def (ZF) induct_tac}@{text "\<^sup>*"} & : & \isarmeth \\ |
wenzelm@26845 | 126 |
@{method_def (ZF) ind_cases}@{text "\<^sup>*"} & : & \isarmeth \\ |
wenzelm@26845 | 127 |
@{command_def (ZF) "inductive_cases"} & : & \isartrans{theory}{theory} \\ |
wenzelm@26845 | 128 |
\end{matharray} |
wenzelm@26845 | 129 |
|
wenzelm@26845 | 130 |
\begin{rail} |
wenzelm@26845 | 131 |
('case\_tac' | 'induct\_tac') goalspec? name |
wenzelm@26845 | 132 |
; |
wenzelm@26845 | 133 |
indcases (prop +) |
wenzelm@26845 | 134 |
; |
wenzelm@26845 | 135 |
inductivecases (thmdecl? (prop +) + 'and') |
wenzelm@26845 | 136 |
; |
wenzelm@26845 | 137 |
\end{rail} |
wenzelm@26845 | 138 |
*} |
wenzelm@26845 | 139 |
|
wenzelm@26840 | 140 |
end |