--- a/doc-src/AxClass/Group/Group.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/AxClass/Group/Group.thy Sat Dec 01 18:52:32 2001 +0100
@@ -4,20 +4,20 @@
theory Group = Main:
text {*
- \medskip\noindent The meta-level type system of Isabelle supports
- \emph{intersections} and \emph{inclusions} of type classes. These
- directly correspond to intersections and inclusions of type
- predicates in a purely set theoretic sense. This is sufficient as a
- means to describe simple hierarchies of structures. As an
- illustration, we use the well-known example of semigroups, monoids,
- general groups and Abelian groups.
+ \medskip\noindent The meta-level type system of Isabelle supports
+ \emph{intersections} and \emph{inclusions} of type classes. These
+ directly correspond to intersections and inclusions of type
+ predicates in a purely set theoretic sense. This is sufficient as a
+ means to describe simple hierarchies of structures. As an
+ illustration, we use the well-known example of semigroups, monoids,
+ general groups and Abelian groups.
*}
subsection {* Monoids and Groups *}
text {*
- First we declare some polymorphic constants required later for the
- signature parts of our structures.
+ First we declare some polymorphic constants required later for the
+ signature parts of our structures.
*}
consts
@@ -26,33 +26,33 @@
one :: 'a ("\<unit>")
text {*
- \noindent Next we define class @{text monoid} of monoids with
- operations @{text \<odot>} and @{text \<unit>}. Note that multiple class
- axioms are allowed for user convenience --- they simply represent the
- conjunction of their respective universal closures.
+ \noindent Next we define class @{text monoid} of monoids with
+ operations @{text \<odot>} and @{text \<unit>}. Note that multiple class
+ axioms are allowed for user convenience --- they simply represent
+ the conjunction of their respective universal closures.
*}
-axclass monoid \<subseteq> "term"
+axclass monoid \<subseteq> type
assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
left_unit: "\<unit> \<odot> x = x"
right_unit: "x \<odot> \<unit> = x"
text {*
- \noindent So class @{text monoid} contains exactly those types @{text
- \<tau>} where @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} and @{text "\<unit> \<Colon> \<tau>"} are
- specified appropriately, such that @{text \<odot>} is associative and
- @{text \<unit>} is a left and right unit element for the @{text \<odot>}
- operation.
+ \noindent So class @{text monoid} contains exactly those types
+ @{text \<tau>} where @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} and @{text "\<unit> \<Colon> \<tau>"}
+ are specified appropriately, such that @{text \<odot>} is associative and
+ @{text \<unit>} is a left and right unit element for the @{text \<odot>}
+ operation.
*}
text {*
- \medskip Independently of @{text monoid}, we now define a linear
- hierarchy of semigroups, general groups and Abelian groups. Note
- that the names of class axioms are automatically qualified with each
- class name, so we may re-use common names such as @{text assoc}.
+ \medskip Independently of @{text monoid}, we now define a linear
+ hierarchy of semigroups, general groups and Abelian groups. Note
+ that the names of class axioms are automatically qualified with each
+ class name, so we may re-use common names such as @{text assoc}.
*}
-axclass semigroup \<subseteq> "term"
+axclass semigroup \<subseteq> type
assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
axclass group \<subseteq> semigroup
@@ -63,32 +63,32 @@
commute: "x \<odot> y = y \<odot> x"
text {*
- \noindent Class @{text group} inherits associativity of @{text \<odot>}
- from @{text semigroup} and adds two further group axioms. Similarly,
- @{text agroup} is defined as the subset of @{text group} such that
- for all of its elements @{text \<tau>}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow>
- \<tau>"} is even commutative.
+ \noindent Class @{text group} inherits associativity of @{text \<odot>}
+ from @{text semigroup} and adds two further group axioms. Similarly,
+ @{text agroup} is defined as the subset of @{text group} such that
+ for all of its elements @{text \<tau>}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow>
+ \<tau>"} is even commutative.
*}
subsection {* Abstract reasoning *}
text {*
- In a sense, axiomatic type classes may be viewed as \emph{abstract
- theories}. Above class definitions gives rise to abstract axioms
- @{text assoc}, @{text left_unit}, @{text left_inverse}, @{text
- commute}, where any of these contain a type variable @{text "'a \<Colon> c"}
- that is restricted to types of the corresponding class @{text c}.
- \emph{Sort constraints} like this express a logical precondition for
- the whole formula. For example, @{text assoc} states that for all
- @{text \<tau>}, provided that @{text "\<tau> \<Colon> semigroup"}, the operation
- @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is associative.
+ In a sense, axiomatic type classes may be viewed as \emph{abstract
+ theories}. Above class definitions gives rise to abstract axioms
+ @{text assoc}, @{text left_unit}, @{text left_inverse}, @{text
+ commute}, where any of these contain a type variable @{text "'a \<Colon>
+ c"} that is restricted to types of the corresponding class @{text
+ c}. \emph{Sort constraints} like this express a logical
+ precondition for the whole formula. For example, @{text assoc}
+ states that for all @{text \<tau>}, provided that @{text "\<tau> \<Colon>
+ semigroup"}, the operation @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is associative.
- \medskip From a technical point of view, abstract axioms are just
- ordinary Isabelle theorems, which may be used in proofs without
- special treatment. Such ``abstract proofs'' usually yield new
- ``abstract theorems''. For example, we may now derive the following
- well-known laws of general groups.
+ \medskip From a technical point of view, abstract axioms are just
+ ordinary Isabelle theorems, which may be used in proofs without
+ special treatment. Such ``abstract proofs'' usually yield new
+ ``abstract theorems''. For example, we may now derive the following
+ well-known laws of general groups.
*}
theorem group_right_inverse: "x \<odot> x\<inv> = (\<unit>\<Colon>'a\<Colon>group)"
@@ -113,9 +113,9 @@
qed
text {*
- \noindent With @{text group_right_inverse} already available, @{text
- group_right_unit}\label{thm:group-right-unit} is now established much
- easier.
+ \noindent With @{text group_right_inverse} already available, @{text
+ group_right_unit}\label{thm:group-right-unit} is now established
+ much easier.
*}
theorem group_right_unit: "x \<odot> \<unit> = (x\<Colon>'a\<Colon>group)"
@@ -132,26 +132,26 @@
qed
text {*
- \medskip Abstract theorems may be instantiated to only those types
- @{text \<tau>} where the appropriate class membership @{text "\<tau> \<Colon> c"} is
- known at Isabelle's type signature level. Since we have @{text
- "agroup \<subseteq> group \<subseteq> semigroup"} by definition, all theorems of @{text
- semigroup} and @{text group} are automatically inherited by @{text
- group} and @{text agroup}.
+ \medskip Abstract theorems may be instantiated to only those types
+ @{text \<tau>} where the appropriate class membership @{text "\<tau> \<Colon> c"} is
+ known at Isabelle's type signature level. Since we have @{text
+ "agroup \<subseteq> group \<subseteq> semigroup"} by definition, all theorems of @{text
+ semigroup} and @{text group} are automatically inherited by @{text
+ group} and @{text agroup}.
*}
subsection {* Abstract instantiation *}
text {*
- From the definition, the @{text monoid} and @{text group} classes
- have been independent. Note that for monoids, @{text right_unit} had
- to be included as an axiom, but for groups both @{text right_unit}
- and @{text right_inverse} are derivable from the other axioms. With
- @{text group_right_unit} derived as a theorem of group theory (see
- page~\pageref{thm:group-right-unit}), we may now instantiate @{text
- "monoid \<subseteq> semigroup"} and @{text "group \<subseteq> monoid"} properly as
- follows (cf.\ \figref{fig:monoid-group}).
+ From the definition, the @{text monoid} and @{text group} classes
+ have been independent. Note that for monoids, @{text right_unit}
+ had to be included as an axiom, but for groups both @{text
+ right_unit} and @{text right_inverse} are derivable from the other
+ axioms. With @{text group_right_unit} derived as a theorem of group
+ theory (see page~\pageref{thm:group-right-unit}), we may now
+ instantiate @{text "monoid \<subseteq> semigroup"} and @{text "group \<subseteq>
+ monoid"} properly as follows (cf.\ \figref{fig:monoid-group}).
\begin{figure}[htbp]
\begin{center}
@@ -163,7 +163,7 @@
\put(15,5){\makebox(0,0){@{text agroup}}}
\put(15,25){\makebox(0,0){@{text group}}}
\put(15,45){\makebox(0,0){@{text semigroup}}}
- \put(30,65){\makebox(0,0){@{text "term"}}} \put(50,45){\makebox(0,0){@{text monoid}}}
+ \put(30,65){\makebox(0,0){@{text type}}} \put(50,45){\makebox(0,0){@{text monoid}}}
\end{picture}
\hspace{4em}
\begin{picture}(30,90)(0,0)
@@ -173,7 +173,7 @@
\put(15,25){\makebox(0,0){@{text group}}}
\put(15,45){\makebox(0,0){@{text monoid}}}
\put(15,65){\makebox(0,0){@{text semigroup}}}
- \put(15,85){\makebox(0,0){@{text term}}}
+ \put(15,85){\makebox(0,0){@{text type}}}
\end{picture}
\caption{Monoids and groups: according to definition, and by proof}
\label{fig:monoid-group}
@@ -200,34 +200,34 @@
qed
text {*
- \medskip The $\INSTANCE$ command sets up an appropriate goal that
- represents the class inclusion (or type arity, see
- \secref{sec:inst-arity}) to be proven (see also
- \cite{isabelle-isar-ref}). The initial proof step causes
- back-chaining of class membership statements wrt.\ the hierarchy of
- any classes defined in the current theory; the effect is to reduce to
- the initial statement to a number of goals that directly correspond
- to any class axioms encountered on the path upwards through the class
- hierarchy.
+ \medskip The $\INSTANCE$ command sets up an appropriate goal that
+ represents the class inclusion (or type arity, see
+ \secref{sec:inst-arity}) to be proven (see also
+ \cite{isabelle-isar-ref}). The initial proof step causes
+ back-chaining of class membership statements wrt.\ the hierarchy of
+ any classes defined in the current theory; the effect is to reduce
+ to the initial statement to a number of goals that directly
+ correspond to any class axioms encountered on the path upwards
+ through the class hierarchy.
*}
subsection {* Concrete instantiation \label{sec:inst-arity} *}
text {*
- So far we have covered the case of the form $\INSTANCE$~@{text
- "c\<^sub>1 \<subseteq> c\<^sub>2"}, namely \emph{abstract instantiation} ---
- $c@1$ is more special than @{text "c\<^sub>1"} and thus an instance
- of @{text "c\<^sub>2"}. Even more interesting for practical
- applications are \emph{concrete instantiations} of axiomatic type
- classes. That is, certain simple schemes @{text "(\<alpha>\<^sub>1, \<dots>,
- \<alpha>\<^sub>n) t \<Colon> c"} of class membership may be established at the
- logical level and then transferred to Isabelle's type signature
- level.
+ So far we have covered the case of the form $\INSTANCE$~@{text
+ "c\<^sub>1 \<subseteq> c\<^sub>2"}, namely \emph{abstract instantiation} ---
+ $c@1$ is more special than @{text "c\<^sub>1"} and thus an instance
+ of @{text "c\<^sub>2"}. Even more interesting for practical
+ applications are \emph{concrete instantiations} of axiomatic type
+ classes. That is, certain simple schemes @{text "(\<alpha>\<^sub>1, \<dots>,
+ \<alpha>\<^sub>n) t \<Colon> c"} of class membership may be established at the
+ logical level and then transferred to Isabelle's type signature
+ level.
- \medskip As a typical example, we show that type @{typ bool} with
- exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and
- @{term False} as @{text \<unit>} forms an Abelian group.
+ \medskip As a typical example, we show that type @{typ bool} with
+ exclusive-or as @{text \<odot>} operation, identity as @{text \<inv>}, and
+ @{term False} as @{text \<unit>} forms an Abelian group.
*}
defs (overloaded)
@@ -236,18 +236,18 @@
unit_bool_def: "\<unit> \<equiv> False"
text {*
- \medskip It is important to note that above $\DEFS$ are just
- overloaded meta-level constant definitions, where type classes are
- not yet involved at all. This form of constant definition with
- overloading (and optional recursion over the syntactic structure of
- simple types) are admissible as definitional extensions of plain HOL
- \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not
- required for overloading. Nevertheless, overloaded definitions are
- best applied in the context of type classes.
+ \medskip It is important to note that above $\DEFS$ are just
+ overloaded meta-level constant definitions, where type classes are
+ not yet involved at all. This form of constant definition with
+ overloading (and optional recursion over the syntactic structure of
+ simple types) are admissible as definitional extensions of plain HOL
+ \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not
+ required for overloading. Nevertheless, overloaded definitions are
+ best applied in the context of type classes.
- \medskip Since we have chosen above $\DEFS$ of the generic group
- operations on type @{typ bool} appropriately, the class membership
- @{text "bool \<Colon> agroup"} may be now derived as follows.
+ \medskip Since we have chosen above $\DEFS$ of the generic group
+ operations on type @{typ bool} appropriately, the class membership
+ @{text "bool \<Colon> agroup"} may be now derived as follows.
*}
instance bool :: agroup
@@ -261,44 +261,44 @@
qed
text {*
- The result of an $\INSTANCE$ statement is both expressed as a theorem
- of Isabelle's meta-logic, and as a type arity of the type signature.
- The latter enables type-inference system to take care of this new
- instance automatically.
+ The result of an $\INSTANCE$ statement is both expressed as a
+ theorem of Isabelle's meta-logic, and as a type arity of the type
+ signature. The latter enables type-inference system to take care of
+ this new instance automatically.
- \medskip We could now also instantiate our group theory classes to
- many other concrete types. For example, @{text "int \<Colon> agroup"}
- (e.g.\ by defining @{text \<odot>} as addition, @{text \<inv>} as negation
- and @{text \<unit>} as zero) or @{text "list \<Colon> (term) semigroup"}
- (e.g.\ if @{text \<odot>} is defined as list append). Thus, the
- characteristic constants @{text \<odot>}, @{text \<inv>}, @{text \<unit>}
- really become overloaded, i.e.\ have different meanings on different
- types.
+ \medskip We could now also instantiate our group theory classes to
+ many other concrete types. For example, @{text "int \<Colon> agroup"}
+ (e.g.\ by defining @{text \<odot>} as addition, @{text \<inv>} as negation
+ and @{text \<unit>} as zero) or @{text "list \<Colon> (type) semigroup"}
+ (e.g.\ if @{text \<odot>} is defined as list append). Thus, the
+ characteristic constants @{text \<odot>}, @{text \<inv>}, @{text \<unit>}
+ really become overloaded, i.e.\ have different meanings on different
+ types.
*}
subsection {* Lifting and Functors *}
text {*
- As already mentioned above, overloading in the simply-typed HOL
- systems may include recursion over the syntactic structure of types.
- That is, definitional equations @{text "c\<^sup>\<tau> \<equiv> t"} may also
- contain constants of name @{text c} on the right-hand side --- if
- these have types that are structurally simpler than @{text \<tau>}.
+ As already mentioned above, overloading in the simply-typed HOL
+ systems may include recursion over the syntactic structure of types.
+ That is, definitional equations @{text "c\<^sup>\<tau> \<equiv> t"} may also
+ contain constants of name @{text c} on the right-hand side --- if
+ these have types that are structurally simpler than @{text \<tau>}.
- This feature enables us to \emph{lift operations}, say to Cartesian
- products, direct sums or function spaces. Subsequently we lift
- @{text \<odot>} component-wise to binary products @{typ "'a \<times> 'b"}.
+ This feature enables us to \emph{lift operations}, say to Cartesian
+ products, direct sums or function spaces. Subsequently we lift
+ @{text \<odot>} component-wise to binary products @{typ "'a \<times> 'b"}.
*}
defs (overloaded)
times_prod_def: "p \<odot> q \<equiv> (fst p \<odot> fst q, snd p \<odot> snd q)"
text {*
- It is very easy to see that associativity of @{text \<odot>} on @{typ 'a}
- and @{text \<odot>} on @{typ 'b} transfers to @{text \<odot>} on @{typ "'a \<times>
- 'b"}. Hence the binary type constructor @{text \<odot>} maps semigroups to
- semigroups. This may be established formally as follows.
+ It is very easy to see that associativity of @{text \<odot>} on @{typ 'a}
+ and @{text \<odot>} on @{typ 'b} transfers to @{text \<odot>} on @{typ "'a \<times>
+ 'b"}. Hence the binary type constructor @{text \<odot>} maps semigroups
+ to semigroups. This may be established formally as follows.
*}
instance * :: (semigroup, semigroup) semigroup
@@ -313,10 +313,10 @@
qed
text {*
- Thus, if we view class instances as ``structures'', then overloaded
- constant definitions with recursion over types indirectly provide
- some kind of ``functors'' --- i.e.\ mappings between abstract
- theories.
+ Thus, if we view class instances as ``structures'', then overloaded
+ constant definitions with recursion over types indirectly provide
+ some kind of ``functors'' --- i.e.\ mappings between abstract
+ theories.
*}
-end
\ No newline at end of file
+end
--- a/doc-src/AxClass/Group/Product.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/AxClass/Group/Product.thy Sat Dec 01 18:52:32 2001 +0100
@@ -4,52 +4,53 @@
theory Product = Main:
text {*
- \medskip\noindent There is still a feature of Isabelle's type system
- left that we have not yet discussed. When declaring polymorphic
- constants @{text "c \<Colon> \<sigma>"}, the type variables occurring in @{text \<sigma>}
- may be constrained by type classes (or even general sorts) in an
- arbitrary way. Note that by default, in Isabelle/HOL the declaration
- @{text "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} is actually an abbreviation for @{text "\<odot>
- \<Colon> 'a\<Colon>term \<Rightarrow> 'a \<Rightarrow> 'a"} Since class @{text "term"} is the universal
- class of HOL, this is not really a constraint at all.
+ \medskip\noindent There is still a feature of Isabelle's type system
+ left that we have not yet discussed. When declaring polymorphic
+ constants @{text "c \<Colon> \<sigma>"}, the type variables occurring in @{text \<sigma>}
+ may be constrained by type classes (or even general sorts) in an
+ arbitrary way. Note that by default, in Isabelle/HOL the
+ declaration @{text "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} is actually an abbreviation
+ for @{text "\<odot> \<Colon> 'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> 'a"} Since class @{text type} is the
+ universal class of HOL, this is not really a constraint at all.
The @{text product} class below provides a less degenerate example of
syntactic type classes.
*}
axclass
- product \<subseteq> "term"
+ product \<subseteq> type
consts
product :: "'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70)
text {*
- Here class @{text product} is defined as subclass of @{text term}
- without any additional axioms. This effects in logical equivalence
- of @{text product} and @{text term}, as is reflected by the trivial
- introduction rule generated for this definition.
+ Here class @{text product} is defined as subclass of @{text type}
+ without any additional axioms. This effects in logical equivalence
+ of @{text product} and @{text type}, as is reflected by the trivial
+ introduction rule generated for this definition.
- \medskip So what is the difference of declaring @{text "\<odot> \<Colon>
- 'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"} vs.\ declaring @{text "\<odot> \<Colon> 'a\<Colon>term \<Rightarrow> 'a \<Rightarrow> 'a"}
- anyway? In this particular case where @{text "product \<equiv> term"}, it
- should be obvious that both declarations are the same from the
- logic's point of view. It even makes the most sense to remove sort
- constraints from constant declarations, as far as the purely logical
- meaning is concerned \cite{Wenzel:1997:TPHOL}.
+ \medskip So what is the difference of declaring @{text "\<odot> \<Colon>
+ 'a\<Colon>product \<Rightarrow> 'a \<Rightarrow> 'a"} vs.\ declaring @{text "\<odot> \<Colon> 'a\<Colon>type \<Rightarrow> 'a \<Rightarrow>
+ 'a"} anyway? In this particular case where @{text "product \<equiv>
+ type"}, it should be obvious that both declarations are the same
+ from the logic's point of view. It even makes the most sense to
+ remove sort constraints from constant declarations, as far as the
+ purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
- On the other hand there are syntactic differences, of course.
- Constants @{text \<odot>} on some type @{text \<tau>} are rejected by the
- type-checker, unless the arity @{text "\<tau> \<Colon> product"} is part of the
- type signature. In our example, this arity may be always added when
- required by means of an $\INSTANCE$ with the default proof $\DDOT$.
+ On the other hand there are syntactic differences, of course.
+ Constants @{text \<odot>} on some type @{text \<tau>} are rejected by the
+ type-checker, unless the arity @{text "\<tau> \<Colon> product"} is part of the
+ type signature. In our example, this arity may be always added when
+ required by means of an $\INSTANCE$ with the default proof $\DDOT$.
- \medskip Thus, we may observe the following discipline of using
- syntactic classes. Overloaded polymorphic constants have their type
- arguments restricted to an associated (logically trivial) class
- @{text c}. Only immediately before \emph{specifying} these constants
- on a certain type @{text \<tau>} do we instantiate @{text "\<tau> \<Colon> c"}.
+ \medskip Thus, we may observe the following discipline of using
+ syntactic classes. Overloaded polymorphic constants have their type
+ arguments restricted to an associated (logically trivial) class
+ @{text c}. Only immediately before \emph{specifying} these
+ constants on a certain type @{text \<tau>} do we instantiate @{text "\<tau> \<Colon>
+ c"}.
- This is done for class @{text product} and type @{typ bool} as
- follows.
+ This is done for class @{text product} and type @{typ bool} as
+ follows.
*}
instance bool :: product ..
@@ -80,4 +81,4 @@
``providing operations'' or even ``names of functions''.
*}
-end
\ No newline at end of file
+end
--- a/doc-src/AxClass/Group/Semigroups.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/AxClass/Group/Semigroups.thy Sat Dec 01 18:52:32 2001 +0100
@@ -4,50 +4,51 @@
theory Semigroups = Main:
text {*
- \medskip\noindent An axiomatic type class is simply a class of types
- that all meet certain properties, which are also called \emph{class
- axioms}. Thus, type classes may be also understood as type predicates
- --- i.e.\ abstractions over a single type argument @{typ 'a}. Class
- axioms typically contain polymorphic constants that depend on this
- type @{typ 'a}. These \emph{characteristic constants} behave like
- operations associated with the ``carrier'' type @{typ 'a}.
+ \medskip\noindent An axiomatic type class is simply a class of types
+ that all meet certain properties, which are also called \emph{class
+ axioms}. Thus, type classes may be also understood as type
+ predicates --- i.e.\ abstractions over a single type argument @{typ
+ 'a}. Class axioms typically contain polymorphic constants that
+ depend on this type @{typ 'a}. These \emph{characteristic
+ constants} behave like operations associated with the ``carrier''
+ type @{typ 'a}.
- We illustrate these basic concepts by the following formulation of
- semigroups.
+ We illustrate these basic concepts by the following formulation of
+ semigroups.
*}
consts
times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70)
-axclass semigroup \<subseteq> "term"
+axclass semigroup \<subseteq> type
assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
text {*
- \noindent Above we have first declared a polymorphic constant @{text
- "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} and then defined the class @{text semigroup} of
- all types @{text \<tau>} such that @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is indeed an
- associative operator. The @{text assoc} axiom contains exactly one
- type variable, which is invisible in the above presentation, though.
- Also note that free term variables (like @{term x}, @{term y}, @{term
- z}) are allowed for user convenience --- conceptually all of these
- are bound by outermost universal quantifiers.
+ \noindent Above we have first declared a polymorphic constant @{text
+ "\<odot> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> 'a"} and then defined the class @{text semigroup} of
+ all types @{text \<tau>} such that @{text "\<odot> \<Colon> \<tau> \<Rightarrow> \<tau> \<Rightarrow> \<tau>"} is indeed an
+ associative operator. The @{text assoc} axiom contains exactly one
+ type variable, which is invisible in the above presentation, though.
+ Also note that free term variables (like @{term x}, @{term y},
+ @{term z}) are allowed for user convenience --- conceptually all of
+ these are bound by outermost universal quantifiers.
- \medskip In general, type classes may be used to describe
- \emph{structures} with exactly one carrier @{typ 'a} and a fixed
- \emph{signature}. Different signatures require different classes.
- Below, class @{text plus_semigroup} represents semigroups
- @{text "(\<tau>, \<oplus>\<^sup>\<tau>)"}, while the original @{text semigroup} would
- correspond to semigroups of the form @{text "(\<tau>, \<odot>\<^sup>\<tau>)"}.
+ \medskip In general, type classes may be used to describe
+ \emph{structures} with exactly one carrier @{typ 'a} and a fixed
+ \emph{signature}. Different signatures require different classes.
+ Below, class @{text plus_semigroup} represents semigroups @{text
+ "(\<tau>, \<oplus>\<^sup>\<tau>)"}, while the original @{text semigroup} would
+ correspond to semigroups of the form @{text "(\<tau>, \<odot>\<^sup>\<tau>)"}.
*}
consts
plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oplus>" 70)
-axclass plus_semigroup \<subseteq> "term"
+axclass plus_semigroup \<subseteq> type
assoc: "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
text {*
- \noindent Even if classes @{text plus_semigroup} and @{text
- semigroup} both represent semigroups in a sense, they are certainly
- not quite the same.
+ \noindent Even if classes @{text plus_semigroup} and @{text
+ semigroup} both represent semigroups in a sense, they are certainly
+ not quite the same.
*}
-end
\ No newline at end of file
+end
--- a/doc-src/AxClass/generated/Group.tex Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/AxClass/generated/Group.tex Sat Dec 01 18:52:32 2001 +0100
@@ -9,12 +9,12 @@
%
\begin{isamarkuptext}%
\medskip\noindent The meta-level type system of Isabelle supports
- \emph{intersections} and \emph{inclusions} of type classes. These
- directly correspond to intersections and inclusions of type
- predicates in a purely set theoretic sense. This is sufficient as a
- means to describe simple hierarchies of structures. As an
- illustration, we use the well-known example of semigroups, monoids,
- general groups and Abelian groups.%
+ \emph{intersections} and \emph{inclusions} of type classes. These
+ directly correspond to intersections and inclusions of type
+ predicates in a purely set theoretic sense. This is sufficient as a
+ means to describe simple hierarchies of structures. As an
+ illustration, we use the well-known example of semigroups, monoids,
+ general groups and Abelian groups.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -24,7 +24,7 @@
%
\begin{isamarkuptext}%
First we declare some polymorphic constants required later for the
- signature parts of our structures.%
+ signature parts of our structures.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isanewline
@@ -34,32 +34,33 @@
%
\begin{isamarkuptext}%
\noindent Next we define class \isa{monoid} of monoids with
- operations \isa{{\isasymodot}} and \isa{{\isasymunit}}. Note that multiple class
- axioms are allowed for user convenience --- they simply represent the
- conjunction of their respective universal closures.%
+ operations \isa{{\isasymodot}} and \isa{{\isasymunit}}. Note that multiple class
+ axioms are allowed for user convenience --- they simply represent
+ the conjunction of their respective universal closures.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{axclass}\ monoid\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\isacommand{axclass}\ monoid\ {\isasymsubseteq}\ type\isanewline
\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
\ \ left{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}{\isasymunit}\ {\isasymodot}\ x\ {\isacharequal}\ x{\isachardoublequote}\isanewline
\ \ right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ x{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
-\noindent So class \isa{monoid} contains exactly those types \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymunit}\ {\isasymColon}\ {\isasymtau}} are
- specified appropriately, such that \isa{{\isasymodot}} is associative and
- \isa{{\isasymunit}} is a left and right unit element for the \isa{{\isasymodot}}
- operation.%
+\noindent So class \isa{monoid} contains exactly those types
+ \isa{{\isasymtau}} where \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} and \isa{{\isasymunit}\ {\isasymColon}\ {\isasymtau}}
+ are specified appropriately, such that \isa{{\isasymodot}} is associative and
+ \isa{{\isasymunit}} is a left and right unit element for the \isa{{\isasymodot}}
+ operation.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
\medskip Independently of \isa{monoid}, we now define a linear
- hierarchy of semigroups, general groups and Abelian groups. Note
- that the names of class axioms are automatically qualified with each
- class name, so we may re-use common names such as \isa{assoc}.%
+ hierarchy of semigroups, general groups and Abelian groups. Note
+ that the names of class axioms are automatically qualified with each
+ class name, so we may re-use common names such as \isa{assoc}.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline
\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isanewline
\isanewline
\isamarkupfalse%
@@ -73,9 +74,9 @@
%
\begin{isamarkuptext}%
\noindent Class \isa{group} inherits associativity of \isa{{\isasymodot}}
- from \isa{semigroup} and adds two further group axioms. Similarly,
- \isa{agroup} is defined as the subset of \isa{group} such that
- for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.%
+ from \isa{semigroup} and adds two further group axioms. Similarly,
+ \isa{agroup} is defined as the subset of \isa{group} such that
+ for all of its elements \isa{{\isasymtau}}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is even commutative.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -85,19 +86,16 @@
%
\begin{isamarkuptext}%
In a sense, axiomatic type classes may be viewed as \emph{abstract
- theories}. Above class definitions gives rise to abstract axioms
- \isa{assoc}, \isa{left{\isacharunderscore}unit}, \isa{left{\isacharunderscore}inverse}, \isa{commute}, where any of these contain a type variable \isa{{\isacharprime}a\ {\isasymColon}\ c}
- that is restricted to types of the corresponding class \isa{c}.
- \emph{Sort constraints} like this express a logical precondition for
- the whole formula. For example, \isa{assoc} states that for all
- \isa{{\isasymtau}}, provided that \isa{{\isasymtau}\ {\isasymColon}\ semigroup}, the operation
- \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is associative.
+ theories}. Above class definitions gives rise to abstract axioms
+ \isa{assoc}, \isa{left{\isacharunderscore}unit}, \isa{left{\isacharunderscore}inverse}, \isa{commute}, where any of these contain a type variable \isa{{\isacharprime}a\ {\isasymColon}\ c} that is restricted to types of the corresponding class \isa{c}. \emph{Sort constraints} like this express a logical
+ precondition for the whole formula. For example, \isa{assoc}
+ states that for all \isa{{\isasymtau}}, provided that \isa{{\isasymtau}\ {\isasymColon}\ semigroup}, the operation \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is associative.
- \medskip From a technical point of view, abstract axioms are just
- ordinary Isabelle theorems, which may be used in proofs without
- special treatment. Such ``abstract proofs'' usually yield new
- ``abstract theorems''. For example, we may now derive the following
- well-known laws of general groups.%
+ \medskip From a technical point of view, abstract axioms are just
+ ordinary Isabelle theorems, which may be used in proofs without
+ special treatment. Such ``abstract proofs'' usually yield new
+ ``abstract theorems''. For example, we may now derive the following
+ well-known laws of general groups.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}inverse{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ x{\isasyminv}\ {\isacharequal}\ {\isacharparenleft}{\isasymunit}{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
@@ -150,8 +148,8 @@
\isacommand{qed}\isamarkupfalse%
%
\begin{isamarkuptext}%
-\noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established much
- easier.%
+\noindent With \isa{group{\isacharunderscore}right{\isacharunderscore}inverse} already available, \isa{group{\isacharunderscore}right{\isacharunderscore}unit}\label{thm:group-right-unit} is now established
+ much easier.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\ group{\isacharunderscore}right{\isacharunderscore}unit{\isacharcolon}\ {\isachardoublequote}x\ {\isasymodot}\ {\isasymunit}\ {\isacharequal}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isasymColon}group{\isacharparenright}{\isachardoublequote}\isanewline
@@ -185,8 +183,8 @@
%
\begin{isamarkuptext}%
\medskip Abstract theorems may be instantiated to only those types
- \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is
- known at Isabelle's type signature level. Since we have \isa{agroup\ {\isasymsubseteq}\ group\ {\isasymsubseteq}\ semigroup} by definition, all theorems of \isa{semigroup} and \isa{group} are automatically inherited by \isa{group} and \isa{agroup}.%
+ \isa{{\isasymtau}} where the appropriate class membership \isa{{\isasymtau}\ {\isasymColon}\ c} is
+ known at Isabelle's type signature level. Since we have \isa{agroup\ {\isasymsubseteq}\ group\ {\isasymsubseteq}\ semigroup} by definition, all theorems of \isa{semigroup} and \isa{group} are automatically inherited by \isa{group} and \isa{agroup}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -196,12 +194,11 @@
%
\begin{isamarkuptext}%
From the definition, the \isa{monoid} and \isa{group} classes
- have been independent. Note that for monoids, \isa{right{\isacharunderscore}unit} had
- to be included as an axiom, but for groups both \isa{right{\isacharunderscore}unit}
- and \isa{right{\isacharunderscore}inverse} are derivable from the other axioms. With
- \isa{group{\isacharunderscore}right{\isacharunderscore}unit} derived as a theorem of group theory (see
- page~\pageref{thm:group-right-unit}), we may now instantiate \isa{monoid\ {\isasymsubseteq}\ semigroup} and \isa{group\ {\isasymsubseteq}\ monoid} properly as
- follows (cf.\ \figref{fig:monoid-group}).
+ have been independent. Note that for monoids, \isa{right{\isacharunderscore}unit}
+ had to be included as an axiom, but for groups both \isa{right{\isacharunderscore}unit} and \isa{right{\isacharunderscore}inverse} are derivable from the other
+ axioms. With \isa{group{\isacharunderscore}right{\isacharunderscore}unit} derived as a theorem of group
+ theory (see page~\pageref{thm:group-right-unit}), we may now
+ instantiate \isa{monoid\ {\isasymsubseteq}\ semigroup} and \isa{group\ {\isasymsubseteq}\ monoid} properly as follows (cf.\ \figref{fig:monoid-group}).
\begin{figure}[htbp]
\begin{center}
@@ -213,7 +210,7 @@
\put(15,5){\makebox(0,0){\isa{agroup}}}
\put(15,25){\makebox(0,0){\isa{group}}}
\put(15,45){\makebox(0,0){\isa{semigroup}}}
- \put(30,65){\makebox(0,0){\isa{term}}} \put(50,45){\makebox(0,0){\isa{monoid}}}
+ \put(30,65){\makebox(0,0){\isa{type}}} \put(50,45){\makebox(0,0){\isa{monoid}}}
\end{picture}
\hspace{4em}
\begin{picture}(30,90)(0,0)
@@ -223,7 +220,7 @@
\put(15,25){\makebox(0,0){\isa{group}}}
\put(15,45){\makebox(0,0){\isa{monoid}}}
\put(15,65){\makebox(0,0){\isa{semigroup}}}
- \put(15,85){\makebox(0,0){\isa{term}}}
+ \put(15,85){\makebox(0,0){\isa{type}}}
\end{picture}
\caption{Monoids and groups: according to definition, and by proof}
\label{fig:monoid-group}
@@ -266,14 +263,14 @@
%
\begin{isamarkuptext}%
\medskip The $\INSTANCE$ command sets up an appropriate goal that
- represents the class inclusion (or type arity, see
- \secref{sec:inst-arity}) to be proven (see also
- \cite{isabelle-isar-ref}). The initial proof step causes
- back-chaining of class membership statements wrt.\ the hierarchy of
- any classes defined in the current theory; the effect is to reduce to
- the initial statement to a number of goals that directly correspond
- to any class axioms encountered on the path upwards through the class
- hierarchy.%
+ represents the class inclusion (or type arity, see
+ \secref{sec:inst-arity}) to be proven (see also
+ \cite{isabelle-isar-ref}). The initial proof step causes
+ back-chaining of class membership statements wrt.\ the hierarchy of
+ any classes defined in the current theory; the effect is to reduce
+ to the initial statement to a number of goals that directly
+ correspond to any class axioms encountered on the path upwards
+ through the class hierarchy.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -283,16 +280,16 @@
%
\begin{isamarkuptext}%
So far we have covered the case of the form $\INSTANCE$~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}}, namely \emph{abstract instantiation} ---
- $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance
- of \isa{c\isactrlsub {\isadigit{2}}}. Even more interesting for practical
- applications are \emph{concrete instantiations} of axiomatic type
- classes. That is, certain simple schemes \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isasymColon}\ c} of class membership may be established at the
- logical level and then transferred to Isabelle's type signature
- level.
+ $c@1$ is more special than \isa{c\isactrlsub {\isadigit{1}}} and thus an instance
+ of \isa{c\isactrlsub {\isadigit{2}}}. Even more interesting for practical
+ applications are \emph{concrete instantiations} of axiomatic type
+ classes. That is, certain simple schemes \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isasymColon}\ c} of class membership may be established at the
+ logical level and then transferred to Isabelle's type signature
+ level.
- \medskip As a typical example, we show that type \isa{bool} with
- exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and
- \isa{False} as \isa{{\isasymunit}} forms an Abelian group.%
+ \medskip As a typical example, we show that type \isa{bool} with
+ exclusive-or as \isa{{\isasymodot}} operation, identity as \isa{{\isasyminv}}, and
+ \isa{False} as \isa{{\isasymunit}} forms an Abelian group.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
@@ -302,17 +299,17 @@
%
\begin{isamarkuptext}%
\medskip It is important to note that above $\DEFS$ are just
- overloaded meta-level constant definitions, where type classes are
- not yet involved at all. This form of constant definition with
- overloading (and optional recursion over the syntactic structure of
- simple types) are admissible as definitional extensions of plain HOL
- \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not
- required for overloading. Nevertheless, overloaded definitions are
- best applied in the context of type classes.
+ overloaded meta-level constant definitions, where type classes are
+ not yet involved at all. This form of constant definition with
+ overloading (and optional recursion over the syntactic structure of
+ simple types) are admissible as definitional extensions of plain HOL
+ \cite{Wenzel:1997:TPHOL}. The Haskell-style type system is not
+ required for overloading. Nevertheless, overloaded definitions are
+ best applied in the context of type classes.
- \medskip Since we have chosen above $\DEFS$ of the generic group
- operations on type \isa{bool} appropriately, the class membership
- \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.%
+ \medskip Since we have chosen above $\DEFS$ of the generic group
+ operations on type \isa{bool} appropriately, the class membership
+ \isa{bool\ {\isasymColon}\ agroup} may be now derived as follows.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ agroup\isanewline
@@ -337,19 +334,19 @@
\isacommand{qed}\isamarkupfalse%
%
\begin{isamarkuptext}%
-The result of an $\INSTANCE$ statement is both expressed as a theorem
- of Isabelle's meta-logic, and as a type arity of the type signature.
- The latter enables type-inference system to take care of this new
- instance automatically.
+The result of an $\INSTANCE$ statement is both expressed as a
+ theorem of Isabelle's meta-logic, and as a type arity of the type
+ signature. The latter enables type-inference system to take care of
+ this new instance automatically.
- \medskip We could now also instantiate our group theory classes to
- many other concrete types. For example, \isa{int\ {\isasymColon}\ agroup}
- (e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation
- and \isa{{\isasymunit}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}term{\isacharparenright}\ semigroup}
- (e.g.\ if \isa{{\isasymodot}} is defined as list append). Thus, the
- characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymunit}}
- really become overloaded, i.e.\ have different meanings on different
- types.%
+ \medskip We could now also instantiate our group theory classes to
+ many other concrete types. For example, \isa{int\ {\isasymColon}\ agroup}
+ (e.g.\ by defining \isa{{\isasymodot}} as addition, \isa{{\isasyminv}} as negation
+ and \isa{{\isasymunit}} as zero) or \isa{list\ {\isasymColon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup}
+ (e.g.\ if \isa{{\isasymodot}} is defined as list append). Thus, the
+ characteristic constants \isa{{\isasymodot}}, \isa{{\isasyminv}}, \isa{{\isasymunit}}
+ really become overloaded, i.e.\ have different meanings on different
+ types.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -359,14 +356,14 @@
%
\begin{isamarkuptext}%
As already mentioned above, overloading in the simply-typed HOL
- systems may include recursion over the syntactic structure of types.
- That is, definitional equations \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also
- contain constants of name \isa{c} on the right-hand side --- if
- these have types that are structurally simpler than \isa{{\isasymtau}}.
+ systems may include recursion over the syntactic structure of types.
+ That is, definitional equations \isa{c\isactrlsup {\isasymtau}\ {\isasymequiv}\ t} may also
+ contain constants of name \isa{c} on the right-hand side --- if
+ these have types that are structurally simpler than \isa{{\isasymtau}}.
- This feature enables us to \emph{lift operations}, say to Cartesian
- products, direct sums or function spaces. Subsequently we lift
- \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.%
+ This feature enables us to \emph{lift operations}, say to Cartesian
+ products, direct sums or function spaces. Subsequently we lift
+ \isa{{\isasymodot}} component-wise to binary products \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
@@ -374,8 +371,8 @@
%
\begin{isamarkuptext}%
It is very easy to see that associativity of \isa{{\isasymodot}} on \isa{{\isacharprime}a}
- and \isa{{\isasymodot}} on \isa{{\isacharprime}b} transfers to \isa{{\isasymodot}} on \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}. Hence the binary type constructor \isa{{\isasymodot}} maps semigroups to
- semigroups. This may be established formally as follows.%
+ and \isa{{\isasymodot}} on \isa{{\isacharprime}b} transfers to \isa{{\isasymodot}} on \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b}. Hence the binary type constructor \isa{{\isasymodot}} maps semigroups
+ to semigroups. This may be established formally as follows.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{instance}\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
@@ -396,12 +393,13 @@
%
\begin{isamarkuptext}%
Thus, if we view class instances as ``structures'', then overloaded
- constant definitions with recursion over types indirectly provide
- some kind of ``functors'' --- i.e.\ mappings between abstract
- theories.%
+ constant definitions with recursion over types indirectly provide
+ some kind of ``functors'' --- i.e.\ mappings between abstract
+ theories.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{end}\isamarkupfalse%
+\isacommand{end}\isanewline
+\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/AxClass/generated/Product.tex Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/AxClass/generated/Product.tex Sat Dec 01 18:52:32 2001 +0100
@@ -9,50 +9,49 @@
%
\begin{isamarkuptext}%
\medskip\noindent There is still a feature of Isabelle's type system
- left that we have not yet discussed. When declaring polymorphic
- constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}}
- may be constrained by type classes (or even general sorts) in an
- arbitrary way. Note that by default, in Isabelle/HOL the declaration
- \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} is actually an abbreviation for \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}term\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} Since class \isa{term} is the universal
- class of HOL, this is not really a constraint at all.
+ left that we have not yet discussed. When declaring polymorphic
+ constants \isa{c\ {\isasymColon}\ {\isasymsigma}}, the type variables occurring in \isa{{\isasymsigma}}
+ may be constrained by type classes (or even general sorts) in an
+ arbitrary way. Note that by default, in Isabelle/HOL the
+ declaration \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} is actually an abbreviation
+ for \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}type\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} Since class \isa{type} is the
+ universal class of HOL, this is not really a constraint at all.
The \isa{product} class below provides a less degenerate example of
syntactic type classes.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{axclass}\isanewline
-\ \ product\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\ \ product\ {\isasymsubseteq}\ type\isanewline
\isamarkupfalse%
\isacommand{consts}\isanewline
\ \ product\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptext}%
-Here class \isa{product} is defined as subclass of \isa{term}
- without any additional axioms. This effects in logical equivalence
- of \isa{product} and \isa{term}, as is reflected by the trivial
- introduction rule generated for this definition.
+Here class \isa{product} is defined as subclass of \isa{type}
+ without any additional axioms. This effects in logical equivalence
+ of \isa{product} and \isa{type}, as is reflected by the trivial
+ introduction rule generated for this definition.
- \medskip So what is the difference of declaring \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} vs.\ declaring \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}term\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a}
- anyway? In this particular case where \isa{product\ {\isasymequiv}\ term}, it
- should be obvious that both declarations are the same from the
- logic's point of view. It even makes the most sense to remove sort
- constraints from constant declarations, as far as the purely logical
- meaning is concerned \cite{Wenzel:1997:TPHOL}.
+ \medskip So what is the difference of declaring \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}product\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} vs.\ declaring \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}type\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} anyway? In this particular case where \isa{product\ {\isasymequiv}\ type}, it should be obvious that both declarations are the same
+ from the logic's point of view. It even makes the most sense to
+ remove sort constraints from constant declarations, as far as the
+ purely logical meaning is concerned \cite{Wenzel:1997:TPHOL}.
- On the other hand there are syntactic differences, of course.
- Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the
- type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the
- type signature. In our example, this arity may be always added when
- required by means of an $\INSTANCE$ with the default proof $\DDOT$.
+ On the other hand there are syntactic differences, of course.
+ Constants \isa{{\isasymodot}} on some type \isa{{\isasymtau}} are rejected by the
+ type-checker, unless the arity \isa{{\isasymtau}\ {\isasymColon}\ product} is part of the
+ type signature. In our example, this arity may be always added when
+ required by means of an $\INSTANCE$ with the default proof $\DDOT$.
- \medskip Thus, we may observe the following discipline of using
- syntactic classes. Overloaded polymorphic constants have their type
- arguments restricted to an associated (logically trivial) class
- \isa{c}. Only immediately before \emph{specifying} these constants
- on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}.
+ \medskip Thus, we may observe the following discipline of using
+ syntactic classes. Overloaded polymorphic constants have their type
+ arguments restricted to an associated (logically trivial) class
+ \isa{c}. Only immediately before \emph{specifying} these
+ constants on a certain type \isa{{\isasymtau}} do we instantiate \isa{{\isasymtau}\ {\isasymColon}\ c}.
- This is done for class \isa{product} and type \isa{bool} as
- follows.%
+ This is done for class \isa{product} and type \isa{bool} as
+ follows.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{instance}\ bool\ {\isacharcolon}{\isacharcolon}\ product\ \isamarkupfalse%
@@ -85,7 +84,8 @@
``providing operations'' or even ``names of functions''.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{end}\isamarkupfalse%
+\isacommand{end}\isanewline
+\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/AxClass/generated/Semigroups.tex Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/AxClass/generated/Semigroups.tex Sat Dec 01 18:52:32 2001 +0100
@@ -9,51 +9,52 @@
%
\begin{isamarkuptext}%
\medskip\noindent An axiomatic type class is simply a class of types
- that all meet certain properties, which are also called \emph{class
- axioms}. Thus, type classes may be also understood as type predicates
- --- i.e.\ abstractions over a single type argument \isa{{\isacharprime}a}. Class
- axioms typically contain polymorphic constants that depend on this
- type \isa{{\isacharprime}a}. These \emph{characteristic constants} behave like
- operations associated with the ``carrier'' type \isa{{\isacharprime}a}.
+ that all meet certain properties, which are also called \emph{class
+ axioms}. Thus, type classes may be also understood as type
+ predicates --- i.e.\ abstractions over a single type argument \isa{{\isacharprime}a}. Class axioms typically contain polymorphic constants that
+ depend on this type \isa{{\isacharprime}a}. These \emph{characteristic
+ constants} behave like operations associated with the ``carrier''
+ type \isa{{\isacharprime}a}.
- We illustrate these basic concepts by the following formulation of
- semigroups.%
+ We illustrate these basic concepts by the following formulation of
+ semigroups.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isanewline
\ \ times\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymodot}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
\isamarkupfalse%
-\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\isacommand{axclass}\ semigroup\ {\isasymsubseteq}\ type\isanewline
\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymodot}\ y{\isacharparenright}\ {\isasymodot}\ z\ {\isacharequal}\ x\ {\isasymodot}\ {\isacharparenleft}y\ {\isasymodot}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Above we have first declared a polymorphic constant \isa{{\isasymodot}\ {\isasymColon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and then defined the class \isa{semigroup} of
- all types \isa{{\isasymtau}} such that \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is indeed an
- associative operator. The \isa{assoc} axiom contains exactly one
- type variable, which is invisible in the above presentation, though.
- Also note that free term variables (like \isa{x}, \isa{y}, \isa{z}) are allowed for user convenience --- conceptually all of these
- are bound by outermost universal quantifiers.
+ all types \isa{{\isasymtau}} such that \isa{{\isasymodot}\ {\isasymColon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}} is indeed an
+ associative operator. The \isa{assoc} axiom contains exactly one
+ type variable, which is invisible in the above presentation, though.
+ Also note that free term variables (like \isa{x}, \isa{y},
+ \isa{z}) are allowed for user convenience --- conceptually all of
+ these are bound by outermost universal quantifiers.
- \medskip In general, type classes may be used to describe
- \emph{structures} with exactly one carrier \isa{{\isacharprime}a} and a fixed
- \emph{signature}. Different signatures require different classes.
- Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups
- \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would
- correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.%
+ \medskip In general, type classes may be used to describe
+ \emph{structures} with exactly one carrier \isa{{\isacharprime}a} and a fixed
+ \emph{signature}. Different signatures require different classes.
+ Below, class \isa{plus{\isacharunderscore}semigroup} represents semigroups \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymoplus}\isactrlsup {\isasymtau}{\isacharparenright}}, while the original \isa{semigroup} would
+ correspond to semigroups of the form \isa{{\isacharparenleft}{\isasymtau}{\isacharcomma}\ {\isasymodot}\isactrlsup {\isasymtau}{\isacharparenright}}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isanewline
\ \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
\isamarkupfalse%
-\isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ {\isachardoublequote}term{\isachardoublequote}\isanewline
+\isacommand{axclass}\ plus{\isacharunderscore}semigroup\ {\isasymsubseteq}\ type\isanewline
\ \ assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isasymoplus}\ y{\isacharparenright}\ {\isasymoplus}\ z\ {\isacharequal}\ x\ {\isasymoplus}\ {\isacharparenleft}y\ {\isasymoplus}\ z{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Even if classes \isa{plus{\isacharunderscore}semigroup} and \isa{semigroup} both represent semigroups in a sense, they are certainly
- not quite the same.%
+ not quite the same.%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{end}\isamarkupfalse%
+\isacommand{end}\isanewline
+\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
--- a/doc-src/TutorialI/Types/Overloading.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading.thy Sat Dec 01 18:52:32 2001 +0100
@@ -1,13 +1,13 @@
(*<*)theory Overloading = Overloading1:(*>*)
-instance list :: ("term")ordrel
+instance list :: (type)ordrel
by intro_classes
text{*\noindent
This \isacommand{instance} declaration can be read like the declaration of
a function on types. The constructor @{text list} maps types of class @{text
-term} (all HOL types), to types of class @{text ordrel};
+type} (all HOL types), to types of class @{text ordrel};
in other words,
-if @{text"ty :: term"} then @{text"ty list :: ordrel"}.
+if @{text"ty :: type"} then @{text"ty list :: ordrel"}.
Of course we should also define the meaning of @{text <<=} and
@{text <<} on lists:
*}
--- a/doc-src/TutorialI/Types/Overloading1.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading1.thy Sat Dec 01 18:52:32 2001 +0100
@@ -10,13 +10,12 @@
introduce the class @{text ordrel}:
*}
-axclass ordrel < "term"
+axclass ordrel < type
text{*\noindent
This introduces a new class @{text ordrel} and makes it a subclass of
-the predefined class @{text term}, which
-is the class of all HOL types.\footnote{The quotes around @{text term}
-simply avoid the clash with the command \isacommand{term}.}
+the predefined class @{text type}, which
+is the class of all HOL types.
This is a degenerate form of axiomatic type class without any axioms.
Its sole purpose is to restrict the use of overloaded constants to meaningful
instances:
--- a/doc-src/TutorialI/Types/document/Overloading.tex Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading.tex Sat Dec 01 18:52:32 2001 +0100
@@ -2,16 +2,16 @@
\begin{isabellebody}%
\def\isabellecontext{Overloading}%
\isamarkupfalse%
-\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequote}term{\isachardoublequote}{\isacharparenright}ordrel\isanewline
+\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}ordrel\isanewline
\isamarkupfalse%
\isacommand{by}\ intro{\isacharunderscore}classes\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
This \isacommand{instance} declaration can be read like the declaration of
-a function on types. The constructor \isa{list} maps types of class \isa{term} (all HOL types), to types of class \isa{ordrel};
+a function on types. The constructor \isa{list} maps types of class \isa{type} (all HOL types), to types of class \isa{ordrel};
in other words,
-if \isa{ty\ {\isacharcolon}{\isacharcolon}\ term} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}.
+if \isa{ty\ {\isacharcolon}{\isacharcolon}\ type} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}.
Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
\isa{{\isacharless}{\isacharless}} on lists:%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/Types/document/Overloading1.tex Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex Sat Dec 01 18:52:32 2001 +0100
@@ -14,14 +14,13 @@
introduce the class \isa{ordrel}:%
\end{isamarkuptext}%
\isamarkuptrue%
-\isacommand{axclass}\ ordrel\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}\isamarkupfalse%
+\isacommand{axclass}\ ordrel\ {\isacharless}\ type\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
This introduces a new class \isa{ordrel} and makes it a subclass of
-the predefined class \isa{term}, which
-is the class of all HOL types.\footnote{The quotes around \isa{term}
-simply avoid the clash with the command \isacommand{term}.}
+the predefined class \isa{type}, which
+is the class of all HOL types.
This is a degenerate form of axiomatic type class without any axioms.
Its sole purpose is to restrict the use of overloaded constants to meaningful
instances:%
--- a/doc-src/TutorialI/tutorial.ind Sat Dec 01 18:51:46 2001 +0100
+++ b/doc-src/TutorialI/tutorial.ind Sat Dec 01 18:52:32 2001 +0100
@@ -90,7 +90,7 @@
\item bisimulations, 106
\item \isa {blast} (method), 79--80, 82
\item \isa {bool} (type), 4, 5
- \item boolean expressions example, 19--22
+ \item boolean expressions example, 20--22
\item \isa {bspec} (theorem), \bold{98}
\item \isacommand{by} (command), 63
@@ -213,7 +213,7 @@
\item flags, 5, 6, 33
\subitem setting and resetting, 5
\item \isa {force} (method), 81, 82
- \item formulae, 5
+ \item formulae, 5--6
\item forward proof, 82--88
\item \isa {frule} (method), 73
\item \isa {frule_tac} (method), 66
@@ -254,7 +254,7 @@
\item \isa {if} expressions, 5, 6
\subitem simplification of, 33
\subitem splitting of, 31, 49
- \item if-and-only-if, 5
+ \item if-and-only-if, 6
\item \isa {iff} (attribute), 80, 92, 120
\item \isa {iffD1} (theorem), \bold{84}
\item \isa {iffD2} (theorem), \bold{84}
@@ -266,7 +266,7 @@
\item \isa {impI} (theorem), \bold{62}
\item implication, 62--63
\item \isa {ind_cases} (method), 121
- \item \isa {induct_tac} (method), 12, 19, 52, 178
+ \item \isa {induct_tac} (method), 12, 19, 51, 178
\item induction, 174--181
\subitem complete, 176
\subitem deriving new schemas, 178
@@ -326,7 +326,7 @@
\item least number operator, \see{\protect\isa{LEAST}}{75}
\item \isacommand {lemma} (command), 13
\item \isacommand {lemmas} (command), 83, 92
- \item \isa {length} (symbol), 17
+ \item \isa {length} (symbol), 18
\item \isa {length_induct}, \bold{178}
\item \isa {less_than} (constant), 104
\item \isa {less_than_iff} (theorem), \bold{104}
@@ -336,9 +336,10 @@
\item lexicographic product, \bold{105}, 166
\item {\texttt{lfp}}
\subitem applications of, \see{CTL}{106}
+ \item Library, 4
\item linear arithmetic, 22--24, 139
\item \isa {List} (theory), 17
- \item \isa {list} (type), 4, 9, 17
+ \item \isa {list} (type), 5, 9, 17
\item \isa {list.split} (theorem), 32
\item \isa {lists_mono} (theorem), \bold{127}
\item Lowe, Gavin, 184--185
@@ -351,7 +352,7 @@
\item measure functions, 47, 104
\item \isa {measure_def} (theorem), \bold{105}
\item meta-logic, \bold{70}
- \item methods, \bold{15}
+ \item methods, \bold{16}
\item \isa {min} (constant), 23, 24
\item \isa {mod} (symbol), 23
\item \isa {mod_div_equality} (theorem), \bold{141}
@@ -377,8 +378,8 @@
\item negation, 63--65
\item \isa {Nil} (constant), 9
\item \isa {no_asm} (modifier), 29
- \item \isa {no_asm_simp} (modifier), 29
- \item \isa {no_asm_use} (modifier), 29
+ \item \isa {no_asm_simp} (modifier), 30
+ \item \isa {no_asm_use} (modifier), 30
\item non-standard reals, 145
\item \isa {None} (constant), \bold{24}
\item \isa {notE} (theorem), \bold{63}
@@ -426,7 +427,7 @@
\indexspace
- \item quantifiers, 5
+ \item quantifiers, 6
\subitem and inductive definitions, 125--127
\subitem existential, 72
\subitem for sets, 98
@@ -483,7 +484,7 @@
\item \isa {safe} (method), 81, 82
\item safe rules, \bold{80}
- \item \isa {set} (type), 4, 95
+ \item \isa {set} (type), 5, 95
\item set comprehensions, 97--98
\item \isa {set_ext} (theorem), \bold{96}
\item sets, 95--99
@@ -495,7 +496,7 @@
\item \isa {simp} (attribute), 11, 28
\item \isa {simp} (method), \bold{28}
\item \isa {simp} del (attribute), 28
- \item \isa {simp_all} (method), 28, 37
+ \item \isa {simp_all} (method), 29, 37
\item simplification, 27--33, 163--166
\subitem of \isa{let}-expressions, 31
\subitem with definitions, 30
@@ -569,7 +570,7 @@
\item tuples, \see{pairs and tuples}{1}
\item \isacommand {typ} (command), 16
\item type constraints, \bold{6}
- \item type constructors, 4
+ \item type constructors, 5
\item type inference, \bold{5}
\item type synonyms, 25
\item type variables, 5
@@ -597,14 +598,14 @@
\subitem indexed, 98
\item \isa {Union_iff} (theorem), \bold{98}
\item \isa {unit} (type), 24
- \item unknowns, 6, \bold{58}
+ \item unknowns, 7, \bold{58}
\item unsafe rules, \bold{80}
\item updating a function, \bold{99}
\indexspace
- \item variables, 6--7
- \subitem schematic, 6
+ \item variables, 7
+ \subitem schematic, 7
\subitem type, 5
\item \isa {vimage_def} (theorem), \bold{101}
--- a/src/HOL/AxClasses/Group.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/AxClasses/Group.thy Sat Dec 01 18:52:32 2001 +0100
@@ -14,12 +14,12 @@
one :: 'a
-axclass monoid < "term"
+axclass monoid < type
assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
left_unit: "one [*] x = x"
right_unit: "x [*] one = x"
-axclass semigroup < "term"
+axclass semigroup < type
assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
axclass group < semigroup
--- a/src/HOL/AxClasses/Product.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/AxClasses/Product.thy Sat Dec 01 18:52:32 2001 +0100
@@ -6,7 +6,7 @@
theory Product = Main:
-axclass product < "term"
+axclass product < type
consts
product :: "'a::product => 'a => 'a" (infixl "[*]" 70)
--- a/src/HOL/AxClasses/Semigroups.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/AxClasses/Semigroups.thy Sat Dec 01 18:52:32 2001 +0100
@@ -9,14 +9,14 @@
consts
times :: "'a => 'a => 'a" (infixl "[*]" 70)
-axclass semigroup < "term"
+axclass semigroup < type
assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
consts
plus :: "'a => 'a => 'a" (infixl "[+]" 70)
-axclass plus_semigroup < "term"
+axclass plus_semigroup < type
assoc: "(x [+] y) [+] z = x [+] (y [+] z)"
end
--- a/src/HOL/Divides.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Divides.thy Sat Dec 01 18:52:32 2001 +0100
@@ -11,7 +11,7 @@
(*We use the same class for div and mod;
moreover, dvd is defined whenever multiplication is*)
axclass
- div < term
+ div < type
instance nat :: div
instance nat :: plus_ac0 (add_commute,add_assoc,add_0)
--- a/src/HOL/Finite.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Finite.thy Sat Dec 01 18:52:32 2001 +0100
@@ -18,7 +18,7 @@
syntax finite :: 'a set => bool
translations "finite A" == "A : Finites"
-axclass finite<term
+axclass finite < type
finite "finite UNIV"
(* This definition, although traditional, is ugly to work with
--- a/src/HOL/Fun.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Fun.ML Sat Dec 01 18:52:32 2001 +0100
@@ -373,7 +373,7 @@
fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r)
in
val fun_upd2_simproc = Simplifier.mk_simproc "fun_upd2"
- [Thm.read_cterm (sign_of (the_context ())) ("f(v:=w,x:=y)", HOLogic.termT)]
+ [HOLogic.read_cterm (sign_of (the_context ())) "f(v := w, x := y)"]
(fn sg => (K (fn t => case find_double t of (T,None)=> None | (T,Some rhs)=>
Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover))))
end;
--- a/src/HOL/Fun.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Fun.thy Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
Fun = Typedef +
-instance set :: (term) order
+instance set :: (type) order
(subset_refl,subset_trans,subset_antisym,psubset_eq)
consts
fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
--- a/src/HOL/HOL.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/HOL.thy Sat Dec 01 18:52:32 2001 +0100
@@ -13,16 +13,16 @@
subsubsection {* Core syntax *}
-global
+classes type < logic
+defaultsort type
-classes "term" < logic
-defaultsort "term"
+global
typedecl bool
arities
- bool :: "term"
- fun :: ("term", "term") "term"
+ bool :: type
+ fun :: (type, type) type
judgment
Trueprop :: "bool => prop" ("(_)" 5)
@@ -145,12 +145,12 @@
subsubsection {* Generic algebraic operations *}
-axclass zero < "term"
-axclass one < "term"
-axclass plus < "term"
-axclass minus < "term"
-axclass times < "term"
-axclass inverse < "term"
+axclass zero < type
+axclass one < type
+axclass plus < type
+axclass minus < type
+axclass times < type
+axclass inverse < type
global
@@ -528,7 +528,7 @@
subsection {* Order signatures and orders *}
axclass
- ord < "term"
+ ord < type
syntax
"op <" :: "['a::ord, 'a] => bool" ("op <")
--- a/src/HOL/IMP/Com.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/IMP/Com.thy Sat Dec 01 18:52:32 2001 +0100
@@ -16,7 +16,7 @@
aexp = state => val
bexp = state => bool
-arities loc :: term
+arities loc :: type
datatype
com = SKIP
--- a/src/HOL/IMP/Expr.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/IMP/Expr.thy Sat Dec 01 18:52:32 2001 +0100
@@ -15,7 +15,7 @@
n2n = "nat => nat"
n2n2n = "nat => nat => nat"
-arities loc :: term
+arities loc :: type
datatype
aexp = N nat
--- a/src/HOL/IMPP/Com.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/IMPP/Com.thy Sat Dec 01 18:52:32 2001 +0100
@@ -12,7 +12,7 @@
current Isabelle, types cannot be refined later *)
types glb
loc
-arities (*val,*)glb,loc :: term
+arities (*val,*)glb,loc :: type
consts Arg, Res :: loc
datatype vname = Glb glb | Loc loc
@@ -21,14 +21,14 @@
datatype state = st globs locals
(* for the meta theory, the following would be sufficient:
types state
-arities state::term
+arities state::type
consts st:: [globs , locals] => state
*)
types aexp = state => val
bexp = state => bool
types pname
-arities pname :: term
+arities pname :: type
datatype com
= SKIP
--- a/src/HOL/Induct/Com.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Induct/Com.thy Sat Dec 01 18:52:32 2001 +0100
@@ -12,7 +12,7 @@
state = "loc => nat"
n2n2n = "nat => nat => nat"
-arities loc :: term
+arities loc :: type
datatype
exp = N nat
--- a/src/HOL/Integ/Bin.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Integ/Bin.ML Sat Dec 01 18:52:32 2001 +0100
@@ -349,7 +349,7 @@
fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg []
fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc
- fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.termT)
+ fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context())) s
val prep_pats = map prep_pat
fun is_numeral (Const("Numeral.number_of", _) $ w) = true
--- a/src/HOL/Integ/nat_simprocs.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML Sat Dec 01 18:52:32 2001 +0100
@@ -169,8 +169,7 @@
bin_arith_simps @ bin_rel_simps;
fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
-fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
- (s, HOLogic.termT);
+fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s;
val prep_pats = map prep_pat;
--- a/src/HOL/Lattice/Lattice.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Lattice/Lattice.thy Sat Dec 01 18:52:32 2001 +0100
@@ -519,7 +519,7 @@
qed
qed
-instance fun :: ("term", lattice) lattice
+instance fun :: (type, lattice) lattice
proof
fix f g :: "'a \<Rightarrow> 'b::lattice"
show "\<exists>inf. is_inf f g inf" by rule (rule is_inf_fun) (* FIXME @{text "from \<dots> show \<dots> .."} does not work!? unification incompleteness!? *)
--- a/src/HOL/Lattice/Orders.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Lattice/Orders.thy Sat Dec 01 18:52:32 2001 +0100
@@ -18,7 +18,7 @@
required to be related (in either direction).
*}
-axclass leq < "term"
+axclass leq < type
consts
leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool" (infixl "[=" 50)
syntax (xsymbols)
@@ -249,7 +249,7 @@
orders need \emph{not} be linear in general.
*}
-instance fun :: ("term", leq) leq ..
+instance fun :: (type, leq) leq ..
defs (overloaded)
leq_fun_def: "f \<sqsubseteq> g \<equiv> \<forall>x. f x \<sqsubseteq> g x"
@@ -260,7 +260,7 @@
lemma leq_funD [dest?]: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
by (unfold leq_fun_def) blast
-instance fun :: ("term", quasi_order) quasi_order
+instance fun :: (type, quasi_order) quasi_order
proof
fix f g h :: "'a \<Rightarrow> 'b::quasi_order"
show "f \<sqsubseteq> f"
@@ -276,7 +276,7 @@
qed
qed
-instance fun :: ("term", partial_order) partial_order
+instance fun :: (type, partial_order) partial_order
proof
fix f g :: "'a \<Rightarrow> 'b::partial_order"
assume fg: "f \<sqsubseteq> g" and gf: "g \<sqsubseteq> f"
--- a/src/HOL/Library/List_Prefix.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Library/List_Prefix.thy Sat Dec 01 18:52:32 2001 +0100
@@ -13,13 +13,13 @@
subsection {* Prefix order on lists *}
-instance list :: ("term") ord ..
+instance list :: (type) ord ..
defs (overloaded)
prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs"
strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)"
-instance list :: ("term") order
+instance list :: (type) order
by intro_classes (auto simp add: prefix_def strict_prefix_def)
lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys"
--- a/src/HOL/Library/Multiset.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Library/Multiset.thy Sat Dec 01 18:52:32 2001 +0100
@@ -47,9 +47,9 @@
set_of :: "'a multiset => 'a set"
"set_of M == {x. x :# M}"
-instance multiset :: ("term") plus ..
-instance multiset :: ("term") minus ..
-instance multiset :: ("term") zero ..
+instance multiset :: (type) plus ..
+instance multiset :: (type) minus ..
+instance multiset :: (type) zero ..
defs (overloaded)
union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
@@ -114,7 +114,7 @@
theorems union_ac = union_assoc union_commute union_lcomm
-instance multiset :: ("term") plus_ac0
+instance multiset :: (type) plus_ac0
apply intro_classes
apply (rule union_commute)
apply (rule union_assoc)
@@ -660,7 +660,7 @@
subsubsection {* Partial-order properties *}
-instance multiset :: ("term") ord ..
+instance multiset :: (type) ord ..
defs (overloaded)
less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}"
--- a/src/HOL/Library/Quotient.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Library/Quotient.thy Sat Dec 01 18:52:32 2001 +0100
@@ -23,7 +23,7 @@
"\<sim> :: 'a => 'a => bool"}.
*}
-axclass eqv \<subseteq> "term"
+axclass eqv \<subseteq> type
consts
eqv :: "('a::eqv) => 'a => bool" (infixl "\<sim>" 50)
--- a/src/HOL/MicroJava/J/Type.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/MicroJava/J/Type.thy Sat Dec 01 18:52:32 2001 +0100
@@ -11,9 +11,6 @@
typedecl cname (* class name *)
typedecl vnam (* variable or field name *)
typedecl mname (* method name *)
-arities cname :: "term"
- vnam :: "term"
- mname :: "term"
datatype vname (* names for This pointer and local/field variables *)
= This
--- a/src/HOL/MicroJava/J/Value.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/MicroJava/J/Value.thy Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,6 @@
theory Value = Type:
typedecl loc (* locations, i.e. abstract references on objects *)
-arities loc :: "term"
datatype val
= Unit (* dummy result value of void methods *)
--- a/src/HOL/MiniML/Type.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/MiniML/Type.thy Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,7 @@
Type = Maybe +
(* new class for structures containing type variables *)
-axclass type_struct < term
+axclass type_struct < type
(* type expressions *)
@@ -33,7 +33,7 @@
instance typ::type_struct
instance type_scheme::type_struct
instance list::(type_struct)type_struct
-instance fun::(term,type_struct)type_struct
+instance fun::(type,type_struct)type_struct
(* free_tv s: the type variables occuring freely in the type structure s *)
--- a/src/HOL/Nat.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Nat.thy Sat Dec 01 18:52:32 2001 +0100
@@ -19,7 +19,7 @@
instance nat :: linorder (nat_le_linear)
instance nat :: wellorder (wf_less)
-axclass power < term
+axclass power < type
consts
power :: ['a::power, nat] => 'a (infixr "^" 80)
--- a/src/HOL/NatDef.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/NatDef.thy Sat Dec 01 18:52:32 2001 +0100
@@ -12,13 +12,8 @@
(** type ind **)
-global
-
-types
- ind
-
-arities
- ind :: term
+types ind
+arities ind :: type
consts
Zero_Rep :: ind
@@ -43,6 +38,8 @@
Zero_RepI "Zero_Rep : Nat'"
Suc_RepI "i : Nat' ==> Suc_Rep i : Nat'"
+global
+
typedef (Nat)
nat = "Nat'" (Nat'.Zero_RepI)
--- a/src/HOL/Numeral.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Numeral.thy Sat Dec 01 18:52:32 2001 +0100
@@ -14,7 +14,7 @@
| Bit bin bool (infixl "BIT" 90)
axclass
- number < "term" (*for numeric types: nat, int, real, ...*)
+ number < type -- {* for numeric types: nat, int, real, \dots *}
consts
number_of :: "bin => 'a::number"
--- a/src/HOL/Product_Type.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Product_Type.thy Sat Dec 01 18:52:32 2001 +0100
@@ -342,8 +342,8 @@
(cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
(K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
val sign = sign_of (the_context ());
- fun simproc name patstr = Simplifier.mk_simproc name
- [Thm.read_cterm sign (patstr, HOLogic.termT)];
+ fun simproc name patstr =
+ Simplifier.mk_simproc name [HOLogic.read_cterm sign patstr];
val beta_patstr = "split f z";
val eta_patstr = "split f";
--- a/src/HOL/Prolog/Func.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Prolog/Func.thy Sat Dec 01 18:52:32 2001 +0100
@@ -4,7 +4,7 @@
types tm
-arities tm :: term
+arities tm :: type
consts abs :: (tm => tm) => tm
app :: tm => tm => tm
--- a/src/HOL/Prolog/Test.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Prolog/Test.thy Sat Dec 01 18:52:32 2001 +0100
@@ -3,10 +3,10 @@
Test = HOHH +
types nat
-arities nat :: term
+arities nat :: type
types 'a list
-arities list :: (term) term
+arities list :: (type) type
consts Nil :: 'a list ("[]")
Cons :: 'a => 'a list => 'a list (infixr "#" 65)
@@ -20,7 +20,7 @@
"[x]" == "x#[]"
types person
-arities person :: term
+arities person :: type
consts
append :: ['a list, 'a list, 'a list] => bool
--- a/src/HOL/Prolog/Type.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Prolog/Type.thy Sat Dec 01 18:52:32 2001 +0100
@@ -4,7 +4,7 @@
types ty
-arities ty :: term
+arities ty :: type
consts bool :: ty
nat :: ty
--- a/src/HOL/Real/RealBin.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Real/RealBin.ML Sat Dec 01 18:52:32 2001 +0100
@@ -403,7 +403,7 @@
real_mult_0, real_mult_0_right, real_mult_1, real_mult_1_right];
fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
-fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT);
+fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s;
val prep_pats = map prep_pat;
structure CancelNumeralsCommon =
--- a/src/HOL/Relation_Power.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Relation_Power.thy Sat Dec 01 18:52:32 2001 +0100
@@ -15,7 +15,7 @@
Relation_Power = Nat +
instance
- set :: (term) {power} (* only ('a * 'a) set should be in power! *)
+ set :: (type) power (* only ('a * 'a) set should be in power! *)
primrec (relpow)
"R^0 = Id"
@@ -23,7 +23,7 @@
instance
- fun :: (term,term)power (* only 'a => 'a should be in power! *)
+ fun :: (type, type) power (* only 'a => 'a should be in power! *)
primrec (funpow)
"f^0 = id"
--- a/src/HOL/Set.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Set.thy Sat Dec 01 18:52:32 2001 +0100
@@ -17,7 +17,7 @@
global
typedecl 'a set
-arities set :: ("term") "term"
+arities set :: (type) type
consts
"{}" :: "'a set" ("{}")
@@ -42,8 +42,8 @@
local
-instance set :: ("term") ord ..
-instance set :: ("term") minus ..
+instance set :: (type) ord ..
+instance set :: (type) minus ..
subsection {* Additional concrete syntax *}
--- a/src/HOL/TLA/Init.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/TLA/Init.thy Sat Dec 01 18:52:32 2001 +0100
@@ -17,7 +17,7 @@
temporal = behavior form
arities
- behavior :: term
+ behavior :: type
instance
behavior :: world
--- a/src/HOL/TLA/Intensional.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/TLA/Intensional.thy Sat Dec 01 18:52:32 2001 +0100
@@ -13,12 +13,12 @@
Intensional = Main +
axclass
- world < term
+ world < type
(** abstract syntax **)
types
- ('w,'a) expr = 'w => 'a (* intention: 'w::world, 'a::term *)
+ ('w,'a) expr = 'w => 'a (* intention: 'w::world, 'a::type *)
'w form = ('w, bool) expr
consts
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy Sat Dec 01 18:52:32 2001 +0100
@@ -21,7 +21,7 @@
('a,'r) channel = (PrIds => ('a,'r) chan) stfun
arities
- chan :: (term,term) term
+ chan :: (type,type) type
consts
(* data-level functions *)
--- a/src/HOL/TLA/Stfun.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/TLA/Stfun.thy Sat Dec 01 18:52:32 2001 +0100
@@ -17,7 +17,7 @@
stpred = "bool stfun"
arities
- state :: term
+ state :: type
instance
state :: world
--- a/src/HOL/Tools/datatype_abs_proofs.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Sat Dec 01 18:52:32 2001 +0100
@@ -120,7 +120,7 @@
(1 upto (length descr'))));
val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
- replicate (length descr') HOLogic.termS);
+ replicate (length descr') HOLogic.typeS);
val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
@@ -302,7 +302,7 @@
val recTs = get_rec_types descr' sorts;
val used = foldr add_typ_tfree_names (recTs, []);
val newTs = take (length (hd descr), recTs);
- val T' = TFree (variant used "'t", HOLogic.termS);
+ val T' = TFree (variant used "'t", HOLogic.typeS);
fun mk_dummyT (DtRec _) = T'
| mk_dummyT (DtType ("fun", [T, _])) = typ_of_dtyp descr' sorts T --> T'
--- a/src/HOL/Tools/datatype_package.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Tools/datatype_package.ML Sat Dec 01 18:52:32 2001 +0100
@@ -365,7 +365,7 @@
| _ => None)
| distinct_proc sg _ _ = None;
-val distinct_pats = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s = t", HOLogic.termT)];
+val distinct_pats = [HOLogic.read_cterm (Theory.sign_of HOL.thy) "s = t"];
val distinct_simproc = mk_simproc distinctN distinct_pats distinct_proc;
val dist_ss = HOL_ss addsimprocs [distinct_simproc];
@@ -460,7 +460,7 @@
(constrs ~~ constr_syntax')) ((hd descr) ~~ newTs ~~ constr_syntax);
val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
- replicate (length descr') HOLogic.termS);
+ replicate (length descr') HOLogic.typeS);
val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
@@ -484,7 +484,7 @@
val size_names = DatatypeProp.indexify_names
(map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs)));
- val freeT = TFree (variant used "'t", HOLogic.termS);
+ val freeT = TFree (variant used "'t", HOLogic.typeS);
val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
let val Ts = map (typ_of_dtyp descr' sorts) cargs
--- a/src/HOL/Tools/datatype_prop.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Tools/datatype_prop.ML Sat Dec 01 18:52:32 2001 +0100
@@ -177,7 +177,7 @@
val used = foldr add_typ_tfree_names (recTs, []);
val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
- replicate (length descr') HOLogic.termS);
+ replicate (length descr') HOLogic.typeS);
val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
@@ -241,7 +241,7 @@
val recTs = get_rec_types descr' sorts;
val used = foldr add_typ_tfree_names (recTs, []);
val newTs = take (length (hd descr), recTs);
- val T' = TFree (variant used "'t", HOLogic.termS);
+ val T' = TFree (variant used "'t", HOLogic.typeS);
val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
@@ -326,7 +326,7 @@
val recTs = get_rec_types descr' sorts;
val used' = foldr add_typ_tfree_names (recTs, []);
val newTs = take (length (hd descr), recTs);
- val T' = TFree (variant used' "'t", HOLogic.termS);
+ val T' = TFree (variant used' "'t", HOLogic.typeS);
val P = Free ("P", T' --> HOLogic.boolT);
fun make_split (((_, (_, _, constrs)), T), comb_t) =
--- a/src/HOL/Tools/inductive_package.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Tools/inductive_package.ML Sat Dec 01 18:52:32 2001 +0100
@@ -838,7 +838,7 @@
fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =
let
val sign = Theory.sign_of thy;
- val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
+ val cs = map (term_of o HOLogic.read_cterm sign) c_strings;
val intr_names = map (fst o fst) intro_srcs;
fun read_rule s = Thm.read_cterm sign (s, propT)
--- a/src/HOL/Tools/record_package.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Tools/record_package.ML Sat Dec 01 18:52:32 2001 +0100
@@ -493,7 +493,7 @@
local
-val sel_upd_pat = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s (u k r)", HOLogic.termT)];
+val sel_upd_pat = [HOLogic.read_cterm (Theory.sign_of HOL.thy) "s (u k r)"];
fun proc sg _ t =
(case t of (sel as Const (s, _)) $ ((upd as Const (u, _)) $ k $ r) =>
@@ -560,7 +560,7 @@
fun field_typedefs zeta moreT names theory =
let
val alpha = "'a";
- val aT = TFree (alpha, HOLogic.termS);
+ val aT = TFree (alpha, HOLogic.typeS);
val UNIV = HOLogic.mk_UNIV (HOLogic.mk_prodT (aT, moreT));
fun type_def (thy, name) =
@@ -581,7 +581,7 @@
val base = Sign.base_name;
val full_path = Sign.full_name_path sign;
- val xT = TFree (variant alphas "'x", HOLogic.termS);
+ val xT = TFree (variant alphas "'x", HOLogic.typeS);
(* prepare declarations and definitions *)
@@ -683,7 +683,7 @@
val all_named_vars = parent_named_vars @ named_vars;
val zeta = variant alphas "'z";
- val moreT = TFree (zeta, HOLogic.termS);
+ val moreT = TFree (zeta, HOLogic.typeS);
val more = Free (moreN, moreT);
val full_moreN = full moreN;
fun more_part t = mk_more t full_moreN;
--- a/src/HOL/Tools/typedef_package.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Tools/typedef_package.ML Sat Dec 01 18:52:32 2001 +0100
@@ -58,7 +58,7 @@
val full = Sign.full_name (Theory.sign_of thy);
fun arity_of (raw_name, args, mx) =
- (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.termS, HOLogic.termS);
+ (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.typeS, HOLogic.typeS);
in
if can (Theory.assert_super HOL.thy) thy then
thy
@@ -97,7 +97,7 @@
(* prepare_typedef *)
fun read_term sg used s =
- #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termT));
+ #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.typeT));
fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg;
@@ -125,7 +125,7 @@
val goal_pat = mk_nonempty (Var (vname, setT));
(*lhs*)
- val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs;
+ val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.typeS)) vs;
val tname = Syntax.type_name t mx;
val full_tname = full tname;
val newT = Type (full_tname, map TFree lhs_tfrees);
@@ -162,7 +162,9 @@
fun make th = Drule.standard (th OF [type_definition]);
val (theory'', [Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
Rep_cases, Abs_cases, Rep_induct, Abs_induct]) =
- theory' |> PureThy.add_thms
+ theory'
+ |> Theory.add_path name
+ |> PureThy.add_thms
([((Rep_name, make Rep), []),
((Rep_name ^ "_inverse", make Rep_inverse), []),
((Abs_name ^ "_inverse", make Abs_inverse), []),
@@ -175,7 +177,8 @@
((Rep_name ^ "_induct", make Rep_induct),
[RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
((Abs_name ^ "_induct", make Abs_induct),
- [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])]);
+ [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])])
+ |>> Theory.parent_path;
val result = {type_definition = type_definition, set_def = set_def,
Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
--- a/src/HOL/UNITY/Comp.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/Comp.thy Sat Dec 01 18:52:32 2001 +0100
@@ -16,7 +16,7 @@
Comp = Union +
instance
- program :: (term)ord
+ program :: (type) ord
defs
component_def "F <= H == EX G. F Join G = H"
--- a/src/HOL/UNITY/Comp/Counterc.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/Comp/Counterc.thy Sat Dec 01 18:52:32 2001 +0100
@@ -13,7 +13,7 @@
Counterc = Comp +
types state
-arities state :: term
+arities state :: type
consts
C :: "state=>int"
--- a/src/HOL/UNITY/Comp/PriorityAux.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/Comp/PriorityAux.thy Sat Dec 01 18:52:32 2001 +0100
@@ -6,10 +6,10 @@
Auxiliary definitions needed in Priority.thy
*)
-PriorityAux = Main +
+PriorityAux = Main +
types vertex
-arities vertex::term
+arities vertex :: type
constdefs
(* symmetric closure: removes the orientation of a relation *)
--- a/src/HOL/UNITY/Extend.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/Extend.ML Sat Dec 01 18:52:32 2001 +0100
@@ -125,7 +125,7 @@
(** A sequence of proof steps borrowed from Provers/split_paired_all.ML **)
-val cT = TFree ("'c", ["term"]);
+val cT = TFree ("'c", HOLogic.typeS);
(* "PROP P x == PROP P (h (f x, g x))" *)
val lemma1 = Thm.combination
--- a/src/HOL/UNITY/GenPrefix.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/GenPrefix.thy Sat Dec 01 18:52:32 2001 +0100
@@ -27,7 +27,7 @@
append "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)"
-instance list :: (term)ord
+instance list :: (type)ord
defs
prefix_def "xs <= zs == (xs,zs) : genPrefix Id"
--- a/src/HOL/UNITY/Guar.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/Guar.thy Sat Dec 01 18:52:32 2001 +0100
@@ -20,7 +20,7 @@
Guar = Comp +
-instance program :: (term) order
+instance program :: (type) order
(component_refl, component_trans, component_antisym,
program_less_le)
--- a/src/HOL/UNITY/ListOrder.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/ListOrder.thy Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
ListOrder = GenPrefix +
-instance list :: (term) order
+instance list :: (type) order
(prefix_refl,prefix_trans,prefix_antisym,prefix_less_le)
end
--- a/src/HOL/UNITY/Simple/Reach.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/UNITY/Simple/Reach.thy Sat Dec 01 18:52:32 2001 +0100
@@ -11,7 +11,7 @@
types vertex
state = "vertex=>bool"
-arities vertex :: term
+arities vertex :: type
consts
init :: "vertex"
--- a/src/HOL/W0/Type.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/W0/Type.thy Sat Dec 01 18:52:32 2001 +0100
@@ -10,7 +10,7 @@
(* new class for structures containing type variables *)
classes
- type_struct < term
+ type_struct < type
(* type expressions *)
datatype
@@ -23,7 +23,7 @@
arities
typ::type_struct
list::(type_struct)type_struct
- fun::(term,type_struct)type_struct
+ fun::(type,type_struct)type_struct
(* substitutions *)
--- a/src/HOL/arith_data.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/arith_data.ML Sat Dec 01 18:52:32 2001 +0100
@@ -138,8 +138,7 @@
(** prepare nat_cancel simprocs **)
-fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
- (s, HOLogic.termT);
+fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s;
val prep_pats = map prep_pat;
fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
--- a/src/HOL/ex/MT.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/ex/MT.thy Sat Dec 01 18:52:32 2001 +0100
@@ -31,19 +31,19 @@
TyEnv
arities
- Const :: term
+ Const :: type
- ExVar :: term
- Ex :: term
+ ExVar :: type
+ Ex :: type
- TyConst :: term
- Ty :: term
+ TyConst :: type
+ Ty :: type
- Clos :: term
- Val :: term
+ Clos :: type
+ Val :: type
- ValEnv :: term
- TyEnv :: term
+ ValEnv :: type
+ TyEnv :: type
consts
c_app :: [Const, Const] => Const
--- a/src/HOL/ex/PER.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/ex/PER.thy Sat Dec 01 18:52:32 2001 +0100
@@ -8,39 +8,40 @@
theory PER = Main:
text {*
- Higher-order quotients are defined over partial equivalence relations
- (PERs) instead of total ones. We provide axiomatic type classes
- @{text "equiv < partial_equiv"} and a type constructor
- @{text "'a quot"} with basic operations. This development is based
- on:
+ Higher-order quotients are defined over partial equivalence
+ relations (PERs) instead of total ones. We provide axiomatic type
+ classes @{text "equiv < partial_equiv"} and a type constructor
+ @{text "'a quot"} with basic operations. This development is based
+ on:
- Oscar Slotosch: \emph{Higher Order Quotients and their Implementation
- in Isabelle HOL.} Elsa L. Gunter and Amy Felty, editors, Theorem
- Proving in Higher Order Logics: TPHOLs '97, Springer LNCS 1275, 1997.
+ Oscar Slotosch: \emph{Higher Order Quotients and their
+ Implementation in Isabelle HOL.} Elsa L. Gunter and Amy Felty,
+ editors, Theorem Proving in Higher Order Logics: TPHOLs '97,
+ Springer LNCS 1275, 1997.
*}
subsection {* Partial equivalence *}
text {*
- Type class @{text partial_equiv} models partial equivalence relations
- (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation,
- which is required to be symmetric and transitive, but not necessarily
- reflexive.
+ Type class @{text partial_equiv} models partial equivalence
+ relations (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a =>
+ bool"} relation, which is required to be symmetric and transitive,
+ but not necessarily reflexive.
*}
consts
eqv :: "'a => 'a => bool" (infixl "\<sim>" 50)
-axclass partial_equiv < "term"
+axclass partial_equiv < type
partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
text {*
- \medskip The domain of a partial equivalence relation is the set of
- reflexive elements. Due to symmetry and transitivity this
- characterizes exactly those elements that are connected with
- \emph{any} other one.
+ \medskip The domain of a partial equivalence relation is the set of
+ reflexive elements. Due to symmetry and transitivity this
+ characterizes exactly those elements that are connected with
+ \emph{any} other one.
*}
constdefs
@@ -64,9 +65,9 @@
subsection {* Equivalence on function spaces *}
text {*
- The @{text \<sim>} relation is lifted to function spaces. It is
- important to note that this is \emph{not} the direct product, but a
- structural one corresponding to the congruence property.
+ The @{text \<sim>} relation is lifted to function spaces. It is
+ important to note that this is \emph{not} the direct product, but a
+ structural one corresponding to the congruence property.
*}
defs (overloaded)
@@ -81,8 +82,8 @@
by (unfold eqv_fun_def) blast
text {*
- The class of partial equivalence relations is closed under function
- spaces (in \emph{both} argument positions).
+ The class of partial equivalence relations is closed under function
+ spaces (in \emph{both} argument positions).
*}
instance fun :: (partial_equiv, partial_equiv) partial_equiv
@@ -113,18 +114,18 @@
subsection {* Total equivalence *}
text {*
- The class of total equivalence relations on top of PERs. It
- coincides with the standard notion of equivalence, i.e.\
- @{text "\<sim> :: 'a => 'a => bool"} is required to be reflexive, transitive
- and symmetric.
+ The class of total equivalence relations on top of PERs. It
+ coincides with the standard notion of equivalence, i.e.\ @{text "\<sim>
+ :: 'a => 'a => bool"} is required to be reflexive, transitive and
+ symmetric.
*}
axclass equiv < partial_equiv
eqv_refl [intro]: "x \<sim> x"
text {*
- On total equivalences all elements are reflexive, and congruence
- holds unconditionally.
+ On total equivalences all elements are reflexive, and congruence
+ holds unconditionally.
*}
theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain"
@@ -145,8 +146,8 @@
subsection {* Quotient types *}
text {*
- The quotient type @{text "'a quot"} consists of all \emph{equivalence
- classes} over elements of the base type @{typ 'a}.
+ The quotient type @{text "'a quot"} consists of all
+ \emph{equivalence classes} over elements of the base type @{typ 'a}.
*}
typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}"
@@ -159,8 +160,8 @@
by (unfold quot_def) blast
text {*
- \medskip Abstracted equivalence classes are the canonical
- representation of elements of a quotient type.
+ \medskip Abstracted equivalence classes are the canonical
+ representation of elements of a quotient type.
*}
constdefs
@@ -183,8 +184,8 @@
subsection {* Equality on quotients *}
text {*
- Equality of canonical quotient elements corresponds to the original
- relation as follows.
+ Equality of canonical quotient elements corresponds to the original
+ relation as follows.
*}
theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
--- a/src/HOL/hologic.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/hologic.ML Sat Dec 01 18:52:32 2001 +0100
@@ -7,9 +7,9 @@
signature HOLOGIC =
sig
- val termC: class
- val termS: sort
- val termT: typ
+ val typeS: sort
+ val typeT: typ
+ val read_cterm: Sign.sg -> string -> cterm
val boolN: string
val boolT: typ
val false_const: term
@@ -80,11 +80,12 @@
structure HOLogic: HOLOGIC =
struct
-(* basics *)
+(* HOL syntax *)
-val termC: class = "term";
-val termS: sort = [termC];
-val termT = TypeInfer.anyT termS;
+val typeS: sort = ["HOL.type"];
+val typeT = TypeInfer.anyT typeS;
+
+fun read_cterm sg s = Thm.read_cterm sg (s, typeT);
(* bool and set *)
--- a/src/HOLCF/Discrete.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Discrete.ML Sat Dec 01 18:52:32 2001 +0100
@@ -10,11 +10,11 @@
Addsimps [undiscr_Discr];
Goal
- "!!S::nat=>('a::term)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
+ "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
qed "discr_chain_f_range0";
-Goalw [cont,is_lub_def,is_ub_def] "cont(%x::('a::term)discr. f x)";
+Goalw [cont,is_lub_def,is_ub_def] "cont(%x::('a::type)discr. f x)";
by (simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
qed "cont_discr";
AddIffs [cont_discr];
--- a/src/HOLCF/Discrete.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Discrete.thy Sat Dec 01 18:52:32 2001 +0100
@@ -8,10 +8,10 @@
Discrete = Discrete1 +
-instance discr :: (term)cpo (discr_cpo)
+instance discr :: (type)cpo (discr_cpo)
constdefs
- undiscr :: ('a::term)discr => 'a
+ undiscr :: ('a::type)discr => 'a
"undiscr x == (case x of Discr y => y)"
end
--- a/src/HOLCF/Discrete0.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Discrete0.ML Sat Dec 01 18:52:32 2001 +0100
@@ -6,17 +6,17 @@
Proves that 'a discr is a po
*)
-Goalw [less_discr_def] "(x::('a::term)discr) << x";
+Goalw [less_discr_def] "(x::('a::type)discr) << x";
by (rtac refl 1);
qed "less_discr_refl";
Goalw [less_discr_def]
- "!!x. [| (x::('a::term)discr) << y; y << z |] ==> x << z";
+ "!!x. [| (x::('a::type)discr) << y; y << z |] ==> x << z";
by (etac trans 1);
by (assume_tac 1);
qed "less_discr_trans";
Goalw [less_discr_def]
- "!!x. [| (x::('a::term)discr) << y; y << x |] ==> x=y";
+ "!!x. [| (x::('a::type)discr) << y; y << x |] ==> x=y";
by (assume_tac 1);
qed "less_discr_antisym";
--- a/src/HOLCF/Discrete0.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Discrete0.thy Sat Dec 01 18:52:32 2001 +0100
@@ -8,11 +8,11 @@
Discrete0 = Cont + Datatype +
-datatype 'a discr = Discr "'a :: term"
+datatype 'a discr = Discr "'a :: type"
-instance discr :: (term)sq_ord
+instance discr :: (type) sq_ord
defs
-less_discr_def "((op <<)::('a::term)discr=>'a discr=>bool) == op ="
+less_discr_def "((op <<)::('a::type)discr=>'a discr=>bool) == op ="
end
--- a/src/HOLCF/Discrete1.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Discrete1.ML Sat Dec 01 18:52:32 2001 +0100
@@ -6,13 +6,13 @@
Proves that 'a discr is a cpo
*)
-Goalw [less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
+Goalw [less_discr_def] "((x::('a::type)discr) << y) = (x=y)";
by (rtac refl 1);
qed "discr_less_eq";
AddIffs [discr_less_eq];
Goalw [chain_def]
- "!!S::nat=>('a::term)discr. chain S ==> S i = S 0";
+ "!!S::nat=>('a::type)discr. chain S ==> S i = S 0";
by (induct_tac "i" 1);
by (rtac refl 1);
by (etac subst 1);
@@ -21,12 +21,12 @@
qed "discr_chain0";
Goal
- "!!S::nat=>('a::term)discr. chain(S) ==> range(S) = {S 0}";
+ "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}";
by (fast_tac (claset() addEs [discr_chain0]) 1);
qed "discr_chain_range0";
Addsimps [discr_chain_range0];
Goalw [is_lub_def,is_ub_def]
- "!!S. chain S ==> ? x::('a::term)discr. range(S) <<| x";
+ "!!S. chain S ==> ? x::('a::type)discr. range(S) <<| x";
by (Asm_simp_tac 1);
qed "discr_cpo";
--- a/src/HOLCF/Discrete1.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Discrete1.thy Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
Discrete1 = Discrete0 +
-instance discr :: (term)po
+instance discr :: (type) po
(less_discr_refl,less_discr_trans,less_discr_antisym)
end
--- a/src/HOLCF/FOCUS/Buffer.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/FOCUS/Buffer.thy Sat Dec 01 18:52:32 2001 +0100
@@ -21,7 +21,7 @@
Buffer = FOCUS +
types D
-arities D::term
+arities D :: type
datatype
--- a/src/HOLCF/FOCUS/Fstream.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/FOCUS/Fstream.thy Sat Dec 01 18:52:32 2001 +0100
@@ -10,7 +10,7 @@
Fstream = Stream +
-default term
+default type
types 'a fstream = ('a lift) stream
--- a/src/HOLCF/Fun1.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Fun1.ML Sat Dec 01 18:52:32 2001 +0100
@@ -10,19 +10,19 @@
(* less_fun is a partial order on 'a => 'b *)
(* ------------------------------------------------------------------------ *)
-val prems = goalw thy [less_fun_def] "(f::'a::term =>'b::po) << f";
+val prems = goalw thy [less_fun_def] "(f::'a::type =>'b::po) << f";
by (fast_tac (HOL_cs addSIs [refl_less]) 1);
qed "refl_less_fun";
val prems = goalw Fun1.thy [less_fun_def]
- "[|(f1::'a::term =>'b::po) << f2; f2 << f1|] ==> f1 = f2";
+ "[|(f1::'a::type =>'b::po) << f2; f2 << f1|] ==> f1 = f2";
by (cut_facts_tac prems 1);
by (stac expand_fun_eq 1);
by (fast_tac (HOL_cs addSIs [antisym_less]) 1);
qed "antisym_less_fun";
val prems = goalw Fun1.thy [less_fun_def]
- "[|(f1::'a::term =>'b::po) << f2; f2 << f3 |] ==> f1 << f3";
+ "[|(f1::'a::type =>'b::po) << f2; f2 << f3 |] ==> f1 << f3";
by (cut_facts_tac prems 1);
by (strip_tac 1);
by (rtac trans_less 1);
--- a/src/HOLCF/Fun1.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Fun1.thy Sat Dec 01 18:52:32 2001 +0100
@@ -13,7 +13,7 @@
instance flat<chfin (flat_imp_chfin)
(* to make << defineable: *)
-instance fun :: (term,sq_ord)sq_ord
+instance fun :: (type, sq_ord) sq_ord
defs
less_fun_def "(op <<) == (%f1 f2.!x. f1 x << f2 x)"
--- a/src/HOLCF/Fun2.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Fun2.ML Sat Dec 01 18:52:32 2001 +0100
@@ -2,8 +2,6 @@
ID: $Id$
Author: Franz Regensburger
License: GPL (GNU GENERAL PUBLIC LICENSE)
-
-Class Instance =>::(term,po)po
*)
(* for compatibility with old HOLCF-Version *)
@@ -13,7 +11,7 @@
qed "inst_fun_po";
(* ------------------------------------------------------------------------ *)
-(* Type 'a::term => 'b::pcpo is pointed *)
+(* Type 'a::type => 'b::pcpo is pointed *)
(* ------------------------------------------------------------------------ *)
Goal "(%z. UU) << x";
@@ -48,7 +46,7 @@
(* upper bounds of function chains yield upper bound in the po range *)
(* ------------------------------------------------------------------------ *)
-Goal "range(S::nat=>('a::term => 'b::po)) <| u ==> range(%i. S i x) <| u(x)";
+Goal "range(S::nat=>('a::type => 'b::po)) <| u ==> range(%i. S i x) <| u(x)";
by (rtac ub_rangeI 1);
by (dtac ub_rangeD 1);
by (asm_full_simp_tac (simpset() addsimps [less_fun]) 1);
@@ -56,10 +54,10 @@
qed "ub2ub_fun";
(* ------------------------------------------------------------------------ *)
-(* Type 'a::term => 'b::pcpo is chain complete *)
+(* Type 'a::type => 'b::pcpo is chain complete *)
(* ------------------------------------------------------------------------ *)
-Goal "chain(S::nat=>('a::term => 'b::cpo)) ==> \
+Goal "chain(S::nat=>('a::type => 'b::cpo)) ==> \
\ range(S) <<| (% x. lub(range(% i. S(i)(x))))";
by (rtac is_lubI 1);
by (rtac ub_rangeI 1);
@@ -78,7 +76,7 @@
bind_thm ("thelub_fun", lub_fun RS thelubI);
(* chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
-Goal "chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x";
+Goal "chain(S::nat=>('a::type => 'b::cpo)) ==> ? x. range(S) <<| x";
by (rtac exI 1);
by (etac lub_fun 1);
qed "cpo_fun";
--- a/src/HOLCF/Fun2.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Fun2.thy Sat Dec 01 18:52:32 2001 +0100
@@ -2,15 +2,13 @@
ID: $Id$
Author: Franz Regensburger
License: GPL (GNU GENERAL PUBLIC LICENSE)
-
-Class Instance =>::(term,po)po
*)
Fun2 = Fun1 +
-(* default class is still term !*)
+(* default class is still type!*)
-instance fun :: (term,po)po (refl_less_fun,antisym_less_fun,trans_less_fun)
+instance fun :: (type, po) po (refl_less_fun,antisym_less_fun,trans_less_fun)
end
--- a/src/HOLCF/Fun3.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Fun3.thy Sat Dec 01 18:52:32 2001 +0100
@@ -8,10 +8,10 @@
Fun3 = Fun2 +
-(* default class is still term *)
+(* default class is still type *)
-instance fun :: (term,cpo)cpo (cpo_fun)
-instance fun :: (term,pcpo)pcpo (least_fun)
+instance fun :: (type, cpo) cpo (cpo_fun)
+instance fun :: (type, pcpo)pcpo (least_fun)
end
--- a/src/HOLCF/IMP/Denotational.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IMP/Denotational.thy Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,7 @@
Denotational = HOLCF + Natural +
constdefs
- dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)"
+ dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)"
"dlift f == (LAM x. case x of UU => UU | Def(y) => f$(Discr y))"
consts D :: "com => state discr -> state lift"
--- a/src/HOLCF/IOA/NTP/Multiset.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/NTP/Multiset.thy Sat Dec 01 18:52:32 2001 +0100
@@ -15,7 +15,7 @@
arities
- multiset :: (term) term
+ multiset :: (type) type
consts
--- a/src/HOLCF/IOA/Storage/Correctness.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/Storage/Correctness.thy Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
Correctness = SimCorrectness + Spec + Impl +
-default term
+default type
consts
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,7 @@
Abstraction = LiveIOA +
-default term
+default type
consts
--- a/src/HOLCF/IOA/meta_theory/Automata.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,7 @@
Automata = Option + Asig + Inductive +
-default term
+default type
types
('a,'s)transition = "'s * 'a * 's"
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
LiveIOA = TLS +
-default term
+default type
types
--- a/src/HOLCF/IOA/meta_theory/Pred.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
Pred = Main +
-default term
+default type
types
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
RefMappings = Traces +
-default term
+default type
consts
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Sat Dec 01 18:52:32 2001 +0100
@@ -8,9 +8,9 @@
Sequence = Seq +
-default term
+default type
-types 'a Seq = ('a::term lift)seq
+types 'a Seq = ('a::type lift)seq
consts
@@ -89,5 +89,4 @@
(* for test purposes should be deleted FIX !! *)
adm_all "adm f"
-
-end
\ No newline at end of file
+end
--- a/src/HOLCF/IOA/meta_theory/Simulations.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Simulations.thy Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
Simulations = RefCorrectness +
-default term
+default type
consts
--- a/src/HOLCF/IOA/meta_theory/TL.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.thy Sat Dec 01 18:52:32 2001 +0100
@@ -8,7 +8,7 @@
TL = Pred + Sequence +
-default term
+default type
types
--- a/src/HOLCF/IOA/meta_theory/TLS.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,7 @@
TLS = IOA + TL +
-default term
+default type
types
--- a/src/HOLCF/IOA/meta_theory/Traces.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,7 @@
Traces = Sequence + Automata +
-default term
+default type
types
('a,'s)pairs = "('a * 's) Seq"
--- a/src/HOLCF/Lift.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Lift.thy Sat Dec 01 18:52:32 2001 +0100
@@ -4,11 +4,11 @@
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
-header {* Lifting types of class term to flat pcpo's *}
+header {* Lifting types of class type to flat pcpo's *}
theory Lift = Cprod3:
-defaultsort "term"
+defaultsort type
typedef 'a lift = "UNIV :: 'a option set" ..
@@ -19,12 +19,12 @@
Def :: "'a => 'a lift"
"Def x == Abs_lift (Some x)"
-instance lift :: ("term") sq_ord ..
+instance lift :: (type) sq_ord ..
defs (overloaded)
less_lift_def: "x << y == (x=y | x=Undef)"
-instance lift :: ("term") po
+instance lift :: (type) po
proof
fix x y z :: "'a lift"
show "x << x" by (unfold less_lift_def) blast
@@ -111,7 +111,7 @@
apply (blast intro: lub_finch1)
done
-instance lift :: ("term") pcpo
+instance lift :: (type) pcpo
apply intro_classes
apply (erule cpo_lift)
apply (rule least_lift)
@@ -153,7 +153,7 @@
consts
flift1 :: "('a => 'b::pcpo) => ('a lift -> 'b)"
flift2 :: "('a => 'b) => ('a lift -> 'b lift)"
- liftpair ::"'a::term lift * 'b::term lift => ('a * 'b) lift"
+ liftpair ::"'a::type lift * 'b::type lift => ('a * 'b) lift"
defs
flift1_def:
@@ -219,7 +219,7 @@
subsection {* Lift is flat *}
-instance lift :: ("term") flat
+instance lift :: (type) flat
proof
show "ALL x y::'a lift. x << y --> x = UU | x = y"
by (simp add: less_lift)
--- a/src/HOLCF/Porder.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Porder.thy Sat Dec 01 18:52:32 2001 +0100
@@ -18,8 +18,7 @@
finite_chain :: "(nat=>'a::po)=>bool"
syntax
-
- "@LUB" :: "(('b::term) => 'a) => 'a" (binder "LUB " 10)
+ "@LUB" :: "('b => 'a) => 'a" (binder "LUB " 10)
translations
--- a/src/HOLCF/Porder0.thy Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Porder0.thy Sat Dec 01 18:52:32 2001 +0100
@@ -9,7 +9,7 @@
Porder0 = Main +
(* introduce a (syntactic) class for the constant << *)
-axclass sq_ord<term
+axclass sq_ord < type
(* characteristic constant << for po *)
consts