# HG changeset patch # User paulson # Date 1082711047 -7200 # Node ID b1293d0f8d5fedb70f1adc27034e9d72d6c6b5e9 # Parent c7cc01735801695385d1cc1d928248145a5b6e2f congruent2 now allows different equiv relations diff -r c7cc01735801 -r b1293d0f8d5f src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Thu Apr 22 13:26:47 2004 +0200 +++ b/src/HOL/Complex/NSComplex.thy Fri Apr 23 11:04:07 2004 +0200 @@ -243,7 +243,7 @@ subsection{*Addition for Nonstandard Complex Numbers*} lemma hcomplex_add_congruent2: - "congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})" + "congruent2 hcomplexrel hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})" by (auto simp add: congruent2_def iff: hcomplexrel_iff, ultra) lemma hcomplex_add: @@ -1562,7 +1562,6 @@ val hcomplex_hIm_one = thm"hcomplex_hIm_one"; val inj_hcomplex_of_complex = thm"inj_hcomplex_of_complex"; val hcomplex_of_complex_i = thm"hcomplex_of_complex_i"; -val hcomplex_add_congruent2 = thm"hcomplex_add_congruent2"; val hcomplex_add = thm"hcomplex_add"; val hcomplex_add_commute = thm"hcomplex_add_commute"; val hcomplex_add_assoc = thm"hcomplex_add_assoc"; diff -r c7cc01735801 -r b1293d0f8d5f src/HOL/Hyperreal/HyperDef.thy --- a/src/HOL/Hyperreal/HyperDef.thy Thu Apr 22 13:26:47 2004 +0200 +++ b/src/HOL/Hyperreal/HyperDef.thy Fri Apr 23 11:04:07 2004 +0200 @@ -317,16 +317,15 @@ subsection{*Hyperreal Addition*} lemma hypreal_add_congruent2: - "congruent2 hyprel (%X Y. hyprel``{%n. X n + Y n})" + "congruent2 hyprel hyprel (%X Y. hyprel``{%n. X n + Y n})" apply (simp add: congruent2_def, auto, ultra) done lemma hypreal_add: "Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) = Abs_hypreal(hyprel``{%n. X n + Y n})" -apply (simp add: hypreal_add_def) -apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_add_congruent2]) -done +by (simp add: hypreal_add_def + UN_equiv_class2 [OF equiv_hyprel equiv_hyprel hypreal_add_congruent2]) lemma hypreal_add_commute: "(z::hypreal) + w = w + z" apply (cases z, cases w) @@ -383,16 +382,14 @@ subsection{*Hyperreal Multiplication*} lemma hypreal_mult_congruent2: - "congruent2 hyprel (%X Y. hyprel``{%n. X n * Y n})" -apply (simp add: congruent2_def, auto, ultra) -done + "congruent2 hyprel hyprel (%X Y. hyprel``{%n. X n * Y n})" +by (simp add: congruent2_def, auto, ultra) lemma hypreal_mult: "Abs_hypreal(hyprel``{%n. X n}) * Abs_hypreal(hyprel``{%n. Y n}) = Abs_hypreal(hyprel``{%n. X n * Y n})" -apply (simp add: hypreal_mult_def) -apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_mult_congruent2]) -done +by (simp add: hypreal_mult_def + UN_equiv_class2 [OF equiv_hyprel equiv_hyprel hypreal_mult_congruent2]) lemma hypreal_mult_commute: "(z::hypreal) * w = w * z" apply (cases z, cases w) @@ -765,10 +762,6 @@ val FreeUltrafilterNat_all = thm "FreeUltrafilterNat_all"; val FreeUltrafilterNat_Un = thm "FreeUltrafilterNat_Un"; val hyprel_iff = thm "hyprel_iff"; -val hyprel_refl = thm "hyprel_refl"; -val hyprel_sym = thm "hyprel_sym"; -val hyprel_trans = thm "hyprel_trans"; -val equiv_hyprel = thm "equiv_hyprel"; val hyprel_in_hypreal = thm "hyprel_in_hypreal"; val Abs_hypreal_inverse = thm "Abs_hypreal_inverse"; val inj_on_Abs_hypreal = thm "inj_on_Abs_hypreal"; @@ -780,7 +773,6 @@ val eq_Abs_hypreal = thm "eq_Abs_hypreal"; val hypreal_minus_congruent = thm "hypreal_minus_congruent"; val hypreal_minus = thm "hypreal_minus"; -val hypreal_add_congruent2 = thm "hypreal_add_congruent2"; val hypreal_add = thm "hypreal_add"; val hypreal_diff = thm "hypreal_diff"; val hypreal_add_commute = thm "hypreal_add_commute"; @@ -789,7 +781,6 @@ val hypreal_add_zero_right = thm "hypreal_add_zero_right"; val hypreal_add_minus = thm "hypreal_add_minus"; val hypreal_add_minus_left = thm "hypreal_add_minus_left"; -val hypreal_mult_congruent2 = thm "hypreal_mult_congruent2"; val hypreal_mult = thm "hypreal_mult"; val hypreal_mult_commute = thm "hypreal_mult_commute"; val hypreal_mult_assoc = thm "hypreal_mult_assoc"; diff -r c7cc01735801 -r b1293d0f8d5f src/HOL/Hyperreal/HyperNat.thy --- a/src/HOL/Hyperreal/HyperNat.thy Thu Apr 22 13:26:47 2004 +0200 +++ b/src/HOL/Hyperreal/HyperNat.thy Fri Apr 23 11:04:07 2004 +0200 @@ -139,14 +139,14 @@ subsection{*Hypernat Addition*} lemma hypnat_add_congruent2: - "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})" -apply (simp add: congruent2_def, auto, ultra) -done + "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})" +by (simp add: congruent2_def, auto, ultra) lemma hypnat_add: "Abs_hypnat(hypnatrel``{%n. X n}) + Abs_hypnat(hypnatrel``{%n. Y n}) = Abs_hypnat(hypnatrel``{%n. X n + Y n})" -by (simp add: hypnat_add_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_add_congruent2]) +by (simp add: hypnat_add_def + UN_equiv_class2 [OF equiv_hypnatrel equiv_hypnatrel hypnat_add_congruent2]) lemma hypnat_add_commute: "(z::hypnat) + w = w + z" apply (cases z, cases w) @@ -173,14 +173,14 @@ lemma hypnat_minus_congruent2: - "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})" -apply (simp add: congruent2_def, auto, ultra) -done + "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})" +by (simp add: congruent2_def, auto, ultra) lemma hypnat_minus: "Abs_hypnat(hypnatrel``{%n. X n}) - Abs_hypnat(hypnatrel``{%n. Y n}) = Abs_hypnat(hypnatrel``{%n. X n - Y n})" -by (simp add: hypnat_minus_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_minus_congruent2]) +by (simp add: hypnat_minus_def + UN_equiv_class2 [OF equiv_hypnatrel equiv_hypnatrel hypnat_minus_congruent2]) lemma hypnat_minus_zero: "z - z = (0::hypnat)" apply (cases z) @@ -241,18 +241,17 @@ subsection{*Hyperreal Multiplication*} lemma hypnat_mult_congruent2: - "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})" + "congruent2 hypnatrel hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})" by (simp add: congruent2_def, auto, ultra) lemma hypnat_mult: "Abs_hypnat(hypnatrel``{%n. X n}) * Abs_hypnat(hypnatrel``{%n. Y n}) = Abs_hypnat(hypnatrel``{%n. X n * Y n})" -by (simp add: hypnat_mult_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_mult_congruent2]) +by (simp add: hypnat_mult_def + UN_equiv_class2 [OF equiv_hypnatrel equiv_hypnatrel hypnat_mult_congruent2]) lemma hypnat_mult_commute: "(z::hypnat) * w = w * z" -apply (cases z, cases w) -apply (simp add: hypnat_mult mult_ac) -done +by (cases z, cases w, simp add: hypnat_mult mult_ac) lemma hypnat_mult_assoc: "((z1::hypnat) * z2) * z3 = z1 * (z2 * z3)" apply (cases z1, cases z2, cases z3) @@ -797,11 +796,6 @@ val hypnat_omega_def = thm"hypnat_omega_def"; val hypnatrel_iff = thm "hypnatrel_iff"; -val hypnatrel_refl = thm "hypnatrel_refl"; -val hypnatrel_sym = thm "hypnatrel_sym"; -val hypnatrel_trans = thm "hypnatrel_trans"; -val equiv_hypnatrel = thm "equiv_hypnatrel"; -val equiv_hypnatrel_iff = thms "equiv_hypnatrel_iff"; val hypnatrel_in_hypnat = thm "hypnatrel_in_hypnat"; val inj_on_Abs_hypnat = thm "inj_on_Abs_hypnat"; val inj_Rep_hypnat = thm "inj_Rep_hypnat"; @@ -809,7 +803,6 @@ val hypnat_empty_not_mem = thm "hypnat_empty_not_mem"; val Rep_hypnat_nonempty = thm "Rep_hypnat_nonempty"; val eq_Abs_hypnat = thm "eq_Abs_hypnat"; -val hypnat_add_congruent2 = thm "hypnat_add_congruent2"; val hypnat_add = thm "hypnat_add"; val hypnat_add_commute = thm "hypnat_add_commute"; val hypnat_add_assoc = thm "hypnat_add_assoc"; diff -r c7cc01735801 -r b1293d0f8d5f src/HOL/Induct/QuoDataType.thy --- a/src/HOL/Induct/QuoDataType.thy Thu Apr 22 13:26:47 2004 +0200 +++ b/src/HOL/Induct/QuoDataType.thy Fri Apr 23 11:04:07 2004 +0200 @@ -85,36 +85,36 @@ text{*A function to return the left part of the top pair in a message. It will be lifted to the initial algrebra, to serve as an example of that process.*} -consts free_left :: "freemsg \ freemsg" +consts freeleft :: "freemsg \ freemsg" primrec - "free_left (NONCE N) = NONCE N" - "free_left (MPAIR X Y) = X" - "free_left (CRYPT K X) = free_left X" - "free_left (DECRYPT K X) = free_left X" + "freeleft (NONCE N) = NONCE N" + "freeleft (MPAIR X Y) = X" + "freeleft (CRYPT K X) = freeleft X" + "freeleft (DECRYPT K X) = freeleft X" text{*This theorem lets us prove that the left function respects the equivalence relation. It also helps us prove that MPair (the abstract constructor) is injective*} -theorem msgrel_imp_eqv_free_left: - "U \ V \ free_left U \ free_left V" +theorem msgrel_imp_eqv_freeleft: + "U \ V \ freeleft U \ freeleft V" by (erule msgrel.induct, auto intro: msgrel.intros) subsubsection{*The Right Projection*} text{*A function to return the right part of the top pair in a message.*} -consts free_right :: "freemsg \ freemsg" +consts freeright :: "freemsg \ freemsg" primrec - "free_right (NONCE N) = NONCE N" - "free_right (MPAIR X Y) = Y" - "free_right (CRYPT K X) = free_right X" - "free_right (DECRYPT K X) = free_right X" + "freeright (NONCE N) = NONCE N" + "freeright (MPAIR X Y) = Y" + "freeright (CRYPT K X) = freeright X" + "freeright (DECRYPT K X) = freeright X" text{*This theorem lets us prove that the right function respects the equivalence relation. It also helps us prove that MPair (the abstract constructor) is injective*} -theorem msgrel_imp_eqv_free_right: - "U \ V \ free_right U \ free_right V" +theorem msgrel_imp_eqv_freeright: + "U \ V \ freeright U \ freeright V" by (erule msgrel.induct, auto intro: msgrel.intros) @@ -147,15 +147,15 @@ MPair :: "[msg,msg] \ msg" "MPair X Y == - Abs_Msg (\U \ Rep_Msg X. \V \ Rep_Msg Y. msgrel``{MPAIR U V})" + Abs_Msg (\\<^bsub>U \ Rep_Msg X\<^esub> \\<^bsub>V \ Rep_Msg Y\<^esub> msgrel``{MPAIR U V})" Crypt :: "[nat,msg] \ msg" "Crypt K X == - Abs_Msg (\U \ Rep_Msg X. msgrel``{CRYPT K U})" + Abs_Msg (\\<^bsub>U \ Rep_Msg X\<^esub> msgrel``{CRYPT K U})" Decrypt :: "[nat,msg] \ msg" "Decrypt K X == - Abs_Msg (\U \ Rep_Msg X. msgrel``{DECRYPT K U})" + Abs_Msg (\\<^bsub>U \ Rep_Msg X\<^esub> msgrel``{DECRYPT K U})" text{*Reduces equality of equivalence classes to the @{term msgrel} relation: @@ -185,10 +185,10 @@ lemma MPair: "MPair (Abs_Msg(msgrel``{U})) (Abs_Msg(msgrel``{V})) = Abs_Msg (msgrel``{MPAIR U V})" proof - - have "congruent2 msgrel (\U V. msgrel `` {MPAIR U V})" + have "congruent2 msgrel msgrel (\U V. msgrel `` {MPAIR U V})" by (simp add: congruent2_def msgrel.MPAIR) thus ?thesis - by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel]) + by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel]) qed lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})" @@ -228,7 +228,7 @@ constdefs nonces :: "msg \ nat set" - "nonces X == \U \ Rep_Msg X. freenonces U" + "nonces X == \\<^bsub>U \ Rep_Msg X\<^esub> freenonces U" lemma nonces_congruent: "congruent msgrel freenonces" by (simp add: congruent_def msgrel_imp_eq_freenonces) @@ -263,10 +263,10 @@ constdefs left :: "msg \ msg" - "left X == Abs_Msg (\U \ Rep_Msg X. msgrel``{free_left U})" + "left X == Abs_Msg (\\<^bsub>U \ Rep_Msg X\<^esub> msgrel``{freeleft U})" -lemma left_congruent: "congruent msgrel (\U. msgrel `` {free_left U})" -by (simp add: congruent_def msgrel_imp_eqv_free_left) +lemma left_congruent: "congruent msgrel (\U. msgrel `` {freeleft U})" +by (simp add: congruent_def msgrel_imp_eqv_freeleft) text{*Now prove the four equations for @{term left}*} @@ -297,10 +297,10 @@ constdefs right :: "msg \ msg" - "right X == Abs_Msg (\U \ Rep_Msg X. msgrel``{free_right U})" + "right X == Abs_Msg (\\<^bsub>U \ Rep_Msg X\<^esub> msgrel``{freeright U})" -lemma right_congruent: "congruent msgrel (\U. msgrel `` {free_right U})" -by (simp add: congruent_def msgrel_imp_eqv_free_right) +lemma right_congruent: "congruent msgrel (\U. msgrel `` {freeright U})" +by (simp add: congruent_def msgrel_imp_eqv_freeright) text{*Now prove the four equations for @{term right}*} @@ -337,7 +337,7 @@ by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq) lemma MPAIR_imp_eqv_left: "MPAIR X Y \ MPAIR X' Y' \ X \ X'" -by (drule msgrel_imp_eqv_free_left, simp) +by (drule msgrel_imp_eqv_freeleft, simp) lemma MPair_imp_eq_left: assumes eq: "MPair X Y = MPair X' Y'" shows "X = X'" @@ -348,7 +348,7 @@ qed lemma MPAIR_imp_eqv_right: "MPAIR X Y \ MPAIR X' Y' \ Y \ Y'" -by (drule msgrel_imp_eqv_free_right, simp) +by (drule msgrel_imp_eqv_freeright, simp) lemma MPair_imp_eq_right: "MPair X Y = MPair X' Y' \ Y = Y'" apply (cases X, cases X', cases Y, cases Y') diff -r c7cc01735801 -r b1293d0f8d5f src/HOL/Integ/Equiv.thy --- a/src/HOL/Integ/Equiv.thy Thu Apr 22 13:26:47 2004 +0200 +++ b/src/HOL/Integ/Equiv.thy Fri Apr 23 11:04:07 2004 +0200 @@ -8,7 +8,7 @@ theory Equiv = Relation + Finite_Set: -subsection {* Equiv relations *} +subsection {* Equivalence relations *} locale equiv = fixes A and r @@ -37,9 +37,7 @@ apply (rules intro: sym_trans_comp_subset refl_comp_subset)+ done -text {* - Second half. -*} +text {* Second half. *} lemma comp_equivI: "r\ O r = r ==> Domain r = A ==> equiv A r" @@ -136,9 +134,10 @@ subsection {* Defining unary operations upon equivalence classes *} +text{*A congruence-preserving function*} locale congruent = fixes r and f - assumes congruent: "(y, z) \ r ==> f y = f z" + assumes congruent: "(y,z) \ r ==> f y = f z" lemma UN_constant_eq: "a \ A ==> \y \ A. f y = c ==> (\y \ A. f(y))=c" -- {* lemma required to prove @{text UN_equiv_class} *} @@ -186,18 +185,19 @@ subsection {* Defining binary operations upon equivalence classes *} +text{*A congruence-preserving function of two arguments*} locale congruent2 = - fixes r and f + fixes r1 and r2 and f assumes congruent2: - "(y1, z1) \ r ==> (y2, z2) \ r ==> f y1 y2 = f z1 z2" + "(y1,z1) \ r1 ==> (y2,z2) \ r2 ==> f y1 y2 = f z1 z2" lemma congruent2_implies_congruent: - "equiv A r ==> congruent2 r f ==> a \ A ==> congruent r (f a)" + "equiv A r1 ==> congruent2 r1 r2 f ==> a \ A ==> congruent r2 (f a)" by (unfold congruent_def congruent2_def equiv_def refl_def) blast lemma congruent2_implies_congruent_UN: - "equiv A r ==> congruent2 r f ==> a \ A ==> - congruent r (\x1. \x2 \ r``{a}. f x1 x2)" + "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \ A2 ==> + congruent r1 (\x1. \x2 \ r2``{a}. f x1 x2)" apply (unfold congruent_def) apply clarify apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+) @@ -207,14 +207,15 @@ done lemma UN_equiv_class2: - "equiv A r ==> congruent2 r f ==> a1 \ A ==> a2 \ A - ==> (\x1 \ r``{a1}. \x2 \ r``{a2}. f x1 x2) = f a1 a2" + "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a1 \ A1 ==> a2 \ A2 + ==> (\x1 \ r1``{a1}. \x2 \ r2``{a2}. f x1 x2) = f a1 a2" by (simp add: UN_equiv_class congruent2_implies_congruent congruent2_implies_congruent_UN) lemma UN_equiv_class_type2: - "equiv A r ==> congruent2 r f ==> X1 \ A//r ==> X2 \ A//r - ==> (!!x1 x2. x1 \ A ==> x2 \ A ==> f x1 x2 \ B) + "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f + ==> X1 \ A1//r1 ==> X2 \ A2//r2 + ==> (!!x1 x2. x1 \ A1 ==> x2 \ A2 ==> f x1 x2 \ B) ==> (\x1 \ X1. \x2 \ X2. f x1 x2) \ B" apply (unfold quotient_def) apply clarify @@ -230,10 +231,10 @@ by auto lemma congruent2I: - "equiv A r - ==> (!!y z w. w \ A ==> (y, z) \ r ==> f y w = f z w) - ==> (!!y z w. w \ A ==> (y, z) \ r ==> f w y = f w z) - ==> congruent2 r f" + "equiv A1 r1 ==> equiv A2 r2 + ==> (!!y z w. w \ A2 ==> (y,z) \ r1 ==> f y w = f z w) + ==> (!!y z w. w \ A1 ==> (y,z) \ r2 ==> f w y = f w z) + ==> congruent2 r1 r2 f" -- {* Suggested by John Harrison -- the two subproofs may be *} -- {* \emph{much} simpler than the direct proof. *} apply (unfold congruent2_def equiv_def refl_def) @@ -244,9 +245,9 @@ lemma congruent2_commuteI: assumes equivA: "equiv A r" and commute: "!!y z. y \ A ==> z \ A ==> f y z = f z y" - and congt: "!!y z w. w \ A ==> (y, z) \ r ==> f w y = f w z" - shows "congruent2 r f" - apply (rule equivA [THEN congruent2I]) + and congt: "!!y z w. w \ A ==> (y,z) \ r ==> f w y = f w z" + shows "congruent2 r r f" + apply (rule congruent2I [OF equivA equivA]) apply (rule commute [THEN trans]) apply (rule_tac [3] commute [THEN trans, symmetric]) apply (rule_tac [5] sym) diff -r c7cc01735801 -r b1293d0f8d5f src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Thu Apr 22 13:26:47 2004 +0200 +++ b/src/HOL/Integ/IntDef.thy Fri Apr 23 11:04:07 2004 +0200 @@ -133,12 +133,12 @@ "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) = Abs_Integ (intrel``{(x+u, y+v)})" proof - - have "congruent2 intrel + have "congruent2 intrel intrel (\z w. (\(x,y). (\(u,v). intrel `` {(x+u, y+v)}) w) z)" by (simp add: congruent2_def) thus ?thesis by (simp add: add_int_def UN_UN_split_split_eq - UN_equiv_class2 [OF equiv_intrel]) + UN_equiv_class2 [OF equiv_intrel equiv_intrel]) qed lemma zminus_zadd_distrib: "- (z + w) = (- z) + (- w::int)" @@ -187,7 +187,7 @@ text{*Congruence property for multiplication*} lemma mult_congruent2: - "congruent2 intrel + "congruent2 intrel intrel (%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)" apply (rule equiv_intrel [THEN congruent2_commuteI]) @@ -204,7 +204,7 @@ "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) = Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})" by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2 - equiv_intrel [THEN UN_equiv_class2]) + UN_equiv_class2 [OF equiv_intrel equiv_intrel]) lemma zmult_zminus: "(- z) * w = - (z * (w::int))" by (cases z, cases w, simp add: minus mult add_ac) diff -r c7cc01735801 -r b1293d0f8d5f src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Thu Apr 22 13:26:47 2004 +0200 +++ b/src/HOL/Real/RealDef.thy Fri Apr 23 11:04:07 2004 +0200 @@ -158,12 +158,12 @@ "Abs_Real (realrel``{(x,y)}) + Abs_Real (realrel``{(u,v)}) = Abs_Real (realrel``{(x+u, y+v)})" proof - - have "congruent2 realrel + have "congruent2 realrel realrel (\z w. (\(x,y). (\(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)" by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma) thus ?thesis by (simp add: real_add_def UN_UN_split_split_eq - UN_equiv_class2 [OF equiv_realrel]) + UN_equiv_class2 [OF equiv_realrel equiv_realrel]) qed lemma real_add_commute: "(z::real) + w = w + z" @@ -207,10 +207,10 @@ done lemma real_mult_congruent2: - "congruent2 realrel (%p1 p2. + "congruent2 realrel realrel (%p1 p2. (%(x1,y1). (%(x2,y2). { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1)" -apply (rule equiv_realrel [THEN congruent2_commuteI], clarify) +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) done @@ -219,7 +219,7 @@ "Abs_Real((realrel``{(x1,y1)})) * Abs_Real((realrel``{(x2,y2)})) = Abs_Real(realrel `` {(x1*x2+y1*y2,x1*y2+y1*x2)})" by (simp add: real_mult_def UN_UN_split_split_eq - UN_equiv_class2 [OF equiv_realrel real_mult_congruent2]) + UN_equiv_class2 [OF equiv_realrel equiv_realrel real_mult_congruent2]) lemma real_mult_commute: "(z::real) * w = w * z" by (cases z, cases w, simp add: real_mult preal_add_ac preal_mult_ac)