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