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