define (1::preal); clean up instance declarations
authorhuffman
Thu Jun 07 03:11:31 2007 +0200 (2007-06-07)
changeset 23287063039db59dd
parent 23286 85e7e043b980
child 23288 3e45b5464d2b
define (1::preal); clean up instance declarations
src/HOL/Real/PReal.thy
src/HOL/Real/RealDef.thy
     1.1 --- a/src/HOL/Real/PReal.thy	Thu Jun 07 02:34:37 2007 +0200
     1.2 +++ b/src/HOL/Real/PReal.thy	Thu Jun 07 03:11:31 2007 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4  typedef preal = "{A. cut A}"
     1.5    by (blast intro: cut_of_rat [OF zero_less_one])
     1.6  
     1.7 -instance preal :: "{ord, plus, minus, times, inverse}" ..
     1.8 +instance preal :: "{ord, plus, minus, times, inverse, one}" ..
     1.9  
    1.10  definition
    1.11    preal_of_rat :: "rat => preal" where
    1.12 @@ -100,6 +100,9 @@
    1.13    preal_inverse_def:
    1.14      "inverse R == Abs_preal (inverse_set (Rep_preal R))"
    1.15  
    1.16 +  preal_one_def:
    1.17 +    "1 == preal_of_rat 1"
    1.18 +
    1.19  
    1.20  text{*Reduces equality on abstractions to equality on representatives*}
    1.21  declare Abs_preal_inject [simp]
    1.22 @@ -334,11 +337,15 @@
    1.23  apply (force simp add: add_set_def add_ac)
    1.24  done
    1.25  
    1.26 +instance preal :: ab_semigroup_add
    1.27 +proof
    1.28 +  fix a b c :: preal
    1.29 +  show "(a + b) + c = a + (b + c)" by (rule preal_add_assoc)
    1.30 +  show "a + b = b + a" by (rule preal_add_commute)
    1.31 +qed
    1.32 +
    1.33  lemma preal_add_left_commute: "x + (y + z) = y + ((x + z)::preal)"
    1.34 -  apply (rule mk_left_commute [of "op +"])
    1.35 -  apply (rule preal_add_assoc)
    1.36 -  apply (rule preal_add_commute)
    1.37 -  done
    1.38 +by (rule add_left_commute)
    1.39  
    1.40  text{* Positive Real addition is an AC operator *}
    1.41  lemmas preal_add_ac = preal_add_assoc preal_add_commute preal_add_left_commute
    1.42 @@ -465,11 +472,15 @@
    1.43  apply (force simp add: mult_set_def mult_ac)
    1.44  done
    1.45  
    1.46 +instance preal :: ab_semigroup_mult
    1.47 +proof
    1.48 +  fix a b c :: preal
    1.49 +  show "(a * b) * c = a * (b * c)" by (rule preal_mult_assoc)
    1.50 +  show "a * b = b * a" by (rule preal_mult_commute)
    1.51 +qed
    1.52 +
    1.53  lemma preal_mult_left_commute: "x * (y * z) = y * ((x * z)::preal)"
    1.54 -  apply (rule mk_left_commute [of "op *"])
    1.55 -  apply (rule preal_mult_assoc)
    1.56 -  apply (rule preal_mult_commute)
    1.57 -  done
    1.58 +by (rule mult_left_commute)
    1.59  
    1.60  
    1.61  text{* Positive Real multiplication is an AC operator *}
    1.62 @@ -479,7 +490,8 @@
    1.63  
    1.64  text{* Positive real 1 is the multiplicative identity element *}
    1.65  
    1.66 -lemma preal_mult_1: "(preal_of_rat 1) * z = z"
    1.67 +lemma preal_mult_1: "(1::preal) * z = z"
    1.68 +unfolding preal_one_def
    1.69  proof (induct z)
    1.70    fix A :: "rat set"
    1.71    assume A: "A \<in> preal"
    1.72 @@ -525,11 +537,11 @@
    1.73                    rat_mem_preal A)
    1.74  qed
    1.75  
    1.76 +instance preal :: comm_monoid_mult
    1.77 +by intro_classes (rule preal_mult_1)
    1.78  
    1.79 -lemma preal_mult_1_right: "z * (preal_of_rat 1) = z"
    1.80 -apply (rule preal_mult_commute [THEN subst])
    1.81 -apply (rule preal_mult_1)
    1.82 -done
    1.83 +lemma preal_mult_1_right: "z * (1::preal) = z"
    1.84 +by (rule mult_1_right)
    1.85  
    1.86  
    1.87  subsection{*Distribution of Multiplication across Addition*}
    1.88 @@ -596,6 +608,9 @@
    1.89  lemma preal_add_mult_distrib: "(((x::preal) + y) * w) = (x * w) + (y * w)"
    1.90  by (simp add: preal_mult_commute preal_add_mult_distrib2)
    1.91  
    1.92 +instance preal :: comm_semiring
    1.93 +by intro_classes (rule preal_add_mult_distrib)
    1.94 +
    1.95  
    1.96  subsection{*Existence of Inverse, a Positive Real*}
    1.97  
    1.98 @@ -875,12 +890,13 @@
    1.99  apply (blast intro: inverse_mult_subset_lemma) 
   1.100  done
   1.101  
   1.102 -lemma preal_mult_inverse: "inverse R * R = (preal_of_rat 1)"
   1.103 +lemma preal_mult_inverse: "inverse R * R = (1::preal)"
   1.104 +unfolding preal_one_def
   1.105  apply (rule Rep_preal_inject [THEN iffD1])
   1.106  apply (rule equalityI [OF inverse_mult_subset subset_inverse_mult]) 
   1.107  done
   1.108  
   1.109 -lemma preal_mult_inverse_right: "R * inverse R = (preal_of_rat 1)"
   1.110 +lemma preal_mult_inverse_right: "R * inverse R = (1::preal)"
   1.111  apply (rule preal_mult_commute [THEN subst])
   1.112  apply (rule preal_mult_inverse)
   1.113  done
   1.114 @@ -1131,11 +1147,8 @@
   1.115  instance preal :: ordered_cancel_ab_semigroup_add
   1.116  proof
   1.117    fix a b c :: preal
   1.118 -  show "a + b + c = a + (b + c)" by (rule preal_add_assoc)
   1.119 -  show "a + b = b + a" by (rule preal_add_commute)
   1.120    show "a + b = a + c \<Longrightarrow> b = c" by (rule preal_add_left_cancel)
   1.121 -  show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   1.122 -    by (simp only: preal_add_le_cancel_left)
   1.123 +  show "a \<le> b \<Longrightarrow> c + a \<le> c + b" by (simp only: preal_add_le_cancel_left)
   1.124  qed
   1.125  
   1.126  
     2.1 --- a/src/HOL/Real/RealDef.thy	Thu Jun 07 02:34:37 2007 +0200
     2.2 +++ b/src/HOL/Real/RealDef.thy	Thu Jun 07 03:11:31 2007 +0200
     2.3 @@ -37,12 +37,10 @@
     2.4  defs (overloaded)
     2.5  
     2.6    real_zero_def:
     2.7 -  "0 == Abs_Real(realrel``{(preal_of_rat 1, preal_of_rat 1)})"
     2.8 +  "0 == Abs_Real(realrel``{(1, 1)})"
     2.9  
    2.10    real_one_def:
    2.11 -  "1 == Abs_Real(realrel``
    2.12 -               {(preal_of_rat 1 + preal_of_rat 1,
    2.13 -		 preal_of_rat 1)})"
    2.14 +  "1 == Abs_Real(realrel``{(1 + 1, 1)})"
    2.15  
    2.16    real_minus_def:
    2.17    "- r ==  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
    2.18 @@ -61,7 +59,7 @@
    2.19  		 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
    2.20  
    2.21    real_inverse_def:
    2.22 -  "inverse (R::real) == (SOME S. (R = 0 & S = 0) | S * R = 1)"
    2.23 +  "inverse (R::real) == (THE S. (R = 0 & S = 0) | S * R = 1)"
    2.24  
    2.25    real_divide_def:
    2.26    "R / (S::real) == R * inverse S"
    2.27 @@ -75,21 +73,20 @@
    2.28    real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)"
    2.29  
    2.30  
    2.31 -
    2.32 -subsection{*Proving that realrel is an equivalence relation*}
    2.33 +subsection {* Equivalence relation over positive reals *}
    2.34  
    2.35  lemma preal_trans_lemma:
    2.36    assumes "x + y1 = x1 + y"
    2.37        and "x + y2 = x2 + y"
    2.38    shows "x1 + y2 = x2 + (y1::preal)"
    2.39  proof -
    2.40 -  have "(x1 + y2) + x = (x + y2) + x1" by (simp add: preal_add_ac) 
    2.41 +  have "(x1 + y2) + x = (x + y2) + x1" by (simp add: add_ac)
    2.42    also have "... = (x2 + y) + x1"  by (simp add: prems)
    2.43 -  also have "... = x2 + (x1 + y)"  by (simp add: preal_add_ac)
    2.44 +  also have "... = x2 + (x1 + y)"  by (simp add: add_ac)
    2.45    also have "... = x2 + (x + y1)"  by (simp add: prems)
    2.46 -  also have "... = (x2 + y1) + x"  by (simp add: preal_add_ac)
    2.47 +  also have "... = (x2 + y1) + x"  by (simp add: add_ac)
    2.48    finally have "(x1 + y2) + x = (x2 + y1) + x" .
    2.49 -  thus ?thesis by (simp add: preal_add_right_cancel_iff) 
    2.50 +  thus ?thesis by (rule add_right_imp_eq)
    2.51  qed
    2.52  
    2.53  
    2.54 @@ -126,15 +123,15 @@
    2.55  done
    2.56  
    2.57  
    2.58 -subsection{*Congruence property for addition*}
    2.59 +subsection {* Addition and Subtraction *}
    2.60  
    2.61  lemma real_add_congruent2_lemma:
    2.62       "[|a + ba = aa + b; ab + bc = ac + bb|]
    2.63        ==> a + ab + (ba + bc) = aa + ac + (b + (bb::preal))"
    2.64 -apply (simp add: preal_add_assoc) 
    2.65 -apply (rule preal_add_left_commute [of ab, THEN ssubst])
    2.66 -apply (simp add: preal_add_assoc [symmetric])
    2.67 -apply (simp add: preal_add_ac)
    2.68 +apply (simp add: add_assoc)
    2.69 +apply (rule add_left_commute [of ab, THEN ssubst])
    2.70 +apply (simp add: add_assoc [symmetric])
    2.71 +apply (simp add: add_ac)
    2.72  done
    2.73  
    2.74  lemma real_add:
    2.75 @@ -149,23 +146,6 @@
    2.76                    UN_equiv_class2 [OF equiv_realrel equiv_realrel])
    2.77  qed
    2.78  
    2.79 -lemma real_add_commute: "(z::real) + w = w + z"
    2.80 -by (cases z, cases w, simp add: real_add preal_add_ac)
    2.81 -
    2.82 -lemma real_add_assoc: "((z1::real) + z2) + z3 = z1 + (z2 + z3)"
    2.83 -by (cases z1, cases z2, cases z3, simp add: real_add preal_add_assoc)
    2.84 -
    2.85 -lemma real_add_zero_left: "(0::real) + z = z"
    2.86 -by (cases z, simp add: real_add real_zero_def preal_add_ac)
    2.87 -
    2.88 -instance real :: comm_monoid_add
    2.89 -  by (intro_classes,
    2.90 -      (assumption | 
    2.91 -       rule real_add_commute real_add_assoc real_add_zero_left)+)
    2.92 -
    2.93 -
    2.94 -subsection{*Additive Inverse on real*}
    2.95 -
    2.96  lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})"
    2.97  proof -
    2.98    have "(\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel"
    2.99 @@ -174,17 +154,29 @@
   2.100      by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel])
   2.101  qed
   2.102  
   2.103 -lemma real_add_minus_left: "(-z) + z = (0::real)"
   2.104 -by (cases z, simp add: real_minus real_add real_zero_def preal_add_commute)
   2.105 +instance real :: ab_group_add
   2.106 +proof
   2.107 +  fix x y z :: real
   2.108 +  show "(x + y) + z = x + (y + z)"
   2.109 +    by (cases x, cases y, cases z, simp add: real_add add_assoc)
   2.110 +  show "x + y = y + x"
   2.111 +    by (cases x, cases y, simp add: real_add add_commute)
   2.112 +  show "0 + x = x"
   2.113 +    by (cases x, simp add: real_add real_zero_def add_ac)
   2.114 +  show "- x + x = 0"
   2.115 +    by (cases x, simp add: real_minus real_add real_zero_def add_commute)
   2.116 +  show "x - y = x + - y"
   2.117 +    by (simp add: real_diff_def)
   2.118 +qed
   2.119  
   2.120  
   2.121 -subsection{*Congruence property for multiplication*}
   2.122 +subsection {* Multiplication *}
   2.123  
   2.124  lemma real_mult_congruent2_lemma:
   2.125       "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==>
   2.126            x * x1 + y * y1 + (x * y2 + y * x2) =
   2.127            x * x2 + y * y2 + (x * y1 + y * x1)"
   2.128 -apply (simp add: preal_add_left_commute preal_add_assoc [symmetric])
   2.129 +apply (simp add: add_left_commute add_assoc [symmetric])
   2.130  apply (simp add: preal_add_assoc preal_add_mult_distrib2 [symmetric])
   2.131  apply (simp add: preal_add_commute)
   2.132  done
   2.133 @@ -228,13 +220,23 @@
   2.134  text{*one and zero are distinct*}
   2.135  lemma real_zero_not_eq_one: "0 \<noteq> (1::real)"
   2.136  proof -
   2.137 -  have "preal_of_rat 1 < preal_of_rat 1 + preal_of_rat 1"
   2.138 -    by (simp add: preal_self_less_add_left) 
   2.139 +  have "(1::preal) < 1 + 1"
   2.140 +    by (simp add: preal_self_less_add_left)
   2.141    thus ?thesis
   2.142      by (simp add: real_zero_def real_one_def preal_add_right_cancel_iff)
   2.143  qed
   2.144  
   2.145 -subsection{*existence of inverse*}
   2.146 +instance real :: comm_ring_1
   2.147 +proof
   2.148 +  fix x y z :: real
   2.149 +  show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc)
   2.150 +  show "x * y = y * x" by (rule real_mult_commute)
   2.151 +  show "1 * x = x" by (rule real_mult_1)
   2.152 +  show "(x + y) * z = x * z + y * z" by (rule real_add_mult_distrib)
   2.153 +  show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
   2.154 +qed
   2.155 +
   2.156 +subsection {* Inverse and Division *}
   2.157  
   2.158  lemma real_zero_iff: "Abs_Real (realrel `` {(x, x)}) = 0"
   2.159  by (simp add: real_zero_def preal_add_commute)
   2.160 @@ -247,12 +249,10 @@
   2.161  apply (cut_tac x = xa and y = y in linorder_less_linear)
   2.162  apply (auto dest!: less_add_left_Ex simp add: real_zero_iff)
   2.163  apply (rule_tac
   2.164 -        x = "Abs_Real (realrel `` { (preal_of_rat 1, 
   2.165 -                            inverse (D) + preal_of_rat 1)}) " 
   2.166 +        x = "Abs_Real (realrel``{(1, inverse (D) + 1)})"
   2.167         in exI)
   2.168  apply (rule_tac [2]
   2.169 -        x = "Abs_Real (realrel `` { (inverse (D) + preal_of_rat 1,
   2.170 -                   preal_of_rat 1)})" 
   2.171 +        x = "Abs_Real (realrel``{(inverse (D) + 1, 1)})" 
   2.172         in exI)
   2.173  apply (auto simp add: real_mult preal_mult_1_right
   2.174                preal_add_mult_distrib2 preal_add_mult_distrib preal_mult_1
   2.175 @@ -261,8 +261,11 @@
   2.176  
   2.177  lemma real_mult_inverse_left: "x \<noteq> 0 ==> inverse(x)*x = (1::real)"
   2.178  apply (simp add: real_inverse_def)
   2.179 -apply (frule real_mult_inverse_left_ex, safe)
   2.180 -apply (rule someI2, auto)
   2.181 +apply (drule real_mult_inverse_left_ex, safe)
   2.182 +apply (rule theI, assumption, rename_tac z)
   2.183 +apply (subgoal_tac "(z * x) * y = z * (x * y)")
   2.184 +apply (simp add: mult_commute)
   2.185 +apply (rule mult_assoc)
   2.186  done
   2.187  
   2.188  
   2.189 @@ -271,13 +274,6 @@
   2.190  instance real :: field
   2.191  proof
   2.192    fix x y z :: real
   2.193 -  show "- x + x = 0" by (rule real_add_minus_left)
   2.194 -  show "x - y = x + (-y)" by (simp add: real_diff_def)
   2.195 -  show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc)
   2.196 -  show "x * y = y * x" by (rule real_mult_commute)
   2.197 -  show "1 * x = x" by (rule real_mult_1)
   2.198 -  show "(x + y) * z = x * z + y * z" by (simp add: real_add_mult_distrib)
   2.199 -  show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
   2.200    show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left)
   2.201    show "x / y = x * inverse y" by (simp add: real_divide_def)
   2.202  qed