doc-src/IsarImplementation/Thy/logic.thy
 changeset 20521 189811b39869 parent 20520 05fd007bdeb9 child 20537 b6b49903db7e
1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 12 17:45:58 2006 +0200
1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 12 21:05:39 2006 +0200
1.3 @@ -384,13 +384,14 @@
1.4  section {* Theorems \label{sec:thms} *}
1.6  text {*
1.7 -  \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
1.8 -  @{text "prop"}.  Internally, there is nothing special about
1.9 -  propositions apart from their type, but the concrete syntax enforces
1.10 -  a clear distinction.  Propositions are structured via implication
1.11 -  @{text "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} ---
1.12 -  anything else is considered atomic.  The canonical form for
1.13 -  propositions is that of a \seeglossary{Hereditary Harrop Formula}. FIXME}
1.14 +  \glossary{Proposition}{FIXME A \seeglossary{term} of
1.15 +  \seeglossary{type} @{text "prop"}.  Internally, there is nothing
1.16 +  special about propositions apart from their type, but the concrete
1.17 +  syntax enforces a clear distinction.  Propositions are structured
1.18 +  via implication @{text "A \<Longrightarrow> B"} or universal quantification @{text
1.19 +  "\<And>x. B x"} --- anything else is considered atomic.  The canonical
1.20 +  form for propositions is that of a \seeglossary{Hereditary Harrop
1.21 +  Formula}. FIXME}
1.23    \glossary{Theorem}{A proven proposition within a certain theory and
1.24    proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
1.25 @@ -419,22 +420,39 @@
1.26    \seeglossary{type variable}.  The distinguishing feature of
1.27    different variables is their binding scope. FIXME}
1.29 -  A \emph{proposition} is a well-formed term of type @{text "prop"}.
1.30 -  The connectives of minimal logic are declared as constants of the
1.31 -  basic theory:
1.32 +  A \emph{proposition} is a well-formed term of type @{text "prop"}, a
1.33 +  \emph{theorem} is a proven proposition (depending on a context of
1.34 +  hypotheses and the background theory).  Primitive inferences include
1.35 +  plain natural deduction rules for the primary connectives @{text
1.36 +  "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There are separate (derived)
1.37 +  rules for equality/equivalence @{text "\<equiv>"} and internal conjunction
1.38 +  @{text "&"}.
1.39 +*}
1.40 +
1.41 +subsection {* Standard connectives and rules *}
1.43 -  \smallskip
1.44 +text {*
1.45 +  The basic theory is called @{text "Pure"}, it contains declarations
1.46 +  for the standard logical connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and
1.47 +  @{text "\<equiv>"} of the framework, see \figref{fig:pure-connectives}.
1.48 +  The derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is
1.49 +  defined inductively by the primitive inferences given in
1.50 +  \figref{fig:prim-rules}, with the global syntactic restriction that
1.51 +  hypotheses may never contain schematic variables.  The builtin
1.52 +  equality is conceptually axiomatized shown in
1.53 +  \figref{fig:pure-equality}, although the implementation works
1.54 +  directly with (derived) inference rules.
1.55 +
1.56 +  \begin{figure}[htb]
1.57 +  \begin{center}
1.58    \begin{tabular}{ll}
1.59    @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
1.60    @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
1.61 +  @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
1.62    \end{tabular}
1.63 -
1.64 -  \medskip A \emph{theorem} is a proven proposition, depending on a
1.65 -  collection of assumptions, and axioms from the theory context.  The
1.66 -  judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is defined
1.67 -  inductively by the primitive inferences given in
1.68 -  \figref{fig:prim-rules}; there is a global syntactic restriction
1.69 -  that the hypotheses may not contain schematic variables.
1.70 +  \caption{Standard connectives of Pure}\label{fig:pure-connectives}
1.71 +  \end{center}
1.72 +  \end{figure}
1.74    \begin{figure}[htb]
1.75    \begin{center}
1.76 @@ -453,7 +471,20 @@
1.78    \infer[@{text "(\<Longrightarrow>_elim)"}]{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}}
1.79    \]
1.80 -  \caption{Primitive inferences of the Pure logic}\label{fig:prim-rules}
1.81 +  \caption{Primitive inferences of Pure}\label{fig:prim-rules}
1.82 +  \end{center}
1.83 +  \end{figure}
1.84 +
1.85 +  \begin{figure}[htb]
1.86 +  \begin{center}
1.87 +  \begin{tabular}{ll}
1.88 +  @{text "\<turnstile> (\<lambda>x. b x) a \<equiv> b a"} & @{text "\<beta>"}-conversion \\
1.89 +  @{text "\<turnstile> x \<equiv> x"} & reflexivity \\
1.90 +  @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\
1.91 +  @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
1.92 +  @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & coincidence with equivalence \\
1.93 +  \end{tabular}
1.94 +  \caption{Conceptual axiomatization of builtin equality}\label{fig:pure-equality}
1.95    \end{center}
1.96    \end{figure}
1.98 @@ -461,26 +492,35 @@
1.99    "\<Longrightarrow>"} are analogous to formation of (dependently typed) @{text
1.100    "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
1.101    are \emph{irrelevant} in the Pure logic, they may never occur within
1.102 -  propositions, i.e.\ the @{text "\<Longrightarrow>"} arrow of the framework is a
1.103 -  non-dependent one.
1.104 +  propositions, i.e.\ the @{text "\<Longrightarrow>"} arrow is non-dependent.  The
1.105 +  system provides a runtime option to record explicit proof terms for
1.106 +  primitive inferences, cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}.  Thus
1.107 +  the three-fold @{text "\<lambda>"}-structure can be made explicit.
1.109 -  Also note that fixed parameters as in @{text "\<And>_intro"} need not be
1.110 -  recorded in the context @{text "\<Gamma>"}, since syntactic types are
1.111 -  always inhabitable.  An assumption'' @{text "x :: \<tau>"} is logically
1.112 -  vacuous, because @{text "\<tau>"} is always non-empty.  This is the deeper
1.113 -  reason why @{text "\<Gamma>"} only consists of hypothetical proofs, but no
1.114 -  hypothetical terms.
1.115 +  Observe that locally fixed parameters (as used in rule @{text
1.116 +  "\<And>_intro"}) need not be recorded in the hypotheses, because the
1.117 +  simple syntactic types of Pure are always inhabitable.  The typing
1.118 +  assumption'' @{text "x :: \<tau>"} is logically vacuous, it disappears
1.119 +  automatically whenever the statement body ceases to mention variable
1.120 +  @{text "x\<^isub>\<tau>"}.\footnote{This greatly simplifies many basic
1.121 +  reasoning steps, and is the key difference to the formulation of
1.122 +  this logic as @{text "\<lambda>HOL"}'' in the PTS framework
1.123 +  \cite{Barendregt-Geuvers:2001}.}
1.125 -  The corresponding proof terms are left implicit in the classic
1.126 -  LCF-approach'', although they could be exploited separately
1.127 -  \cite{Berghofer-Nipkow:2000}.  The implementation provides a runtime
1.128 -  option to control the generation of full proof terms.
1.129 +  \medskip FIXME @{text "\<alpha>\<beta>\<eta>"}-equivalence and primitive definitions
1.131 +  Since the basic representation of terms already accounts for @{text
1.132 +  "\<alpha>"}-conversion, Pure equality essentially acts like @{text
1.133 +  "\<alpha>\<beta>\<eta>"}-equivalence on terms, while coinciding with bi-implication.
1.135    \medskip The axiomatization of a theory is implicitly closed by
1.136    forming all instances of type and term variables: @{text "\<turnstile> A\<vartheta>"} for
1.137    any substitution instance of axiom @{text "\<turnstile> A"}.  By pushing
1.138    substitution through derivations inductively, we get admissible
1.139    substitution rules for theorems shown in \figref{fig:subst-rules}.
1.140 +  Alternatively, the term substitution rules could be derived from
1.141 +  @{text "\<And>_intro/elim"}.  The versions for types are genuine
1.142 +  admissible rules, due to the lack of true polymorphism in the logic.
1.144    \begin{figure}[htb]
1.145    \begin{center}
1.146 @@ -498,58 +538,105 @@
1.147    \end{center}
1.148    \end{figure}
1.150 -  Note that @{text "instantiate_term"} could be derived using @{text
1.151 -  "\<And>_intro/elim"}, but this is not how it is implemented.  The type
1.152 -  instantiation rule is a genuine admissible one, due to the lack of
1.153 -  true polymorphism in the logic.
1.155    Since @{text "\<Gamma>"} may never contain any schematic variables, the
1.156    @{text "instantiate"} do not require an explicit side-condition.  In
1.157    principle, variables could be substituted in hypotheses as well, but
1.158    this could disrupt monotonicity of the basic calculus: derivations
1.159    could leave the current proof context.
1.160 +*}
1.162 -  \medskip The framework also provides builtin equality @{text "\<equiv>"},
1.163 -  which is conceptually axiomatized shown in \figref{fig:equality},
1.164 -  although the implementation provides derived rules directly:
1.165 +text %mlref {*
1.166 +  \begin{mldecls}
1.167 +  @{index_ML_type ctyp} \\
1.168 +  @{index_ML_type cterm} \\
1.169 +  @{index_ML_type thm} \\
1.170 +  \end{mldecls}
1.172 +  \begin{description}
1.174 +  \item @{ML_type ctyp} FIXME
1.176 +  \item @{ML_type cterm} FIXME
1.178 +  \item @{ML_type thm} FIXME
1.180 +  \end{description}
1.181 +*}
1.184 +subsection {* Auxiliary connectives *}
1.186 +text {*
1.187 +  Pure also provides various auxiliary connectives based on primitive
1.188 +  definitions, see \figref{fig:pure-aux}.  These are normally not
1.189 +  exposed to the user, but appear in internal encodings only.
1.191    \begin{figure}[htb]
1.192    \begin{center}
1.193    \begin{tabular}{ll}
1.194 -  @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
1.195 -  @{text "\<turnstile> (\<lambda>x. b x) a \<equiv> b a"} & @{text "\<beta>"}-conversion \\
1.196 -  @{text "\<turnstile> x \<equiv> x"} & reflexivity law \\
1.197 -  @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution law \\
1.198 -  @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
1.199 -  @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & coincidence with equivalence \\
1.200 +  @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&"}) \\
1.201 +  @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\[1ex]
1.202 +  @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}) \\
1.203 +  @{text "#A \<equiv> A"} \\[1ex]
1.204 +  @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\
1.205 +  @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]
1.206 +  @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
1.207 +  @{text "(unspecified)"} \\
1.208    \end{tabular}
1.209 -  \caption{Conceptual axiomatization of equality.}\label{fig:equality}
1.210 +  \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
1.211    \end{center}
1.212    \end{figure}
1.214 -  Since the basic representation of terms already accounts for @{text
1.215 -  "\<alpha>"}-conversion, Pure equality essentially acts like @{text
1.216 -  "\<alpha>\<beta>\<eta>"}-equivalence on terms, while coinciding with bi-implication.
1.218 +  Conjunction as an explicit connective allows to treat both
1.219 +  simultaneous assumptions and conclusions uniformly.  The definition
1.220 +  allows to derive the usual introduction @{text "\<turnstile> A \<Longrightarrow> B \<Longrightarrow> A & B"},
1.221 +  and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B \<Longrightarrow> B"}.  For
1.222 +  example, several claims may be stated at the same time, which is
1.223 +  intermediately represented as an assumption, but the user only
1.224 +  encounters several sub-goals, and several resulting facts in the
1.225 +  very end (cf.\ \secref{sec:tactical-goals}).
1.227 -  \medskip Conjunction is defined in Pure as a derived connective, see
1.228 -  \figref{fig:conjunction}.  This is occasionally useful to represent
1.229 -  simultaneous statements behind the scenes --- framework conjunction
1.230 -  is usually not exposed to the user.
1.231 +  The @{text "#"} marker allows complex propositions (nested @{text
1.232 +  "\<And>"} and @{text "\<Longrightarrow>"}) to appear formally as atomic, without changing
1.233 +  the meaning: @{text "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are
1.234 +  interchangeable.  See \secref{sec:tactical-goals} for specific
1.235 +  operations.
1.237 +  The @{text "TERM"} marker turns any well-formed term into a
1.238 +  derivable proposition: @{text "\<turnstile> TERM t"} holds
1.239 +  unconditionally.  Despite its logically vacous meaning, this is
1.240 +  occasionally useful to treat syntactic terms and proven propositions
1.241 +  uniformly, as in a type-theoretic framework.
1.243 -  \begin{figure}[htb]
1.244 -  \begin{center}
1.245 -  \begin{tabular}{ll}
1.246 -  @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} & conjunction (hidden) \\
1.247 -  @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\
1.248 -  \end{tabular}
1.249 -  \caption{Definition of conjunction.}\label{fig:equality}
1.250 -  \end{center}
1.251 -  \end{figure}
1.252 +  The @{text "TYPE"} constructor (which is the canonical
1.253 +  representative of the unspecified type @{text "\<alpha> itself"}) injects
1.254 +  the language of types into that of terms.  There is specific
1.255 +  notation @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau>
1.256 + itself\<^esub>"}.
1.257 +  Although being devoid of any particular meaning, the term @{text
1.258 +  "TYPE(\<tau>)"} is able to carry the type @{text "\<tau>"} formally.  @{text
1.259 +  "TYPE(\<alpha>)"} may be used as an additional formal argument in primitive
1.260 +  definitions, in order to avoid hidden polymorphism (cf.\
1.261 +  \secref{sec:terms}).  For example, @{text "c TYPE(\<alpha>) \<equiv> A[\<alpha>]"} turns
1.262 +  out as a formally correct definition of some proposition @{text "A"}
1.263 +  that depends on an additional type argument.
1.264 +*}
1.266 -  The definition allows to derive the usual introduction @{text "\<turnstile> A \<Longrightarrow>
1.267 -  B \<Longrightarrow> A & B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B
1.268 -  \<Longrightarrow> B"}.
1.269 +text %mlref {*
1.270 +  \begin{mldecls}
1.271 +  @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\
1.272 +  @{index_ML Conjunction.elim: "thm -> thm * thm"} \\
1.273 +  @{index_ML Drule.mk_term: "cterm -> thm"} \\
1.274 +  @{index_ML Drule.dest_term: "thm -> cterm"} \\
1.275 +  @{index_ML Logic.mk_type: "typ -> term"} \\
1.276 +  @{index_ML Logic.dest_type: "term -> typ"} \\
1.277 +  \end{mldecls}
1.279 +  \begin{description}
1.281 +  \item FIXME
1.283 +  \end{description}
1.284  *}