doc-src/IsarImplementation/Thy/logic.thy
author wenzelm
Tue Sep 05 22:05:41 2006 +0200 (2006-09-05)
changeset 20480 4e0522d38968
parent 20477 e623b0e30541
child 20491 98ba42f19995
permissions -rw-r--r--
more on types and type classes;
wenzelm@18537
     1
wenzelm@18537
     2
(* $Id$ *)
wenzelm@18537
     3
wenzelm@18537
     4
theory logic imports base begin
wenzelm@18537
     5
wenzelm@20470
     6
chapter {* Primitive logic \label{ch:logic} *}
wenzelm@18537
     7
wenzelm@20480
     8
text {*
wenzelm@20480
     9
  The logical foundations of Isabelle/Isar are that of the Pure logic,
wenzelm@20480
    10
  which has been introduced as a natural-deduction framework in
wenzelm@20480
    11
  \cite{paulson700}.  This is essentially the same logic as ``@{text
wenzelm@20480
    12
  "\<lambda>HOL"}'' in the more abstract framework of Pure Type Systems (PTS)
wenzelm@20480
    13
  \cite{Barendregt-Geuvers:2001}, although there are some key
wenzelm@20480
    14
  differences in the practical treatment of simple types.
wenzelm@20480
    15
wenzelm@20480
    16
  Following type-theoretic parlance, the Pure logic consists of three
wenzelm@20480
    17
  levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text
wenzelm@20480
    18
  "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text
wenzelm@20480
    19
  "\<And>"} for universal quantification (proofs depending on terms), and
wenzelm@20480
    20
  @{text "\<Longrightarrow>"} for implication (proofs depending on proofs).
wenzelm@20480
    21
wenzelm@20480
    22
  Pure derivations are relative to a logical theory, which declares
wenzelm@20480
    23
  type constructors, term constants, and axioms.  Term constants and
wenzelm@20480
    24
  axioms support schematic polymorphism.
wenzelm@20480
    25
*}
wenzelm@20480
    26
wenzelm@20480
    27
wenzelm@20451
    28
section {* Types \label{sec:types} *}
wenzelm@20437
    29
wenzelm@20437
    30
text {*
wenzelm@20480
    31
  The language of types is an uninterpreted order-sorted first-order
wenzelm@20480
    32
  algebra; types are qualified by ordered type classes.
wenzelm@20480
    33
wenzelm@20480
    34
  \medskip A \emph{type class} is an abstract syntactic entity
wenzelm@20480
    35
  declared in the theory context.  The \emph{subclass relation} @{text
wenzelm@20480
    36
  "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic
wenzelm@20480
    37
  generating relation; the transitive closure maintained internally.
wenzelm@20451
    38
wenzelm@20480
    39
  A \emph{sort} is a list of type classes written as @{text
wenzelm@20480
    40
  "{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic
wenzelm@20480
    41
  intersection.  Notationally, the curly braces are omitted for
wenzelm@20480
    42
  singleton intersections, i.e.\ any class @{text "c"} may be read as
wenzelm@20480
    43
  a sort @{text "{c}"}.  The ordering on type classes is extended to
wenzelm@20480
    44
  sorts in the canonical fashion: @{text "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq>
wenzelm@20480
    45
  {d\<^isub>1, \<dots>, d\<^isub>n}"} iff @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq>
wenzelm@20480
    46
  d\<^isub>j"}.  The empty intersection @{text "{}"} refers to the
wenzelm@20480
    47
  universal sort, which is the largest element wrt.\ the sort order.
wenzelm@20480
    48
  The intersections of all (i.e.\ finitely many) classes declared in
wenzelm@20480
    49
  the current theory are the minimal elements wrt.\ sort order.
wenzelm@20480
    50
wenzelm@20480
    51
  \medskip A \emph{fixed type variable} is pair of a basic name
wenzelm@20480
    52
  (starting with @{text "'"} character) and a sort constraint.  For
wenzelm@20480
    53
  example, @{text "('a, s)"} which is usually printed as @{text
wenzelm@20480
    54
  "\<alpha>\<^isub>s"}.  A \emph{schematic type variable} is a pair of an
wenzelm@20480
    55
  indexname and a sort constraint.  For example, @{text "(('a, 0),
wenzelm@20480
    56
  s)"} which is usually printed @{text "?\<alpha>\<^isub>s"}.
wenzelm@20451
    57
wenzelm@20480
    58
  Note that \emph{all} syntactic components contribute to the identity
wenzelm@20480
    59
  of a type variables, including the literal sort constraint.  The
wenzelm@20480
    60
  core logic handles type variables with the same name but different
wenzelm@20480
    61
  sorts as different, even though the outer layers of the system make
wenzelm@20480
    62
  it hard to produce anything like this.
wenzelm@20451
    63
wenzelm@20480
    64
  A \emph{type constructor} is an @{text "k"}-ary type operator
wenzelm@20480
    65
  declared in the theory.
wenzelm@20480
    66
  
wenzelm@20480
    67
  A \emph{type} is defined inductively over type variables and type
wenzelm@20480
    68
  constructors: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s | (\<tau>\<^sub>1, \<dots>,
wenzelm@20480
    69
  \<tau>\<^sub>k)c"}.  Type constructor application is usually written
wenzelm@20480
    70
  postfix.  For @{text "k = 0"} the argument tuple is omitted, e.g.\
wenzelm@20480
    71
  @{text "prop"} instead of @{text "()prop"}.  For @{text "k = 1"} the
wenzelm@20480
    72
  parentheses are omitted, e.g.\ @{text "\<tau> list"} instead of @{text
wenzelm@20480
    73
  "(\<tau>) list"}.  Further notation is provided for specific
wenzelm@20480
    74
  constructors, notably right-associative infix @{text "\<tau>\<^isub>1 \<Rightarrow>
wenzelm@20480
    75
  \<tau>\<^isub>2"} instead of @{text "(\<tau>\<^isub>1, \<tau>\<^isub>2)fun"}
wenzelm@20480
    76
  constructor.
wenzelm@20451
    77
wenzelm@20480
    78
  A \emph{type abbreviation} is a syntactic abbreviation of an
wenzelm@20480
    79
  arbitrary type expression of the theory.  Type abbreviations looks
wenzelm@20480
    80
  like type constructors at the surface, but are expanded before the
wenzelm@20480
    81
  core logic encounters them.
wenzelm@20480
    82
wenzelm@20480
    83
  A \emph{type arity} declares the image behavior of a type
wenzelm@20480
    84
  constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>,
wenzelm@20480
    85
  s\<^isub>n)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is
wenzelm@20480
    86
  of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of
wenzelm@20480
    87
  sort @{text "s\<^isub>i"}.  The sort algebra is always maintained as
wenzelm@20480
    88
  \emph{coregular}, which means that type arities are consistent with
wenzelm@20480
    89
  the subclass relation: for each type constructor @{text "c"} and
wenzelm@20480
    90
  classes @{text "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::
wenzelm@20480
    91
  (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c
wenzelm@20480
    92
  :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
wenzelm@20480
    93
  \<^vec>s\<^isub>2"} holds pointwise for all argument sorts.
wenzelm@20451
    94
wenzelm@20480
    95
  The key property of the order-sorted algebra of types is that sort
wenzelm@20480
    96
  constraints may be always fulfilled in a most general fashion: for
wenzelm@20480
    97
  each type constructor @{text "c"} and sort @{text "s"} there is a
wenzelm@20480
    98
  most general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
wenzelm@20480
    99
  s\<^isub>k)"} such that @{text "(\<tau>\<^bsub>s\<^isub>1\<^esub>, \<dots>,
wenzelm@20480
   100
  \<tau>\<^bsub>s\<^isub>k\<^esub>)"} for arbitrary @{text "\<tau>\<^isub>i"} of
wenzelm@20480
   101
  sort @{text "s\<^isub>i"}.  This means the unification problem on
wenzelm@20480
   102
  the algebra of types has most general solutions (modulo renaming and
wenzelm@20480
   103
  equivalence of sorts).  As a consequence, type-inference is able to
wenzelm@20480
   104
  produce primary types.
wenzelm@20480
   105
*}
wenzelm@20451
   106
wenzelm@20480
   107
text %mlref {*
wenzelm@20480
   108
  \begin{mldecls}
wenzelm@20480
   109
  @{index_ML_type class} \\
wenzelm@20480
   110
  @{index_ML_type sort} \\
wenzelm@20480
   111
  @{index_ML_type typ} \\
wenzelm@20480
   112
  @{index_ML_type arity} \\
wenzelm@20480
   113
  @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
wenzelm@20480
   114
  @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
wenzelm@20480
   115
  @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
wenzelm@20480
   116
  @{index_ML Sign.add_tyabbrs_i: "
wenzelm@20480
   117
  (bstring * string list * typ * mixfix) list -> theory -> theory"} \\
wenzelm@20480
   118
  @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
wenzelm@20480
   119
  @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
wenzelm@20480
   120
  @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
wenzelm@20480
   121
  \end{mldecls}
wenzelm@20480
   122
wenzelm@20480
   123
  \begin{description}
wenzelm@20480
   124
wenzelm@20480
   125
  \item @{ML_type class} represents type classes; this is an alias for
wenzelm@20480
   126
  @{ML_type string}.
wenzelm@20480
   127
wenzelm@20480
   128
  \item @{ML_type sort} represents sorts; this is an alias for
wenzelm@20480
   129
  @{ML_type "class list"}.
wenzelm@20451
   130
wenzelm@20480
   131
  \item @{ML_type arity} represents type arities; this is an alias for
wenzelm@20480
   132
  triples of the form @{text "(c, \<^vec>s, s)"} for @{text "c ::
wenzelm@20480
   133
  (\<^vec>s)s"} described above.
wenzelm@20480
   134
wenzelm@20480
   135
  \item @{ML_type typ} represents types; this is a datatype with
wenzelm@20480
   136
  constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
wenzelm@20480
   137
wenzelm@20480
   138
  \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
wenzelm@20480
   139
  tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
wenzelm@20480
   140
wenzelm@20480
   141
  \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
wenzelm@20480
   142
  expression of of a given sort.
wenzelm@20480
   143
wenzelm@20480
   144
  \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new
wenzelm@20480
   145
  type constructors @{text "c"} with @{text "k"} arguments, and
wenzelm@20480
   146
  optional mixfix syntax.
wenzelm@20451
   147
wenzelm@20480
   148
  \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
wenzelm@20480
   149
  defines type abbreviation @{text "(\<^vec>\<alpha>)c"} (with optional
wenzelm@20480
   150
  mixfix syntax) as @{text "\<tau>"}.
wenzelm@20480
   151
wenzelm@20480
   152
  \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
wenzelm@20480
   153
  c\<^isub>n])"} declares new class @{text "c"} derived together with
wenzelm@20480
   154
  class relations @{text "c \<subseteq> c\<^isub>i"}.
wenzelm@20480
   155
wenzelm@20480
   156
  \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
wenzelm@20480
   157
  c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
wenzelm@20480
   158
  c\<^isub>2"}.
wenzelm@20480
   159
wenzelm@20480
   160
  \item @{ML Sign.primitive_arity}~@{text "(c, \<^vec>s, s)"} declares
wenzelm@20480
   161
  arity @{text "c :: (\<^vec>s)s"}.
wenzelm@20480
   162
wenzelm@20480
   163
  \end{description}
wenzelm@20437
   164
*}
wenzelm@20437
   165
wenzelm@20437
   166
wenzelm@20480
   167
wenzelm@20451
   168
section {* Terms \label{sec:terms} *}
wenzelm@18537
   169
wenzelm@18537
   170
text {*
wenzelm@20451
   171
  \glossary{Term}{FIXME}
wenzelm@18537
   172
wenzelm@20451
   173
  FIXME de-Bruijn representation of lambda terms
wenzelm@20480
   174
wenzelm@20480
   175
  Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}
wenzelm@20480
   176
  and application @{text "t u"}, while types are usually implicit
wenzelm@20480
   177
  thanks to type-inference.
wenzelm@20480
   178
wenzelm@20480
   179
  Terms of type @{text "prop"} are called
wenzelm@20480
   180
  propositions.  Logical statements are composed via @{text "\<And>x ::
wenzelm@20480
   181
  \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.
wenzelm@18537
   182
*}
wenzelm@18537
   183
wenzelm@18537
   184
wenzelm@18537
   185
text {*
wenzelm@18537
   186
wenzelm@18537
   187
FIXME
wenzelm@18537
   188
wenzelm@18537
   189
\glossary{Schematic polymorphism}{FIXME}
wenzelm@18537
   190
wenzelm@18537
   191
\glossary{Type variable}{FIXME}
wenzelm@18537
   192
wenzelm@18537
   193
*}
wenzelm@18537
   194
wenzelm@18537
   195
wenzelm@20477
   196
section {* Proof terms *}
wenzelm@20477
   197
wenzelm@20477
   198
text {*
wenzelm@20477
   199
  FIXME
wenzelm@20477
   200
*}
wenzelm@20477
   201
wenzelm@20477
   202
wenzelm@20451
   203
section {* Theorems \label{sec:thms} *}
wenzelm@18537
   204
wenzelm@18537
   205
text {*
wenzelm@18537
   206
wenzelm@20480
   207
  Primitive reasoning operates on judgments of the form @{text "\<Gamma> \<turnstile>
wenzelm@20480
   208
  \<phi>"}, with standard introduction and elimination rules for @{text
wenzelm@20480
   209
  "\<And>"} and @{text "\<Longrightarrow>"} that refer to fixed parameters @{text "x"} and
wenzelm@20480
   210
  hypotheses @{text "A"} from the context @{text "\<Gamma>"}.  The
wenzelm@20480
   211
  corresponding proof terms are left implicit in the classic
wenzelm@20480
   212
  ``LCF-approach'', although they could be exploited separately
wenzelm@20480
   213
  \cite{Berghofer-Nipkow:2000}.
wenzelm@20480
   214
wenzelm@20480
   215
  The framework also provides definitional equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha>
wenzelm@20480
   216
  \<Rightarrow> prop"}, with @{text "\<alpha>\<beta>\<eta>"}-conversion rules.  The internal
wenzelm@20480
   217
  conjunction @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} enables the view of
wenzelm@20480
   218
  assumptions and conclusions emerging uniformly as simultaneous
wenzelm@20480
   219
  statements.
wenzelm@20480
   220
wenzelm@20480
   221
wenzelm@20480
   222
wenzelm@18537
   223
  FIXME
wenzelm@18537
   224
wenzelm@18537
   225
\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
wenzelm@18537
   226
@{text "prop"}.  Internally, there is nothing special about
wenzelm@18537
   227
propositions apart from their type, but the concrete syntax enforces a
wenzelm@18537
   228
clear distinction.  Propositions are structured via implication @{text
wenzelm@18537
   229
"A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
wenzelm@18537
   230
else is considered atomic.  The canonical form for propositions is
wenzelm@18537
   231
that of a \seeglossary{Hereditary Harrop Formula}.}
wenzelm@18537
   232
wenzelm@18537
   233
\glossary{Theorem}{A proven proposition within a certain theory and
wenzelm@18537
   234
proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
wenzelm@18537
   235
rarely spelled out explicitly.  Theorems are usually normalized
wenzelm@18537
   236
according to the \seeglossary{HHF} format.}
wenzelm@18537
   237
wenzelm@18537
   238
\glossary{Fact}{Sometimes used interchangably for
wenzelm@18537
   239
\seeglossary{theorem}.  Strictly speaking, a list of theorems,
wenzelm@18537
   240
essentially an extra-logical conjunction.  Facts emerge either as
wenzelm@18537
   241
local assumptions, or as results of local goal statements --- both may
wenzelm@18537
   242
be simultaneous, hence the list representation.}
wenzelm@18537
   243
wenzelm@18537
   244
\glossary{Schematic variable}{FIXME}
wenzelm@18537
   245
wenzelm@18537
   246
\glossary{Fixed variable}{A variable that is bound within a certain
wenzelm@18537
   247
proof context; an arbitrary-but-fixed entity within a portion of proof
wenzelm@18537
   248
text.}
wenzelm@18537
   249
wenzelm@18537
   250
\glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
wenzelm@18537
   251
wenzelm@18537
   252
\glossary{Bound variable}{FIXME}
wenzelm@18537
   253
wenzelm@18537
   254
\glossary{Variable}{See \seeglossary{schematic variable},
wenzelm@18537
   255
\seeglossary{fixed variable}, \seeglossary{bound variable}, or
wenzelm@18537
   256
\seeglossary{type variable}.  The distinguishing feature of different
wenzelm@18537
   257
variables is their binding scope.}
wenzelm@18537
   258
wenzelm@18537
   259
*}
wenzelm@18537
   260
wenzelm@18537
   261
subsection {* Primitive inferences *}
wenzelm@18537
   262
wenzelm@18537
   263
text FIXME
wenzelm@18537
   264
wenzelm@20480
   265
wenzelm@18537
   266
subsection {* Higher-order resolution *}
wenzelm@18537
   267
wenzelm@18537
   268
text {*
wenzelm@18537
   269
wenzelm@18537
   270
FIXME
wenzelm@18537
   271
wenzelm@18537
   272
\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
wenzelm@18537
   273
format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
wenzelm@18537
   274
A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
wenzelm@18537
   275
Any proposition may be put into HHF form by normalizing with the rule
wenzelm@18537
   276
@{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
wenzelm@18537
   277
quantifier prefix is represented via \seeglossary{schematic
wenzelm@18537
   278
variables}, such that the top-level structure is merely that of a
wenzelm@18537
   279
\seeglossary{Horn Clause}}.
wenzelm@18537
   280
wenzelm@18537
   281
\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
wenzelm@18537
   282
wenzelm@18537
   283
*}
wenzelm@18537
   284
wenzelm@18537
   285
subsection {* Equational reasoning *}
wenzelm@18537
   286
wenzelm@18537
   287
text FIXME
wenzelm@18537
   288
wenzelm@18537
   289
wenzelm@18537
   290
end