doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Tue Sep 12 17:45:58 2006 +0200 (2006-09-12) changeset 20520 05fd007bdeb9 parent 20519 d7ad1217c24a child 20521 189811b39869 permissions -rw-r--r--
tuned;
     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}{A \seeglossary{term} of \seeglossary{type}

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

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

   390   a clear distinction.  Propositions are structured via implication

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

   392   anything else is considered atomic.  The canonical form for

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

   394

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

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

   397   rarely spelled out explicitly.  Theorems are usually normalized

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

   399

   400   \glossary{Fact}{Sometimes used interchangeably for

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

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

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

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

   405

   406   \glossary{Schematic variable}{FIXME}

   407

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

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

   410   proof text. FIXME}

   411

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

   413   variable}. FIXME}

   414

   415   \glossary{Bound variable}{FIXME}

   416

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

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

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

   420   different variables is their binding scope. FIXME}

   421

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

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

   424   basic theory:

   425

   426   \smallskip

   427   \begin{tabular}{ll}

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

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

   430   \end{tabular}

   431

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

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

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

   435   inductively by the primitive inferences given in

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

   437   that the hypotheses may not contain schematic variables.

   438

   439   \begin{figure}[htb]

   440   \begin{center}

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

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

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

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

   457   \end{center}

   458   \end{figure}

   459

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

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

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

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

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

   465   non-dependent one.

   466

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

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

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

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

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

   472   hypothetical terms.

   473

   474   The corresponding proof terms are left implicit in the classic

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

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

   477   option to control the generation of full proof terms.

   478

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

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

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

   482   substitution through derivations inductively, we get admissible

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

   484

   485   \begin{figure}[htb]

   486   \begin{center}

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

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

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

   498   \end{center}

   499   \end{figure}

   500

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

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

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

   504   true polymorphism in the logic.

   505

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

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

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

   509   this could disrupt monotonicity of the basic calculus: derivations

   510   could leave the current proof context.

   511

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

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

   514   although the implementation provides derived rules directly:

   515

   516   \begin{figure}[htb]

   517   \begin{center}

   518   \begin{tabular}{ll}

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

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

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

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

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

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

   525   \end{tabular}

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

   527   \end{center}

   528   \end{figure}

   529

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

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

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

   533

   534

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

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

   537   simultaneous statements behind the scenes --- framework conjunction

   538   is usually not exposed to the user.

   539

   540   \begin{figure}[htb]

   541   \begin{center}

   542   \begin{tabular}{ll}

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

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

   545   \end{tabular}

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

   547   \end{center}

   548   \end{figure}

   549

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

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

   552   \<Longrightarrow> B"}.

   553 *}

   554

   555

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

   557

   558 text {*

   559

   560 FIXME

   561

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

   563   separate calculus for rule composition, which is modeled after

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

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

   566

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

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

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

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

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

   572

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

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

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

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

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

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

   579   rule calculus.

   580

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

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

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

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

   585

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

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

   588   practice not to contract or expand unnecessarily.  Some mechanisms

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

   590   danger to produce some oscillation!

   591

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

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

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

   595

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

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

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

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

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

   601 quantifier prefix is represented via \seeglossary{schematic

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

   603 \seeglossary{Horn Clause}}.

   604

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

   606

   607

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

   612

   613

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

   618

   619

   620   $  621 \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"}}   622$

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

   626

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

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

   629

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

   639

   640

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

   642 *}

   643

   644

   645 end