doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Tue Sep 12 17:23:34 2006 +0200 (2006-09-12) changeset 20519 d7ad1217c24a parent 20514 5ede702cd2ca child 20520 05fd007bdeb9 permissions -rw-r--r--
more on terms;
     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: "(bstring * int * mixfix) list -> theory -> theory"} \\

   130   @{index_ML Sign.add_tyabbrs_i: "

   131   (bstring * 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

   196   \cite{debruijn72,paulson-ml2}, and named free variables and

   197   constants.  Terms with loose bound variables are usually considered

   198   malformed.  The types of variables and constants is stored

   199   explicitly at each 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: "(bstring * typ * mixfix) list -> theory -> theory"} \\

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

   322   ((bstring * 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"} 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 @{text "t"} is an

   365   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>)"} produces the

   375   type arguments of the instance @{text "c\<^isub>\<tau>"} wrt.\ its

   376   declaration in the theory.

   377

   378   \item @{ML Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>,

   379   \<tau>\<^isub>n])"} produces the full instance @{text "c(\<tau>\<^isub>1, \<dots>,

   380   \<tau>\<^isub>n)"} wrt.\ its declaration in the theory.

   381

   382   \end{description}

   383 *}

   384

   385

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

   387

   388 text {*

   389   \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}

   390   @{text "prop"}.  Internally, there is nothing special about

   391   propositions apart from their type, but the concrete syntax enforces

   392   a clear distinction.  Propositions are structured via implication

   393   @{text "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} ---

   394   anything else is considered atomic.  The canonical form for

   395   propositions is that of a \seeglossary{Hereditary Harrop Formula}. FIXME}

   396

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

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

   399   rarely spelled out explicitly.  Theorems are usually normalized

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

   401

   402   \glossary{Fact}{Sometimes used interchangeably for

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

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

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

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

   407

   408   \glossary{Schematic variable}{FIXME}

   409

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

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

   412   proof text. FIXME}

   413

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

   415   variable}. FIXME}

   416

   417   \glossary{Bound variable}{FIXME}

   418

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

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

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

   422   different variables is their binding scope. FIXME}

   423

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

   425   The connectives of minimal logic are declared as constants of the

   426   basic theory:

   427

   428   \smallskip

   429   \begin{tabular}{ll}

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

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

   432   \end{tabular}

   433

   434   \medskip A \emph{theorem} is a proven proposition, depending on a

   435   collection of assumptions, and axioms from the theory context.  The

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

   437   inductively by the primitive inferences given in

   438   \figref{fig:prim-rules}; there is a global syntactic restriction

   439   that the hypotheses may not contain schematic variables.

   440

   441   \begin{figure}[htb]

   442   \begin{center}

   443   $  444 \infer[@{text "(axiom)"}]{@{text "\<turnstile> A"}}{@{text "A \<in> \<Theta>"}}   445 \qquad   446 \infer[@{text "(assume)"}]{@{text "A \<turnstile> A"}}{}   447$

   448   $  449 \infer[@{text "(\<And>_intro)"}]{@{text "\<Gamma> \<turnstile> \<And>x. b x"}}{@{text "\<Gamma> \<turnstile> b x"} & @{text "x \<notin> \<Gamma>"}}   450 \qquad   451 \infer[@{text "(\<And>_elim)"}]{@{text "\<Gamma> \<turnstile> b a"}}{@{text "\<Gamma> \<turnstile> \<And>x. b x"}}   452$

   453   $  454 \infer[@{text "(\<Longrightarrow>_intro)"}]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}   455 \qquad   456 \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"}}   457$

   458   \caption{Primitive inferences of the Pure logic}\label{fig:prim-rules}

   459   \end{center}

   460   \end{figure}

   461

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

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

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

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

   466   propositions, i.e.\ the @{text "\<Longrightarrow>"} arrow of the framework is a

   467   non-dependent one.

   468

   469   Also note that fixed parameters as in @{text "\<And>_intro"} need not be

   470   recorded in the context @{text "\<Gamma>"}, since syntactic types are

   471   always inhabitable.  An assumption'' @{text "x :: \<tau>"} is logically

   472   vacuous, because @{text "\<tau>"} is always non-empty.  This is the deeper

   473   reason why @{text "\<Gamma>"} only consists of hypothetical proofs, but no

   474   hypothetical terms.

   475

   476   The corresponding proof terms are left implicit in the classic

   477   LCF-approach'', although they could be exploited separately

   478   \cite{Berghofer-Nipkow:2000}.  The implementation provides a runtime

   479   option to control the generation of full proof terms.

   480

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

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

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

   484   substitution through derivations inductively, we get admissible

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

   486

   487   \begin{figure}[htb]

   488   \begin{center}

   489   $  490 \infer{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}{@{text "\<Gamma> \<turnstile> B[\<alpha>]"} & @{text "\<alpha> \<notin> \<Gamma>"}}   491 \quad   492 \infer[\quad@{text "(generalize)"}]{@{text "\<Gamma> \<turnstile> B[?x]"}}{@{text "\<Gamma> \<turnstile> B[x]"} & @{text "x \<notin> \<Gamma>"}}   493$

   494   $  495 \infer{@{text "\<Gamma> \<turnstile> B[\<tau>]"}}{@{text "\<Gamma> \<turnstile> B[?\<alpha>]"}}   496 \quad   497 \infer[\quad@{text "(instantiate)"}]{@{text "\<Gamma> \<turnstile> B[t]"}}{@{text "\<Gamma> \<turnstile> B[?x]"}}   498$

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

   500   \end{center}

   501   \end{figure}

   502

   503   Note that @{text "instantiate_term"} could be derived using @{text

   504   "\<And>_intro/elim"}, but this is not how it is implemented.  The type

   505   instantiation rule is a genuine admissible one, due to the lack of

   506   true polymorphism in the logic.

   507

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

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

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

   511   this could disrupt monotonicity of the basic calculus: derivations

   512   could leave the current proof context.

   513

   514   \medskip The framework also provides builtin equality @{text "\<equiv>"},

   515   which is conceptually axiomatized shown in \figref{fig:equality},

   516   although the implementation provides derived rules directly:

   517

   518   \begin{figure}[htb]

   519   \begin{center}

   520   \begin{tabular}{ll}

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

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

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

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

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

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

   527   \end{tabular}

   528   \caption{Conceptual axiomatization of equality.}\label{fig:equality}

   529   \end{center}

   530   \end{figure}

   531

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

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

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

   535

   536

   537   \medskip Conjunction is defined in Pure as a derived connective, see

   538   \figref{fig:conjunction}.  This is occasionally useful to represent

   539   simultaneous statements behind the scenes --- framework conjunction

   540   is usually not exposed to the user.

   541

   542   \begin{figure}[htb]

   543   \begin{center}

   544   \begin{tabular}{ll}

   545   @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} & conjunction (hidden) \\

   546   @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\

   547   \end{tabular}

   548   \caption{Definition of conjunction.}\label{fig:equality}

   549   \end{center}

   550   \end{figure}

   551

   552   The definition allows to derive the usual introduction @{text "\<turnstile> A \<Longrightarrow>

   553   B \<Longrightarrow> A & B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B

   554   \<Longrightarrow> B"}.

   555 *}

   556

   557

   558 section {* Rules \label{sec:rules} *}

   559

   560 text {*

   561

   562 FIXME

   563

   564   A \emph{rule} is any Pure theorem in HHF normal form; there is a

   565   separate calculus for rule composition, which is modeled after

   566   Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows

   567   rules to be nested arbitrarily, similar to \cite{extensions91}.

   568

   569   Normally, all theorems accessible to the user are proper rules.

   570   Low-level inferences are occasional required internally, but the

   571   result should be always presented in canonical form.  The higher

   572   interfaces of Isabelle/Isar will always produce proper rules.  It is

   573   important to maintain this invariant in add-on applications!

   574

   575   There are two main principles of rule composition: @{text

   576   "resolution"} (i.e.\ backchaining of rules) and @{text

   577   "by-assumption"} (i.e.\ closing a branch); both principles are

   578   combined in the variants of @{text "elim-resolution"} and @{text

   579   "dest-resolution"}.  Raw @{text "composition"} is occasionally

   580   useful as well, also it is strictly speaking outside of the proper

   581   rule calculus.

   582

   583   Rules are treated modulo general higher-order unification, which is

   584   unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion

   585   on @{text "\<lambda>"}-terms.  Moreover, propositions are understood modulo

   586   the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.

   587

   588   This means that any operations within the rule calculus may be

   589   subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions.  It is common

   590   practice not to contract or expand unnecessarily.  Some mechanisms

   591   prefer an one form, others the opposite, so there is a potential

   592   danger to produce some oscillation!

   593

   594   Only few operations really work \emph{modulo} HHF conversion, but

   595   expect a normal form: quantifiers @{text "\<And>"} before implications

   596   @{text "\<Longrightarrow>"} at each level of nesting.

   597

   598 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF

   599 format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>

   600 A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.

   601 Any proposition may be put into HHF form by normalizing with the rule

   602 @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost

   603 quantifier prefix is represented via \seeglossary{schematic

   604 variables}, such that the top-level structure is merely that of a

   605 \seeglossary{Horn Clause}}.

   606

   607 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}

   608

   609

   610   $  611 \infer[@{text "(assumption)"}]{@{text "C\<vartheta>"}}   612 {@{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})}}   613$

   614

   615

   616   $  617 \infer[@{text "(compose)"}]{@{text "\<^vec>A\<vartheta> \<Longrightarrow> C\<vartheta>"}}   618 {@{text "\<^vec>A \<Longrightarrow> B"} & @{text "B' \<Longrightarrow> C"} & @{text "B\<vartheta> = B'\<vartheta>"}}   619$

   620

   621

   622   $  623 \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"}}   624$

   625   $  626 \infer[@{text "(\<Longrightarrow>_lift)"}]{@{text "(\<^vec>H \<Longrightarrow> \<^vec>A) \<Longrightarrow> (\<^vec>H \<Longrightarrow> B)"}}{@{text "\<^vec>A \<Longrightarrow> B"}}   627$

   628

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

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

   631

   632   $  633 \infer[@{text "(resolution)"}]   634 {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> \<^vec>A (?\<^vec>a \<^vec>x))\<vartheta> \<Longrightarrow> C\<vartheta>"}}   635 {\begin{tabular}{l}   636 @{text "\<^vec>A ?\<^vec>a \<Longrightarrow> B ?\<^vec>a"} \\   637 @{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> B' \<^vec>x) \<Longrightarrow> C"} \\   638 @{text "(\<lambda>\<^vec>x. B (?\<^vec>a \<^vec>x))\<vartheta> = B'\<vartheta>"} \\   639 \end{tabular}}   640$

   641

   642

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

   644 *}

   645

   646

   647 end