doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Fri Sep 08 19:44:43 2006 +0200 (2006-09-08) changeset 20494 99ad217b6974 parent 20493 48fea5e99505 child 20498 825a8d2335ce 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} is defined inductively over type variables and type

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

    83   (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)k"}.

    84

    85   A \emph{type abbreviation} is a syntactic abbreviation @{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 componentwise.

   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 fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\

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

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

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

   129   @{index_ML Sign.add_tyabbrs_i: "

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

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

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

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

   134   \end{mldecls}

   135

   136   \begin{description}

   137

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

   139   @{ML_type string}.

   140

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

   142   @{ML_type "class list"}.

   143

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

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

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

   147

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

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

   150

   151   \item @{ML fold_atyps}~@{text "f \<tau>"} iterates function @{text "f"}

   152   over all occurrences of atoms (@{ML TFree} or @{ML TVar}) of @{text

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

   154

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

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

   157

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

   159   is of a given sort.

   160

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

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

   163   optional mixfix syntax.

   164

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

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

   167   optional mixfix syntax.

   168

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

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

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

   172

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

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

   175   c\<^isub>2"}.

   176

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

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

   179

   180   \end{description}

   181 *}

   182

   183

   184

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

   186

   187 text {*

   188   \glossary{Term}{FIXME}

   189

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

   191   with de-Bruijn indices for bound variables, and named free

   192   variables, and constants.  Terms with loose bound variables are

   193   usually considered malformed.  The types of variables and constants

   194   is stored explicitly at each occurrence in the term (which is a

   195   known performance issue).

   196

   197   FIXME de-Bruijn representation of lambda terms

   198

   199   Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}

   200   and application @{text "t u"}, while types are usually implicit

   201   thanks to type-inference.

   202

   203   Terms of type @{text "prop"} are called

   204   propositions.  Logical statements are composed via @{text "\<And>x ::

   205   \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.

   206 *}

   207

   208

   209 text {*

   210

   211 FIXME

   212

   213 \glossary{Schematic polymorphism}{FIXME}

   214

   215 \glossary{Type variable}{FIXME}

   216

   217 *}

   218

   219

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

   221

   222 text {*

   223

   224   Primitive reasoning operates on judgments of the form @{text "\<Gamma> \<turnstile>

   225   \<phi>"}, with standard introduction and elimination rules for @{text

   226   "\<And>"} and @{text "\<Longrightarrow>"} that refer to fixed parameters @{text "x"} and

   227   hypotheses @{text "A"} from the context @{text "\<Gamma>"}.  The

   228   corresponding proof terms are left implicit in the classic

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

   230   \cite{Berghofer-Nipkow:2000}.

   231

   232   The framework also provides definitional equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha>

   233   \<Rightarrow> prop"}, with @{text "\<alpha>\<beta>\<eta>"}-conversion rules.  The internal

   234   conjunction @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} enables the view of

   235   assumptions and conclusions emerging uniformly as simultaneous

   236   statements.

   237

   238

   239

   240   FIXME

   241

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

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

   244 propositions apart from their type, but the concrete syntax enforces a

   245 clear distinction.  Propositions are structured via implication @{text

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

   247 else is considered atomic.  The canonical form for propositions is

   248 that of a \seeglossary{Hereditary Harrop Formula}.}

   249

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

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

   252 rarely spelled out explicitly.  Theorems are usually normalized

   253 according to the \seeglossary{HHF} format.}

   254

   255 \glossary{Fact}{Sometimes used interchangably for

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

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

   258 local assumptions, or as results of local goal statements --- both may

   259 be simultaneous, hence the list representation.}

   260

   261 \glossary{Schematic variable}{FIXME}

   262

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

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

   265 text.}

   266

   267 \glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}

   268

   269 \glossary{Bound variable}{FIXME}

   270

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

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

   273 \seeglossary{type variable}.  The distinguishing feature of different

   274 variables is their binding scope.}

   275

   276 *}

   277

   278

   279 section {* Proof terms *}

   280

   281 text {*

   282   FIXME !?

   283 *}

   284

   285

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

   287

   288 text {*

   289

   290 FIXME

   291

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

   293   separate calculus for rule composition, which is modeled after

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

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

   296

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

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

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

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

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

   302

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

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

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

   306   combined in the variants of @{text "elim-resosultion"} and @{text

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

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

   309   rule calculus.

   310

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

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

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

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

   315

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

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

   318   practice not to contract or expand unnecessarily.  Some mechanisms

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

   320   danger to produce some oscillation!

   321

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

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

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

   325

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

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

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

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

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

   331 quantifier prefix is represented via \seeglossary{schematic

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

   333 \seeglossary{Horn Clause}}.

   334

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

   336

   337 *}

   338

   339 end