doc-src/IsarImplementation/Thy/logic.thy
 author wenzelm Fri Sep 08 17:33:05 2006 +0200 (2006-09-08) changeset 20493 48fea5e99505 parent 20491 98ba42f19995 child 20494 99ad217b6974 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 "(FIXME)\<kappa>"}.  For @{text "k = 0"}

    74   the argument tuple is omitted, e.g.\ @{text "prop"} instead of

    75   @{text "()prop"}.  For @{text "k = 1"} the parentheses are omitted,

    76   e.g.\ @{text "\<alpha> list"} instead of @{text "(\<alpha>)list"}.  Further

    77   notation is provided for specific constructors, notably

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

    79   \<beta>)fun"} constructor.

    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)c"}.

    84

    85   A \emph{type abbreviation} is a syntactic abbreviation of an

    86   arbitrary type expression of the theory.  Type abbreviations looks

    87   like type constructors at the surface, but are expanded before the

    88   core logic encounters them.

    89

    90   A \emph{type arity} declares the image behavior of a type

    91   constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>,

    92   s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is

    93   of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of

    94   sort @{text "s\<^isub>i"}.  Arity declarations are implicitly

    95   completed, i.e.\ @{text "c :: (\<^vec>s)c"} entails @{text "c ::

    96   (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.

    97

    98   \medskip The sort algebra is always maintained as \emph{coregular},

    99   which means that type arities are consistent with the subclass

   100   relation: for each type constructor @{text "c"} and classes @{text

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

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

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

   104   \<^vec>s\<^isub>2"} holds pointwise for all argument sorts.

   105

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

   107   constraints may be always fulfilled in a most general fashion: for

   108   each type constructor @{text "c"} and sort @{text "s"} there is a

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

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

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

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

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

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

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

   116 *}

   117

   118 text %mlref {*

   119   \begin{mldecls}

   120   @{index_ML_type class} \\

   121   @{index_ML_type sort} \\

   122   @{index_ML_type typ} \\

   123   @{index_ML_type arity} \\

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

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

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

   127   @{index_ML Sign.add_tyabbrs_i: "

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

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

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

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

   132   \end{mldecls}

   133

   134   \begin{description}

   135

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

   137   @{ML_type string}.

   138

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

   140   @{ML_type "class list"}.

   141

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

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

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

   145

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

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

   148

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

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

   151

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

   153   is of a given sort.

   154

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

   156   type constructors @{text "c"} with @{text "k"} arguments and

   157   optional mixfix syntax.

   158

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

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

   161   optional mixfix syntax.

   162

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

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

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

   166

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

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

   169   c\<^isub>2"}.

   170

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

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

   173

   174   \end{description}

   175 *}

   176

   177

   178

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

   180

   181 text {*

   182   \glossary{Term}{FIXME}

   183

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

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

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

   187   usually considered malformed.  The types of variables and constants

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

   189   known performance issue).

   190

   191   FIXME de-Bruijn representation of lambda terms

   192

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

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

   195   thanks to type-inference.

   196

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

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

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

   200 *}

   201

   202

   203 text {*

   204

   205 FIXME

   206

   207 \glossary{Schematic polymorphism}{FIXME}

   208

   209 \glossary{Type variable}{FIXME}

   210

   211 *}

   212

   213

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

   215

   216 text {*

   217

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

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

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

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

   222   corresponding proof terms are left implicit in the classic

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

   224   \cite{Berghofer-Nipkow:2000}.

   225

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

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

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

   229   assumptions and conclusions emerging uniformly as simultaneous

   230   statements.

   231

   232

   233

   234   FIXME

   235

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

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

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

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

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

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

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

   243

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

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

   246 rarely spelled out explicitly.  Theorems are usually normalized

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

   248

   249 \glossary{Fact}{Sometimes used interchangably for

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

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

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

   253 be simultaneous, hence the list representation.}

   254

   255 \glossary{Schematic variable}{FIXME}

   256

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

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

   259 text.}

   260

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

   262

   263 \glossary{Bound variable}{FIXME}

   264

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

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

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

   268 variables is their binding scope.}

   269

   270 *}

   271

   272

   273 section {* Proof terms *}

   274

   275 text {*

   276   FIXME !?

   277 *}

   278

   279

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

   281

   282 text {*

   283

   284 FIXME

   285

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

   287   separate calculus for rule composition, which is modeled after

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

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

   290

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

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

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

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

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

   296

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

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

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

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

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

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

   303   rule calculus.

   304

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

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

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

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

   309

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

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

   312   practice not to contract or expand unnecessarily.  Some mechanisms

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

   314   danger to produce some oscillation!

   315

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

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

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

   319

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

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

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

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

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

   325 quantifier prefix is represented via \seeglossary{schematic

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

   327 \seeglossary{Horn Clause}}.

   328

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

   330

   331 *}

   332

   333 end