src/Doc/IsarImplementation/Logic.thy
 author wenzelm Tue Aug 28 18:57:32 2012 +0200 (2012-08-28) changeset 48985 5386df44a037 parent 48938 doc-src/IsarImplementation/Logic.thy@d468d72a458f child 50126 3dec88149176 permissions -rw-r--r--
renamed doc-src to src/Doc;
renamed TutorialI to Tutorial;
     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.transfer: "theory -> thm -> thm"} \\   652 @{index_ML Thm.assume: "cterm -> thm"} \\   653 @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\   654 @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\   655 @{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\   656 @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\   657 @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\   658 @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\   659 @{index_ML Thm.add_axiom: "Proof.context ->   660 binding * term -> theory -> (string * thm) * theory"} \\   661 @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->   662 (string * ('a -> thm)) * theory"} \\   663 @{index_ML Thm.add_def: "Proof.context -> bool -> bool ->   664 binding * term -> theory -> (string * thm) * theory"} \\   665 \end{mldecls}   666 \begin{mldecls}   667 @{index_ML Theory.add_deps: "Proof.context -> string ->   668 string * typ -> (string * typ) list -> theory -> theory"} \\   669 \end{mldecls}   670   671 \begin{description}   672   673 \item @{ML Logic.all}~@{text "a B"} produces a Pure quantification   674 @{text "\<And>a. B"}, where occurrences of the atomic term @{text "a"} in   675 the body proposition @{text "B"} are replaced by bound variables.   676 (See also @{ML lambda} on terms.)   677   678 \item @{ML Logic.mk_implies}~@{text "(A, B)"} produces a Pure   679 implication @{text "A \<Longrightarrow> B"}.   680   681 \item Types @{ML_type ctyp} and @{ML_type cterm} represent certified   682 types and terms, respectively. These are abstract datatypes that   683 guarantee that its values have passed the full well-formedness (and   684 well-typedness) checks, relative to the declarations of type   685 constructors, constants etc.\ in the background theory. The   686 abstract types @{ML_type ctyp} and @{ML_type cterm} are part of the   687 same inference kernel that is mainly responsible for @{ML_type thm}.   688 Thus syntactic operations on @{ML_type ctyp} and @{ML_type cterm}   689 are located in the @{ML_struct Thm} module, even though theorems are   690 not yet involved at that stage.   691   692 \item @{ML Thm.ctyp_of}~@{text "thy \<tau>"} and @{ML   693 Thm.cterm_of}~@{text "thy t"} explicitly checks types and terms,   694 respectively. This also involves some basic normalizations, such   695 expansion of type and term abbreviations from the theory context.   696 Full re-certification is relatively slow and should be avoided in   697 tight reasoning loops.   698   699 \item @{ML Thm.apply}, @{ML Thm.lambda}, @{ML Thm.all}, @{ML   700 Drule.mk_implies} etc.\ compose certified terms (or propositions)   701 incrementally. This is equivalent to @{ML Thm.cterm_of} after   702 unchecked @{ML_op "$"}, @{ML lambda}, @{ML Logic.all}, @{ML

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

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

   705   constructions on top.  There are separate operations to decompose

   706   certified terms and theorems to produce certified terms again.

   707

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

   709   an abstract datatype that guarantees that its values have been

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

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

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

   713

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

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

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

   717   records full proof terms.  Officially named theorems that contribute

   718   to a result are recorded in any case.

   719

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

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

   722   This formal adjustment of the background context has no logical

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

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

   725   the current situation.

   726

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

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

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

   730

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

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

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

   734   variables are generalized simultaneously, specified by the given

   735   basic names.

   736

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

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

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

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

   741   refer to the instantiated versions.

   742

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

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

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

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

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

   748

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

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

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

   752

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

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

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

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

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

   758   the returned theorem.

   759

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

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

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

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

   764

   765   \end{description}

   766 *}

   767

   768

   769 text %mlantiq {*

   770   \begin{matharray}{rcl}

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

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

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

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

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

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

   777   \end{matharray}

   778

   779   @{rail "

   780   @@{ML_antiquotation ctyp} typ

   781   ;

   782   @@{ML_antiquotation cterm} term

   783   ;

   784   @@{ML_antiquotation cprop} prop

   785   ;

   786   @@{ML_antiquotation thm} thmref

   787   ;

   788   @@{ML_antiquotation thms} thmrefs

   789   ;

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

   791     @'by' method method?

   792   "}

   793

   794   \begin{description}

   795

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

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

   798   ctyp}.

   799

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

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

   802   value of type @{ML_type cterm}.

   803

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

   805   value of type @{ML_type thm}.

   806

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

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

   809

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

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

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

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

   814   given here.

   815

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

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

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

   819

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

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

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

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

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

   825   the result.

   826

   827   \end{description}

   828

   829 *}

   830

   831

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

   833

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

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

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

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

   838   the user.

   839

   840   \begin{figure}[htb]

   841   \begin{center}

   842   \begin{tabular}{ll}

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

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

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

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

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

   952   object-level inference corresponds to an iterated implication in

   953   Pure like this:

   954   $  955 @{text "A\<^sub>1 \<Longrightarrow> \<dots> A\<^sub>n \<Longrightarrow> A"}   956$

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

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

   959   conceptionally treated as arbitrary:

   960   $  961 @{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"}   962$

   963

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

   965   again hold compound rules, not just atomic propositions.

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

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

   968   inductive characterization as follows:

   969

   970   \medskip

   971   \begin{tabular}{ll}

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

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

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

   975   \end{tabular}

   976   \medskip

   977

   978   Thus we essentially impose nesting levels on propositions formed

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

   980   of parameters and compound premises, concluding an atomic

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

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

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

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

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

   986   practice.

   987

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

   989   maintain the following canonical form of results:

   990

   991   \begin{itemize}

   992

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

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

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

   996   Hereditary Harrop Formula.

   997

   998   \item The outermost prefix of parameters is represented via

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

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

  1001   Note that this representation looses information about the order of

  1002   parameters, and vacuous quantifiers vanish automatically.

  1003

  1004   \end{itemize}

  1005 *}

  1006

  1007 text %mlref {*

  1008   \begin{mldecls}

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

  1010   \end{mldecls}

  1011

  1012   \begin{description}

  1013

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

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

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

  1017   handle Hereditary Harrop Formulae properly.

  1018

  1019   \end{description}

  1020 *}

  1021

  1022

  1023 subsection {* Rule composition *}

  1024

  1025 text {*

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

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

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

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

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

  1031

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

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

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

  1035   $  1036 \infer[(@{inference_def composition})]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}   1037 {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}   1038$

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

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

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

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

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

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

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

  1046

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

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

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

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

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

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

  1053   by means of iterated application of the following inferences:

  1054   $  1055 \infer[(@{inference_def imp_lift})]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}   1056$

  1057   $  1058 \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"}}   1059$

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

  1061   resolution} as follows:

  1062   $  1063 \infer[(@{inference_def resolution})]   1064 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}   1065 {\begin{tabular}{l}   1066 @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\   1067 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\   1068 @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\   1069 \end{tabular}}   1070$

  1071

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

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

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

  1075   solved situation (again modulo unification):

  1076   $  1077 \infer[(@{inference_def assumption})]{@{text "C\<vartheta>"}}   1078 {@{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})}}   1079$

  1080

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

  1082 *}

  1083

  1084 text %mlref {*

  1085   \begin{mldecls}

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

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

  1088

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

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

  1091

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

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

  1094   \end{mldecls}

  1095

  1096   \begin{description}

  1097

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

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

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

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

  1102   THM}.

  1103

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

  1105   source language.

  1106

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

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

  1109

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

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

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

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

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

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

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

  1117

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

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

  1120

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

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

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

  1124   concatenated in the result, without interfering.

  1125

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

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

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

  1129   not be atomic.

  1130

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

  1132   source language.

  1133

  1134   \end{description}

  1135 *}

  1136

  1137 end