tuned instance statements;
authorwenzelm
Sat May 01 22:01:57 2004 +0200 (2004-05-01 ago)
changeset 14691e1eedc8cad37
parent 14690 f61ea8bfa81e
child 14692 b8d6c395c9e2
tuned instance statements;
src/HOL/Complex/Complex.thy
src/HOL/Complex/NSComplex.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Integ/IntDef.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Matrix/MatrixGeneral.thy
src/HOL/Nat.thy
src/HOL/Real/PReal.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
     1.1 --- a/src/HOL/Complex/Complex.thy	Sat May 01 21:59:12 2004 +0200
     1.2 +++ b/src/HOL/Complex/Complex.thy	Sat May 01 22:01:57 2004 +0200
     1.3 @@ -11,13 +11,7 @@
     1.4  
     1.5  datatype complex = Complex real real
     1.6  
     1.7 -instance complex :: zero ..
     1.8 -instance complex :: one ..
     1.9 -instance complex :: plus ..
    1.10 -instance complex :: times ..
    1.11 -instance complex :: minus ..
    1.12 -instance complex :: inverse ..
    1.13 -instance complex :: power ..
    1.14 +instance complex :: "{zero, one, plus, times, minus, inverse, power}" ..
    1.15  
    1.16  consts
    1.17    "ii"    :: complex    ("\<i>")
     2.1 --- a/src/HOL/Complex/NSComplex.thy	Sat May 01 21:59:12 2004 +0200
     2.2 +++ b/src/HOL/Complex/NSComplex.thy	Sat May 01 22:01:57 2004 +0200
     2.3 @@ -17,13 +17,7 @@
     2.4  typedef hcomplex = "{x::nat=>complex. True}//hcomplexrel"
     2.5    by (auto simp add: quotient_def)
     2.6  
     2.7 -instance hcomplex :: zero ..
     2.8 -instance hcomplex :: one ..
     2.9 -instance hcomplex :: plus ..
    2.10 -instance hcomplex :: times ..
    2.11 -instance hcomplex :: minus ..
    2.12 -instance hcomplex :: inverse ..
    2.13 -instance hcomplex :: power ..
    2.14 +instance hcomplex :: "{zero, one, plus, times, minus, inverse, power}" ..
    2.15  
    2.16  defs (overloaded)
    2.17    hcomplex_zero_def:
     3.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Sat May 01 21:59:12 2004 +0200
     3.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Sat May 01 22:01:57 2004 +0200
     3.3 @@ -23,14 +23,7 @@
     3.4  typedef hypreal = "UNIV//hyprel" 
     3.5      by (auto simp add: quotient_def) 
     3.6  
     3.7 -instance hypreal :: ord ..
     3.8 -instance hypreal :: zero ..
     3.9 -instance hypreal :: one ..
    3.10 -instance hypreal :: plus ..
    3.11 -instance hypreal :: times ..
    3.12 -instance hypreal :: minus ..
    3.13 -instance hypreal :: inverse ..
    3.14 -
    3.15 +instance hypreal :: "{ord, zero, one, plus, times, minus, inverse}" ..
    3.16  
    3.17  defs (overloaded)
    3.18  
    3.19 @@ -58,10 +51,10 @@
    3.20    hypreal_of_real  :: "real => hypreal"
    3.21    "hypreal_of_real r         == Abs_hypreal(hyprel``{%n::nat. r})"
    3.22  
    3.23 -  omega   :: hypreal   (*an infinite number = [<1,2,3,...>] *)
    3.24 +  omega   :: hypreal   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
    3.25    "omega == Abs_hypreal(hyprel``{%n::nat. real (Suc n)})"
    3.26  
    3.27 -  epsilon :: hypreal   (*an infinitesimal number = [<1,1/2,1/3,...>] *)
    3.28 +  epsilon :: hypreal   -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
    3.29    "epsilon == Abs_hypreal(hyprel``{%n::nat. inverse (real (Suc n))})"
    3.30  
    3.31  syntax (xsymbols)
    3.32 @@ -341,9 +334,9 @@
    3.33  by (cases z, simp add: hypreal_zero_def hypreal_add)
    3.34  
    3.35  instance hypreal :: plus_ac0
    3.36 -  by (intro_classes,
    3.37 -      (assumption | 
    3.38 -       rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+)
    3.39 +  by intro_classes
    3.40 +    (assumption | 
    3.41 +      rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+
    3.42  
    3.43  lemma hypreal_add_zero_right [simp]: "z + (0::hypreal) = z"
    3.44  by (simp add: hypreal_add_zero_left hypreal_add_commute)
    3.45 @@ -502,9 +495,9 @@
    3.46  by (simp add: hypreal_less_def)
    3.47  
    3.48  instance hypreal :: order
    3.49 -proof qed
    3.50 - (assumption |
    3.51 -  rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym hypreal_less_le)+
    3.52 +  by intro_classes
    3.53 +    (assumption |
    3.54 +      rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym hypreal_less_le)+
    3.55  
    3.56  
    3.57  (* Axiom 'linorder_linear' of class 'linorder': *)
    3.58 @@ -514,7 +507,7 @@
    3.59  done
    3.60  
    3.61  instance hypreal :: linorder 
    3.62 -  by (intro_classes, rule hypreal_le_linear)
    3.63 +  by intro_classes (rule hypreal_le_linear)
    3.64  
    3.65  lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
    3.66  by (auto simp add: order_less_irrefl)
     4.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Sat May 01 21:59:12 2004 +0200
     4.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Sat May 01 22:01:57 2004 +0200
     4.3 @@ -17,12 +17,7 @@
     4.4  typedef hypnat = "UNIV//hypnatrel"
     4.5      by (auto simp add: quotient_def)
     4.6  
     4.7 -instance hypnat :: ord ..
     4.8 -instance hypnat :: zero ..
     4.9 -instance hypnat :: one ..
    4.10 -instance hypnat :: plus ..
    4.11 -instance hypnat :: times ..
    4.12 -instance hypnat :: minus ..
    4.13 +instance hypnat :: "{ord, zero, one, plus, times, minus}" ..
    4.14  
    4.15  consts whn :: hypnat
    4.16  
    4.17 @@ -164,9 +159,9 @@
    4.18  done
    4.19  
    4.20  instance hypnat :: plus_ac0
    4.21 -  by (intro_classes,
    4.22 -      (assumption |
    4.23 -       rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+)
    4.24 +  by intro_classes
    4.25 +    (assumption |
    4.26 +      rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+
    4.27  
    4.28  
    4.29  subsection{*Subtraction inverse on @{typ hypreal}*}
    4.30 @@ -332,9 +327,9 @@
    4.31  by (simp add: hypnat_less_def)
    4.32  
    4.33  instance hypnat :: order
    4.34 -proof qed
    4.35 - (assumption |
    4.36 -  rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+
    4.37 +  by intro_classes
    4.38 +    (assumption |
    4.39 +      rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+
    4.40  
    4.41  (* Axiom 'linorder_linear' of class 'linorder': *)
    4.42  lemma hypnat_le_linear: "(z::hypnat) \<le> w | w \<le> z"
    4.43 @@ -343,7 +338,7 @@
    4.44  done
    4.45  
    4.46  instance hypnat :: linorder
    4.47 -  by (intro_classes, rule hypnat_le_linear)
    4.48 +  by intro_classes (rule hypnat_le_linear)
    4.49  
    4.50  lemma hypnat_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypnat)"
    4.51  apply (cases x, cases y, cases z)
     5.1 --- a/src/HOL/Integ/IntDef.thy	Sat May 01 21:59:12 2004 +0200
     5.2 +++ b/src/HOL/Integ/IntDef.thy	Sat May 01 22:01:57 2004 +0200
     5.3 @@ -18,15 +18,9 @@
     5.4    int = "UNIV//intrel"
     5.5      by (auto simp add: quotient_def)
     5.6  
     5.7 -instance int :: ord ..
     5.8 -instance int :: zero ..
     5.9 -instance int :: one ..
    5.10 -instance int :: plus ..
    5.11 -instance int :: times ..
    5.12 -instance int :: minus ..
    5.13 +instance int :: "{ord, zero, one, plus, times, minus}" ..
    5.14  
    5.15  constdefs
    5.16 -
    5.17    int :: "nat => int"
    5.18    "int m == Abs_Integ(intrel `` {(m,0)})"
    5.19  
    5.20 @@ -279,16 +273,16 @@
    5.21  by (simp add: less_int_def)
    5.22  
    5.23  instance int :: order
    5.24 -proof qed
    5.25 - (assumption |
    5.26 -  rule zle_refl zle_trans zle_anti_sym zless_le)+
    5.27 +  by intro_classes
    5.28 +    (assumption |
    5.29 +      rule zle_refl zle_trans zle_anti_sym zless_le)+
    5.30  
    5.31  (* Axiom 'linorder_linear' of class 'linorder': *)
    5.32  lemma zle_linear: "(z::int) \<le> w | w \<le> z"
    5.33 -by (cases z, cases w, simp add: le linorder_linear)
    5.34 +by (cases z, cases w) (simp add: le linorder_linear)
    5.35  
    5.36  instance int :: linorder
    5.37 -proof qed (rule zle_linear)
    5.38 +  by intro_classes (rule zle_linear)
    5.39  
    5.40  
    5.41  lemmas zless_linear = linorder_less_linear [where 'a = int]
     6.1 --- a/src/HOL/Library/Multiset.thy	Sat May 01 21:59:12 2004 +0200
     6.2 +++ b/src/HOL/Library/Multiset.thy	Sat May 01 22:01:57 2004 +0200
     6.3 @@ -46,9 +46,7 @@
     6.4    set_of :: "'a multiset => 'a set"
     6.5    "set_of M == {x. x :# M}"
     6.6  
     6.7 -instance multiset :: (type) plus ..
     6.8 -instance multiset :: (type) minus ..
     6.9 -instance multiset :: (type) zero ..
    6.10 +instance multiset :: (type) "{plus, minus, zero}" ..
    6.11  
    6.12  defs (overloaded)
    6.13    union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
     7.1 --- a/src/HOL/Library/Nat_Infinity.thy	Sat May 01 21:59:12 2004 +0200
     7.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Sat May 01 22:01:57 2004 +0200
     7.3 @@ -21,8 +21,7 @@
     7.4  
     7.5  datatype inat = Fin nat | Infty
     7.6  
     7.7 -instance inat :: ord ..
     7.8 -instance inat :: zero ..
     7.9 +instance inat :: "{ord, zero}" ..
    7.10  
    7.11  consts
    7.12    iSuc :: "inat => inat"
     8.1 --- a/src/HOL/Matrix/Matrix.thy	Sat May 01 21:59:12 2004 +0200
     8.2 +++ b/src/HOL/Matrix/Matrix.thy	Sat May 01 22:01:57 2004 +0200
     8.3 @@ -20,11 +20,8 @@
     8.4  axclass matrix_element < almost_matrix_element
     8.5  matrix_add_0[simp]: "0+0 = 0"
     8.6  
     8.7 -instance matrix :: (plus) plus
     8.8 -by (intro_classes)
     8.9 -
    8.10 -instance matrix :: (times) times
    8.11 -by (intro_classes)
    8.12 +instance matrix :: (plus) plus ..
    8.13 +instance matrix :: (times) times ..
    8.14  
    8.15  defs (overloaded)
    8.16  plus_matrix_def: "A + B == combine_matrix (op +) A B"
    8.17 @@ -127,7 +124,7 @@
    8.18  g_add_leftimp_eq: "a+b = a+c \<Longrightarrow> b = c"
    8.19  
    8.20  instance g_almost_semiring < matrix_element
    8.21 -by (intro_classes, simp)
    8.22 +  by intro_classes simp
    8.23  
    8.24  instance semiring < g_semiring
    8.25  apply (intro_classes)
    8.26 @@ -197,8 +194,7 @@
    8.27  apply (intro_classes)
    8.28  by (simp_all add: add_right_mono mult_right_mono mult_left_mono)
    8.29  
    8.30 -instance matrix :: (pordered_g_semiring) pordered_g_semiring
    8.31 -by (intro_classes)
    8.32 +instance matrix :: (pordered_g_semiring) pordered_g_semiring ..
    8.33  
    8.34  lemma nrows_mult: "nrows ((A::('a::matrix_element) matrix) * B) <= nrows A"
    8.35  by (simp add: times_matrix_def mult_nrows)
     9.1 --- a/src/HOL/Matrix/MatrixGeneral.thy	Sat May 01 21:59:12 2004 +0200
     9.2 +++ b/src/HOL/Matrix/MatrixGeneral.thy	Sat May 01 22:01:57 2004 +0200
     9.3 @@ -746,7 +746,7 @@
     9.4  qed
     9.5  
     9.6  
     9.7 -instance matrix :: (zero)zero by intro_classes
     9.8 +instance matrix :: (zero) zero ..
     9.9  
    9.10  defs(overloaded)
    9.11    zero_matrix_def: "(0::('a::zero) matrix) == Abs_matrix(% j i. 0)"
    9.12 @@ -1183,7 +1183,7 @@
    9.13    apply (rule ext)+
    9.14    by (simp! add: Rep_mult_matrix max_ac)
    9.15  
    9.16 -instance matrix :: ("{ord,zero}") ord by intro_classes
    9.17 +instance matrix :: ("{ord, zero}") ord ..
    9.18  
    9.19  defs (overloaded)
    9.20    le_matrix_def: "(A::('a::{ord,zero}) matrix) <= B == ! j i. (Rep_matrix A j i) <= (Rep_matrix B j i)"
    10.1 --- a/src/HOL/Nat.thy	Sat May 01 21:59:12 2004 +0200
    10.2 +++ b/src/HOL/Nat.thy	Sat May 01 22:01:57 2004 +0200
    10.3 @@ -41,9 +41,7 @@
    10.4  typedef (open Nat)
    10.5    nat = Nat by (rule exI, rule Nat.Zero_RepI)
    10.6  
    10.7 -instance nat :: ord ..
    10.8 -instance nat :: zero ..
    10.9 -instance nat :: one ..
   10.10 +instance nat :: "{ord, zero, one}" ..
   10.11  
   10.12  
   10.13  text {* Abstract constants and syntax *}
   10.14 @@ -462,16 +460,14 @@
   10.15  
   10.16  text {* Type {@typ nat} is a wellfounded linear order *}
   10.17  
   10.18 -instance nat :: order by (intro_classes,
   10.19 -  (assumption | rule le_refl le_trans le_anti_sym nat_less_le)+)
   10.20 -instance nat :: linorder by (intro_classes, rule nat_le_linear)
   10.21 -instance nat :: wellorder by (intro_classes, rule wf_less)
   10.22 -
   10.23 +instance nat :: "{order, linorder, wellorder}"
   10.24 +  by intro_classes
   10.25 +    (assumption |
   10.26 +      rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
   10.27  
   10.28  lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
   10.29    by (blast elim!: less_SucE)
   10.30  
   10.31 -
   10.32  text {*
   10.33    Rewrite @{term "n < Suc m"} to @{term "n = m"}
   10.34    if @{term "~ n < m"} or @{term "m \<le> n"} hold.
   10.35 @@ -506,10 +502,7 @@
   10.36  
   10.37  text {* arithmetic operators @{text "+ -"} and @{text "*"} *}
   10.38  
   10.39 -instance nat :: plus ..
   10.40 -instance nat :: minus ..
   10.41 -instance nat :: times ..
   10.42 -instance nat :: power ..
   10.43 +instance nat :: "{plus, minus, times, power}" ..
   10.44  
   10.45  text {* size of a datatype value; overloaded *}
   10.46  consts size :: "'a => nat"
    11.1 --- a/src/HOL/Real/PReal.thy	Sat May 01 21:59:12 2004 +0200
    11.2 +++ b/src/HOL/Real/PReal.thy	Sat May 01 22:01:57 2004 +0200
    11.3 @@ -50,12 +50,7 @@
    11.4  typedef preal = "{A. cut A}"
    11.5    by (blast intro: cut_of_rat [OF zero_less_one])
    11.6  
    11.7 -instance preal :: ord ..
    11.8 -instance preal :: plus ..
    11.9 -instance preal :: minus ..
   11.10 -instance preal :: times ..
   11.11 -instance preal :: inverse ..
   11.12 -
   11.13 +instance preal :: "{ord, plus, minus, times, inverse}" ..
   11.14  
   11.15  constdefs
   11.16    preal_of_rat :: "rat => preal"
   11.17 @@ -211,9 +206,9 @@
   11.18  by (simp add: preal_le_def preal_less_def Rep_preal_inject psubset_def)
   11.19  
   11.20  instance preal :: order
   11.21 -proof qed
   11.22 - (assumption |
   11.23 -  rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
   11.24 +  by intro_classes
   11.25 +    (assumption |
   11.26 +      rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
   11.27  
   11.28  lemma preal_imp_pos: "[|A \<in> preal; r \<in> A|] ==> 0 < r"
   11.29  by (insert preal_imp_psubset_positives, blast)
   11.30 @@ -226,7 +221,7 @@
   11.31  done
   11.32  
   11.33  instance preal :: linorder
   11.34 -  by (intro_classes, rule preal_le_linear)
   11.35 +  by intro_classes (rule preal_le_linear)
   11.36  
   11.37  
   11.38  
    12.1 --- a/src/HOL/Real/Rational.thy	Sat May 01 21:59:12 2004 +0200
    12.2 +++ b/src/HOL/Real/Rational.thy	Sat May 01 22:01:57 2004 +0200
    12.3 @@ -4,10 +4,7 @@
    12.4      License: GPL (GNU GENERAL PUBLIC LICENSE)
    12.5  *)
    12.6  
    12.7 -header {*
    12.8 -  \title{Rational numbers}
    12.9 -  \author{Markus Wenzel}
   12.10 -*}
   12.11 +header {* Rational numbers *}
   12.12  
   12.13  theory Rational = Quotient + Main
   12.14  files ("rat_arith.ML"):
   12.15 @@ -117,13 +114,7 @@
   12.16   to equivalence of fractions.
   12.17  *}
   12.18  
   12.19 -instance fraction :: zero ..
   12.20 -instance fraction :: one ..
   12.21 -instance fraction :: plus ..
   12.22 -instance fraction :: minus ..
   12.23 -instance fraction :: times ..
   12.24 -instance fraction :: inverse ..
   12.25 -instance fraction :: ord ..
   12.26 +instance fraction :: "{zero, one, plus, minus, times, inverse, ord}" ..
   12.27  
   12.28  defs (overloaded)
   12.29    zero_fraction_def: "0 == fract 0 1"
   12.30 @@ -354,13 +345,7 @@
   12.31  
   12.32  subsubsection {* Standard operations on rational numbers *}
   12.33  
   12.34 -instance rat :: zero ..
   12.35 -instance rat :: one ..
   12.36 -instance rat :: plus ..
   12.37 -instance rat :: minus ..
   12.38 -instance rat :: times ..
   12.39 -instance rat :: inverse ..
   12.40 -instance rat :: ord ..
   12.41 +instance rat :: "{zero, one, plus, minus, times, inverse, ord}" ..
   12.42  
   12.43  defs (overloaded)
   12.44    zero_rat_def: "0 == rat_of 0"
   12.45 @@ -369,7 +354,7 @@
   12.46    minus_rat_def: "-q == rat_of (-(fraction_of q))"
   12.47    diff_rat_def: "q - r == q + (-(r::rat))"
   12.48    mult_rat_def: "q * r == rat_of (fraction_of q * fraction_of r)"
   12.49 -  inverse_rat_def: "inverse q == 
   12.50 +  inverse_rat_def: "inverse q ==
   12.51                      if q=0 then 0 else rat_of (inverse (fraction_of q))"
   12.52    divide_rat_def: "q / r == q * inverse (r::rat)"
   12.53    le_rat_def: "q \<le> r == fraction_of q \<le> fraction_of r"
   12.54 @@ -377,7 +362,7 @@
   12.55    abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)"
   12.56  
   12.57  theorem zero_rat: "0 = Fract 0 1"
   12.58 -  by (simp add: zero_rat_def zero_fraction_def rat_of_def Fract_def)        
   12.59 +  by (simp add: zero_rat_def zero_fraction_def rat_of_def Fract_def)
   12.60  
   12.61  theorem one_rat: "1 = Fract 1 1"
   12.62    by (simp add: one_rat_def one_fraction_def rat_of_def Fract_def)
   12.63 @@ -470,14 +455,14 @@
   12.64  
   12.65  theorem abs_rat: "b \<noteq> 0 ==> \<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
   12.66    by (simp add: abs_rat_def minus_rat zero_rat less_rat eq_rat)
   12.67 -     (auto simp add: mult_less_0_iff zero_less_mult_iff order_le_less 
   12.68 +     (auto simp add: mult_less_0_iff zero_less_mult_iff order_le_less
   12.69                  split: abs_split)
   12.70  
   12.71  
   12.72  subsubsection {* The ordered field of rational numbers *}
   12.73  
   12.74  lemma rat_add_assoc: "(q + r) + s = q + (r + (s::rat))"
   12.75 -  by (induct q, induct r, induct s) 
   12.76 +  by (induct q, induct r, induct s)
   12.77       (simp add: add_rat add_ac mult_ac int_distrib)
   12.78  
   12.79  lemma rat_add_0: "0 + q = (q::rat)"
   12.80 @@ -507,14 +492,14 @@
   12.81    show "1 * q = q"
   12.82      by (induct q) (simp add: one_rat mult_rat)
   12.83    show "(q + r) * s = q * s + r * s"
   12.84 -    by (induct q, induct r, induct s) 
   12.85 +    by (induct q, induct r, induct s)
   12.86         (simp add: add_rat mult_rat eq_rat int_distrib)
   12.87    show "q \<noteq> 0 ==> inverse q * q = 1"
   12.88      by (induct q) (simp add: inverse_rat mult_rat one_rat zero_rat eq_rat)
   12.89    show "q / r = q * inverse r"
   12.90 -    by (simp add: divide_rat_def) 
   12.91 +    by (simp add: divide_rat_def)
   12.92    show "0 \<noteq> (1::rat)"
   12.93 -    by (simp add: zero_rat one_rat eq_rat) 
   12.94 +    by (simp add: zero_rat one_rat eq_rat)
   12.95  qed
   12.96  
   12.97  instance rat :: linorder
   12.98 @@ -638,7 +623,7 @@
   12.99  subsection {* Various Other Results *}
  12.100  
  12.101  lemma minus_rat_cancel [simp]: "b \<noteq> 0 ==> Fract (-a) (-b) = Fract a b"
  12.102 -by (simp add: Fract_equality eq_fraction_iff) 
  12.103 +by (simp add: Fract_equality eq_fraction_iff)
  12.104  
  12.105  theorem Rat_induct_pos [case_names Fract, induct type: rat]:
  12.106    assumes step: "!!a b. 0 < b ==> P (Fract a b)"
  12.107 @@ -658,44 +643,43 @@
  12.108  
  12.109  lemma zero_less_Fract_iff:
  12.110       "0 < b ==> (0 < Fract a b) = (0 < a)"
  12.111 -by (simp add: zero_rat less_rat order_less_imp_not_eq2 zero_less_mult_iff) 
  12.112 +by (simp add: zero_rat less_rat order_less_imp_not_eq2 zero_less_mult_iff)
  12.113  
  12.114  lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1"
  12.115  apply (insert add_rat [of concl: m n 1 1])
  12.116 -apply (simp add: one_rat  [symmetric]) 
  12.117 +apply (simp add: one_rat  [symmetric])
  12.118  done
  12.119  
  12.120  lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
  12.121 -apply (induct k) 
  12.122 -apply (simp add: zero_rat) 
  12.123 -apply (simp add: Fract_add_one) 
  12.124 +apply (induct k)
  12.125 +apply (simp add: zero_rat)
  12.126 +apply (simp add: Fract_add_one)
  12.127  done
  12.128  
  12.129  lemma Fract_of_int_eq: "Fract k 1 = of_int k"
  12.130 -proof (cases k rule: int_cases) 
  12.131 +proof (cases k rule: int_cases)
  12.132    case (nonneg n)
  12.133      thus ?thesis by (simp add: int_eq_of_nat Fract_of_nat_eq)
  12.134 -next 
  12.135 +next
  12.136    case (neg n)
  12.137      hence "Fract k 1 = - (Fract (of_nat (Suc n)) 1)"
  12.138 -      by (simp only: minus_rat int_eq_of_nat) 
  12.139 +      by (simp only: minus_rat int_eq_of_nat)
  12.140      also have "... =  - (of_nat (Suc n))"
  12.141        by (simp only: Fract_of_nat_eq)
  12.142 -    finally show ?thesis 
  12.143 -      by (simp add: only: prems int_eq_of_nat of_int_minus of_int_of_nat_eq) 
  12.144 -qed 
  12.145 +    finally show ?thesis
  12.146 +      by (simp add: only: prems int_eq_of_nat of_int_minus of_int_of_nat_eq)
  12.147 +qed
  12.148  
  12.149  
  12.150 -
  12.151 -subsection{*Numerals and Arithmetic*}
  12.152 +subsection {* Numerals and Arithmetic *}
  12.153  
  12.154  instance rat :: number ..
  12.155  
  12.156 -primrec (*the type constraint is essential!*)
  12.157 +primrec  -- {* the type constraint is essential! *}
  12.158    number_of_Pls: "number_of bin.Pls = 0"
  12.159    number_of_Min: "number_of bin.Min = - (1::rat)"
  12.160    number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
  12.161 -	                               (number_of w) + (number_of w)"
  12.162 +                                       (number_of w) + (number_of w)"
  12.163  
  12.164  declare number_of_Pls [simp del]
  12.165          number_of_Min [simp del]
    13.1 --- a/src/HOL/Real/RealDef.thy	Sat May 01 21:59:12 2004 +0200
    13.2 +++ b/src/HOL/Real/RealDef.thy	Sat May 01 22:01:57 2004 +0200
    13.3 @@ -17,13 +17,7 @@
    13.4  typedef (Real)  real = "UNIV//realrel"
    13.5    by (auto simp add: quotient_def)
    13.6  
    13.7 -instance real :: ord ..
    13.8 -instance real :: zero ..
    13.9 -instance real :: one ..
   13.10 -instance real :: plus ..
   13.11 -instance real :: times ..
   13.12 -instance real :: minus ..
   13.13 -instance real :: inverse ..
   13.14 +instance real :: "{ord, zero, one, plus, times, minus, inverse}" ..
   13.15  
   13.16  constdefs
   13.17  
   13.18 @@ -41,6 +35,9 @@
   13.19     (*overloaded constant for injecting other types into "real"*)
   13.20     real :: "'a => real"
   13.21  
   13.22 +syntax (xsymbols)
   13.23 +  Reals     :: "'a set"                   ("\<real>")
   13.24 +
   13.25  
   13.26  defs (overloaded)
   13.27  
   13.28 @@ -83,9 +80,6 @@
   13.29    real_abs_def:  "abs (r::real) == (if 0 \<le> r then r else -r)"
   13.30  
   13.31  
   13.32 -syntax (xsymbols)
   13.33 -  Reals     :: "'a set"                   ("\<real>")
   13.34 -
   13.35  
   13.36  subsection{*Proving that realrel is an equivalence relation*}
   13.37