equal
deleted
inserted
replaced
152 |
152 |
153 lemma real_add: |
153 lemma real_add: |
154 "Abs_Real (realrel``{(x,y)}) + Abs_Real (realrel``{(u,v)}) = |
154 "Abs_Real (realrel``{(x,y)}) + Abs_Real (realrel``{(u,v)}) = |
155 Abs_Real (realrel``{(x+u, y+v)})" |
155 Abs_Real (realrel``{(x+u, y+v)})" |
156 proof - |
156 proof - |
157 have "congruent2 realrel realrel |
157 have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z) |
158 (\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)" |
158 respects2 realrel" |
159 by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma) |
159 by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma) |
160 thus ?thesis |
160 thus ?thesis |
161 by (simp add: real_add_def UN_UN_split_split_eq |
161 by (simp add: real_add_def UN_UN_split_split_eq |
162 UN_equiv_class2 [OF equiv_realrel equiv_realrel]) |
162 UN_equiv_class2 [OF equiv_realrel equiv_realrel]) |
163 qed |
163 qed |
179 |
179 |
180 subsection{*Additive Inverse on real*} |
180 subsection{*Additive Inverse on real*} |
181 |
181 |
182 lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})" |
182 lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})" |
183 proof - |
183 proof - |
184 have "congruent realrel (\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})})" |
184 have "(\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel" |
185 by (simp add: congruent_def preal_add_commute) |
185 by (simp add: congruent_def preal_add_commute) |
186 thus ?thesis |
186 thus ?thesis |
187 by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel]) |
187 by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel]) |
188 qed |
188 qed |
189 |
189 |
201 apply (simp add: preal_add_assoc preal_add_mult_distrib2 [symmetric]) |
201 apply (simp add: preal_add_assoc preal_add_mult_distrib2 [symmetric]) |
202 apply (simp add: preal_add_commute) |
202 apply (simp add: preal_add_commute) |
203 done |
203 done |
204 |
204 |
205 lemma real_mult_congruent2: |
205 lemma real_mult_congruent2: |
206 "congruent2 realrel realrel (%p1 p2. |
206 "(%p1 p2. |
207 (%(x1,y1). (%(x2,y2). |
207 (%(x1,y1). (%(x2,y2). |
208 { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1)" |
208 { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1) |
|
209 respects2 realrel" |
209 apply (rule congruent2_commuteI [OF equiv_realrel], clarify) |
210 apply (rule congruent2_commuteI [OF equiv_realrel], clarify) |
210 apply (simp add: preal_mult_commute preal_add_commute) |
211 apply (simp add: preal_mult_commute preal_add_commute) |
211 apply (auto simp add: real_mult_congruent2_lemma) |
212 apply (auto simp add: real_mult_congruent2_lemma) |
212 done |
213 done |
213 |
214 |