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.5  chapter {* Primitive logic \label{ch:logic} *}
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.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.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.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.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.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.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.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.128 +  \begin{description}
1.130 +  \item @{ML_type class} represents type classes; this is an alias for
1.131 +  @{ML_type string}.
1.133 +  \item @{ML_type sort} represents sorts; this is an alias for
1.134 +  @{ML_type "class list"}.
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.141 +  \item @{ML_type typ} represents types; this is a datatype with
1.142 +  constructors @{ML TFree}, @{ML TVar}, @{ML Type}.
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.147 +  \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether a type
1.148 +  expression of 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 +  optional mixfix syntax.
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.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.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.167 +  \item @{ML Sign.primitive_arity}~@{text "(c, \<^vec>s, s)"} declares
1.168 +  arity @{text "c :: (\<^vec>s)s"}.
1.170 +  \end{description}
1.171  *}
1.175  section {* Terms \label{sec:terms} *}
1.177  text {*
1.178    \glossary{Term}{FIXME}
1.180    FIXME de-Bruijn representation of lambda terms
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.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.192 @@ -58,6 +204,22 @@
1.194  text {*
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.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.212    FIXME
1.214  \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
1.215 @@ -100,6 +262,7 @@
1.217  text FIXME
1.220  subsection {* Higher-order resolution *}
1.222  text {*
1.223 @@ -124,21 +287,4 @@
1.224  text FIXME
1.227 -section {* Raw theories *}
1.229 -text {*
1.231 -FIXME
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.238 -\glossary{Axiom}{FIXME}
1.240 -\glossary{Primitive definition}{FIXME}
1.242 -*}
1.244  end