src/Doc/IsarImplementation/Logic.thy
 author wenzelm Mon Nov 19 20:23:47 2012 +0100 (2012-11-19 ago) changeset 50126 3dec88149176 parent 48985 5386df44a037 child 52406 1e57c3c4e05c permissions -rw-r--r--
theorem status about oracles/futures is no longer printed by default;
renamed Proofterm/Thm.status_of to Proofterm/Thm.peek_status to emphasize its semantics;
     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_type: "Proof.context -> binding * int * mixfix -> theory -> theory"} \\

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

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

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

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

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

   136   \end{mldecls}

   137

   138   \begin{description}

   139

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

   141

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

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

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

   145

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

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

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

   149

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

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

   152

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

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

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

   156

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

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

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

   160   right.

   161

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

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

   164

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

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

   167

   168   \item @{ML Sign.add_type}~@{text "ctxt (\<kappa>, k, mx)"} declares a

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

   170   optional mixfix syntax.

   171

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

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

   174

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

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

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

   178

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

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

   181   c\<^isub>2"}.

   182

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

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

   185

   186   \end{description}

   187 *}

   188

   189 text %mlantiq {*

   190   \begin{matharray}{rcl}

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

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

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

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

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

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

   197   \end{matharray}

   198

   199   @{rail "

   200   @@{ML_antiquotation class} nameref

   201   ;

   202   @@{ML_antiquotation sort} sort

   203   ;

   204   (@@{ML_antiquotation type_name} |

   205    @@{ML_antiquotation type_abbrev} |

   206    @@{ML_antiquotation nonterminal}) nameref

   207   ;

   208   @@{ML_antiquotation typ} type

   209   "}

   210

   211   \begin{description}

   212

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

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

   215

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

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

   218

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

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

   221

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

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

   224

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

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

   227   literal.

   228

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

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

   231

   232   \end{description}

   233 *}

   234

   235

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

   237

   238 text {*

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

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

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

   242   corresponding binders.  In contrast, free variables and constants

   243   have an explicit name and type in each occurrence.

   244

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

   246   which accounts for the number of intermediate binders between the

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

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

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

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

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

   252   the nesting of abstractions.

   253

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

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

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

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

   258   without any loose variables.

   259

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

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

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

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

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

   265

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

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

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

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

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

   271

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

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

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

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

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

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

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

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

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

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

   282

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

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

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

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

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

   288   due to violation of type class restrictions.

   289

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

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

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

   293   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

   294   converting between an external representation with named bound

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

   296   of internal de-Bruijn representation.

   297

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

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

   300   applicatins:

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

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

   309

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

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

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

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

   314   variables, and declarations for polymorphic constants.

   315

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

   317   component.  This means that different variables @{text

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

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

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

   321   polymorphic constants occur routinely.

   322

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

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

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

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

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

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

   329   pathological situation notoriously demands additional care.

   330

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

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

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

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

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

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

   337

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

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

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

   341   abstraction applied to an argument term, substituting the argument

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

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

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

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

   346

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

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

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

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

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

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

   353 *}

   354

   355 text %mlref {*

   356   \begin{mldecls}

   357   @{index_ML_type term} \\

   358   @{index_ML_op "aconv": "term * term -> bool"} \\

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

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

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

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

   363   \end{mldecls}

   364   \begin{mldecls}

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

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

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

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

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

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

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

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

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

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

   375   \end{mldecls}

   376

   377   \begin{description}

   378

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

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

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

   382   Var}, @{ML Const}, @{ML Abs}, @{ML_op "$"}.   383   384 \item @{text "t"}~@{ML_text aconv}~@{text "u"} checks @{text   385 "\<alpha>"}-equivalence of two terms. This is the basic equality relation   386 on type @{ML_type term}; raw datatype equality should only be used   387 for operations related to parsing or printing!   388   389 \item @{ML Term.map_types}~@{text "f t"} applies the mapping @{text   390 "f"} to all types occurring in @{text "t"}.   391   392 \item @{ML Term.fold_types}~@{text "f t"} iterates the operation   393 @{text "f"} over all occurrences of types in @{text "t"}; the term   394 structure is traversed from left to right.   395   396 \item @{ML Term.map_aterms}~@{text "f t"} applies the mapping @{text   397 "f"} to all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML   398 Const}) occurring in @{text "t"}.   399   400 \item @{ML Term.fold_aterms}~@{text "f t"} iterates the operation   401 @{text "f"} over all occurrences of atomic terms (@{ML Bound}, @{ML   402 Free}, @{ML Var}, @{ML Const}) in @{text "t"}; the term structure is   403 traversed from left to right.   404   405 \item @{ML fastype_of}~@{text "t"} determines the type of a   406 well-typed term. This operation is relatively slow, despite the   407 omission of any sanity checks.   408   409 \item @{ML lambda}~@{text "a b"} produces an abstraction @{text   410 "\<lambda>a. b"}, where occurrences of the atomic term @{text "a"} in the   411 body @{text "b"} are replaced by bound variables.   412   413 \item @{ML betapply}~@{text "(t, u)"} produces an application @{text   414 "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an   415 abstraction.   416   417 \item @{ML incr_boundvars}~@{text "j"} increments a term's dangling   418 bound variables by the offset @{text "j"}. This is required when   419 moving a subterm into a context where it is enclosed by a different   420 number of abstractions. Bound variables with a matching abstraction   421 are unaffected.   422   423 \item @{ML Sign.declare_const}~@{text "ctxt ((c, \<sigma>), mx)"} declares   424 a new constant @{text "c :: \<sigma>"} with optional mixfix syntax.   425   426 \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"}   427 introduces a new term abbreviation @{text "c \<equiv> t"}.   428   429 \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML   430 Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}   431 convert between two representations of polymorphic constants: full   432 type instance vs.\ compact type arguments form.   433   434 \end{description}   435 *}   436   437 text %mlantiq {*   438 \begin{matharray}{rcl}   439 @{ML_antiquotation_def "const_name"} & : & @{text ML_antiquotation} \\   440 @{ML_antiquotation_def "const_abbrev"} & : & @{text ML_antiquotation} \\   441 @{ML_antiquotation_def "const"} & : & @{text ML_antiquotation} \\   442 @{ML_antiquotation_def "term"} & : & @{text ML_antiquotation} \\   443 @{ML_antiquotation_def "prop"} & : & @{text ML_antiquotation} \\   444 \end{matharray}   445   446 @{rail "   447 (@@{ML_antiquotation const_name} |   448 @@{ML_antiquotation const_abbrev}) nameref   449 ;   450 @@{ML_antiquotation const} ('(' (type + ',') ')')?   451 ;   452 @@{ML_antiquotation term} term   453 ;   454 @@{ML_antiquotation prop} prop   455 "}   456   457 \begin{description}   458   459 \item @{text "@{const_name c}"} inlines the internalized logical   460 constant name @{text "c"} --- as @{ML_type string} literal.   461   462 \item @{text "@{const_abbrev c}"} inlines the internalized   463 abbreviated constant name @{text "c"} --- as @{ML_type string}   464 literal.   465   466 \item @{text "@{const c(\<^vec>\<tau>)}"} inlines the internalized   467 constant @{text "c"} with precise type instantiation in the sense of   468 @{ML Sign.const_instance} --- as @{ML Const} constructor term for   469 datatype @{ML_type term}.   470   471 \item @{text "@{term t}"} inlines the internalized term @{text "t"}   472 --- as constructor term for datatype @{ML_type term}.   473   474 \item @{text "@{prop \<phi>}"} inlines the internalized proposition   475 @{text "\<phi>"} --- as constructor term for datatype @{ML_type term}.   476   477 \end{description}   478 *}   479   480   481 section {* Theorems \label{sec:thms} *}   482   483 text {*   484 A \emph{proposition} is a well-typed term of type @{text "prop"}, a   485 \emph{theorem} is a proven proposition (depending on a context of   486 hypotheses and the background theory). Primitive inferences include   487 plain Natural Deduction rules for the primary connectives @{text   488 "\<And>"} and @{text "\<Longrightarrow>"} of the framework. There is also a builtin   489 notion of equality/equivalence @{text "\<equiv>"}.   490 *}   491   492   493 subsection {* Primitive connectives and rules \label{sec:prim-rules} *}   494   495 text {*   496 The theory @{text "Pure"} contains constant declarations for the   497 primitive connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"} of   498 the logical framework, see \figref{fig:pure-connectives}. The   499 derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is   500 defined inductively by the primitive inferences given in   501 \figref{fig:prim-rules}, with the global restriction that the   502 hypotheses must \emph{not} contain any schematic variables. The   503 builtin equality is conceptually axiomatized as shown in   504 \figref{fig:pure-equality}, although the implementation works   505 directly with derived inferences.   506   507 \begin{figure}[htb]   508 \begin{center}   509 \begin{tabular}{ll}   510 @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\   511 @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\   512 @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\   513 \end{tabular}   514 \caption{Primitive connectives of Pure}\label{fig:pure-connectives}   515 \end{center}   516 \end{figure}   517   518 \begin{figure}[htb]   519 \begin{center}   520 $  521 \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}}   522 \qquad   523 \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}   524$   525 $  526 \infer[@{text "(\<And>\<hyphen>intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}{@{text "\<Gamma> \<turnstile> b[x]"} & @{text "x \<notin> \<Gamma>"}}   527 \qquad   528 \infer[@{text "(\<And>\<hyphen>elim)"}]{@{text "\<Gamma> \<turnstile> b[a]"}}{@{text "\<Gamma> \<turnstile> \<And>x. b[x]"}}   529$   530 $  531 \infer[@{text "(\<Longrightarrow>\<hyphen>intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}   532 \qquad   533 \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"}}   534$   535 \caption{Primitive inferences of Pure}\label{fig:prim-rules}   536 \end{center}   537 \end{figure}   538   539 \begin{figure}[htb]   540 \begin{center}   541 \begin{tabular}{ll}   542 @{text "\<turnstile> (\<lambda>x. b[x]) a \<equiv> b[a]"} & @{text "\<beta>"}-conversion \\   543 @{text "\<turnstile> x \<equiv> x"} & reflexivity \\   544 @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\   545 @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\   546 @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & logical equivalence \\   547 \end{tabular}   548 \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}   549 \end{center}   550 \end{figure}   551   552 The introduction and elimination rules for @{text "\<And>"} and @{text   553 "\<Longrightarrow>"} are analogous to formation of dependently typed @{text   554 "\<lambda>"}-terms representing the underlying proof objects. Proof terms   555 are irrelevant in the Pure logic, though; they cannot occur within   556 propositions. The system provides a runtime option to record   557 explicit proof terms for primitive inferences. Thus all three   558 levels of @{text "\<lambda>"}-calculus become explicit: @{text "\<Rightarrow>"} for   559 terms, and @{text "\<And>/\<Longrightarrow>"} for proofs (cf.\   560 \cite{Berghofer-Nipkow:2000:TPHOL}).   561   562 Observe that locally fixed parameters (as in @{text   563 "\<And>\<hyphen>intro"}) need not be recorded in the hypotheses, because   564 the simple syntactic types of Pure are always inhabitable.   565 Assumptions'' @{text "x :: \<tau>"} for type-membership are only   566 present as long as some @{text "x\<^isub>\<tau>"} occurs in the statement   567 body.\footnote{This is the key difference to @{text "\<lambda>HOL"}'' in   568 the PTS framework \cite{Barendregt-Geuvers:2001}, where hypotheses   569 @{text "x : A"} are treated uniformly for propositions and types.}   570   571 \medskip The axiomatization of a theory is implicitly closed by   572 forming all instances of type and term variables: @{text "\<turnstile>   573 A\<vartheta>"} holds for any substitution instance of an axiom   574 @{text "\<turnstile> A"}. By pushing substitutions through derivations   575 inductively, we also get admissible @{text "generalize"} and @{text   576 "instantiate"} rules as shown in \figref{fig:subst-rules}.   577   578 \begin{figure}[htb]   579 \begin{center}   580 $  581 \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}   582 \quad   583 \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}   584$   585 $  586 \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}   587 \quad   588 \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}   589$   590 \caption{Admissible substitution rules}\label{fig:subst-rules}   591 \end{center}   592 \end{figure}   593   594 Note that @{text "instantiate"} does not require an explicit   595 side-condition, because @{text "\<Gamma>"} may never contain schematic   596 variables.   597   598 In principle, variables could be substituted in hypotheses as well,   599 but this would disrupt the monotonicity of reasoning: deriving   600 @{text "\<Gamma>\<vartheta> \<turnstile> B\<vartheta>"} from @{text "\<Gamma> \<turnstile> B"} is   601 correct, but @{text "\<Gamma>\<vartheta> \<supseteq> \<Gamma>"} does not necessarily hold:   602 the result belongs to a different proof context.   603   604 \medskip An \emph{oracle} is a function that produces axioms on the   605 fly. Logically, this is an instance of the @{text "axiom"} rule   606 (\figref{fig:prim-rules}), but there is an operational difference.   607 The system always records oracle invocations within derivations of   608 theorems by a unique tag.   609   610 Axiomatizations should be limited to the bare minimum, typically as   611 part of the initial logical basis of an object-logic formalization.   612 Later on, theories are usually developed in a strictly definitional   613 fashion, by stating only certain equalities over new constants.   614   615 A \emph{simple definition} consists of a constant declaration @{text   616 "c :: \<sigma>"} together with an axiom @{text "\<turnstile> c \<equiv> t"}, where @{text "t   617 :: \<sigma>"} is a closed term without any hidden polymorphism. The RHS   618 may depend on further defined constants, but not @{text "c"} itself.   619 Definitions of functions may be presented as @{text "c \<^vec>x \<equiv>   620 t"} instead of the puristic @{text "c \<equiv> \<lambda>\<^vec>x. t"}.   621   622 An \emph{overloaded definition} consists of a collection of axioms   623 for the same constant, with zero or one equations @{text   624 "c((\<^vec>\<alpha>)\<kappa>) \<equiv> t"} for each type constructor @{text "\<kappa>"} (for   625 distinct variables @{text "\<^vec>\<alpha>"}). The RHS may mention   626 previously defined constants as above, or arbitrary constants @{text   627 "d(\<alpha>\<^isub>i)"} for some @{text "\<alpha>\<^isub>i"} projected from @{text   628 "\<^vec>\<alpha>"}. Thus overloaded definitions essentially work by   629 primitive recursion over the syntactic structure of a single type   630 argument. See also \cite[\S4.3]{Haftmann-Wenzel:2006:classes}.   631 *}   632   633 text %mlref {*   634 \begin{mldecls}   635 @{index_ML Logic.all: "term -> term -> term"} \\   636 @{index_ML Logic.mk_implies: "term * term -> term"} \\   637 \end{mldecls}   638 \begin{mldecls}   639 @{index_ML_type ctyp} \\   640 @{index_ML_type cterm} \\   641 @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\   642 @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\   643 @{index_ML Thm.apply: "cterm -> cterm -> cterm"} \\   644 @{index_ML Thm.lambda: "cterm -> cterm -> cterm"} \\   645 @{index_ML Thm.all: "cterm -> cterm -> cterm"} \\   646 @{index_ML Drule.mk_implies: "cterm * cterm -> cterm"} \\   647 \end{mldecls}   648 \begin{mldecls}   649 @{index_ML_type thm} \\   650 @{index_ML proofs: "int Unsynchronized.ref"} \\   651 @{index_ML Thm.peek_status: "thm -> {oracle: bool, unfinished: bool, failed: bool}"} \\   652 @{index_ML Thm.transfer: "theory -> thm -> thm"} \\   653 @{index_ML Thm.assume: "cterm -> thm"} \\   654 @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\   655 @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\   656 @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\   657 @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\   658 @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\   659 @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\   660 @{index_ML Thm.add_axiom: "Proof.context ->   661 binding * term -> theory -> (string * thm) * theory"} \\   662 @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->   663 (string * ('a -> thm)) * theory"} \\   664 @{index_ML Thm.add_def: "Proof.context -> bool -> bool ->   665 binding * term -> theory -> (string * thm) * theory"} \\   666 \end{mldecls}   667 \begin{mldecls}   668 @{index_ML Theory.add_deps: "Proof.context -> string ->   669 string * typ -> (string * typ) list -> theory -> theory"} \\   670 \end{mldecls}   671   672 \begin{description}   673   674 \item @{ML Thm.peek_status}~@{text "thm"} informs about the current   675 status of the derivation object behind the given theorem. This is a   676 snapshot of a potentially ongoing (parallel) evaluation of proofs.   677 The three Boolean values indicate the following: @{verbatim oracle}   678 if the finished part contains some oracle invocation; @{verbatim   679 unfinished} if some future proofs are still pending; @{verbatim   680 failed} if some future proof has failed, rendering the theorem   681 invalid!   682   683 \item @{ML Logic.all}~@{text "a B"} produces a Pure quantification   684 @{text "\<And>a. B"}, where occurrences of the atomic term @{text "a"} in   685 the body proposition @{text "B"} are replaced by bound variables.   686 (See also @{ML lambda} on terms.)   687   688 \item @{ML Logic.mk_implies}~@{text "(A, B)"} produces a Pure   689 implication @{text "A \<Longrightarrow> B"}.   690   691 \item Types @{ML_type ctyp} and @{ML_type cterm} represent certified   692 types and terms, respectively. These are abstract datatypes that   693 guarantee that its values have passed the full well-formedness (and   694 well-typedness) checks, relative to the declarations of type   695 constructors, constants etc.\ in the background theory. The   696 abstract types @{ML_type ctyp} and @{ML_type cterm} are part of the   697 same inference kernel that is mainly responsible for @{ML_type thm}.   698 Thus syntactic operations on @{ML_type ctyp} and @{ML_type cterm}   699 are located in the @{ML_struct Thm} module, even though theorems are   700 not yet involved at that stage.   701   702 \item @{ML Thm.ctyp_of}~@{text "thy \<tau>"} and @{ML   703 Thm.cterm_of}~@{text "thy t"} explicitly checks types and terms,   704 respectively. This also involves some basic normalizations, such   705 expansion of type and term abbreviations from the theory context.   706 Full re-certification is relatively slow and should be avoided in   707 tight reasoning loops.   708   709 \item @{ML Thm.apply}, @{ML Thm.lambda}, @{ML Thm.all}, @{ML   710 Drule.mk_implies} etc.\ compose certified terms (or propositions)   711 incrementally. This is equivalent to @{ML Thm.cterm_of} after   712 unchecked @{ML_op "$"}, @{ML lambda}, @{ML Logic.all}, @{ML

   713   Logic.mk_implies} etc., but there can be a big difference in

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

   715   constructions on top.  There are separate operations to decompose

   716   certified terms and theorems to produce certified terms again.

   717

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

   719   an abstract datatype that guarantees that its values have been

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

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

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

   723

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

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

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

   727   records full proof terms.  Officially named theorems that contribute

   728   to a result are recorded in any case.

   729

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

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

   732   This formal adjustment of the background context has no logical

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

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

   735   the current situation.

   736

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

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

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

   740

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

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

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

   744   variables are generalized simultaneously, specified by the given

   745   basic names.

   746

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

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

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

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

   751   refer to the instantiated versions.

   752

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

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

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

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

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

   758

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

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

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

   762

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

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

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

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

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

   768   the returned theorem.

   769

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

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

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

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

   774

   775   \end{description}

   776 *}

   777

   778

   779 text %mlantiq {*

   780   \begin{matharray}{rcl}

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

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

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

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

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

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

   787   \end{matharray}

   788

   789   @{rail "

   790   @@{ML_antiquotation ctyp} typ

   791   ;

   792   @@{ML_antiquotation cterm} term

   793   ;

   794   @@{ML_antiquotation cprop} prop

   795   ;

   796   @@{ML_antiquotation thm} thmref

   797   ;

   798   @@{ML_antiquotation thms} thmrefs

   799   ;

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

   801     @'by' method method?

   802   "}

   803

   804   \begin{description}

   805

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

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

   808   ctyp}.

   809

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

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

   812   value of type @{ML_type cterm}.

   813

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

   815   value of type @{ML_type thm}.

   816

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

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

   819

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

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

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

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

   824   given here.

   825

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

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

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

   829

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

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

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

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

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

   835   the result.

   836

   837   \end{description}

   838

   839 *}

   840

   841

   842 subsection {* Auxiliary connectives \label{sec:logic-aux} *}

   843

   844 text {* Theory @{text "Pure"} provides a few auxiliary connectives

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

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

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

   848   the user.

   849

   850   \begin{figure}[htb]

   851   \begin{center}

   852   \begin{tabular}{ll}

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

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

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

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

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

   962   object-level inference corresponds to an iterated implication in

   963   Pure like this:

   964   $  965 @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A"}   966$

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

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

   969   conceptionally treated as arbitrary:

   970   $  971 @{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"}   972$

   973

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

   975   again hold compound rules, not just atomic propositions.

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

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

   978   inductive characterization as follows:

   979

   980   \medskip

   981   \begin{tabular}{ll}

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

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

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

   985   \end{tabular}

   986   \medskip

   987

   988   Thus we essentially impose nesting levels on propositions formed

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

   990   of parameters and compound premises, concluding an atomic

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

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

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

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

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

   996   practice.

   997

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

   999   maintain the following canonical form of results:

  1000

  1001   \begin{itemize}

  1002

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

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

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

  1006   Hereditary Harrop Formula.

  1007

  1008   \item The outermost prefix of parameters is represented via

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

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

  1011   Note that this representation looses information about the order of

  1012   parameters, and vacuous quantifiers vanish automatically.

  1013

  1014   \end{itemize}

  1015 *}

  1016

  1017 text %mlref {*

  1018   \begin{mldecls}

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

  1020   \end{mldecls}

  1021

  1022   \begin{description}

  1023

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

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

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

  1027   handle Hereditary Harrop Formulae properly.

  1028

  1029   \end{description}

  1030 *}

  1031

  1032

  1033 subsection {* Rule composition *}

  1034

  1035 text {*

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

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

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

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

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

  1041

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

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

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

  1045   $  1046 \infer[(@{inference_def composition})]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}   1047 {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}   1048$

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

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

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

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

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

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

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

  1056

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

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

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

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

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

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

  1063   by means of iterated application of the following inferences:

  1064   $  1065 \infer[(@{inference_def imp_lift})]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}   1066$

  1067   $  1068 \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"}}   1069$

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

  1071   resolution} as follows:

  1072   $  1073 \infer[(@{inference_def resolution})]   1074 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}   1075 {\begin{tabular}{l}   1076 @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\   1077 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\   1078 @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\   1079 \end{tabular}}   1080$

  1081

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

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

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

  1085   solved situation (again modulo unification):

  1086   $  1087 \infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}}   1088 {@{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})}}   1089$

  1090

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

  1092 *}

  1093

  1094 text %mlref {*

  1095   \begin{mldecls}

  1096   @{index_ML_op "RSN": "thm * (int * thm) -> thm"} \\

  1097   @{index_ML_op "RS": "thm * thm -> thm"} \\

  1098

  1099   @{index_ML_op "RLN": "thm list * (int * thm list) -> thm list"} \\

  1100   @{index_ML_op "RL": "thm list * thm list -> thm list"} \\

  1101

  1102   @{index_ML_op "MRS": "thm list * thm -> thm"} \\

  1103   @{index_ML_op "OF": "thm * thm list -> thm"} \\

  1104   \end{mldecls}

  1105

  1106   \begin{description}

  1107

  1108   \item @{text "rule\<^sub>1 RSN (i, rule\<^sub>2)"} resolves the conclusion of

  1109   @{text "rule\<^sub>1"} with the @{text i}-th premise of @{text "rule\<^sub>2"},

  1110   according to the @{inference resolution} principle explained above.

  1111   Unless there is precisely one resolvent it raises exception @{ML

  1112   THM}.

  1113

  1114   This corresponds to the rule attribute @{attribute THEN} in Isar

  1115   source language.

  1116

  1117   \item @{text "rule\<^sub>1 RS rule\<^sub>2"} abbreviates @{text "rule\<^sub>1 RS (1,

  1118   rule\<^sub>2)"}.

  1119

  1120   \item @{text "rules\<^sub>1 RLN (i, rules\<^sub>2)"} joins lists of rules.  For

  1121   every @{text "rule\<^sub>1"} in @{text "rules\<^sub>1"} and @{text "rule\<^sub>2"} in

  1122   @{text "rules\<^sub>2"}, it resolves the conclusion of @{text "rule\<^sub>1"} with

  1123   the @{text "i"}-th premise of @{text "rule\<^sub>2"}, accumulating multiple

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

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

  1126   variant seen in elementary tactics like @{ML resolve_tac}.

  1127

  1128   \item @{text "rules\<^sub>1 RL rules\<^sub>2"} abbreviates @{text "rules\<^sub>1 RLN (1,

  1129   rules\<^sub>2)"}.

  1130

  1131   \item @{text "[rule\<^sub>1, \<dots>, rule\<^sub>n] MRS rule"} resolves @{text "rule\<^isub>i"}

  1132   against premise @{text "i"} of @{text "rule"}, for @{text "i = n, \<dots>,

  1133   1"}.  By working from right to left, newly emerging premises are

  1134   concatenated in the result, without interfering.

  1135

  1136   \item @{text "rule OF rules"} is an alternative notation for @{text

  1137   "rules MRS rule"}, which makes rule composition look more like

  1138   function application.  Note that the argument @{text "rules"} need

  1139   not be atomic.

  1140

  1141   This corresponds to the rule attribute @{attribute OF} in Isar

  1142   source language.

  1143

  1144   \end{description}

  1145 *}

  1146

  1147 end