--- a/src/HOL/Complex/Complex.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Complex/Complex.thy Fri Dec 07 15:07:59 2007 +0100
@@ -33,19 +33,24 @@
subsection {* Addition and Subtraction *}
-instance complex :: zero
- complex_zero_def:
- "0 \<equiv> Complex 0 0" ..
+instantiation complex :: "{zero, plus, minus}"
+begin
+
+definition
+ complex_zero_def: "0 = Complex 0 0"
+
+definition
+ complex_add_def: "x + y = Complex (Re x + Re y) (Im x + Im y)"
-instance complex :: plus
- complex_add_def:
- "x + y \<equiv> Complex (Re x + Re y) (Im x + Im y)" ..
+definition
+ complex_minus_def: "- x = Complex (- Re x) (- Im x)"
-instance complex :: minus
- complex_minus_def:
- "- x \<equiv> Complex (- Re x) (- Im x)"
- complex_diff_def:
- "x - (y\<Colon>complex) \<equiv> x + - y" ..
+definition
+ complex_diff_def: "x - (y\<Colon>complex) = x + - y"
+
+instance ..
+
+end
lemma Complex_eq_0 [simp]: "(Complex a b = 0) = (a = 0 \<and> b = 0)"
by (simp add: complex_zero_def)
@@ -103,20 +108,26 @@
subsection {* Multiplication and Division *}
-instance complex :: one
- complex_one_def:
- "1 \<equiv> Complex 1 0" ..
+instantiation complex :: "{one, times, inverse}"
+begin
+
+definition
+ complex_one_def: "1 = Complex 1 0"
+
+definition
+ complex_mult_def: "x * y =
+ Complex (Re x * Re y - Im x * Im y) (Re x * Im y + Im x * Re y)"
-instance complex :: times
- complex_mult_def:
- "x * y \<equiv> Complex (Re x * Re y - Im x * Im y) (Re x * Im y + Im x * Re y)" ..
+definition
+ complex_inverse_def: "inverse x =
+ Complex (Re x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>)) (- Im x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>))"
-instance complex :: inverse
- complex_inverse_def:
- "inverse x \<equiv>
- Complex (Re x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>)) (- Im x / ((Re x)\<twosuperior> + (Im x)\<twosuperior>))"
- complex_divide_def:
- "x / (y\<Colon>complex) \<equiv> x * inverse y" ..
+definition
+ complex_divide_def: "x / (y\<Colon>complex) = x * inverse y"
+
+instance ..
+
+end
lemma Complex_eq_1 [simp]: "(Complex a b = 1) = (a = 1 \<and> b = 0)"
by (simp add: complex_one_def)
@@ -193,12 +204,16 @@
subsection {* Numerals and Arithmetic *}
-instance complex :: number
- complex_number_of_def:
- "number_of w \<equiv> of_int w \<Colon> complex" ..
+instantiation complex :: number_ring
+begin
-instance complex :: number_ring
-by (intro_classes, simp only: complex_number_of_def)
+definition
+ complex_number_of_def: "number_of w = (of_int w \<Colon> complex)"
+
+instance
+ by (intro_classes, simp only: complex_number_of_def)
+
+end
lemma complex_Re_of_nat [simp]: "Re (of_nat n) = of_nat n"
by (induct n) simp_all
@@ -225,9 +240,15 @@
subsection {* Scalar Multiplication *}
-instance complex :: scaleR
- complex_scaleR_def:
- "scaleR r x \<equiv> Complex (r * Re x) (r * Im x)" ..
+instantiation complex :: scaleR
+begin
+
+definition
+ complex_scaleR_def: "scaleR r x = Complex (r * Re x) (r * Im x)"
+
+instance ..
+
+end
lemma complex_scaleR [simp]:
"scaleR r (Complex a b) = Complex (r * a) (r * b)"
@@ -291,16 +312,29 @@
subsection {* Vector Norm *}
-instance complex :: norm
- complex_norm_def:
- "norm z \<equiv> sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)" ..
+instantiation complex :: norm
+begin
+
+definition
+ complex_norm_def: "norm z = sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
+
+instance ..
+
+end
abbreviation
cmod :: "complex \<Rightarrow> real" where
"cmod \<equiv> norm"
-instance complex :: sgn
- complex_sgn_def: "sgn x == x /\<^sub>R cmod x" ..
+instantiation complex :: sgn
+begin
+
+definition
+ complex_sgn_def: "sgn x = x /\<^sub>R cmod x"
+
+instance ..
+
+end
lemmas cmod_def = complex_norm_def
--- a/src/HOL/Divides.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Divides.thy Fri Dec 07 15:07:59 2007 +0100
@@ -15,11 +15,20 @@
fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
-instance nat :: Divides.div
+instantiation nat :: Divides.div
+begin
+
+definition
div_def: "m div n == wfrec (pred_nat^+)
(%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
+
+definition
mod_def: "m mod n == wfrec (pred_nat^+)
- (%f j. if j<n | n=0 then j else f (j-n)) m" ..
+ (%f j. if j<n | n=0 then j else f (j-n)) m"
+
+instance ..
+
+end
definition (in div)
dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50)
--- a/src/HOL/Finite_Set.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Finite_Set.thy Fri Dec 07 15:07:59 2007 +0100
@@ -2665,32 +2665,48 @@
lemma univ_unit [noatp]:
"UNIV = {()}" by auto
-instance unit :: finite
- "Finite_Set.itself \<equiv> TYPE(unit)"
-proof
+instantiation unit :: finite
+begin
+
+definition
+ "itself = TYPE(unit)"
+
+instance proof
have "finite {()}" by simp
also note univ_unit [symmetric]
finally show "finite (UNIV :: unit set)" .
qed
+end
+
lemmas [code func] = univ_unit
lemma univ_bool [noatp]:
"UNIV = {False, True}" by auto
-instance bool :: finite
- "itself \<equiv> TYPE(bool)"
-proof
+instantiation bool :: finite
+begin
+
+definition
+ "itself = TYPE(bool)"
+
+instance proof
have "finite {False, True}" by simp
also note univ_bool [symmetric]
finally show "finite (UNIV :: bool set)" .
qed
+end
+
lemmas [code func] = univ_bool
-instance * :: (finite, finite) finite
- "itself \<equiv> TYPE('a \<times> 'b)"
-proof
+instantiation * :: (finite, finite) finite
+begin
+
+definition
+ "itself = TYPE('a \<times> 'b)"
+
+instance proof
show "finite (UNIV :: ('a \<times> 'b) set)"
proof (rule finite_Prod_UNIV)
show "finite (UNIV :: 'a set)" by (rule finite)
@@ -2698,13 +2714,19 @@
qed
qed
+end
+
lemma univ_prod [noatp, code func]:
"UNIV = (UNIV \<Colon> 'a\<Colon>finite set) \<times> (UNIV \<Colon> 'b\<Colon>finite set)"
unfolding UNIV_Times_UNIV ..
-instance "+" :: (finite, finite) finite
- "itself \<equiv> TYPE('a + 'b)"
-proof
+instantiation "+" :: (finite, finite) finite
+begin
+
+definition
+ "itself = TYPE('a + 'b)"
+
+instance proof
have a: "finite (UNIV :: 'a set)" by (rule finite)
have b: "finite (UNIV :: 'b set)" by (rule finite)
from a b have "finite ((UNIV :: 'a set) <+> (UNIV :: 'b set))"
@@ -2712,28 +2734,40 @@
thus "finite (UNIV :: ('a + 'b) set)" by simp
qed
+end
+
lemma univ_sum [noatp, code func]:
"UNIV = (UNIV \<Colon> 'a\<Colon>finite set) <+> (UNIV \<Colon> 'b\<Colon>finite set)"
unfolding UNIV_Plus_UNIV ..
-instance set :: (finite) finite
- "itself \<equiv> TYPE('a set)"
-proof
+instantiation set :: (finite) finite
+begin
+
+definition
+ "itself = TYPE('a set)"
+
+instance proof
have "finite (UNIV :: 'a set)" by (rule finite)
hence "finite (Pow (UNIV :: 'a set))"
by (rule finite_Pow_iff [THEN iffD2])
thus "finite (UNIV :: 'a set set)" by simp
qed
+end
+
lemma univ_set [noatp, code func]:
"UNIV = Pow (UNIV \<Colon> 'a\<Colon>finite set)" unfolding Pow_UNIV ..
lemma inj_graph: "inj (%f. {(x, y). y = f x})"
by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
-instance "fun" :: (finite, finite) finite
+instantiation "fun" :: (finite, finite) finite
+begin
+
+definition
"itself \<equiv> TYPE('a \<Rightarrow> 'b)"
-proof
+
+instance proof
show "finite (UNIV :: ('a => 'b) set)"
proof (rule finite_imageD)
let ?graph = "%f::'a => 'b. {(x, y). y = f x}"
@@ -2742,6 +2776,8 @@
qed
qed
+end
+
hide (open) const itself
subsection {* Equality and order on functions *}
--- a/src/HOL/Hyperreal/StarClasses.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Hyperreal/StarClasses.thy Fri Dec 07 15:07:59 2007 +0100
@@ -11,45 +11,137 @@
subsection {* Syntactic classes *}
-instance star :: (zero) zero
- star_zero_def: "0 \<equiv> star_of 0" ..
+instantiation star :: (zero) zero
+begin
+
+definition
+ star_zero_def: "0 \<equiv> star_of 0"
+
+instance ..
+
+end
+
+instantiation star :: (one) one
+begin
+
+definition
+ star_one_def: "1 \<equiv> star_of 1"
-instance star :: (one) one
- star_one_def: "1 \<equiv> star_of 1" ..
+instance ..
+
+end
+
+instantiation star :: (plus) plus
+begin
-instance star :: (plus) plus
- star_add_def: "(op +) \<equiv> *f2* (op +)" ..
+definition
+ star_add_def: "(op +) \<equiv> *f2* (op +)"
+
+instance ..
+
+end
+
+instantiation star :: (times) times
+begin
-instance star :: (times) times
- star_mult_def: "(op *) \<equiv> *f2* (op *)" ..
+definition
+ star_mult_def: "(op *) \<equiv> *f2* (op *)"
+
+instance ..
-instance star :: (minus) minus
+end
+
+instantiation star :: (minus) minus
+begin
+
+definition
star_minus_def: "uminus \<equiv> *f* uminus"
- star_diff_def: "(op -) \<equiv> *f2* (op -)" ..
+
+definition
+ star_diff_def: "(op -) \<equiv> *f2* (op -)"
+
+instance ..
+
+end
-instance star :: (abs) abs
- star_abs_def: "abs \<equiv> *f* abs" ..
+instantiation star :: (abs) abs
+begin
+
+definition
+ star_abs_def: "abs \<equiv> *f* abs"
+
+instance ..
+
+end
+
+instantiation star :: (sgn) sgn
+begin
-instance star :: (sgn) sgn
- star_sgn_def: "sgn \<equiv> *f* sgn" ..
+definition
+ star_sgn_def: "sgn \<equiv> *f* sgn"
+
+instance ..
-instance star :: (inverse) inverse
+end
+
+instantiation star :: (inverse) inverse
+begin
+
+definition
star_divide_def: "(op /) \<equiv> *f2* (op /)"
- star_inverse_def: "inverse \<equiv> *f* inverse" ..
+
+definition
+ star_inverse_def: "inverse \<equiv> *f* inverse"
+
+instance ..
+
+end
-instance star :: (number) number
- star_number_def: "number_of b \<equiv> star_of (number_of b)" ..
+instantiation star :: (number) number
+begin
+
+definition
+ star_number_def: "number_of b \<equiv> star_of (number_of b)"
+
+instance ..
+
+end
+
+instantiation star :: (Divides.div) Divides.div
+begin
-instance star :: (Divides.div) Divides.div
+definition
star_div_def: "(op div) \<equiv> *f2* (op div)"
- star_mod_def: "(op mod) \<equiv> *f2* (op mod)" ..
+
+definition
+ star_mod_def: "(op mod) \<equiv> *f2* (op mod)"
+
+instance ..
+
+end
+
+instantiation star :: (power) power
+begin
+
+definition
+ star_power_def: "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
-instance star :: (power) power
- star_power_def: "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x" ..
+instance ..
+
+end
+
+instantiation star :: (ord) ord
+begin
-instance star :: (ord) ord
+definition
star_le_def: "(op \<le>) \<equiv> *p2* (op \<le>)"
- star_less_def: "(op <) \<equiv> *p2* (op <)" ..
+
+definition
+ star_less_def: "(op <) \<equiv> *p2* (op <)"
+
+instance ..
+
+end
lemmas star_class_defs [transfer_unfold] =
star_zero_def star_one_def star_number_def
@@ -220,14 +312,28 @@
apply (transfer, erule (1) order_antisym)
done
-instance star :: (lower_semilattice) lower_semilattice
+instantiation star :: (lower_semilattice) lower_semilattice
+begin
+
+definition
star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf"
+
+instance
by default (transfer star_inf_def, auto)+
-instance star :: (upper_semilattice) upper_semilattice
+end
+
+instantiation star :: (upper_semilattice) upper_semilattice
+begin
+
+definition
star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup"
+
+instance
by default (transfer star_sup_def, auto)+
+end
+
instance star :: (lattice) lattice ..
instance star :: (distrib_lattice) distrib_lattice
--- a/src/HOL/IntDef.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/IntDef.thy Fri Dec 07 15:07:59 2007 +0100
@@ -22,34 +22,48 @@
int = "UNIV//intrel"
by (auto simp add: quotient_def)
-instance int :: zero
- Zero_int_def: "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})" ..
+instantiation int :: "{zero, one, plus, minus, times, ord, abs, sgn}"
+begin
+
+definition
+ Zero_int_def [code func del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
+
+definition
+ One_int_def [code func del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
-instance int :: one
- One_int_def: "1 \<equiv> Abs_Integ (intrel `` {(1, 0)})" ..
+definition
+ add_int_def [code func del]: "z + w = Abs_Integ
+ (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
+ intrel `` {(x + u, y + v)})"
-instance int :: plus
- add_int_def: "z + w \<equiv> Abs_Integ
- (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
- intrel `` {(x + u, y + v)})" ..
+definition
+ minus_int_def [code func del]:
+ "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
+
+definition
+ diff_int_def [code func del]: "z - w = z + (-w \<Colon> int)"
-instance int :: minus
- minus_int_def:
- "- z \<equiv> Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
- diff_int_def: "z - w \<equiv> z + (-w \<Colon> int)" ..
-
-instance int :: times
- mult_int_def: "z * w \<equiv> Abs_Integ
+definition
+ mult_int_def [code func del]: "z * w = Abs_Integ
(\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
- intrel `` {(x*u + y*v, x*v + y*u)})" ..
+ intrel `` {(x*u + y*v, x*v + y*u)})"
+
+definition
+ le_int_def [code func del]:
+ "z \<le> w \<longleftrightarrow> (\<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w)"
+
+definition
+ less_int_def [code func del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
-instance int :: ord
- le_int_def:
- "z \<le> w \<equiv> \<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w"
- less_int_def: "(z\<Colon>int) < w \<equiv> z \<le> w \<and> z \<noteq> w" ..
+definition
+ zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
-lemmas [code func del] = Zero_int_def One_int_def add_int_def
- minus_int_def mult_int_def le_int_def less_int_def
+definition
+ zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+
+instance ..
+
+end
subsection{*Construction of the Integers*}
@@ -212,17 +226,21 @@
apply (auto simp add: zmult_zless_mono2_lemma)
done
-instance int :: abs
- zabs_def: "\<bar>i\<Colon>int\<bar> \<equiv> if i < 0 then - i else i" ..
-instance int :: sgn
- zsgn_def: "sgn(i\<Colon>int) \<equiv> (if i=0 then 0 else if 0<i then 1 else - 1)" ..
+instantiation int :: distrib_lattice
+begin
-instance int :: distrib_lattice
- "inf \<Colon> int \<Rightarrow> int \<Rightarrow> int \<equiv> min"
- "sup \<Colon> int \<Rightarrow> int \<Rightarrow> int \<equiv> max"
+definition
+ "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
+
+definition
+ "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
+
+instance
by intro_classes
(auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
+end
+
text{*The integers form an ordered integral domain*}
instance int :: ordered_idom
proof
@@ -744,7 +762,7 @@
lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
-lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
+lemmas zless_le = less_int_def
lemmas int_eq_of_nat = TrueI
abbreviation
--- a/src/HOL/IntDiv.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/IntDiv.thy Fri Dec 07 15:07:59 2007 +0100
@@ -62,9 +62,18 @@
if 0<b then negDivAlg a b
else negateSnd (posDivAlg (-a) (-b))))"
-instance int :: Divides.div
- div_def: "a div b == fst (divAlg (a, b))"
- mod_def: "a mod b == snd (divAlg (a, b))" ..
+instantiation int :: Divides.div
+begin
+
+definition
+ div_def: "a div b = fst (divAlg (a, b))"
+
+definition
+ mod_def: "a mod b = snd (divAlg (a, b))"
+
+instance ..
+
+end
lemma divAlg_mod_div:
"divAlg (p, q) = (p div q, p mod q)"
--- a/src/HOL/Library/Multiset.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Dec 07 15:07:59 2007 +0100
@@ -49,11 +49,24 @@
set_of :: "'a multiset => 'a set" where
"set_of M = {x. x :# M}"
-instance multiset :: (type) "{plus, minus, zero, size}"
+instantiation multiset :: (type) "{plus, minus, zero, size}"
+begin
+
+definition
union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
+
+definition
diff_def: "M - N == Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
+
+definition
Zero_multiset_def [simp]: "0 == {#}"
- size_def: "size M == setsum (count M) (set_of M)" ..
+
+definition
+ size_def: "size M == setsum (count M) (set_of M)"
+
+instance ..
+
+end
definition
multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
--- a/src/HOL/Library/Parity.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Library/Parity.thy Fri Dec 07 15:07:59 2007 +0100
@@ -16,11 +16,18 @@
odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where
"odd x \<equiv> \<not> even x"
-instance int :: even_odd
- even_def[presburger]: "even x \<equiv> (x\<Colon>int) mod 2 = 0" ..
+instantiation int and nat :: even_odd
+begin
+
+definition
+ even_def [presburger]: "even x \<longleftrightarrow> (x\<Colon>int) mod 2 = 0"
-instance nat :: even_odd
- even_nat_def[presburger]: "even x \<equiv> even (int x)" ..
+definition
+ even_nat_def [presburger]: "even x \<longleftrightarrow> even (int x)"
+
+instance ..
+
+end
subsection {* Even and odd are mutually exclusive *}
--- a/src/HOL/Library/Product_ord.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Library/Product_ord.thy Fri Dec 07 15:07:59 2007 +0100
@@ -9,9 +9,18 @@
imports Main
begin
-instance "*" :: (ord, ord) ord
+instantiation "*" :: (ord, ord) ord
+begin
+
+definition
prod_le_def [code func del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
- prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y" ..
+
+definition
+ prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
+
+instance ..
+
+end
lemma [code func]:
"(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
@@ -29,10 +38,19 @@
instance * :: (linorder, linorder) linorder
by default (auto simp: prod_le_def)
-instance * :: (linorder, linorder) distrib_lattice
+instantiation * :: (linorder, linorder) distrib_lattice
+begin
+
+definition
inf_prod_def: "(inf \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = min"
+
+definition
sup_prod_def: "(sup \<Colon> 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
+
+instance
by intro_classes
(auto simp add: inf_prod_def sup_prod_def min_max.sup_inf_distrib1)
end
+
+end
--- a/src/HOL/List.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/List.thy Fri Dec 07 15:07:59 2007 +0100
@@ -109,7 +109,6 @@
where
append_Nil:"[] @ ys = ys"
| append_Cons: "(x#xs) @ ys = x # xs @ ys"
-declare append.simps [code]
primrec
"rev([]) = []"
@@ -2691,9 +2690,16 @@
text{* The integers are an instance of the above class: *}
-instance int:: finite_intvl_succ
- successor_int_def: "successor == (%i\<Colon>int. i+1)"
-by intro_classes (simp_all add: successor_int_def)
+instantiation int:: finite_intvl_succ
+begin
+
+definition
+ successor_int_def: "successor = (%i\<Colon>int. i+1)"
+
+instance
+ by intro_classes (simp_all add: successor_int_def)
+
+end
text{* Now @{term"[i..j::int]"} is defined for integers. *}
@@ -3178,7 +3184,6 @@
where
"x mem [] \<longleftrightarrow> False"
| "x mem (y#ys) \<longleftrightarrow> (if y = x then True else x mem ys)"
-declare member.simps [code]
primrec
"null [] = True"
--- a/src/HOL/Nat.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Nat.thy Fri Dec 07 15:07:59 2007 +0100
@@ -139,20 +139,30 @@
subsection {* Arithmetic operators *}
-instance nat :: "{one, plus, minus, times}"
- One_nat_def [simp]: "1 == Suc 0" ..
+instantiation nat :: "{one, plus, minus, times}"
+begin
-primrec
- add_0: "0 + n = n"
- add_Suc: "Suc m + n = Suc (m + n)"
+definition
+ One_nat_def [simp]: "1 = Suc 0"
+
+primrec plus_nat
+where
+ add_0: "0 + n = (n\<Colon>nat)"
+ | add_Suc: "Suc m + n = Suc (m + n)"
-primrec
- diff_0: "m - 0 = m"
- diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
+primrec minus_nat
+where
+ diff_0: "m - 0 = (m\<Colon>nat)"
+ | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
-primrec
- mult_0: "0 * n = 0"
- mult_Suc: "Suc m * n = n + (m * n)"
+primrec times_nat
+where
+ mult_0: "0 * n = (0\<Colon>nat)"
+ | mult_Suc: "Suc m * n = n + (m * n)"
+
+instance ..
+
+end
subsection {* Orders on @{typ nat} *}
@@ -341,9 +351,6 @@
apply (blast dest: Suc_lessD)
done
-lemma [code]: "((n::nat) < 0) = False" by simp
-lemma [code]: "(0 < Suc n) = True" by simp
-
text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *}
lemma not_less_eq: "(~ m < n) = (n < Suc m)"
by (induct m n rule: diff_induct) simp_all
@@ -621,6 +628,13 @@
declare diff_Suc [simp del, code del]
+lemma [code]:
+ "(0\<Colon>nat) \<le> m \<longleftrightarrow> True"
+ "Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m"
+ "(n\<Colon>nat) < 0 \<longleftrightarrow> False"
+ "(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m"
+ using Suc_le_eq less_Suc_eq_le by simp_all
+
subsection {* Addition *}
@@ -1141,16 +1155,6 @@
declare "*.size" [noatp]
-subsection {* Code generator setup *}
-
-lemma [code func]:
- "(0\<Colon>nat) \<le> m \<longleftrightarrow> True"
- "Suc (n\<Colon>nat) \<le> m \<longleftrightarrow> n < m"
- "(n\<Colon>nat) < 0 \<longleftrightarrow> False"
- "(n\<Colon>nat) < Suc m \<longleftrightarrow> n \<le> m"
- using Suc_le_eq less_Suc_eq_le by simp_all
-
-
subsection {* Embedding of the Naturals into any
@{text semiring_1}: @{term of_nat} *}
@@ -1162,7 +1166,6 @@
where
of_nat_0: "of_nat 0 = 0"
| of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
-declare of_nat.simps [code]
lemma of_nat_1 [simp]: "of_nat 1 = 1"
by simp
--- a/src/HOL/NatBin.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/NatBin.thy Fri Dec 07 15:07:59 2007 +0100
@@ -14,8 +14,15 @@
Arithmetic for naturals is reduced to that for the non-negative integers.
*}
-instance nat :: number
- nat_number_of_def [code inline]: "number_of v == nat (number_of (v\<Colon>int))" ..
+instantiation nat :: number
+begin
+
+definition
+ nat_number_of_def [code inline]: "number_of v = nat (number_of (v\<Colon>int))"
+
+instance ..
+
+end
abbreviation (xsymbols)
square :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) where
--- a/src/HOL/Numeral.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Numeral.thy Fri Dec 07 15:07:59 2007 +0100
@@ -210,11 +210,16 @@
text {* self-embedding of the integers *}
-instance int :: number_ring
- int_number_of_def: "number_of w \<equiv> of_int w \<Colon> int"
+instantiation int :: number_ring
+begin
+
+definition
+ int_number_of_def [code func del]: "number_of w = (of_int w \<Colon> int)"
+
+instance
by intro_classes (simp only: int_number_of_def)
-lemmas [code func del] = int_number_of_def
+end
lemma number_of_is_id:
"number_of (k::int) = k"
--- a/src/HOL/Real/PReal.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Real/PReal.thy Fri Dec 07 15:07:59 2007 +0100
@@ -211,12 +211,20 @@
instance preal :: linorder
by intro_classes (rule preal_le_linear)
-instance preal :: distrib_lattice
- "inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal \<equiv> min"
- "sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal \<equiv> max"
+instantiation preal :: distrib_lattice
+begin
+
+definition
+ "(inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = min"
+
+definition
+ "(sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = max"
+
+instance
by intro_classes
(auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
+end
subsection{*Properties of Addition*}
--- a/src/HOL/Real/Rational.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Real/Rational.thy Fri Dec 07 15:07:59 2007 +0100
@@ -163,60 +163,72 @@
subsubsection {* Standard operations on rational numbers *}
-instance rat :: zero
- Zero_rat_def: "0 == Fract 0 1" ..
-lemmas [code func del] = Zero_rat_def
+instantiation rat :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}"
+begin
+
+definition
+ Zero_rat_def [code func del]: "0 = Fract 0 1"
-instance rat :: one
- One_rat_def: "1 == Fract 1 1" ..
-lemmas [code func del] = One_rat_def
+definition
+ One_rat_def [code func del]: "1 = Fract 1 1"
-instance rat :: plus
- add_rat_def:
- "q + r ==
+definition
+ add_rat_def [code func del]:
+ "q + r =
Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
- ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)})" ..
-lemmas [code func del] = add_rat_def
+ ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)})"
-instance rat :: minus
- minus_rat_def:
- "- q == Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel``{(- fst x, snd x)})"
- diff_rat_def: "q - r == q + - (r::rat)" ..
-lemmas [code func del] = minus_rat_def diff_rat_def
+definition
+ minus_rat_def [code func del]:
+ "- q = Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel``{(- fst x, snd x)})"
+
+definition
+ diff_rat_def [code func del]: "q - r = q + - (r::rat)"
-instance rat :: times
- mult_rat_def:
- "q * r ==
+definition
+ mult_rat_def [code func del]:
+ "q * r =
Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
- ratrel``{(fst x * fst y, snd x * snd y)})" ..
-lemmas [code func del] = mult_rat_def
+ ratrel``{(fst x * fst y, snd x * snd y)})"
-instance rat :: inverse
- inverse_rat_def:
- "inverse q ==
+definition
+ inverse_rat_def [code func del]:
+ "inverse q =
Abs_Rat (\<Union>x \<in> Rep_Rat q.
ratrel``{if fst x=0 then (0,1) else (snd x, fst x)})"
- divide_rat_def: "q / r == q * inverse (r::rat)" ..
-lemmas [code func del] = inverse_rat_def divide_rat_def
+
+definition
+ divide_rat_def [code func del]: "q / r = q * inverse (r::rat)"
-instance rat :: ord
- le_rat_def:
- "q \<le> r == contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
+definition
+ le_rat_def [code func del]:
+ "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
{(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"
- less_rat_def: "(z < (w::rat)) == (z \<le> w & z \<noteq> w)" ..
-lemmas [code func del] = le_rat_def less_rat_def
+
+definition
+ less_rat_def [code func del]: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
+
+definition
+ abs_rat_def: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
-instance rat :: abs
- abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)" ..
+definition
+ sgn_rat_def: "sgn (q::rat) = (if q=0 then 0 else if 0<q then 1 else - 1)"
-instance rat :: sgn
- sgn_rat_def: "sgn(q::rat) == (if q=0 then 0 else if 0<q then 1 else - 1)" ..
+instance ..
+
+end
-instance rat :: power ..
+instantiation rat :: power
+begin
-primrec (rat)
- rat_power_0: "q ^ 0 = 1"
- rat_power_Suc: "q ^ (Suc n) = (q::rat) * (q ^ n)"
+primrec power_rat
+where
+ rat_power_0: "q ^ 0 = (1\<Colon>rat)"
+ | rat_power_Suc: "q ^ (Suc n) = (q\<Colon>rat) * (q ^ n)"
+
+instance ..
+
+end
theorem eq_rat: "b \<noteq> 0 ==> d \<noteq> 0 ==>
(Fract a b = Fract c d) = (a * d = c * b)"
@@ -361,11 +373,20 @@
}
qed
-instance rat :: distrib_lattice
- "inf \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat \<equiv> min"
- "sup \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat \<equiv> max"
+instantiation rat :: distrib_lattice
+begin
+
+definition
+ "(inf \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = min"
+
+definition
+ "(sup \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat) = max"
+
+instance
by default (auto simp add: min_max.sup_inf_distrib1 inf_rat_def sup_rat_def)
+end
+
instance rat :: ordered_field
proof
fix q r s :: rat
@@ -474,11 +495,16 @@
subsection {* Numerals and Arithmetic *}
-instance rat :: number
- rat_number_of_def: "(number_of w :: rat) \<equiv> of_int w" ..
+instantiation rat :: number_ring
+begin
-instance rat :: number_ring
- by default (simp add: rat_number_of_def)
+definition
+ rat_number_of_def: "number_of w = (of_int w \<Colon> rat)"
+
+instance
+ by default (simp add: rat_number_of_def)
+
+end
use "rat_arith.ML"
declaration {* K rat_arith_setup *}
@@ -488,7 +514,7 @@
class field_char_0 = field + ring_char_0
-instance ordered_field < field_char_0 ..
+instance ordered_field < field_char_0 ..
definition
of_rat :: "rat \<Rightarrow> 'a::field_char_0"
--- a/src/HOL/Real/RealDef.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Real/RealDef.thy Fri Dec 07 15:07:59 2007 +0100
@@ -25,48 +25,54 @@
real_of_preal :: "preal => real" where
"real_of_preal m = Abs_Real(realrel``{(m + 1, 1)})"
-instance real :: zero
- real_zero_def: "0 == Abs_Real(realrel``{(1, 1)})" ..
-lemmas [code func del] = real_zero_def
+instantiation real :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}"
+begin
-instance real :: one
- real_one_def: "1 == Abs_Real(realrel``{(1 + 1, 1)})" ..
-lemmas [code func del] = real_one_def
+definition
+ real_zero_def [code func del]: "0 = Abs_Real(realrel``{(1, 1)})"
+
+definition
+ real_one_def [code func del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
-instance real :: plus
- real_add_def: "z + w ==
+definition
+ real_add_def [code func del]: "z + w =
contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
- { Abs_Real(realrel``{(x+u, y+v)}) })" ..
-lemmas [code func del] = real_add_def
+ { Abs_Real(realrel``{(x+u, y+v)}) })"
-instance real :: minus
- real_minus_def: "- r == contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
- real_diff_def: "r - (s::real) == r + - s" ..
-lemmas [code func del] = real_minus_def real_diff_def
+definition
+ real_minus_def [code func del]: "- r = contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
+
+definition
+ real_diff_def [code func del]: "r - (s::real) = r + - s"
-instance real :: times
- real_mult_def:
- "z * w ==
+definition
+ real_mult_def [code func del]:
+ "z * w =
contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
- { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })" ..
-lemmas [code func del] = real_mult_def
+ { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
-instance real :: inverse
- real_inverse_def: "inverse (R::real) == (THE S. (R = 0 & S = 0) | S * R = 1)"
- real_divide_def: "R / (S::real) == R * inverse S" ..
-lemmas [code func del] = real_inverse_def real_divide_def
+definition
+ real_inverse_def [code func del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
+
+definition
+ real_divide_def [code func del]: "R / (S::real) = R * inverse S"
-instance real :: ord
- real_le_def: "z \<le> (w::real) ==
- \<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w"
- real_less_def: "(x < (y::real)) == (x \<le> y & x \<noteq> y)" ..
-lemmas [code func del] = real_le_def real_less_def
+definition
+ real_le_def [code func del]: "z \<le> (w::real) \<longleftrightarrow>
+ (\<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w)"
+
+definition
+ real_less_def [code func del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
-instance real :: abs
- real_abs_def: "abs (r::real) == (if r < 0 then - r else r)" ..
+definition
+ real_abs_def: "abs (r::real) = (if r < 0 then - r else r)"
-instance real :: sgn
- real_sgn_def: "sgn (x::real) == (if x=0 then 0 else if 0<x then 1 else - 1)" ..
+definition
+ real_sgn_def: "sgn (x::real) = (if x=0 then 0 else if 0<x then 1 else - 1)"
+
+instance ..
+
+end
subsection {* Equivalence relation over positive reals *}
@@ -400,11 +406,20 @@
apply (simp add: right_distrib)
done
-instance real :: distrib_lattice
- "inf \<Colon> real \<Rightarrow> real \<Rightarrow> real \<equiv> min"
- "sup \<Colon> real \<Rightarrow> real \<Rightarrow> real \<equiv> max"
+instantiation real :: distrib_lattice
+begin
+
+definition
+ "(inf \<Colon> real \<Rightarrow> real \<Rightarrow> real) = min"
+
+definition
+ "(sup \<Colon> real \<Rightarrow> real \<Rightarrow> real) = max"
+
+instance
by default (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
+end
+
subsection{*The Reals Form an Ordered Field*}
@@ -833,10 +848,17 @@
subsection{*Numerals and Arithmetic*}
-instance real :: number_ring
- real_number_of_def: "number_of w \<equiv> real_of_int w"
+instantiation real :: number_ring
+begin
+
+definition
+ real_number_of_def: "number_of w = real_of_int w"
+
+instance
by intro_classes (simp add: real_number_of_def)
+end
+
lemma [code, code unfold]:
"number_of k = real_of_int (number_of k)"
unfolding number_of_is_id real_number_of_def ..
--- a/src/HOL/Real/RealVector.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Real/RealVector.thy Fri Dec 07 15:07:59 2007 +0100
@@ -54,8 +54,15 @@
end
-instance real :: scaleR
- real_scaleR_def [simp]: "scaleR a x \<equiv> a * x" ..
+instantiation real :: scaleR
+begin
+
+definition
+ real_scaleR_def [simp]: "scaleR a x = a * x"
+
+instance ..
+
+end
class real_vector = scaleR + ab_group_add +
assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
@@ -371,8 +378,15 @@
class norm = type +
fixes norm :: "'a \<Rightarrow> real"
-instance real :: norm
- real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
+instantiation real :: norm
+begin
+
+definition
+ real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>"
+
+instance ..
+
+end
class sgn_div_norm = scaleR + norm + sgn +
assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"