doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Mon Sep 11 14:35:25 2006 +0200 (2006-09-11) changeset 20501 de0b523b0d62 parent 20498 825a8d2335ce child 20514 5ede702cd2ca permissions -rw-r--r--
more rules;
     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} is defined inductively over type variables and type

    82   constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |

    83   (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)k"}.

    84

    85   A \emph{type abbreviation} is a syntactic abbreviation @{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

   192   variables, and constants.  Terms with loose bound variables are

   193   usually considered malformed.  The types of variables and constants

   194   is stored explicitly at each occurrence in the term (which is a

   195   known performance issue).

   196

   197   FIXME de-Bruijn representation of lambda terms

   198

   199   Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}

   200   and application @{text "t u"}, while types are usually implicit

   201   thanks to type-inference.

   202

   203

   204   $  205 \infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{}   206 \qquad   207 \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}}   208 \qquad   209 \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}}   210$

   211

   212 *}

   213

   214

   215 text {*

   216

   217 FIXME

   218

   219 \glossary{Schematic polymorphism}{FIXME}

   220

   221 \glossary{Type variable}{FIXME}

   222

   223 *}

   224

   225

   226 section {* Theorems \label{sec:thms} *}

   227

   228 text {*

   229   \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}

   230   @{text "prop"}.  Internally, there is nothing special about

   231   propositions apart from their type, but the concrete syntax enforces

   232   a clear distinction.  Propositions are structured via implication

   233   @{text "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} ---

   234   anything else is considered atomic.  The canonical form for

   235   propositions is that of a \seeglossary{Hereditary Harrop Formula}. FIXME}

   236

   237   \glossary{Theorem}{A proven proposition within a certain theory and

   238   proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are

   239   rarely spelled out explicitly.  Theorems are usually normalized

   240   according to the \seeglossary{HHF} format. FIXME}

   241

   242   \glossary{Fact}{Sometimes used interchangably for

   243   \seeglossary{theorem}.  Strictly speaking, a list of theorems,

   244   essentially an extra-logical conjunction.  Facts emerge either as

   245   local assumptions, or as results of local goal statements --- both

   246   may be simultaneous, hence the list representation. FIXME}

   247

   248   \glossary{Schematic variable}{FIXME}

   249

   250   \glossary{Fixed variable}{A variable that is bound within a certain

   251   proof context; an arbitrary-but-fixed entity within a portion of

   252   proof text. FIXME}

   253

   254   \glossary{Free variable}{Synonymous for \seeglossary{fixed

   255   variable}. FIXME}

   256

   257   \glossary{Bound variable}{FIXME}

   258

   259   \glossary{Variable}{See \seeglossary{schematic variable},

   260   \seeglossary{fixed variable}, \seeglossary{bound variable}, or

   261   \seeglossary{type variable}.  The distinguishing feature of

   262   different variables is their binding scope. FIXME}

   263

   264   A \emph{proposition} is a well-formed term of type @{text "prop"}.

   265   The connectives of minimal logic are declared as constants of the

   266   basic theory:

   267

   268   \smallskip

   269   \begin{tabular}{ll}

   270   @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\

   271   @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\

   272   \end{tabular}

   273

   274   \medskip A \emph{theorem} is a proven proposition, depending on a

   275   collection of assumptions, and axioms from the theory context.  The

   276   judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is defined

   277   inductively by the primitive inferences given in

   278   \figref{fig:prim-rules}; there is a global syntactic restriction

   279   that the hypotheses may not contain schematic variables.

   280

   281   \begin{figure}[htb]

   282   \begin{center}

   283   $  284 \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}}   285 \qquad   286 \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}   287$

   288   $  289 \infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b x"}}{@{text "\<Gamma> \<turnstile> b x"} & @{text "x \<notin> \<Gamma>"}}   290 \qquad   291 \infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b a"}}{@{text "\<Gamma> \<turnstile> \<And>x. b x"}}   292$

   293   $  294 \infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}   295 \qquad   296 \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"}}   297$

   298   \caption{Primitive inferences of the Pure logic}\label{fig:prim-rules}

   299   \end{center}

   300   \end{figure}

   301

   302   The introduction and elimination rules for @{text "\<And>"} and @{text

   303   "\<Longrightarrow>"} are analogous to formation of (dependently typed) @{text

   304   "\<lambda>"}-terms representing the underlying proof objects.  Proof terms

   305   are \emph{irrelevant} in the Pure logic, they may never occur within

   306   propositions, i.e.\ the @{text "\<Longrightarrow>"} arrow of the framework is a

   307   non-dependent one.

   308

   309   Also note that fixed parameters as in @{text "\<And>_intro"} need not be

   310   recorded in the context @{text "\<Gamma>"}, since syntactic types are

   311   always inhabitable.  An assumption'' @{text "x :: \<tau>"} is logically

   312   vacuous, because @{text "\<tau>"} is always non-empty.  This is the deeper

   313   reason why @{text "\<Gamma>"} only consists of hypothetical proofs, but no

   314   hypothetical terms.

   315

   316   The corresponding proof terms are left implicit in the classic

   317   LCF-approach'', although they could be exploited separately

   318   \cite{Berghofer-Nipkow:2000}.  The implementation provides a runtime

   319   option to control the generation of full proof terms.

   320

   321   \medskip The axiomatization of a theory is implicitly closed by

   322   forming all instances of type and term variables: @{text "\<turnstile> A\<theta>"} for

   323   any substirution instance of axiom @{text "\<turnstile> A"}.  By pushing

   324   substitution through derivations inductively, we get admissible

   325   substitution rules for theorems shown in \figref{fig:subst-rules}.

   326

   327   \begin{figure}[htb]

   328   \begin{center}

   329   $  330 \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}   331 \quad   332 \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}   333$

   334   $  335 \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}   336 \quad   337 \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}   338$

   339   \caption{Admissible substitution rules}\label{fig:subst-rules}

   340   \end{center}

   341   \end{figure}

   342

   343   Note that @{text "instantiate_term"} could be derived using @{text

   344   "\<And>_intro/elim"}, but this is not how it is implemented.  The type

   345   instantiation rule is a genuine admissible one, due to the lack of

   346   true polymorphism in the logic.

   347

   348   Since @{text "\<Gamma>"} may never contain any schematic variables, the

   349   @{text "instantiate"} do not require an explicit side-condition.  In

   350   principle, variables could be substituted in hypotheses as well, but

   351   this could disrupt monotonicity of the basic calculus: derivations

   352   could leave the current proof context.

   353

   354   \medskip The framework also provides builtin equality @{text "\<equiv>"},

   355   which is conceptually axiomatized shown in \figref{fig:equality},

   356   although the implementation provides derived rules directly:

   357

   358   \begin{figure}[htb]

   359   \begin{center}

   360   \begin{tabular}{ll}

   361   @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\

   362   @{text "\<turnstile> (\<lambda>x. b x) a \<equiv> b a"} & @{text "\<beta>"}-conversion \\

   363   @{text "\<turnstile> x \<equiv> x"} & reflexivity law \\

   364   @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution law \\

   365   @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\

   366   @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & coincidence with equivalence \\

   367   \end{tabular}

   368   \caption{Conceptual axiomatization of equality.}\label{fig:equality}

   369   \end{center}

   370   \end{figure}

   371

   372   Since the basic representation of terms already accounts for @{text

   373   "\<alpha>"}-conversion, Pure equality essentially acts like @{text

   374   "\<alpha>\<beta>\<eta>"}-equivalence on terms, while coinciding with bi-implication.

   375

   376

   377   \medskip Conjunction is defined in Pure as a derived connective, see

   378   \figref{fig:conjunction}.  This is occasionally useful to represent

   379   simultaneous statements behind the scenes --- framework conjunction

   380   is usually not exposed to the user.

   381

   382   \begin{figure}[htb]

   383   \begin{center}

   384   \begin{tabular}{ll}

   385   @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} & conjunction (hidden) \\

   386   @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\

   387   \end{tabular}

   388   \caption{Definition of conjunction.}\label{fig:equality}

   389   \end{center}

   390   \end{figure}

   391

   392   The definition allows to derive the usual introduction @{text "\<turnstile> A \<Longrightarrow>

   393   B \<Longrightarrow> A & B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B

   394   \<Longrightarrow> B"}.

   395 *}

   396

   397

   398 section {* Rules \label{sec:rules} *}

   399

   400 text {*

   401

   402 FIXME

   403

   404   A \emph{rule} is any Pure theorem in HHF normal form; there is a

   405   separate calculus for rule composition, which is modeled after

   406   Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows

   407   rules to be nested arbitrarily, similar to \cite{extensions91}.

   408

   409   Normally, all theorems accessible to the user are proper rules.

   410   Low-level inferences are occasional required internally, but the

   411   result should be always presented in canonical form.  The higher

   412   interfaces of Isabelle/Isar will always produce proper rules.  It is

   413   important to maintain this invariant in add-on applications!

   414

   415   There are two main principles of rule composition: @{text

   416   "resolution"} (i.e.\ backchaining of rules) and @{text

   417   "by-assumption"} (i.e.\ closing a branch); both principles are

   418   combined in the variants of @{text "elim-resosultion"} and @{text

   419   "dest-resolution"}.  Raw @{text "composition"} is occasionally

   420   useful as well, also it is strictly speaking outside of the proper

   421   rule calculus.

   422

   423   Rules are treated modulo general higher-order unification, which is

   424   unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion

   425   on @{text "\<lambda>"}-terms.  Moreover, propositions are understood modulo

   426   the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.

   427

   428   This means that any operations within the rule calculus may be

   429   subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions.  It is common

   430   practice not to contract or expand unnecessarily.  Some mechanisms

   431   prefer an one form, others the opposite, so there is a potential

   432   danger to produce some oscillation!

   433

   434   Only few operations really work \emph{modulo} HHF conversion, but

   435   expect a normal form: quantifiers @{text "\<And>"} before implications

   436   @{text "\<Longrightarrow>"} at each level of nesting.

   437

   438 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF

   439 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>

   440 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.

   441 Any proposition may be put into HHF form by normalizing with the rule

   442 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost

   443 quantifier prefix is represented via \seeglossary{schematic

   444 variables}, such that the top-level structure is merely that of a

   445 \seeglossary{Horn Clause}}.

   446

   447 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}

   448

   449

   450   $  451 \infer[@{text "(assumption)"}]{@{text "C\<vartheta>"}}   452 {@{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})}}   453$

   454

   455

   456   $  457 \infer[@{text "(compose)"}]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}   458 {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}   459$

   460

   461

   462   $  463 \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"}}   464$

   465   $  466 \infer[@{text "(\<Longrightarrow>_lift)"}]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}   467$

   468

   469   The @{text resolve} scheme is now acquired from @{text "\<And>_lift"},

   470   @{text "\<Longrightarrow>_lift"}, and @{text compose}.

   471

   472   $  473 \infer[@{text "(resolution)"}]   474 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}   475 {\begin{tabular}{l}   476 @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\   477 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\   478 @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\   479 \end{tabular}}   480$

   481

   482

   483   FIXME @{text "elim_resolution"}, @{text "dest_resolution"}

   484 *}

   485

   486

   487 end