doc-src/IsarImplementation/Thy/logic.thy
author wenzelm
Tue Sep 05 22:05:41 2006 +0200 (2006-09-05)
changeset 20480 4e0522d38968
parent 20477 e623b0e30541
child 20491 98ba42f19995
permissions -rw-r--r--
more on types and type classes;
     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 practical treatment of simple types.
    15 
    16   Following type-theoretic parlance, the Pure logic consists of three
    17   levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text
    18   "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text
    19   "\<And>"} for universal quantification (proofs depending on terms), and
    20   @{text "\<Longrightarrow>"} for implication (proofs depending on proofs).
    21 
    22   Pure derivations are relative to a logical theory, which declares
    23   type constructors, term constants, and axioms.  Term constants and
    24   axioms support schematic polymorphism.
    25 *}
    26 
    27 
    28 section {* Types \label{sec:types} *}
    29 
    30 text {*
    31   The language of types is an uninterpreted order-sorted first-order
    32   algebra; types are qualified by ordered type classes.
    33 
    34   \medskip A \emph{type class} is an abstract syntactic entity
    35   declared in the theory context.  The \emph{subclass relation} @{text
    36   "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic
    37   generating relation; the transitive closure maintained internally.
    38 
    39   A \emph{sort} is a list of type classes written as @{text
    40   "{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic
    41   intersection.  Notationally, the curly braces are omitted for
    42   singleton intersections, i.e.\ any class @{text "c"} may be read as
    43   a sort @{text "{c}"}.  The ordering on type classes is extended to
    44   sorts in the canonical fashion: @{text "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq>
    45   {d\<^isub>1, \<dots>, d\<^isub>n}"} iff @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq>
    46   d\<^isub>j"}.  The empty intersection @{text "{}"} refers to the
    47   universal sort, which is the largest element wrt.\ the sort order.
    48   The intersections of all (i.e.\ finitely many) classes declared in
    49   the current theory are the minimal elements wrt.\ sort order.
    50 
    51   \medskip A \emph{fixed type variable} is pair of a basic name
    52   (starting with @{text "'"} character) and a sort constraint.  For
    53   example, @{text "('a, s)"} which is usually printed as @{text
    54   "\<alpha>\<^isub>s"}.  A \emph{schematic type variable} is a pair of an
    55   indexname and a sort constraint.  For example, @{text "(('a, 0),
    56   s)"} which is usually printed @{text "?\<alpha>\<^isub>s"}.
    57 
    58   Note that \emph{all} syntactic components contribute to the identity
    59   of a type variables, including the literal sort constraint.  The
    60   core logic handles type variables with the same name but different
    61   sorts as different, even though the outer layers of the system make
    62   it hard to produce anything like this.
    63 
    64   A \emph{type constructor} is an @{text "k"}-ary type operator
    65   declared in the theory.
    66   
    67   A \emph{type} is defined inductively over type variables and type
    68   constructors: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s | (\<tau>\<^sub>1, \<dots>,
    69   \<tau>\<^sub>k)c"}.  Type constructor application is usually written
    70   postfix.  For @{text "k = 0"} the argument tuple is omitted, e.g.\
    71   @{text "prop"} instead of @{text "()prop"}.  For @{text "k = 1"} the
    72   parentheses are omitted, e.g.\ @{text "\<tau> list"} instead of @{text
    73   "(\<tau>) list"}.  Further notation is provided for specific
    74   constructors, notably right-associative infix @{text "\<tau>\<^isub>1 \<Rightarrow>
    75   \<tau>\<^isub>2"} instead of @{text "(\<tau>\<^isub>1, \<tau>\<^isub>2)fun"}
    76   constructor.
    77 
    78   A \emph{type abbreviation} is a syntactic abbreviation of an
    79   arbitrary type expression of the theory.  Type abbreviations looks
    80   like type constructors at the surface, but are expanded before the
    81   core logic encounters them.
    82 
    83   A \emph{type arity} declares the image behavior of a type
    84   constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>,
    85   s\<^isub>n)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is
    86   of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of
    87   sort @{text "s\<^isub>i"}.  The sort algebra is always maintained as
    88   \emph{coregular}, which means that type arities are consistent with
    89   the subclass relation: for each type constructor @{text "c"} and
    90   classes @{text "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::
    91   (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c
    92   :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
    93   \<^vec>s\<^isub>2"} holds pointwise for all argument sorts.
    94 
    95   The key property of the order-sorted algebra of types is that sort
    96   constraints may be always fulfilled in a most general fashion: for
    97   each type constructor @{text "c"} and sort @{text "s"} there is a
    98   most general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
    99   s\<^isub>k)"} such that @{text "(\<tau>\<^bsub>s\<^isub>1\<^esub>, \<dots>,
   100   \<tau>\<^bsub>s\<^isub>k\<^esub>)"} for arbitrary @{text "\<tau>\<^isub>i"} of
   101   sort @{text "s\<^isub>i"}.  This means the unification problem on
   102   the algebra of types has most general solutions (modulo renaming and
   103   equivalence of sorts).  As a consequence, type-inference is able to
   104   produce primary types.
   105 *}
   106 
   107 text %mlref {*
   108   \begin{mldecls}
   109   @{index_ML_type class} \\
   110   @{index_ML_type sort} \\
   111   @{index_ML_type typ} \\
   112   @{index_ML_type arity} \\
   113   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
   114   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
   115   @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
   116   @{index_ML Sign.add_tyabbrs_i: "
   117   (bstring * string list * typ * mixfix) list -> theory -> theory"} \\
   118   @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
   119   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
   120   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
   121   \end{mldecls}
   122 
   123   \begin{description}
   124 
   125   \item @{ML_type class} represents type classes; this is an alias for
   126   @{ML_type string}.
   127 
   128   \item @{ML_type sort} represents sorts; this is an alias for
   129   @{ML_type "class list"}.
   130 
   131   \item @{ML_type arity} represents type arities; this is an alias for
   132   triples of the form @{text "(c, \<^vec>s, s)"} for @{text "c ::
   133   (\<^vec>s)s"} described above.
   134 
   135   \item @{ML_type typ} represents types; this is a datatype with
   136   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
   137 
   138   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
   139   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
   140 
   141   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
   142   expression of of a given sort.
   143 
   144   \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new
   145   type constructors @{text "c"} with @{text "k"} arguments, and
   146   optional mixfix syntax.
   147 
   148   \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
   149   defines type abbreviation @{text "(\<^vec>\<alpha>)c"} (with optional
   150   mixfix syntax) as @{text "\<tau>"}.
   151 
   152   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
   153   c\<^isub>n])"} declares new class @{text "c"} derived together with
   154   class relations @{text "c \<subseteq> c\<^isub>i"}.
   155 
   156   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
   157   c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
   158   c\<^isub>2"}.
   159 
   160   \item @{ML Sign.primitive_arity}~@{text "(c, \<^vec>s, s)"} declares
   161   arity @{text "c :: (\<^vec>s)s"}.
   162 
   163   \end{description}
   164 *}
   165 
   166 
   167 
   168 section {* Terms \label{sec:terms} *}
   169 
   170 text {*
   171   \glossary{Term}{FIXME}
   172 
   173   FIXME de-Bruijn representation of lambda terms
   174 
   175   Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}
   176   and application @{text "t u"}, while types are usually implicit
   177   thanks to type-inference.
   178 
   179   Terms of type @{text "prop"} are called
   180   propositions.  Logical statements are composed via @{text "\<And>x ::
   181   \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.
   182 *}
   183 
   184 
   185 text {*
   186 
   187 FIXME
   188 
   189 \glossary{Schematic polymorphism}{FIXME}
   190 
   191 \glossary{Type variable}{FIXME}
   192 
   193 *}
   194 
   195 
   196 section {* Proof terms *}
   197 
   198 text {*
   199   FIXME
   200 *}
   201 
   202 
   203 section {* Theorems \label{sec:thms} *}
   204 
   205 text {*
   206 
   207   Primitive reasoning operates on judgments of the form @{text "\<Gamma> \<turnstile>
   208   \<phi>"}, with standard introduction and elimination rules for @{text
   209   "\<And>"} and @{text "\<Longrightarrow>"} that refer to fixed parameters @{text "x"} and
   210   hypotheses @{text "A"} from the context @{text "\<Gamma>"}.  The
   211   corresponding proof terms are left implicit in the classic
   212   ``LCF-approach'', although they could be exploited separately
   213   \cite{Berghofer-Nipkow:2000}.
   214 
   215   The framework also provides definitional equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha>
   216   \<Rightarrow> prop"}, with @{text "\<alpha>\<beta>\<eta>"}-conversion rules.  The internal
   217   conjunction @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} enables the view of
   218   assumptions and conclusions emerging uniformly as simultaneous
   219   statements.
   220 
   221 
   222 
   223   FIXME
   224 
   225 \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
   226 @{text "prop"}.  Internally, there is nothing special about
   227 propositions apart from their type, but the concrete syntax enforces a
   228 clear distinction.  Propositions are structured via implication @{text
   229 "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
   230 else is considered atomic.  The canonical form for propositions is
   231 that of a \seeglossary{Hereditary Harrop Formula}.}
   232 
   233 \glossary{Theorem}{A proven proposition within a certain theory and
   234 proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
   235 rarely spelled out explicitly.  Theorems are usually normalized
   236 according to the \seeglossary{HHF} format.}
   237 
   238 \glossary{Fact}{Sometimes used interchangably for
   239 \seeglossary{theorem}.  Strictly speaking, a list of theorems,
   240 essentially an extra-logical conjunction.  Facts emerge either as
   241 local assumptions, or as results of local goal statements --- both may
   242 be simultaneous, hence the list representation.}
   243 
   244 \glossary{Schematic variable}{FIXME}
   245 
   246 \glossary{Fixed variable}{A variable that is bound within a certain
   247 proof context; an arbitrary-but-fixed entity within a portion of proof
   248 text.}
   249 
   250 \glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
   251 
   252 \glossary{Bound variable}{FIXME}
   253 
   254 \glossary{Variable}{See \seeglossary{schematic variable},
   255 \seeglossary{fixed variable}, \seeglossary{bound variable}, or
   256 \seeglossary{type variable}.  The distinguishing feature of different
   257 variables is their binding scope.}
   258 
   259 *}
   260 
   261 subsection {* Primitive inferences *}
   262 
   263 text FIXME
   264 
   265 
   266 subsection {* Higher-order resolution *}
   267 
   268 text {*
   269 
   270 FIXME
   271 
   272 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
   273 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
   274 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
   275 Any proposition may be put into HHF form by normalizing with the rule
   276 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
   277 quantifier prefix is represented via \seeglossary{schematic
   278 variables}, such that the top-level structure is merely that of a
   279 \seeglossary{Horn Clause}}.
   280 
   281 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
   282 
   283 *}
   284 
   285 subsection {* Equational reasoning *}
   286 
   287 text FIXME
   288 
   289 
   290 end