--- a/src/HOL/Complex/Complex.thy Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Complex/Complex.thy Sat May 01 22:01:57 2004 +0200
@@ -11,13 +11,7 @@
datatype complex = Complex real real
-instance complex :: zero ..
-instance complex :: one ..
-instance complex :: plus ..
-instance complex :: times ..
-instance complex :: minus ..
-instance complex :: inverse ..
-instance complex :: power ..
+instance complex :: "{zero, one, plus, times, minus, inverse, power}" ..
consts
"ii" :: complex ("\<i>")
--- a/src/HOL/Complex/NSComplex.thy Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Complex/NSComplex.thy Sat May 01 22:01:57 2004 +0200
@@ -17,13 +17,7 @@
typedef hcomplex = "{x::nat=>complex. True}//hcomplexrel"
by (auto simp add: quotient_def)
-instance hcomplex :: zero ..
-instance hcomplex :: one ..
-instance hcomplex :: plus ..
-instance hcomplex :: times ..
-instance hcomplex :: minus ..
-instance hcomplex :: inverse ..
-instance hcomplex :: power ..
+instance hcomplex :: "{zero, one, plus, times, minus, inverse, power}" ..
defs (overloaded)
hcomplex_zero_def:
--- a/src/HOL/Hyperreal/HyperDef.thy Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Sat May 01 22:01:57 2004 +0200
@@ -23,14 +23,7 @@
typedef hypreal = "UNIV//hyprel"
by (auto simp add: quotient_def)
-instance hypreal :: ord ..
-instance hypreal :: zero ..
-instance hypreal :: one ..
-instance hypreal :: plus ..
-instance hypreal :: times ..
-instance hypreal :: minus ..
-instance hypreal :: inverse ..
-
+instance hypreal :: "{ord, zero, one, plus, times, minus, inverse}" ..
defs (overloaded)
@@ -58,10 +51,10 @@
hypreal_of_real :: "real => hypreal"
"hypreal_of_real r == Abs_hypreal(hyprel``{%n::nat. r})"
- omega :: hypreal (*an infinite number = [<1,2,3,...>] *)
+ omega :: hypreal -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
"omega == Abs_hypreal(hyprel``{%n::nat. real (Suc n)})"
- epsilon :: hypreal (*an infinitesimal number = [<1,1/2,1/3,...>] *)
+ epsilon :: hypreal -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
"epsilon == Abs_hypreal(hyprel``{%n::nat. inverse (real (Suc n))})"
syntax (xsymbols)
@@ -341,9 +334,9 @@
by (cases z, simp add: hypreal_zero_def hypreal_add)
instance hypreal :: plus_ac0
- by (intro_classes,
- (assumption |
- rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+)
+ by intro_classes
+ (assumption |
+ rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+
lemma hypreal_add_zero_right [simp]: "z + (0::hypreal) = z"
by (simp add: hypreal_add_zero_left hypreal_add_commute)
@@ -502,9 +495,9 @@
by (simp add: hypreal_less_def)
instance hypreal :: order
-proof qed
- (assumption |
- rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym hypreal_less_le)+
+ by intro_classes
+ (assumption |
+ rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym hypreal_less_le)+
(* Axiom 'linorder_linear' of class 'linorder': *)
@@ -514,7 +507,7 @@
done
instance hypreal :: linorder
- by (intro_classes, rule hypreal_le_linear)
+ by intro_classes (rule hypreal_le_linear)
lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
by (auto simp add: order_less_irrefl)
--- a/src/HOL/Hyperreal/HyperNat.thy Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy Sat May 01 22:01:57 2004 +0200
@@ -17,12 +17,7 @@
typedef hypnat = "UNIV//hypnatrel"
by (auto simp add: quotient_def)
-instance hypnat :: ord ..
-instance hypnat :: zero ..
-instance hypnat :: one ..
-instance hypnat :: plus ..
-instance hypnat :: times ..
-instance hypnat :: minus ..
+instance hypnat :: "{ord, zero, one, plus, times, minus}" ..
consts whn :: hypnat
@@ -164,9 +159,9 @@
done
instance hypnat :: plus_ac0
- by (intro_classes,
- (assumption |
- rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+)
+ by intro_classes
+ (assumption |
+ rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+
subsection{*Subtraction inverse on @{typ hypreal}*}
@@ -332,9 +327,9 @@
by (simp add: hypnat_less_def)
instance hypnat :: order
-proof qed
- (assumption |
- rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+
+ by intro_classes
+ (assumption |
+ rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+
(* Axiom 'linorder_linear' of class 'linorder': *)
lemma hypnat_le_linear: "(z::hypnat) \<le> w | w \<le> z"
@@ -343,7 +338,7 @@
done
instance hypnat :: linorder
- by (intro_classes, rule hypnat_le_linear)
+ by intro_classes (rule hypnat_le_linear)
lemma hypnat_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypnat)"
apply (cases x, cases y, cases z)
--- a/src/HOL/Integ/IntDef.thy Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy Sat May 01 22:01:57 2004 +0200
@@ -18,15 +18,9 @@
int = "UNIV//intrel"
by (auto simp add: quotient_def)
-instance int :: ord ..
-instance int :: zero ..
-instance int :: one ..
-instance int :: plus ..
-instance int :: times ..
-instance int :: minus ..
+instance int :: "{ord, zero, one, plus, times, minus}" ..
constdefs
-
int :: "nat => int"
"int m == Abs_Integ(intrel `` {(m,0)})"
@@ -279,16 +273,16 @@
by (simp add: less_int_def)
instance int :: order
-proof qed
- (assumption |
- rule zle_refl zle_trans zle_anti_sym zless_le)+
+ by intro_classes
+ (assumption |
+ rule zle_refl zle_trans zle_anti_sym zless_le)+
(* Axiom 'linorder_linear' of class 'linorder': *)
lemma zle_linear: "(z::int) \<le> w | w \<le> z"
-by (cases z, cases w, simp add: le linorder_linear)
+by (cases z, cases w) (simp add: le linorder_linear)
instance int :: linorder
-proof qed (rule zle_linear)
+ by intro_classes (rule zle_linear)
lemmas zless_linear = linorder_less_linear [where 'a = int]
--- a/src/HOL/Library/Multiset.thy Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Library/Multiset.thy Sat May 01 22:01:57 2004 +0200
@@ -46,9 +46,7 @@
set_of :: "'a multiset => 'a set"
"set_of M == {x. x :# M}"
-instance multiset :: (type) plus ..
-instance multiset :: (type) minus ..
-instance multiset :: (type) zero ..
+instance multiset :: (type) "{plus, minus, zero}" ..
defs (overloaded)
union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
--- a/src/HOL/Library/Nat_Infinity.thy Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Sat May 01 22:01:57 2004 +0200
@@ -21,8 +21,7 @@
datatype inat = Fin nat | Infty
-instance inat :: ord ..
-instance inat :: zero ..
+instance inat :: "{ord, zero}" ..
consts
iSuc :: "inat => inat"
--- a/src/HOL/Matrix/Matrix.thy Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Matrix/Matrix.thy Sat May 01 22:01:57 2004 +0200
@@ -20,11 +20,8 @@
axclass matrix_element < almost_matrix_element
matrix_add_0[simp]: "0+0 = 0"
-instance matrix :: (plus) plus
-by (intro_classes)
-
-instance matrix :: (times) times
-by (intro_classes)
+instance matrix :: (plus) plus ..
+instance matrix :: (times) times ..
defs (overloaded)
plus_matrix_def: "A + B == combine_matrix (op +) A B"
@@ -127,7 +124,7 @@
g_add_leftimp_eq: "a+b = a+c \<Longrightarrow> b = c"
instance g_almost_semiring < matrix_element
-by (intro_classes, simp)
+ by intro_classes simp
instance semiring < g_semiring
apply (intro_classes)
@@ -197,8 +194,7 @@
apply (intro_classes)
by (simp_all add: add_right_mono mult_right_mono mult_left_mono)
-instance matrix :: (pordered_g_semiring) pordered_g_semiring
-by (intro_classes)
+instance matrix :: (pordered_g_semiring) pordered_g_semiring ..
lemma nrows_mult: "nrows ((A::('a::matrix_element) matrix) * B) <= nrows A"
by (simp add: times_matrix_def mult_nrows)
--- a/src/HOL/Matrix/MatrixGeneral.thy Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy Sat May 01 22:01:57 2004 +0200
@@ -746,7 +746,7 @@
qed
-instance matrix :: (zero)zero by intro_classes
+instance matrix :: (zero) zero ..
defs(overloaded)
zero_matrix_def: "(0::('a::zero) matrix) == Abs_matrix(% j i. 0)"
@@ -1183,7 +1183,7 @@
apply (rule ext)+
by (simp! add: Rep_mult_matrix max_ac)
-instance matrix :: ("{ord,zero}") ord by intro_classes
+instance matrix :: ("{ord, zero}") ord ..
defs (overloaded)
le_matrix_def: "(A::('a::{ord,zero}) matrix) <= B == ! j i. (Rep_matrix A j i) <= (Rep_matrix B j i)"
--- a/src/HOL/Nat.thy Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Nat.thy Sat May 01 22:01:57 2004 +0200
@@ -41,9 +41,7 @@
typedef (open Nat)
nat = Nat by (rule exI, rule Nat.Zero_RepI)
-instance nat :: ord ..
-instance nat :: zero ..
-instance nat :: one ..
+instance nat :: "{ord, zero, one}" ..
text {* Abstract constants and syntax *}
@@ -462,16 +460,14 @@
text {* Type {@typ nat} is a wellfounded linear order *}
-instance nat :: order by (intro_classes,
- (assumption | rule le_refl le_trans le_anti_sym nat_less_le)+)
-instance nat :: linorder by (intro_classes, rule nat_le_linear)
-instance nat :: wellorder by (intro_classes, rule wf_less)
-
+instance nat :: "{order, linorder, wellorder}"
+ by intro_classes
+ (assumption |
+ rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
by (blast elim!: less_SucE)
-
text {*
Rewrite @{term "n < Suc m"} to @{term "n = m"}
if @{term "~ n < m"} or @{term "m \<le> n"} hold.
@@ -506,10 +502,7 @@
text {* arithmetic operators @{text "+ -"} and @{text "*"} *}
-instance nat :: plus ..
-instance nat :: minus ..
-instance nat :: times ..
-instance nat :: power ..
+instance nat :: "{plus, minus, times, power}" ..
text {* size of a datatype value; overloaded *}
consts size :: "'a => nat"
--- a/src/HOL/Real/PReal.thy Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Real/PReal.thy Sat May 01 22:01:57 2004 +0200
@@ -50,12 +50,7 @@
typedef preal = "{A. cut A}"
by (blast intro: cut_of_rat [OF zero_less_one])
-instance preal :: ord ..
-instance preal :: plus ..
-instance preal :: minus ..
-instance preal :: times ..
-instance preal :: inverse ..
-
+instance preal :: "{ord, plus, minus, times, inverse}" ..
constdefs
preal_of_rat :: "rat => preal"
@@ -211,9 +206,9 @@
by (simp add: preal_le_def preal_less_def Rep_preal_inject psubset_def)
instance preal :: order
-proof qed
- (assumption |
- rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
+ by intro_classes
+ (assumption |
+ rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
lemma preal_imp_pos: "[|A \<in> preal; r \<in> A|] ==> 0 < r"
by (insert preal_imp_psubset_positives, blast)
@@ -226,7 +221,7 @@
done
instance preal :: linorder
- by (intro_classes, rule preal_le_linear)
+ by intro_classes (rule preal_le_linear)
--- a/src/HOL/Real/Rational.thy Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Real/Rational.thy Sat May 01 22:01:57 2004 +0200
@@ -4,10 +4,7 @@
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
-header {*
- \title{Rational numbers}
- \author{Markus Wenzel}
-*}
+header {* Rational numbers *}
theory Rational = Quotient + Main
files ("rat_arith.ML"):
@@ -117,13 +114,7 @@
to equivalence of fractions.
*}
-instance fraction :: zero ..
-instance fraction :: one ..
-instance fraction :: plus ..
-instance fraction :: minus ..
-instance fraction :: times ..
-instance fraction :: inverse ..
-instance fraction :: ord ..
+instance fraction :: "{zero, one, plus, minus, times, inverse, ord}" ..
defs (overloaded)
zero_fraction_def: "0 == fract 0 1"
@@ -354,13 +345,7 @@
subsubsection {* Standard operations on rational numbers *}
-instance rat :: zero ..
-instance rat :: one ..
-instance rat :: plus ..
-instance rat :: minus ..
-instance rat :: times ..
-instance rat :: inverse ..
-instance rat :: ord ..
+instance rat :: "{zero, one, plus, minus, times, inverse, ord}" ..
defs (overloaded)
zero_rat_def: "0 == rat_of 0"
@@ -369,7 +354,7 @@
minus_rat_def: "-q == rat_of (-(fraction_of q))"
diff_rat_def: "q - r == q + (-(r::rat))"
mult_rat_def: "q * r == rat_of (fraction_of q * fraction_of r)"
- inverse_rat_def: "inverse q ==
+ inverse_rat_def: "inverse q ==
if q=0 then 0 else rat_of (inverse (fraction_of q))"
divide_rat_def: "q / r == q * inverse (r::rat)"
le_rat_def: "q \<le> r == fraction_of q \<le> fraction_of r"
@@ -377,7 +362,7 @@
abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)"
theorem zero_rat: "0 = Fract 0 1"
- by (simp add: zero_rat_def zero_fraction_def rat_of_def Fract_def)
+ by (simp add: zero_rat_def zero_fraction_def rat_of_def Fract_def)
theorem one_rat: "1 = Fract 1 1"
by (simp add: one_rat_def one_fraction_def rat_of_def Fract_def)
@@ -470,14 +455,14 @@
theorem abs_rat: "b \<noteq> 0 ==> \<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
by (simp add: abs_rat_def minus_rat zero_rat less_rat eq_rat)
- (auto simp add: mult_less_0_iff zero_less_mult_iff order_le_less
+ (auto simp add: mult_less_0_iff zero_less_mult_iff order_le_less
split: abs_split)
subsubsection {* The ordered field of rational numbers *}
lemma rat_add_assoc: "(q + r) + s = q + (r + (s::rat))"
- by (induct q, induct r, induct s)
+ by (induct q, induct r, induct s)
(simp add: add_rat add_ac mult_ac int_distrib)
lemma rat_add_0: "0 + q = (q::rat)"
@@ -507,14 +492,14 @@
show "1 * q = q"
by (induct q) (simp add: one_rat mult_rat)
show "(q + r) * s = q * s + r * s"
- by (induct q, induct r, induct s)
+ by (induct q, induct r, induct s)
(simp add: add_rat mult_rat eq_rat int_distrib)
show "q \<noteq> 0 ==> inverse q * q = 1"
by (induct q) (simp add: inverse_rat mult_rat one_rat zero_rat eq_rat)
show "q / r = q * inverse r"
- by (simp add: divide_rat_def)
+ by (simp add: divide_rat_def)
show "0 \<noteq> (1::rat)"
- by (simp add: zero_rat one_rat eq_rat)
+ by (simp add: zero_rat one_rat eq_rat)
qed
instance rat :: linorder
@@ -638,7 +623,7 @@
subsection {* Various Other Results *}
lemma minus_rat_cancel [simp]: "b \<noteq> 0 ==> Fract (-a) (-b) = Fract a b"
-by (simp add: Fract_equality eq_fraction_iff)
+by (simp add: Fract_equality eq_fraction_iff)
theorem Rat_induct_pos [case_names Fract, induct type: rat]:
assumes step: "!!a b. 0 < b ==> P (Fract a b)"
@@ -658,44 +643,43 @@
lemma zero_less_Fract_iff:
"0 < b ==> (0 < Fract a b) = (0 < a)"
-by (simp add: zero_rat less_rat order_less_imp_not_eq2 zero_less_mult_iff)
+by (simp add: zero_rat less_rat order_less_imp_not_eq2 zero_less_mult_iff)
lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1"
apply (insert add_rat [of concl: m n 1 1])
-apply (simp add: one_rat [symmetric])
+apply (simp add: one_rat [symmetric])
done
lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
-apply (induct k)
-apply (simp add: zero_rat)
-apply (simp add: Fract_add_one)
+apply (induct k)
+apply (simp add: zero_rat)
+apply (simp add: Fract_add_one)
done
lemma Fract_of_int_eq: "Fract k 1 = of_int k"
-proof (cases k rule: int_cases)
+proof (cases k rule: int_cases)
case (nonneg n)
thus ?thesis by (simp add: int_eq_of_nat Fract_of_nat_eq)
-next
+next
case (neg n)
hence "Fract k 1 = - (Fract (of_nat (Suc n)) 1)"
- by (simp only: minus_rat int_eq_of_nat)
+ by (simp only: minus_rat int_eq_of_nat)
also have "... = - (of_nat (Suc n))"
by (simp only: Fract_of_nat_eq)
- finally show ?thesis
- by (simp add: only: prems int_eq_of_nat of_int_minus of_int_of_nat_eq)
-qed
+ finally show ?thesis
+ by (simp add: only: prems int_eq_of_nat of_int_minus of_int_of_nat_eq)
+qed
-
-subsection{*Numerals and Arithmetic*}
+subsection {* Numerals and Arithmetic *}
instance rat :: number ..
-primrec (*the type constraint is essential!*)
+primrec -- {* the type constraint is essential! *}
number_of_Pls: "number_of bin.Pls = 0"
number_of_Min: "number_of bin.Min = - (1::rat)"
number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
- (number_of w) + (number_of w)"
+ (number_of w) + (number_of w)"
declare number_of_Pls [simp del]
number_of_Min [simp del]
--- a/src/HOL/Real/RealDef.thy Sat May 01 21:59:12 2004 +0200
+++ b/src/HOL/Real/RealDef.thy Sat May 01 22:01:57 2004 +0200
@@ -17,13 +17,7 @@
typedef (Real) real = "UNIV//realrel"
by (auto simp add: quotient_def)
-instance real :: ord ..
-instance real :: zero ..
-instance real :: one ..
-instance real :: plus ..
-instance real :: times ..
-instance real :: minus ..
-instance real :: inverse ..
+instance real :: "{ord, zero, one, plus, times, minus, inverse}" ..
constdefs
@@ -41,6 +35,9 @@
(*overloaded constant for injecting other types into "real"*)
real :: "'a => real"
+syntax (xsymbols)
+ Reals :: "'a set" ("\<real>")
+
defs (overloaded)
@@ -83,9 +80,6 @@
real_abs_def: "abs (r::real) == (if 0 \<le> r then r else -r)"
-syntax (xsymbols)
- Reals :: "'a set" ("\<real>")
-
subsection{*Proving that realrel is an equivalence relation*}