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

doc-src/IsarImplementation/Thy/logic.thy

changeset 20543 | dc294418ff17 |

parent 20542 | a54ca4e90874 |

child 20547 | 796ae7fa1049 |

1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy Thu Sep 14 22:48:37 2006 +0200 1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy Fri Sep 15 16:49:41 2006 +0200 1.3 @@ -15,7 +15,7 @@ 1.4 Isabelle/Pure. 1.5 1.6 Following type-theoretic parlance, the Pure logic consists of three 1.7 - levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text 1.8 + levels of @{text "\<lambda>"}-calculus with corresponding arrows, @{text 1.9 "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text 1.10 "\<And>"} for universal quantification (proofs depending on terms), and 1.11 @{text "\<Longrightarrow>"} for implication (proofs depending on proofs). 1.12 @@ -80,7 +80,7 @@ 1.13 1.14 A \emph{type} is defined inductively over type variables and type 1.15 constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s | 1.16 - (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)k"}. 1.17 + (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>"}. 1.18 1.19 A \emph{type abbreviation} is a syntactic definition @{text 1.20 "(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over 1.21 @@ -110,10 +110,9 @@ 1.22 vector of argument sorts @{text "(s\<^isub>1, \<dots>, s\<^isub>k)"} such 1.23 that a type scheme @{text "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, 1.24 \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is of sort @{text "s"}. 1.25 - Consequently, unification on the algebra of types has most general 1.26 - solutions (modulo equivalence of sorts). This means that 1.27 - type-inference will produce primary types as expected 1.28 - \cite{nipkow-prehofer}. 1.29 + Consequently, type unification has most general solutions (modulo 1.30 + equivalence of sorts), so type-inference produces primary types as 1.31 + expected \cite{nipkow-prehofer}. 1.32 *} 1.33 1.34 text %mlref {* 1.35 @@ -176,7 +175,7 @@ 1.36 relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}. 1.37 1.38 \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1, 1.39 - c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq> 1.40 + c\<^isub>2)"} declares the class relation @{text "c\<^isub>1 \<subseteq> 1.41 c\<^isub>2"}. 1.42 1.43 \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares 1.44 @@ -201,17 +200,19 @@ 1.45 \medskip A \emph{bound variable} is a natural number @{text "b"}, 1.46 which accounts for the number of intermediate binders between the 1.47 variable occurrence in the body and its binding position. For 1.48 - example, the de-Bruijn term @{text "\<lambda>\<^isub>\<tau>. \<lambda>\<^isub>\<tau>. 1 + 0"} 1.49 - would correspond to @{text "\<lambda>x\<^isub>\<tau>. \<lambda>y\<^isub>\<tau>. x + y"} in a 1.50 - named representation. Note that a bound variable may be represented 1.51 - by different de-Bruijn indices at different occurrences, depending 1.52 - on the nesting of abstractions. 1.53 + example, the de-Bruijn term @{text 1.54 + "\<lambda>\<^bsub>nat\<^esub>. \<lambda>\<^bsub>nat\<^esub>. 1 + 0"} would 1.55 + correspond to @{text 1.56 + "\<lambda>x\<^bsub>nat\<^esub>. \<lambda>y\<^bsub>nat\<^esub>. x + y"} in a named 1.57 + representation. Note that a bound variable may be represented by 1.58 + different de-Bruijn indices at different occurrences, depending on 1.59 + the nesting of abstractions. 1.60 1.61 - A \emph{loose variables} is a bound variable that is outside the 1.62 + A \emph{loose variable} is a bound variable that is outside the 1.63 scope of local binders. The types (and names) for loose variables 1.64 - can be managed as a separate context, that is maintained inside-out 1.65 - like a stack of hypothetical binders. The core logic only operates 1.66 - on closed terms, without any loose variables. 1.67 + can be managed as a separate context, that is maintained as a stack 1.68 + of hypothetical binders. The core logic operates on closed terms, 1.69 + without any loose variables. 1.70 1.71 A \emph{fixed variable} is a pair of a basic name and a type, e.g.\ 1.72 @{text "(x, \<tau>)"} which is usually printed @{text "x\<^isub>\<tau>"}. A 1.73 @@ -222,8 +223,8 @@ 1.74 \medskip A \emph{constant} is a pair of a basic name and a type, 1.75 e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text 1.76 "c\<^isub>\<tau>"}. Constants are declared in the context as polymorphic 1.77 - families @{text "c :: \<sigma>"}, meaning that valid all substitution 1.78 - instances @{text "c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid. 1.79 + families @{text "c :: \<sigma>"}, meaning that all substitution instances 1.80 + @{text "c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid. 1.81 1.82 The vector of \emph{type arguments} of constant @{text "c\<^isub>\<tau>"} 1.83 wrt.\ the declaration @{text "c :: \<sigma>"} is defined as the codomain of 1.84 @@ -243,13 +244,14 @@ 1.85 polymorphic constants that the user-level type-checker would reject 1.86 due to violation of type class restrictions. 1.87 1.88 - \medskip A \emph{term} is defined inductively over variables and 1.89 - constants, with abstraction and application as follows: @{text "t = 1.90 - b | x\<^isub>\<tau> | ?x\<^isub>\<tau> | c\<^isub>\<tau> | \<lambda>\<^isub>\<tau>. t | 1.91 - t\<^isub>1 t\<^isub>2"}. Parsing and printing takes care of 1.92 - converting between an external representation with named bound 1.93 - variables. Subsequently, we shall use the latter notation instead 1.94 - of internal de-Bruijn representation. 1.95 + \medskip An \emph{atomic} term is either a variable or constant. A 1.96 + \emph{term} is defined inductively over atomic terms, with 1.97 + abstraction and application as follows: @{text "t = b | x\<^isub>\<tau> | 1.98 + ?x\<^isub>\<tau> | c\<^isub>\<tau> | \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}. 1.99 + Parsing and printing takes care of converting between an external 1.100 + representation with named bound variables. Subsequently, we shall 1.101 + use the latter notation instead of internal de-Bruijn 1.102 + representation. 1.103 1.104 The inductive relation @{text "t :: \<tau>"} assigns a (unique) type to a 1.105 term according to the structure of atomic terms, abstractions, and 1.106 @@ -275,25 +277,22 @@ 1.107 "x\<^bsub>\<tau>\<^isub>2\<^esub>"} may become the same after type 1.108 instantiation. Some outer layers of the system make it hard to 1.109 produce variables of the same name, but different types. In 1.110 - particular, type-inference always demands ``consistent'' type 1.111 - constraints for free variables. In contrast, mixed instances of 1.112 - polymorphic constants occur frequently. 1.113 + contrast, mixed instances of polymorphic constants occur frequently. 1.114 1.115 \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"} 1.116 is the set of type variables occurring in @{text "t"}, but not in 1.117 @{text "\<sigma>"}. This means that the term implicitly depends on type 1.118 - arguments that are not accounted in result type, i.e.\ there are 1.119 + arguments that are not accounted in the result type, i.e.\ there are 1.120 different type instances @{text "t\<vartheta> :: \<sigma>"} and @{text 1.121 "t\<vartheta>' :: \<sigma>"} with the same type. This slightly 1.122 - pathological situation demands special care. 1.123 + pathological situation notoriously demands additional care. 1.124 1.125 \medskip A \emph{term abbreviation} is a syntactic definition @{text 1.126 "c\<^isub>\<sigma> \<equiv> t"} of a closed term @{text "t"} of type @{text "\<sigma>"}, 1.127 without any hidden polymorphism. A term abbreviation looks like a 1.128 - constant in the syntax, but is fully expanded before entering the 1.129 - logical core. Abbreviations are usually reverted when printing 1.130 - terms, using the collective @{text "t \<rightarrow> c\<^isub>\<sigma>"} as rules for 1.131 - higher-order rewriting. 1.132 + constant in the syntax, but is expanded before entering the logical 1.133 + core. Abbreviations are usually reverted when printing terms, using 1.134 + @{text "t \<rightarrow> c\<^isub>\<sigma>"} as rules for higher-order rewriting. 1.135 1.136 \medskip Canonical operations on @{text "\<lambda>"}-terms include @{text 1.137 "\<alpha>\<beta>\<eta>"}-conversion: @{text "\<alpha>"}-conversion refers to capture-free 1.138 @@ -308,7 +307,7 @@ 1.139 implicit in the de-Bruijn representation. Names for bound variables 1.140 in abstractions are maintained separately as (meaningless) comments, 1.141 mostly for parsing and printing. Full @{text "\<alpha>\<beta>\<eta>"}-conversion is 1.142 - commonplace in various higher operations (\secref{sec:rules}) that 1.143 + commonplace in various standard operations (\secref{sec:rules}) that 1.144 are based on higher-order unification and matching. 1.145 *} 1.146 1.147 @@ -379,9 +378,8 @@ 1.148 1.149 \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML 1.150 Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"} 1.151 - convert between the representations of polymorphic constants: the 1.152 - full type instance vs.\ the compact type arguments form (depending 1.153 - on the most general declaration given in the context). 1.154 + convert between two representations of polymorphic constants: full 1.155 + type instance vs.\ compact type arguments form. 1.156 1.157 \end{description} 1.158 *} 1.159 @@ -426,7 +424,7 @@ 1.160 \seeglossary{type variable}. The distinguishing feature of 1.161 different variables is their binding scope. FIXME} 1.162 1.163 - A \emph{proposition} is a well-formed term of type @{text "prop"}, a 1.164 + A \emph{proposition} is a well-typed term of type @{text "prop"}, a 1.165 \emph{theorem} is a proven proposition (depending on a context of 1.166 hypotheses and the background theory). Primitive inferences include 1.167 plain natural deduction rules for the primary connectives @{text 1.168 @@ -437,16 +435,16 @@ 1.169 subsection {* Primitive connectives and rules *} 1.170 1.171 text {* 1.172 - The theory @{text "Pure"} contains declarations for the standard 1.173 - connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of the logical 1.174 - framework, see \figref{fig:pure-connectives}. The derivability 1.175 - judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is defined 1.176 - inductively by the primitive inferences given in 1.177 - \figref{fig:prim-rules}, with the global restriction that hypotheses 1.178 - @{text "\<Gamma>"} may \emph{not} contain schematic variables. The builtin 1.179 - equality is conceptually axiomatized as shown in 1.180 + The theory @{text "Pure"} contains constant declarations for the 1.181 + primitive connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of 1.182 + the logical framework, see \figref{fig:pure-connectives}. The 1.183 + derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is 1.184 + defined inductively by the primitive inferences given in 1.185 + \figref{fig:prim-rules}, with the global restriction that the 1.186 + hypotheses must \emph{not} contain any schematic variables. The 1.187 + builtin equality is conceptually axiomatized as shown in 1.188 \figref{fig:pure-equality}, although the implementation works 1.189 - directly with derived inference rules. 1.190 + directly with derived inferences. 1.191 1.192 \begin{figure}[htb] 1.193 \begin{center} 1.194 @@ -496,8 +494,8 @@ 1.195 The introduction and elimination rules for @{text "\<And>"} and @{text 1.196 "\<Longrightarrow>"} are analogous to formation of dependently typed @{text 1.197 "\<lambda>"}-terms representing the underlying proof objects. Proof terms 1.198 - are irrelevant in the Pure logic, though, they may never occur 1.199 - within propositions. The system provides a runtime option to record 1.200 + are irrelevant in the Pure logic, though; they cannot occur within 1.201 + propositions. The system provides a runtime option to record 1.202 explicit proof terms for primitive inferences. Thus all three 1.203 levels of @{text "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for 1.204 terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\ 1.205 @@ -505,19 +503,19 @@ 1.206 1.207 Observe that locally fixed parameters (as in @{text "\<And>_intro"}) need 1.208 not be recorded in the hypotheses, because the simple syntactic 1.209 - types of Pure are always inhabitable. Typing ``assumptions'' @{text 1.210 - "x :: \<tau>"} are (implicitly) present only with occurrences of @{text 1.211 - "x\<^isub>\<tau>"} in the statement body.\footnote{This is the key 1.212 - difference ``@{text "\<lambda>HOL"}'' in the PTS framework 1.213 - \cite{Barendregt-Geuvers:2001}, where @{text "x : A"} hypotheses are 1.214 - treated explicitly for types, in the same way as propositions.} 1.215 + types of Pure are always inhabitable. ``Assumptions'' @{text "x :: 1.216 + \<tau>"} for type-membership are only present as long as some @{text 1.217 + "x\<^isub>\<tau>"} occurs in the statement body.\footnote{This is the key 1.218 + difference to ``@{text "\<lambda>HOL"}'' in the PTS framework 1.219 + \cite{Barendregt-Geuvers:2001}, where hypotheses @{text "x : A"} are 1.220 + treated uniformly for propositions and types.} 1.221 1.222 \medskip The axiomatization of a theory is implicitly closed by 1.223 forming all instances of type and term variables: @{text "\<turnstile> 1.224 A\<vartheta>"} holds for any substitution instance of an axiom 1.225 - @{text "\<turnstile> A"}. By pushing substitution through derivations 1.226 - inductively, we get admissible @{text "generalize"} and @{text 1.227 - "instance"} rules shown in \figref{fig:subst-rules}. 1.228 + @{text "\<turnstile> A"}. By pushing substitutions through derivations 1.229 + inductively, we also get admissible @{text "generalize"} and @{text 1.230 + "instance"} rules as shown in \figref{fig:subst-rules}. 1.231 1.232 \begin{figure}[htb] 1.233 \begin{center} 1.234 @@ -540,38 +538,38 @@ 1.235 variables. 1.236 1.237 In principle, variables could be substituted in hypotheses as well, 1.238 - but this would disrupt monotonicity reasoning: deriving @{text 1.239 - "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is correct, but 1.240 - @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold --- the result 1.241 - belongs to a different proof context. 1.242 + but this would disrupt the monotonicity of reasoning: deriving 1.243 + @{text "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is 1.244 + correct, but @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold: 1.245 + the result belongs to a different proof context. 1.246 1.247 - \medskip The system allows axioms to be stated either as plain 1.248 - propositions, or as arbitrary functions (``oracles'') that produce 1.249 - propositions depending on given arguments. It is possible to trace 1.250 - the used of axioms (and defined theorems) in derivations. 1.251 - Invocations of oracles are recorded invariable. 1.252 + \medskip An \emph{oracle} is a function that produces axioms on the 1.253 + fly. Logically, this is an instance of the @{text "axiom"} rule 1.254 + (\figref{fig:prim-rules}), but there is an operational difference. 1.255 + The system always records oracle invocations within derivations of 1.256 + theorems. Tracing plain axioms (and named theorems) is optional. 1.257 1.258 Axiomatizations should be limited to the bare minimum, typically as 1.259 part of the initial logical basis of an object-logic formalization. 1.260 - Normally, theories will be developed definitionally, by stating 1.261 - restricted equalities over constants. 1.262 + Later on, theories are usually developed in a strictly definitional 1.263 + fashion, by stating only certain equalities over new constants. 1.264 1.265 A \emph{simple definition} consists of a constant declaration @{text 1.266 - "c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text 1.267 - "t"} is a closed term without any hidden polymorphism. The RHS may 1.268 - depend on further defined constants, but not @{text "c"} itself. 1.269 - Definitions of constants with function type may be presented 1.270 - liberally as @{text "c \<^vec> \<equiv> t"} instead of the puristic @{text 1.271 - "c \<equiv> \<lambda>\<^vec>x. t"}. 1.272 + "c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text "t 1.273 + :: \<sigma>"} is a closed term without any hidden polymorphism. The RHS 1.274 + may depend on further defined constants, but not @{text "c"} itself. 1.275 + Definitions of functions may be presented as @{text "c \<^vec>x \<equiv> 1.276 + t"} instead of the puristic @{text "c \<equiv> \<lambda>\<^vec>x. t"}. 1.277 1.278 - An \emph{overloaded definition} consists may give zero or one 1.279 - equality axioms @{text "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type 1.280 - constructor @{text "\<kappa>"}, with distinct variables @{text "\<^vec>\<alpha>"} 1.281 - as formal arguments. The RHS may mention previously defined 1.282 - constants as above, or arbitrary constants @{text "d(\<alpha>\<^isub>i)"} 1.283 - for some @{text "\<alpha>\<^isub>i"} projected from @{text "\<^vec>\<alpha>"}. 1.284 - Thus overloaded definitions essentially work by primitive recursion 1.285 - over the syntactic structure of a single type argument. 1.286 + An \emph{overloaded definition} consists of a collection of axioms 1.287 + for the same constant, with zero or one equations @{text 1.288 + "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type constructor @{text "\<kappa>"} (for 1.289 + distinct variables @{text "\<^vec>\<alpha>"}). The RHS may mention 1.290 + previously defined constants as above, or arbitrary constants @{text 1.291 + "d(\<alpha>\<^isub>i)"} for some @{text "\<alpha>\<^isub>i"} projected from @{text 1.292 + "\<^vec>\<alpha>"}. Thus overloaded definitions essentially work by 1.293 + primitive recursion over the syntactic structure of a single type 1.294 + argument. 1.295 *} 1.296 1.297 text %mlref {* 1.298 @@ -612,10 +610,13 @@ 1.299 \item @{ML_type thm} represents proven propositions. This is an 1.300 abstract datatype that guarantees that its values have been 1.301 constructed by basic principles of the @{ML_struct Thm} module. 1.302 + Every @{ML thm} value contains a sliding back-reference to the 1.303 + enclosing theory, cf.\ \secref{sec:context-theory}. 1.304 1.305 - \item @{ML proofs} determines the detail of proof recording: @{ML 0} 1.306 - records only oracles, @{ML 1} records oracles, axioms and named 1.307 - theorems, @{ML 2} records full proof terms. 1.308 + \item @{ML proofs} determines the detail of proof recording within 1.309 + @{ML_type thm} values: @{ML 0} records only oracles, @{ML 1} records 1.310 + oracles, axioms and named theorems, @{ML 2} records full proof 1.311 + terms. 1.312 1.313 \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML 1.314 Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim} 1.315 @@ -623,8 +624,9 @@ 1.316 1.317 \item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"} 1.318 corresponds to the @{text "generalize"} rules of 1.319 - \figref{fig:subst-rules}. A collection of type and term variables 1.320 - is generalized simultaneously, according to the given basic names. 1.321 + \figref{fig:subst-rules}. Here collections of type and term 1.322 + variables are generalized simultaneously, specified by the given 1.323 + basic names. 1.324 1.325 \item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^isub>s, 1.326 \<^vec>x\<^isub>\<tau>)"} corresponds to the @{text "instantiate"} rules 1.327 @@ -635,45 +637,43 @@ 1.328 \item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named 1.329 axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}. 1.330 1.331 - \item @{ML Thm.invoke_oracle_i}~@{text "thy name arg"} invokes the 1.332 - oracle function @{text "name"} of the theory. Logically, this is 1.333 - just another instance of @{text "axiom"} in \figref{fig:prim-rules}, 1.334 - but the system records an explicit trace of oracle invocations with 1.335 - the @{text "thm"} value. 1.336 + \item @{ML Thm.invoke_oracle_i}~@{text "thy name arg"} invokes a 1.337 + named oracle function, cf.\ @{text "axiom"} in 1.338 + \figref{fig:prim-rules}. 1.339 1.340 - \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} adds 1.341 - arbitrary axioms, without any checking of the proposition. 1.342 + \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares 1.343 + arbitrary propositions as axioms. 1.344 1.345 - \item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an 1.346 - oracle, i.e.\ a function for generating arbitrary axioms. 1.347 + \item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an oracle 1.348 + function for generating arbitrary axioms on the fly. 1.349 1.350 \item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau> 1.351 - \<^vec>d\<^isub>\<sigma>"} declares dependencies of a new specification for 1.352 - constant @{text "c\<^isub>\<tau>"} from relative to existing ones for 1.353 - constants @{text "\<^vec>d\<^isub>\<sigma>"}. 1.354 + \<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification 1.355 + for constant @{text "c\<^isub>\<tau>"}, relative to existing 1.356 + specifications for constants @{text "\<^vec>d\<^isub>\<sigma>"}. 1.357 1.358 \item @{ML Theory.add_defs_i}~@{text "unchecked overloaded [(name, c 1.359 - \<^vec>x \<equiv> t), \<dots>]"} states a definitional axiom for an already 1.360 - declared constant @{text "c"}. Dependencies are recorded using @{ML 1.361 - Theory.add_deps}, unless the @{text "unchecked"} option is set. 1.362 + \<^vec>x \<equiv> t), \<dots>]"} states a definitional axiom for an existing 1.363 + constant @{text "c"}. Dependencies are recorded (cf.\ @{ML 1.364 + Theory.add_deps}), unless the @{text "unchecked"} option is set. 1.365 1.366 \end{description} 1.367 *} 1.368 1.369 1.370 -subsection {* Auxiliary connectives *} 1.371 +subsection {* Auxiliary definitions *} 1.372 1.373 text {* 1.374 - Theory @{text "Pure"} also defines a few auxiliary connectives, see 1.375 - \figref{fig:pure-aux}. These are normally not exposed to the user, 1.376 - but appear in internal encodings only. 1.377 + Theory @{text "Pure"} provides a few auxiliary definitions, see 1.378 + \figref{fig:pure-aux}. These special constants are normally not 1.379 + exposed to the user, but appear in internal encodings. 1.380 1.381 \begin{figure}[htb] 1.382 \begin{center} 1.383 \begin{tabular}{ll} 1.384 @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&"}) \\ 1.385 @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\[1ex] 1.386 - @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}, hidden) \\ 1.387 + @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}, suppressed) \\ 1.388 @{text "#A \<equiv> A"} \\[1ex] 1.389 @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\ 1.390 @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex] 1.391 @@ -688,9 +688,9 @@ 1.392 B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B \<Longrightarrow> B"}. 1.393 Conjunction allows to treat simultaneous assumptions and conclusions 1.394 uniformly. For example, multiple claims are intermediately 1.395 - represented as explicit conjunction, but this is usually refined 1.396 - into separate sub-goals before the user continues the proof; the 1.397 - final result is projected into a list of theorems (cf.\ 1.398 + represented as explicit conjunction, but this is refined into 1.399 + separate sub-goals before the user continues the proof; the final 1.400 + result is projected into a list of theorems (cf.\ 1.401 \secref{sec:tactical-goals}). 1.402 1.403 The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex 1.404 @@ -698,10 +698,10 @@ 1.405 "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are interchangeable. See 1.406 \secref{sec:tactical-goals} for specific operations. 1.407 1.408 - The @{text "term"} marker turns any well-formed term into a 1.409 - derivable proposition: @{text "\<turnstile> TERM t"} holds unconditionally. 1.410 - Although this is logically vacuous, it allows to treat terms and 1.411 - proofs uniformly, similar to a type-theoretic framework. 1.412 + The @{text "term"} marker turns any well-typed term into a derivable 1.413 + proposition: @{text "\<turnstile> TERM t"} holds unconditionally. Although 1.414 + this is logically vacuous, it allows to treat terms and proofs 1.415 + uniformly, similar to a type-theoretic framework. 1.416 1.417 The @{text "TYPE"} constructor is the canonical representative of 1.418 the unspecified type @{text "\<alpha> itself"}; it essentially injects the 1.419 @@ -733,13 +733,13 @@ 1.420 \item @{ML Conjunction.intr} derives @{text "A & B"} from @{text 1.421 "A"} and @{text "B"}. 1.422 1.423 - \item @{ML Conjunction.intr} derives @{text "A"} and @{text "B"} 1.424 + \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"} 1.425 from @{text "A & B"}. 1.426 1.427 - \item @{ML Drule.mk_term}~@{text "t"} derives @{text "TERM t"}. 1.428 + \item @{ML Drule.mk_term} derives @{text "TERM t"}. 1.429 1.430 - \item @{ML Drule.dest_term}~@{text "TERM t"} recovers term @{text 1.431 - "t"}. 1.432 + \item @{ML Drule.dest_term} recovers term @{text "t"} from @{text 1.433 + "TERM t"}. 1.434 1.435 \item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text 1.436 "TYPE(\<tau>)"}.