--- a/src/HOL/Isar_Examples/Group.thy Tue Feb 23 10:11:15 2010 +0100
+++ b/src/HOL/Isar_Examples/Group.thy Tue Feb 23 10:11:15 2010 +0100
@@ -17,15 +17,12 @@
$\idt{times}$ is provided by the basic HOL theory.
*}
-consts
- one :: "'a"
- inverse :: "'a => 'a"
+notation Groups.one ("one")
-axclass
- group < times
- group_assoc: "(x * y) * z = x * (y * z)"
- group_left_one: "one * x = x"
- group_left_inverse: "inverse x * x = one"
+class group = times + one + inverse +
+ assumes group_assoc: "(x * y) * z = x * (y * z)"
+ assumes group_left_one: "one * x = x"
+ assumes group_left_inverse: "inverse x * x = one"
text {*
The group axioms only state the properties of left one and inverse,
@@ -144,10 +141,10 @@
\idt{one} :: \alpha)$ are defined like this.
*}
-axclass monoid < times
- monoid_assoc: "(x * y) * z = x * (y * z)"
- monoid_left_one: "one * x = x"
- monoid_right_one: "x * one = x"
+class monoid = times + one +
+ assumes monoid_assoc: "(x * y) * z = x * (y * z)"
+ assumes monoid_left_one: "one * x = x"
+ assumes monoid_right_one: "x * one = x"
text {*
Groups are \emph{not} yet monoids directly from the definition. For
--- a/src/HOL/Lattice/Bounds.thy Tue Feb 23 10:11:15 2010 +0100
+++ b/src/HOL/Lattice/Bounds.thy Tue Feb 23 10:11:15 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Lattice/Bounds.thy
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
*)
--- a/src/HOL/Lattice/CompleteLattice.thy Tue Feb 23 10:11:15 2010 +0100
+++ b/src/HOL/Lattice/CompleteLattice.thy Tue Feb 23 10:11:15 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Lattice/CompleteLattice.thy
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
*)
@@ -16,8 +15,8 @@
bounds (see \S\ref{sec:connect-bounds}).
*}
-axclass complete_lattice \<subseteq> partial_order
- ex_Inf: "\<exists>inf. is_Inf A inf"
+class complete_lattice =
+ assumes ex_Inf: "\<exists>inf. is_Inf A inf"
theorem ex_Sup: "\<exists>sup::'a::complete_lattice. is_Sup A sup"
proof -
--- a/src/HOL/Lattice/Lattice.thy Tue Feb 23 10:11:15 2010 +0100
+++ b/src/HOL/Lattice/Lattice.thy Tue Feb 23 10:11:15 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Lattice/Lattice.thy
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
*)
@@ -15,9 +14,9 @@
as well).
*}
-axclass lattice \<subseteq> partial_order
- ex_inf: "\<exists>inf. is_inf x y inf"
- ex_sup: "\<exists>sup. is_sup x y sup"
+class lattice =
+ assumes ex_inf: "\<exists>inf. is_inf x y inf"
+ assumes ex_sup: "\<exists>sup. is_sup x y sup"
text {*
The @{text \<sqinter>} (meet) and @{text \<squnion>} (join) operations select such
--- a/src/HOL/Lattice/Orders.thy Tue Feb 23 10:11:15 2010 +0100
+++ b/src/HOL/Lattice/Orders.thy Tue Feb 23 10:11:15 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Lattice/Orders.thy
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
*)
@@ -18,21 +17,21 @@
required to be related (in either direction).
*}
-axclass leq < type
-consts
- leq :: "'a::leq \<Rightarrow> 'a \<Rightarrow> bool" (infixl "[=" 50)
+class leq =
+ fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "[=" 50)
+
notation (xsymbols)
leq (infixl "\<sqsubseteq>" 50)
-axclass quasi_order < leq
- leq_refl [intro?]: "x \<sqsubseteq> x"
- leq_trans [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
+class quasi_order = leq +
+ assumes leq_refl [intro?]: "x \<sqsubseteq> x"
+ assumes leq_trans [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
-axclass partial_order < quasi_order
- leq_antisym [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
+class partial_order = quasi_order +
+ assumes leq_antisym [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
-axclass linear_order < partial_order
- leq_linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
+class linear_order = partial_order +
+ assumes leq_linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
lemma linear_order_cases:
"((x::'a::linear_order) \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> (y \<sqsubseteq> x \<Longrightarrow> C) \<Longrightarrow> C"
@@ -54,11 +53,16 @@
primrec
undual_dual: "undual (dual x) = x"
-instance dual :: (leq) leq ..
+instantiation dual :: (leq) leq
+begin
-defs (overloaded)
+definition
leq_dual_def: "x' \<sqsubseteq> y' \<equiv> undual y' \<sqsubseteq> undual x'"
+instance ..
+
+end
+
lemma undual_leq [iff?]: "(undual x' \<sqsubseteq> undual y') = (y' \<sqsubseteq> x')"
by (simp add: leq_dual_def)
@@ -192,11 +196,16 @@
\emph{not} be linear in general.
*}
-instance * :: (leq, leq) leq ..
+instantiation * :: (leq, leq) leq
+begin
-defs (overloaded)
+definition
leq_prod_def: "p \<sqsubseteq> q \<equiv> fst p \<sqsubseteq> fst q \<and> snd p \<sqsubseteq> snd q"
+instance ..
+
+end
+
lemma leq_prodI [intro?]:
"fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> p \<sqsubseteq> q"
by (unfold leq_prod_def) blast
@@ -249,11 +258,16 @@
orders need \emph{not} be linear in general.
*}
-instance "fun" :: (type, leq) leq ..
+instantiation "fun" :: (type, leq) leq
+begin
-defs (overloaded)
+definition
leq_fun_def: "f \<sqsubseteq> g \<equiv> \<forall>x. f x \<sqsubseteq> g x"
+instance ..
+
+end
+
lemma leq_funI [intro?]: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
by (unfold leq_fun_def) blast