doc-src/IsarImplementation/Thy/logic.thy
author wenzelm
Fri Sep 08 17:33:05 2006 +0200 (2006-09-08)
changeset 20493 48fea5e99505
parent 20491 98ba42f19995
child 20494 99ad217b6974
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 "(FIXME)\<kappa>"}.  For @{text "k = 0"}
    74   the argument tuple is omitted, e.g.\ @{text "prop"} instead of
    75   @{text "()prop"}.  For @{text "k = 1"} the parentheses are omitted,
    76   e.g.\ @{text "\<alpha> list"} instead of @{text "(\<alpha>)list"}.  Further
    77   notation is provided for specific constructors, notably
    78   right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,
    79   \<beta>)fun"} constructor.
    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)c"}.
    84 
    85   A \emph{type abbreviation} is a syntactic abbreviation of an
    86   arbitrary type expression of the theory.  Type abbreviations looks
    87   like type constructors at the surface, but are expanded before the
    88   core logic encounters them.
    89 
    90   A \emph{type arity} declares the image behavior of a type
    91   constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>,
    92   s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is
    93   of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of
    94   sort @{text "s\<^isub>i"}.  Arity declarations are implicitly
    95   completed, i.e.\ @{text "c :: (\<^vec>s)c"} entails @{text "c ::
    96   (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
    97 
    98   \medskip The sort algebra is always maintained as \emph{coregular},
    99   which means that type arities are consistent with the subclass
   100   relation: for each type constructor @{text "c"} and classes @{text
   101   "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::
   102   (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c
   103   :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
   104   \<^vec>s\<^isub>2"} holds pointwise for all argument sorts.
   105 
   106   The key property of a coregular order-sorted algebra is that sort
   107   constraints may be always fulfilled in a most general fashion: for
   108   each type constructor @{text "c"} and sort @{text "s"} there is a
   109   most general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
   110   s\<^isub>k)"} such that a type scheme @{text
   111   "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)c"} is
   112   of sort @{text "s"}.  Consequently, the unification problem on the
   113   algebra of types has most general solutions (modulo renaming and
   114   equivalence of sorts).  Moreover, the usual type-inference algorithm
   115   will produce primary types as expected \cite{nipkow-prehofer}.
   116 *}
   117 
   118 text %mlref {*
   119   \begin{mldecls}
   120   @{index_ML_type class} \\
   121   @{index_ML_type sort} \\
   122   @{index_ML_type typ} \\
   123   @{index_ML_type arity} \\
   124   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
   125   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
   126   @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
   127   @{index_ML Sign.add_tyabbrs_i: "
   128   (bstring * string list * typ * mixfix) list -> theory -> theory"} \\
   129   @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
   130   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
   131   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
   132   \end{mldecls}
   133 
   134   \begin{description}
   135 
   136   \item @{ML_type class} represents type classes; this is an alias for
   137   @{ML_type string}.
   138 
   139   \item @{ML_type sort} represents sorts; this is an alias for
   140   @{ML_type "class list"}.
   141 
   142   \item @{ML_type arity} represents type arities; this is an alias for
   143   triples of the form @{text "(c, \<^vec>s, s)"} for @{text "c ::
   144   (\<^vec>s)s"} described above.
   145 
   146   \item @{ML_type typ} represents types; this is a datatype with
   147   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
   148 
   149   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
   150   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
   151 
   152   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
   153   is of a given sort.
   154 
   155   \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new
   156   type constructors @{text "c"} with @{text "k"} arguments and
   157   optional mixfix syntax.
   158 
   159   \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
   160   defines a new type abbreviation @{text "(\<^vec>\<alpha>)c = \<tau>"} with
   161   optional mixfix syntax.
   162 
   163   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
   164   c\<^isub>n])"} declares new class @{text "c"} derived together with
   165   class relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
   166 
   167   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
   168   c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
   169   c\<^isub>2"}.
   170 
   171   \item @{ML Sign.primitive_arity}~@{text "(c, \<^vec>s, s)"} declares
   172   arity @{text "c :: (\<^vec>s)s"}.
   173 
   174   \end{description}
   175 *}
   176 
   177 
   178 
   179 section {* Terms \label{sec:terms} *}
   180 
   181 text {*
   182   \glossary{Term}{FIXME}
   183 
   184   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
   185   with de-Bruijn indices for bound variables, and named free
   186   variables, and constants.  Terms with loose bound variables are
   187   usually considered malformed.  The types of variables and constants
   188   is stored explicitly at each occurrence in the term (which is a
   189   known performance issue).
   190 
   191   FIXME de-Bruijn representation of lambda terms
   192 
   193   Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}
   194   and application @{text "t u"}, while types are usually implicit
   195   thanks to type-inference.
   196 
   197   Terms of type @{text "prop"} are called
   198   propositions.  Logical statements are composed via @{text "\<And>x ::
   199   \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.
   200 *}
   201 
   202 
   203 text {*
   204 
   205 FIXME
   206 
   207 \glossary{Schematic polymorphism}{FIXME}
   208 
   209 \glossary{Type variable}{FIXME}
   210 
   211 *}
   212 
   213 
   214 section {* Theorems \label{sec:thms} *}
   215 
   216 text {*
   217 
   218   Primitive reasoning operates on judgments of the form @{text "\<Gamma> \<turnstile>
   219   \<phi>"}, with standard introduction and elimination rules for @{text
   220   "\<And>"} and @{text "\<Longrightarrow>"} that refer to fixed parameters @{text "x"} and
   221   hypotheses @{text "A"} from the context @{text "\<Gamma>"}.  The
   222   corresponding proof terms are left implicit in the classic
   223   ``LCF-approach'', although they could be exploited separately
   224   \cite{Berghofer-Nipkow:2000}.
   225 
   226   The framework also provides definitional equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha>
   227   \<Rightarrow> prop"}, with @{text "\<alpha>\<beta>\<eta>"}-conversion rules.  The internal
   228   conjunction @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} enables the view of
   229   assumptions and conclusions emerging uniformly as simultaneous
   230   statements.
   231 
   232 
   233 
   234   FIXME
   235 
   236 \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
   237 @{text "prop"}.  Internally, there is nothing special about
   238 propositions apart from their type, but the concrete syntax enforces a
   239 clear distinction.  Propositions are structured via implication @{text
   240 "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
   241 else is considered atomic.  The canonical form for propositions is
   242 that of a \seeglossary{Hereditary Harrop Formula}.}
   243 
   244 \glossary{Theorem}{A proven proposition within a certain theory and
   245 proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
   246 rarely spelled out explicitly.  Theorems are usually normalized
   247 according to the \seeglossary{HHF} format.}
   248 
   249 \glossary{Fact}{Sometimes used interchangably for
   250 \seeglossary{theorem}.  Strictly speaking, a list of theorems,
   251 essentially an extra-logical conjunction.  Facts emerge either as
   252 local assumptions, or as results of local goal statements --- both may
   253 be simultaneous, hence the list representation.}
   254 
   255 \glossary{Schematic variable}{FIXME}
   256 
   257 \glossary{Fixed variable}{A variable that is bound within a certain
   258 proof context; an arbitrary-but-fixed entity within a portion of proof
   259 text.}
   260 
   261 \glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
   262 
   263 \glossary{Bound variable}{FIXME}
   264 
   265 \glossary{Variable}{See \seeglossary{schematic variable},
   266 \seeglossary{fixed variable}, \seeglossary{bound variable}, or
   267 \seeglossary{type variable}.  The distinguishing feature of different
   268 variables is their binding scope.}
   269 
   270 *}
   271 
   272 
   273 section {* Proof terms *}
   274 
   275 text {*
   276   FIXME !?
   277 *}
   278 
   279 
   280 section {* Rules \label{sec:rules} *}
   281 
   282 text {*
   283 
   284 FIXME
   285 
   286   A \emph{rule} is any Pure theorem in HHF normal form; there is a
   287   separate calculus for rule composition, which is modeled after
   288   Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows
   289   rules to be nested arbitrarily, similar to \cite{extensions91}.
   290 
   291   Normally, all theorems accessible to the user are proper rules.
   292   Low-level inferences are occasional required internally, but the
   293   result should be always presented in canonical form.  The higher
   294   interfaces of Isabelle/Isar will always produce proper rules.  It is
   295   important to maintain this invariant in add-on applications!
   296 
   297   There are two main principles of rule composition: @{text
   298   "resolution"} (i.e.\ backchaining of rules) and @{text
   299   "by-assumption"} (i.e.\ closing a branch); both principles are
   300   combined in the variants of @{text "elim-resosultion"} and @{text
   301   "dest-resolution"}.  Raw @{text "composition"} is occasionally
   302   useful as well, also it is strictly speaking outside of the proper
   303   rule calculus.
   304 
   305   Rules are treated modulo general higher-order unification, which is
   306   unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion
   307   on @{text "\<lambda>"}-terms.  Moreover, propositions are understood modulo
   308   the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.
   309 
   310   This means that any operations within the rule calculus may be
   311   subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions.  It is common
   312   practice not to contract or expand unnecessarily.  Some mechanisms
   313   prefer an one form, others the opposite, so there is a potential
   314   danger to produce some oscillation!
   315 
   316   Only few operations really work \emph{modulo} HHF conversion, but
   317   expect a normal form: quantifiers @{text "\<And>"} before implications
   318   @{text "\<Longrightarrow>"} at each level of nesting.
   319 
   320 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
   321 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
   322 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
   323 Any proposition may be put into HHF form by normalizing with the rule
   324 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
   325 quantifier prefix is represented via \seeglossary{schematic
   326 variables}, such that the top-level structure is merely that of a
   327 \seeglossary{Horn Clause}}.
   328 
   329 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
   330 
   331 *}
   332 
   333 end