doc-src/IsarImplementation/Thy/Logic.thy
 author wenzelm Mon Jun 06 19:08:46 2011 +0200 (2011-06-06) changeset 42934 287182c2f23a parent 42933 7860ffc5ec08 child 46253 3e427a12f0f3 permissions -rw-r--r--
moved incr_boundvars;
discontinued low-level term operations;
     1 theory Logic

     2 imports Base

     3 begin

     4

     5 chapter {* Primitive logic \label{ch:logic} *}

     6

     7 text {*

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

     9   which has been introduced as a Natural Deduction framework in

    10   \cite{paulson700}.  This is essentially the same logic as @{text

    11   "\<lambda>HOL"}'' in the more abstract setting of Pure Type Systems (PTS)

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

    13   differences in the specific treatment of simple types in

    14   Isabelle/Pure.

    15

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

    17   levels of @{text "\<lambda>"}-calculus with corresponding arrows, @{text

    18   "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text

    19   "\<And>"} for universal quantification (proofs depending on terms), and

    20   @{text "\<Longrightarrow>"} for implication (proofs depending on proofs).

    21

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

    23   constructors, constants, and axioms.  Theory declarations support

    24   schematic polymorphism, which is strictly speaking outside the

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

    26   context @{text "\<Theta>"} is separate from the proof context @{text "\<Gamma>"}

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

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

    29   of a locally fixed term parameter is also fixed!}

    30 *}

    31

    32

    33 section {* Types \label{sec:types} *}

    34

    35 text {*

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

    37   algebra; types are qualified by ordered type classes.

    38

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

    40   declared in the theory context.  The \emph{subclass relation} @{text

    41   "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic

    42   generating relation; the transitive closure is maintained

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

    44   transitive, and antisymmetric.

    45

    46   A \emph{sort} is a list of type classes written as @{text "s = {c\<^isub>1,

    47   \<dots>, c\<^isub>m}"}, it represents symbolic intersection.  Notationally, the

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

    49   class @{text "c"} may be read as a sort @{text "{c}"}.  The ordering

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

    51   intersections: @{text "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff @{text

    52   "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}.  The empty intersection @{text "{}"} refers to

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

    54   order.  Thus @{text "{}"} represents the full sort'', not the

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

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

    57

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

    59   (starting with a @{text "'"} character) and a sort constraint, e.g.\

    60   @{text "('a, s)"} which is usually printed as @{text "\<alpha>\<^isub>s"}.

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

    62   sort constraint, e.g.\ @{text "(('a, 0), s)"} which is usually

    63   printed as @{text "?\<alpha>\<^isub>s"}.

    64

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

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

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

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

    69   the core) rejects anything like that.

    70

    71   A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}-ary operator

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

    73   written postfix as @{text "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}.  For

    74   @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text "prop"}

    75   instead of @{text "()prop"}.  For @{text "k = 1"} the parentheses

    76   are omitted, e.g.\ @{text "\<alpha> list"} instead of @{text "(\<alpha>)list"}.

    77   Further notation is provided for specific constructors, notably the

    78   right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of @{text "(\<alpha>,

    79   \<beta>)fun"}.

    80

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

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

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

    84

    85   A \emph{type abbreviation} is a syntactic definition @{text

    86   "(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over

    87   variables @{text "\<^vec>\<alpha>"}.  Type abbreviations appear as type

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

    89   logical core.

    90

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

    92   constructor wrt.\ the algebra of sorts: @{text "\<kappa> :: (s\<^isub>1, \<dots>,

    93   s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)\<kappa>"} is

    94   of sort @{text "s"} if every argument type @{text "\<tau>\<^isub>i"} is

    95   of sort @{text "s\<^isub>i"}.  Arity declarations are implicitly

    96   completed, i.e.\ @{text "\<kappa> :: (\<^vec>s)c"} entails @{text "\<kappa> ::

    97   (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.

    98

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

   100   which means that type arities are consistent with the subclass

   101   relation: for any type constructor @{text "\<kappa>"}, and classes @{text

   102   "c\<^isub>1 \<subseteq> c\<^isub>2"}, and arities @{text "\<kappa> ::

   103   (\<^vec>s\<^isub>1)c\<^isub>1"} and @{text "\<kappa> ::

   104   (\<^vec>s\<^isub>2)c\<^isub>2"} holds @{text "\<^vec>s\<^isub>1 \<subseteq>

   105   \<^vec>s\<^isub>2"} component-wise.

   106

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

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

   109   constructor @{text "\<kappa>"} and sort @{text "s"} there is a most general

   110   vector of argument sorts @{text "(s\<^isub>1, \<dots>, s\<^isub>k)"} such

   111   that a type scheme @{text "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>,

   112   \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is of sort @{text "s"}.

   113   Consequently, type unification has most general solutions (modulo

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

   115   expected \cite{nipkow-prehofer}.

   116 *}

   117

   118 text %mlref {*

   119   \begin{mldecls}

   120   @{index_ML_type class: string} \\

   121   @{index_ML_type sort: "class list"} \\

   122   @{index_ML_type arity: "string * sort list * sort"} \\

   123   @{index_ML_type typ} \\

   124   @{index_ML Term.map_atyps: "(typ -> typ) -> typ -> typ"} \\

   125   @{index_ML Term.fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\

   126   \end{mldecls}

   127   \begin{mldecls}

   128   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\

   129   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\

   130   @{index_ML Sign.add_types: "Proof.context ->

   131   (binding * int * mixfix) list -> theory -> theory"} \\

   132   @{index_ML Sign.add_type_abbrev: "Proof.context ->

   133   binding * string list * typ -> theory -> theory"} \\

   134   @{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\

   135   @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\

   136   @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\

   137   \end{mldecls}

   138

   139   \begin{description}

   140

   141   \item Type @{ML_type class} represents type classes.

   142

   143   \item Type @{ML_type sort} represents sorts, i.e.\ finite

   144   intersections of classes.  The empty list @{ML "[]: sort"} refers to

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

   146

   147   \item Type @{ML_type arity} represents type arities.  A triple

   148   @{text "(\<kappa>, \<^vec>s, s) : arity"} represents @{text "\<kappa> ::

   149   (\<^vec>s)s"} as described above.

   150

   151   \item Type @{ML_type typ} represents types; this is a datatype with

   152   constructors @{ML TFree}, @{ML TVar}, @{ML Type}.

   153

   154   \item @{ML Term.map_atyps}~@{text "f \<tau>"} applies the mapping @{text

   155   "f"} to all atomic types (@{ML TFree}, @{ML TVar}) occurring in

   156   @{text "\<tau>"}.

   157

   158   \item @{ML Term.fold_atyps}~@{text "f \<tau>"} iterates the operation

   159   @{text "f"} over all occurrences of atomic types (@{ML TFree}, @{ML

   160   TVar}) in @{text "\<tau>"}; the type structure is traversed from left to

   161   right.

   162

   163   \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}

   164   tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.

   165

   166   \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether type

   167   @{text "\<tau>"} is of sort @{text "s"}.

   168

   169   \item @{ML Sign.add_types}~@{text "ctxt [(\<kappa>, k, mx), \<dots>]"} declares a

   170   new type constructors @{text "\<kappa>"} with @{text "k"} arguments and

   171   optional mixfix syntax.

   172

   173   \item @{ML Sign.add_type_abbrev}~@{text "ctxt (\<kappa>, \<^vec>\<alpha>, \<tau>)"}

   174   defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"}.

   175

   176   \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,

   177   c\<^isub>n])"} declares a new class @{text "c"}, together with class

   178   relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.

   179

   180   \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,

   181   c\<^isub>2)"} declares the class relation @{text "c\<^isub>1 \<subseteq>

   182   c\<^isub>2"}.

   183

   184   \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares

   185   the arity @{text "\<kappa> :: (\<^vec>s)s"}.

   186

   187   \end{description}

   188 *}

   189

   190 text %mlantiq {*

   191   \begin{matharray}{rcl}

   192   @{ML_antiquotation_def "class"} & : & @{text ML_antiquotation} \\

   193   @{ML_antiquotation_def "sort"} & : & @{text ML_antiquotation} \\

   194   @{ML_antiquotation_def "type_name"} & : & @{text ML_antiquotation} \\

   195   @{ML_antiquotation_def "type_abbrev"} & : & @{text ML_antiquotation} \\

   196   @{ML_antiquotation_def "nonterminal"} & : & @{text ML_antiquotation} \\

   197   @{ML_antiquotation_def "typ"} & : & @{text ML_antiquotation} \\

   198   \end{matharray}

   199

   200   @{rail "

   201   @@{ML_antiquotation class} nameref

   202   ;

   203   @@{ML_antiquotation sort} sort

   204   ;

   205   (@@{ML_antiquotation type_name} |

   206    @@{ML_antiquotation type_abbrev} |

   207    @@{ML_antiquotation nonterminal}) nameref

   208   ;

   209   @@{ML_antiquotation typ} type

   210   "}

   211

   212   \begin{description}

   213

   214   \item @{text "@{class c}"} inlines the internalized class @{text

   215   "c"} --- as @{ML_type string} literal.

   216

   217   \item @{text "@{sort s}"} inlines the internalized sort @{text "s"}

   218   --- as @{ML_type "string list"} literal.

   219

   220   \item @{text "@{type_name c}"} inlines the internalized type

   221   constructor @{text "c"} --- as @{ML_type string} literal.

   222

   223   \item @{text "@{type_abbrev c}"} inlines the internalized type

   224   abbreviation @{text "c"} --- as @{ML_type string} literal.

   225

   226   \item @{text "@{nonterminal c}"} inlines the internalized syntactic

   227   type~/ grammar nonterminal @{text "c"} --- as @{ML_type string}

   228   literal.

   229

   230   \item @{text "@{typ \<tau>}"} inlines the internalized type @{text "\<tau>"}

   231   --- as constructor term for datatype @{ML_type typ}.

   232

   233   \end{description}

   234 *}

   235

   236

   237 section {* Terms \label{sec:terms} *}

   238

   239 text {*

   240   The language of terms is that of simply-typed @{text "\<lambda>"}-calculus

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

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

   243   corresponding binders.  In contrast, free variables and constants

   244   have an explicit name and type in each occurrence.

   245

   246   \medskip A \emph{bound variable} is a natural number @{text "b"},

   247   which accounts for the number of intermediate binders between the

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

   249   example, the de-Bruijn term @{text "\<lambda>\<^bsub>bool\<^esub>. \<lambda>\<^bsub>bool\<^esub>. 1 \<and> 0"} would

   250   correspond to @{text "\<lambda>x\<^bsub>bool\<^esub>. \<lambda>y\<^bsub>bool\<^esub>. x \<and> y"} in a named

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

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

   253   the nesting of abstractions.

   254

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

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

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

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

   259   without any loose variables.

   260

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

   262   @{text "(x, \<tau>)"} which is usually printed @{text "x\<^isub>\<tau>"} here.  A

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

   264   e.g.\ @{text "((x, 0), \<tau>)"} which is likewise printed as @{text

   265   "?x\<^isub>\<tau>"}.

   266

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

   268   e.g.\ @{text "(c, \<tau>)"} which is usually printed as @{text "c\<^isub>\<tau>"}

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

   270   @{text "c :: \<sigma>"}, meaning that all substitution instances @{text

   271   "c\<^isub>\<tau>"} for @{text "\<tau> = \<sigma>\<vartheta>"} are valid.

   272

   273   The vector of \emph{type arguments} of constant @{text "c\<^isub>\<tau>"} wrt.\

   274   the declaration @{text "c :: \<sigma>"} is defined as the codomain of the

   275   matcher @{text "\<vartheta> = {?\<alpha>\<^isub>1 \<mapsto> \<tau>\<^isub>1, \<dots>, ?\<alpha>\<^isub>n \<mapsto> \<tau>\<^isub>n}"} presented in

   276   canonical order @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}, corresponding to the

   277   left-to-right occurrences of the @{text "\<alpha>\<^isub>i"} in @{text "\<sigma>"}.

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

   279   between any constant @{text "c\<^isub>\<tau>"} and the application @{text "c(\<tau>\<^isub>1,

   280   \<dots>, \<tau>\<^isub>n)"} of its type arguments.  For example, with @{text "plus :: \<alpha>

   281   \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"}, the instance @{text "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow> nat\<^esub>"} corresponds to

   282   @{text "plus(nat)"}.

   283

   284   Constant declarations @{text "c :: \<sigma>"} may contain sort constraints

   285   for type variables in @{text "\<sigma>"}.  These are observed by

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

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

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

   289   due to violation of type class restrictions.

   290

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

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

   293   terms, with abstraction and application as follows: @{text "t = b |

   294   x\<^isub>\<tau> | ?x\<^isub>\<tau> | c\<^isub>\<tau> | \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}.  Parsing and printing takes care of

   295   converting between an external representation with named bound

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

   297   of internal de-Bruijn representation.

   298

   299   The inductive relation @{text "t :: \<tau>"} assigns a (unique) type to a

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

   301   applicatins:

   302   $  303 \infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{}   304 \qquad   305 \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}}   306 \qquad   307 \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}}   308$

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

   310

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

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

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

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

   315   variables, and declarations for polymorphic constants.

   316

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

   318   component.  This means that different variables @{text

   319   "x\<^bsub>\<tau>\<^isub>1\<^esub>"} and @{text "x\<^bsub>\<tau>\<^isub>2\<^esub>"} may become the same after

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

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

   322   polymorphic constants occur routinely.

   323

   324   \medskip The \emph{hidden polymorphism} of a term @{text "t :: \<sigma>"}

   325   is the set of type variables occurring in @{text "t"}, but not in

   326   its type @{text "\<sigma>"}.  This means that the term implicitly depends

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

   328   there are different type instances @{text "t\<vartheta> :: \<sigma>"} and

   329   @{text "t\<vartheta>' :: \<sigma>"} with the same type.  This slightly

   330   pathological situation notoriously demands additional care.

   331

   332   \medskip A \emph{term abbreviation} is a syntactic definition @{text

   333   "c\<^isub>\<sigma> \<equiv> t"} of a closed term @{text "t"} of type @{text "\<sigma>"},

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

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

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

   337   @{text "t \<rightarrow> c\<^isub>\<sigma>"} as rules for higher-order rewriting.

   338

   339   \medskip Canonical operations on @{text "\<lambda>"}-terms include @{text

   340   "\<alpha>\<beta>\<eta>"}-conversion: @{text "\<alpha>"}-conversion refers to capture-free

   341   renaming of bound variables; @{text "\<beta>"}-conversion contracts an

   342   abstraction applied to an argument term, substituting the argument

   343   in the body: @{text "(\<lambda>x. b)a"} becomes @{text "b[a/x]"}; @{text

   344   "\<eta>"}-conversion contracts vacuous application-abstraction: @{text

   345   "\<lambda>x. f x"} becomes @{text "f"}, provided that the bound variable

   346   does not occur in @{text "f"}.

   347

   348   Terms are normally treated modulo @{text "\<alpha>"}-conversion, which is

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

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

   351   mostly for parsing and printing.  Full @{text "\<alpha>\<beta>\<eta>"}-conversion is

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

   353   that are based on higher-order unification and matching.

   354 *}

   355

   356 text %mlref {*

   357   \begin{mldecls}

   358   @{index_ML_type term} \\

   359   @{index_ML "op aconv": "term * term -> bool"} \\

   360   @{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\

   361   @{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\

   362   @{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\

   363   @{index_ML Term.fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\

   364   \end{mldecls}

   365   \begin{mldecls}

   366   @{index_ML fastype_of: "term -> typ"} \\

   367   @{index_ML lambda: "term -> term -> term"} \\

   368   @{index_ML betapply: "term * term -> term"} \\

   369   @{index_ML incr_boundvars: "int -> term -> term"} \\

   370   @{index_ML Sign.declare_const: "Proof.context ->

   371   (binding * typ) * mixfix -> theory -> term * theory"} \\

   372   @{index_ML Sign.add_abbrev: "string -> binding * term ->

   373   theory -> (term * term) * theory"} \\

   374   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\

   375   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\

   376   \end{mldecls}

   377

   378   \begin{description}

   379

   380   \item Type @{ML_type term} represents de-Bruijn terms, with comments

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

   382   this is a datatype with constructors @{ML Bound}, @{ML Free}, @{ML

   383   Var}, @{ML Const}, @{ML Abs}, @{ML "op \$"}.

   384

   385   \item @{text "t"}~@{ML_text aconv}~@{text "u"} checks @{text

   386   "\<alpha>"}-equivalence of two terms.  This is the basic equality relation

   387   on type @{ML_type term}; raw datatype equality should only be used

   388   for operations related to parsing or printing!

   389

   390   \item @{ML Term.map_types}~@{text "f t"} applies the mapping @{text

   391   "f"} to all types occurring in @{text "t"}.

   392

   393   \item @{ML Term.fold_types}~@{text "f t"} iterates the operation

   394   @{text "f"} over all occurrences of types in @{text "t"}; the term

   395   structure is traversed from left to right.

   396

   397   \item @{ML Term.map_aterms}~@{text "f t"} applies the mapping @{text

   398   "f"} to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML

   399   Const}) occurring in @{text "t"}.

   400

   401   \item @{ML Term.fold_aterms}~@{text "f t"} iterates the operation

   402   @{text "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML

   403   Free}, @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is

   404   traversed from left to right.

   405

   406   \item @{ML fastype_of}~@{text "t"} determines the type of a

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

   408   omission of any sanity checks.

   409

   410   \item @{ML lambda}~@{text "a b"} produces an abstraction @{text

   411   "\<lambda>a. b"}, where occurrences of the atomic term @{text "a"} in the

   412   body @{text "b"} are replaced by bound variables.

   413

   414   \item @{ML betapply}~@{text "(t, u)"} produces an application @{text

   415   "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an

   416   abstraction.

   417

   418   \item @{ML incr_boundvars}~@{text "j"} increments a term's dangling

   419   bound variables by the offset @{text "j"}.  This is required when

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

   421   number of abstractions.  Bound variables with a matching abstraction

   422   are unaffected.

   423

   424   \item @{ML Sign.declare_const}~@{text "ctxt ((c, \<sigma>), mx)"} declares

   425   a new constant @{text "c :: \<sigma>"} with optional mixfix syntax.

   426

   427   \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"}

   428   introduces a new term abbreviation @{text "c \<equiv> t"}.

   429

   430   \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML

   431   Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}

   432   convert between two representations of polymorphic constants: full

   433   type instance vs.\ compact type arguments form.

   434

   435   \end{description}

   436 *}

   437

   438 text %mlantiq {*

   439   \begin{matharray}{rcl}

   440   @{ML_antiquotation_def "const_name"} & : & @{text ML_antiquotation} \\

   441   @{ML_antiquotation_def "const_abbrev"} & : & @{text ML_antiquotation} \\

   442   @{ML_antiquotation_def "const"} & : & @{text ML_antiquotation} \\

   443   @{ML_antiquotation_def "term"} & : & @{text ML_antiquotation} \\

   444   @{ML_antiquotation_def "prop"} & : & @{text ML_antiquotation} \\

   445   \end{matharray}

   446

   447   @{rail "

   448   (@@{ML_antiquotation const_name} |

   449    @@{ML_antiquotation const_abbrev}) nameref

   450   ;

   451   @@{ML_antiquotation const} ('(' (type + ',') ')')?

   452   ;

   453   @@{ML_antiquotation term} term

   454   ;

   455   @@{ML_antiquotation prop} prop

   456   "}

   457

   458   \begin{description}

   459

   460   \item @{text "@{const_name c}"} inlines the internalized logical

   461   constant name @{text "c"} --- as @{ML_type string} literal.

   462

   463   \item @{text "@{const_abbrev c}"} inlines the internalized

   464   abbreviated constant name @{text "c"} --- as @{ML_type string}

   465   literal.

   466

   467   \item @{text "@{const c(\<^vec>\<tau>)}"} inlines the internalized

   468   constant @{text "c"} with precise type instantiation in the sense of

   469   @{ML Sign.const_instance} --- as @{ML Const} constructor term for

   470   datatype @{ML_type term}.

   471

   472   \item @{text "@{term t}"} inlines the internalized term @{text "t"}

   473   --- as constructor term for datatype @{ML_type term}.

   474

   475   \item @{text "@{prop \<phi>}"} inlines the internalized proposition

   476   @{text "\<phi>"} --- as constructor term for datatype @{ML_type term}.

   477

   478   \end{description}

   479 *}

   480

   481

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

   483

   484 text {*

   485   A \emph{proposition} is a well-typed term of type @{text "prop"}, a

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

   487   hypotheses and the background theory).  Primitive inferences include

   488   plain Natural Deduction rules for the primary connectives @{text

   489   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There is also a builtin

   490   notion of equality/equivalence @{text "\<equiv>"}.

   491 *}

   492

   493

   494 subsection {* Primitive connectives and rules \label{sec:prim-rules} *}

   495

   496 text {*

   497   The theory @{text "Pure"} contains constant declarations for the

   498   primitive connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of

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

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

   501   defined inductively by the primitive inferences given in

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

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

   504   builtin equality is conceptually axiomatized as shown in

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

   506   directly with derived inferences.

   507

   508   \begin{figure}[htb]

   509   \begin{center}

   510   \begin{tabular}{ll}

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

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

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

   514   \end{tabular}

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

   516   \end{center}

   517   \end{figure}

   518

   519   \begin{figure}[htb]

   520   \begin{center}

   521   $  522 \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}}   523 \qquad   524 \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}   525$

   526   $  527 \infer[@{text "(\<And>\<hyphen>intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}}   528 \qquad   529 \infer[@{text "(\<And>\<hyphen>elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}   530$

   531   $  532 \infer[@{text "(\<Longrightarrow>\<hyphen>intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}   533 \qquad   534 \infer[@{text "(\<Longrightarrow>\<hyphen>elim)"}]{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}}   535$

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

   537   \end{center}

   538   \end{figure}

   539

   540   \begin{figure}[htb]

   541   \begin{center}

   542   \begin{tabular}{ll}

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

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

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

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

   547   @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\

   548   \end{tabular}

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

   550   \end{center}

   551   \end{figure}

   552

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

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

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

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

   557   propositions.  The system provides a runtime option to record

   558   explicit proof terms for primitive inferences.  Thus all three

   559   levels of @{text "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for

   560   terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\

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

   562

   563   Observe that locally fixed parameters (as in @{text

   564   "\<And>\<hyphen>intro"}) need not be recorded in the hypotheses, because

   565   the simple syntactic types of Pure are always inhabitable.

   566   Assumptions'' @{text "x :: \<tau>"} for type-membership are only

   567   present as long as some @{text "x\<^isub>\<tau>"} occurs in the statement

   568   body.\footnote{This is the key difference to @{text "\<lambda>HOL"}'' in

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

   570   @{text "x : A"} are treated uniformly for propositions and types.}

   571

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

   573   forming all instances of type and term variables: @{text "\<turnstile>

   574   A\<vartheta>"} holds for any substitution instance of an axiom

   575   @{text "\<turnstile> A"}.  By pushing substitutions through derivations

   576   inductively, we also get admissible @{text "generalize"} and @{text

   577   "instantiate"} rules as shown in \figref{fig:subst-rules}.

   578

   579   \begin{figure}[htb]

   580   \begin{center}

   581   $  582 \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}   583 \quad   584 \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}   585$

   586   $  587 \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}   588 \quad   589 \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}   590$

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

   592   \end{center}

   593   \end{figure}

   594

   595   Note that @{text "instantiate"} does not require an explicit

   596   side-condition, because @{text "\<Gamma>"} may never contain schematic

   597   variables.

   598

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

   600   but this would disrupt the monotonicity of reasoning: deriving

   601   @{text "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is

   602   correct, but @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold:

   603   the result belongs to a different proof context.

   604

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

   606   fly.  Logically, this is an instance of the @{text "axiom"} rule

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

   608   The system always records oracle invocations within derivations of

   609   theorems by a unique tag.

   610

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

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

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

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

   615

   616   A \emph{simple definition} consists of a constant declaration @{text

   617   "c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text "t

   618   :: \<sigma>"} is a closed term without any hidden polymorphism.  The RHS

   619   may depend on further defined constants, but not @{text "c"} itself.

   620   Definitions of functions may be presented as @{text "c \<^vec>x \<equiv>

   621   t"} instead of the puristic @{text "c \<equiv> \<lambda>\<^vec>x. t"}.

   622

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

   624   for the same constant, with zero or one equations @{text

   625   "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type constructor @{text "\<kappa>"} (for

   626   distinct variables @{text "\<^vec>\<alpha>"}).  The RHS may mention

   627   previously defined constants as above, or arbitrary constants @{text

   628   "d(\<alpha>\<^isub>i)"} for some @{text "\<alpha>\<^isub>i"} projected from @{text

   629   "\<^vec>\<alpha>"}.  Thus overloaded definitions essentially work by

   630   primitive recursion over the syntactic structure of a single type

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

   632 *}

   633

   634 text %mlref {*

   635   \begin{mldecls}

   636   @{index_ML_type ctyp} \\

   637   @{index_ML_type cterm} \\

   638   @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\

   639   @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\

   640   \end{mldecls}

   641   \begin{mldecls}

   642   @{index_ML_type thm} \\

   643   @{index_ML proofs: "int Unsynchronized.ref"} \\

   644   @{index_ML Thm.transfer: "theory -> thm -> thm"} \\

   645   @{index_ML Thm.assume: "cterm -> thm"} \\

   646   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\

   647   @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\

   648   @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\

   649   @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\

   650   @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\

   651   @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\

   652   @{index_ML Thm.add_axiom: "Proof.context ->

   653   binding * term -> theory -> (string * thm) * theory"} \\

   654   @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->

   655   (string * ('a -> thm)) * theory"} \\

   656   @{index_ML Thm.add_def: "Proof.context -> bool -> bool ->

   657   binding * term -> theory -> (string * thm) * theory"} \\

   658   \end{mldecls}

   659   \begin{mldecls}

   660   @{index_ML Theory.add_deps: "Proof.context -> string ->

   661   string * typ -> (string * typ) list -> theory -> theory"} \\

   662   \end{mldecls}

   663

   664   \begin{description}

   665

   666   \item Types @{ML_type ctyp} and @{ML_type cterm} represent certified

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

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

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

   670   constructors, constants etc. in the theory.

   671

   672   \item @{ML Thm.ctyp_of}~@{text "thy \<tau>"} and @{ML

   673   Thm.cterm_of}~@{text "thy t"} explicitly checks types and terms,

   674   respectively.  This also involves some basic normalizations, such

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

   676

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

   678   reasoning loops.  There are separate operations to decompose

   679   certified entities (including actual theorems).

   680

   681   \item Type @{ML_type thm} represents proven propositions.  This is

   682   an abstract datatype that guarantees that its values have been

   683   constructed by basic principles of the @{ML_struct Thm} module.

   684   Every @{ML_type thm} value contains a sliding back-reference to the

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

   686

   687   \item @{ML proofs} specifies the detail of proof recording within

   688   @{ML_type thm} values: @{ML 0} records only the names of oracles,

   689   @{ML 1} records oracle names and propositions, @{ML 2} additionally

   690   records full proof terms.  Officially named theorems that contribute

   691   to a result are recorded in any case.

   692

   693   \item @{ML Thm.transfer}~@{text "thy thm"} transfers the given

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

   695   This formal adjustment of the background context has no logical

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

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

   698   the current situation.

   699

   700   \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML

   701   Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}

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

   703

   704   \item @{ML Thm.generalize}~@{text "(\<^vec>\<alpha>, \<^vec>x)"}

   705   corresponds to the @{text "generalize"} rules of

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

   707   variables are generalized simultaneously, specified by the given

   708   basic names.

   709

   710   \item @{ML Thm.instantiate}~@{text "(\<^vec>\<alpha>\<^isub>s,

   711   \<^vec>x\<^isub>\<tau>)"} corresponds to the @{text "instantiate"} rules

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

   713   term variables.  Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}

   714   refer to the instantiated versions.

   715

   716   \item @{ML Thm.add_axiom}~@{text "ctxt (name, A)"} declares an

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

   718   the resulting theory, cf.\ @{text "axiom"} in

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

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

   721

   722   \item @{ML Thm.add_oracle}~@{text "(binding, oracle)"} produces a named

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

   724   cf.\ @{text "axiom"} in \figref{fig:prim-rules}.

   725

   726   \item @{ML Thm.add_def}~@{text "ctxt unchecked overloaded (name, c

   727   \<^vec>x \<equiv> t)"} states a definitional axiom for an existing constant

   728   @{text "c"}.  Dependencies are recorded via @{ML Theory.add_deps},

   729   unless the @{text "unchecked"} option is set.  Note that the

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

   731   the returned theorem.

   732

   733   \item @{ML Theory.add_deps}~@{text "ctxt name c\<^isub>\<tau> \<^vec>d\<^isub>\<sigma>"}

   734   declares dependencies of a named specification for constant @{text

   735   "c\<^isub>\<tau>"}, relative to existing specifications for constants @{text

   736   "\<^vec>d\<^isub>\<sigma>"}.

   737

   738   \end{description}

   739 *}

   740

   741

   742 text %mlantiq {*

   743   \begin{matharray}{rcl}

   744   @{ML_antiquotation_def "ctyp"} & : & @{text ML_antiquotation} \\

   745   @{ML_antiquotation_def "cterm"} & : & @{text ML_antiquotation} \\

   746   @{ML_antiquotation_def "cprop"} & : & @{text ML_antiquotation} \\

   747   @{ML_antiquotation_def "thm"} & : & @{text ML_antiquotation} \\

   748   @{ML_antiquotation_def "thms"} & : & @{text ML_antiquotation} \\

   749   @{ML_antiquotation_def "lemma"} & : & @{text ML_antiquotation} \\

   750   \end{matharray}

   751

   752   @{rail "

   753   @@{ML_antiquotation ctyp} typ

   754   ;

   755   @@{ML_antiquotation cterm} term

   756   ;

   757   @@{ML_antiquotation cprop} prop

   758   ;

   759   @@{ML_antiquotation thm} thmref

   760   ;

   761   @@{ML_antiquotation thms} thmrefs

   762   ;

   763   @@{ML_antiquotation lemma} ('(' @'open' ')')? ((prop +) + @'and') \\

   764     @'by' method method?

   765   "}

   766

   767   \begin{description}

   768

   769   \item @{text "@{ctyp \<tau>}"} produces a certified type wrt.\ the

   770   current background theory --- as abstract value of type @{ML_type

   771   ctyp}.

   772

   773   \item @{text "@{cterm t}"} and @{text "@{cprop \<phi>}"} produce a

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

   775   value of type @{ML_type cterm}.

   776

   777   \item @{text "@{thm a}"} produces a singleton fact --- as abstract

   778   value of type @{ML_type thm}.

   779

   780   \item @{text "@{thms a}"} produces a general fact --- as abstract

   781   value of type @{ML_type "thm list"}.

   782

   783   \item @{text "@{lemma \<phi> by meth}"} produces a fact that is proven on

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

   785   Isar proof.  The result is an abstract value of type @{ML_type thm}

   786   or @{ML_type "thm list"}, depending on the number of propositions

   787   given here.

   788

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

   790   is formally closed, unless the @{text "(open)"} option is specified

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

   792

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

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

   795   the justification is syntactically limited to a single @{command

   796   "by"} step.  More complex Isar proofs should be done in regular

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

   798   the result.

   799

   800   \end{description}

   801

   802 *}

   803

   804

   805 subsection {* Auxiliary definitions \label{sec:logic-aux} *}

   806

   807 text {*

   808   Theory @{text "Pure"} provides a few auxiliary definitions, see

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

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

   811

   812   \begin{figure}[htb]

   813   \begin{center}

   814   \begin{tabular}{ll}

   815   @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&&&"}) \\

   816   @{text "\<turnstile> A &&& B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \$1ex]   817 @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}, suppressed) \\   818 @{text "#A \<equiv> A"} \\[1ex]   819 @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\   820 @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]   821 @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\   822 @{text "(unspecified)"} \\   823 \end{tabular}   824 \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}   825 \end{center}   826 \end{figure}   827   828 The introduction @{text "A \<Longrightarrow> B \<Longrightarrow> A &&& B"}, and eliminations   829 (projections) @{text "A &&& B \<Longrightarrow> A"} and @{text "A &&& B \<Longrightarrow> B"} are   830 available as derived rules. Conjunction allows to treat   831 simultaneous assumptions and conclusions uniformly, e.g.\ consider   832 @{text "A \<Longrightarrow> B \<Longrightarrow> C &&& D"}. In particular, the goal mechanism   833 represents multiple claims as explicit conjunction internally, but   834 this is refined (via backwards introduction) into separate sub-goals   835 before the user commences the proof; the final result is projected   836 into a list of theorems using eliminations (cf.\   837 \secref{sec:tactical-goals}).   838   839 The @{text "prop"} marker (@{text "#"}) makes arbitrarily complex   840 propositions appear as atomic, without changing the meaning: @{text   841 "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are interchangeable. See   842 \secref{sec:tactical-goals} for specific operations.   843   844 The @{text "term"} marker turns any well-typed term into a derivable   845 proposition: @{text "\<turnstile> TERM t"} holds unconditionally. Although   846 this is logically vacuous, it allows to treat terms and proofs   847 uniformly, similar to a type-theoretic framework.   848   849 The @{text "TYPE"} constructor is the canonical representative of   850 the unspecified type @{text "\<alpha> itself"}; it essentially injects the   851 language of types into that of terms. There is specific notation   852 @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau>   853 itself\<^esub>"}.   854 Although being devoid of any particular meaning, the term @{text   855 "TYPE(\<tau>)"} accounts for the type @{text "\<tau>"} within the term   856 language. In particular, @{text "TYPE(\<alpha>)"} may be used as formal   857 argument in primitive definitions, in order to circumvent hidden   858 polymorphism (cf.\ \secref{sec:terms}). For example, @{text "c   859 TYPE(\<alpha>) \<equiv> A[\<alpha>]"} defines @{text "c :: \<alpha> itself \<Rightarrow> prop"} in terms of   860 a proposition @{text "A"} that depends on an additional type   861 argument, which is essentially a predicate on types.   862 *}   863   864 text %mlref {*   865 \begin{mldecls}   866 @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\   867 @{index_ML Conjunction.elim: "thm -> thm * thm"} \\   868 @{index_ML Drule.mk_term: "cterm -> thm"} \\   869 @{index_ML Drule.dest_term: "thm -> cterm"} \\   870 @{index_ML Logic.mk_type: "typ -> term"} \\   871 @{index_ML Logic.dest_type: "term -> typ"} \\   872 \end{mldecls}   873   874 \begin{description}   875   876 \item @{ML Conjunction.intr} derives @{text "A &&& B"} from @{text   877 "A"} and @{text "B"}.   878   879 \item @{ML Conjunction.elim} derives @{text "A"} and @{text "B"}   880 from @{text "A &&& B"}.   881   882 \item @{ML Drule.mk_term} derives @{text "TERM t"}.   883   884 \item @{ML Drule.dest_term} recovers term @{text "t"} from @{text   885 "TERM t"}.   886   887 \item @{ML Logic.mk_type}~@{text "\<tau>"} produces the term @{text   888 "TYPE(\<tau>)"}.   889   890 \item @{ML Logic.dest_type}~@{text "TYPE(\<tau>)"} recovers the type   891 @{text "\<tau>"}.   892   893 \end{description}   894 *}   895   896   897 section {* Object-level rules \label{sec:obj-rules} *}   898   899 text {*   900 The primitive inferences covered so far mostly serve foundational   901 purposes. User-level reasoning usually works via object-level rules   902 that are represented as theorems of Pure. Composition of rules   903 involves \emph{backchaining}, \emph{higher-order unification} modulo   904 @{text "\<alpha>\<beta>\<eta>"}-conversion of @{text "\<lambda>"}-terms, and so-called   905 \emph{lifting} of rules into a context of @{text "\<And>"} and @{text   906 "\<Longrightarrow>"} connectives. Thus the full power of higher-order Natural   907 Deduction in Isabelle/Pure becomes readily available.   908 *}   909   910   911 subsection {* Hereditary Harrop Formulae *}   912   913 text {*   914 The idea of object-level rules is to model Natural Deduction   915 inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow   916 arbitrary nesting similar to \cite{extensions91}. The most basic   917 rule format is that of a \emph{Horn Clause}:   918 \[   919 \infer{@{text "A"}}{@{text "A\<^sub>1"} & @{text "\<dots>"} & @{text "A\<^sub>n"}}   920$

   921   where @{text "A, A\<^sub>1, \<dots>, A\<^sub>n"} are atomic propositions

   922   of the framework, usually of the form @{text "Trueprop B"}, where

   923   @{text "B"} is a (compound) object-level statement.  This

   924   object-level inference corresponds to an iterated implication in

   925   Pure like this:

   926   $  927 @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A"}   928$

   929   As an example consider conjunction introduction: @{text "A \<Longrightarrow> B \<Longrightarrow> A \<and>

   930   B"}.  Any parameters occurring in such rule statements are

   931   conceptionally treated as arbitrary:

   932   $  933 @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. A\<^sub>1 x\<^sub>1 \<dots> x\<^sub>m \<Longrightarrow> \<dots> A\<^sub>n x\<^sub>1 \<dots> x\<^sub>m \<Longrightarrow> A x\<^sub>1 \<dots> x\<^sub>m"}   934$

   935

   936   Nesting of rules means that the positions of @{text "A\<^sub>i"} may

   937   again hold compound rules, not just atomic propositions.

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

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

   940   inductive characterization as follows:

   941

   942   \medskip

   943   \begin{tabular}{ll}

   944   @{text "\<^bold>x"} & set of variables \\

   945   @{text "\<^bold>A"} & set of atomic propositions \\

   946   @{text "\<^bold>H  =  \<And>\<^bold>x\<^sup>*. \<^bold>H\<^sup>* \<Longrightarrow> \<^bold>A"} & set of Hereditary Harrop Formulas \\

   947   \end{tabular}

   948   \medskip

   949

   950   Thus we essentially impose nesting levels on propositions formed

   951   from @{text "\<And>"} and @{text "\<Longrightarrow>"}.  At each level there is a prefix

   952   of parameters and compound premises, concluding an atomic

   953   proposition.  Typical examples are @{text "\<longrightarrow>"}-introduction @{text

   954   "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"} or mathematical induction @{text "P 0 \<Longrightarrow> (\<And>n. P n

   955   \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n"}.  Even deeper nesting occurs in well-founded

   956   induction @{text "(\<And>x. (\<And>y. y \<prec> x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"}, but this

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

   958   practice.

   959

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

   961   maintain the following canonical form of results:

   962

   963   \begin{itemize}

   964

   965   \item Normalization by @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"},

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

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

   968   Hereditary Harrop Formula.

   969

   970   \item The outermost prefix of parameters is represented via

   971   schematic variables: instead of @{text "\<And>\<^vec>x. \<^vec>H \<^vec>x

   972   \<Longrightarrow> A \<^vec>x"} we have @{text "\<^vec>H ?\<^vec>x \<Longrightarrow> A ?\<^vec>x"}.

   973   Note that this representation looses information about the order of

   974   parameters, and vacuous quantifiers vanish automatically.

   975

   976   \end{itemize}

   977 *}

   978

   979 text %mlref {*

   980   \begin{mldecls}

   981   @{index_ML Simplifier.norm_hhf: "thm -> thm"} \\

   982   \end{mldecls}

   983

   984   \begin{description}

   985

   986   \item @{ML Simplifier.norm_hhf}~@{text thm} normalizes the given

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

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

   989   handle Hereditary Harrop Formulae properly.

   990

   991   \end{description}

   992 *}

   993

   994

   995 subsection {* Rule composition *}

   996

   997 text {*

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

   999   @{inference resolution} (i.e.\ back-chaining of rules) and

  1000   @{inference assumption} (i.e.\ closing a branch), both modulo

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

  1002   @{inference elim_resolution} and @{inference dest_resolution}.

  1003

  1004   To understand the all-important @{inference resolution} principle,

  1005   we first consider raw @{inference_def composition} (modulo

  1006   higher-order unification with substitution @{text "\<vartheta>"}):

  1007   $  1008 \infer[(@{inference_def composition})]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}   1009 {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}   1010$

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

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

  1013   first and conclusion of the second.  Note that @{text "C"} can again

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

  1015   of the second rule back-and-forth in order to compose with @{text

  1016   "B'"} in any position (subsequently we shall always refer to

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

  1018

  1019   In @{inference composition} the internal structure of the common

  1020   part @{text "B"} and @{text "B'"} is not taken into account.  For

  1021   proper @{inference resolution} we require @{text "B"} to be atomic,

  1022   and explicitly observe the structure @{text "\<And>\<^vec>x. \<^vec>H

  1023   \<^vec>x \<Longrightarrow> B' \<^vec>x"} of the premise of the second rule.  The

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

  1025   by means of iterated application of the following inferences:

  1026   $  1027 \infer[(@{inference_def imp_lift})]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}   1028$

  1029   $  1030 \infer[(@{inference_def all_lift})]{@{text "(\<And>\<^vec>x. \<^vec>A (?\<^vec>a \<^vec>x)) \<Longrightarrow> (\<And>\<^vec>x. B (?\<^vec>a \<^vec>x))"}}{@{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"}}   1031$

  1032   By combining raw composition with lifting, we get full @{inference

  1033   resolution} as follows:

  1034   $  1035 \infer[(@{inference_def resolution})]   1036 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}   1037 {\begin{tabular}{l}   1038 @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\   1039 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\   1040 @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\   1041 \end{tabular}}   1042$

  1043

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

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

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

  1047   solved situation (again modulo unification):

  1048   $  1049 \infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}}   1050 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text i})}}   1051$

  1052

  1053   FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}

  1054 *}

  1055

  1056 text %mlref {*

  1057   \begin{mldecls}

  1058   @{index_ML "op RS": "thm * thm -> thm"} \\

  1059   @{index_ML "op OF": "thm * thm list -> thm"} \\

  1060   \end{mldecls}

  1061

  1062   \begin{description}

  1063

  1064   \item @{text "rule\<^sub>1 RS rule\<^sub>2"} resolves @{text "rule\<^sub>1"} with @{text

  1065   "rule\<^sub>2"} according to the @{inference resolution} principle

  1066   explained above.  Note that the corresponding rule attribute in the

  1067   Isar language is called @{attribute THEN}.

  1068

  1069   \item @{text "rule OF rules"} resolves a list of rules with the

  1070   first rule, addressing its premises @{text "1, \<dots>, length rules"}

  1071   (operating from last to first).  This means the newly emerging

  1072   premises are all concatenated, without interfering.  Also note that

  1073   compared to @{text "RS"}, the rule argument order is swapped: @{text

  1074   "rule\<^sub>1 RS rule\<^sub>2 = rule\<^sub>2 OF [rule\<^sub>1]"}.

  1075

  1076   \end{description}

  1077 *}

  1078

  1079 end