# HG changeset patch # User wenzelm # Date 1083441717 -7200 # Node ID e1eedc8cad37fa3974482bcbe865dd3388470d7e # Parent f61ea8bfa81ed3353a799624a705fce75111f50a tuned instance statements; diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Complex/Complex.thy --- 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 ("\") diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Complex/NSComplex.thy --- 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: diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Hyperreal/HyperDef.thy --- 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 \ y" by (auto simp add: order_less_irrefl) diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Hyperreal/HyperNat.thy --- 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) \ w | w \ 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 \ y ==> z + x \ z + (y::hypnat)" apply (cases x, cases y, cases z) diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Integ/IntDef.thy --- 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) \ w | w \ 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] diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Library/Multiset.thy --- 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 (\a. Rep_multiset M a + Rep_multiset N a)" diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Library/Nat_Infinity.thy --- 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" diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Matrix/Matrix.thy --- 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 \ 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) diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Matrix/MatrixGeneral.thy --- 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)" diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Nat.thy --- 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 \ 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" diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Real/PReal.thy --- 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 \ preal; r \ 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) diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Real/Rational.thy --- 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 \ r == fraction_of q \ fraction_of r" @@ -377,7 +362,7 @@ abs_rat_def: "\q\ == 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 \ 0 ==> \Fract a b\ = Fract \a\ \b\" 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 \ 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 \ (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 \ 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 \ 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] diff -r f61ea8bfa81e -r e1eedc8cad37 src/HOL/Real/RealDef.thy --- 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" ("\") + defs (overloaded) @@ -83,9 +80,6 @@ real_abs_def: "abs (r::real) == (if 0 \ r then r else -r)" -syntax (xsymbols) - Reals :: "'a set" ("\") - subsection{*Proving that realrel is an equivalence relation*}