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

doc-src/IsarRef/logics.tex

changeset 13041 | 6faccf7d0f25 |

parent 13039 | cfcc1f6f21df |

child 13042 | d8a345d9e067 |

1.1 --- a/doc-src/IsarRef/logics.tex Thu Mar 07 19:04:00 2002 +0100 1.2 +++ b/doc-src/IsarRef/logics.tex Thu Mar 07 22:52:07 2002 +0100 1.3 @@ -18,11 +18,13 @@ 1.4 The very starting point for any Isabelle object-logic is a ``truth judgment'' 1.5 that links object-level statements to the meta-logic (with its minimal 1.6 language of $prop$ that covers universal quantification $\Forall$ and 1.7 -implication $\Imp$). Common object-logics are sufficiently expressive to 1.8 -\emph{internalize} rule statements over $\Forall$ and $\Imp$ within their own 1.9 -language. This is useful in certain situations where a rule needs to be 1.10 -viewed as an atomic statement from the meta-level perspective (e.g.\ $\All x x 1.11 -\in A \Imp P(x)$ versus $\forall x \in A. P(x)$). 1.12 +implication $\Imp$). 1.13 + 1.14 +Common object-logics are sufficiently expressive to internalize rule 1.15 +statements over $\Forall$ and $\Imp$ within their own language. This is 1.16 +useful in certain situations where a rule needs to be viewed as an atomic 1.17 +statement from the meta-level perspective, e.g.\ $\All x x \in A \Imp P(x)$ 1.18 +versus $\forall x \in A. P(x)$. 1.19 1.20 From the following language elements, only the $atomize$ method and 1.21 $rule_format$ attribute are occasionally required by end-users, the rest is 1.22 @@ -31,34 +33,36 @@ 1.23 realistic examples. 1.24 1.25 Generic tools may refer to the information provided by object-logic 1.26 -declarations internally (e.g.\ locales \S\ref{sec:locale}, or the Classical 1.27 -Reasoner \S\ref{sec:classical}). 1.28 +declarations internally. 1.29 + 1.30 +\railalias{ruleformat}{rule\_format} 1.31 +\railterm{ruleformat} 1.32 1.33 \begin{rail} 1.34 'judgment' constdecl 1.35 ; 1.36 - atomize ('(' 'full' ')')? 1.37 + 'atomize' ('(' 'full' ')')? 1.38 ; 1.39 ruleformat ('(' 'noasm' ')')? 1.40 ; 1.41 \end{rail} 1.42 1.43 \begin{descr} 1.44 - 1.45 -\item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the 1.46 + 1.47 +\item [$\isarkeyword{judgment}~c::\sigma~~(mx)$] declares constant $c$ as the 1.48 truth judgment of the current object-logic. Its type $\sigma$ should 1.49 specify a coercion of the category of object-level propositions to $prop$ of 1.50 - the Pure meta-logic; the mixfix annotation $syn$ would typically just link 1.51 + the Pure meta-logic; the mixfix annotation $(mx)$ would typically just link 1.52 the object language (internally of syntactic category $logic$) with that of 1.53 $prop$. Only one $\isarkeyword{judgment}$ declaration may be given in any 1.54 theory development. 1.55 - 1.56 + 1.57 \item [$atomize$] (as a method) rewrites any non-atomic premises of a 1.58 sub-goal, using the meta-level equations declared via $atomize$ (as an 1.59 attribute) beforehand. As a result, heavily nested goals become amenable to 1.60 fundamental operations such as resolution (cf.\ the $rule$ method) and 1.61 proof-by-assumption (cf.\ $assumption$). Giving the ``$(full)$'' option 1.62 - here means to turn the subgoal into an object-statement (if possible), 1.63 + here means to turn the whole subgoal into an object-statement (if possible), 1.64 including the outermost parameters and assumptions as well. 1.65 1.66 A typical collection of $atomize$ rules for a particular object-logic would 1.67 @@ -106,7 +110,7 @@ 1.68 1.69 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original 1.70 $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but 1.71 - also declares type arity $t :: (term, \dots, term) term$, making $t$ an 1.72 + also declares type arity $t :: (type, \dots, type) type$, making $t$ an 1.73 actual HOL type constructor. 1.74 1.75 \item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating 1.76 @@ -120,21 +124,22 @@ 1.77 $Abs_t$ (this may be changed via an explicit $\isarkeyword{morphisms}$ 1.78 declaration). 1.79 1.80 - Theorems $Rep_t$, $Rep_inverse$, and $Abs_inverse$ provide the most basic 1.81 - characterization as a corresponding injection/surjection pair (in both 1.82 + Theorems $Rep_t$, $Rep_t_inverse$, and $Abs_t_inverse$ provide the most 1.83 + basic characterization as a corresponding injection/surjection pair (in both 1.84 directions). Rules $Rep_t_inject$ and $Abs_t_inject$ provide a slightly 1.85 - more comfortable view on the injectivity part, suitable for automated proof 1.86 - tools (e.g.\ in $simp$ or $iff$ declarations). Rules $Rep_t_cases$, 1.87 - $Rep_t_induct$, and $Abs_t_cases$, $Abs_t_induct$ provide alternative views 1.88 - on surjectivity; these are already declared as type or set rules for the 1.89 - generic $cases$ and $induct$ methods. 1.90 + more convenient view on the injectivity part, suitable for automated proof 1.91 + tools (e.g.\ in $simp$ or $iff$ declarations). Rules 1.92 + $Rep_t_cases/Rep_t_induct$, and $Abs_t_cases/Abs_t_induct$ provide 1.93 + alternative views on surjectivity; these are already declared as set or type 1.94 + rules for the generic $cases$ and $induct$ methods. 1.95 \end{descr} 1.96 1.97 -Raw type declarations are rarely used in practice; the main application is 1.98 -with experimental (or even axiomatic!) theory fragments. Instead of primitive 1.99 -HOL type definitions, user-level theories usually refer to higher-level 1.100 -packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) or 1.101 -$\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}). 1.102 +Note that raw type declarations are rarely used in practice; the main 1.103 +application is with experimental (or even axiomatic!) theory fragments. 1.104 +Instead of primitive HOL type definitions, user-level theories usually refer 1.105 +to higher-level packages such as $\isarkeyword{record}$ (see 1.106 +\S\ref{sec:hol-record}) or $\isarkeyword{datatype}$ (see 1.107 +\S\ref{sec:hol-datatype}). 1.108 1.109 1.110 \subsection{Adhoc tuples} 1.111 @@ -153,13 +158,12 @@ 1.112 \end{rail} 1.113 1.114 \begin{descr} 1.115 - 1.116 + 1.117 \item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level 1.118 tuple types into canonical form as specified by the arguments given; $\vec 1.119 - p@i$ refers to occurrences in premise $i$ of the rule. The 1.120 - $split_format~(complete)$ form causes \emph{all} arguments in function 1.121 - applications to be represented canonically according to their tuple type 1.122 - structure. 1.123 + p@i$ refers to occurrences in premise $i$ of the rule. The $(complete)$ 1.124 + option causes \emph{all} arguments in function applications to be 1.125 + represented canonically according to their tuple type structure. 1.126 1.127 Note that these operations tend to invent funny names for new local 1.128 parameters to be introduced. 1.129 @@ -169,8 +173,8 @@ 1.130 1.131 \subsection{Records}\label{sec:hol-record} 1.132 1.133 -In principle, records merely generalize the concept of tuples where components 1.134 -may be addressed by labels instead of just position. The logical 1.135 +In principle, records merely generalize the concept of tuples, where 1.136 +components may be addressed by labels instead of just position. The logical 1.137 infrastructure of records in Isabelle/HOL is slightly more advanced, though, 1.138 supporting truly extensible record schemes. This admits operations that are 1.139 polymorphic with respect to record extension, yielding ``object-oriented'' 1.140 @@ -203,8 +207,8 @@ 1.141 ``$\more$'' notation (which is actually part of the syntax). The improper 1.142 field ``$\more$'' of a record scheme is called the \emph{more part}. 1.143 Logically it is just a free variable, which is occasionally referred to as 1.144 -\emph{row variable} in the literature. The more part of a record scheme may 1.145 -be instantiated by zero or more further components. For example, the above 1.146 +``row variable'' in the literature. The more part of a record scheme may be 1.147 +instantiated by zero or more further components. For example, the previous 1.148 scheme may get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = 1.149 m'}$, where $m'$ refers to a different more part. Fixed records are special 1.150 instances of record schemes, where ``$\more$'' is properly terminated by the 1.151 @@ -295,11 +299,11 @@ 1.152 reverse than in the actual term. Since repeated updates are just function 1.153 applications, fields may be freely permuted in $\record{x \asn a\fs y \asn 1.154 b\fs z \asn c}$, as far as logical equality is concerned. Thus 1.155 -commutativity of updates can be proven within the logic for any two fields, 1.156 -but not as a general theorem: fields are not first-class values. 1.157 +commutativity of independent updates can be proven within the logic for any 1.158 +two fields, but not as a general theorem. 1.159 1.160 \medskip The \textbf{make} operation provides a cumulative record constructor 1.161 -functions: 1.162 +function: 1.163 \begin{matharray}{lll} 1.164 t{\dtt}make & \ty & \vec\sigma \To \record{\vec c \ty \vec \sigma} \\ 1.165 \end{matharray} 1.166 @@ -336,25 +340,26 @@ 1.167 \record{\vec d \ty \vec \rho, \vec c \ty \vec\sigma} \\ 1.168 \end{matharray} 1.169 1.170 -\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ are actually coincide for root records. 1.171 +\noindent Note that $t{\dtt}make$ and $t{\dtt}fields$ actually coincide for root records. 1.172 1.173 1.174 \subsubsection{Derived rules and proof tools}\label{sec:hol-record-thms} 1.175 1.176 The record package proves several results internally, declaring these facts to 1.177 appropriate proof tools. This enables users to reason about record structures 1.178 -quite comfortably. Assume that $t$ is a record type as specified above. 1.179 +quite conveniently. Assume that $t$ is a record type as specified above. 1.180 1.181 \begin{enumerate} 1.182 - 1.183 + 1.184 \item Standard conversions for selectors or updates applied to record 1.185 constructor terms are made part of the default Simplifier context; thus 1.186 proofs by reduction of basic operations merely require the $simp$ method 1.187 - without further arguments. These rules are available as $t{\dtt}simps$. 1.188 - 1.189 + without further arguments. These rules are available as $t{\dtt}simps$, 1.190 + too. 1.191 + 1.192 \item Selectors applied to updated records are automatically reduced by an 1.193 - internal simplification procedure, which is also part of the default 1.194 - Simplifier context. 1.195 + internal simplification procedure, which is also part of the standard 1.196 + Simplifier setup. 1.197 1.198 \item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x' 1.199 \conj y=y'$ are declared to the Simplifier and Classical Reasoner as $iff$ 1.200 @@ -368,10 +373,10 @@ 1.201 terms are provided both in $cases$ and $induct$ format (cf.\ the generic 1.202 proof methods of the same name, \S\ref{sec:cases-induct}). Several 1.203 variations are available, for fixed records, record schemes, more parts etc. 1.204 - 1.205 + 1.206 The generic proof methods are sufficiently smart to pick the most sensible 1.207 rule according to the type of the indicated record expression: users just 1.208 - need to apply something like ``$(cases r)$'' to a certain proof problem. 1.209 + need to apply something like ``$(cases~r)$'' to a certain proof problem. 1.210 1.211 \item The derived record operations $t{\dtt}make$, $t{\dtt}fields$, 1.212 $t{\dtt}extend$, $t{\dtt}truncate$ are \emph{not} treated automatically, but 1.213 @@ -471,7 +476,7 @@ 1.214 1.215 \item [$\isarkeyword{recdef}$] defines general well-founded recursive 1.216 functions (using the TFL package), see also \cite{isabelle-HOL}. The 1.217 - $(permissive)$ option tells TFL to recover from failed proof attempts, 1.218 + ``$(permissive)$'' option tells TFL to recover from failed proof attempts, 1.219 returning unfinished results. The $recdef_simp$, $recdef_cong$, and 1.220 $recdef_wf$ hints refer to auxiliary rules to be used in the internal 1.221 automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\ 1.222 @@ -496,8 +501,8 @@ 1.223 $\isarkeyword{recdef}$ are numbered (starting from $1$). 1.224 1.225 The equations provided by these packages may be referred later as theorem list 1.226 -$f\mathord.simps$, where $f$ is the (collective) name of the functions 1.227 -defined. Individual equations may be named explicitly as well; note that for 1.228 +$f{\dtt}simps$, where $f$ is the (collective) name of the functions defined. 1.229 +Individual equations may be named explicitly as well; note that for 1.230 $\isarkeyword{recdef}$ each specification given by the user may result in 1.231 several theorems. 1.232 1.233 @@ -631,10 +636,10 @@ 1.234 both goal addressing and dynamic instantiation. Note that named rule cases 1.235 are \emph{not} provided as would be by the proper $induct$ and $cases$ proof 1.236 methods (see \S\ref{sec:cases-induct}). 1.237 - 1.238 + 1.239 \item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface 1.240 - to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted 1.241 - forward manner. 1.242 + to the internal \texttt{mk_cases} operation. Rules are simplified in an 1.243 + unrestricted forward manner. 1.244 1.245 While $ind_cases$ is a proof method to apply the result immediately as 1.246 elimination rules, $\isarkeyword{inductive_cases}$ provides case split 1.247 @@ -648,7 +653,7 @@ 1.248 from executable specifications, both functional and relational programs. 1.249 Isabelle/HOL instantiates these mechanisms in a way that is amenable to 1.250 end-user applications. See \cite{isabelle-HOL} for further information (this 1.251 -actually covers the new-style theory format). 1.252 +actually covers the new-style theory format as well). 1.253 1.254 \indexisarcmd{generate-code}\indexisarcmd{consts-code}\indexisarcmd{types-code} 1.255 \indexisaratt{code} 1.256 @@ -727,10 +732,10 @@ 1.257 dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs 1.258 \end{rail} 1.259 1.260 -Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\ 1.261 -\S\ref{sec:hol-datatype}). Mutual recursive is supported, but no nesting nor 1.262 +Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\ 1.263 +\S\ref{sec:hol-datatype}). Mutual recursion is supported, but no nesting nor 1.264 arbitrary branching. Domain constructors may be strict (default) or lazy, the 1.265 -latter admits to introduce infinitary objects in the typical LCF manner (e.g.\ 1.266 +latter admits to introduce infinitary objects in the typical LCF manner (e.g.\ 1.267 lazy lists). See also \cite{MuellerNvOS99} for a general discussion of HOLCF 1.268 domains. 1.269 1.270 @@ -742,7 +747,7 @@ 1.271 The ZF logic is essentially untyped, so the concept of ``type checking'' is 1.272 performed as logical reasoning about set-membership statements. A special 1.273 method assists users in this task; a version of this is already declared as a 1.274 -``solver'' in the default Simplifier context. 1.275 +``solver'' in the standard Simplifier setup. 1.276 1.277 \indexisarcmd{print-tcset}\indexisaratt{typecheck}\indexisaratt{TC} 1.278 1.279 @@ -779,7 +784,7 @@ 1.280 1.281 In ZF everything is a set. The generic inductive package also provides a 1.282 specific view for ``datatype'' specifications. Coinductive definitions are 1.283 -available as well. 1.284 +available in both cases, too. 1.285 1.286 \indexisarcmdof{ZF}{inductive}\indexisarcmdof{ZF}{coinductive} 1.287 \indexisarcmdof{ZF}{datatype}\indexisarcmdof{ZF}{codatatype}