doc-src/IsarImplementation/Thy/logic.thy
author wenzelm
Tue Sep 12 14:50:11 2006 +0200 (2006-09-12)
changeset 20514 5ede702cd2ca
parent 20501 de0b523b0d62
child 20519 d7ad1217c24a
permissions -rw-r--r--
more on terms;
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} @{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 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 variables
   192   and constants.  Terms with loose bound variables are usually
   193   considered malformed.  The types of variables and constants is
   194   stored explicitly at each occurrence in the term.
   195 
   196   \medskip A \emph{bound variable} is a natural number @{text "b"},
   197   which refers to the next binder that is @{text "b"} steps upwards
   198   from the occurrence of @{text "b"} (counting from zero).  Bindings
   199   may be introduced as abstractions within the term, or as a separate
   200   context (an inside-out list).  This associates each bound variable
   201   with a type, and a name that is maintained as a comment for parsing
   202   and printing.  A \emph{loose variables} is a bound variable that is
   203   outside the current scope of local binders or the context.  For
   204   example, the de-Bruijn term @{text "\<lambda>\<^isub>\<tau>. \<lambda>\<^isub>\<tau>. 1 + 0"}
   205   corresponds to @{text "\<lambda>x\<^isub>\<tau>. \<lambda>y\<^isub>\<tau>. x + y"} in a named
   206   representation.  Also note that the very same bound variable may get
   207   different numbers at different occurrences.
   208 
   209   A \emph{fixed variable} is a pair of a basic name and a type.  For
   210   example, @{text "(x, \<tau>)"} which is usually printed @{text
   211   "x\<^isub>\<tau>"}.  A \emph{schematic variable} is a pair of an
   212   indexname and a type.  For example, @{text "((x, 0), \<tau>)"} which is
   213   usually printed as @{text "?x\<^isub>\<tau>"}.
   214 
   215   \medskip A \emph{constant} is a atomic terms consisting of a basic
   216   name and a type.  Constants are declared in the context as
   217   polymorphic families @{text "c :: \<sigma>"}, meaning that any @{text
   218   "c\<^isub>\<tau>"} is a valid constant for all substitution instances
   219   @{text "\<tau> \<le> \<sigma>"}.
   220 
   221   The list of \emph{type arguments} of @{text "c\<^isub>\<tau>"} wrt.\ the
   222   declaration @{text "c :: \<sigma>"} is the codomain of the type matcher
   223   presented in canonical order (according to the left-to-right
   224   occurrences of type variables in in @{text "\<sigma>"}).  Thus @{text
   225   "c\<^isub>\<tau>"} can be represented more compactly as @{text
   226   "c(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}.  For example, the instance @{text
   227   "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow> nat\<^esub>"} of some @{text "plus :: \<alpha> \<Rightarrow> \<alpha>
   228   \<Rightarrow> \<alpha>"} has the singleton list @{text "nat"} as type arguments, the
   229   constant may be represented as @{text "plus(nat)"}.
   230 
   231   Constant declarations @{text "c :: \<sigma>"} may contain sort constraints
   232   for type variables in @{text "\<sigma>"}.  These are observed by
   233   type-inference as expected, but \emph{ignored} by the core logic.
   234   This means the primitive logic is able to reason with instances of
   235   polymorphic constants that the user-level type-checker would reject.
   236 
   237   \medskip A \emph{term} @{text "t"} is defined inductively over
   238   variables and constants, with abstraction and application as
   239   follows: @{text "t = b | x\<^isub>\<tau> | ?x\<^isub>\<tau> | c\<^isub>\<tau> |
   240   \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}.  Parsing and printing takes
   241   care of converting between an external representation with named
   242   bound variables.  Subsequently, we shall use the latter notation
   243   instead of internal de-Bruijn representation.
   244 
   245   The subsequent inductive relation @{text "t :: \<tau>"} assigns a
   246   (unique) type to a term, using the special type constructor @{text
   247   "(\<alpha>, \<beta>)fun"}, which is written @{text "\<alpha> \<Rightarrow> \<beta>"}.
   248   \[
   249   \infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{}
   250   \qquad
   251   \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}}
   252   \qquad
   253   \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}}
   254   \]
   255   A \emph{well-typed term} is a term that can be typed according to these rules.
   256 
   257   Typing information can be omitted: type-inference is able to
   258   reconstruct the most general type of a raw term, while assigning
   259   most general types to all of its variables and constants.
   260   Type-inference depends on a context of type constraints for fixed
   261   variables, and declarations for polymorphic constants.
   262 
   263   The identity of atomic terms consists both of the name and the type.
   264   Thus different entities @{text "c\<^bsub>\<tau>\<^isub>1\<^esub>"} and
   265   @{text "c\<^bsub>\<tau>\<^isub>2\<^esub>"} may well identified by type
   266   instantiation, by mapping @{text "\<tau>\<^isub>1"} and @{text
   267   "\<tau>\<^isub>2"} to the same @{text "\<tau>"}.  Although,
   268   different type instances of constants of the same basic name are
   269   commonplace, this rarely happens for variables: type-inference
   270   always demands ``consistent'' type constraints.
   271 
   272   \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}
   273   is the set of type variables occurring in @{text "t"}, but not in
   274   @{text "\<sigma>"}.  This means that the term implicitly depends on the
   275   values of various type variables that are not visible in the overall
   276   type, i.e.\ there are different type instances @{text "t\<vartheta>
   277   :: \<sigma>"} and @{text "t\<vartheta>' :: \<sigma>"} with the same type.  This
   278   slightly pathological situation is apt to cause strange effects.
   279 
   280   \medskip A \emph{term abbreviation} is a syntactic definition @{text
   281   "c\<^isub>\<sigma> \<equiv> t"} of an arbitrary closed term @{text "t"} of type
   282   @{text "\<sigma>"} without any hidden polymorphism.  A term abbreviation
   283   looks like a constant at the surface, but is fully expanded before
   284   entering the logical core.  Abbreviations are usually reverted when
   285   printing terms, using rules @{text "t \<rightarrow> c\<^isub>\<sigma>"} has a
   286   higher-order term rewrite system.
   287 *}
   288 
   289 text %mlref {*
   290   \begin{mldecls}
   291   @{index_ML_type term} \\
   292   @{index_ML map_aterms: "(term -> term) -> term -> term"} \\
   293   @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   294   @{index_ML fastype_of: "term -> typ"} \\
   295   @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   296   \end{mldecls}
   297 
   298   \begin{description}
   299 
   300   \item @{ML_type term} FIXME
   301 
   302   \end{description}
   303 *}
   304 
   305 
   306 section {* Theorems \label{sec:thms} *}
   307 
   308 text {*
   309   \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
   310   @{text "prop"}.  Internally, there is nothing special about
   311   propositions apart from their type, but the concrete syntax enforces
   312   a clear distinction.  Propositions are structured via implication
   313   @{text "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} ---
   314   anything else is considered atomic.  The canonical form for
   315   propositions is that of a \seeglossary{Hereditary Harrop Formula}. FIXME}
   316 
   317   \glossary{Theorem}{A proven proposition within a certain theory and
   318   proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
   319   rarely spelled out explicitly.  Theorems are usually normalized
   320   according to the \seeglossary{HHF} format. FIXME}
   321 
   322   \glossary{Fact}{Sometimes used interchangably for
   323   \seeglossary{theorem}.  Strictly speaking, a list of theorems,
   324   essentially an extra-logical conjunction.  Facts emerge either as
   325   local assumptions, or as results of local goal statements --- both
   326   may be simultaneous, hence the list representation. FIXME}
   327 
   328   \glossary{Schematic variable}{FIXME}
   329 
   330   \glossary{Fixed variable}{A variable that is bound within a certain
   331   proof context; an arbitrary-but-fixed entity within a portion of
   332   proof text. FIXME}
   333 
   334   \glossary{Free variable}{Synonymous for \seeglossary{fixed
   335   variable}. FIXME}
   336 
   337   \glossary{Bound variable}{FIXME}
   338 
   339   \glossary{Variable}{See \seeglossary{schematic variable},
   340   \seeglossary{fixed variable}, \seeglossary{bound variable}, or
   341   \seeglossary{type variable}.  The distinguishing feature of
   342   different variables is their binding scope. FIXME}
   343 
   344   A \emph{proposition} is a well-formed term of type @{text "prop"}.
   345   The connectives of minimal logic are declared as constants of the
   346   basic theory:
   347 
   348   \smallskip
   349   \begin{tabular}{ll}
   350   @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
   351   @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
   352   \end{tabular}
   353 
   354   \medskip A \emph{theorem} is a proven proposition, depending on a
   355   collection of assumptions, and axioms from the theory context.  The
   356   judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is defined
   357   inductively by the primitive inferences given in
   358   \figref{fig:prim-rules}; there is a global syntactic restriction
   359   that the hypotheses may not contain schematic variables.
   360 
   361   \begin{figure}[htb]
   362   \begin{center}
   363   \[
   364   \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}}
   365   \qquad
   366   \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}
   367   \]
   368   \[
   369   \infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b x"}}{@{text "\<Gamma> \<turnstile> b x"} & @{text "x \<notin> \<Gamma>"}}
   370   \qquad
   371   \infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b a"}}{@{text "\<Gamma> \<turnstile> \<And>x. b x"}}
   372   \]
   373   \[
   374   \infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
   375   \qquad
   376   \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"}}
   377   \]
   378   \caption{Primitive inferences of the Pure logic}\label{fig:prim-rules}
   379   \end{center}
   380   \end{figure}
   381 
   382   The introduction and elimination rules for @{text "\<And>"} and @{text
   383   "\<Longrightarrow>"} are analogous to formation of (dependently typed) @{text
   384   "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
   385   are \emph{irrelevant} in the Pure logic, they may never occur within
   386   propositions, i.e.\ the @{text "\<Longrightarrow>"} arrow of the framework is a
   387   non-dependent one.
   388 
   389   Also note that fixed parameters as in @{text "\<And>_intro"} need not be
   390   recorded in the context @{text "\<Gamma>"}, since syntactic types are
   391   always inhabitable.  An ``assumption'' @{text "x :: \<tau>"} is logically
   392   vacuous, because @{text "\<tau>"} is always non-empty.  This is the deeper
   393   reason why @{text "\<Gamma>"} only consists of hypothetical proofs, but no
   394   hypothetical terms.
   395 
   396   The corresponding proof terms are left implicit in the classic
   397   ``LCF-approach'', although they could be exploited separately
   398   \cite{Berghofer-Nipkow:2000}.  The implementation provides a runtime
   399   option to control the generation of full proof terms.
   400 
   401   \medskip The axiomatization of a theory is implicitly closed by
   402   forming all instances of type and term variables: @{text "\<turnstile> A\<theta>"} for
   403   any substitution instance of axiom @{text "\<turnstile> A"}.  By pushing
   404   substitution through derivations inductively, we get admissible
   405   substitution rules for theorems shown in \figref{fig:subst-rules}.
   406 
   407   \begin{figure}[htb]
   408   \begin{center}
   409   \[
   410   \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}
   411   \quad
   412   \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}
   413   \]
   414   \[
   415   \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}
   416   \quad
   417   \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}
   418   \]
   419   \caption{Admissible substitution rules}\label{fig:subst-rules}
   420   \end{center}
   421   \end{figure}
   422 
   423   Note that @{text "instantiate_term"} could be derived using @{text
   424   "\<And>_intro/elim"}, but this is not how it is implemented.  The type
   425   instantiation rule is a genuine admissible one, due to the lack of
   426   true polymorphism in the logic.
   427 
   428   Since @{text "\<Gamma>"} may never contain any schematic variables, the
   429   @{text "instantiate"} do not require an explicit side-condition.  In
   430   principle, variables could be substituted in hypotheses as well, but
   431   this could disrupt monotonicity of the basic calculus: derivations
   432   could leave the current proof context.
   433 
   434   \medskip The framework also provides builtin equality @{text "\<equiv>"},
   435   which is conceptually axiomatized shown in \figref{fig:equality},
   436   although the implementation provides derived rules directly:
   437 
   438   \begin{figure}[htb]
   439   \begin{center}
   440   \begin{tabular}{ll}
   441   @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
   442   @{text "\<turnstile> (\<lambda>x. b x) a \<equiv> b a"} & @{text "\<beta>"}-conversion \\
   443   @{text "\<turnstile> x \<equiv> x"} & reflexivity law \\
   444   @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution law \\
   445   @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
   446   @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & coincidence with equivalence \\
   447   \end{tabular}
   448   \caption{Conceptual axiomatization of equality.}\label{fig:equality}
   449   \end{center}
   450   \end{figure}
   451 
   452   Since the basic representation of terms already accounts for @{text
   453   "\<alpha>"}-conversion, Pure equality essentially acts like @{text
   454   "\<alpha>\<beta>\<eta>"}-equivalence on terms, while coinciding with bi-implication.
   455 
   456 
   457   \medskip Conjunction is defined in Pure as a derived connective, see
   458   \figref{fig:conjunction}.  This is occasionally useful to represent
   459   simultaneous statements behind the scenes --- framework conjunction
   460   is usually not exposed to the user.
   461 
   462   \begin{figure}[htb]
   463   \begin{center}
   464   \begin{tabular}{ll}
   465   @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} & conjunction (hidden) \\
   466   @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\
   467   \end{tabular}
   468   \caption{Definition of conjunction.}\label{fig:equality}
   469   \end{center}
   470   \end{figure}
   471 
   472   The definition allows to derive the usual introduction @{text "\<turnstile> A \<Longrightarrow>
   473   B \<Longrightarrow> A & B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B
   474   \<Longrightarrow> B"}.
   475 *}
   476 
   477 
   478 section {* Rules \label{sec:rules} *}
   479 
   480 text {*
   481 
   482 FIXME
   483 
   484   A \emph{rule} is any Pure theorem in HHF normal form; there is a
   485   separate calculus for rule composition, which is modeled after
   486   Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows
   487   rules to be nested arbitrarily, similar to \cite{extensions91}.
   488 
   489   Normally, all theorems accessible to the user are proper rules.
   490   Low-level inferences are occasional required internally, but the
   491   result should be always presented in canonical form.  The higher
   492   interfaces of Isabelle/Isar will always produce proper rules.  It is
   493   important to maintain this invariant in add-on applications!
   494 
   495   There are two main principles of rule composition: @{text
   496   "resolution"} (i.e.\ backchaining of rules) and @{text
   497   "by-assumption"} (i.e.\ closing a branch); both principles are
   498   combined in the variants of @{text "elim-resosultion"} and @{text
   499   "dest-resolution"}.  Raw @{text "composition"} is occasionally
   500   useful as well, also it is strictly speaking outside of the proper
   501   rule calculus.
   502 
   503   Rules are treated modulo general higher-order unification, which is
   504   unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion
   505   on @{text "\<lambda>"}-terms.  Moreover, propositions are understood modulo
   506   the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.
   507 
   508   This means that any operations within the rule calculus may be
   509   subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions.  It is common
   510   practice not to contract or expand unnecessarily.  Some mechanisms
   511   prefer an one form, others the opposite, so there is a potential
   512   danger to produce some oscillation!
   513 
   514   Only few operations really work \emph{modulo} HHF conversion, but
   515   expect a normal form: quantifiers @{text "\<And>"} before implications
   516   @{text "\<Longrightarrow>"} at each level of nesting.
   517 
   518 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
   519 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
   520 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
   521 Any proposition may be put into HHF form by normalizing with the rule
   522 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
   523 quantifier prefix is represented via \seeglossary{schematic
   524 variables}, such that the top-level structure is merely that of a
   525 \seeglossary{Horn Clause}}.
   526 
   527 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
   528 
   529 
   530   \[
   531   \infer[@{text "(assumption)"}]{@{text "C\<vartheta>"}}
   532   {@{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})}}
   533   \]
   534 
   535 
   536   \[
   537   \infer[@{text "(compose)"}]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}
   538   {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}
   539   \]
   540 
   541 
   542   \[
   543   \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"}}
   544   \]
   545   \[
   546   \infer[@{text "(\<Longrightarrow>_lift)"}]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}
   547   \]
   548 
   549   The @{text resolve} scheme is now acquired from @{text "\<And>_lift"},
   550   @{text "\<Longrightarrow>_lift"}, and @{text compose}.
   551 
   552   \[
   553   \infer[@{text "(resolution)"}]
   554   {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}
   555   {\begin{tabular}{l}
   556     @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\
   557     @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\
   558     @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\
   559    \end{tabular}}
   560   \]
   561 
   562 
   563   FIXME @{text "elim_resolution"}, @{text "dest_resolution"}
   564 *}
   565 
   566 
   567 end