src/HOL/Real/RealDef.thy
changeset 15169 2b5da07a0b89
parent 15140 322485b816ac
child 15229 1eb23f805c06
     1.1 --- a/src/HOL/Real/RealDef.thy	Wed Sep 01 15:03:41 2004 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Wed Sep 01 15:04:01 2004 +0200
     1.3 @@ -154,8 +154,8 @@
     1.4       "Abs_Real (realrel``{(x,y)}) + Abs_Real (realrel``{(u,v)}) =
     1.5        Abs_Real (realrel``{(x+u, y+v)})"
     1.6  proof -
     1.7 -  have "congruent2 realrel realrel
     1.8 -        (\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)"
     1.9 +  have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)
    1.10 +        respects2 realrel"
    1.11      by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma) 
    1.12    thus ?thesis
    1.13      by (simp add: real_add_def UN_UN_split_split_eq
    1.14 @@ -181,7 +181,7 @@
    1.15  
    1.16  lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})"
    1.17  proof -
    1.18 -  have "congruent realrel (\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})})"
    1.19 +  have "(\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel"
    1.20      by (simp add: congruent_def preal_add_commute) 
    1.21    thus ?thesis
    1.22      by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel])
    1.23 @@ -203,9 +203,10 @@
    1.24  done
    1.25  
    1.26  lemma real_mult_congruent2:
    1.27 -    "congruent2 realrel realrel (%p1 p2.
    1.28 +    "(%p1 p2.
    1.29          (%(x1,y1). (%(x2,y2). 
    1.30 -          { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1)"
    1.31 +          { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1)
    1.32 +     respects2 realrel"
    1.33  apply (rule congruent2_commuteI [OF equiv_realrel], clarify)
    1.34  apply (simp add: preal_mult_commute preal_add_commute)
    1.35  apply (auto simp add: real_mult_congruent2_lemma)