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.5  
     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.22  
    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.28  
    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.42  
    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.73  
    1.74    \begin{figure}[htb]
    1.75    \begin{center}
    1.76 @@ -453,7 +471,20 @@
    1.77    \qquad
    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.97  
    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.108  
   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.124  
   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.130 +
   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.134  
   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.143  
   1.144    \begin{figure}[htb]
   1.145    \begin{center}
   1.146 @@ -498,58 +538,105 @@
   1.147    \end{center}
   1.148    \end{figure}
   1.149  
   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.154 -
   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.161  
   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.171 +
   1.172 +  \begin{description}
   1.173 +
   1.174 +  \item @{ML_type ctyp} FIXME
   1.175 +
   1.176 +  \item @{ML_type cterm} FIXME
   1.177 +
   1.178 +  \item @{ML_type thm} FIXME
   1.179 +
   1.180 +  \end{description}
   1.181 +*}
   1.182 +
   1.183 +
   1.184 +subsection {* Auxiliary connectives *}
   1.185 +
   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.190  
   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.213  
   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.217 -
   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.226  
   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.236 +
   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.242  
   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.265  
   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.278 +
   1.279 +  \begin{description}
   1.280 +
   1.281 +  \item FIXME
   1.282 +
   1.283 +  \end{description}
   1.284  *}
   1.285  
   1.286