doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Tue Sep 12 21:05:39 2006 +0200 (2006-09-12) changeset 20521 189811b39869 parent 20520 05fd007bdeb9 child 20537 b6b49903db7e permissions -rw-r--r--
more on theorems;
     1

     2 (* $Id$ *)

     3

     4 theory logic imports base begin

     5

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

     7

     8 text {*

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

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

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

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

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

    14   differences in the specific treatment of simple types in

    15   Isabelle/Pure.

    16

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

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

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

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

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

    22

    23   Pure derivations are relative to a logical theory, which declares

    24   type constructors, term constants, and axioms.  Theory declarations

    25   support schematic polymorphism, which is strictly speaking outside

    26   the logic.\footnote{Incidently, this is the main logical reason, why

    27   the theory context @{text "\<Theta>"} is separate from the context @{text

    28   "\<Gamma>"} of the core calculus.}

    29 *}

    30

    31

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

    33

    34 text {*

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

    36   algebra; types are qualified by ordered type classes.

    37

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

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

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

    41   generating relation; the transitive closure is maintained

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

    43   transitive, and antisymmetric.

    44

    45   A \emph{sort} is a list of type classes written as @{text

    46   "{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic

    47   intersection.  Notationally, the curly braces are omitted for

    48   singleton intersections, i.e.\ any class @{text "c"} may be read as

    49   a sort @{text "{c}"}.  The ordering on type classes is extended to

    50   sorts according to the meaning of intersections: @{text

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

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

    53   @{text "{}"} refers to the universal sort, which is the largest

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

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

    56   elements wrt.\ the sort order.

    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.  For

    60   example, @{text "('a, s)"} which is usually printed as @{text

    61   "\<alpha>\<^isub>s"}.  A \emph{schematic type variable} is a pair of an

    62   indexname and a sort constraint.  For example, @{text "(('a, 0),

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

    64

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

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

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

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

    69   produce anything like this.

    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   usually written postfix as @{text "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}.

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

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

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

    77   "(\<alpha>)list"}.  Further notation is provided for specific constructors,

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

    79   @{text "(\<alpha>, \<beta>)fun"}.

    80

    81   A \emph{type} @{text "\<tau>"} is defined inductively over type variables

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

    83   ?\<alpha>\<^isub>s | (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)k"}.

    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 looks like type

    88   constructors at the surface, but are fully expanded before entering

    89   the 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 each type constructor @{text "\<kappa>"} and classes @{text

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

   103   (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "\<kappa>

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

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

   106

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

   108   constraints may be always solved in a most general fashion: for each

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

   110   general vector of argument sorts @{text "(s\<^isub>1, \<dots>,

   111   s\<^isub>k)"} such that a type scheme @{text

   112   "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is

   113   of sort @{text "s"}.  Consequently, the unification problem on the

   114   algebra of types has most general solutions (modulo renaming and

   115   equivalence of sorts).  Moreover, the usual type-inference algorithm

   116   will produce primary types as expected \cite{nipkow-prehofer}.

   117 *}

   118

   119 text %mlref {*

   120   \begin{mldecls}

   121   @{index_ML_type class} \\

   122   @{index_ML_type sort} \\

   123   @{index_ML_type arity} \\

   124   @{index_ML_type typ} \\

   125   @{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\

   126   @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\

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

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

   129   @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\

   130   @{index_ML Sign.add_tyabbrs_i: "

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

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

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

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

   135   \end{mldecls}

   136

   137   \begin{description}

   138

   139   \item @{ML_type class} represents type classes; this is an alias for

   140   @{ML_type string}.

   141

   142   \item @{ML_type sort} represents sorts; this is an alias for

   143   @{ML_type "class list"}.

   144

   145   \item @{ML_type arity} represents type arities; this is an alias for

   146   triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::

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

   148

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

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

   151

   152   \item @{ML map_atyps}~@{text "f \<tau>"} applies mapping @{text "f"} to

   153   all atomic types (@{ML TFree}, @{ML TVar}) occurring in @{text "\<tau>"}.

   154

   155   \item @{ML fold_atyps}~@{text "f \<tau>"} iterates operation @{text "f"}

   156   over all occurrences of atoms (@{ML TFree}, @{ML TVar}) in @{text

   157   "\<tau>"}; the type structure is traversed from left to right.

   158

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

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

   161

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

   163   is of a given sort.

   164

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

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

   167   optional mixfix syntax.

   168

   169   \item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}

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

   171   optional mixfix syntax.

   172

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

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

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

   176

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

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

   179   c\<^isub>2"}.

   180

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

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

   183

   184   \end{description}

   185 *}

   186

   187

   188

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

   190

   191 text {*

   192   \glossary{Term}{FIXME}

   193

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

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

   196   or \cite{paulson-ml2}), and named free variables and constants.

   197   Terms with loose bound variables are usually considered malformed.

   198   The types of variables and constants is stored explicitly at each

   199   occurrence in the term.

   200

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

   202   which refers to the next binder that is @{text "b"} steps upwards

   203   from the occurrence of @{text "b"} (counting from zero).  Bindings

   204   may be introduced as abstractions within the term, or as a separate

   205   context (an inside-out list).  This associates each bound variable

   206   with a type.  A \emph{loose variables} is a bound variable that is

   207   outside the current scope of local binders or the context.  For

   208   example, the de-Bruijn term @{text "\<lambda>\<^isub>\<tau>. \<lambda>\<^isub>\<tau>. 1 + 0"}

   209   corresponds to @{text "\<lambda>x\<^isub>\<tau>. \<lambda>y\<^isub>\<tau>. x + y"} in a named

   210   representation.  Also note that the very same bound variable may get

   211   different numbers at different occurrences.

   212

   213   A \emph{fixed variable} is a pair of a basic name and a type.  For

   214   example, @{text "(x, \<tau>)"} which is usually printed @{text

   215   "x\<^isub>\<tau>"}.  A \emph{schematic variable} is a pair of an

   216   indexname and a type.  For example, @{text "((x, 0), \<tau>)"} which is

   217   usually printed as @{text "?x\<^isub>\<tau>"}.

   218

   219   \medskip A \emph{constant} is a atomic terms consisting of a basic

   220   name and a type.  Constants are declared in the context as

   221   polymorphic families @{text "c :: \<sigma>"}, meaning that any @{text

   222   "c\<^isub>\<tau>"} is a valid constant for all substitution instances

   223   @{text "\<tau> \<le> \<sigma>"}.

   224

   225   The list of \emph{type arguments} of @{text "c\<^isub>\<tau>"} wrt.\ the

   226   declaration @{text "c :: \<sigma>"} is the codomain of the type matcher

   227   presented in canonical order (according to the left-to-right

   228   occurrences of type variables in in @{text "\<sigma>"}).  Thus @{text

   229   "c\<^isub>\<tau>"} can be represented more compactly as @{text

   230   "c(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n)"}.  For example, the instance @{text

   231   "plus\<^bsub>nat \<Rightarrow> nat \<Rightarrow> nat\<^esub>"} of some @{text "plus :: \<alpha> \<Rightarrow> \<alpha>

   232   \<Rightarrow> \<alpha>"} has the singleton list @{text "nat"} as type arguments, the

   233   constant may be represented as @{text "plus(nat)"}.

   234

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

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

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

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

   239   polymorphic constants that the user-level type-checker would reject.

   240

   241   \medskip A \emph{term} @{text "t"} is defined inductively over

   242   variables and constants, with abstraction and application as

   243   follows: @{text "t = b | x\<^isub>\<tau> | ?x\<^isub>\<tau> | c\<^isub>\<tau> |

   244   \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}.  Parsing and printing takes

   245   care of converting between an external representation with named

   246   bound variables.  Subsequently, we shall use the latter notation

   247   instead of internal de-Bruijn representation.

   248

   249   The subsequent inductive relation @{text "t :: \<tau>"} assigns a

   250   (unique) type to a term, using the special type constructor @{text

   251   "(\<alpha>, \<beta>)fun"}, which is written @{text "\<alpha> \<Rightarrow> \<beta>"}.

   252   $  253 \infer{@{text "a\<^isub>\<tau> :: \<tau>"}}{}   254 \qquad   255 \infer{@{text "(\<lambda>x\<^sub>\<tau>. t) :: \<tau> \<Rightarrow> \<sigma>"}}{@{text "t :: \<sigma>"}}   256 \qquad   257 \infer{@{text "t u :: \<sigma>"}}{@{text "t :: \<tau> \<Rightarrow> \<sigma>"} & @{text "u :: \<tau>"}}   258$

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

   260

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

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

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

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

   265   variables, and declarations for polymorphic constants.

   266

   267   The identity of atomic terms consists both of the name and the type.

   268   Thus different entities @{text "c\<^bsub>\<tau>\<^isub>1\<^esub>"} and

   269   @{text "c\<^bsub>\<tau>\<^isub>2\<^esub>"} may well identified by type

   270   instantiation, by mapping @{text "\<tau>\<^isub>1"} and @{text

   271   "\<tau>\<^isub>2"} to the same @{text "\<tau>"}.  Although,

   272   different type instances of constants of the same basic name are

   273   commonplace, this rarely happens for variables: type-inference

   274   always demands consistent'' type constraints.

   275

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

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

   278   @{text "\<sigma>"}.  This means that the term implicitly depends on the

   279   values of various type variables that are not visible in the overall

   280   type, i.e.\ there are different type instances @{text "t\<vartheta>

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

   282   slightly pathological situation is apt to cause strange effects.

   283

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

   285   "c\<^isub>\<sigma> \<equiv> t"} of an arbitrary closed term @{text "t"} of type

   286   @{text "\<sigma>"} without any hidden polymorphism.  A term abbreviation

   287   looks like a constant at the surface, but is fully expanded before

   288   entering the logical core.  Abbreviations are usually reverted when

   289   printing terms, using rules @{text "t \<rightarrow> c\<^isub>\<sigma>"} has a

   290   higher-order term rewrite system.

   291

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

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

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

   295   abstraction applied to some argument term, substituting the argument

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

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

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

   299   @{text "0"} does not occur in @{text "f"}.

   300

   301   Terms are almost always treated module @{text "\<alpha>"}-conversion, which

   302   is implicit in the de-Bruijn representation.  The names in

   303   abstractions of bound variables are maintained only as a comment for

   304   parsing and printing.  Full @{text "\<alpha>\<beta>\<eta>"}-equivalence is usually

   305   taken for granted higher rules (\secref{sec:rules}), anything

   306   depending on higher-order unification or rewriting.

   307 *}

   308

   309 text %mlref {*

   310   \begin{mldecls}

   311   @{index_ML_type term} \\

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

   313   @{index_ML map_term_types: "(typ -> typ) -> term -> term"} \\  %FIXME rename map_types

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

   315   @{index_ML map_aterms: "(term -> term) -> term -> term"} \\

   316   @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\

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

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

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

   320   @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\

   321   @{index_ML Sign.add_abbrevs: "string * bool ->

   322   ((string * mixfix) * term) list -> theory -> theory"} \\

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

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

   325   \end{mldecls}

   326

   327   \begin{description}

   328

   329   \item @{ML_type term} represents de-Bruijn terms with comments in

   330   abstractions for bound variable names.  This is a datatype with

   331   constructors @{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const}, @{ML

   332   Abs}, @{ML "op \$"}.

   333

   334   \item @{text "t"}~@{ML aconv}~@{text "u"} checks @{text

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

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

   337   for operations related to parsing or printing!

   338

   339   \item @{ML map_term_types}~@{text "f t"} applies mapping @{text "f"}

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

   341

   342   \item @{ML fold_types}~@{text "f t"} iterates operation @{text "f"}

   343   over all occurrences of types in @{text "t"}; the term structure is

   344   traversed from left to right.

   345

   346   \item @{ML map_aterms}~@{text "f t"} applies mapping @{text "f"} to

   347   all atomic terms (@{ML Bound}, @{ML Free}, @{ML Var}, @{ML Const})

   348   occurring in @{text "t"}.

   349

   350   \item @{ML fold_aterms}~@{text "f t"} iterates operation @{text "f"}

   351   over all occurrences of atomic terms in (@{ML Bound}, @{ML Free},

   352   @{ML Var}, @{ML Const}) @{text "t"}; the term structure is traversed

   353   from left to right.

   354

   355   \item @{ML fastype_of}~@{text "t"} recomputes the type of a

   356   well-formed term, while omitting any sanity checks.  This operation

   357   is relatively slow.

   358

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

   360   "\<lambda>a. b"}, where occurrences of the original (atomic) term @{text

   361   "a"} in the body @{text "b"} are replaced by bound variables.

   362

   363   \item @{ML betapply}~@{text "t u"} produces an application @{text "t

   364   u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} happens to

   365   be an abstraction.

   366

   367   \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a

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

   369

   370   \item @{ML Sign.add_abbrevs}~@{text "print_mode [((c, t), mx), \<dots>]"}

   371   declares a new term abbreviation @{text "c \<equiv> t"} with optional

   372   mixfix syntax.

   373

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

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

   376   convert between the two representations of constants, namely full

   377   type instance vs.\ compact type arguments form (depending on the

   378   most general declaration given in the context).

   379

   380   \end{description}

   381 *}

   382

   383

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

   385

   386 text {*

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

   388   \seeglossary{type} @{text "prop"}.  Internally, there is nothing

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

   390   syntax enforces a clear distinction.  Propositions are structured

   391   via implication @{text "A \<Longrightarrow> B"} or universal quantification @{text

   392   "\<And>x. B x"} --- anything else is considered atomic.  The canonical

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

   394   Formula}. FIXME}

   395

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

   397   proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are

   398   rarely spelled out explicitly.  Theorems are usually normalized

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

   400

   401   \glossary{Fact}{Sometimes used interchangeably for

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

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

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

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

   406

   407   \glossary{Schematic variable}{FIXME}

   408

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

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

   411   proof text. FIXME}

   412

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

   414   variable}. FIXME}

   415

   416   \glossary{Bound variable}{FIXME}

   417

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

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

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

   421   different variables is their binding scope. FIXME}

   422

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

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

   425   hypotheses and the background theory).  Primitive inferences include

   426   plain natural deduction rules for the primary connectives @{text

   427   "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There are separate (derived)

   428   rules for equality/equivalence @{text "\<equiv>"} and internal conjunction

   429   @{text "&"}.

   430 *}

   431

   432 subsection {* Standard connectives and rules *}

   433

   434 text {*

   435   The basic theory is called @{text "Pure"}, it contains declarations

   436   for the standard logical connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and

   437   @{text "\<equiv>"} of the framework, see \figref{fig:pure-connectives}.

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

   439   defined inductively by the primitive inferences given in

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

   441   hypotheses may never contain schematic variables.  The builtin

   442   equality is conceptually axiomatized shown in

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

   444   directly with (derived) inference rules.

   445

   446   \begin{figure}[htb]

   447   \begin{center}

   448   \begin{tabular}{ll}

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

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

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

   452   \end{tabular}

   453   \caption{Standard connectives of Pure}\label{fig:pure-connectives}

   454   \end{center}

   455   \end{figure}

   456

   457   \begin{figure}[htb]

   458   \begin{center}

   459   $  460 \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}}   461 \qquad   462 \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}   463$

   464   $  465 \infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b x"}}{@{text "\<Gamma> \<turnstile> b x"} & @{text "x \<notin> \<Gamma>"}}   466 \qquad   467 \infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b a"}}{@{text "\<Gamma> \<turnstile> \<And>x. b x"}}   468$

   469   $  470 \infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}   471 \qquad   472 \infer[@{text "(\<Longrightarrow>_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"}}   473$

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

   475   \end{center}

   476   \end{figure}

   477

   478   \begin{figure}[htb]

   479   \begin{center}

   480   \begin{tabular}{ll}

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

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

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

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

   485   @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & coincidence with equivalence \\

   486   \end{tabular}

   487   \caption{Conceptual axiomatization of builtin equality}\label{fig:pure-equality}

   488   \end{center}

   489   \end{figure}

   490

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

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

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

   494   are \emph{irrelevant} in the Pure logic, they may never occur within

   495   propositions, i.e.\ the @{text "\<Longrightarrow>"} arrow is non-dependent.  The

   496   system provides a runtime option to record explicit proof terms for

   497   primitive inferences, cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}.  Thus

   498   the three-fold @{text "\<lambda>"}-structure can be made explicit.

   499

   500   Observe that locally fixed parameters (as used in rule @{text

   501   "\<And>_intro"}) need not be recorded in the hypotheses, because the

   502   simple syntactic types of Pure are always inhabitable.  The typing

   503   assumption'' @{text "x :: \<tau>"} is logically vacuous, it disappears

   504   automatically whenever the statement body ceases to mention variable

   505   @{text "x\<^isub>\<tau>"}.\footnote{This greatly simplifies many basic

   506   reasoning steps, and is the key difference to the formulation of

   507   this logic as @{text "\<lambda>HOL"}'' in the PTS framework

   508   \cite{Barendregt-Geuvers:2001}.}

   509

   510   \medskip FIXME @{text "\<alpha>\<beta>\<eta>"}-equivalence and primitive definitions

   511

   512   Since the basic representation of terms already accounts for @{text

   513   "\<alpha>"}-conversion, Pure equality essentially acts like @{text

   514   "\<alpha>\<beta>\<eta>"}-equivalence on terms, while coinciding with bi-implication.

   515

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

   517   forming all instances of type and term variables: @{text "\<turnstile> A\<vartheta>"} for

   518   any substitution instance of axiom @{text "\<turnstile> A"}.  By pushing

   519   substitution through derivations inductively, we get admissible

   520   substitution rules for theorems shown in \figref{fig:subst-rules}.

   521   Alternatively, the term substitution rules could be derived from

   522   @{text "\<And>_intro/elim"}.  The versions for types are genuine

   523   admissible rules, due to the lack of true polymorphism in the logic.

   524

   525   \begin{figure}[htb]

   526   \begin{center}

   527   $  528 \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}   529 \quad   530 \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}   531$

   532   $  533 \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}   534 \quad   535 \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}   536$

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

   538   \end{center}

   539   \end{figure}

   540

   541   Since @{text "\<Gamma>"} may never contain any schematic variables, the

   542   @{text "instantiate"} do not require an explicit side-condition.  In

   543   principle, variables could be substituted in hypotheses as well, but

   544   this could disrupt monotonicity of the basic calculus: derivations

   545   could leave the current proof context.

   546 *}

   547

   548 text %mlref {*

   549   \begin{mldecls}

   550   @{index_ML_type ctyp} \\

   551   @{index_ML_type cterm} \\

   552   @{index_ML_type thm} \\

   553   \end{mldecls}

   554

   555   \begin{description}

   556

   557   \item @{ML_type ctyp} FIXME

   558

   559   \item @{ML_type cterm} FIXME

   560

   561   \item @{ML_type thm} FIXME

   562

   563   \end{description}

   564 *}

   565

   566

   567 subsection {* Auxiliary connectives *}

   568

   569 text {*

   570   Pure also provides various auxiliary connectives based on primitive

   571   definitions, see \figref{fig:pure-aux}.  These are normally not

   572   exposed to the user, but appear in internal encodings only.

   573

   574   \begin{figure}[htb]

   575   \begin{center}

   576   \begin{tabular}{ll}

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

   578   @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \$1ex]   579 @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}) \\   580 @{text "#A \<equiv> A"} \\[1ex]   581 @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\   582 @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]   583 @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\   584 @{text "(unspecified)"} \\   585 \end{tabular}   586 \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}   587 \end{center}   588 \end{figure}   589   590 Conjunction as an explicit connective allows to treat both   591 simultaneous assumptions and conclusions uniformly. The definition   592 allows to derive the usual introduction @{text "\<turnstile> A \<Longrightarrow> B \<Longrightarrow> A & B"},   593 and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B \<Longrightarrow> B"}. For   594 example, several claims may be stated at the same time, which is   595 intermediately represented as an assumption, but the user only   596 encounters several sub-goals, and several resulting facts in the   597 very end (cf.\ \secref{sec:tactical-goals}).   598   599 The @{text "#"} marker allows complex propositions (nested @{text   600 "\<And>"} and @{text "\<Longrightarrow>"}) to appear formally as atomic, without changing   601 the meaning: @{text "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are   602 interchangeable. See \secref{sec:tactical-goals} for specific   603 operations.   604   605 The @{text "TERM"} marker turns any well-formed term into a   606 derivable proposition: @{text "\<turnstile> TERM t"} holds   607 unconditionally. Despite its logically vacous meaning, this is   608 occasionally useful to treat syntactic terms and proven propositions   609 uniformly, as in a type-theoretic framework.   610   611 The @{text "TYPE"} constructor (which is the canonical   612 representative of the unspecified type @{text "\<alpha> itself"}) injects   613 the language of types into that of terms. There is specific   614 notation @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau>   615 itself\<^esub>"}.   616 Although being devoid of any particular meaning, the term @{text   617 "TYPE(\<tau>)"} is able to carry the type @{text "\<tau>"} formally. @{text   618 "TYPE(\<alpha>)"} may be used as an additional formal argument in primitive   619 definitions, in order to avoid hidden polymorphism (cf.\   620 \secref{sec:terms}). For example, @{text "c TYPE(\<alpha>) \<equiv> A[\<alpha>]"} turns   621 out as a formally correct definition of some proposition @{text "A"}   622 that depends on an additional type argument.   623 *}   624   625 text %mlref {*   626 \begin{mldecls}   627 @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\   628 @{index_ML Conjunction.elim: "thm -> thm * thm"} \\   629 @{index_ML Drule.mk_term: "cterm -> thm"} \\   630 @{index_ML Drule.dest_term: "thm -> cterm"} \\   631 @{index_ML Logic.mk_type: "typ -> term"} \\   632 @{index_ML Logic.dest_type: "term -> typ"} \\   633 \end{mldecls}   634   635 \begin{description}   636   637 \item FIXME   638   639 \end{description}   640 *}   641   642   643 section {* Rules \label{sec:rules} *}   644   645 text {*   646   647 FIXME   648   649 A \emph{rule} is any Pure theorem in HHF normal form; there is a   650 separate calculus for rule composition, which is modeled after   651 Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows   652 rules to be nested arbitrarily, similar to \cite{extensions91}.   653   654 Normally, all theorems accessible to the user are proper rules.   655 Low-level inferences are occasional required internally, but the   656 result should be always presented in canonical form. The higher   657 interfaces of Isabelle/Isar will always produce proper rules. It is   658 important to maintain this invariant in add-on applications!   659   660 There are two main principles of rule composition: @{text   661 "resolution"} (i.e.\ backchaining of rules) and @{text   662 "by-assumption"} (i.e.\ closing a branch); both principles are   663 combined in the variants of @{text "elim-resolution"} and @{text   664 "dest-resolution"}. Raw @{text "composition"} is occasionally   665 useful as well, also it is strictly speaking outside of the proper   666 rule calculus.   667   668 Rules are treated modulo general higher-order unification, which is   669 unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion   670 on @{text "\<lambda>"}-terms. Moreover, propositions are understood modulo   671 the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.   672   673 This means that any operations within the rule calculus may be   674 subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions. It is common   675 practice not to contract or expand unnecessarily. Some mechanisms   676 prefer an one form, others the opposite, so there is a potential   677 danger to produce some oscillation!   678   679 Only few operations really work \emph{modulo} HHF conversion, but   680 expect a normal form: quantifiers @{text "\<And>"} before implications   681 @{text "\<Longrightarrow>"} at each level of nesting.   682   683 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF   684 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>   685 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.   686 Any proposition may be put into HHF form by normalizing with the rule   687 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}. In Isabelle, the outermost   688 quantifier prefix is represented via \seeglossary{schematic   689 variables}, such that the top-level structure is merely that of a   690 \seeglossary{Horn Clause}}.   691   692 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}   693   694   695 \[   696 \infer[@{text "(assumption)"}]{@{text "C\<vartheta>"}}   697 {@{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})}}   698$

   699

   700

   701   $  702 \infer[@{text "(compose)"}]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}   703 {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}   704$

   705

   706

   707   $  708 \infer[@{text "(\<And>_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"}}   709$

   710   $  711 \infer[@{text "(\<Longrightarrow>_lift)"}]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}   712$

   713

   714   The @{text resolve} scheme is now acquired from @{text "\<And>_lift"},

   715   @{text "\<Longrightarrow>_lift"}, and @{text compose}.

   716

   717   $  718 \infer[@{text "(resolution)"}]   719 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}   720 {\begin{tabular}{l}   721 @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\   722 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\   723 @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\   724 \end{tabular}}   725$

   726

   727

   728   FIXME @{text "elim_resolution"}, @{text "dest_resolution"}

   729 *}

   730

   731

   732 end