doc-src/IsarImplementation/Thy/logic.thy
author wenzelm
Fri Sep 08 19:44:43 2006 +0200 (2006-09-08)
changeset 20494 99ad217b6974
parent 20493 48fea5e99505
child 20498 825a8d2335ce
permissions -rw-r--r--
tuned;
     1 
     2 (* $Id$ *)
     3 
     4 theory logic imports base begin
     5 
     6 chapter {* Primitive logic \label{ch:logic} *}
     7 
     8 text {*
     9   The logical foundations of Isabelle/Isar are that of the Pure logic,
    10   which has been introduced as a natural-deduction framework in
    11   \cite{paulson700}.  This is essentially the same logic as ``@{text
    12   "\<lambda>HOL"}'' in the more abstract setting of Pure Type Systems (PTS)
    13   \cite{Barendregt-Geuvers:2001}, although there are some key
    14   differences in the specific treatment of simple types in
    15   Isabelle/Pure.
    16 
    17   Following type-theoretic parlance, the Pure logic consists of three
    18   levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text
    19   "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text
    20   "\<And>"} for universal quantification (proofs depending on terms), and
    21   @{text "\<Longrightarrow>"} for implication (proofs depending on proofs).
    22 
    23   Pure derivations are relative to a logical theory, which declares
    24   type constructors, term constants, and axioms.  Theory declarations
    25   support schematic polymorphism, which is strictly speaking outside
    26   the logic.\footnote{Incidently, this is the main logical reason, why
    27   the theory context @{text "\<Theta>"} is separate from the context @{text
    28   "\<Gamma>"} of the core calculus.}
    29 *}
    30 
    31 
    32 section {* Types \label{sec:types} *}
    33 
    34 text {*
    35   The language of types is an uninterpreted order-sorted first-order
    36   algebra; types are qualified by ordered type classes.
    37 
    38   \medskip A \emph{type class} is an abstract syntactic entity
    39   declared in the theory context.  The \emph{subclass relation} @{text
    40   "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic
    41   generating relation; the transitive closure is maintained
    42   internally.  The resulting relation is an ordering: reflexive,
    43   transitive, and antisymmetric.
    44 
    45   A \emph{sort} is a list of type classes written as @{text
    46   "{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic
    47   intersection.  Notationally, the curly braces are omitted for
    48   singleton intersections, i.e.\ any class @{text "c"} may be read as
    49   a sort @{text "{c}"}.  The ordering on type classes is extended to
    50   sorts according to the meaning of intersections: @{text
    51   "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff
    52   @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}.  The empty intersection
    53   @{text "{}"} refers to the universal sort, which is the largest
    54   element wrt.\ the sort order.  The intersections of all (finitely
    55   many) classes declared in the current theory are the minimal
    56   elements wrt.\ the sort order.
    57 
    58   \medskip A \emph{fixed type variable} is a pair of a basic name
    59   (starting with a @{text "'"} character) and a sort constraint.  For
    60   example, @{text "('a, s)"} which is usually printed as @{text
    61   "\<alpha>\<^isub>s"}.  A \emph{schematic type variable} is a pair of an
    62   indexname and a sort constraint.  For example, @{text "(('a, 0),
    63   s)"} which is usually printed as @{text "?\<alpha>\<^isub>s"}.
    64 
    65   Note that \emph{all} syntactic components contribute to the identity
    66   of type variables, including the sort constraint.  The core logic
    67   handles type variables with the same name but different sorts as
    68   different, although some outer layers of the system make it hard to
    69   produce anything like this.
    70 
    71   A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}-ary operator
    72   on types declared in the theory.  Type constructor application is
    73   usually written postfix as @{text "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}.
    74   For @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text
    75   "prop"} instead of @{text "()prop"}.  For @{text "k = 1"} the
    76   parentheses are omitted, e.g.\ @{text "\<alpha> list"} instead of @{text
    77   "(\<alpha>)list"}.  Further notation is provided for specific constructors,
    78   notably the right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of
    79   @{text "(\<alpha>, \<beta>)fun"}.
    80   
    81   A \emph{type} is defined inductively over type variables and type
    82   constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
    83   (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)k"}.
    84 
    85   A \emph{type abbreviation} is a syntactic abbreviation @{text
    86   "(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over
    87   variables @{text "\<^vec>\<alpha>"}.  Type abbreviations looks like type
    88   constructors at the surface, but are fully expanded before entering
    89   the logical core.
    90 
    91   A \emph{type arity} declares the image behavior of a type
    92   constructor wrt.\ the algebra of sorts: @{text "\<kappa> :: (s\<^isub>1, \<dots>,
    93   s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)\<kappa>"} is
    94   of sort @{text "s"} if every argument type @{text "\<tau>\<^isub>i"} is
    95   of sort @{text "s\<^isub>i"}.  Arity declarations are implicitly
    96   completed, i.e.\ @{text "\<kappa> :: (\<^vec>s)c"} entails @{text "\<kappa> ::
    97   (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
    98 
    99   \medskip The sort algebra is always maintained as \emph{coregular},
   100   which means that type arities are consistent with the subclass
   101   relation: for each type constructor @{text "\<kappa>"} and classes @{text
   102   "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "\<kappa> ::
   103   (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "\<kappa>
   104   :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
   105   \<^vec>s\<^isub>2"} holds componentwise.
   106 
   107   The key property of a coregular order-sorted algebra is that sort
   108   constraints may be always solved in a most general fashion: for each
   109   type constructor @{text "\<kappa>"} and sort @{text "s"} there is a most
   110   general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
   111   s\<^isub>k)"} such that a type scheme @{text
   112   "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is
   113   of sort @{text "s"}.  Consequently, the unification problem on the
   114   algebra of types has most general solutions (modulo renaming and
   115   equivalence of sorts).  Moreover, the usual type-inference algorithm
   116   will produce primary types as expected \cite{nipkow-prehofer}.
   117 *}
   118 
   119 text %mlref {*
   120   \begin{mldecls}
   121   @{index_ML_type class} \\
   122   @{index_ML_type sort} \\
   123   @{index_ML_type arity} \\
   124   @{index_ML_type typ} \\
   125   @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
   126   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
   127   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
   128   @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
   129   @{index_ML Sign.add_tyabbrs_i: "
   130   (bstring * string list * typ * mixfix) list -> theory -> theory"} \\
   131   @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
   132   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
   133   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
   134   \end{mldecls}
   135 
   136   \begin{description}
   137 
   138   \item @{ML_type class} represents type classes; this is an alias for
   139   @{ML_type string}.
   140 
   141   \item @{ML_type sort} represents sorts; this is an alias for
   142   @{ML_type "class list"}.
   143 
   144   \item @{ML_type arity} represents type arities; this is an alias for
   145   triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::
   146   (\<^vec>s)s"} described above.
   147 
   148   \item @{ML_type typ} represents types; this is a datatype with
   149   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
   150 
   151   \item @{ML fold_atyps}~@{text "f \<tau>"} iterates function @{text "f"}
   152   over all occurrences of atoms (@{ML TFree} or @{ML TVar}) of @{text
   153   "\<tau>"}; the type structure is traversed from left to right.
   154 
   155   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
   156   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
   157 
   158   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
   159   is of a given sort.
   160 
   161   \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares new
   162   type constructors @{text "\<kappa>"} with @{text "k"} arguments and
   163   optional mixfix syntax.
   164 
   165   \item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
   166   defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with
   167   optional mixfix syntax.
   168 
   169   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
   170   c\<^isub>n])"} declares new class @{text "c"}, together with class
   171   relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
   172 
   173   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
   174   c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
   175   c\<^isub>2"}.
   176 
   177   \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares
   178   arity @{text "\<kappa> :: (\<^vec>s)s"}.
   179 
   180   \end{description}
   181 *}
   182 
   183 
   184 
   185 section {* Terms \label{sec:terms} *}
   186 
   187 text {*
   188   \glossary{Term}{FIXME}
   189 
   190   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
   191   with de-Bruijn indices for bound variables, and named free
   192   variables, and constants.  Terms with loose bound variables are
   193   usually considered malformed.  The types of variables and constants
   194   is stored explicitly at each occurrence in the term (which is a
   195   known performance issue).
   196 
   197   FIXME de-Bruijn representation of lambda terms
   198 
   199   Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}
   200   and application @{text "t u"}, while types are usually implicit
   201   thanks to type-inference.
   202 
   203   Terms of type @{text "prop"} are called
   204   propositions.  Logical statements are composed via @{text "\<And>x ::
   205   \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.
   206 *}
   207 
   208 
   209 text {*
   210 
   211 FIXME
   212 
   213 \glossary{Schematic polymorphism}{FIXME}
   214 
   215 \glossary{Type variable}{FIXME}
   216 
   217 *}
   218 
   219 
   220 section {* Theorems \label{sec:thms} *}
   221 
   222 text {*
   223 
   224   Primitive reasoning operates on judgments of the form @{text "\<Gamma> \<turnstile>
   225   \<phi>"}, with standard introduction and elimination rules for @{text
   226   "\<And>"} and @{text "\<Longrightarrow>"} that refer to fixed parameters @{text "x"} and
   227   hypotheses @{text "A"} from the context @{text "\<Gamma>"}.  The
   228   corresponding proof terms are left implicit in the classic
   229   ``LCF-approach'', although they could be exploited separately
   230   \cite{Berghofer-Nipkow:2000}.
   231 
   232   The framework also provides definitional equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha>
   233   \<Rightarrow> prop"}, with @{text "\<alpha>\<beta>\<eta>"}-conversion rules.  The internal
   234   conjunction @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} enables the view of
   235   assumptions and conclusions emerging uniformly as simultaneous
   236   statements.
   237 
   238 
   239 
   240   FIXME
   241 
   242 \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
   243 @{text "prop"}.  Internally, there is nothing special about
   244 propositions apart from their type, but the concrete syntax enforces a
   245 clear distinction.  Propositions are structured via implication @{text
   246 "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
   247 else is considered atomic.  The canonical form for propositions is
   248 that of a \seeglossary{Hereditary Harrop Formula}.}
   249 
   250 \glossary{Theorem}{A proven proposition within a certain theory and
   251 proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
   252 rarely spelled out explicitly.  Theorems are usually normalized
   253 according to the \seeglossary{HHF} format.}
   254 
   255 \glossary{Fact}{Sometimes used interchangably for
   256 \seeglossary{theorem}.  Strictly speaking, a list of theorems,
   257 essentially an extra-logical conjunction.  Facts emerge either as
   258 local assumptions, or as results of local goal statements --- both may
   259 be simultaneous, hence the list representation.}
   260 
   261 \glossary{Schematic variable}{FIXME}
   262 
   263 \glossary{Fixed variable}{A variable that is bound within a certain
   264 proof context; an arbitrary-but-fixed entity within a portion of proof
   265 text.}
   266 
   267 \glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
   268 
   269 \glossary{Bound variable}{FIXME}
   270 
   271 \glossary{Variable}{See \seeglossary{schematic variable},
   272 \seeglossary{fixed variable}, \seeglossary{bound variable}, or
   273 \seeglossary{type variable}.  The distinguishing feature of different
   274 variables is their binding scope.}
   275 
   276 *}
   277 
   278 
   279 section {* Proof terms *}
   280 
   281 text {*
   282   FIXME !?
   283 *}
   284 
   285 
   286 section {* Rules \label{sec:rules} *}
   287 
   288 text {*
   289 
   290 FIXME
   291 
   292   A \emph{rule} is any Pure theorem in HHF normal form; there is a
   293   separate calculus for rule composition, which is modeled after
   294   Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows
   295   rules to be nested arbitrarily, similar to \cite{extensions91}.
   296 
   297   Normally, all theorems accessible to the user are proper rules.
   298   Low-level inferences are occasional required internally, but the
   299   result should be always presented in canonical form.  The higher
   300   interfaces of Isabelle/Isar will always produce proper rules.  It is
   301   important to maintain this invariant in add-on applications!
   302 
   303   There are two main principles of rule composition: @{text
   304   "resolution"} (i.e.\ backchaining of rules) and @{text
   305   "by-assumption"} (i.e.\ closing a branch); both principles are
   306   combined in the variants of @{text "elim-resosultion"} and @{text
   307   "dest-resolution"}.  Raw @{text "composition"} is occasionally
   308   useful as well, also it is strictly speaking outside of the proper
   309   rule calculus.
   310 
   311   Rules are treated modulo general higher-order unification, which is
   312   unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion
   313   on @{text "\<lambda>"}-terms.  Moreover, propositions are understood modulo
   314   the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.
   315 
   316   This means that any operations within the rule calculus may be
   317   subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions.  It is common
   318   practice not to contract or expand unnecessarily.  Some mechanisms
   319   prefer an one form, others the opposite, so there is a potential
   320   danger to produce some oscillation!
   321 
   322   Only few operations really work \emph{modulo} HHF conversion, but
   323   expect a normal form: quantifiers @{text "\<And>"} before implications
   324   @{text "\<Longrightarrow>"} at each level of nesting.
   325 
   326 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
   327 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
   328 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
   329 Any proposition may be put into HHF form by normalizing with the rule
   330 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
   331 quantifier prefix is represented via \seeglossary{schematic
   332 variables}, such that the top-level structure is merely that of a
   333 \seeglossary{Horn Clause}}.
   334 
   335 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
   336 
   337 *}
   338 
   339 end