doc-src/IsarImplementation/Thy/logic.thy
author wenzelm
Fri, 08 Sep 2006 19:44:43 +0200
changeset 20494 99ad217b6974
parent 20493 48fea5e99505
child 20498 825a8d2335ce
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     1
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     2
(* $Id$ *)
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     3
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     4
theory logic imports base begin
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     5
20470
c839b38a1f32 more on variables;
wenzelm
parents: 20451
diff changeset
     6
chapter {* Primitive logic \label{ch:logic} *}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     7
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
     8
text {*
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
     9
  The logical foundations of Isabelle/Isar are that of the Pure logic,
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    10
  which has been introduced as a natural-deduction framework in
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    11
  \cite{paulson700}.  This is essentially the same logic as ``@{text
20493
wenzelm
parents: 20491
diff changeset
    12
  "\<lambda>HOL"}'' in the more abstract setting of Pure Type Systems (PTS)
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    13
  \cite{Barendregt-Geuvers:2001}, although there are some key
20491
wenzelm
parents: 20480
diff changeset
    14
  differences in the specific treatment of simple types in
wenzelm
parents: 20480
diff changeset
    15
  Isabelle/Pure.
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    16
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    17
  Following type-theoretic parlance, the Pure logic consists of three
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    18
  levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    19
  "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    20
  "\<And>"} for universal quantification (proofs depending on terms), and
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    21
  @{text "\<Longrightarrow>"} for implication (proofs depending on proofs).
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    22
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    23
  Pure derivations are relative to a logical theory, which declares
20491
wenzelm
parents: 20480
diff changeset
    24
  type constructors, term constants, and axioms.  Theory declarations
wenzelm
parents: 20480
diff changeset
    25
  support schematic polymorphism, which is strictly speaking outside
wenzelm
parents: 20480
diff changeset
    26
  the logic.\footnote{Incidently, this is the main logical reason, why
wenzelm
parents: 20480
diff changeset
    27
  the theory context @{text "\<Theta>"} is separate from the context @{text
wenzelm
parents: 20480
diff changeset
    28
  "\<Gamma>"} of the core calculus.}
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    29
*}
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    30
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    31
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    32
section {* Types \label{sec:types} *}
20437
wenzelm
parents: 18537
diff changeset
    33
wenzelm
parents: 18537
diff changeset
    34
text {*
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    35
  The language of types is an uninterpreted order-sorted first-order
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    36
  algebra; types are qualified by ordered type classes.
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    37
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    38
  \medskip A \emph{type class} is an abstract syntactic entity
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    39
  declared in the theory context.  The \emph{subclass relation} @{text
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    40
  "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic
20491
wenzelm
parents: 20480
diff changeset
    41
  generating relation; the transitive closure is maintained
wenzelm
parents: 20480
diff changeset
    42
  internally.  The resulting relation is an ordering: reflexive,
wenzelm
parents: 20480
diff changeset
    43
  transitive, and antisymmetric.
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    44
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    45
  A \emph{sort} is a list of type classes written as @{text
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    46
  "{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    47
  intersection.  Notationally, the curly braces are omitted for
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    48
  singleton intersections, i.e.\ any class @{text "c"} may be read as
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    49
  a sort @{text "{c}"}.  The ordering on type classes is extended to
20491
wenzelm
parents: 20480
diff changeset
    50
  sorts according to the meaning of intersections: @{text
wenzelm
parents: 20480
diff changeset
    51
  "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff
wenzelm
parents: 20480
diff changeset
    52
  @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}.  The empty intersection
wenzelm
parents: 20480
diff changeset
    53
  @{text "{}"} refers to the universal sort, which is the largest
wenzelm
parents: 20480
diff changeset
    54
  element wrt.\ the sort order.  The intersections of all (finitely
wenzelm
parents: 20480
diff changeset
    55
  many) classes declared in the current theory are the minimal
wenzelm
parents: 20480
diff changeset
    56
  elements wrt.\ the sort order.
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    57
20491
wenzelm
parents: 20480
diff changeset
    58
  \medskip A \emph{fixed type variable} is a pair of a basic name
20493
wenzelm
parents: 20491
diff changeset
    59
  (starting with a @{text "'"} character) and a sort constraint.  For
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    60
  example, @{text "('a, s)"} which is usually printed as @{text
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    61
  "\<alpha>\<^isub>s"}.  A \emph{schematic type variable} is a pair of an
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    62
  indexname and a sort constraint.  For example, @{text "(('a, 0),
20491
wenzelm
parents: 20480
diff changeset
    63
  s)"} which is usually printed as @{text "?\<alpha>\<^isub>s"}.
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    64
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    65
  Note that \emph{all} syntactic components contribute to the identity
20493
wenzelm
parents: 20491
diff changeset
    66
  of type variables, including the sort constraint.  The core logic
wenzelm
parents: 20491
diff changeset
    67
  handles type variables with the same name but different sorts as
wenzelm
parents: 20491
diff changeset
    68
  different, although some outer layers of the system make it hard to
wenzelm
parents: 20491
diff changeset
    69
  produce anything like this.
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    70
20493
wenzelm
parents: 20491
diff changeset
    71
  A \emph{type constructor} @{text "\<kappa>"} is a @{text "k"}-ary operator
wenzelm
parents: 20491
diff changeset
    72
  on types declared in the theory.  Type constructor application is
20494
wenzelm
parents: 20493
diff changeset
    73
  usually written postfix as @{text "(\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>k)\<kappa>"}.
wenzelm
parents: 20493
diff changeset
    74
  For @{text "k = 0"} the argument tuple is omitted, e.g.\ @{text
wenzelm
parents: 20493
diff changeset
    75
  "prop"} instead of @{text "()prop"}.  For @{text "k = 1"} the
wenzelm
parents: 20493
diff changeset
    76
  parentheses are omitted, e.g.\ @{text "\<alpha> list"} instead of @{text
wenzelm
parents: 20493
diff changeset
    77
  "(\<alpha>)list"}.  Further notation is provided for specific constructors,
wenzelm
parents: 20493
diff changeset
    78
  notably the right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"} instead of
wenzelm
parents: 20493
diff changeset
    79
  @{text "(\<alpha>, \<beta>)fun"}.
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    80
  
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    81
  A \emph{type} is defined inductively over type variables and type
20491
wenzelm
parents: 20480
diff changeset
    82
  constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
20494
wenzelm
parents: 20493
diff changeset
    83
  (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)k"}.
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
    84
20494
wenzelm
parents: 20493
diff changeset
    85
  A \emph{type abbreviation} is a syntactic abbreviation @{text
wenzelm
parents: 20493
diff changeset
    86
  "(\<^vec>\<alpha>)\<kappa> = \<tau>"} of an arbitrary type expression @{text "\<tau>"} over
wenzelm
parents: 20493
diff changeset
    87
  variables @{text "\<^vec>\<alpha>"}.  Type abbreviations looks like type
wenzelm
parents: 20493
diff changeset
    88
  constructors at the surface, but are fully expanded before entering
wenzelm
parents: 20493
diff changeset
    89
  the logical core.
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    90
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
    91
  A \emph{type arity} declares the image behavior of a type
20494
wenzelm
parents: 20493
diff changeset
    92
  constructor wrt.\ the algebra of sorts: @{text "\<kappa> :: (s\<^isub>1, \<dots>,
wenzelm
parents: 20493
diff changeset
    93
  s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)\<kappa>"} is
wenzelm
parents: 20493
diff changeset
    94
  of sort @{text "s"} if every argument type @{text "\<tau>\<^isub>i"} is
wenzelm
parents: 20493
diff changeset
    95
  of sort @{text "s\<^isub>i"}.  Arity declarations are implicitly
wenzelm
parents: 20493
diff changeset
    96
  completed, i.e.\ @{text "\<kappa> :: (\<^vec>s)c"} entails @{text "\<kappa> ::
20491
wenzelm
parents: 20480
diff changeset
    97
  (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
wenzelm
parents: 20480
diff changeset
    98
wenzelm
parents: 20480
diff changeset
    99
  \medskip The sort algebra is always maintained as \emph{coregular},
wenzelm
parents: 20480
diff changeset
   100
  which means that type arities are consistent with the subclass
20494
wenzelm
parents: 20493
diff changeset
   101
  relation: for each type constructor @{text "\<kappa>"} and classes @{text
wenzelm
parents: 20493
diff changeset
   102
  "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "\<kappa> ::
wenzelm
parents: 20493
diff changeset
   103
  (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "\<kappa>
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   104
  :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
20494
wenzelm
parents: 20493
diff changeset
   105
  \<^vec>s\<^isub>2"} holds componentwise.
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   106
20491
wenzelm
parents: 20480
diff changeset
   107
  The key property of a coregular order-sorted algebra is that sort
20494
wenzelm
parents: 20493
diff changeset
   108
  constraints may be always solved in a most general fashion: for each
wenzelm
parents: 20493
diff changeset
   109
  type constructor @{text "\<kappa>"} and sort @{text "s"} there is a most
wenzelm
parents: 20493
diff changeset
   110
  general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
20491
wenzelm
parents: 20480
diff changeset
   111
  s\<^isub>k)"} such that a type scheme @{text
20494
wenzelm
parents: 20493
diff changeset
   112
  "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)\<kappa>"} is
20491
wenzelm
parents: 20480
diff changeset
   113
  of sort @{text "s"}.  Consequently, the unification problem on the
wenzelm
parents: 20480
diff changeset
   114
  algebra of types has most general solutions (modulo renaming and
wenzelm
parents: 20480
diff changeset
   115
  equivalence of sorts).  Moreover, the usual type-inference algorithm
wenzelm
parents: 20480
diff changeset
   116
  will produce primary types as expected \cite{nipkow-prehofer}.
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   117
*}
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   118
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   119
text %mlref {*
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   120
  \begin{mldecls}
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   121
  @{index_ML_type class} \\
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   122
  @{index_ML_type sort} \\
20494
wenzelm
parents: 20493
diff changeset
   123
  @{index_ML_type arity} \\
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   124
  @{index_ML_type typ} \\
20494
wenzelm
parents: 20493
diff changeset
   125
  @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   126
  @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   127
  @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   128
  @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   129
  @{index_ML Sign.add_tyabbrs_i: "
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   130
  (bstring * string list * typ * mixfix) list -> theory -> theory"} \\
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   131
  @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   132
  @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   133
  @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   134
  \end{mldecls}
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   135
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   136
  \begin{description}
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   137
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   138
  \item @{ML_type class} represents type classes; this is an alias for
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   139
  @{ML_type string}.
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   140
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   141
  \item @{ML_type sort} represents sorts; this is an alias for
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   142
  @{ML_type "class list"}.
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   143
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   144
  \item @{ML_type arity} represents type arities; this is an alias for
20494
wenzelm
parents: 20493
diff changeset
   145
  triples of the form @{text "(\<kappa>, \<^vec>s, s)"} for @{text "\<kappa> ::
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   146
  (\<^vec>s)s"} described above.
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   147
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   148
  \item @{ML_type typ} represents types; this is a datatype with
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   149
  constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   150
20494
wenzelm
parents: 20493
diff changeset
   151
  \item @{ML fold_atyps}~@{text "f \<tau>"} iterates function @{text "f"}
wenzelm
parents: 20493
diff changeset
   152
  over all occurrences of atoms (@{ML TFree} or @{ML TVar}) of @{text
wenzelm
parents: 20493
diff changeset
   153
  "\<tau>"}; the type structure is traversed from left to right.
wenzelm
parents: 20493
diff changeset
   154
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   155
  \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   156
  tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   157
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   158
  \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
20491
wenzelm
parents: 20480
diff changeset
   159
  is of a given sort.
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   160
20494
wenzelm
parents: 20493
diff changeset
   161
  \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares new
wenzelm
parents: 20493
diff changeset
   162
  type constructors @{text "\<kappa>"} with @{text "k"} arguments and
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   163
  optional mixfix syntax.
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   164
20494
wenzelm
parents: 20493
diff changeset
   165
  \item @{ML Sign.add_tyabbrs_i}~@{text "[(\<kappa>, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
wenzelm
parents: 20493
diff changeset
   166
  defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"} with
20491
wenzelm
parents: 20480
diff changeset
   167
  optional mixfix syntax.
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   168
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   169
  \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
20494
wenzelm
parents: 20493
diff changeset
   170
  c\<^isub>n])"} declares new class @{text "c"}, together with class
wenzelm
parents: 20493
diff changeset
   171
  relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   172
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   173
  \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   174
  c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   175
  c\<^isub>2"}.
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   176
20494
wenzelm
parents: 20493
diff changeset
   177
  \item @{ML Sign.primitive_arity}~@{text "(\<kappa>, \<^vec>s, s)"} declares
wenzelm
parents: 20493
diff changeset
   178
  arity @{text "\<kappa> :: (\<^vec>s)s"}.
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   179
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   180
  \end{description}
20437
wenzelm
parents: 18537
diff changeset
   181
*}
wenzelm
parents: 18537
diff changeset
   182
wenzelm
parents: 18537
diff changeset
   183
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   184
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   185
section {* Terms \label{sec:terms} *}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   186
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   187
text {*
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   188
  \glossary{Term}{FIXME}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   189
20491
wenzelm
parents: 20480
diff changeset
   190
  The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
wenzelm
parents: 20480
diff changeset
   191
  with de-Bruijn indices for bound variables, and named free
wenzelm
parents: 20480
diff changeset
   192
  variables, and constants.  Terms with loose bound variables are
wenzelm
parents: 20480
diff changeset
   193
  usually considered malformed.  The types of variables and constants
wenzelm
parents: 20480
diff changeset
   194
  is stored explicitly at each occurrence in the term (which is a
wenzelm
parents: 20480
diff changeset
   195
  known performance issue).
wenzelm
parents: 20480
diff changeset
   196
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   197
  FIXME de-Bruijn representation of lambda terms
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   198
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   199
  Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   200
  and application @{text "t u"}, while types are usually implicit
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   201
  thanks to type-inference.
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   202
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   203
  Terms of type @{text "prop"} are called
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   204
  propositions.  Logical statements are composed via @{text "\<And>x ::
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   205
  \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   206
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   207
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   208
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   209
text {*
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   210
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   211
FIXME
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   212
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   213
\glossary{Schematic polymorphism}{FIXME}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   214
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   215
\glossary{Type variable}{FIXME}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   216
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   217
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   218
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   219
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20450
diff changeset
   220
section {* Theorems \label{sec:thms} *}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   221
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   222
text {*
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   223
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   224
  Primitive reasoning operates on judgments of the form @{text "\<Gamma> \<turnstile>
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   225
  \<phi>"}, with standard introduction and elimination rules for @{text
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   226
  "\<And>"} and @{text "\<Longrightarrow>"} that refer to fixed parameters @{text "x"} and
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   227
  hypotheses @{text "A"} from the context @{text "\<Gamma>"}.  The
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   228
  corresponding proof terms are left implicit in the classic
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   229
  ``LCF-approach'', although they could be exploited separately
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   230
  \cite{Berghofer-Nipkow:2000}.
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   231
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   232
  The framework also provides definitional equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha>
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   233
  \<Rightarrow> prop"}, with @{text "\<alpha>\<beta>\<eta>"}-conversion rules.  The internal
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   234
  conjunction @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} enables the view of
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   235
  assumptions and conclusions emerging uniformly as simultaneous
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   236
  statements.
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   237
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   238
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   239
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   240
  FIXME
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   241
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   242
\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   243
@{text "prop"}.  Internally, there is nothing special about
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   244
propositions apart from their type, but the concrete syntax enforces a
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   245
clear distinction.  Propositions are structured via implication @{text
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   246
"A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} --- anything
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   247
else is considered atomic.  The canonical form for propositions is
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   248
that of a \seeglossary{Hereditary Harrop Formula}.}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   249
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   250
\glossary{Theorem}{A proven proposition within a certain theory and
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   251
proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   252
rarely spelled out explicitly.  Theorems are usually normalized
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   253
according to the \seeglossary{HHF} format.}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   254
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   255
\glossary{Fact}{Sometimes used interchangably for
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   256
\seeglossary{theorem}.  Strictly speaking, a list of theorems,
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   257
essentially an extra-logical conjunction.  Facts emerge either as
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   258
local assumptions, or as results of local goal statements --- both may
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   259
be simultaneous, hence the list representation.}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   260
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   261
\glossary{Schematic variable}{FIXME}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   262
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   263
\glossary{Fixed variable}{A variable that is bound within a certain
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   264
proof context; an arbitrary-but-fixed entity within a portion of proof
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   265
text.}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   266
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   267
\glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   268
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   269
\glossary{Bound variable}{FIXME}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   270
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   271
\glossary{Variable}{See \seeglossary{schematic variable},
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   272
\seeglossary{fixed variable}, \seeglossary{bound variable}, or
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   273
\seeglossary{type variable}.  The distinguishing feature of different
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   274
variables is their binding scope.}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   275
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   276
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   277
20491
wenzelm
parents: 20480
diff changeset
   278
wenzelm
parents: 20480
diff changeset
   279
section {* Proof terms *}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   280
20491
wenzelm
parents: 20480
diff changeset
   281
text {*
wenzelm
parents: 20480
diff changeset
   282
  FIXME !?
wenzelm
parents: 20480
diff changeset
   283
*}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   284
20480
4e0522d38968 more on types and type classes;
wenzelm
parents: 20477
diff changeset
   285
20491
wenzelm
parents: 20480
diff changeset
   286
section {* Rules \label{sec:rules} *}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   287
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   288
text {*
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   289
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   290
FIXME
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   291
20491
wenzelm
parents: 20480
diff changeset
   292
  A \emph{rule} is any Pure theorem in HHF normal form; there is a
wenzelm
parents: 20480
diff changeset
   293
  separate calculus for rule composition, which is modeled after
wenzelm
parents: 20480
diff changeset
   294
  Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows
wenzelm
parents: 20480
diff changeset
   295
  rules to be nested arbitrarily, similar to \cite{extensions91}.
wenzelm
parents: 20480
diff changeset
   296
wenzelm
parents: 20480
diff changeset
   297
  Normally, all theorems accessible to the user are proper rules.
wenzelm
parents: 20480
diff changeset
   298
  Low-level inferences are occasional required internally, but the
wenzelm
parents: 20480
diff changeset
   299
  result should be always presented in canonical form.  The higher
wenzelm
parents: 20480
diff changeset
   300
  interfaces of Isabelle/Isar will always produce proper rules.  It is
wenzelm
parents: 20480
diff changeset
   301
  important to maintain this invariant in add-on applications!
wenzelm
parents: 20480
diff changeset
   302
wenzelm
parents: 20480
diff changeset
   303
  There are two main principles of rule composition: @{text
wenzelm
parents: 20480
diff changeset
   304
  "resolution"} (i.e.\ backchaining of rules) and @{text
wenzelm
parents: 20480
diff changeset
   305
  "by-assumption"} (i.e.\ closing a branch); both principles are
wenzelm
parents: 20480
diff changeset
   306
  combined in the variants of @{text "elim-resosultion"} and @{text
wenzelm
parents: 20480
diff changeset
   307
  "dest-resolution"}.  Raw @{text "composition"} is occasionally
wenzelm
parents: 20480
diff changeset
   308
  useful as well, also it is strictly speaking outside of the proper
wenzelm
parents: 20480
diff changeset
   309
  rule calculus.
wenzelm
parents: 20480
diff changeset
   310
wenzelm
parents: 20480
diff changeset
   311
  Rules are treated modulo general higher-order unification, which is
wenzelm
parents: 20480
diff changeset
   312
  unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion
wenzelm
parents: 20480
diff changeset
   313
  on @{text "\<lambda>"}-terms.  Moreover, propositions are understood modulo
wenzelm
parents: 20480
diff changeset
   314
  the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.
wenzelm
parents: 20480
diff changeset
   315
wenzelm
parents: 20480
diff changeset
   316
  This means that any operations within the rule calculus may be
wenzelm
parents: 20480
diff changeset
   317
  subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions.  It is common
wenzelm
parents: 20480
diff changeset
   318
  practice not to contract or expand unnecessarily.  Some mechanisms
wenzelm
parents: 20480
diff changeset
   319
  prefer an one form, others the opposite, so there is a potential
wenzelm
parents: 20480
diff changeset
   320
  danger to produce some oscillation!
wenzelm
parents: 20480
diff changeset
   321
wenzelm
parents: 20480
diff changeset
   322
  Only few operations really work \emph{modulo} HHF conversion, but
wenzelm
parents: 20480
diff changeset
   323
  expect a normal form: quantifiers @{text "\<And>"} before implications
wenzelm
parents: 20480
diff changeset
   324
  @{text "\<Longrightarrow>"} at each level of nesting.
wenzelm
parents: 20480
diff changeset
   325
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   326
\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   327
format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   328
A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   329
Any proposition may be put into HHF form by normalizing with the rule
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   330
@{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.  In Isabelle, the outermost
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   331
quantifier prefix is represented via \seeglossary{schematic
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   332
variables}, such that the top-level structure is merely that of a
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   333
\seeglossary{Horn Clause}}.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   334
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   335
\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   336
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   337
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   338
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   339
end