doc-src/IsarImplementation/Thy/document/logic.tex
 author wenzelm Sat May 10 14:13:20 2008 +0200 (2008-05-10) changeset 26873 691f35f855cd parent 26854 9b4aec46ad78 child 28086 db584d1d2af4 permissions -rw-r--r--
updated generated file;
     1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{logic}%

     4 %

     5 \isadelimtheory

     6 \isanewline

     7 \isanewline

     8 \isanewline

     9 %

    10 \endisadelimtheory

    11 %

    12 \isatagtheory

    13 \isacommand{theory}\isamarkupfalse%

    14 \ logic\ \isakeyword{imports}\ base\ \isakeyword{begin}%

    15 \endisatagtheory

    16 {\isafoldtheory}%

    17 %

    18 \isadelimtheory

    19 %

    20 \endisadelimtheory

    21 %

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

    23 }

    24 \isamarkuptrue%

    25 %

    26 \begin{isamarkuptext}%

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

    28   which has been introduced as a natural-deduction framework in

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

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

    31   differences in the specific treatment of simple types in

    32   Isabelle/Pure.

    33

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

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

    36   \isa{{\isasymLongrightarrow}} for implication (proofs depending on proofs).

    37

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

    39   constructors, constants, and axioms.  Theory declarations support

    40   schematic polymorphism, which is strictly speaking outside the

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

    42   context \isa{{\isasymTheta}} is separate from the proof context \isa{{\isasymGamma}}

    43   of the core calculus.}%

    44 \end{isamarkuptext}%

    45 \isamarkuptrue%

    46 %

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

    48 }

    49 \isamarkuptrue%

    50 %

    51 \begin{isamarkuptext}%

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

    53   algebra; types are qualified by ordered type classes.

    54

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

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

    57   generating relation; the transitive closure is maintained

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

    59   transitive, and antisymmetric.

    60

    61   A \emph{sort} is a list of type classes written as \isa{s\ {\isacharequal}\ {\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub m{\isacharbraceright}}, which represents symbolic

    62   intersection.  Notationally, the curly braces are omitted for

    63   singleton intersections, i.e.\ any class \isa{c} may be read as

    64   a sort \isa{{\isacharbraceleft}c{\isacharbraceright}}.  The ordering on type classes is extended to

    65   sorts according to the meaning of intersections: \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ c\isactrlisub m{\isacharbraceright}\ {\isasymsubseteq}\ {\isacharbraceleft}d\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlisub n{\isacharbraceright}} iff

    66   \isa{{\isasymforall}j{\isachardot}\ {\isasymexists}i{\isachardot}\ c\isactrlisub i\ {\isasymsubseteq}\ d\isactrlisub j}.  The empty intersection

    67   \isa{{\isacharbraceleft}{\isacharbraceright}} refers to the universal sort, which is the largest

    68   element wrt.\ the sort order.  The intersections of all (finitely

    69   many) classes declared in the current theory are the minimal

    70   elements wrt.\ the sort order.

    71

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

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

    74   \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ s{\isacharparenright}} which is usually printed as \isa{{\isasymalpha}\isactrlisub s}.

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

    76   sort constraint, e.g.\ \isa{{\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ s{\isacharparenright}} which is usually

    77   printed as \isa{{\isacharquery}{\isasymalpha}\isactrlisub s}.

    78

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

    80   of type variables, including the sort constraint.  The core logic

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

    82   different, although some outer layers of the system make it hard to

    83   produce anything like this.

    84

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

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

    87   written postfix as \isa{{\isacharparenleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub k{\isacharparenright}{\isasymkappa}}.  For

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

    89   instead of \isa{{\isacharparenleft}{\isacharparenright}prop}.  For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the parentheses

    90   are omitted, e.g.\ \isa{{\isasymalpha}\ list} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharparenright}list}.

    91   Further notation is provided for specific constructors, notably the

    92   right-associative infix \isa{{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharcomma}\ {\isasymbeta}{\isacharparenright}fun}.

    93

    94   A \emph{type} is defined inductively over type variables and type

    95   constructors as follows: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}{\isasymkappa}}.

    96

    97   A \emph{type abbreviation} is a syntactic definition \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}\ {\isacharequal}\ {\isasymtau}} of an arbitrary type expression \isa{{\isasymtau}} over

    98   variables \isa{\isactrlvec {\isasymalpha}}.  Type abbreviations appear as type

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

   100   logical core.

   101

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

   103   constructor wrt.\ the algebra of sorts: \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}s} means that \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub k{\isacharparenright}{\isasymkappa}} is

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

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

   106   completed, i.e.\ \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c} entails \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}} for any \isa{c{\isacharprime}\ {\isasymsupseteq}\ c}.

   107

   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{{\isasymkappa}}, and classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, and arities \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} and \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} holds \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} component-wise.

   111

   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{{\isasymkappa}} and sort \isa{s} there is a most general

   115   vector of argument sorts \isa{{\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}} such

   116   that a type scheme \isa{{\isacharparenleft}{\isasymalpha}\isactrlbsub s\isactrlisub {\isadigit{1}}\isactrlesub {\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlbsub s\isactrlisub k\isactrlesub {\isacharparenright}{\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   \indexmltype{class}\verb|type class| \\

   132   \indexmltype{sort}\verb|type sort| \\

   133   \indexmltype{arity}\verb|type arity| \\

   134   \indexmltype{typ}\verb|type typ| \\

   135   \indexml{map\_atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\

   136   \indexml{fold\_atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\

   137   \end{mldecls}

   138   \begin{mldecls}

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

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

   141   \indexml{Sign.add\_types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\

   142   \indexml{Sign.add\_tyabbrs\_i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%

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

   144   \indexml{Sign.primitive\_class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\

   145   \indexml{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\

   146   \indexml{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\

   147   \end{mldecls}

   148

   149   \begin{description}

   150

   151   \item \verb|class| represents type classes; this is an alias for

   152   \verb|string|.

   153

   154   \item \verb|sort| represents sorts; this is an alias for

   155   \verb|class list|.

   156

   157   \item \verb|arity| represents type arities; this is an alias for

   158   triples of the form \isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} for \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s} described above.

   159

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

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

   162

   163   \item \verb|map_atyps|~\isa{f\ {\isasymtau}} applies the mapping \isa{f}

   164   to all atomic types (\verb|TFree|, \verb|TVar|) occurring in \isa{{\isasymtau}}.

   165

   166   \item \verb|fold_atyps|~\isa{f\ {\isasymtau}} iterates the operation \isa{f} over all occurrences of atomic types (\verb|TFree|, \verb|TVar|)

   167   in \isa{{\isasymtau}}; the type structure is traversed from left to right.

   168

   169   \item \verb|Sign.subsort|~\isa{thy\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ s\isactrlisub {\isadigit{2}}{\isacharparenright}}

   170   tests the subsort relation \isa{s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlisub {\isadigit{2}}}.

   171

   172   \item \verb|Sign.of_sort|~\isa{thy\ {\isacharparenleft}{\isasymtau}{\isacharcomma}\ s{\isacharparenright}} tests whether type

   173   \isa{{\isasymtau}} is of sort \isa{s}.

   174

   175   \item \verb|Sign.add_types|~\isa{{\isacharbrackleft}{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ k{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a new

   176   type constructors \isa{{\isasymkappa}} with \isa{k} arguments and

   177   optional mixfix syntax.

   178

   179   \item \verb|Sign.add_tyabbrs_i|~\isa{{\isacharbrackleft}{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec {\isasymalpha}{\isacharcomma}\ {\isasymtau}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}}

   180   defines a new type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}\ {\isacharequal}\ {\isasymtau}} with

   181   optional mixfix syntax.

   182

   183   \item \verb|Sign.primitive_class|~\isa{{\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub n{\isacharbrackright}{\isacharparenright}} declares a new class \isa{c}, together with class

   184   relations \isa{c\ {\isasymsubseteq}\ c\isactrlisub i}, for \isa{i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n}.

   185

   186   \item \verb|Sign.primitive_classrel|~\isa{{\isacharparenleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ c\isactrlisub {\isadigit{2}}{\isacharparenright}} declares the class relation \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}.

   187

   188   \item \verb|Sign.primitive_arity|~\isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} declares

   189   the arity \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s}.

   190

   191   \end{description}%

   192 \end{isamarkuptext}%

   193 \isamarkuptrue%

   194 %

   195 \endisatagmlref

   196 {\isafoldmlref}%

   197 %

   198 \isadelimmlref

   199 %

   200 \endisadelimmlref

   201 %

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

   203 }

   204 \isamarkuptrue%

   205 %

   206 \begin{isamarkuptext}%

   207 \glossary{Term}{FIXME}

   208

   209   The language of terms is that of simply-typed \isa{{\isasymlambda}}-calculus

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

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

   212   by the corresponding binders.  In contrast, free variables and

   213   constants are have an explicit name and type in each occurrence.

   214

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

   216   which accounts for the number of intermediate binders between the

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

   218   example, the de-Bruijn term \isa{{\isasymlambda}\isactrlbsub nat\isactrlesub {\isachardot}\ {\isasymlambda}\isactrlbsub nat\isactrlesub {\isachardot}\ {\isadigit{1}}\ {\isacharplus}\ {\isadigit{0}}} would

   219   correspond to \isa{{\isasymlambda}x\isactrlbsub nat\isactrlesub {\isachardot}\ {\isasymlambda}y\isactrlbsub nat\isactrlesub {\isachardot}\ x\ {\isacharplus}\ y} in a named

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

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

   222   the nesting of abstractions.

   223

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

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

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

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

   228   without any loose variables.

   229

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

   231   \isa{{\isacharparenleft}x{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed \isa{x\isactrlisub {\isasymtau}}.  A

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

   233   e.g.\ \isa{{\isacharparenleft}{\isacharparenleft}x{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed as \isa{{\isacharquery}x\isactrlisub {\isasymtau}}.

   234

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

   236   e.g.\ \isa{{\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed as \isa{c\isactrlisub {\isasymtau}}.  Constants are declared in the context as polymorphic

   237   families \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}, meaning that all substitution instances

   238   \isa{c\isactrlisub {\isasymtau}} for \isa{{\isasymtau}\ {\isacharequal}\ {\isasymsigma}{\isasymvartheta}} are valid.

   239

   240   The vector of \emph{type arguments} of constant \isa{c\isactrlisub {\isasymtau}}

   241   wrt.\ the declaration \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} is defined as the codomain of

   242   the matcher \isa{{\isasymvartheta}\ {\isacharequal}\ {\isacharbraceleft}{\isacharquery}{\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymmapsto}\ {\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isacharquery}{\isasymalpha}\isactrlisub n\ {\isasymmapsto}\ {\isasymtau}\isactrlisub n{\isacharbraceright}} presented in canonical order \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}}.  Within a given theory context,

   243   there is a one-to-one correspondence between any constant \isa{c\isactrlisub {\isasymtau}} and the application \isa{c{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}} of its type arguments.  For example, with \isa{plus\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}}, the instance \isa{plus\isactrlbsub nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\isactrlesub } corresponds to \isa{plus{\isacharparenleft}nat{\isacharparenright}}.

   244

   245   Constant declarations \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} may contain sort constraints

   246   for type variables in \isa{{\isasymsigma}}.  These are observed by

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

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

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

   250   due to violation of type class restrictions.

   251

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

   253   \emph{term} is defined inductively over atomic terms, with

   254   abstraction and application as follows: \isa{t\ {\isacharequal}\ b\ {\isacharbar}\ x\isactrlisub {\isasymtau}\ {\isacharbar}\ {\isacharquery}x\isactrlisub {\isasymtau}\ {\isacharbar}\ c\isactrlisub {\isasymtau}\ {\isacharbar}\ {\isasymlambda}\isactrlisub {\isasymtau}{\isachardot}\ t\ {\isacharbar}\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}}.

   255   Parsing and printing takes care of converting between an external

   256   representation with named bound variables.  Subsequently, we shall

   257   use the latter notation instead of internal de-Bruijn

   258   representation.

   259

   260   The inductive relation \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} assigns a (unique) type to a

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

   262   applicatins:

   263   $  264 \infer{\isa{a\isactrlisub {\isasymtau}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}}{}   265 \qquad   266 \infer{\isa{{\isacharparenleft}{\isasymlambda}x\isactrlsub {\isasymtau}{\isachardot}\ t{\isacharparenright}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymsigma}}}{\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}}   267 \qquad   268 \infer{\isa{t\ u\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}}{\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymsigma}} & \isa{u\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}}   269$

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

   271

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

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

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

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

   276   variables, and declarations for polymorphic constants.

   277

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

   279   component.  This means that different variables \isa{x\isactrlbsub {\isasymtau}\isactrlisub {\isadigit{1}}\isactrlesub } and \isa{x\isactrlbsub {\isasymtau}\isactrlisub {\isadigit{2}}\isactrlesub } may become the same after type

   280   instantiation.  Some outer layers of the system make it hard to

   281   produce variables of the same name, but different types.  In

   282   contrast, mixed instances of polymorphic constants occur frequently.

   283

   284   \medskip The \emph{hidden polymorphism} of a term \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}

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

   286   \isa{{\isasymsigma}}.  This means that the term implicitly depends on type

   287   arguments that are not accounted in the result type, i.e.\ there are

   288   different type instances \isa{t{\isasymvartheta}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} and \isa{t{\isasymvartheta}{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with the same type.  This slightly

   289   pathological situation notoriously demands additional care.

   290

   291   \medskip A \emph{term abbreviation} is a syntactic definition \isa{c\isactrlisub {\isasymsigma}\ {\isasymequiv}\ t} of a closed term \isa{t} of type \isa{{\isasymsigma}},

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

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

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

   295   \isa{t\ {\isasymrightarrow}\ c\isactrlisub {\isasymsigma}} as rules for higher-order rewriting.

   296

   297   \medskip Canonical operations on \isa{{\isasymlambda}}-terms include \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion: \isa{{\isasymalpha}}-conversion refers to capture-free

   298   renaming of bound variables; \isa{{\isasymbeta}}-conversion contracts an

   299   abstraction applied to an argument term, substituting the argument

   300   in the body: \isa{{\isacharparenleft}{\isasymlambda}x{\isachardot}\ b{\isacharparenright}a} becomes \isa{b{\isacharbrackleft}a{\isacharslash}x{\isacharbrackright}}; \isa{{\isasymeta}}-conversion contracts vacuous application-abstraction: \isa{{\isasymlambda}x{\isachardot}\ f\ x} becomes \isa{f}, provided that the bound variable

   301   does not occur in \isa{f}.

   302

   303   Terms are normally treated modulo \isa{{\isasymalpha}}-conversion, which is

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

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

   306   mostly for parsing and printing.  Full \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion is

   307   commonplace in various standard operations (\secref{sec:rules}) that

   308   are based on higher-order unification and matching.%

   309 \end{isamarkuptext}%

   310 \isamarkuptrue%

   311 %

   312 \isadelimmlref

   313 %

   314 \endisadelimmlref

   315 %

   316 \isatagmlref

   317 %

   318 \begin{isamarkuptext}%

   319 \begin{mldecls}

   320   \indexmltype{term}\verb|type term| \\

   321   \indexml{op aconv}\verb|op aconv: term * term -> bool| \\

   322   \indexml{map\_types}\verb|map_types: (typ -> typ) -> term -> term| \\

   323   \indexml{fold\_types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\

   324   \indexml{map\_aterms}\verb|map_aterms: (term -> term) -> term -> term| \\

   325   \indexml{fold\_aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\

   326   \end{mldecls}

   327   \begin{mldecls}

   328   \indexml{fastype\_of}\verb|fastype_of: term -> typ| \\

   329   \indexml{lambda}\verb|lambda: term -> term -> term| \\

   330   \indexml{betapply}\verb|betapply: term * term -> term| \\

   331   \indexml{Sign.declare\_const}\verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix ->|\isasep\isanewline%

   332 \verb|  theory -> term * theory| \\

   333   \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Markup.property list -> bstring * term ->|\isasep\isanewline%

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

   335   \indexml{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\

   336   \indexml{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\

   337   \end{mldecls}

   338

   339   \begin{description}

   340

   341   \item \verb|term| represents de-Bruijn terms, with comments in

   342   abstractions, and explicitly named free variables and constants;

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

   344

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

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

   347   for operations related to parsing or printing!

   348

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

   350

   351   \item \verb|fold_types|~\isa{f\ t} iterates the operation \isa{f} over all occurrences of types in \isa{t}; the term

   352   structure is traversed from left to right.

   353

   354   \item \verb|map_aterms|~\isa{f\ t} applies the mapping \isa{f}

   355   to all atomic terms (\verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|) occurring in \isa{t}.

   356

   357   \item \verb|fold_aterms|~\isa{f\ t} iterates the operation \isa{f} over all occurrences of atomic terms (\verb|Bound|, \verb|Free|,

   358   \verb|Var|, \verb|Const|) in \isa{t}; the term structure is

   359   traversed from left to right.

   360

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

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

   363   omission of any sanity checks.

   364

   365   \item \verb|lambda|~\isa{a\ b} produces an abstraction \isa{{\isasymlambda}a{\isachardot}\ b}, where occurrences of the atomic term \isa{a} in the

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

   367

   368   \item \verb|betapply|~\isa{{\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}} produces an application \isa{t\ u}, with topmost \isa{{\isasymbeta}}-conversion if \isa{t} is an

   369   abstraction.

   370

   371   \item \verb|Sign.declare_const|~\isa{properties\ {\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}}

   372   declares a new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix

   373   syntax.

   374

   375   \item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ properties\ {\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}}

   376   introduces a new term abbreviation \isa{c\ {\isasymequiv}\ t}.

   377

   378   \item \verb|Sign.const_typargs|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} and \verb|Sign.const_instance|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharbrackright}{\isacharparenright}}

   379   convert between two representations of polymorphic constants: full

   380   type instance vs.\ compact type arguments form.

   381

   382   \end{description}%

   383 \end{isamarkuptext}%

   384 \isamarkuptrue%

   385 %

   386 \endisatagmlref

   387 {\isafoldmlref}%

   388 %

   389 \isadelimmlref

   390 %

   391 \endisadelimmlref

   392 %

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

   394 }

   395 \isamarkuptrue%

   396 %

   397 \begin{isamarkuptext}%

   398 \glossary{Proposition}{FIXME A \seeglossary{term} of

   399   \seeglossary{type} \isa{prop}.  Internally, there is nothing

   400   special about propositions apart from their type, but the concrete

   401   syntax enforces a clear distinction.  Propositions are structured

   402   via implication \isa{A\ {\isasymLongrightarrow}\ B} or universal quantification \isa{{\isasymAnd}x{\isachardot}\ B\ x} --- anything else is considered atomic.  The canonical

   403   form for propositions is that of a \seeglossary{Hereditary Harrop

   404   Formula}. FIXME}

   405

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

   407   proof context, formally \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}; both contexts are

   408   rarely spelled out explicitly.  Theorems are usually normalized

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

   410

   411   \glossary{Fact}{Sometimes used interchangeably for

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

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

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

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

   416

   417   \glossary{Schematic variable}{FIXME}

   418

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

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

   421   proof text. FIXME}

   422

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

   424   variable}. FIXME}

   425

   426   \glossary{Bound variable}{FIXME}

   427

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

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

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

   431   different variables is their binding scope. FIXME}

   432

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

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

   435   hypotheses and the background theory).  Primitive inferences include

   436   plain natural deduction rules for the primary connectives \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} of the framework.  There is also a builtin

   437   notion of equality/equivalence \isa{{\isasymequiv}}.%

   438 \end{isamarkuptext}%

   439 \isamarkuptrue%

   440 %

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

   442 }

   443 \isamarkuptrue%

   444 %

   445 \begin{isamarkuptext}%

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

   447   primitive connectives \isa{{\isasymAnd}}, \isa{{\isasymLongrightarrow}}, and \isa{{\isasymequiv}} of

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

   449   derivability judgment \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} is

   450   defined inductively by the primitive inferences given in

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

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

   453   builtin equality is conceptually axiomatized as shown in

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

   455   directly with derived inferences.

   456

   457   \begin{figure}[htb]

   458   \begin{center}

   459   \begin{tabular}{ll}

   460   \isa{all\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymalpha}\ {\isasymRightarrow}\ prop{\isacharparenright}\ {\isasymRightarrow}\ prop} & universal quantification (binder \isa{{\isasymAnd}}) \\

   461   \isa{{\isasymLongrightarrow}\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & implication (right associative infix) \\

   462   \isa{{\isasymequiv}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ prop} & equality relation (infix) \\

   463   \end{tabular}

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

   465   \end{center}

   466   \end{figure}

   467

   468   \begin{figure}[htb]

   469   \begin{center}

   470   $  471 \infer[\isa{{\isacharparenleft}axiom{\isacharparenright}}]{\isa{{\isasymturnstile}\ A}}{\isa{A\ {\isasymin}\ {\isasymTheta}}}   472 \qquad   473 \infer[\isa{{\isacharparenleft}assume{\isacharparenright}}]{\isa{A\ {\isasymturnstile}\ A}}{}   474$

   475   $  476 \infer[\isa{{\isacharparenleft}{\isasymAnd}{\isacharunderscore}intro{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ b{\isacharbrackleft}x{\isacharbrackright}} & \isa{x\ {\isasymnotin}\ {\isasymGamma}}}   477 \qquad   478 \infer[\isa{{\isacharparenleft}{\isasymAnd}{\isacharunderscore}elim{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ b{\isacharbrackleft}a{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}}}   479$

   480   $  481 \infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isacharunderscore}intro{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}   482 \qquad   483 \infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isacharunderscore}elim{\isacharparenright}}]{\isa{{\isasymGamma}\isactrlsub {\isadigit{1}}\ {\isasymunion}\ {\isasymGamma}\isactrlsub {\isadigit{2}}\ {\isasymturnstile}\ B}}{\isa{{\isasymGamma}\isactrlsub {\isadigit{1}}\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B} & \isa{{\isasymGamma}\isactrlsub {\isadigit{2}}\ {\isasymturnstile}\ A}}   484$

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

   486   \end{center}

   487   \end{figure}

   488

   489   \begin{figure}[htb]

   490   \begin{center}

   491   \begin{tabular}{ll}

   492   \isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ a\ {\isasymequiv}\ b{\isacharbrackleft}a{\isacharbrackright}} & \isa{{\isasymbeta}}-conversion \\

   493   \isa{{\isasymturnstile}\ x\ {\isasymequiv}\ x} & reflexivity \\

   494   \isa{{\isasymturnstile}\ x\ {\isasymequiv}\ y\ {\isasymLongrightarrow}\ P\ x\ {\isasymLongrightarrow}\ P\ y} & substitution \\

   495   \isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ f\ x\ {\isasymequiv}\ g\ x{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isasymequiv}\ g} & extensionality \\

   496   \isa{{\isasymturnstile}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymequiv}\ B} & logical equivalence \\

   497   \end{tabular}

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

   499   \end{center}

   500   \end{figure}

   501

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

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

   504   propositions.  The system provides a runtime option to record

   505   explicit proof terms for primitive inferences.  Thus all three

   506   levels of \isa{{\isasymlambda}}-calculus become explicit: \isa{{\isasymRightarrow}} for

   507   terms, and \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} for proofs (cf.\

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

   509

   510   Observe that locally fixed parameters (as in \isa{{\isasymAnd}{\isacharunderscore}intro}) need

   511   not be recorded in the hypotheses, because the simple syntactic

   512   types of Pure are always inhabitable.  Assumptions'' \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} for type-membership are only present as long as some \isa{x\isactrlisub {\isasymtau}} occurs in the statement body.\footnote{This is the key

   513   difference to \isa{{\isasymlambda}HOL}'' in the PTS framework

   514   \cite{Barendregt-Geuvers:2001}, where hypotheses \isa{x\ {\isacharcolon}\ A} are

   515   treated uniformly for propositions and types.}

   516

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

   518   forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymvartheta}} holds for any substitution instance of an axiom

   519   \isa{{\isasymturnstile}\ A}.  By pushing substitutions through derivations

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

   521

   522   \begin{figure}[htb]

   523   \begin{center}

   524   $  525 \infer{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}{\isasymalpha}{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} & \isa{{\isasymalpha}\ {\isasymnotin}\ {\isasymGamma}}}   526 \quad   527 \infer[\quad\isa{{\isacharparenleft}generalize{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}x{\isacharbrackright}} & \isa{x\ {\isasymnotin}\ {\isasymGamma}}}   528$

   529   $  530 \infer{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isasymtau}{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}{\isasymalpha}{\isacharbrackright}}}   531 \quad   532 \infer[\quad\isa{{\isacharparenleft}instantiate{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}t{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}}   533$

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

   535   \end{center}

   536   \end{figure}

   537

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

   539   side-condition, because \isa{{\isasymGamma}} may never contain schematic

   540   variables.

   541

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

   543   but this would disrupt the monotonicity of reasoning: deriving

   544   \isa{{\isasymGamma}{\isasymvartheta}\ {\isasymturnstile}\ B{\isasymvartheta}} from \isa{{\isasymGamma}\ {\isasymturnstile}\ B} is

   545   correct, but \isa{{\isasymGamma}{\isasymvartheta}\ {\isasymsupseteq}\ {\isasymGamma}} does not necessarily hold:

   546   the result belongs to a different proof context.

   547

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

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

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

   551   The system always records oracle invocations within derivations of

   552   theorems.  Tracing plain axioms (and named theorems) is optional.

   553

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

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

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

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

   558

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

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

   561   Definitions of functions may be presented as \isa{c\ \isactrlvec x\ {\isasymequiv}\ t} instead of the puristic \isa{c\ {\isasymequiv}\ {\isasymlambda}\isactrlvec x{\isachardot}\ t}.

   562

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

   564   for the same constant, with zero or one equations \isa{c{\isacharparenleft}{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}{\isacharparenright}\ {\isasymequiv}\ t} for each type constructor \isa{{\isasymkappa}} (for

   565   distinct variables \isa{\isactrlvec {\isasymalpha}}).  The RHS may mention

   566   previously defined constants as above, or arbitrary constants \isa{d{\isacharparenleft}{\isasymalpha}\isactrlisub i{\isacharparenright}} for some \isa{{\isasymalpha}\isactrlisub i} projected from \isa{\isactrlvec {\isasymalpha}}.  Thus overloaded definitions essentially work by

   567   primitive recursion over the syntactic structure of a single type

   568   argument.%

   569 \end{isamarkuptext}%

   570 \isamarkuptrue%

   571 %

   572 \isadelimmlref

   573 %

   574 \endisadelimmlref

   575 %

   576 \isatagmlref

   577 %

   578 \begin{isamarkuptext}%

   579 \begin{mldecls}

   580   \indexmltype{ctyp}\verb|type ctyp| \\

   581   \indexmltype{cterm}\verb|type cterm| \\

   582   \indexml{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\

   583   \indexml{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\

   584   \end{mldecls}

   585   \begin{mldecls}

   586   \indexmltype{thm}\verb|type thm| \\

   587   \indexml{proofs}\verb|proofs: int ref| \\

   588   \indexml{Thm.assume}\verb|Thm.assume: cterm -> thm| \\

   589   \indexml{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\

   590   \indexml{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\

   591   \indexml{Thm.implies\_intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\

   592   \indexml{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\

   593   \indexml{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\

   594   \indexml{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\

   595   \indexml{Thm.get\_axiom\_i}\verb|Thm.get_axiom_i: theory -> string -> thm| \\

   596   \indexml{Thm.invoke\_oracle\_i}\verb|Thm.invoke_oracle_i: theory -> string -> theory * Object.T -> thm| \\

   597   \end{mldecls}

   598   \begin{mldecls}

   599   \indexml{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (string * term) list -> theory -> theory| \\

   600   \indexml{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\

   601   \indexml{Theory.add\_oracle}\verb|Theory.add_oracle: string * (theory * Object.T -> term) -> theory -> theory| \\

   602   \indexml{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory| \\

   603   \end{mldecls}

   604

   605   \begin{description}

   606

   607   \item \verb|ctyp| and \verb|cterm| represent certified types

   608   and terms, respectively.  These are abstract datatypes that

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

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

   611   constructors, constants etc. in the theory.

   612

   613   \item \verb|ctyp_of|~\isa{thy\ {\isasymtau}} and \verb|cterm_of|~\isa{thy\ t} explicitly checks types and terms, respectively.  This also

   614   involves some basic normalizations, such expansion of type and term

   615   abbreviations from the theory context.

   616

   617   Re-certification is relatively slow and should be avoided in tight

   618   reasoning loops.  There are separate operations to decompose

   619   certified entities (including actual theorems).

   620

   621   \item \verb|thm| represents proven propositions.  This is an

   622   abstract datatype that guarantees that its values have been

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

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

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

   626

   627   \item \verb|proofs| determines the detail of proof recording within

   628   \verb|thm| values: \verb|0| records only oracles, \verb|1| records

   629   oracles, axioms and named theorems, \verb|2| records full proof

   630   terms.

   631

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

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

   634

   635   \item \verb|Thm.generalize|~\isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharcomma}\ \isactrlvec x{\isacharparenright}}

   636   corresponds to the \isa{generalize} rules of

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

   638   variables are generalized simultaneously, specified by the given

   639   basic names.

   640

   641   \item \verb|Thm.instantiate|~\isa{{\isacharparenleft}\isactrlvec {\isasymalpha}\isactrlisub s{\isacharcomma}\ \isactrlvec x\isactrlisub {\isasymtau}{\isacharparenright}} corresponds to the \isa{instantiate} rules

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

   643   term variables.  Note that the types in \isa{\isactrlvec x\isactrlisub {\isasymtau}}

   644   refer to the instantiated versions.

   645

   646   \item \verb|Thm.get_axiom_i|~\isa{thy\ name} retrieves a named

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

   648

   649   \item \verb|Thm.invoke_oracle_i|~\isa{thy\ name\ arg} invokes a

   650   named oracle function, cf.\ \isa{axiom} in

   651   \figref{fig:prim-rules}.

   652

   653   \item \verb|Theory.add_axioms_i|~\isa{{\isacharbrackleft}{\isacharparenleft}name{\isacharcomma}\ A{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares

   654   arbitrary propositions as axioms.

   655

   656   \item \verb|Theory.add_oracle|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}} declares an oracle

   657   function for generating arbitrary axioms on the fly.

   658

   659   \item \verb|Theory.add_deps|~\isa{name\ c\isactrlisub {\isasymtau}\ \isactrlvec d\isactrlisub {\isasymsigma}} declares dependencies of a named specification

   660   for constant \isa{c\isactrlisub {\isasymtau}}, relative to existing

   661   specifications for constants \isa{\isactrlvec d\isactrlisub {\isasymsigma}}.

   662

   663   \item \verb|Theory.add_defs_i|~\isa{unchecked\ overloaded\ {\isacharbrackleft}{\isacharparenleft}name{\isacharcomma}\ c\ \isactrlvec x\ {\isasymequiv}\ t{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} states a definitional axiom for an existing

   664   constant \isa{c}.  Dependencies are recorded (cf.\ \verb|Theory.add_deps|), unless the \isa{unchecked} option is set.

   665

   666   \end{description}%

   667 \end{isamarkuptext}%

   668 \isamarkuptrue%

   669 %

   670 \endisatagmlref

   671 {\isafoldmlref}%

   672 %

   673 \isadelimmlref

   674 %

   675 \endisadelimmlref

   676 %

   677 \isamarkupsubsection{Auxiliary definitions%

   678 }

   679 \isamarkuptrue%

   680 %

   681 \begin{isamarkuptext}%

   682 Theory \isa{Pure} provides a few auxiliary definitions, see

   683   \figref{fig:pure-aux}.  These special constants are normally not

   684   exposed to the user, but appear in internal encodings.

   685

   686   \begin{figure}[htb]

   687   \begin{center}

   688   \begin{tabular}{ll}

   689   \isa{conjunction\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & (infix \isa{{\isacharampersand}}) \\

   690   \isa{{\isasymturnstile}\ A\ {\isacharampersand}\ B\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}C{\isachardot}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isacharparenright}} \$1ex]   691 \isa{prop\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop} & (prefix \isa{{\isacharhash}}, suppressed) \\   692 \isa{{\isacharhash}A\ {\isasymequiv}\ A} \\[1ex]   693 \isa{term\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ prop} & (prefix \isa{TERM}) \\   694 \isa{term\ x\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}A{\isachardot}\ A\ {\isasymLongrightarrow}\ A{\isacharparenright}} \\[1ex]   695 \isa{TYPE\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ itself} & (prefix \isa{TYPE}) \\   696 \isa{{\isacharparenleft}unspecified{\isacharparenright}} \\   697 \end{tabular}   698 \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}   699 \end{center}   700 \end{figure}   701   702 Derived conjunction rules include introduction \isa{A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isacharampersand}\ B}, and destructions \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ A} and \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ B}.   703 Conjunction allows to treat simultaneous assumptions and conclusions   704 uniformly. For example, multiple claims are intermediately   705 represented as explicit conjunction, but this is refined into   706 separate sub-goals before the user continues the proof; the final   707 result is projected into a list of theorems (cf.\   708 \secref{sec:tactical-goals}).   709   710 The \isa{prop} marker (\isa{{\isacharhash}}) makes arbitrarily complex   711 propositions appear as atomic, without changing the meaning: \isa{{\isasymGamma}\ {\isasymturnstile}\ A} and \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isacharhash}A} are interchangeable. See   712 \secref{sec:tactical-goals} for specific operations.   713   714 The \isa{term} marker turns any well-typed term into a derivable   715 proposition: \isa{{\isasymturnstile}\ TERM\ t} holds unconditionally. Although   716 this is logically vacuous, it allows to treat terms and proofs   717 uniformly, similar to a type-theoretic framework.   718   719 The \isa{TYPE} constructor is the canonical representative of   720 the unspecified type \isa{{\isasymalpha}\ itself}; it essentially injects the   721 language of types into that of terms. There is specific notation   722 \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} for \isa{TYPE\isactrlbsub {\isasymtau}\ itself\isactrlesub }.   723 Although being devoid of any particular meaning, the \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} accounts for the type \isa{{\isasymtau}} within the term   724 language. In particular, \isa{TYPE{\isacharparenleft}{\isasymalpha}{\isacharparenright}} may be used as formal   725 argument in primitive definitions, in order to circumvent hidden   726 polymorphism (cf.\ \secref{sec:terms}). For example, \isa{c\ TYPE{\isacharparenleft}{\isasymalpha}{\isacharparenright}\ {\isasymequiv}\ A{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} defines \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ itself\ {\isasymRightarrow}\ prop} in terms of   727 a proposition \isa{A} that depends on an additional type   728 argument, which is essentially a predicate on types.%   729 \end{isamarkuptext}%   730 \isamarkuptrue%   731 %   732 \isadelimmlref   733 %   734 \endisadelimmlref   735 %   736 \isatagmlref   737 %   738 \begin{isamarkuptext}%   739 \begin{mldecls}   740 \indexml{Conjunction.intr}\verb|Conjunction.intr: thm -> thm -> thm| \\   741 \indexml{Conjunction.elim}\verb|Conjunction.elim: thm -> thm * thm| \\   742 \indexml{Drule.mk\_term}\verb|Drule.mk_term: cterm -> thm| \\   743 \indexml{Drule.dest\_term}\verb|Drule.dest_term: thm -> cterm| \\   744 \indexml{Logic.mk\_type}\verb|Logic.mk_type: typ -> term| \\   745 \indexml{Logic.dest\_type}\verb|Logic.dest_type: term -> typ| \\   746 \end{mldecls}   747   748 \begin{description}   749   750 \item \verb|Conjunction.intr| derives \isa{A\ {\isacharampersand}\ B} from \isa{A} and \isa{B}.   751   752 \item \verb|Conjunction.elim| derives \isa{A} and \isa{B}   753 from \isa{A\ {\isacharampersand}\ B}.   754   755 \item \verb|Drule.mk_term| derives \isa{TERM\ t}.   756   757 \item \verb|Drule.dest_term| recovers term \isa{t} from \isa{TERM\ t}.   758   759 \item \verb|Logic.mk_type|~\isa{{\isasymtau}} produces the term \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}}.   760   761 \item \verb|Logic.dest_type|~\isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} recovers the type   762 \isa{{\isasymtau}}.   763   764 \end{description}%   765 \end{isamarkuptext}%   766 \isamarkuptrue%   767 %   768 \endisatagmlref   769 {\isafoldmlref}%   770 %   771 \isadelimmlref   772 %   773 \endisadelimmlref   774 %   775 \isamarkupsection{Rules \label{sec:rules}%   776 }   777 \isamarkuptrue%   778 %   779 \isadelimFIXME   780 %   781 \endisadelimFIXME   782 %   783 \isatagFIXME   784 %   785 \begin{isamarkuptext}%   786 FIXME   787   788 A \emph{rule} is any Pure theorem in HHF normal form; there is a   789 separate calculus for rule composition, which is modeled after   790 Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows   791 rules to be nested arbitrarily, similar to \cite{extensions91}.   792   793 Normally, all theorems accessible to the user are proper rules.   794 Low-level inferences are occasional required internally, but the   795 result should be always presented in canonical form. The higher   796 interfaces of Isabelle/Isar will always produce proper rules. It is   797 important to maintain this invariant in add-on applications!   798   799 There are two main principles of rule composition: \isa{resolution} (i.e.\ backchaining of rules) and \isa{by{\isacharminus}assumption} (i.e.\ closing a branch); both principles are   800 combined in the variants of \isa{elim{\isacharminus}resolution} and \isa{dest{\isacharminus}resolution}. Raw \isa{composition} is occasionally   801 useful as well, also it is strictly speaking outside of the proper   802 rule calculus.   803   804 Rules are treated modulo general higher-order unification, which is   805 unification modulo the equational theory of \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion   806 on \isa{{\isasymlambda}}-terms. Moreover, propositions are understood modulo   807 the (derived) equivalence \isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}}.   808   809 This means that any operations within the rule calculus may be   810 subject to spontaneous \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-HHF conversions. It is common   811 practice not to contract or expand unnecessarily. Some mechanisms   812 prefer an one form, others the opposite, so there is a potential   813 danger to produce some oscillation!   814   815 Only few operations really work \emph{modulo} HHF conversion, but   816 expect a normal form: quantifiers \isa{{\isasymAnd}} before implications   817 \isa{{\isasymLongrightarrow}} at each level of nesting.   818   819 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF   820 format is defined inductively as \isa{H\ {\isacharequal}\ {\isacharparenleft}{\isasymAnd}x\isactrlsup {\isacharasterisk}{\isachardot}\ H\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ A{\isacharparenright}}, for variables \isa{x} and atomic propositions \isa{A}.   821 Any proposition may be put into HHF form by normalizing with the rule   822 \isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}}. In Isabelle, the outermost   823 quantifier prefix is represented via \seeglossary{schematic   824 variables}, such that the top-level structure is merely that of a   825 \seeglossary{Horn Clause}}.   826   827 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}   828   829   830 \[   831 \infer[\isa{{\isacharparenleft}assumption{\isacharparenright}}]{\isa{C{\isasymvartheta}}}   832 {\isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ A\ \isactrlvec x{\isacharparenright}\ {\isasymLongrightarrow}\ C} & \isa{A{\isasymvartheta}\ {\isacharequal}\ H\isactrlsub i{\isasymvartheta}}~~\text{(for some~\isa{i})}}   833$

   834

   835

   836   $  837 \infer[\isa{{\isacharparenleft}compose{\isacharparenright}}]{\isa{\isactrlvec A{\isasymvartheta}\ {\isasymLongrightarrow}\ C{\isasymvartheta}}}   838 {\isa{\isactrlvec A\ {\isasymLongrightarrow}\ B} & \isa{B{\isacharprime}\ {\isasymLongrightarrow}\ C} & \isa{B{\isasymvartheta}\ {\isacharequal}\ B{\isacharprime}{\isasymvartheta}}}   839$

   840

   841

   842   $  843 \infer[\isa{{\isacharparenleft}{\isasymAnd}{\isacharunderscore}lift{\isacharparenright}}]{\isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec A\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ B\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}}}{\isa{\isactrlvec A\ {\isacharquery}\isactrlvec a\ {\isasymLongrightarrow}\ B\ {\isacharquery}\isactrlvec a}}   844$

   845   $  846 \infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isacharunderscore}lift{\isacharparenright}}]{\isa{{\isacharparenleft}\isactrlvec H\ {\isasymLongrightarrow}\ \isactrlvec A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}\isactrlvec H\ {\isasymLongrightarrow}\ B{\isacharparenright}}}{\isa{\isactrlvec A\ {\isasymLongrightarrow}\ B}}   847$

   848

   849   The \isa{resolve} scheme is now acquired from \isa{{\isasymAnd}{\isacharunderscore}lift},

   850   \isa{{\isasymLongrightarrow}{\isacharunderscore}lift}, and \isa{compose}.

   851

   852   $  853 \infer[\isa{{\isacharparenleft}resolution{\isacharparenright}}]   854 {\isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ \isactrlvec A\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}{\isasymvartheta}\ {\isasymLongrightarrow}\ C{\isasymvartheta}}}   855 {\begin{tabular}{l}   856 \isa{\isactrlvec A\ {\isacharquery}\isactrlvec a\ {\isasymLongrightarrow}\ B\ {\isacharquery}\isactrlvec a} \\   857 \isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ B{\isacharprime}\ \isactrlvec x{\isacharparenright}\ {\isasymLongrightarrow}\ C} \\   858 \isa{{\isacharparenleft}{\isasymlambda}\isactrlvec x{\isachardot}\ B\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}{\isasymvartheta}\ {\isacharequal}\ B{\isacharprime}{\isasymvartheta}} \\   859 \end{tabular}}   860$

   861

   862

   863   FIXME \isa{elim{\isacharunderscore}resolution}, \isa{dest{\isacharunderscore}resolution}%

   864 \end{isamarkuptext}%

   865 \isamarkuptrue%

   866 %

   867 \endisatagFIXME

   868 {\isafoldFIXME}%

   869 %

   870 \isadelimFIXME

   871 %

   872 \endisadelimFIXME

   873 %

   874 \isadelimtheory

   875 %

   876 \endisadelimtheory

   877 %

   878 \isatagtheory

   879 \isacommand{end}\isamarkupfalse%

   880 %

   881 \endisatagtheory

   882 {\isafoldtheory}%

   883 %

   884 \isadelimtheory

   885 %

   886 \endisadelimtheory

   887 \isanewline

   888 \end{isabellebody}%

   889 %%% Local Variables:

   890 %%% mode: latex

   891 %%% TeX-master: "root"

   892 %%% End: