--- a/src/HOL/Complex/CStar.thy Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Complex/CStar.thy Wed Sep 01 15:04:01 2004 +0200
@@ -206,9 +206,8 @@
by (simp add: starfunCR_n_def starfunCR_def)
lemma starfunC_congruent:
- "congruent hcomplexrel (%X. hcomplexrel``{%n. f (X n)})"
-apply (auto simp add: hcomplexrel_iff congruent_def, ultra)
-done
+ "(%X. hcomplexrel``{%n. f (X n)}) respects hcomplexrel"
+by (auto simp add: hcomplexrel_iff congruent_def, ultra)
(* f::complex => complex *)
lemma starfunC:
@@ -508,7 +507,7 @@
subsection{*Internal Functions - Some Redundancy With *Fc* Now*}
lemma starfunC_n_congruent:
- "congruent hcomplexrel (%X. hcomplexrel``{%n. f n (X n)})"
+ "(%X. hcomplexrel``{%n. f n (X n)}) respects hcomplexrel"
by (auto simp add: congruent_def hcomplexrel_iff, ultra)
lemma starfunC_n:
--- a/src/HOL/Complex/NSComplex.thy Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Complex/NSComplex.thy Wed Sep 01 15:04:01 2004 +0200
@@ -283,7 +283,7 @@
subsection{*Additive Inverse on Nonstandard Complex Numbers*}
lemma hcomplex_minus_congruent:
- "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"
+ "(%X. hcomplexrel `` {%n. - (X n)}) respects hcomplexrel"
by (simp add: congruent_def)
lemma hcomplex_minus:
--- a/src/HOL/Hyperreal/HyperDef.thy Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Wed Sep 01 15:04:01 2004 +0200
@@ -342,8 +342,7 @@
subsection{*Additive inverse on @{typ hypreal}*}
-lemma hypreal_minus_congruent:
- "congruent hyprel (%X. hyprel``{%n. - (X n)})"
+lemma hypreal_minus_congruent: "(%X. hyprel``{%n. - (X n)}) respects hyprel"
by (force simp add: congruent_def)
lemma hypreal_minus:
@@ -397,7 +396,7 @@
subsection{*Multiplicative Inverse on @{typ hypreal} *}
lemma hypreal_inverse_congruent:
- "congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})"
+ "(%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)}) respects hyprel"
by (auto simp add: congruent_def, ultra)
lemma hypreal_inverse:
--- a/src/HOL/Hyperreal/HyperNat.thy Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy Wed Sep 01 15:04:01 2004 +0200
@@ -136,7 +136,7 @@
subsection{*Hypernat Addition*}
lemma hypnat_add_congruent2:
- "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})"
+ "(%X Y. hypnatrel``{%n. X n + Y n}) respects2 hypnatrel"
by (simp add: congruent2_def, auto, ultra)
lemma hypnat_add:
@@ -170,7 +170,7 @@
lemma hypnat_minus_congruent2:
- "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})"
+ "(%X Y. hypnatrel``{%n. X n - Y n}) respects2 hypnatrel"
by (simp add: congruent2_def, auto, ultra)
lemma hypnat_minus:
@@ -238,7 +238,7 @@
subsection{*Hyperreal Multiplication*}
lemma hypnat_mult_congruent2:
- "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})"
+ "(%X Y. hypnatrel``{%n. X n * Y n}) respects2 hypnatrel"
by (simp add: congruent2_def, auto, ultra)
lemma hypnat_mult:
--- a/src/HOL/Hyperreal/HyperPow.thy Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy Wed Sep 01 15:04:01 2004 +0200
@@ -114,12 +114,8 @@
subsection{*Powers with Hypernatural Exponents*}
-lemma hyperpow_congruent:
- "congruent hyprel
- (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"
-apply (unfold congruent_def)
-apply (auto intro!: ext, fuf+)
-done
+lemma hyperpow_congruent: "(%X Y. hyprel``{%n. (X n ^ Y n)}) respects hyprel"
+by (auto simp add: congruent_def intro!: ext, fuf+)
lemma hyperpow:
"Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
--- a/src/HOL/Hyperreal/NatStar.thy Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy Wed Sep 01 15:04:01 2004 +0200
@@ -185,8 +185,7 @@
lemma starfunNat2_n_starfunNat2: "\<forall>n. (F n = f) ==> *fNat2n* F = *fNat2* f"
by (simp add: starfunNat2_n_def starfunNat2_def)
-lemma starfunNat_congruent:
- "congruent hypnatrel (%X. hypnatrel``{%n. f (X n)})"
+lemma starfunNat_congruent: "(%X. hypnatrel``{%n. f (X n)}) respects hypnatrel"
apply (simp add: congruent_def, safe)
apply (ultra+)
done
@@ -396,10 +395,8 @@
text{*Internal functions - some redundancy with *fNat* now*}
lemma starfunNat_n_congruent:
- "congruent hypnatrel (%X. hypnatrel``{%n. f n (X n)})"
-apply (simp add: congruent_def, safe)
-apply (ultra+)
-done
+ "(%X. hypnatrel``{%n. f n (X n)}) respects hypnatrel"
+by (auto simp add: congruent_def, ultra+)
lemma starfunNat_n:
"( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
--- a/src/HOL/Hyperreal/Star.thy Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Hyperreal/Star.thy Wed Sep 01 15:04:01 2004 +0200
@@ -53,9 +53,7 @@
apply (blast intro: LeastI)
done
-(*------------------------------------------------------------
- Properties of the *-transform applied to sets of reals
- ------------------------------------------------------------*)
+subsection{*Properties of the Star-transform Applied to Sets of Reals*}
lemma STAR_real_set: "*s*(UNIV::real set) = (UNIV::hypreal set)"
by (simp add: starset_def)
@@ -148,10 +146,8 @@
lemma STAR_subset_closed: "[| x : *s* A; A <= B |] ==> x : *s* B"
by (blast dest: STAR_subset)
-(*------------------------------------------------------------------
- Nonstandard extension of a set (defined using a constant
- sequence) as a special case of an internal set
- -----------------------------------------------------------------*)
+text{*Nonstandard extension of a set (defined using a constant
+ sequence) as a special case of an internal set*}
lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A"
by (simp add: starset_n_def starset_def)
@@ -197,11 +193,9 @@
apply (auto, ultra)
done
-(*-----------------------------------------------------------------------
- Nonstandard extension of functions- congruence
- -----------------------------------------------------------------------*)
+text{*Nonstandard extension of functions*}
-lemma starfun_congruent: "congruent hyprel (%X. hyprel``{%n. f (X n)})"
+lemma starfun_congruent: "(%X. hyprel``{%n. f (X n)}) respects hyprel"
by (simp add: congruent_def, auto, ultra)
lemma starfun:
@@ -272,9 +266,7 @@
apply (simp (no_asm) add: starfun_o2)
done
-(*--------------------------------------
- NS extension of constant function
- --------------------------------------*)
+text{*NS extension of constant function*}
lemma starfun_const_fun: "( *f* (%x. k)) xa = hypreal_of_real k"
apply (cases xa)
apply (auto simp add: starfun hypreal_of_real_def)
@@ -282,9 +274,7 @@
declare starfun_const_fun [simp]
-(*----------------------------------------------------
- the NS extension of the identity function
- ----------------------------------------------------*)
+text{*the NS extension of the identity function*}
lemma starfun_Idfun_approx: "x @= hypreal_of_real a ==> ( *f* (%x. x)) x @= hypreal_of_real a"
apply (cases x)
@@ -297,9 +287,7 @@
done
declare starfun_Id [simp]
-(*----------------------------------------------------------------------
- the *-function is a (nonstandard) extension of the function
- ----------------------------------------------------------------------*)
+text{*The Star-function is a (nonstandard) extension of the function*}
lemma is_starext_starfun: "is_starext ( *f* f) f"
apply (simp add: is_starext_def, auto)
@@ -308,9 +296,7 @@
apply (auto intro!: bexI simp add: starfun)
done
-(*----------------------------------------------------------------------
- Any nonstandard extension is in fact the *-function
- ----------------------------------------------------------------------*)
+text{*Any nonstandard extension is in fact the Star-function*}
lemma is_starfun_starext: "is_starext F f ==> F = *f* f"
apply (simp add: is_starext_def)
@@ -324,11 +310,9 @@
lemma is_starext_starfun_iff: "(is_starext F f) = (F = *f* f)"
by (blast intro: is_starfun_starext is_starext_starfun)
-(*--------------------------------------------------------
- extented function has same solution as its standard
+text{*extented function has same solution as its standard
version for real arguments. i.e they are the same
- for all real arguments
- -------------------------------------------------------*)
+ for all real arguments*}
lemma starfun_eq: "( *f* f) (hypreal_of_real a) = hypreal_of_real (f a)"
by (auto simp add: starfun hypreal_of_real_def)
@@ -360,10 +344,8 @@
apply (auto intro: approx_add)
done
-(*----------------------------------------------------
- Examples: hrabs is nonstandard extension of rabs
- inverse is nonstandard extension of inverse
- ---------------------------------------------------*)
+text{*Examples: hrabs is nonstandard extension of rabs
+ inverse is nonstandard extension of inverse*}
(* can be proved easily using theorem "starfun" and *)
(* properties of ultrafilter as for inverse below we *)
@@ -393,10 +375,8 @@
apply (auto intro: FreeUltrafilterNat_subset dest!: FreeUltrafilterNat_Compl_mem simp add: starfun hypreal_inverse hypreal_zero_def)
done
-(*-------------------------------------------------------------
- General lemma/theorem needed for proofs in elementary
- topology of the reals
- ------------------------------------------------------------*)
+text{*General lemma/theorem needed for proofs in elementary
+ topology of the reals*}
lemma starfun_mem_starset:
"( *f* f) x : *s* A ==> x : *s* {x. f x \<in> A}"
apply (simp add: starset_def)
@@ -407,22 +387,18 @@
apply (auto, ultra)
done
-(*------------------------------------------------------------
- Alternative definition for hrabs with rabs function
+text{*Alternative definition for hrabs with rabs function
applied entrywise to equivalence class representative.
- This is easily proved using starfun and ns extension thm
- ------------------------------------------------------------*)
+ This is easily proved using starfun and ns extension thm*}
lemma hypreal_hrabs: "abs (Abs_hypreal (hyprel `` {X})) =
Abs_hypreal(hyprel `` {%n. abs (X n)})"
apply (simp (no_asm) add: starfun_rabs_hrabs [symmetric] starfun)
done
-(*----------------------------------------------------------------
- nonstandard extension of set through nonstandard extension
+text{*nonstandard extension of set through nonstandard extension
of rabs function i.e hrabs. A more general result should be
where we replace rabs by some arbitrary function f and hrabs
- by its NS extenson ( *f* f). See second NS set extension below.
- ----------------------------------------------------------------*)
+ by its NS extenson. See second NS set extension below.*}
lemma STAR_rabs_add_minus:
"*s* {x. abs (x + - y) < r} =
{x. abs(x + -hypreal_of_real y) < hypreal_of_real r}"
@@ -439,11 +415,9 @@
apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less starfun, ultra)
done
-(*-------------------------------------------------------------------
- Another characterization of Infinitesimal and one of @= relation.
+text{*Another characterization of Infinitesimal and one of @= relation.
In this theory since hypreal_hrabs proved here. (To Check:) Maybe
- move both if possible?
- -------------------------------------------------------------------*)
+ move both if possible?*}
lemma Infinitesimal_FreeUltrafilterNat_iff2:
"(x \<in> Infinitesimal) =
(\<exists>X \<in> Rep_hypreal(x).
--- a/src/HOL/Induct/QuoDataType.thy Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Induct/QuoDataType.thy Wed Sep 01 15:04:01 2004 +0200
@@ -166,7 +166,7 @@
text{*All equivalence classes belong to set of representatives*}
-lemma msgrel_in_integ [simp]: "msgrel``{U} \<in> Msg"
+lemma [simp]: "msgrel``{U} \<in> Msg"
by (auto simp add: Msg_def quotient_def intro: msgrel_refl)
lemma inj_on_Abs_Msg: "inj_on Abs_Msg Msg"
@@ -185,7 +185,7 @@
lemma MPair: "MPair (Abs_Msg(msgrel``{U})) (Abs_Msg(msgrel``{V})) =
Abs_Msg (msgrel``{MPAIR U V})"
proof -
- have "congruent2 msgrel msgrel (\<lambda>U V. msgrel `` {MPAIR U V})"
+ have "(\<lambda>U V. msgrel `` {MPAIR U V}) respects2 msgrel"
by (simp add: congruent2_def msgrel.MPAIR)
thus ?thesis
by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel])
@@ -193,7 +193,7 @@
lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})"
proof -
- have "congruent msgrel (\<lambda>U. msgrel `` {CRYPT K U})"
+ have "(\<lambda>U. msgrel `` {CRYPT K U}) respects msgrel"
by (simp add: congruent_def msgrel.CRYPT)
thus ?thesis
by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel])
@@ -202,7 +202,7 @@
lemma Decrypt:
"Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})"
proof -
- have "congruent msgrel (\<lambda>U. msgrel `` {DECRYPT K U})"
+ have "(\<lambda>U. msgrel `` {DECRYPT K U}) respects msgrel"
by (simp add: congruent_def msgrel.DECRYPT)
thus ?thesis
by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])
@@ -230,7 +230,7 @@
nonces :: "msg \<Rightarrow> nat set"
"nonces X == \<Union>U \<in> Rep_Msg X. freenonces U"
-lemma nonces_congruent: "congruent msgrel freenonces"
+lemma nonces_congruent: "freenonces respects msgrel"
by (simp add: congruent_def msgrel_imp_eq_freenonces)
@@ -265,7 +265,7 @@
left :: "msg \<Rightarrow> msg"
"left X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
-lemma left_congruent: "congruent msgrel (\<lambda>U. msgrel `` {freeleft U})"
+lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
by (simp add: congruent_def msgrel_imp_eqv_freeleft)
text{*Now prove the four equations for @{term left}*}
@@ -299,7 +299,7 @@
right :: "msg \<Rightarrow> msg"
"right X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
-lemma right_congruent: "congruent msgrel (\<lambda>U. msgrel `` {freeright U})"
+lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
by (simp add: congruent_def msgrel_imp_eqv_freeright)
text{*Now prove the four equations for @{term right}*}
@@ -433,7 +433,7 @@
discrim :: "msg \<Rightarrow> int"
"discrim X == contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
-lemma discrim_congruent: "congruent msgrel (\<lambda>U. {freediscrim U})"
+lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
by (simp add: congruent_def msgrel_imp_eq_freediscrim)
text{*Now prove the four equations for @{term discrim}*}
--- a/src/HOL/Integ/Equiv.thy Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Integ/Equiv.thy Wed Sep 01 15:04:01 2004 +0200
@@ -151,12 +151,19 @@
fixes r and f
assumes congruent: "(y,z) \<in> r ==> f y = f z"
+syntax
+ RESPECTS ::"['a => 'b, ('a * 'a) set] => bool" (infixr "respects" 80)
+
+translations
+ "f respects r" == "congruent r f"
+
+
lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"
-- {* lemma required to prove @{text UN_equiv_class} *}
by auto
lemma UN_equiv_class:
- "equiv A r ==> congruent r f ==> a \<in> A
+ "equiv A r ==> f respects r ==> a \<in> A
==> (\<Union>x \<in> r``{a}. f x) = f a"
-- {* Conversion rule *}
apply (rule equiv_class_self [THEN UN_constant_eq], assumption+)
@@ -165,7 +172,7 @@
done
lemma UN_equiv_class_type:
- "equiv A r ==> congruent r f ==> X \<in> A//r ==>
+ "equiv A r ==> f respects r ==> X \<in> A//r ==>
(!!x. x \<in> A ==> f x \<in> B) ==> (\<Union>x \<in> X. f x) \<in> B"
apply (unfold quotient_def)
apply clarify
@@ -180,7 +187,7 @@
*}
lemma UN_equiv_class_inject:
- "equiv A r ==> congruent r f ==>
+ "equiv A r ==> f respects r ==>
(\<Union>x \<in> X. f x) = (\<Union>y \<in> Y. f y) ==> X \<in> A//r ==> Y \<in> A//r
==> (!!x y. x \<in> A ==> y \<in> A ==> f x = f y ==> (x, y) \<in> r)
==> X = Y"
@@ -203,6 +210,13 @@
assumes congruent2:
"(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2"
+text{*Abbreviation for the common case where the relations are identical*}
+syntax
+ RESPECTS2 ::"['a => 'b, ('a * 'a) set] => bool" (infixr "respects2 " 80)
+
+translations
+ "f respects2 r" => "congruent2 r r f"
+
lemma congruent2_implies_congruent:
"equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"
by (unfold congruent_def congruent2_def equiv_def refl_def) blast
@@ -258,7 +272,7 @@
assumes equivA: "equiv A r"
and commute: "!!y z. y \<in> A ==> z \<in> A ==> f y z = f z y"
and congt: "!!y z w. w \<in> A ==> (y,z) \<in> r ==> f w y = f w z"
- shows "congruent2 r r f"
+ shows "f respects2 r"
apply (rule congruent2I [OF equivA equivA])
apply (rule commute [THEN trans])
apply (rule_tac [3] commute [THEN trans, symmetric])
@@ -270,7 +284,7 @@
subsection {* Cardinality results *}
-text {* (suggested by Florian Kammüller) *}
+text {*Suggested by Florian Kammüller*}
lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
-- {* recall @{thm equiv_type} *}
--- a/src/HOL/Integ/IntDef.thy Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy Wed Sep 01 15:04:01 2004 +0200
@@ -110,7 +110,7 @@
lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
proof -
- have "congruent intrel (\<lambda>(x,y). intrel``{(y,x)})"
+ have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
by (simp add: congruent_def)
thus ?thesis
by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
@@ -129,8 +129,8 @@
"Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) =
Abs_Integ (intrel``{(x+u, y+v)})"
proof -
- have "congruent2 intrel intrel
- (\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z)"
+ have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z)
+ respects2 intrel"
by (simp add: congruent2_def)
thus ?thesis
by (simp add: add_int_def UN_UN_split_split_eq
@@ -183,9 +183,8 @@
text{*Congruence property for multiplication*}
lemma mult_congruent2:
- "congruent2 intrel intrel
- (%p1 p2. (%(x,y). (%(u,v).
- intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)"
+ "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)
+ respects2 intrel"
apply (rule equiv_intrel [THEN congruent2_commuteI])
apply (force simp add: mult_ac, clarify)
apply (simp add: congruent_def mult_ac)
@@ -393,7 +392,7 @@
lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
proof -
- have "congruent intrel (\<lambda>(x,y). {x-y})"
+ have "(\<lambda>(x,y). {x-y}) respects intrel"
by (simp add: congruent_def, arith)
thus ?thesis
by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
@@ -695,7 +694,7 @@
lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
proof -
- have "congruent intrel (\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) })"
+ have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
by (simp add: congruent_def compare_rls of_nat_add [symmetric]
del: of_nat_add)
thus ?thesis
--- a/src/HOL/Real/RealDef.thy Wed Sep 01 15:03:41 2004 +0200
+++ b/src/HOL/Real/RealDef.thy Wed Sep 01 15:04:01 2004 +0200
@@ -154,8 +154,8 @@
"Abs_Real (realrel``{(x,y)}) + Abs_Real (realrel``{(u,v)}) =
Abs_Real (realrel``{(x+u, y+v)})"
proof -
- have "congruent2 realrel realrel
- (\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)"
+ have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)
+ respects2 realrel"
by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma)
thus ?thesis
by (simp add: real_add_def UN_UN_split_split_eq
@@ -181,7 +181,7 @@
lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})"
proof -
- have "congruent realrel (\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})})"
+ have "(\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel"
by (simp add: congruent_def preal_add_commute)
thus ?thesis
by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel])
@@ -203,9 +203,10 @@
done
lemma real_mult_congruent2:
- "congruent2 realrel realrel (%p1 p2.
+ "(%p1 p2.
(%(x1,y1). (%(x2,y2).
- { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1)"
+ { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1)
+ respects2 realrel"
apply (rule congruent2_commuteI [OF equiv_realrel], clarify)
apply (simp add: preal_mult_commute preal_add_commute)
apply (auto simp add: real_mult_congruent2_lemma)