doc-src/IsarImplementation/Thy/logic.thy
author wenzelm
Tue Sep 12 21:05:39 2006 +0200 (2006-09-12)
changeset 20521 189811b39869
parent 20520 05fd007bdeb9
child 20537 b6b49903db7e
permissions -rw-r--r--
more on theorems;
     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} @{text "\<tau>"} is defined inductively over type variables
    82   and type constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s |
    83   ?\<alpha>\<^isub>s | (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)k"}.
    84 
    85   A \emph{type abbreviation} is a syntactic definition @{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 component-wise.
   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 map_atyps: "(typ -> typ) -> typ -> typ"} \\
   126   @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
   127   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
   128   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
   129   @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\
   130   @{index_ML Sign.add_tyabbrs_i: "
   131   (string * string list * typ * mixfix) list -> theory -> theory"} \\
   132   @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
   133   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
   134   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
   135   \end{mldecls}
   136 
   137   \begin{description}
   138 
   139   \item @{ML_type class} represents type classes; this is an alias for
   140   @{ML_type string}.
   141 
   142   \item @{ML_type sort} represents sorts; this is an alias for
   143   @{ML_type "class list"}.
   144 
   145   \item @{ML_type arity} represents type arities; this is an alias for
   146   triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::
   147   (\<^vec>s)s"} described above.
   148 
   149   \item @{ML_type typ} represents types; this is a datatype with
   150   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
   151 
   152   \item @{ML map_atyps}~@{text "f \<tau>"} applies mapping @{text "f"} to
   153   all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text "\<tau>"}.
   154 
   155   \item @{ML fold_atyps}~@{text "f \<tau>"} iterates operation @{text "f"}
   156   over all occurrences of atoms (@{ML TFree}, @{ML TVar}) in @{text
   157   "\<tau>"}; the type structure is traversed from left to right.
   158 
   159   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
   160   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
   161 
   162   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
   163   is of a given sort.
   164 
   165   \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares new
   166   type constructors @{text "\<kappa>"} with @{text "k"} arguments and
   167   optional mixfix syntax.
   168 
   169   \item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
   170   defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with
   171   optional mixfix syntax.
   172 
   173   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
   174   c\<^isub>n])"} declares new class @{text "c"}, together with class
   175   relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
   176 
   177   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
   178   c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
   179   c\<^isub>2"}.
   180 
   181   \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares
   182   arity @{text "\<kappa> :: (\<^vec>s)s"}.
   183 
   184   \end{description}
   185 *}
   186 
   187 
   188 
   189 section {* Terms \label{sec:terms} *}
   190 
   191 text {*
   192   \glossary{Term}{FIXME}
   193 
   194   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
   195   with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
   196   or \cite{paulson-ml2}), and named free variables and constants.
   197   Terms with loose bound variables are usually considered malformed.
   198   The types of variables and constants is stored explicitly at each
   199   occurrence in the term.
   200 
   201   \medskip A \emph{bound variable} is a natural number @{text "b"},
   202   which refers to the next binder that is @{text "b"} steps upwards
   203   from the occurrence of @{text "b"} (counting from zero).  Bindings
   204   may be introduced as abstractions within the term, or as a separate
   205   context (an inside-out list).  This associates each bound variable
   206   with a type.  A \emph{loose variables} is a bound variable that is
   207   outside the current scope of local binders or the context.  For
   208   example, the de-Bruijn term @{text "\<lambda>\<^isub>\<tau>. \<lambda>\<^isub>\<tau>. 1 + 0"}
   209   corresponds to @{text "\<lambda>x\<^isub>\<tau>. \<lambda>y\<^isub>\<tau>. x + y"} in a named
   210   representation.  Also note that the very same bound variable may get
   211   different numbers at different occurrences.
   212 
   213   A \emph{fixed variable} is a pair of a basic name and a type.  For
   214   example, @{text "(x, \<tau>)"} which is usually printed @{text
   215   "x\<^isub>\<tau>"}.  A \emph{schematic variable} is a pair of an
   216   indexname and a type.  For example, @{text "((x, 0), \<tau>)"} which is
   217   usually printed as @{text "?x\<^isub>\<tau>"}.
   218 
   219   \medskip A \emph{constant} is a atomic terms consisting of a basic
   220   name and a type.  Constants are declared in the context as
   221   polymorphic families @{text "c :: \<sigma>"}, meaning that any @{text
   222   "c\<^isub>\<tau>"} is a valid constant for all substitution instances
   223   @{text "\<tau> \<le> \<sigma>"}.
   224 
   225   The list of \emph{type arguments} of @{text "c\<^isub>\<tau>"} wrt.\ the
   226   declaration @{text "c :: \<sigma>"} is the codomain of the type matcher
   227   presented in canonical order (according to the left-to-right
   228   occurrences of type variables in in @{text "\<sigma>"}).  Thus @{text
   229   "c\<^isub>\<tau>"} can be represented more compactly as @{text
   230   "c(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}.  For example, the instance @{text
   231   "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow> nat\<^esub>"} of some @{text "plus :: \<alpha> \<Rightarrow> \<alpha>
   232   \<Rightarrow> \<alpha>"} has the singleton list @{text "nat"} as type arguments, the
   233   constant may be represented as @{text "plus(nat)"}.
   234 
   235   Constant declarations @{text "c :: \<sigma>"} may contain sort constraints
   236   for type variables in @{text "\<sigma>"}.  These are observed by
   237   type-inference as expected, but \emph{ignored} by the core logic.
   238   This means the primitive logic is able to reason with instances of
   239   polymorphic constants that the user-level type-checker would reject.
   240 
   241   \medskip A \emph{term} @{text "t"} is defined inductively over
   242   variables and constants, with abstraction and application as
   243   follows: @{text "t = b | x\<^isub>\<tau> | ?x\<^isub>\<tau> | c\<^isub>\<tau> |
   244   \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}.  Parsing and printing takes
   245   care of converting between an external representation with named
   246   bound variables.  Subsequently, we shall use the latter notation
   247   instead of internal de-Bruijn representation.
   248 
   249   The subsequent inductive relation @{text "t :: \<tau>"} assigns a
   250   (unique) type to a term, using the special type constructor @{text
   251   "(\<alpha>, \<beta>)fun"}, which is written @{text "\<alpha> \<Rightarrow> \<beta>"}.
   252   \[
   253   \infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{}
   254   \qquad
   255   \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}}
   256   \qquad
   257   \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}}
   258   \]
   259   A \emph{well-typed term} is a term that can be typed according to these rules.
   260 
   261   Typing information can be omitted: type-inference is able to
   262   reconstruct the most general type of a raw term, while assigning
   263   most general types to all of its variables and constants.
   264   Type-inference depends on a context of type constraints for fixed
   265   variables, and declarations for polymorphic constants.
   266 
   267   The identity of atomic terms consists both of the name and the type.
   268   Thus different entities @{text "c\<^bsub>\<tau>\<^isub>1\<^esub>"} and
   269   @{text "c\<^bsub>\<tau>\<^isub>2\<^esub>"} may well identified by type
   270   instantiation, by mapping @{text "\<tau>\<^isub>1"} and @{text
   271   "\<tau>\<^isub>2"} to the same @{text "\<tau>"}.  Although,
   272   different type instances of constants of the same basic name are
   273   commonplace, this rarely happens for variables: type-inference
   274   always demands ``consistent'' type constraints.
   275 
   276   \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
   277   is the set of type variables occurring in @{text "t"}, but not in
   278   @{text "\<sigma>"}.  This means that the term implicitly depends on the
   279   values of various type variables that are not visible in the overall
   280   type, i.e.\ there are different type instances @{text "t\<vartheta>
   281   :: \<sigma>"} and @{text "t\<vartheta>' :: \<sigma>"} with the same type.  This
   282   slightly pathological situation is apt to cause strange effects.
   283 
   284   \medskip A \emph{term abbreviation} is a syntactic definition @{text
   285   "c\<^isub>\<sigma> \<equiv> t"} of an arbitrary closed term @{text "t"} of type
   286   @{text "\<sigma>"} without any hidden polymorphism.  A term abbreviation
   287   looks like a constant at the surface, but is fully expanded before
   288   entering the logical core.  Abbreviations are usually reverted when
   289   printing terms, using rules @{text "t \<rightarrow> c\<^isub>\<sigma>"} has a
   290   higher-order term rewrite system.
   291 
   292   \medskip Canonical operations on @{text "\<lambda>"}-terms include @{text
   293   "\<alpha>\<beta>\<eta>"}-conversion. @{text "\<alpha>"}-conversion refers to capture-free
   294   renaming of bound variables; @{text "\<beta>"}-conversion contracts an
   295   abstraction applied to some argument term, substituting the argument
   296   in the body: @{text "(\<lambda>x. b)a"} becomes @{text "b[a/x]"}; @{text
   297   "\<eta>"}-conversion contracts vacuous application-abstraction: @{text
   298   "\<lambda>x. f x"} becomes @{text "f"}, provided that the bound variable
   299   @{text "0"} does not occur in @{text "f"}.
   300 
   301   Terms are almost always treated module @{text "\<alpha>"}-conversion, which
   302   is implicit in the de-Bruijn representation.  The names in
   303   abstractions of bound variables are maintained only as a comment for
   304   parsing and printing.  Full @{text "\<alpha>\<beta>\<eta>"}-equivalence is usually
   305   taken for granted higher rules (\secref{sec:rules}), anything
   306   depending on higher-order unification or rewriting.
   307 *}
   308 
   309 text %mlref {*
   310   \begin{mldecls}
   311   @{index_ML_type term} \\
   312   @{index_ML "op aconv": "term * term -> bool"} \\
   313   @{index_ML map_term_types: "(typ -> typ) -> term -> term"} \\  %FIXME rename map_types
   314   @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   315   @{index_ML map_aterms: "(term -> term) -> term -> term"} \\
   316   @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   317   @{index_ML fastype_of: "term -> typ"} \\
   318   @{index_ML lambda: "term -> term -> term"} \\
   319   @{index_ML betapply: "term * term -> term"} \\
   320   @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
   321   @{index_ML Sign.add_abbrevs: "string * bool ->
   322   ((string * mixfix) * term) list -> theory -> theory"} \\
   323   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
   324   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
   325   \end{mldecls}
   326 
   327   \begin{description}
   328 
   329   \item @{ML_type term} represents de-Bruijn terms with comments in
   330   abstractions for bound variable names.  This is a datatype with
   331   constructors @{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const}, @{ML
   332   Abs}, @{ML "op $"}.
   333 
   334   \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text
   335   "\<alpha>"}-equivalence of two terms.  This is the basic equality relation
   336   on type @{ML_type term}; raw datatype equality should only be used
   337   for operations related to parsing or printing!
   338 
   339   \item @{ML map_term_types}~@{text "f t"} applies mapping @{text "f"}
   340   to all types occurring in @{text "t"}.
   341 
   342   \item @{ML fold_types}~@{text "f t"} iterates operation @{text "f"}
   343   over all occurrences of types in @{text "t"}; the term structure is
   344   traversed from left to right.
   345 
   346   \item @{ML map_aterms}~@{text "f t"} applies mapping @{text "f"} to
   347   all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const})
   348   occurring in @{text "t"}.
   349 
   350   \item @{ML fold_aterms}~@{text "f t"} iterates operation @{text "f"}
   351   over all occurrences of atomic terms in (@{ML Bound}, @{ML Free},
   352   @{ML Var}, @{ML Const}) @{text "t"}; the term structure is traversed
   353   from left to right.
   354 
   355   \item @{ML fastype_of}~@{text "t"} recomputes the type of a
   356   well-formed term, while omitting any sanity checks.  This operation
   357   is relatively slow.
   358 
   359   \item @{ML lambda}~@{text "a b"} produces an abstraction @{text
   360   "\<lambda>a. b"}, where occurrences of the original (atomic) term @{text
   361   "a"} in the body @{text "b"} are replaced by bound variables.
   362 
   363   \item @{ML betapply}~@{text "t u"} produces an application @{text "t
   364   u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} happens to
   365   be an abstraction.
   366 
   367   \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
   368   new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
   369 
   370   \item @{ML Sign.add_abbrevs}~@{text "print_mode [((c, t), mx), \<dots>]"}
   371   declares a new term abbreviation @{text "c \<equiv> t"} with optional
   372   mixfix syntax.
   373 
   374   \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
   375   Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
   376   convert between the two representations of constants, namely full
   377   type instance vs.\ compact type arguments form (depending on the
   378   most general declaration given in the context).
   379 
   380   \end{description}
   381 *}
   382 
   383 
   384 section {* Theorems \label{sec:thms} *}
   385 
   386 text {*
   387   \glossary{Proposition}{FIXME A \seeglossary{term} of
   388   \seeglossary{type} @{text "prop"}.  Internally, there is nothing
   389   special about propositions apart from their type, but the concrete
   390   syntax enforces a clear distinction.  Propositions are structured
   391   via implication @{text "A \<Longrightarrow> B"} or universal quantification @{text
   392   "\<And>x. B x"} --- anything else is considered atomic.  The canonical
   393   form for propositions is that of a \seeglossary{Hereditary Harrop
   394   Formula}. FIXME}
   395 
   396   \glossary{Theorem}{A proven proposition within a certain theory and
   397   proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
   398   rarely spelled out explicitly.  Theorems are usually normalized
   399   according to the \seeglossary{HHF} format. FIXME}
   400 
   401   \glossary{Fact}{Sometimes used interchangeably for
   402   \seeglossary{theorem}.  Strictly speaking, a list of theorems,
   403   essentially an extra-logical conjunction.  Facts emerge either as
   404   local assumptions, or as results of local goal statements --- both
   405   may be simultaneous, hence the list representation. FIXME}
   406 
   407   \glossary{Schematic variable}{FIXME}
   408 
   409   \glossary{Fixed variable}{A variable that is bound within a certain
   410   proof context; an arbitrary-but-fixed entity within a portion of
   411   proof text. FIXME}
   412 
   413   \glossary{Free variable}{Synonymous for \seeglossary{fixed
   414   variable}. FIXME}
   415 
   416   \glossary{Bound variable}{FIXME}
   417 
   418   \glossary{Variable}{See \seeglossary{schematic variable},
   419   \seeglossary{fixed variable}, \seeglossary{bound variable}, or
   420   \seeglossary{type variable}.  The distinguishing feature of
   421   different variables is their binding scope. FIXME}
   422 
   423   A \emph{proposition} is a well-formed term of type @{text "prop"}, a
   424   \emph{theorem} is a proven proposition (depending on a context of
   425   hypotheses and the background theory).  Primitive inferences include
   426   plain natural deduction rules for the primary connectives @{text
   427   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There are separate (derived)
   428   rules for equality/equivalence @{text "\<equiv>"} and internal conjunction
   429   @{text "&"}.
   430 *}
   431 
   432 subsection {* Standard connectives and rules *}
   433 
   434 text {*
   435   The basic theory is called @{text "Pure"}, it contains declarations
   436   for the standard logical connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and
   437   @{text "\<equiv>"} of the framework, see \figref{fig:pure-connectives}.
   438   The derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is
   439   defined inductively by the primitive inferences given in
   440   \figref{fig:prim-rules}, with the global syntactic restriction that
   441   hypotheses may never contain schematic variables.  The builtin
   442   equality is conceptually axiomatized shown in
   443   \figref{fig:pure-equality}, although the implementation works
   444   directly with (derived) inference rules.
   445 
   446   \begin{figure}[htb]
   447   \begin{center}
   448   \begin{tabular}{ll}
   449   @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
   450   @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
   451   @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
   452   \end{tabular}
   453   \caption{Standard connectives of Pure}\label{fig:pure-connectives}
   454   \end{center}
   455   \end{figure}
   456 
   457   \begin{figure}[htb]
   458   \begin{center}
   459   \[
   460   \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}}
   461   \qquad
   462   \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}
   463   \]
   464   \[
   465   \infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b x"}}{@{text "\<Gamma> \<turnstile> b x"} & @{text "x \<notin> \<Gamma>"}}
   466   \qquad
   467   \infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b a"}}{@{text "\<Gamma> \<turnstile> \<And>x. b x"}}
   468   \]
   469   \[
   470   \infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
   471   \qquad
   472   \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"}}
   473   \]
   474   \caption{Primitive inferences of Pure}\label{fig:prim-rules}
   475   \end{center}
   476   \end{figure}
   477 
   478   \begin{figure}[htb]
   479   \begin{center}
   480   \begin{tabular}{ll}
   481   @{text "\<turnstile> (\<lambda>x. b x) a \<equiv> b a"} & @{text "\<beta>"}-conversion \\
   482   @{text "\<turnstile> x \<equiv> x"} & reflexivity \\
   483   @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\
   484   @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
   485   @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & coincidence with equivalence \\
   486   \end{tabular}
   487   \caption{Conceptual axiomatization of builtin equality}\label{fig:pure-equality}
   488   \end{center}
   489   \end{figure}
   490 
   491   The introduction and elimination rules for @{text "\<And>"} and @{text
   492   "\<Longrightarrow>"} are analogous to formation of (dependently typed) @{text
   493   "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
   494   are \emph{irrelevant} in the Pure logic, they may never occur within
   495   propositions, i.e.\ the @{text "\<Longrightarrow>"} arrow is non-dependent.  The
   496   system provides a runtime option to record explicit proof terms for
   497   primitive inferences, cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}.  Thus
   498   the three-fold @{text "\<lambda>"}-structure can be made explicit.
   499 
   500   Observe that locally fixed parameters (as used in rule @{text
   501   "\<And>_intro"}) need not be recorded in the hypotheses, because the
   502   simple syntactic types of Pure are always inhabitable.  The typing
   503   ``assumption'' @{text "x :: \<tau>"} is logically vacuous, it disappears
   504   automatically whenever the statement body ceases to mention variable
   505   @{text "x\<^isub>\<tau>"}.\footnote{This greatly simplifies many basic
   506   reasoning steps, and is the key difference to the formulation of
   507   this logic as ``@{text "\<lambda>HOL"}'' in the PTS framework
   508   \cite{Barendregt-Geuvers:2001}.}
   509 
   510   \medskip FIXME @{text "\<alpha>\<beta>\<eta>"}-equivalence and primitive definitions
   511 
   512   Since the basic representation of terms already accounts for @{text
   513   "\<alpha>"}-conversion, Pure equality essentially acts like @{text
   514   "\<alpha>\<beta>\<eta>"}-equivalence on terms, while coinciding with bi-implication.
   515 
   516   \medskip The axiomatization of a theory is implicitly closed by
   517   forming all instances of type and term variables: @{text "\<turnstile> A\<vartheta>"} for
   518   any substitution instance of axiom @{text "\<turnstile> A"}.  By pushing
   519   substitution through derivations inductively, we get admissible
   520   substitution rules for theorems shown in \figref{fig:subst-rules}.
   521   Alternatively, the term substitution rules could be derived from
   522   @{text "\<And>_intro/elim"}.  The versions for types are genuine
   523   admissible rules, due to the lack of true polymorphism in the logic.
   524 
   525   \begin{figure}[htb]
   526   \begin{center}
   527   \[
   528   \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}
   529   \quad
   530   \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}
   531   \]
   532   \[
   533   \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}
   534   \quad
   535   \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}
   536   \]
   537   \caption{Admissible substitution rules}\label{fig:subst-rules}
   538   \end{center}
   539   \end{figure}
   540 
   541   Since @{text "\<Gamma>"} may never contain any schematic variables, the
   542   @{text "instantiate"} do not require an explicit side-condition.  In
   543   principle, variables could be substituted in hypotheses as well, but
   544   this could disrupt monotonicity of the basic calculus: derivations
   545   could leave the current proof context.
   546 *}
   547 
   548 text %mlref {*
   549   \begin{mldecls}
   550   @{index_ML_type ctyp} \\
   551   @{index_ML_type cterm} \\
   552   @{index_ML_type thm} \\
   553   \end{mldecls}
   554 
   555   \begin{description}
   556 
   557   \item @{ML_type ctyp} FIXME
   558 
   559   \item @{ML_type cterm} FIXME
   560 
   561   \item @{ML_type thm} FIXME
   562 
   563   \end{description}
   564 *}
   565 
   566 
   567 subsection {* Auxiliary connectives *}
   568 
   569 text {*
   570   Pure also provides various auxiliary connectives based on primitive
   571   definitions, see \figref{fig:pure-aux}.  These are normally not
   572   exposed to the user, but appear in internal encodings only.
   573 
   574   \begin{figure}[htb]
   575   \begin{center}
   576   \begin{tabular}{ll}
   577   @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&"}) \\
   578   @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\[1ex]
   579   @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}) \\
   580   @{text "#A \<equiv> A"} \\[1ex]
   581   @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\
   582   @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]
   583   @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
   584   @{text "(unspecified)"} \\
   585   \end{tabular}
   586   \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
   587   \end{center}
   588   \end{figure}
   589 
   590   Conjunction as an explicit connective allows to treat both
   591   simultaneous assumptions and conclusions uniformly.  The definition
   592   allows to derive the usual introduction @{text "\<turnstile> A \<Longrightarrow> B \<Longrightarrow> A & B"},
   593   and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B \<Longrightarrow> B"}.  For
   594   example, several claims may be stated at the same time, which is
   595   intermediately represented as an assumption, but the user only
   596   encounters several sub-goals, and several resulting facts in the
   597   very end (cf.\ \secref{sec:tactical-goals}).
   598 
   599   The @{text "#"} marker allows complex propositions (nested @{text
   600   "\<And>"} and @{text "\<Longrightarrow>"}) to appear formally as atomic, without changing
   601   the meaning: @{text "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are
   602   interchangeable.  See \secref{sec:tactical-goals} for specific
   603   operations.
   604 
   605   The @{text "TERM"} marker turns any well-formed term into a
   606   derivable proposition: @{text "\<turnstile> TERM t"} holds
   607   unconditionally.  Despite its logically vacous meaning, this is
   608   occasionally useful to treat syntactic terms and proven propositions
   609   uniformly, as in a type-theoretic framework.
   610 
   611   The @{text "TYPE"} constructor (which is the canonical
   612   representative of the unspecified type @{text "\<alpha> itself"}) injects
   613   the language of types into that of terms.  There is specific
   614   notation @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau>
   615  itself\<^esub>"}.
   616   Although being devoid of any particular meaning, the term @{text
   617   "TYPE(\<tau>)"} is able to carry the type @{text "\<tau>"} formally.  @{text
   618   "TYPE(\<alpha>)"} may be used as an additional formal argument in primitive
   619   definitions, in order to avoid hidden polymorphism (cf.\
   620   \secref{sec:terms}).  For example, @{text "c TYPE(\<alpha>) \<equiv> A[\<alpha>]"} turns
   621   out as a formally correct definition of some proposition @{text "A"}
   622   that depends on an additional type argument.
   623 *}
   624 
   625 text %mlref {*
   626   \begin{mldecls}
   627   @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\
   628   @{index_ML Conjunction.elim: "thm -> thm * thm"} \\
   629   @{index_ML Drule.mk_term: "cterm -> thm"} \\
   630   @{index_ML Drule.dest_term: "thm -> cterm"} \\
   631   @{index_ML Logic.mk_type: "typ -> term"} \\
   632   @{index_ML Logic.dest_type: "term -> typ"} \\
   633   \end{mldecls}
   634 
   635   \begin{description}
   636 
   637   \item FIXME
   638 
   639   \end{description}
   640 *}
   641 
   642 
   643 section {* Rules \label{sec:rules} *}
   644 
   645 text {*
   646 
   647 FIXME
   648 
   649   A \emph{rule} is any Pure theorem in HHF normal form; there is a
   650   separate calculus for rule composition, which is modeled after
   651   Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows
   652   rules to be nested arbitrarily, similar to \cite{extensions91}.
   653 
   654   Normally, all theorems accessible to the user are proper rules.
   655   Low-level inferences are occasional required internally, but the
   656   result should be always presented in canonical form.  The higher
   657   interfaces of Isabelle/Isar will always produce proper rules.  It is
   658   important to maintain this invariant in add-on applications!
   659 
   660   There are two main principles of rule composition: @{text
   661   "resolution"} (i.e.\ backchaining of rules) and @{text
   662   "by-assumption"} (i.e.\ closing a branch); both principles are
   663   combined in the variants of @{text "elim-resolution"} and @{text
   664   "dest-resolution"}.  Raw @{text "composition"} is occasionally
   665   useful as well, also it is strictly speaking outside of the proper
   666   rule calculus.
   667 
   668   Rules are treated modulo general higher-order unification, which is
   669   unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion
   670   on @{text "\<lambda>"}-terms.  Moreover, propositions are understood modulo
   671   the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.
   672 
   673   This means that any operations within the rule calculus may be
   674   subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions.  It is common
   675   practice not to contract or expand unnecessarily.  Some mechanisms
   676   prefer an one form, others the opposite, so there is a potential
   677   danger to produce some oscillation!
   678 
   679   Only few operations really work \emph{modulo} HHF conversion, but
   680   expect a normal form: quantifiers @{text "\<And>"} before implications
   681   @{text "\<Longrightarrow>"} at each level of nesting.
   682 
   683 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
   684 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
   685 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
   686 Any proposition may be put into HHF form by normalizing with the rule
   687 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
   688 quantifier prefix is represented via \seeglossary{schematic
   689 variables}, such that the top-level structure is merely that of a
   690 \seeglossary{Horn Clause}}.
   691 
   692 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
   693 
   694 
   695   \[
   696   \infer[@{text "(assumption)"}]{@{text "C\<vartheta>"}}
   697   {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text i})}}
   698   \]
   699 
   700 
   701   \[
   702   \infer[@{text "(compose)"}]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}
   703   {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}
   704   \]
   705 
   706 
   707   \[
   708   \infer[@{text "(\<And>_lift)"}]{@{text "(\<And>\<^vec>x. \<^vec>A (?\<^vec>a \<^vec>x)) \<Longrightarrow> (\<And>\<^vec>x. B (?\<^vec>a \<^vec>x))"}}{@{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"}}
   709   \]
   710   \[
   711   \infer[@{text "(\<Longrightarrow>_lift)"}]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}
   712   \]
   713 
   714   The @{text resolve} scheme is now acquired from @{text "\<And>_lift"},
   715   @{text "\<Longrightarrow>_lift"}, and @{text compose}.
   716 
   717   \[
   718   \infer[@{text "(resolution)"}]
   719   {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}
   720   {\begin{tabular}{l}
   721     @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\
   722     @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\
   723     @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\
   724    \end{tabular}}
   725   \]
   726 
   727 
   728   FIXME @{text "elim_resolution"}, @{text "dest_resolution"}
   729 *}
   730 
   731 
   732 end