doc-src/IsarImplementation/Thy/logic.thy
 changeset 20491 98ba42f19995 parent 20480 4e0522d38968 child 20493 48fea5e99505
1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Sep 07 15:16:51 2006 +0200
1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Sep 07 20:12:08 2006 +0200
1.3 @@ -11,7 +11,8 @@
1.4    \cite{paulson700}.  This is essentially the same logic as @{text
1.5    "\<lambda>HOL"}'' in the more abstract framework of Pure Type Systems (PTS)
1.6    \cite{Barendregt-Geuvers:2001}, although there are some key
1.7 -  differences in the practical treatment of simple types.
1.8 +  differences in the specific treatment of simple types in
1.9 +  Isabelle/Pure.
1.11    Following type-theoretic parlance, the Pure logic consists of three
1.12    levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text
1.13 @@ -20,8 +21,11 @@
1.14    @{text "\<Longrightarrow>"} for implication (proofs depending on proofs).
1.16    Pure derivations are relative to a logical theory, which declares
1.17 -  type constructors, term constants, and axioms.  Term constants and
1.18 -  axioms support schematic polymorphism.
1.19 +  type constructors, term constants, and axioms.  Theory declarations
1.20 +  support schematic polymorphism, which is strictly speaking outside
1.21 +  the logic.\footnote{Incidently, this is the main logical reason, why
1.22 +  the theory context @{text "\<Theta>"} is separate from the context @{text
1.23 +  "\<Gamma>"} of the core calculus.}
1.24  *}
1.27 @@ -34,46 +38,48 @@
1.28    \medskip A \emph{type class} is an abstract syntactic entity
1.29    declared in the theory context.  The \emph{subclass relation} @{text
1.30    "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic
1.31 -  generating relation; the transitive closure maintained internally.
1.32 +  generating relation; the transitive closure is maintained
1.33 +  internally.  The resulting relation is an ordering: reflexive,
1.34 +  transitive, and antisymmetric.
1.36    A \emph{sort} is a list of type classes written as @{text
1.37    "{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic
1.38    intersection.  Notationally, the curly braces are omitted for
1.39    singleton intersections, i.e.\ any class @{text "c"} may be read as
1.40    a sort @{text "{c}"}.  The ordering on type classes is extended to
1.41 -  sorts in the canonical fashion: @{text "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq>
1.42 -  {d\<^isub>1, \<dots>, d\<^isub>n}"} iff @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq>
1.43 -  d\<^isub>j"}.  The empty intersection @{text "{}"} refers to the
1.44 -  universal sort, which is the largest element wrt.\ the sort order.
1.45 -  The intersections of all (i.e.\ finitely many) classes declared in
1.46 -  the current theory are the minimal elements wrt.\ sort order.
1.47 +  sorts according to the meaning of intersections: @{text
1.48 +  "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq> {d\<^isub>1, \<dots>, d\<^isub>n}"} iff
1.49 +  @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq> d\<^isub>j"}.  The empty intersection
1.50 +  @{text "{}"} refers to the universal sort, which is the largest
1.51 +  element wrt.\ the sort order.  The intersections of all (finitely
1.52 +  many) classes declared in the current theory are the minimal
1.53 +  elements wrt.\ the sort order.
1.55 -  \medskip A \emph{fixed type variable} is pair of a basic name
1.56 +  \medskip A \emph{fixed type variable} is a pair of a basic name
1.57    (starting with @{text "'"} character) and a sort constraint.  For
1.58    example, @{text "('a, s)"} which is usually printed as @{text
1.59    "\<alpha>\<^isub>s"}.  A \emph{schematic type variable} is a pair of an
1.60    indexname and a sort constraint.  For example, @{text "(('a, 0),
1.61 -  s)"} which is usually printed @{text "?\<alpha>\<^isub>s"}.
1.62 +  s)"} which is usually printed as @{text "?\<alpha>\<^isub>s"}.
1.64    Note that \emph{all} syntactic components contribute to the identity
1.65 -  of a type variables, including the literal sort constraint.  The
1.66 -  core logic handles type variables with the same name but different
1.67 -  sorts as different, even though the outer layers of the system make
1.68 -  it hard to produce anything like this.
1.69 +  of type variables, including the literal sort constraint.  The core
1.70 +  logic handles type variables with the same name but different sorts
1.71 +  as different, although some outer layers of the system make it hard
1.72 +  to produce anything like this.
1.74 -  A \emph{type constructor} is an @{text "k"}-ary type operator
1.75 -  declared in the theory.
1.76 +  A \emph{type constructor} is a @{text "k"}-ary operator on types
1.77 +  declared in the theory.  Type constructor application is usually
1.78 +  written postfix.  For @{text "k = 0"} the argument tuple is omitted,
1.79 +  e.g.\ @{text "prop"} instead of @{text "()prop"}.  For @{text "k =
1.80 +  1"} the parentheses are omitted, e.g.\ @{text "\<alpha> list"} instead of
1.81 +  @{text "(\<alpha>)list"}.  Further notation is provided for specific
1.82 +  constructors, notably right-associative infix @{text "\<alpha> \<Rightarrow> \<beta>"}
1.83 +  instead of @{text "(\<alpha>, \<beta>)fun"} constructor.
1.85    A \emph{type} is defined inductively over type variables and type
1.86 -  constructors: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s | (\<tau>\<^sub>1, \<dots>,
1.87 -  \<tau>\<^sub>k)c"}.  Type constructor application is usually written
1.88 -  postfix.  For @{text "k = 0"} the argument tuple is omitted, e.g.\
1.89 -  @{text "prop"} instead of @{text "()prop"}.  For @{text "k = 1"} the
1.90 -  parentheses are omitted, e.g.\ @{text "\<tau> list"} instead of @{text
1.91 -  "(\<tau>) list"}.  Further notation is provided for specific
1.92 -  constructors, notably right-associative infix @{text "\<tau>\<^isub>1 \<Rightarrow>
1.93 -  \<tau>\<^isub>2"} instead of @{text "(\<tau>\<^isub>1, \<tau>\<^isub>2)fun"}
1.94 -  constructor.
1.95 +  constructors as follows: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s |
1.96 +  (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)c"}.
1.98    A \emph{type abbreviation} is a syntactic abbreviation of an
1.99    arbitrary type expression of the theory.  Type abbreviations looks
1.100 @@ -82,26 +88,30 @@
1.102    A \emph{type arity} declares the image behavior of a type
1.103    constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>,
1.104 -  s\<^isub>n)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is
1.105 +  s\<^isub>k)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is
1.106    of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of
1.107 -  sort @{text "s\<^isub>i"}.  The sort algebra is always maintained as
1.108 -  \emph{coregular}, which means that type arities are consistent with
1.109 -  the subclass relation: for each type constructor @{text "c"} and
1.110 -  classes @{text "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::
1.111 +  sort @{text "s\<^isub>i"}.  Arity declarations are implicitly
1.112 +  completed, i.e.\ @{text "c :: (\<^vec>s)c"} entails @{text "c ::
1.113 +  (\<^vec>s)c'"} for any @{text "c' \<supseteq> c"}.
1.115 +  \medskip The sort algebra is always maintained as \emph{coregular},
1.116 +  which means that type arities are consistent with the subclass
1.117 +  relation: for each type constructor @{text "c"} and classes @{text
1.118 +  "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::
1.119    (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c
1.120    :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
1.121    \<^vec>s\<^isub>2"} holds pointwise for all argument sorts.
1.123 -  The key property of the order-sorted algebra of types is that sort
1.124 +  The key property of a coregular order-sorted algebra is that sort
1.125    constraints may be always fulfilled in a most general fashion: for
1.126    each type constructor @{text "c"} and sort @{text "s"} there is a
1.127    most general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
1.128 -  s\<^isub>k)"} such that @{text "(\<tau>\<^bsub>s\<^isub>1\<^esub>, \<dots>,
1.129 -  \<tau>\<^bsub>s\<^isub>k\<^esub>)"} for arbitrary @{text "\<tau>\<^isub>i"} of
1.130 -  sort @{text "s\<^isub>i"}.  This means the unification problem on
1.131 -  the algebra of types has most general solutions (modulo renaming and
1.132 -  equivalence of sorts).  As a consequence, type-inference is able to
1.133 -  produce primary types.
1.134 +  s\<^isub>k)"} such that a type scheme @{text
1.135 +  "(\<alpha>\<^bsub>s\<^isub>1\<^esub>, \<dots>, \<alpha>\<^bsub>s\<^isub>k\<^esub>)c"} is
1.136 +  of sort @{text "s"}.  Consequently, the unification problem on the
1.137 +  algebra of types has most general solutions (modulo renaming and
1.138 +  equivalence of sorts).  Moreover, the usual type-inference algorithm
1.139 +  will produce primary types as expected \cite{nipkow-prehofer}.
1.140  *}
1.142  text %mlref {*
1.143 @@ -139,19 +149,19 @@
1.144    tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
1.146    \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
1.147 -  expression of of a given sort.
1.148 +  is of a given sort.
1.150    \item @{ML Sign.add_types}~@{text "[(c, k, mx), \<dots>]"} declares new
1.151 -  type constructors @{text "c"} with @{text "k"} arguments, and
1.152 +  type constructors @{text "c"} with @{text "k"} arguments and
1.153    optional mixfix syntax.
1.155    \item @{ML Sign.add_tyabbrs_i}~@{text "[(c, \<^vec>\<alpha>, \<tau>, mx), \<dots>]"}
1.156 -  defines type abbreviation @{text "(\<^vec>\<alpha>)c"} (with optional
1.157 -  mixfix syntax) as @{text "\<tau>"}.
1.158 +  defines a new type abbreviation @{text "(\<^vec>\<alpha>)c = \<tau>"} with
1.159 +  optional mixfix syntax.
1.161    \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
1.162    c\<^isub>n])"} declares new class @{text "c"} derived together with
1.163 -  class relations @{text "c \<subseteq> c\<^isub>i"}.
1.164 +  class relations @{text "c \<subseteq> c\<^isub>i"}, for @{text "i = 1, \<dots>, n"}.
1.166    \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
1.167    c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
1.168 @@ -170,6 +180,13 @@
1.169  text {*
1.170    \glossary{Term}{FIXME}
1.172 +  The language of terms is that of simply-typed @{text "\<lambda>"}-calculus
1.173 +  with de-Bruijn indices for bound variables, and named free
1.174 +  variables, and constants.  Terms with loose bound variables are
1.175 +  usually considered malformed.  The types of variables and constants
1.176 +  is stored explicitly at each occurrence in the term (which is a
1.177 +  known performance issue).
1.179    FIXME de-Bruijn representation of lambda terms
1.181    Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}
1.182 @@ -193,13 +210,6 @@
1.183  *}
1.186 -section {* Proof terms *}
1.188 -text {*
1.189 -  FIXME
1.190 -*}
1.193  section {* Theorems \label{sec:thms} *}
1.195  text {*
1.196 @@ -258,17 +268,54 @@
1.198  *}
1.200 -subsection {* Primitive inferences *}
1.202 +section {* Proof terms *}
1.204 -text FIXME
1.205 +text {*
1.206 +  FIXME !?
1.207 +*}
1.210 -subsection {* Higher-order resolution *}
1.211 +section {* Rules \label{sec:rules} *}
1.213  text {*
1.215  FIXME
1.217 +  A \emph{rule} is any Pure theorem in HHF normal form; there is a
1.218 +  separate calculus for rule composition, which is modeled after
1.219 +  Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows
1.220 +  rules to be nested arbitrarily, similar to \cite{extensions91}.
1.222 +  Normally, all theorems accessible to the user are proper rules.
1.223 +  Low-level inferences are occasional required internally, but the
1.224 +  result should be always presented in canonical form.  The higher
1.225 +  interfaces of Isabelle/Isar will always produce proper rules.  It is
1.226 +  important to maintain this invariant in add-on applications!
1.228 +  There are two main principles of rule composition: @{text
1.229 +  "resolution"} (i.e.\ backchaining of rules) and @{text
1.230 +  "by-assumption"} (i.e.\ closing a branch); both principles are
1.231 +  combined in the variants of @{text "elim-resosultion"} and @{text
1.232 +  "dest-resolution"}.  Raw @{text "composition"} is occasionally
1.233 +  useful as well, also it is strictly speaking outside of the proper
1.234 +  rule calculus.
1.236 +  Rules are treated modulo general higher-order unification, which is
1.237 +  unification modulo the equational theory of @{text "\<alpha>\<beta>\<eta>"}-conversion
1.238 +  on @{text "\<lambda>"}-terms.  Moreover, propositions are understood modulo
1.239 +  the (derived) equivalence @{text "(A \<Longrightarrow> (\<And>x. B x)) \<equiv> (\<And>x. A \<Longrightarrow> B x)"}.
1.241 +  This means that any operations within the rule calculus may be
1.242 +  subject to spontaneous @{text "\<alpha>\<beta>\<eta>"}-HHF conversions.  It is common
1.243 +  practice not to contract or expand unnecessarily.  Some mechanisms
1.244 +  prefer an one form, others the opposite, so there is a potential
1.245 +  danger to produce some oscillation!
1.247 +  Only few operations really work \emph{modulo} HHF conversion, but
1.248 +  expect a normal form: quantifiers @{text "\<And>"} before implications
1.249 +  @{text "\<Longrightarrow>"} at each level of nesting.
1.251  \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
1.252  format is defined inductively as @{text "H = (\<And>x\<^sup>*. H\<^sup>* \<Longrightarrow>
1.253  A)"}, for variables @{text "x"} and atomic propositions @{text "A"}.
1.254 @@ -282,9 +329,4 @@
1.256  *}
1.258 -subsection {* Equational reasoning *}
1.260 -text FIXME
1.263  end