src/HOL/Real/RealDef.thy
changeset 23288 3e45b5464d2b
parent 23287 063039db59dd
child 23289 0cf371d943b1
     1.1 --- a/src/HOL/Real/RealDef.thy	Thu Jun 07 03:11:31 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Thu Jun 07 03:45:56 2007 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4    (** these don't use the overloaded "real" function: users don't see them **)
     1.5  
     1.6    real_of_preal :: "preal => real" where
     1.7 -  "real_of_preal m = Abs_Real(realrel``{(m + preal_of_rat 1, preal_of_rat 1)})"
     1.8 +  "real_of_preal m = Abs_Real(realrel``{(m + 1, 1)})"
     1.9  
    1.10  consts
    1.11     (*overloaded constant for injecting other types into "real"*)
    1.12 @@ -149,7 +149,7 @@
    1.13  lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})"
    1.14  proof -
    1.15    have "(\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel"
    1.16 -    by (simp add: congruent_def preal_add_commute) 
    1.17 +    by (simp add: congruent_def add_commute) 
    1.18    thus ?thesis
    1.19      by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel])
    1.20  qed
    1.21 @@ -177,8 +177,8 @@
    1.22            x * x1 + y * y1 + (x * y2 + y * x2) =
    1.23            x * x2 + y * y2 + (x * y1 + y * x1)"
    1.24  apply (simp add: add_left_commute add_assoc [symmetric])
    1.25 -apply (simp add: preal_add_assoc preal_add_mult_distrib2 [symmetric])
    1.26 -apply (simp add: preal_add_commute)
    1.27 +apply (simp add: add_assoc right_distrib [symmetric])
    1.28 +apply (simp add: add_commute)
    1.29  done
    1.30  
    1.31  lemma real_mult_congruent2:
    1.32 @@ -187,7 +187,7 @@
    1.33            { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1)
    1.34       respects2 realrel"
    1.35  apply (rule congruent2_commuteI [OF equiv_realrel], clarify)
    1.36 -apply (simp add: preal_mult_commute preal_add_commute)
    1.37 +apply (simp add: mult_commute add_commute)
    1.38  apply (auto simp add: real_mult_congruent2_lemma)
    1.39  done
    1.40  
    1.41 @@ -198,23 +198,22 @@
    1.42           UN_equiv_class2 [OF equiv_realrel equiv_realrel real_mult_congruent2])
    1.43  
    1.44  lemma real_mult_commute: "(z::real) * w = w * z"
    1.45 -by (cases z, cases w, simp add: real_mult preal_add_ac preal_mult_ac)
    1.46 +by (cases z, cases w, simp add: real_mult add_ac mult_ac)
    1.47  
    1.48  lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)"
    1.49  apply (cases z1, cases z2, cases z3)
    1.50 -apply (simp add: real_mult preal_add_mult_distrib2 preal_add_ac preal_mult_ac)
    1.51 +apply (simp add: real_mult right_distrib add_ac mult_ac)
    1.52  done
    1.53  
    1.54  lemma real_mult_1: "(1::real) * z = z"
    1.55  apply (cases z)
    1.56 -apply (simp add: real_mult real_one_def preal_add_mult_distrib2
    1.57 -                 preal_mult_1_right preal_mult_ac preal_add_ac)
    1.58 +apply (simp add: real_mult real_one_def right_distrib
    1.59 +                  mult_1_right mult_ac add_ac)
    1.60  done
    1.61  
    1.62  lemma real_add_mult_distrib: "((z1::real) + z2) * w = (z1 * w) + (z2 * w)"
    1.63  apply (cases z1, cases z2, cases w)
    1.64 -apply (simp add: real_add real_mult preal_add_mult_distrib2 
    1.65 -                 preal_add_ac preal_mult_ac)
    1.66 +apply (simp add: real_add real_mult right_distrib add_ac mult_ac)
    1.67  done
    1.68  
    1.69  text{*one and zero are distinct*}
    1.70 @@ -223,7 +222,7 @@
    1.71    have "(1::preal) < 1 + 1"
    1.72      by (simp add: preal_self_less_add_left)
    1.73    thus ?thesis
    1.74 -    by (simp add: real_zero_def real_one_def preal_add_right_cancel_iff)
    1.75 +    by (simp add: real_zero_def real_one_def)
    1.76  qed
    1.77  
    1.78  instance real :: comm_ring_1
    1.79 @@ -239,7 +238,7 @@
    1.80  subsection {* Inverse and Division *}
    1.81  
    1.82  lemma real_zero_iff: "Abs_Real (realrel `` {(x, x)}) = 0"
    1.83 -by (simp add: real_zero_def preal_add_commute)
    1.84 +by (simp add: real_zero_def add_commute)
    1.85  
    1.86  text{*Instead of using an existential quantifier and constructing the inverse
    1.87  within the proof, we could define the inverse explicitly.*}
    1.88 @@ -254,9 +253,8 @@
    1.89  apply (rule_tac [2]
    1.90          x = "Abs_Real (realrel``{(inverse (D) + 1, 1)})" 
    1.91         in exI)
    1.92 -apply (auto simp add: real_mult preal_mult_1_right
    1.93 -              preal_add_mult_distrib2 preal_add_mult_distrib preal_mult_1
    1.94 -              preal_mult_inverse_right preal_add_ac preal_mult_ac)
    1.95 +apply (auto simp add: real_mult ring_distrib
    1.96 +              preal_mult_inverse_right add_ac mult_ac)
    1.97  done
    1.98  
    1.99  lemma real_mult_inverse_left: "x \<noteq> 0 ==> inverse(x)*x = (1::real)"
   1.100 @@ -302,9 +300,9 @@
   1.101    assumes eq: "a+b = c+d" and le: "c \<le> a"
   1.102    shows "b \<le> (d::preal)"
   1.103  proof -
   1.104 -  have "c+d \<le> a+d" by (simp add: prems preal_cancels)
   1.105 +  have "c+d \<le> a+d" by (simp add: prems)
   1.106    hence "a+b \<le> a+d" by (simp add: prems)
   1.107 -  thus "b \<le> d" by (simp add: preal_cancels)
   1.108 +  thus "b \<le> d" by simp
   1.109  qed
   1.110  
   1.111  lemma real_le_lemma:
   1.112 @@ -314,16 +312,15 @@
   1.113    shows "x1 + y2 \<le> x2 + (y1::preal)"
   1.114  proof -
   1.115    have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: prems)
   1.116 -  hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: preal_add_ac)
   1.117 -  also have "... \<le> (x2+y1) + (u2+v1)"
   1.118 -         by (simp add: prems preal_add_le_cancel_left)
   1.119 -  finally show ?thesis by (simp add: preal_add_le_cancel_right)
   1.120 -qed						 
   1.121 +  hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: add_ac)
   1.122 +  also have "... \<le> (x2+y1) + (u2+v1)" by (simp add: prems)
   1.123 +  finally show ?thesis by simp
   1.124 +qed
   1.125  
   1.126  lemma real_le: 
   1.127       "(Abs_Real(realrel``{(x1,y1)}) \<le> Abs_Real(realrel``{(x2,y2)})) =  
   1.128        (x1 + y2 \<le> x2 + y1)"
   1.129 -apply (simp add: real_le_def) 
   1.130 +apply (simp add: real_le_def)
   1.131  apply (auto intro: real_le_lemma)
   1.132  done
   1.133  
   1.134 @@ -336,19 +333,17 @@
   1.135        and "x2 + v2 = u2 + y2"
   1.136    shows "x + v' \<le> u' + (y::preal)"
   1.137  proof -
   1.138 -  have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: preal_add_ac)
   1.139 -  also have "... \<le> (u+y) + (u+v')" 
   1.140 -    by (simp add: preal_add_le_cancel_right prems) 
   1.141 -  also have "... \<le> (u+y) + (u'+v)" 
   1.142 -    by (simp add: preal_add_le_cancel_left prems) 
   1.143 -  also have "... = (u'+y) + (u+v)"  by (simp add: preal_add_ac)
   1.144 -  finally show ?thesis by (simp add: preal_add_le_cancel_right)
   1.145 +  have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: add_ac)
   1.146 +  also have "... \<le> (u+y) + (u+v')" by (simp add: prems)
   1.147 +  also have "... \<le> (u+y) + (u'+v)" by (simp add: prems)
   1.148 +  also have "... = (u'+y) + (u+v)"  by (simp add: add_ac)
   1.149 +  finally show ?thesis by simp
   1.150  qed
   1.151  
   1.152  lemma real_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::real)"
   1.153  apply (cases i, cases j, cases k)
   1.154  apply (simp add: real_le)
   1.155 -apply (blast intro: real_trans_lemma) 
   1.156 +apply (blast intro: real_trans_lemma)
   1.157  done
   1.158  
   1.159  (* Axiom 'order_less_le' of class 'order': *)
   1.160 @@ -362,8 +357,8 @@
   1.161  
   1.162  (* Axiom 'linorder_linear' of class 'linorder': *)
   1.163  lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
   1.164 -apply (cases z, cases w) 
   1.165 -apply (auto simp add: real_le real_zero_def preal_add_ac preal_cancels)
   1.166 +apply (cases z, cases w)
   1.167 +apply (auto simp add: real_le real_zero_def add_ac)
   1.168  done
   1.169  
   1.170  
   1.171 @@ -374,8 +369,8 @@
   1.172  lemma real_le_eq_diff: "(x \<le> y) = (x-y \<le> (0::real))"
   1.173  apply (cases x, cases y) 
   1.174  apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus
   1.175 -                      preal_add_ac)
   1.176 -apply (simp_all add: preal_add_assoc [symmetric] preal_cancels)
   1.177 +                      add_ac)
   1.178 +apply (simp_all add: add_assoc [symmetric])
   1.179  done
   1.180  
   1.181  lemma real_add_left_mono: 
   1.182 @@ -400,8 +395,8 @@
   1.183                    real_zero_def real_le real_mult)
   1.184    --{*Reduce to the (simpler) @{text "\<le>"} relation *}
   1.185  apply (auto dest!: less_add_left_Ex
   1.186 -     simp add: preal_add_ac preal_mult_ac 
   1.187 -          preal_add_mult_distrib2 preal_cancels preal_self_less_add_left)
   1.188 +     simp add: add_ac mult_ac
   1.189 +          right_distrib preal_self_less_add_left)
   1.190  done
   1.191  
   1.192  lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y"
   1.193 @@ -433,36 +428,32 @@
   1.194  
   1.195  lemma real_of_preal_add:
   1.196       "real_of_preal ((x::preal) + y) = real_of_preal x + real_of_preal y"
   1.197 -by (simp add: real_of_preal_def real_add preal_add_mult_distrib preal_mult_1 
   1.198 -              preal_add_ac)
   1.199 +by (simp add: real_of_preal_def real_add left_distrib add_ac)
   1.200  
   1.201  lemma real_of_preal_mult:
   1.202       "real_of_preal ((x::preal) * y) = real_of_preal x* real_of_preal y"
   1.203 -by (simp add: real_of_preal_def real_mult preal_add_mult_distrib2
   1.204 -              preal_mult_1 preal_mult_1_right preal_add_ac preal_mult_ac)
   1.205 +by (simp add: real_of_preal_def real_mult right_distrib add_ac mult_ac)
   1.206  
   1.207  
   1.208  text{*Gleason prop 9-4.4 p 127*}
   1.209  lemma real_of_preal_trichotomy:
   1.210        "\<exists>m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)"
   1.211  apply (simp add: real_of_preal_def real_zero_def, cases x)
   1.212 -apply (auto simp add: real_minus preal_add_ac)
   1.213 +apply (auto simp add: real_minus add_ac)
   1.214  apply (cut_tac x = x and y = y in linorder_less_linear)
   1.215 -apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc [symmetric])
   1.216 +apply (auto dest!: less_add_left_Ex simp add: add_assoc [symmetric])
   1.217  done
   1.218  
   1.219  lemma real_of_preal_leD:
   1.220        "real_of_preal m1 \<le> real_of_preal m2 ==> m1 \<le> m2"
   1.221 -by (simp add: real_of_preal_def real_le preal_cancels)
   1.222 +by (simp add: real_of_preal_def real_le)
   1.223  
   1.224  lemma real_of_preal_lessI: "m1 < m2 ==> real_of_preal m1 < real_of_preal m2"
   1.225  by (auto simp add: real_of_preal_leD linorder_not_le [symmetric])
   1.226  
   1.227  lemma real_of_preal_lessD:
   1.228        "real_of_preal m1 < real_of_preal m2 ==> m1 < m2"
   1.229 -by (simp add: real_of_preal_def real_le linorder_not_le [symmetric] 
   1.230 -              preal_cancels) 
   1.231 -
   1.232 +by (simp add: real_of_preal_def real_le linorder_not_le [symmetric])
   1.233  
   1.234  lemma real_of_preal_less_iff [simp]:
   1.235       "(real_of_preal m1 < real_of_preal m2) = (m1 < m2)"
   1.236 @@ -470,15 +461,14 @@
   1.237  
   1.238  lemma real_of_preal_le_iff:
   1.239       "(real_of_preal m1 \<le> real_of_preal m2) = (m1 \<le> m2)"
   1.240 -by (simp add: linorder_not_less [symmetric]) 
   1.241 +by (simp add: linorder_not_less [symmetric])
   1.242  
   1.243  lemma real_of_preal_zero_less: "0 < real_of_preal m"
   1.244 -apply (auto simp add: real_zero_def real_of_preal_def real_less_def real_le_def
   1.245 -            preal_add_ac preal_cancels)
   1.246 -apply (simp_all add: preal_add_assoc [symmetric] preal_cancels)
   1.247 -apply (blast intro: preal_self_less_add_left order_less_imp_le)
   1.248 -apply (insert preal_not_eq_self [of "preal_of_rat 1" m]) 
   1.249 -apply (simp add: preal_add_ac) 
   1.250 +apply (insert preal_self_less_add_left [of 1 m])
   1.251 +apply (auto simp add: real_zero_def real_of_preal_def
   1.252 +                      real_less_def real_le_def add_ac)
   1.253 +apply (rule_tac x="m + 1" in exI, rule_tac x="1" in exI)
   1.254 +apply (simp add: add_ac)
   1.255  done
   1.256  
   1.257  lemma real_of_preal_minus_less_zero: "- real_of_preal m < 0"