doc-src/IsarImplementation/Thy/logic.thy
changeset 20501 de0b523b0d62
parent 20498 825a8d2335ce
child 20514 5ede702cd2ca
     1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Mon Sep 11 14:28:47 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Mon Sep 11 14:35:25 2006 +0200
     1.3 @@ -200,15 +200,13 @@
     1.4    and application @{text "t u"}, while types are usually implicit
     1.5    thanks to type-inference.
     1.6  
     1.7 -  Terms of type @{text "prop"} are called
     1.8 -  propositions.  Logical statements are composed via @{text "\<And>x ::
     1.9 -  \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.
    1.10 -
    1.11  
    1.12    \[
    1.13 -  \infer{@{text "(\<lambda>x\<^sub>\<tau>. t): \<tau> \<Rightarrow> \<sigma>"}}{@{text "t: \<sigma>"}}
    1.14 +  \infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{}
    1.15    \qquad
    1.16 -  \infer{@{text "(t u): \<sigma>"}}{@{text "t: \<tau> \<Rightarrow> \<sigma>"} & @{text "u: \<tau>"}}
    1.17 +  \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}}
    1.18 +  \qquad
    1.19 +  \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}}
    1.20    \]
    1.21  
    1.22  *}
    1.23 @@ -228,60 +226,60 @@
    1.24  section {* Theorems \label{sec:thms} *}
    1.25  
    1.26  text {*
    1.27 -
    1.28 -  Primitive reasoning operates on judgments of the form @{text "\<Gamma> \<turnstile>
    1.29 -  \<phi>"}, with standard introduction and elimination rules for @{text
    1.30 -  "\<And>"} and @{text "\<Longrightarrow>"} that refer to fixed parameters @{text "x"} and
    1.31 -  hypotheses @{text "A"} from the context @{text "\<Gamma>"}.  The
    1.32 -  corresponding proof terms are left implicit in the classic
    1.33 -  ``LCF-approach'', although they could be exploited separately
    1.34 -  \cite{Berghofer-Nipkow:2000}.
    1.35 +  \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
    1.36 +  @{text "prop"}.  Internally, there is nothing special about
    1.37 +  propositions apart from their type, but the concrete syntax enforces
    1.38 +  a clear distinction.  Propositions are structured via implication
    1.39 +  @{text "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} ---
    1.40 +  anything else is considered atomic.  The canonical form for
    1.41 +  propositions is that of a \seeglossary{Hereditary Harrop Formula}. FIXME}
    1.42  
    1.43 -  The framework also provides definitional equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha>
    1.44 -  \<Rightarrow> prop"}, with @{text "\<alpha>\<beta>\<eta>"}-conversion rules.  The internal
    1.45 -  conjunction @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} enables the view of
    1.46 -  assumptions and conclusions emerging uniformly as simultaneous
    1.47 -  statements.
    1.48 -
    1.49 -
    1.50 +  \glossary{Theorem}{A proven proposition within a certain theory and
    1.51 +  proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
    1.52 +  rarely spelled out explicitly.  Theorems are usually normalized
    1.53 +  according to the \seeglossary{HHF} format. FIXME}
    1.54  
    1.55 -  FIXME
    1.56 +  \glossary{Fact}{Sometimes used interchangably for
    1.57 +  \seeglossary{theorem}.  Strictly speaking, a list of theorems,
    1.58 +  essentially an extra-logical conjunction.  Facts emerge either as
    1.59 +  local assumptions, or as results of local goal statements --- both
    1.60 +  may be simultaneous, hence the list representation. FIXME}
    1.61  
    1.62 -\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
    1.63 -@{text "prop"}.  Internally, there is nothing special about
    1.64 -propositions apart from their type, but the concrete syntax enforces a
    1.65 -clear distinction.  Propositions are structured via implication @{text
    1.66 -"A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
    1.67 -else is considered atomic.  The canonical form for propositions is
    1.68 -that of a \seeglossary{Hereditary Harrop Formula}.}
    1.69 +  \glossary{Schematic variable}{FIXME}
    1.70 +
    1.71 +  \glossary{Fixed variable}{A variable that is bound within a certain
    1.72 +  proof context; an arbitrary-but-fixed entity within a portion of
    1.73 +  proof text. FIXME}
    1.74  
    1.75 -\glossary{Theorem}{A proven proposition within a certain theory and
    1.76 -proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
    1.77 -rarely spelled out explicitly.  Theorems are usually normalized
    1.78 -according to the \seeglossary{HHF} format.}
    1.79 +  \glossary{Free variable}{Synonymous for \seeglossary{fixed
    1.80 +  variable}. FIXME}
    1.81 +
    1.82 +  \glossary{Bound variable}{FIXME}
    1.83  
    1.84 -\glossary{Fact}{Sometimes used interchangably for
    1.85 -\seeglossary{theorem}.  Strictly speaking, a list of theorems,
    1.86 -essentially an extra-logical conjunction.  Facts emerge either as
    1.87 -local assumptions, or as results of local goal statements --- both may
    1.88 -be simultaneous, hence the list representation.}
    1.89 +  \glossary{Variable}{See \seeglossary{schematic variable},
    1.90 +  \seeglossary{fixed variable}, \seeglossary{bound variable}, or
    1.91 +  \seeglossary{type variable}.  The distinguishing feature of
    1.92 +  different variables is their binding scope. FIXME}
    1.93  
    1.94 -\glossary{Schematic variable}{FIXME}
    1.95 +  A \emph{proposition} is a well-formed term of type @{text "prop"}.
    1.96 +  The connectives of minimal logic are declared as constants of the
    1.97 +  basic theory:
    1.98  
    1.99 -\glossary{Fixed variable}{A variable that is bound within a certain
   1.100 -proof context; an arbitrary-but-fixed entity within a portion of proof
   1.101 -text.}
   1.102 -
   1.103 -\glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
   1.104 +  \smallskip
   1.105 +  \begin{tabular}{ll}
   1.106 +  @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
   1.107 +  @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
   1.108 +  \end{tabular}
   1.109  
   1.110 -\glossary{Bound variable}{FIXME}
   1.111 +  \medskip A \emph{theorem} is a proven proposition, depending on a
   1.112 +  collection of assumptions, and axioms from the theory context.  The
   1.113 +  judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is defined
   1.114 +  inductively by the primitive inferences given in
   1.115 +  \figref{fig:prim-rules}; there is a global syntactic restriction
   1.116 +  that the hypotheses may not contain schematic variables.
   1.117  
   1.118 -\glossary{Variable}{See \seeglossary{schematic variable},
   1.119 -\seeglossary{fixed variable}, \seeglossary{bound variable}, or
   1.120 -\seeglossary{type variable}.  The distinguishing feature of different
   1.121 -variables is their binding scope.}
   1.122 -
   1.123 -
   1.124 +  \begin{figure}[htb]
   1.125 +  \begin{center}
   1.126    \[
   1.127    \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}}
   1.128    \qquad
   1.129 @@ -297,40 +295,103 @@
   1.130    \qquad
   1.131    \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.132    \]
   1.133 +  \caption{Primitive inferences of the Pure logic}\label{fig:prim-rules}
   1.134 +  \end{center}
   1.135 +  \end{figure}
   1.136  
   1.137 +  The introduction and elimination rules for @{text "\<And>"} and @{text
   1.138 +  "\<Longrightarrow>"} are analogous to formation of (dependently typed) @{text
   1.139 +  "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
   1.140 +  are \emph{irrelevant} in the Pure logic, they may never occur within
   1.141 +  propositions, i.e.\ the @{text "\<Longrightarrow>"} arrow of the framework is a
   1.142 +  non-dependent one.
   1.143  
   1.144 -  Admissible rules:
   1.145 +  Also note that fixed parameters as in @{text "\<And>_intro"} need not be
   1.146 +  recorded in the context @{text "\<Gamma>"}, since syntactic types are
   1.147 +  always inhabitable.  An ``assumption'' @{text "x :: \<tau>"} is logically
   1.148 +  vacuous, because @{text "\<tau>"} is always non-empty.  This is the deeper
   1.149 +  reason why @{text "\<Gamma>"} only consists of hypothetical proofs, but no
   1.150 +  hypothetical terms.
   1.151 +
   1.152 +  The corresponding proof terms are left implicit in the classic
   1.153 +  ``LCF-approach'', although they could be exploited separately
   1.154 +  \cite{Berghofer-Nipkow:2000}.  The implementation provides a runtime
   1.155 +  option to control the generation of full proof terms.
   1.156 +
   1.157 +  \medskip The axiomatization of a theory is implicitly closed by
   1.158 +  forming all instances of type and term variables: @{text "\<turnstile> A\<theta>"} for
   1.159 +  any substirution instance of axiom @{text "\<turnstile> A"}.  By pushing
   1.160 +  substitution through derivations inductively, we get admissible
   1.161 +  substitution rules for theorems shown in \figref{fig:subst-rules}.
   1.162 +
   1.163 +  \begin{figure}[htb]
   1.164 +  \begin{center}
   1.165    \[
   1.166 -  \infer[@{text "(generalize_type)"}]{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}
   1.167 -  \qquad
   1.168 -  \infer[@{text "(generalize_term)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}
   1.169 +  \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}
   1.170 +  \quad
   1.171 +  \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}
   1.172    \]
   1.173    \[
   1.174 -  \infer[@{text "(instantiate_type)"}]{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}
   1.175 -  \qquad
   1.176 -  \infer[@{text "(instantiate_term)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}
   1.177 +  \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}
   1.178 +  \quad
   1.179 +  \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}
   1.180    \]
   1.181 +  \caption{Admissible substitution rules}\label{fig:subst-rules}
   1.182 +  \end{center}
   1.183 +  \end{figure}
   1.184  
   1.185    Note that @{text "instantiate_term"} could be derived using @{text
   1.186    "\<And>_intro/elim"}, but this is not how it is implemented.  The type
   1.187 -  instantiation rule is a genuine admissible one, due to the lack of true
   1.188 -  polymorphism in the logic.
   1.189 -
   1.190 +  instantiation rule is a genuine admissible one, due to the lack of
   1.191 +  true polymorphism in the logic.
   1.192  
   1.193 -  Equality and logical equivalence:
   1.194 +  Since @{text "\<Gamma>"} may never contain any schematic variables, the
   1.195 +  @{text "instantiate"} do not require an explicit side-condition.  In
   1.196 +  principle, variables could be substituted in hypotheses as well, but
   1.197 +  this could disrupt monotonicity of the basic calculus: derivations
   1.198 +  could leave the current proof context.
   1.199  
   1.200 -  \smallskip
   1.201 +  \medskip The framework also provides builtin equality @{text "\<equiv>"},
   1.202 +  which is conceptually axiomatized shown in \figref{fig:equality},
   1.203 +  although the implementation provides derived rules directly:
   1.204 +
   1.205 +  \begin{figure}[htb]
   1.206 +  \begin{center}
   1.207    \begin{tabular}{ll}
   1.208    @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
   1.209 +  @{text "\<turnstile> (\<lambda>x. b x) a \<equiv> b a"} & @{text "\<beta>"}-conversion \\
   1.210    @{text "\<turnstile> x \<equiv> x"} & reflexivity law \\
   1.211    @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution law \\
   1.212    @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
   1.213    @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & coincidence with equivalence \\
   1.214    \end{tabular}
   1.215 -  \smallskip
   1.216 +  \caption{Conceptual axiomatization of equality.}\label{fig:equality}
   1.217 +  \end{center}
   1.218 +  \end{figure}
   1.219 +
   1.220 +  Since the basic representation of terms already accounts for @{text
   1.221 +  "\<alpha>"}-conversion, Pure equality essentially acts like @{text
   1.222 +  "\<alpha>\<beta>\<eta>"}-equivalence on terms, while coinciding with bi-implication.
   1.223  
   1.224  
   1.225 +  \medskip Conjunction is defined in Pure as a derived connective, see
   1.226 +  \figref{fig:conjunction}.  This is occasionally useful to represent
   1.227 +  simultaneous statements behind the scenes --- framework conjunction
   1.228 +  is usually not exposed to the user.
   1.229  
   1.230 +  \begin{figure}[htb]
   1.231 +  \begin{center}
   1.232 +  \begin{tabular}{ll}
   1.233 +  @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} & conjunction (hidden) \\
   1.234 +  @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\
   1.235 +  \end{tabular}
   1.236 +  \caption{Definition of conjunction.}\label{fig:equality}
   1.237 +  \end{center}
   1.238 +  \end{figure}
   1.239 +
   1.240 +  The definition allows to derive the usual introduction @{text "\<turnstile> A \<Longrightarrow>
   1.241 +  B \<Longrightarrow> A & B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B
   1.242 +  \<Longrightarrow> B"}.
   1.243  *}
   1.244  
   1.245