wneuper/isa: doc-src/IsarImplementation/Thy/document/Logic.tex@89ccf66aa73d

1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{Logic}%

4 %

     5 \isadelimtheory

6 %

     7 \endisadelimtheory

8 %

     9 \isatagtheory

    10 \isacommand{theory}\isamarkupfalse%

    11 \ Logic\isanewline

    12 \isakeyword{imports}\ Base\isanewline

    13 \isakeyword{begin}%

    14 \endisatagtheory

    15 {\isafoldtheory}%

    16 %

    17 \isadelimtheory

    18 %

    19 \endisadelimtheory

    20 %

    21 \isamarkupchapter{Primitive logic \label{ch:logic}%

    22 }

    23 \isamarkuptrue%

    24 %

    25 \begin{isamarkuptext}%

    26 The logical foundations of Isabelle/Isar are that of the Pure logic,

    27   which has been introduced as a Natural Deduction framework in

    28   \cite{paulson700}.  This is essentially the same logic as ``\isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}HOL}'' in the more abstract setting of Pure Type Systems (PTS)

    29   \cite{Barendregt-Geuvers:2001}, although there are some key

    30   differences in the specific treatment of simple types in

    31   Isabelle/Pure.

    33   Following type-theoretic parlance, the Pure logic consists of three

    34   levels of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-calculus with corresponding arrows, \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} for syntactic function space (terms depending on terms), \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} for universal quantification (proofs depending on terms), and

    35   \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} for implication (proofs depending on proofs).

    37   Derivations are relative to a logical theory, which declares type

    38   constructors, constants, and axioms.  Theory declarations support

    39   schematic polymorphism, which is strictly speaking outside the

    40   logic.\footnote{This is the deeper logical reason, why the theory

    41   context \isa{{\isaliteral{5C3C54686574613E}{\isasymTheta}}} is separate from the proof context \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}

    42   of the core calculus: type constructors, term constants, and facts

    43   (proof constants) may involve arbitrary type schemes, but the type

    44   of a locally fixed term parameter is also fixed!}%

    45 \end{isamarkuptext}%

    46 \isamarkuptrue%

    47 %

    48 \isamarkupsection{Types \label{sec:types}%

    49 }

    50 \isamarkuptrue%

    51 %

    52 \begin{isamarkuptext}%

    53 The language of types is an uninterpreted order-sorted first-order

    54   algebra; types are qualified by ordered type classes.

    56   \medskip A \emph{type class} is an abstract syntactic entity

    57   declared in the theory context.  The \emph{subclass relation} \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} is specified by stating an acyclic

    58   generating relation; the transitive closure is maintained

    59   internally.  The resulting relation is an ordering: reflexive,

    60   transitive, and antisymmetric.

    62   A \emph{sort} is a list of type classes written as \isa{s\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub m{\isaliteral{7D}{\isacharbraceright}}}, it represents symbolic intersection.  Notationally, the

    63   curly braces are omitted for singleton intersections, i.e.\ any

    64   class \isa{c} may be read as a sort \isa{{\isaliteral{7B}{\isacharbraceleft}}c{\isaliteral{7D}{\isacharbraceright}}}.  The ordering

    65   on type classes is extended to sorts according to the meaning of

    66   intersections: \isa{{\isaliteral{7B}{\isacharbraceleft}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub m{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ {\isaliteral{7B}{\isacharbraceleft}}d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ d\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{7D}{\isacharbraceright}}} iff \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}j{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}i{\isaliteral{2E}{\isachardot}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub i\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ d\isaliteral{5C3C5E697375623E}{}\isactrlisub j}.  The empty intersection \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}} refers to

    67   the universal sort, which is the largest element wrt.\ the sort

    68   order.  Thus \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}} represents the ``full sort'', not the

    69   empty one!  The intersection of all (finitely many) classes declared

    70   in the current theory is the least element wrt.\ the sort ordering.

    72   \medskip A \emph{fixed type variable} is a pair of a basic name

    73   (starting with a \isa{{\isaliteral{27}{\isacharprime}}} character) and a sort constraint, e.g.\

    74   \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}} which is usually printed as \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub s}.

    75   A \emph{schematic type variable} is a pair of an indexname and a

    76   sort constraint, e.g.\ \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}} which is usually

    77   printed as \isa{{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub s}.

    79   Note that \emph{all} syntactic components contribute to the identity

    80   of type variables: basic name, index, and sort constraint.  The core

    81   logic handles type variables with the same name but different sorts

    82   as different, although the type-inference layer (which is outside

    83   the core) rejects anything like that.

    85   A \emph{type constructor} \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} is a \isa{k}-ary operator

    86   on types declared in the theory.  Type constructor application is

    87   written postfix as \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}}.  For

    88   \isa{k\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} the argument tuple is omitted, e.g.\ \isa{prop}

    89   instead of \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}prop}.  For \isa{k\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}} the parentheses

    90   are omitted, e.g.\ \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ list} instead of \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}list}.

    91   Further notation is provided for specific constructors, notably the

    92   right-associative infix \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}} instead of \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{29}{\isacharparenright}}fun}.

    94   The logical category \emph{type} is defined inductively over type

    95   variables and type constructors as follows: \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub s\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub s\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}}.

    97   A \emph{type abbreviation} is a syntactic definition \isa{{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}} of an arbitrary type expression \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} over

    98   variables \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}.  Type abbreviations appear as type

    99   constructors in the syntax, but are expanded before entering the

   100   logical core.

   102   A \emph{type arity} declares the image behavior of a type

   103   constructor wrt.\ the algebra of sorts: \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ s\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{29}{\isacharparenright}}s} means that \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} is

   104   of sort \isa{s} if every argument type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i} is

   105   of sort \isa{s\isaliteral{5C3C5E697375623E}{}\isactrlisub i}.  Arity declarations are implicitly

   106   completed, i.e.\ \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{29}{\isacharparenright}}c} entails \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{29}{\isacharparenright}}c{\isaliteral{27}{\isacharprime}}} for any \isa{c{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C73757073657465713E}{\isasymsupseteq}}\ c}.

   108   \medskip The sort algebra is always maintained as \emph{coregular},

   109   which means that type arities are consistent with the subclass

   110   relation: for any type constructor \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}}, and classes \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}, and arities \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}} and \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} holds \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} component-wise.

   112   The key property of a coregular order-sorted algebra is that sort

   113   constraints can be solved in a most general fashion: for each type

   114   constructor \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} and sort \isa{s} there is a most general

   115   vector of argument sorts \isa{{\isaliteral{28}{\isacharparenleft}}s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ s\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{29}{\isacharparenright}}} such

   116   that a type scheme \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E627375623E}{}\isactrlbsub s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\isaliteral{5C3C5E657375623E}{}\isactrlesub {\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E627375623E}{}\isactrlbsub s\isaliteral{5C3C5E697375623E}{}\isactrlisub k\isaliteral{5C3C5E657375623E}{}\isactrlesub {\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} is of sort \isa{s}.

   117   Consequently, type unification has most general solutions (modulo

   118   equivalence of sorts), so type-inference produces primary types as

   119   expected \cite{nipkow-prehofer}.%

   120 \end{isamarkuptext}%

   121 \isamarkuptrue%

   122 %

   123 \isadelimmlref

   124 %

   125 \endisadelimmlref

   126 %

   127 \isatagmlref

   128 %

   129 \begin{isamarkuptext}%

   130 \begin{mldecls}

   131   \indexdef{}{ML type}{class}\verb|type class = string| \\

   132   \indexdef{}{ML type}{sort}\verb|type sort = class list| \\

   133   \indexdef{}{ML type}{arity}\verb|type arity = string * sort list * sort| \\

   134   \indexdef{}{ML type}{typ}\verb|type typ| \\

   135   \indexdef{}{ML}{Term.map\_atyps}\verb|Term.map_atyps: (typ -> typ) -> typ -> typ| \\

   136   \indexdef{}{ML}{Term.fold\_atyps}\verb|Term.fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\

   137   \end{mldecls}

   138   \begin{mldecls}

   139   \indexdef{}{ML}{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\

   140   \indexdef{}{ML}{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\

   141   \indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: Proof.context ->|\isasep\isanewline%

   142 \verb|  (binding * int * mixfix) list -> theory -> theory| \\

   143   \indexdef{}{ML}{Sign.add\_type\_abbrev}\verb|Sign.add_type_abbrev: Proof.context ->|\isasep\isanewline%

   144 \verb|  binding * string list * typ -> theory -> theory| \\

   145   \indexdef{}{ML}{Sign.primitive\_class}\verb|Sign.primitive_class: binding * class list -> theory -> theory| \\

   146   \indexdef{}{ML}{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\

   147   \indexdef{}{ML}{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\

   148   \end{mldecls}

   150   \begin{description}

   152   \item Type \verb|class| represents type classes.

   154   \item Type \verb|sort| represents sorts, i.e.\ finite

   155   intersections of classes.  The empty list \verb|[]: sort| refers to

   156   the empty class intersection, i.e.\ the ``full sort''.

   158   \item Type \verb|arity| represents type arities.  A triple

   159   \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3A}{\isacharcolon}}\ arity} represents \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{29}{\isacharparenright}}s} as described above.

   161   \item Type \verb|typ| represents types; this is a datatype with

   162   constructors \verb|TFree|, \verb|TVar|, \verb|Type|.

   164   \item \verb|Term.map_atyps|~\isa{f\ {\isaliteral{5C3C7461753E}{\isasymtau}}} applies the mapping \isa{f} to all atomic types (\verb|TFree|, \verb|TVar|) occurring in

   165   \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}.

   167   \item \verb|Term.fold_atyps|~\isa{f\ {\isaliteral{5C3C7461753E}{\isasymtau}}} iterates the operation

   168   \isa{f} over all occurrences of atomic types (\verb|TFree|, \verb|TVar|) in \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}; the type structure is traversed from left to

   169   right.

   171   \item \verb|Sign.subsort|~\isa{thy\ {\isaliteral{28}{\isacharparenleft}}s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}

   172   tests the subsort relation \isa{s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ s\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}.

   174   \item \verb|Sign.of_sort|~\isa{thy\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}} tests whether type

   175   \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} is of sort \isa{s}.

   177   \item \verb|Sign.add_types|~\isa{ctxt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}} declares a

   178   new type constructors \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} with \isa{k} arguments and

   179   optional mixfix syntax.

   181   \item \verb|Sign.add_type_abbrev|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}}

   182   defines a new type abbreviation \isa{{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}}.

   184   \item \verb|Sign.primitive_class|~\isa{{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}} declares a new class \isa{c}, together with class

   185   relations \isa{c\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub i}, for \isa{i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ n}.

   187   \item \verb|Sign.primitive_classrel|~\isa{{\isaliteral{28}{\isacharparenleft}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} declares the class relation \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}.

   189   \item \verb|Sign.primitive_arity|~\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}} declares

   190   the arity \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec s{\isaliteral{29}{\isacharparenright}}s}.

   192   \end{description}%

   193 \end{isamarkuptext}%

   194 \isamarkuptrue%

   195 %

   196 \endisatagmlref

   197 {\isafoldmlref}%

   198 %

   199 \isadelimmlref

   200 %

   201 \endisadelimmlref

   202 %

   203 \isadelimmlantiq

   204 %

   205 \endisadelimmlantiq

   206 %

   207 \isatagmlantiq

   208 %

   209 \begin{isamarkuptext}%

   210 \begin{matharray}{rcl}

   211   \indexdef{}{ML antiquotation}{class}\hypertarget{ML antiquotation.class}{\hyperlink{ML antiquotation.class}{\mbox{\isa{class}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   212   \indexdef{}{ML antiquotation}{sort}\hypertarget{ML antiquotation.sort}{\hyperlink{ML antiquotation.sort}{\mbox{\isa{sort}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   213   \indexdef{}{ML antiquotation}{type\_name}\hypertarget{ML antiquotation.type-name}{\hyperlink{ML antiquotation.type-name}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}name}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   214   \indexdef{}{ML antiquotation}{type\_abbrev}\hypertarget{ML antiquotation.type-abbrev}{\hyperlink{ML antiquotation.type-abbrev}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}abbrev}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   215   \indexdef{}{ML antiquotation}{nonterminal}\hypertarget{ML antiquotation.nonterminal}{\hyperlink{ML antiquotation.nonterminal}{\mbox{\isa{nonterminal}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   216   \indexdef{}{ML antiquotation}{typ}\hypertarget{ML antiquotation.typ}{\hyperlink{ML antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   217   \end{matharray}

   219   \begin{railoutput}

   220 \rail@begin{1}{}

   221 \rail@term{\hyperlink{ML antiquotation.class}{\mbox{\isa{class}}}}[]

   222 \rail@nont{\isa{nameref}}[]

   223 \rail@end

   224 \rail@begin{1}{}

   225 \rail@term{\hyperlink{ML antiquotation.sort}{\mbox{\isa{sort}}}}[]

   226 \rail@nont{\isa{sort}}[]

   227 \rail@end

   228 \rail@begin{3}{}

   229 \rail@bar

   230 \rail@term{\hyperlink{ML antiquotation.type-name}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}name}}}}[]

   231 \rail@nextbar{1}

   232 \rail@term{\hyperlink{ML antiquotation.type-abbrev}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}abbrev}}}}[]

   233 \rail@nextbar{2}

   234 \rail@term{\hyperlink{ML antiquotation.nonterminal}{\mbox{\isa{nonterminal}}}}[]

   235 \rail@endbar

   236 \rail@nont{\isa{nameref}}[]

   237 \rail@end

   238 \rail@begin{1}{}

   239 \rail@term{\hyperlink{ML antiquotation.typ}{\mbox{\isa{typ}}}}[]

   240 \rail@nont{\isa{type}}[]

   241 \rail@end

   242 \end{railoutput}

   245   \begin{description}

   247   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}class\ c{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized class \isa{c} --- as \verb|string| literal.

   249   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}sort\ s{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized sort \isa{s}

   250   --- as \verb|string list| literal.

   252   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}type{\isaliteral{5F}{\isacharunderscore}}name\ c{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized type

   253   constructor \isa{c} --- as \verb|string| literal.

   255   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}type{\isaliteral{5F}{\isacharunderscore}}abbrev\ c{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized type

   256   abbreviation \isa{c} --- as \verb|string| literal.

   258   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}nonterminal\ c{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized syntactic

   259   type~/ grammar nonterminal \isa{c} --- as \verb|string|

   260   literal.

   262   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}typ\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}

   263   --- as constructor term for datatype \verb|typ|.

   265   \end{description}%

   266 \end{isamarkuptext}%

   267 \isamarkuptrue%

   268 %

   269 \endisatagmlantiq

   270 {\isafoldmlantiq}%

   271 %

   272 \isadelimmlantiq

   273 %

   274 \endisadelimmlantiq

   275 %

   276 \isamarkupsection{Terms \label{sec:terms}%

   277 }

   278 \isamarkuptrue%

   279 %

   280 \begin{isamarkuptext}%

   281 The language of terms is that of simply-typed \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-calculus

   282   with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}

   283   or \cite{paulson-ml2}), with the types being determined by the

   284   corresponding binders.  In contrast, free variables and constants

   285   have an explicit name and type in each occurrence.

   287   \medskip A \emph{bound variable} is a natural number \isa{b},

   288   which accounts for the number of intermediate binders between the

   289   variable occurrence in the body and its binding position.  For

   290   example, the de-Bruijn term \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\isaliteral{5C3C5E627375623E}{}\isactrlbsub bool\isaliteral{5C3C5E657375623E}{}\isactrlesub {\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\isaliteral{5C3C5E627375623E}{}\isactrlbsub bool\isaliteral{5C3C5E657375623E}{}\isactrlesub {\isaliteral{2E}{\isachardot}}\ {\isadigit{1}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isadigit{0}}} would

   291   correspond to \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\isaliteral{5C3C5E627375623E}{}\isactrlbsub bool\isaliteral{5C3C5E657375623E}{}\isactrlesub {\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}y\isaliteral{5C3C5E627375623E}{}\isactrlbsub bool\isaliteral{5C3C5E657375623E}{}\isactrlesub {\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C616E643E}{\isasymand}}\ y} in a named

   292   representation.  Note that a bound variable may be represented by

   293   different de-Bruijn indices at different occurrences, depending on

   294   the nesting of abstractions.

   296   A \emph{loose variable} is a bound variable that is outside the

   297   scope of local binders.  The types (and names) for loose variables

   298   can be managed as a separate context, that is maintained as a stack

   299   of hypothetical binders.  The core logic operates on closed terms,

   300   without any loose variables.

   302   A \emph{fixed variable} is a pair of a basic name and a type, e.g.\

   303   \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} which is usually printed \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} here.  A

   304   \emph{schematic variable} is a pair of an indexname and a type,

   305   e.g.\ \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} which is likewise printed as \isa{{\isaliteral{3F}{\isacharquery}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}}.

   307   \medskip A \emph{constant} is a pair of a basic name and a type,

   308   e.g.\ \isa{{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} which is usually printed as \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}}

   309   here.  Constants are declared in the context as polymorphic families

   310   \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}, meaning that all substitution instances \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} for \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}} are valid.

   312   The vector of \emph{type arguments} of constant \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} wrt.\

   313   the declaration \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} is defined as the codomain of the

   314   matcher \isa{{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C6D617073746F3E}{\isasymmapsto}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{7D}{\isacharbraceright}}} presented in

   315   canonical order \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}}, corresponding to the

   316   left-to-right occurrences of the \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i} in \isa{{\isaliteral{5C3C7369676D613E}{\isasymsigma}}}.

   317   Within a given theory context, there is a one-to-one correspondence

   318   between any constant \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} and the application \isa{c{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}} of its type arguments.  For example, with \isa{plus\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}, the instance \isa{plus\isaliteral{5C3C5E627375623E}{}\isactrlbsub nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\isaliteral{5C3C5E657375623E}{}\isactrlesub } corresponds to

   319   \isa{plus{\isaliteral{28}{\isacharparenleft}}nat{\isaliteral{29}{\isacharparenright}}}.

   321   Constant declarations \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} may contain sort constraints

   322   for type variables in \isa{{\isaliteral{5C3C7369676D613E}{\isasymsigma}}}.  These are observed by

   323   type-inference as expected, but \emph{ignored} by the core logic.

   324   This means the primitive logic is able to reason with instances of

   325   polymorphic constants that the user-level type-checker would reject

   326   due to violation of type class restrictions.

   328   \medskip An \emph{atomic term} is either a variable or constant.

   329   The logical category \emph{term} is defined inductively over atomic

   330   terms, with abstraction and application as follows: \isa{t\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{7C}{\isacharbar}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{3F}{\isacharquery}}x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{7C}{\isacharbar}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{7C}{\isacharbar}}\ t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ t\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}.  Parsing and printing takes care of

   331   converting between an external representation with named bound

   332   variables.  Subsequently, we shall use the latter notation instead

   333   of internal de-Bruijn representation.

   335   The inductive relation \isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}} assigns a (unique) type to a

   336   term according to the structure of atomic terms, abstractions, and

   337   applicatins:

   338   \[

   339   \infer{\isa{a\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}}}{}

   340   \qquad

   341   \infer{\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{2E}{\isachardot}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}}{\isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}}

   342   \qquad

   343   \infer{\isa{t\ u\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}}{\isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} & \isa{u\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}}}

   344   \]

   345   A \emph{well-typed term} is a term that can be typed according to these rules.

   347   Typing information can be omitted: type-inference is able to

   348   reconstruct the most general type of a raw term, while assigning

   349   most general types to all of its variables and constants.

   350   Type-inference depends on a context of type constraints for fixed

   351   variables, and declarations for polymorphic constants.

   353   The identity of atomic terms consists both of the name and the type

   354   component.  This means that different variables \isa{x\isaliteral{5C3C5E627375623E}{}\isactrlbsub {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\isaliteral{5C3C5E657375623E}{}\isactrlesub } and \isa{x\isaliteral{5C3C5E627375623E}{}\isactrlbsub {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\isaliteral{5C3C5E657375623E}{}\isactrlesub } may become the same after

   355   type instantiation.  Type-inference rejects variables of the same

   356   name, but different types.  In contrast, mixed instances of

   357   polymorphic constants occur routinely.

   359   \medskip The \emph{hidden polymorphism} of a term \isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}

   360   is the set of type variables occurring in \isa{t}, but not in

   361   its type \isa{{\isaliteral{5C3C7369676D613E}{\isasymsigma}}}.  This means that the term implicitly depends

   362   on type arguments that are not accounted in the result type, i.e.\

   363   there are different type instances \isa{t{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} and

   364   \isa{t{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} with the same type.  This slightly

   365   pathological situation notoriously demands additional care.

   367   \medskip A \emph{term abbreviation} is a syntactic definition \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t} of a closed term \isa{t} of type \isa{{\isaliteral{5C3C7369676D613E}{\isasymsigma}}},

   368   without any hidden polymorphism.  A term abbreviation looks like a

   369   constant in the syntax, but is expanded before entering the logical

   370   core.  Abbreviations are usually reverted when printing terms, using

   371   \isa{t\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} as rules for higher-order rewriting.

   373   \medskip Canonical operations on \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-terms include \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}}-conversion: \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}-conversion refers to capture-free

   374   renaming of bound variables; \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}}-conversion contracts an

   375   abstraction applied to an argument term, substituting the argument

   376   in the body: \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{29}{\isacharparenright}}a} becomes \isa{b{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{2F}{\isacharslash}}x{\isaliteral{5D}{\isacharbrackright}}}; \isa{{\isaliteral{5C3C6574613E}{\isasymeta}}}-conversion contracts vacuous application-abstraction: \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ f\ x} becomes \isa{f}, provided that the bound variable

   377   does not occur in \isa{f}.

   379   Terms are normally treated modulo \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}-conversion, which is

   380   implicit in the de-Bruijn representation.  Names for bound variables

   381   in abstractions are maintained separately as (meaningless) comments,

   382   mostly for parsing and printing.  Full \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}}-conversion is

   383   commonplace in various standard operations (\secref{sec:obj-rules})

   384   that are based on higher-order unification and matching.%

   385 \end{isamarkuptext}%

   386 \isamarkuptrue%

   387 %

   388 \isadelimmlref

   389 %

   390 \endisadelimmlref

   391 %

   392 \isatagmlref

   393 %

   394 \begin{isamarkuptext}%

   395 \begin{mldecls}

   396   \indexdef{}{ML type}{term}\verb|type term| \\

   397   \indexdef{}{ML infix}{aconv}\verb|infix aconv: term * term -> bool| \\

   398   \indexdef{}{ML}{Term.map\_types}\verb|Term.map_types: (typ -> typ) -> term -> term| \\

   399   \indexdef{}{ML}{Term.fold\_types}\verb|Term.fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\

   400   \indexdef{}{ML}{Term.map\_aterms}\verb|Term.map_aterms: (term -> term) -> term -> term| \\

   401   \indexdef{}{ML}{Term.fold\_aterms}\verb|Term.fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\

   402   \end{mldecls}

   403   \begin{mldecls}

   404   \indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\

   405   \indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\

   406   \indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\

   407   \indexdef{}{ML}{incr\_boundvars}\verb|incr_boundvars: int -> term -> term| \\

   408   \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: Proof.context ->|\isasep\isanewline%

   409 \verb|  (binding * typ) * mixfix -> theory -> term * theory| \\

   410   \indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> binding * term ->|\isasep\isanewline%

   411 \verb|  theory -> (term * term) * theory| \\

   412   \indexdef{}{ML}{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\

   413   \indexdef{}{ML}{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\

   414   \end{mldecls}

   416   \begin{description}

   418   \item Type \verb|term| represents de-Bruijn terms, with comments

   419   in abstractions, and explicitly named free variables and constants;

   420   this is a datatype with constructors \verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|, \verb|Abs|, \verb|$|.

   422   \item \isa{t}~\verb|aconv|~\isa{u} checks \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}-equivalence of two terms.  This is the basic equality relation

   423   on type \verb|term|; raw datatype equality should only be used

   424   for operations related to parsing or printing!

   426   \item \verb|Term.map_types|~\isa{f\ t} applies the mapping \isa{f} to all types occurring in \isa{t}.

   428   \item \verb|Term.fold_types|~\isa{f\ t} iterates the operation

   429   \isa{f} over all occurrences of types in \isa{t}; the term

   430   structure is traversed from left to right.

   432   \item \verb|Term.map_aterms|~\isa{f\ t} applies the mapping \isa{f} to all atomic terms (\verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|) occurring in \isa{t}.

   434   \item \verb|Term.fold_aterms|~\isa{f\ t} iterates the operation

   435   \isa{f} over all occurrences of atomic terms (\verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|) in \isa{t}; the term structure is

   436   traversed from left to right.

   438   \item \verb|fastype_of|~\isa{t} determines the type of a

   439   well-typed term.  This operation is relatively slow, despite the

   440   omission of any sanity checks.

   442   \item \verb|lambda|~\isa{a\ b} produces an abstraction \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}a{\isaliteral{2E}{\isachardot}}\ b}, where occurrences of the atomic term \isa{a} in the

   443   body \isa{b} are replaced by bound variables.

   445   \item \verb|betapply|~\isa{{\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ u{\isaliteral{29}{\isacharparenright}}} produces an application \isa{t\ u}, with topmost \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}}-conversion if \isa{t} is an

   446   abstraction.

   448   \item \verb|incr_boundvars|~\isa{j} increments a term's dangling

   449   bound variables by the offset \isa{j}.  This is required when

   450   moving a subterm into a context where it is enclosed by a different

   451   number of abstractions.  Bound variables with a matching abstraction

   452   are unaffected.

   454   \item \verb|Sign.declare_const|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}} declares

   455   a new constant \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} with optional mixfix syntax.

   457   \item \verb|Sign.add_abbrev|~\isa{print{\isaliteral{5F}{\isacharunderscore}}mode\ {\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}}

   458   introduces a new term abbreviation \isa{c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t}.

   460   \item \verb|Sign.const_typargs|~\isa{thy\ {\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} and \verb|Sign.const_instance|~\isa{thy\ {\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}}

   461   convert between two representations of polymorphic constants: full

   462   type instance vs.\ compact type arguments form.

   464   \end{description}%

   465 \end{isamarkuptext}%

   466 \isamarkuptrue%

   467 %

   468 \endisatagmlref

   469 {\isafoldmlref}%

   470 %

   471 \isadelimmlref

   472 %

   473 \endisadelimmlref

   474 %

   475 \isadelimmlantiq

   476 %

   477 \endisadelimmlantiq

   478 %

   479 \isatagmlantiq

   480 %

   481 \begin{isamarkuptext}%

   482 \begin{matharray}{rcl}

   483   \indexdef{}{ML antiquotation}{const\_name}\hypertarget{ML antiquotation.const-name}{\hyperlink{ML antiquotation.const-name}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}name}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   484   \indexdef{}{ML antiquotation}{const\_abbrev}\hypertarget{ML antiquotation.const-abbrev}{\hyperlink{ML antiquotation.const-abbrev}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}abbrev}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   485   \indexdef{}{ML antiquotation}{const}\hypertarget{ML antiquotation.const}{\hyperlink{ML antiquotation.const}{\mbox{\isa{const}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   486   \indexdef{}{ML antiquotation}{term}\hypertarget{ML antiquotation.term}{\hyperlink{ML antiquotation.term}{\mbox{\isa{term}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   487   \indexdef{}{ML antiquotation}{prop}\hypertarget{ML antiquotation.prop}{\hyperlink{ML antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   488   \end{matharray}

   490   \begin{railoutput}

   491 \rail@begin{2}{}

   492 \rail@bar

   493 \rail@term{\hyperlink{ML antiquotation.const-name}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}name}}}}[]

   494 \rail@nextbar{1}

   495 \rail@term{\hyperlink{ML antiquotation.const-abbrev}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}abbrev}}}}[]

   496 \rail@endbar

   497 \rail@nont{\isa{nameref}}[]

   498 \rail@end

   499 \rail@begin{3}{}

   500 \rail@term{\hyperlink{ML antiquotation.const}{\mbox{\isa{const}}}}[]

   501 \rail@bar

   502 \rail@nextbar{1}

   503 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

   504 \rail@plus

   505 \rail@nont{\isa{type}}[]

   506 \rail@nextplus{2}

   507 \rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]

   508 \rail@endplus

   509 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

   510 \rail@endbar

   511 \rail@end

   512 \rail@begin{1}{}

   513 \rail@term{\hyperlink{ML antiquotation.term}{\mbox{\isa{term}}}}[]

   514 \rail@nont{\isa{term}}[]

   515 \rail@end

   516 \rail@begin{1}{}

   517 \rail@term{\hyperlink{ML antiquotation.prop}{\mbox{\isa{prop}}}}[]

   518 \rail@nont{\isa{prop}}[]

   519 \rail@end

   520 \end{railoutput}

   523   \begin{description}

   525   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}const{\isaliteral{5F}{\isacharunderscore}}name\ c{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized logical

   526   constant name \isa{c} --- as \verb|string| literal.

   528   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}const{\isaliteral{5F}{\isacharunderscore}}abbrev\ c{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized

   529   abbreviated constant name \isa{c} --- as \verb|string|

   530   literal.

   532   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}const\ c{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized

   533   constant \isa{c} with precise type instantiation in the sense of

   534   \verb|Sign.const_instance| --- as \verb|Const| constructor term for

   535   datatype \verb|term|.

   537   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}term\ t{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized term \isa{t}

   538   --- as constructor term for datatype \verb|term|.

   540   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}prop\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{7D}{\isacharbraceright}}} inlines the internalized proposition

   541   \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} --- as constructor term for datatype \verb|term|.

   543   \end{description}%

   544 \end{isamarkuptext}%

   545 \isamarkuptrue%

   546 %

   547 \endisatagmlantiq

   548 {\isafoldmlantiq}%

   549 %

   550 \isadelimmlantiq

   551 %

   552 \endisadelimmlantiq

   553 %

   554 \isamarkupsection{Theorems \label{sec:thms}%

   555 }

   556 \isamarkuptrue%

   557 %

   558 \begin{isamarkuptext}%

   559 A \emph{proposition} is a well-typed term of type \isa{prop}, a

   560   \emph{theorem} is a proven proposition (depending on a context of

   561   hypotheses and the background theory).  Primitive inferences include

   562   plain Natural Deduction rules for the primary connectives \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} and \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} of the framework.  There is also a builtin

   563   notion of equality/equivalence \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}}.%

   564 \end{isamarkuptext}%

   565 \isamarkuptrue%

   566 %

   567 \isamarkupsubsection{Primitive connectives and rules \label{sec:prim-rules}%

   568 }

   569 \isamarkuptrue%

   570 %

   571 \begin{isamarkuptext}%

   572 The theory \isa{Pure} contains constant declarations for the

   573   primitive connectives \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}}, \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}, and \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}} of

   574   the logical framework, see \figref{fig:pure-connectives}.  The

   575   derivability judgment \isa{A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B} is

   576   defined inductively by the primitive inferences given in

   577   \figref{fig:prim-rules}, with the global restriction that the

   578   hypotheses must \emph{not} contain any schematic variables.  The

   579   builtin equality is conceptually axiomatized as shown in

   580   \figref{fig:pure-equality}, although the implementation works

   581   directly with derived inferences.

   583   \begin{figure}[htb]

   584   \begin{center}

   585   \begin{tabular}{ll}

   586   \isa{all\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} & universal quantification (binder \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}}) \\

   587   \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ prop\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} & implication (right associative infix) \\

   588   \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} & equality relation (infix) \\

   589   \end{tabular}

   590   \caption{Primitive connectives of Pure}\label{fig:pure-connectives}

   591   \end{center}

   592   \end{figure}

   594   \begin{figure}[htb]

   595   \begin{center}

   596   \[

   597   \infer[\isa{{\isaliteral{28}{\isacharparenleft}}axiom{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}}{\isa{A\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C54686574613E}{\isasymTheta}}}}

   598   \qquad

   599   \infer[\isa{{\isaliteral{28}{\isacharparenleft}}assume{\isaliteral{29}{\isacharparenright}}}]{\isa{A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}}{}

   600   \]

   601   \[

   602   \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}} & \isa{x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}}

   603   \qquad

   604   \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ b{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}}}

   605   \]

   606   \[

   607   \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{2D}{\isacharminus}}\ A\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}

   608   \qquad

   609   \infer[\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}elim{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B} & \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}}

   610   \]

   611   \caption{Primitive inferences of Pure}\label{fig:prim-rules}

   612   \end{center}

   613   \end{figure}

   615   \begin{figure}[htb]

   616   \begin{center}

   617   \begin{tabular}{ll}

   618   \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ b{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ a\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ b{\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}} & \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}}-conversion \\

   619   \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ x} & reflexivity \\

   620   \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ y} & substitution \\

   621   \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ g\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ f\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ g} & extensionality \\

   622   \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ B} & logical equivalence \\

   623   \end{tabular}

   624   \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}

   625   \end{center}

   626   \end{figure}

   628   The introduction and elimination rules for \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} and \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} are analogous to formation of dependently typed \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-terms representing the underlying proof objects.  Proof terms

   629   are irrelevant in the Pure logic, though; they cannot occur within

   630   propositions.  The system provides a runtime option to record

   631   explicit proof terms for primitive inferences.  Thus all three

   632   levels of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-calculus become explicit: \isa{{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}} for

   633   terms, and \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} for proofs (cf.\

   634   \cite{Berghofer-Nipkow:2000:TPHOL}).

   636   Observe that locally fixed parameters (as in \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{5C3C68797068656E3E}{\isasymhyphen}}intro}) need not be recorded in the hypotheses, because

   637   the simple syntactic types of Pure are always inhabitable.

   638   ``Assumptions'' \isa{x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}} for type-membership are only

   639   present as long as some \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}} occurs in the statement

   640   body.\footnote{This is the key difference to ``\isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}HOL}'' in

   641   the PTS framework \cite{Barendregt-Geuvers:2001}, where hypotheses

   642   \isa{x\ {\isaliteral{3A}{\isacharcolon}}\ A} are treated uniformly for propositions and types.}

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

   645   forming all instances of type and term variables: \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}} holds for any substitution instance of an axiom

   646   \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A}.  By pushing substitutions through derivations

   647   inductively, we also get admissible \isa{generalize} and \isa{instantiate} rules as shown in \figref{fig:subst-rules}.

   649   \begin{figure}[htb]

   650   \begin{center}

   651   \[

   652   \infer{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}} & \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}}

   653   \quad

   654   \infer[\quad\isa{{\isaliteral{28}{\isacharparenleft}}generalize{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}} & \isa{x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}}}

   655   \]

   656   \[

   657   \infer{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}}}

   658   \quad

   659   \infer[\quad\isa{{\isaliteral{28}{\isacharparenleft}}instantiate{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}t{\isaliteral{5D}{\isacharbrackright}}}}{\isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}}}

   660   \]

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

   662   \end{center}

   663   \end{figure}

   665   Note that \isa{instantiate} does not require an explicit

   666   side-condition, because \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} may never contain schematic

   667   variables.

   669   In principle, variables could be substituted in hypotheses as well,

   670   but this would disrupt the monotonicity of reasoning: deriving

   671   \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}} from \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ B} is

   672   correct, but \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{5C3C73757073657465713E}{\isasymsupseteq}}\ {\isaliteral{5C3C47616D6D613E}{\isasymGamma}}} does not necessarily hold:

   673   the result belongs to a different proof context.

   675   \medskip An \emph{oracle} is a function that produces axioms on the

   676   fly.  Logically, this is an instance of the \isa{axiom} rule

   677   (\figref{fig:prim-rules}), but there is an operational difference.

   678   The system always records oracle invocations within derivations of

   679   theorems by a unique tag.

   681   Axiomatizations should be limited to the bare minimum, typically as

   682   part of the initial logical basis of an object-logic formalization.

   683   Later on, theories are usually developed in a strictly definitional

   684   fashion, by stating only certain equalities over new constants.

   686   A \emph{simple definition} consists of a constant declaration \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} together with an axiom \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t}, where \isa{t\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} is a closed term without any hidden polymorphism.  The RHS

   687   may depend on further defined constants, but not \isa{c} itself.

   688   Definitions of functions may be presented as \isa{c\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t} instead of the puristic \isa{c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ t}.

   690   An \emph{overloaded definition} consists of a collection of axioms

   691   for the same constant, with zero or one equations \isa{c{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t} for each type constructor \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} (for

   692   distinct variables \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}).  The RHS may mention

   693   previously defined constants as above, or arbitrary constants \isa{d{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{29}{\isacharparenright}}} for some \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub i} projected from \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}}.  Thus overloaded definitions essentially work by

   694   primitive recursion over the syntactic structure of a single type

   695   argument.  See also \cite[\S4.3]{Haftmann-Wenzel:2006:classes}.%

   696 \end{isamarkuptext}%

   697 \isamarkuptrue%

   698 %

   699 \isadelimmlref

   700 %

   701 \endisadelimmlref

   702 %

   703 \isatagmlref

   704 %

   705 \begin{isamarkuptext}%

   706 \begin{mldecls}

   707   \indexdef{}{ML}{Logic.all}\verb|Logic.all: term -> term -> term| \\

   708   \indexdef{}{ML}{Logic.mk\_implies}\verb|Logic.mk_implies: term * term -> term| \\

   709   \end{mldecls}

   710   \begin{mldecls}

   711   \indexdef{}{ML type}{ctyp}\verb|type ctyp| \\

   712   \indexdef{}{ML type}{cterm}\verb|type cterm| \\

   713   \indexdef{}{ML}{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\

   714   \indexdef{}{ML}{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\

   715   \indexdef{}{ML}{Thm.apply}\verb|Thm.apply: cterm -> cterm -> cterm| \\

   716   \indexdef{}{ML}{Thm.lambda}\verb|Thm.lambda: cterm -> cterm -> cterm| \\

   717   \indexdef{}{ML}{Thm.all}\verb|Thm.all: cterm -> cterm -> cterm| \\

   718   \indexdef{}{ML}{Drule.mk\_implies}\verb|Drule.mk_implies: cterm * cterm -> cterm| \\

   719   \end{mldecls}

   720   \begin{mldecls}

   721   \indexdef{}{ML type}{thm}\verb|type thm| \\

   722   \indexdef{}{ML}{proofs}\verb|proofs: int Unsynchronized.ref| \\

   723   \indexdef{}{ML}{Thm.transfer}\verb|Thm.transfer: theory -> thm -> thm| \\

   724   \indexdef{}{ML}{Thm.assume}\verb|Thm.assume: cterm -> thm| \\

   725   \indexdef{}{ML}{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\

   726   \indexdef{}{ML}{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\

   727   \indexdef{}{ML}{Thm.implies\_intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\

   728   \indexdef{}{ML}{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\

   729   \indexdef{}{ML}{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\

   730   \indexdef{}{ML}{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\

   731   \indexdef{}{ML}{Thm.add\_axiom}\verb|Thm.add_axiom: Proof.context ->|\isasep\isanewline%

   732 \verb|  binding * term -> theory -> (string * thm) * theory| \\

   733   \indexdef{}{ML}{Thm.add\_oracle}\verb|Thm.add_oracle: binding * ('a -> cterm) -> theory ->|\isasep\isanewline%

   734 \verb|  (string * ('a -> thm)) * theory| \\

   735   \indexdef{}{ML}{Thm.add\_def}\verb|Thm.add_def: Proof.context -> bool -> bool ->|\isasep\isanewline%

   736 \verb|  binding * term -> theory -> (string * thm) * theory| \\

   737   \end{mldecls}

   738   \begin{mldecls}

   739   \indexdef{}{ML}{Theory.add\_deps}\verb|Theory.add_deps: Proof.context -> string ->|\isasep\isanewline%

   740 \verb|  string * typ -> (string * typ) list -> theory -> theory| \\

   741   \end{mldecls}

   743   \begin{description}

   745   \item \verb|Logic.all|~\isa{a\ B} produces a Pure quantification

   746   \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}a{\isaliteral{2E}{\isachardot}}\ B}, where occurrences of the atomic term \isa{a} in

   747   the body proposition \isa{B} are replaced by bound variables.

   748   (See also \verb|lambda| on terms.)

   750   \item \verb|Logic.mk_implies|~\isa{{\isaliteral{28}{\isacharparenleft}}A{\isaliteral{2C}{\isacharcomma}}\ B{\isaliteral{29}{\isacharparenright}}} produces a Pure

   751   implication \isa{A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}.

   753   \item Types \verb|ctyp| and \verb|cterm| represent certified

   754   types and terms, respectively.  These are abstract datatypes that

   755   guarantee that its values have passed the full well-formedness (and

   756   well-typedness) checks, relative to the declarations of type

   757   constructors, constants etc.\ in the background theory.  The

   758   abstract types \verb|ctyp| and \verb|cterm| are part of the

   759   same inference kernel that is mainly responsible for \verb|thm|.

   760   Thus syntactic operations on \verb|ctyp| and \verb|cterm|

   761   are located in the \verb|Thm| module, even though theorems are

   762   not yet involved at that stage.

   764   \item \verb|Thm.ctyp_of|~\isa{thy\ {\isaliteral{5C3C7461753E}{\isasymtau}}} and \verb|Thm.cterm_of|~\isa{thy\ t} explicitly checks types and terms,

   765   respectively.  This also involves some basic normalizations, such

   766   expansion of type and term abbreviations from the theory context.

   767   Full re-certification is relatively slow and should be avoided in

   768   tight reasoning loops.

   770   \item \verb|Thm.apply|, \verb|Thm.lambda|, \verb|Thm.all|, \verb|Drule.mk_implies| etc.\ compose certified terms (or propositions)

   771   incrementally.  This is equivalent to \verb|Thm.cterm_of| after

   772   unchecked \verb|$|, \verb|lambda|, \verb|Logic.all|, \verb|Logic.mk_implies| etc., but there can be a big difference in

   773   performance when large existing entities are composed by a few extra

   774   constructions on top.  There are separate operations to decompose

   775   certified terms and theorems to produce certified terms again.

   777   \item Type \verb|thm| represents proven propositions.  This is

   778   an abstract datatype that guarantees that its values have been

   779   constructed by basic principles of the \verb|Thm| module.

   780   Every \verb|thm| value contains a sliding back-reference to the

   781   enclosing theory, cf.\ \secref{sec:context-theory}.

   783   \item \verb|proofs| specifies the detail of proof recording within

   784   \verb|thm| values: \verb|0| records only the names of oracles,

   785   \verb|1| records oracle names and propositions, \verb|2| additionally

   786   records full proof terms.  Officially named theorems that contribute

   787   to a result are recorded in any case.

   789   \item \verb|Thm.transfer|~\isa{thy\ thm} transfers the given

   790   theorem to a \emph{larger} theory, see also \secref{sec:context}.

   791   This formal adjustment of the background context has no logical

   792   significance, but is occasionally required for formal reasons, e.g.\

   793   when theorems that are imported from more basic theories are used in

   794   the current situation.

   796   \item \verb|Thm.assume|, \verb|Thm.forall_intr|, \verb|Thm.forall_elim|, \verb|Thm.implies_intr|, and \verb|Thm.implies_elim|

   797   correspond to the primitive inferences of \figref{fig:prim-rules}.

   799   \item \verb|Thm.generalize|~\isa{{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}}

   800   corresponds to the \isa{generalize} rules of

   801   \figref{fig:subst-rules}.  Here collections of type and term

   802   variables are generalized simultaneously, specified by the given

   803   basic names.

   805   \item \verb|Thm.instantiate|~\isa{{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub s{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} corresponds to the \isa{instantiate} rules

   806   of \figref{fig:subst-rules}.  Type variables are substituted before

   807   term variables.  Note that the types in \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}}

   808   refer to the instantiated versions.

   810   \item \verb|Thm.add_axiom|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}} declares an

   811   arbitrary proposition as axiom, and retrieves it as a theorem from

   812   the resulting theory, cf.\ \isa{axiom} in

   813   \figref{fig:prim-rules}.  Note that the low-level representation in

   814   the axiom table may differ slightly from the returned theorem.

   816   \item \verb|Thm.add_oracle|~\isa{{\isaliteral{28}{\isacharparenleft}}binding{\isaliteral{2C}{\isacharcomma}}\ oracle{\isaliteral{29}{\isacharparenright}}} produces a named

   817   oracle rule, essentially generating arbitrary axioms on the fly,

   818   cf.\ \isa{axiom} in \figref{fig:prim-rules}.

   820   \item \verb|Thm.add_def|~\isa{ctxt\ unchecked\ overloaded\ {\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ c\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{29}{\isacharparenright}}} states a definitional axiom for an existing constant

   821   \isa{c}.  Dependencies are recorded via \verb|Theory.add_deps|,

   822   unless the \isa{unchecked} option is set.  Note that the

   823   low-level representation in the axiom table may differ slightly from

   824   the returned theorem.

   826   \item \verb|Theory.add_deps|~\isa{ctxt\ name\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}

   827   declares dependencies of a named specification for constant \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}}, relative to existing specifications for constants \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}.

   829   \end{description}%

   830 \end{isamarkuptext}%

   831 \isamarkuptrue%

   832 %

   833 \endisatagmlref

   834 {\isafoldmlref}%

   835 %

   836 \isadelimmlref

   837 %

   838 \endisadelimmlref

   839 %

   840 \isadelimmlantiq

   841 %

   842 \endisadelimmlantiq

   843 %

   844 \isatagmlantiq

   845 %

   846 \begin{isamarkuptext}%

   847 \begin{matharray}{rcl}

   848   \indexdef{}{ML antiquotation}{ctyp}\hypertarget{ML antiquotation.ctyp}{\hyperlink{ML antiquotation.ctyp}{\mbox{\isa{ctyp}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   849   \indexdef{}{ML antiquotation}{cterm}\hypertarget{ML antiquotation.cterm}{\hyperlink{ML antiquotation.cterm}{\mbox{\isa{cterm}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   850   \indexdef{}{ML antiquotation}{cprop}\hypertarget{ML antiquotation.cprop}{\hyperlink{ML antiquotation.cprop}{\mbox{\isa{cprop}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   851   \indexdef{}{ML antiquotation}{thm}\hypertarget{ML antiquotation.thm}{\hyperlink{ML antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   852   \indexdef{}{ML antiquotation}{thms}\hypertarget{ML antiquotation.thms}{\hyperlink{ML antiquotation.thms}{\mbox{\isa{thms}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   853   \indexdef{}{ML antiquotation}{lemma}\hypertarget{ML antiquotation.lemma}{\hyperlink{ML antiquotation.lemma}{\mbox{\isa{lemma}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\

   854   \end{matharray}

   856   \begin{railoutput}

   857 \rail@begin{1}{}

   858 \rail@term{\hyperlink{ML antiquotation.ctyp}{\mbox{\isa{ctyp}}}}[]

   859 \rail@nont{\isa{typ}}[]

   860 \rail@end

   861 \rail@begin{1}{}

   862 \rail@term{\hyperlink{ML antiquotation.cterm}{\mbox{\isa{cterm}}}}[]

   863 \rail@nont{\isa{term}}[]

   864 \rail@end

   865 \rail@begin{1}{}

   866 \rail@term{\hyperlink{ML antiquotation.cprop}{\mbox{\isa{cprop}}}}[]

   867 \rail@nont{\isa{prop}}[]

   868 \rail@end

   869 \rail@begin{1}{}

   870 \rail@term{\hyperlink{ML antiquotation.thm}{\mbox{\isa{thm}}}}[]

   871 \rail@nont{\isa{thmref}}[]

   872 \rail@end

   873 \rail@begin{1}{}

   874 \rail@term{\hyperlink{ML antiquotation.thms}{\mbox{\isa{thms}}}}[]

   875 \rail@nont{\isa{thmrefs}}[]

   876 \rail@end

   877 \rail@begin{6}{}

   878 \rail@term{\hyperlink{ML antiquotation.lemma}{\mbox{\isa{lemma}}}}[]

   879 \rail@bar

   880 \rail@nextbar{1}

   881 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]

   882 \rail@term{\isa{\isakeyword{open}}}[]

   883 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]

   884 \rail@endbar

   885 \rail@plus

   886 \rail@plus

   887 \rail@nont{\isa{prop}}[]

   888 \rail@nextplus{1}

   889 \rail@endplus

   890 \rail@nextplus{2}

   891 \rail@cterm{\isa{\isakeyword{and}}}[]

   892 \rail@endplus

   893 \rail@cr{4}

   894 \rail@term{\isa{\isakeyword{by}}}[]

   895 \rail@nont{\isa{method}}[]

   896 \rail@bar

   897 \rail@nextbar{5}

   898 \rail@nont{\isa{method}}[]

   899 \rail@endbar

   900 \rail@end

   901 \end{railoutput}

   904   \begin{description}

   906   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}ctyp\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{7D}{\isacharbraceright}}} produces a certified type wrt.\ the

   907   current background theory --- as abstract value of type \verb|ctyp|.

   909   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}cterm\ t{\isaliteral{7D}{\isacharbraceright}}} and \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}cprop\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{7D}{\isacharbraceright}}} produce a

   910   certified term wrt.\ the current background theory --- as abstract

   911   value of type \verb|cterm|.

   913   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}thm\ a{\isaliteral{7D}{\isacharbraceright}}} produces a singleton fact --- as abstract

   914   value of type \verb|thm|.

   916   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}thms\ a{\isaliteral{7D}{\isacharbraceright}}} produces a general fact --- as abstract

   917   value of type \verb|thm list|.

   919   \item \isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}lemma\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ by\ meth{\isaliteral{7D}{\isacharbraceright}}} produces a fact that is proven on

   920   the spot according to the minimal proof, which imitates a terminal

   921   Isar proof.  The result is an abstract value of type \verb|thm|

   922   or \verb|thm list|, depending on the number of propositions

   923   given here.

   925   The internal derivation object lacks a proper theorem name, but it

   926   is formally closed, unless the \isa{{\isaliteral{28}{\isacharparenleft}}open{\isaliteral{29}{\isacharparenright}}} option is specified

   927   (this may impact performance of applications with proof terms).

   929   Since ML antiquotations are always evaluated at compile-time, there

   930   is no run-time overhead even for non-trivial proofs.  Nonetheless,

   931   the justification is syntactically limited to a single \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}} step.  More complex Isar proofs should be done in regular

   932   theory source, before compiling the corresponding ML text that uses

   933   the result.

   935   \end{description}%

   936 \end{isamarkuptext}%

   937 \isamarkuptrue%

   938 %

   939 \endisatagmlantiq

   940 {\isafoldmlantiq}%

   941 %

   942 \isadelimmlantiq

   943 %

   944 \endisadelimmlantiq

   945 %

   946 \isamarkupsubsection{Auxiliary connectives \label{sec:logic-aux}%

   947 }

   948 \isamarkuptrue%

   949 %

   950 \begin{isamarkuptext}%

   951 Theory \isa{Pure} provides a few auxiliary connectives

   952   that are defined on top of the primitive ones, see

   953   \figref{fig:pure-aux}.  These special constants are useful in

   954   certain internal encodings, and are normally not directly exposed to

   955   the user.

   957   \begin{figure}[htb]

   958   \begin{center}

   959   \begin{tabular}{ll}

   960   \isa{conjunction\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ prop\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} & (infix \isa{{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}}) \\

   961   \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A\ {\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}C{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{29}{\isacharparenright}}} \\[1ex]

   962   \isa{prop\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ prop\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} & (prefix \isa{{\isaliteral{23}{\isacharhash}}}, suppressed) \\

   963   \isa{{\isaliteral{23}{\isacharhash}}A\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ A} \\[1ex]

   964   \isa{term\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} & (prefix \isa{TERM}) \\

   965   \isa{term\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}A{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A{\isaliteral{29}{\isacharparenright}}} \\[1ex]

   966   \isa{TYPE\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ itself} & (prefix \isa{TYPE}) \\

   967   \isa{{\isaliteral{28}{\isacharparenleft}}unspecified{\isaliteral{29}{\isacharparenright}}} \\

   968   \end{tabular}

   969   \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}

   970   \end{center}

   971   \end{figure}

   973   The introduction \isa{A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}\ B}, and eliminations

   974   (projections) \isa{A\ {\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A} and \isa{A\ {\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B} are

   975   available as derived rules.  Conjunction allows to treat

   976   simultaneous assumptions and conclusions uniformly, e.g.\ consider

   977   \isa{A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C\ {\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}\ D}.  In particular, the goal mechanism

   978   represents multiple claims as explicit conjunction internally, but

   979   this is refined (via backwards introduction) into separate sub-goals

   980   before the user commences the proof; the final result is projected

   981   into a list of theorems using eliminations (cf.\

   982   \secref{sec:tactical-goals}).

   984   The \isa{prop} marker (\isa{{\isaliteral{23}{\isacharhash}}}) makes arbitrarily complex

   985   propositions appear as atomic, without changing the meaning: \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ A} and \isa{{\isaliteral{5C3C47616D6D613E}{\isasymGamma}}\ {\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ {\isaliteral{23}{\isacharhash}}A} are interchangeable.  See

   986   \secref{sec:tactical-goals} for specific operations.

   988   The \isa{term} marker turns any well-typed term into a derivable

   989   proposition: \isa{{\isaliteral{5C3C7475726E7374696C653E}{\isasymturnstile}}\ TERM\ t} holds unconditionally.  Although

   990   this is logically vacuous, it allows to treat terms and proofs

   991   uniformly, similar to a type-theoretic framework.

   993   The \isa{TYPE} constructor is the canonical representative of

   994   the unspecified type \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ itself}; it essentially injects the

   995   language of types into that of terms.  There is specific notation

   996   \isa{TYPE{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} for \isa{TYPE\isaliteral{5C3C5E627375623E}{}\isactrlbsub {\isaliteral{5C3C7461753E}{\isasymtau}}\ itself\isaliteral{5C3C5E657375623E}{}\isactrlesub }.

   997   Although being devoid of any particular meaning, the term \isa{TYPE{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} accounts for the type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} within the term

   998   language.  In particular, \isa{TYPE{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}} may be used as formal

   999   argument in primitive definitions, in order to circumvent hidden

  1000   polymorphism (cf.\ \secref{sec:terms}).  For example, \isa{c\ TYPE{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ A{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5D}{\isacharbrackright}}} defines \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\ itself\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop} in terms of

  1001   a proposition \isa{A} that depends on an additional type

  1002   argument, which is essentially a predicate on types.%

  1003 \end{isamarkuptext}%

  1004 \isamarkuptrue%

  1005 %

  1006 \isadelimmlref

  1007 %

  1008 \endisadelimmlref

  1009 %

  1010 \isatagmlref

  1011 %

  1012 \begin{isamarkuptext}%

  1013 \begin{mldecls}

  1014   \indexdef{}{ML}{Conjunction.intr}\verb|Conjunction.intr: thm -> thm -> thm| \\

  1015   \indexdef{}{ML}{Conjunction.elim}\verb|Conjunction.elim: thm -> thm * thm| \\

  1016   \indexdef{}{ML}{Drule.mk\_term}\verb|Drule.mk_term: cterm -> thm| \\

  1017   \indexdef{}{ML}{Drule.dest\_term}\verb|Drule.dest_term: thm -> cterm| \\

  1018   \indexdef{}{ML}{Logic.mk\_type}\verb|Logic.mk_type: typ -> term| \\

  1019   \indexdef{}{ML}{Logic.dest\_type}\verb|Logic.dest_type: term -> typ| \\

  1020   \end{mldecls}

  1022   \begin{description}

  1024   \item \verb|Conjunction.intr| derives \isa{A\ {\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}\ B} from \isa{A} and \isa{B}.

  1026   \item \verb|Conjunction.elim| derives \isa{A} and \isa{B}

  1027   from \isa{A\ {\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}{\isaliteral{26}{\isacharampersand}}\ B}.

  1029   \item \verb|Drule.mk_term| derives \isa{TERM\ t}.

  1031   \item \verb|Drule.dest_term| recovers term \isa{t} from \isa{TERM\ t}.

  1033   \item \verb|Logic.mk_type|~\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} produces the term \isa{TYPE{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}}.

  1035   \item \verb|Logic.dest_type|~\isa{TYPE{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} recovers the type

  1036   \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}.

  1038   \end{description}%

  1039 \end{isamarkuptext}%

  1040 \isamarkuptrue%

  1041 %

  1042 \endisatagmlref

  1043 {\isafoldmlref}%

  1044 %

  1045 \isadelimmlref

  1046 %

  1047 \endisadelimmlref

  1048 %

  1049 \isamarkupsection{Object-level rules \label{sec:obj-rules}%

  1050 }

  1051 \isamarkuptrue%

  1052 %

  1053 \begin{isamarkuptext}%

  1054 The primitive inferences covered so far mostly serve foundational

  1055   purposes.  User-level reasoning usually works via object-level rules

  1056   that are represented as theorems of Pure.  Composition of rules

  1057   involves \emph{backchaining}, \emph{higher-order unification} modulo

  1058   \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}}-conversion of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-terms, and so-called

  1059   \emph{lifting} of rules into a context of \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} and \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} connectives.  Thus the full power of higher-order Natural

  1060   Deduction in Isabelle/Pure becomes readily available.%

  1061 \end{isamarkuptext}%

  1062 \isamarkuptrue%

  1063 %

  1064 \isamarkupsubsection{Hereditary Harrop Formulae%

  1065 }

  1066 \isamarkuptrue%

  1067 %

  1068 \begin{isamarkuptext}%

  1069 The idea of object-level rules is to model Natural Deduction

  1070   inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow

  1071   arbitrary nesting similar to \cite{extensions91}.  The most basic

  1072   rule format is that of a \emph{Horn Clause}:

  1073   \[

  1074   \infer{\isa{A}}{\isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} & \isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}} & \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub n}}

  1075   \]

  1076   where \isa{A{\isaliteral{2C}{\isacharcomma}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n} are atomic propositions

  1077   of the framework, usually of the form \isa{Trueprop\ B}, where

  1078   \isa{B} is a (compound) object-level statement.  This

  1079   object-level inference corresponds to an iterated implication in

  1080   Pure like this:

  1081   \[

  1082   \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A}

  1083   \]

  1084   As an example consider conjunction introduction: \isa{A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B}.  Any parameters occurring in such rule statements are

  1085   conceptionally treated as arbitrary:

  1086   \[

  1087   \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2E}{\isachardot}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub m}

  1088   \]

  1090   Nesting of rules means that the positions of \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub i} may

  1091   again hold compound rules, not just atomic propositions.

  1092   Propositions of this format are called \emph{Hereditary Harrop

  1093   Formulae} in the literature \cite{Miller:1991}.  Here we give an

  1094   inductive characterization as follows:

  1096   \medskip

  1097   \begin{tabular}{ll}

  1098   \isa{\isaliteral{5C3C5E626F6C643E}{}\isactrlbold x} & set of variables \\

  1099   \isa{\isaliteral{5C3C5E626F6C643E}{}\isactrlbold A} & set of atomic propositions \\

  1100   \isa{\isaliteral{5C3C5E626F6C643E}{}\isactrlbold H\ \ {\isaliteral{3D}{\isacharequal}}\ \ {\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold x\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E626F6C643E}{}\isactrlbold H\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \isaliteral{5C3C5E626F6C643E}{}\isactrlbold A} & set of Hereditary Harrop Formulas \\

  1101   \end{tabular}

  1102   \medskip

  1104   Thus we essentially impose nesting levels on propositions formed

  1105   from \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}} and \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}.  At each level there is a prefix

  1106   of parameters and compound premises, concluding an atomic

  1107   proposition.  Typical examples are \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}-introduction \isa{{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B} or mathematical induction \isa{P\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ P\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n}.  Even deeper nesting occurs in well-founded

  1108   induction \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}y{\isaliteral{2E}{\isachardot}}\ y\ {\isaliteral{5C3C707265633E}{\isasymprec}}\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x}, but this

  1109   already marks the limit of rule complexity that is usually seen in

  1110   practice.

  1112   \medskip Regular user-level inferences in Isabelle/Pure always

  1113   maintain the following canonical form of results:

  1115   \begin{itemize}

  1117   \item Normalization by \isa{{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{29}{\isacharparenright}}},

  1118   which is a theorem of Pure, means that quantifiers are pushed in

  1119   front of implication at each level of nesting.  The normal form is a

  1120   Hereditary Harrop Formula.

  1122   \item The outermost prefix of parameters is represented via

  1123   schematic variables: instead of \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x} we have \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec H\ {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x}.

  1124   Note that this representation looses information about the order of

  1125   parameters, and vacuous quantifiers vanish automatically.

  1127   \end{itemize}%

  1128 \end{isamarkuptext}%

  1129 \isamarkuptrue%

  1130 %

  1131 \isadelimmlref

  1132 %

  1133 \endisadelimmlref

  1134 %

  1135 \isatagmlref

  1136 %

  1137 \begin{isamarkuptext}%

  1138 \begin{mldecls}

  1139   \indexdef{}{ML}{Simplifier.norm\_hhf}\verb|Simplifier.norm_hhf: thm -> thm| \\

  1140   \end{mldecls}

  1142   \begin{description}

  1144   \item \verb|Simplifier.norm_hhf|~\isa{thm} normalizes the given

  1145   theorem according to the canonical form specified above.  This is

  1146   occasionally helpful to repair some low-level tools that do not

  1147   handle Hereditary Harrop Formulae properly.

  1149   \end{description}%

  1150 \end{isamarkuptext}%

  1151 \isamarkuptrue%

  1152 %

  1153 \endisatagmlref

  1154 {\isafoldmlref}%

  1155 %

  1156 \isadelimmlref

  1157 %

  1158 \endisadelimmlref

  1159 %

  1160 \isamarkupsubsection{Rule composition%

  1161 }

  1162 \isamarkuptrue%

  1163 %

  1164 \begin{isamarkuptext}%

  1165 The rule calculus of Isabelle/Pure provides two main inferences:

  1166   \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} (i.e.\ back-chaining of rules) and

  1167   \hyperlink{inference.assumption}{\mbox{\isa{assumption}}} (i.e.\ closing a branch), both modulo

  1168   higher-order unification.  There are also combined variants, notably

  1169   \hyperlink{inference.elim-resolution}{\mbox{\isa{elim{\isaliteral{5F}{\isacharunderscore}}resolution}}} and \hyperlink{inference.dest-resolution}{\mbox{\isa{dest{\isaliteral{5F}{\isacharunderscore}}resolution}}}.

  1171   To understand the all-important \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} principle,

  1172   we first consider raw \indexdef{}{inference}{composition}\hypertarget{inference.composition}{\hyperlink{inference.composition}{\mbox{\isa{composition}}}} (modulo

  1173   higher-order unification with substitution \isa{{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}}):

  1174   \[

  1175   \infer[(\indexdef{}{inference}{composition}\hypertarget{inference.composition}{\hyperlink{inference.composition}{\mbox{\isa{composition}}}})]{\isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec A{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}}}

  1176   {\isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B} & \isa{B{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C} & \isa{B{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}}}

  1177   \]

  1178   Here the conclusion of the first rule is unified with the premise of

  1179   the second; the resulting rule instance inherits the premises of the

  1180   first and conclusion of the second.  Note that \isa{C} can again

  1181   consist of iterated implications.  We can also permute the premises

  1182   of the second rule back-and-forth in order to compose with \isa{B{\isaliteral{27}{\isacharprime}}} in any position (subsequently we shall always refer to

  1183   position 1 w.l.o.g.).

  1185   In \hyperlink{inference.composition}{\mbox{\isa{composition}}} the internal structure of the common

  1186   part \isa{B} and \isa{B{\isaliteral{27}{\isacharprime}}} is not taken into account.  For

  1187   proper \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} we require \isa{B} to be atomic,

  1188   and explicitly observe the structure \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{27}{\isacharprime}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x} of the premise of the second rule.  The

  1189   idea is to adapt the first rule by ``lifting'' it into this context,

  1190   by means of iterated application of the following inferences:

  1191   \[

  1192   \infer[(\indexdef{}{inference}{imp\_lift}\hypertarget{inference.imp-lift}{\hyperlink{inference.imp-lift}{\mbox{\isa{imp{\isaliteral{5F}{\isacharunderscore}}lift}}}})]{\isa{{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec H\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{29}{\isacharparenright}}}}{\isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}}

  1193   \]

  1194   \[

  1195   \infer[(\indexdef{}{inference}{all\_lift}\hypertarget{inference.all-lift}{\hyperlink{inference.all-lift}{\mbox{\isa{all{\isaliteral{5F}{\isacharunderscore}}lift}}}})]{\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec A\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ B\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}}{\isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec A\ {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a}}

  1196   \]

  1197   By combining raw composition with lifting, we get full \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} as follows:

  1198   \[

  1199   \infer[(\indexdef{}{inference}{resolution}\hypertarget{inference.resolution}{\hyperlink{inference.resolution}{\mbox{\isa{resolution}}}})]

  1200   {\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec A\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}}}

  1201   {\begin{tabular}{l}

  1202     \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec A\ {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a} \\

  1203     \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{27}{\isacharprime}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C} \\

  1204     \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ B\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}\isaliteral{5C3C5E7665633E}{}\isactrlvec a\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}} \\

  1205    \end{tabular}}

  1206   \]

  1208   Continued resolution of rules allows to back-chain a problem towards

  1209   more and sub-problems.  Branches are closed either by resolving with

  1210   a rule of 0 premises, or by producing a ``short-circuit'' within a

  1211   solved situation (again modulo unification):

  1212   \[

  1213   \infer[(\indexdef{}{inference}{assumption}\hypertarget{inference.assumption}{\hyperlink{inference.assumption}{\mbox{\isa{assumption}}}})]{\isa{C{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}}}

  1214   {\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}\isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{2E}{\isachardot}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec H\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C} & \isa{A{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}\ {\isaliteral{3D}{\isacharequal}}\ H\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{5C3C76617274686574613E}{\isasymvartheta}}}~~\text{(for some~\isa{i})}}

  1215   \]

  1217   FIXME \indexdef{}{inference}{elim\_resolution}\hypertarget{inference.elim-resolution}{\hyperlink{inference.elim-resolution}{\mbox{\isa{elim{\isaliteral{5F}{\isacharunderscore}}resolution}}}}, \indexdef{}{inference}{dest\_resolution}\hypertarget{inference.dest-resolution}{\hyperlink{inference.dest-resolution}{\mbox{\isa{dest{\isaliteral{5F}{\isacharunderscore}}resolution}}}}%

  1218 \end{isamarkuptext}%

  1219 \isamarkuptrue%

  1220 %

  1221 \isadelimmlref

  1222 %

  1223 \endisadelimmlref

  1224 %

  1225 \isatagmlref

  1226 %

  1227 \begin{isamarkuptext}%

  1228 \begin{mldecls}

  1229   \indexdef{}{ML infix}{RSN}\verb|infix RSN: thm * (int * thm) -> thm| \\

  1230   \indexdef{}{ML infix}{RS}\verb|infix RS: thm * thm -> thm| \\

  1232   \indexdef{}{ML infix}{RLN}\verb|infix RLN: thm list * (int * thm list) -> thm list| \\

  1233   \indexdef{}{ML infix}{RL}\verb|infix RL: thm list * thm list -> thm list| \\

  1235   \indexdef{}{ML infix}{MRS}\verb|infix MRS: thm list * thm -> thm| \\

  1236   \indexdef{}{ML infix}{OF}\verb|infix OF: thm * thm list -> thm| \\

  1237   \end{mldecls}

  1239   \begin{description}

  1241   \item \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RSN\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} resolves the conclusion of

  1242   \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} with the \isa{i}-th premise of \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}},

  1243   according to the \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} principle explained above.

  1244   Unless there is precisely one resolvent it raises exception \verb|THM|.

  1246   This corresponds to the rule attribute \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}} in Isar

  1247   source language.

  1249   \item \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RS\ rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} abbreviates \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RS\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}.

  1251   \item \isa{rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RLN\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} joins lists of rules.  For

  1252   every \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} in \isa{rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} in

  1253   \isa{rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}, it resolves the conclusion of \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} with

  1254   the \isa{i}-th premise of \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}, accumulating multiple

  1255   results in one big list.  Note that such strict enumerations of

  1256   higher-order unifications can be inefficient compared to the lazy

  1257   variant seen in elementary tactics like \verb|resolve_tac|.

  1259   \item \isa{rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RL\ rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} abbreviates \isa{rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RLN\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}.

  1261   \item \isa{{\isaliteral{5B}{\isacharbrackleft}}rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ rule\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}\ MRS\ rule} resolves \isa{rule\isaliteral{5C3C5E697375623E}{}\isactrlisub i}

  1262   against premise \isa{i} of \isa{rule}, for \isa{i\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{1}}}.  By working from right to left, newly emerging premises are

  1263   concatenated in the result, without interfering.

  1265   \item \isa{rule\ OF\ rules} abbreviates \isa{rules\ MRS\ rule}.

  1267   This corresponds to the rule attribute \hyperlink{attribute.OF}{\mbox{\isa{OF}}} in Isar

  1268   source language.

  1270   \end{description}%

  1271 \end{isamarkuptext}%

  1272 \isamarkuptrue%

  1273 %

  1274 \endisatagmlref

  1275 {\isafoldmlref}%

  1276 %

  1277 \isadelimmlref

  1278 %

  1279 \endisadelimmlref

  1280 %

  1281 \isadelimtheory

  1282 %

  1283 \endisadelimtheory

  1284 %

  1285 \isatagtheory

  1286 \isacommand{end}\isamarkupfalse%

  1287 %

  1288 \endisatagtheory

  1289 {\isafoldtheory}%

  1290 %

  1291 \isadelimtheory

  1292 %

  1293 \endisadelimtheory

  1294 \isanewline

  1295 \end{isabellebody}%

  1296 %%% Local Variables:

  1297 %%% mode: latex

  1298 %%% TeX-master: "root"

  1299 %%% End:

author	wenzelm
	Wed, 15 Feb 2012 23:19:30 +0100
changeset 47368	89ccf66aa73d
parent 47293	912b42e64fde
child 48045	b9b2e183e94d
permissions	-rw-r--r--