doc-src/IsarImplementation/Thy/logic.thy
changeset 20480 4e0522d38968
parent 20477 e623b0e30541
child 20491 98ba42f19995
     1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 05 22:05:15 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 05 22:05:41 2006 +0200
     1.3 @@ -5,34 +5,180 @@
     1.4  
     1.5  chapter {* Primitive logic \label{ch:logic} *}
     1.6  
     1.7 +text {*
     1.8 +  The logical foundations of Isabelle/Isar are that of the Pure logic,
     1.9 +  which has been introduced as a natural-deduction framework in
    1.10 +  \cite{paulson700}.  This is essentially the same logic as ``@{text
    1.11 +  "\<lambda>HOL"}'' in the more abstract framework of Pure Type Systems (PTS)
    1.12 +  \cite{Barendregt-Geuvers:2001}, although there are some key
    1.13 +  differences in the practical treatment of simple types.
    1.14 +
    1.15 +  Following type-theoretic parlance, the Pure logic consists of three
    1.16 +  levels of @{text "\<lambda>"}-calculus with corresponding arrows: @{text
    1.17 +  "\<Rightarrow>"} for syntactic function space (terms depending on terms), @{text
    1.18 +  "\<And>"} for universal quantification (proofs depending on terms), and
    1.19 +  @{text "\<Longrightarrow>"} for implication (proofs depending on proofs).
    1.20 +
    1.21 +  Pure derivations are relative to a logical theory, which declares
    1.22 +  type constructors, term constants, and axioms.  Term constants and
    1.23 +  axioms support schematic polymorphism.
    1.24 +*}
    1.25 +
    1.26 +
    1.27  section {* Types \label{sec:types} *}
    1.28  
    1.29  text {*
    1.30 -  \glossary{Type class}{FIXME}
    1.31 +  The language of types is an uninterpreted order-sorted first-order
    1.32 +  algebra; types are qualified by ordered type classes.
    1.33 +
    1.34 +  \medskip A \emph{type class} is an abstract syntactic entity
    1.35 +  declared in the theory context.  The \emph{subclass relation} @{text
    1.36 +  "c\<^isub>1 \<subseteq> c\<^isub>2"} is specified by stating an acyclic
    1.37 +  generating relation; the transitive closure maintained internally.
    1.38  
    1.39 -  \glossary{Type arity}{FIXME}
    1.40 +  A \emph{sort} is a list of type classes written as @{text
    1.41 +  "{c\<^isub>1, \<dots>, c\<^isub>m}"}, which represents symbolic
    1.42 +  intersection.  Notationally, the curly braces are omitted for
    1.43 +  singleton intersections, i.e.\ any class @{text "c"} may be read as
    1.44 +  a sort @{text "{c}"}.  The ordering on type classes is extended to
    1.45 +  sorts in the canonical fashion: @{text "{c\<^isub>1, \<dots> c\<^isub>m} \<subseteq>
    1.46 +  {d\<^isub>1, \<dots>, d\<^isub>n}"} iff @{text "\<forall>j. \<exists>i. c\<^isub>i \<subseteq>
    1.47 +  d\<^isub>j"}.  The empty intersection @{text "{}"} refers to the
    1.48 +  universal sort, which is the largest element wrt.\ the sort order.
    1.49 +  The intersections of all (i.e.\ finitely many) classes declared in
    1.50 +  the current theory are the minimal elements wrt.\ sort order.
    1.51 +
    1.52 +  \medskip A \emph{fixed type variable} is pair of a basic name
    1.53 +  (starting with @{text "'"} character) and a sort constraint.  For
    1.54 +  example, @{text "('a, s)"} which is usually printed as @{text
    1.55 +  "\<alpha>\<^isub>s"}.  A \emph{schematic type variable} is a pair of an
    1.56 +  indexname and a sort constraint.  For example, @{text "(('a, 0),
    1.57 +  s)"} which is usually printed @{text "?\<alpha>\<^isub>s"}.
    1.58  
    1.59 -  \glossary{Sort}{FIXME}
    1.60 +  Note that \emph{all} syntactic components contribute to the identity
    1.61 +  of a type variables, including the literal sort constraint.  The
    1.62 +  core logic handles type variables with the same name but different
    1.63 +  sorts as different, even though the outer layers of the system make
    1.64 +  it hard to produce anything like this.
    1.65  
    1.66 -  FIXME classes and sorts
    1.67 +  A \emph{type constructor} is an @{text "k"}-ary type operator
    1.68 +  declared in the theory.
    1.69 +  
    1.70 +  A \emph{type} is defined inductively over type variables and type
    1.71 +  constructors: @{text "\<tau> = \<alpha>\<^isub>s | ?\<alpha>\<^isub>s | (\<tau>\<^sub>1, \<dots>,
    1.72 +  \<tau>\<^sub>k)c"}.  Type constructor application is usually written
    1.73 +  postfix.  For @{text "k = 0"} the argument tuple is omitted, e.g.\
    1.74 +  @{text "prop"} instead of @{text "()prop"}.  For @{text "k = 1"} the
    1.75 +  parentheses are omitted, e.g.\ @{text "\<tau> list"} instead of @{text
    1.76 +  "(\<tau>) list"}.  Further notation is provided for specific
    1.77 +  constructors, notably right-associative infix @{text "\<tau>\<^isub>1 \<Rightarrow>
    1.78 +  \<tau>\<^isub>2"} instead of @{text "(\<tau>\<^isub>1, \<tau>\<^isub>2)fun"}
    1.79 +  constructor.
    1.80  
    1.81 +  A \emph{type abbreviation} is a syntactic abbreviation of an
    1.82 +  arbitrary type expression of the theory.  Type abbreviations looks
    1.83 +  like type constructors at the surface, but are expanded before the
    1.84 +  core logic encounters them.
    1.85 +
    1.86 +  A \emph{type arity} declares the image behavior of a type
    1.87 +  constructor wrt.\ the algebra of sorts: @{text "c :: (s\<^isub>1, \<dots>,
    1.88 +  s\<^isub>n)s"} means that @{text "(\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>k)c"} is
    1.89 +  of sort @{text "s"} if each argument type @{text "\<tau>\<^isub>i"} is of
    1.90 +  sort @{text "s\<^isub>i"}.  The sort algebra is always maintained as
    1.91 +  \emph{coregular}, which means that type arities are consistent with
    1.92 +  the subclass relation: for each type constructor @{text "c"} and
    1.93 +  classes @{text "c\<^isub>1 \<subseteq> c\<^isub>2"}, any arity @{text "c ::
    1.94 +  (\<^vec>s\<^isub>1)c\<^isub>1"} has a corresponding arity @{text "c
    1.95 +  :: (\<^vec>s\<^isub>2)c\<^isub>2"} where @{text "\<^vec>s\<^isub>1 \<subseteq>
    1.96 +  \<^vec>s\<^isub>2"} holds pointwise for all argument sorts.
    1.97  
    1.98 -  \glossary{Type}{FIXME}
    1.99 +  The key property of the order-sorted algebra of types is that sort
   1.100 +  constraints may be always fulfilled in a most general fashion: for
   1.101 +  each type constructor @{text "c"} and sort @{text "s"} there is a
   1.102 +  most general vector of argument sorts @{text "(s\<^isub>1, \<dots>,
   1.103 +  s\<^isub>k)"} such that @{text "(\<tau>\<^bsub>s\<^isub>1\<^esub>, \<dots>,
   1.104 +  \<tau>\<^bsub>s\<^isub>k\<^esub>)"} for arbitrary @{text "\<tau>\<^isub>i"} of
   1.105 +  sort @{text "s\<^isub>i"}.  This means the unification problem on
   1.106 +  the algebra of types has most general solutions (modulo renaming and
   1.107 +  equivalence of sorts).  As a consequence, type-inference is able to
   1.108 +  produce primary types.
   1.109 +*}
   1.110  
   1.111 -  \glossary{Type constructor}{FIXME}
   1.112 +text %mlref {*
   1.113 +  \begin{mldecls}
   1.114 +  @{index_ML_type class} \\
   1.115 +  @{index_ML_type sort} \\
   1.116 +  @{index_ML_type typ} \\
   1.117 +  @{index_ML_type arity} \\
   1.118 +  @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
   1.119 +  @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
   1.120 +  @{index_ML Sign.add_types: "(bstring * int * mixfix) list -> theory -> theory"} \\
   1.121 +  @{index_ML Sign.add_tyabbrs_i: "
   1.122 +  (bstring * string list * typ * mixfix) list -> theory -> theory"} \\
   1.123 +  @{index_ML Sign.primitive_class: "string * class list -> theory -> theory"} \\
   1.124 +  @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
   1.125 +  @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
   1.126 +  \end{mldecls}
   1.127 +
   1.128 +  \begin{description}
   1.129 +
   1.130 +  \item @{ML_type class} represents type classes; this is an alias for
   1.131 +  @{ML_type string}.
   1.132 +
   1.133 +  \item @{ML_type sort} represents sorts; this is an alias for
   1.134 +  @{ML_type "class list"}.
   1.135  
   1.136 -  \glossary{Type variable}{FIXME}
   1.137 +  \item @{ML_type arity} represents type arities; this is an alias for
   1.138 +  triples of the form @{text "(c, \<^vec>s, s)"} for @{text "c ::
   1.139 +  (\<^vec>s)s"} described above.
   1.140 +
   1.141 +  \item @{ML_type typ} represents types; this is a datatype with
   1.142 +  constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
   1.143 +
   1.144 +  \item @{ML Sign.subsort}~@{text "thy (s\<^isub>1, s\<^isub>2)"}
   1.145 +  tests the subsort relation @{text "s\<^isub>1 \<subseteq> s\<^isub>2"}.
   1.146 +
   1.147 +  \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
   1.148 +  expression of 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 +  optional mixfix syntax.
   1.153  
   1.154 -  FIXME simple types
   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 +
   1.159 +  \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
   1.160 +  c\<^isub>n])"} declares new class @{text "c"} derived together with
   1.161 +  class relations @{text "c \<subseteq> c\<^isub>i"}.
   1.162 +
   1.163 +  \item @{ML Sign.primitive_classrel}~@{text "(c\<^isub>1,
   1.164 +  c\<^isub>2)"} declares class relation @{text "c\<^isub>1 \<subseteq>
   1.165 +  c\<^isub>2"}.
   1.166 +
   1.167 +  \item @{ML Sign.primitive_arity}~@{text "(c, \<^vec>s, s)"} declares
   1.168 +  arity @{text "c :: (\<^vec>s)s"}.
   1.169 +
   1.170 +  \end{description}
   1.171  *}
   1.172  
   1.173  
   1.174 +
   1.175  section {* Terms \label{sec:terms} *}
   1.176  
   1.177  text {*
   1.178    \glossary{Term}{FIXME}
   1.179  
   1.180    FIXME de-Bruijn representation of lambda terms
   1.181 +
   1.182 +  Term syntax provides explicit abstraction @{text "\<lambda>x :: \<alpha>. b(x)"}
   1.183 +  and application @{text "t u"}, while types are usually implicit
   1.184 +  thanks to type-inference.
   1.185 +
   1.186 +  Terms of type @{text "prop"} are called
   1.187 +  propositions.  Logical statements are composed via @{text "\<And>x ::
   1.188 +  \<alpha>. B(x)"} and @{text "A \<Longrightarrow> B"}.
   1.189  *}
   1.190  
   1.191  
   1.192 @@ -58,6 +204,22 @@
   1.193  
   1.194  text {*
   1.195  
   1.196 +  Primitive reasoning operates on judgments of the form @{text "\<Gamma> \<turnstile>
   1.197 +  \<phi>"}, with standard introduction and elimination rules for @{text
   1.198 +  "\<And>"} and @{text "\<Longrightarrow>"} that refer to fixed parameters @{text "x"} and
   1.199 +  hypotheses @{text "A"} from the context @{text "\<Gamma>"}.  The
   1.200 +  corresponding proof terms are left implicit in the classic
   1.201 +  ``LCF-approach'', although they could be exploited separately
   1.202 +  \cite{Berghofer-Nipkow:2000}.
   1.203 +
   1.204 +  The framework also provides definitional equality @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha>
   1.205 +  \<Rightarrow> prop"}, with @{text "\<alpha>\<beta>\<eta>"}-conversion rules.  The internal
   1.206 +  conjunction @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} enables the view of
   1.207 +  assumptions and conclusions emerging uniformly as simultaneous
   1.208 +  statements.
   1.209 +
   1.210 +
   1.211 +
   1.212    FIXME
   1.213  
   1.214  \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
   1.215 @@ -100,6 +262,7 @@
   1.216  
   1.217  text FIXME
   1.218  
   1.219 +
   1.220  subsection {* Higher-order resolution *}
   1.221  
   1.222  text {*
   1.223 @@ -124,21 +287,4 @@
   1.224  text FIXME
   1.225  
   1.226  
   1.227 -section {* Raw theories *}
   1.228 -
   1.229 -text {*
   1.230 -
   1.231 -FIXME
   1.232 -
   1.233 -\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
   1.234 -theory context, but slightly more flexible since it may be used at
   1.235 -different type-instances, due to \seeglossary{schematic
   1.236 -polymorphism.}}
   1.237 -
   1.238 -\glossary{Axiom}{FIXME}
   1.239 -
   1.240 -\glossary{Primitive definition}{FIXME}
   1.241 -
   1.242 -*}
   1.243 -
   1.244  end