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.10  
    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.15  
    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.25  
    1.26  
    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.35  
    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.54  
    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.63  
    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.73  
    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.84    
    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.97  
    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.101  
   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.114 +
   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.122  
   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.141  
   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.145  
   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.149  
   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.154  
   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.160  
   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.165  
   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.171  
   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.178 +
   1.179    FIXME de-Bruijn representation of lambda terms
   1.180  
   1.181    Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}
   1.182 @@ -193,13 +210,6 @@
   1.183  *}
   1.184  
   1.185  
   1.186 -section {* Proof terms *}
   1.187 -
   1.188 -text {*
   1.189 -  FIXME
   1.190 -*}
   1.191 -
   1.192 -
   1.193  section {* Theorems \label{sec:thms} *}
   1.194  
   1.195  text {*
   1.196 @@ -258,17 +268,54 @@
   1.197  
   1.198  *}
   1.199  
   1.200 -subsection {* Primitive inferences *}
   1.201 +
   1.202 +section {* Proof terms *}
   1.203  
   1.204 -text FIXME
   1.205 +text {*
   1.206 +  FIXME !?
   1.207 +*}
   1.208  
   1.209  
   1.210 -subsection {* Higher-order resolution *}
   1.211 +section {* Rules \label{sec:rules} *}
   1.212  
   1.213  text {*
   1.214  
   1.215  FIXME
   1.216  
   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.221 +
   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.227 +
   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.235 +
   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.240 +
   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.246 +
   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.250 +
   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.255  
   1.256  *}
   1.257  
   1.258 -subsection {* Equational reasoning *}
   1.259 -
   1.260 -text FIXME
   1.261 -
   1.262 -
   1.263  end