--- 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";
--- 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";
--- 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";
--- 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 \<Rightarrow> freemsg"
+consts freeleft :: "freemsg \<Rightarrow> 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 \<sim> V \<Longrightarrow> free_left U \<sim> free_left V"
+theorem msgrel_imp_eqv_freeleft:
+ "U \<sim> V \<Longrightarrow> freeleft U \<sim> 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 \<Rightarrow> freemsg"
+consts freeright :: "freemsg \<Rightarrow> 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 \<sim> V \<Longrightarrow> free_right U \<sim> free_right V"
+theorem msgrel_imp_eqv_freeright:
+ "U \<sim> V \<Longrightarrow> freeright U \<sim> freeright V"
by (erule msgrel.induct, auto intro: msgrel.intros)
@@ -147,15 +147,15 @@
MPair :: "[msg,msg] \<Rightarrow> msg"
"MPair X Y ==
- Abs_Msg (\<Union>U \<in> Rep_Msg X. \<Union>V \<in> Rep_Msg Y. msgrel``{MPAIR U V})"
+ Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> \<Union>\<^bsub>V \<in> Rep_Msg Y\<^esub> msgrel``{MPAIR U V})"
Crypt :: "[nat,msg] \<Rightarrow> msg"
"Crypt K X ==
- Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{CRYPT K U})"
+ Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> msgrel``{CRYPT K U})"
Decrypt :: "[nat,msg] \<Rightarrow> msg"
"Decrypt K X ==
- Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{DECRYPT K U})"
+ Abs_Msg (\<Union>\<^bsub>U \<in> 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 (\<lambda>U V. msgrel `` {MPAIR U V})"
+ have "congruent2 msgrel msgrel (\<lambda>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 \<Rightarrow> nat set"
- "nonces X == \<Union>U \<in> Rep_Msg X. freenonces U"
+ "nonces X == \<Union>\<^bsub>U \<in> 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 \<Rightarrow> msg"
- "left X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{free_left U})"
+ "left X == Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> msgrel``{freeleft U})"
-lemma left_congruent: "congruent msgrel (\<lambda>U. msgrel `` {free_left U})"
-by (simp add: congruent_def msgrel_imp_eqv_free_left)
+lemma left_congruent: "congruent msgrel (\<lambda>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 \<Rightarrow> msg"
- "right X == Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{free_right U})"
+ "right X == Abs_Msg (\<Union>\<^bsub>U \<in> Rep_Msg X\<^esub> msgrel``{freeright U})"
-lemma right_congruent: "congruent msgrel (\<lambda>U. msgrel `` {free_right U})"
-by (simp add: congruent_def msgrel_imp_eqv_free_right)
+lemma right_congruent: "congruent msgrel (\<lambda>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 \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> 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 \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> 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' \<Longrightarrow> Y = Y'"
apply (cases X, cases X', cases Y, cases Y')
--- 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\<inverse> 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) \<in> r ==> f y = f z"
+ assumes congruent: "(y,z) \<in> r ==> f y = f z"
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} *}
@@ -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) \<in> r ==> (y2, z2) \<in> r ==> f y1 y2 = f z1 z2"
+ "(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2"
lemma congruent2_implies_congruent:
- "equiv A r ==> congruent2 r f ==> a \<in> A ==> congruent r (f a)"
+ "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
lemma congruent2_implies_congruent_UN:
- "equiv A r ==> congruent2 r f ==> a \<in> A ==>
- congruent r (\<lambda>x1. \<Union>x2 \<in> r``{a}. f x1 x2)"
+ "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \<in> A2 ==>
+ congruent r1 (\<lambda>x1. \<Union>x2 \<in> 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 \<in> A ==> a2 \<in> A
- ==> (\<Union>x1 \<in> r``{a1}. \<Union>x2 \<in> r``{a2}. f x1 x2) = f a1 a2"
+ "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a1 \<in> A1 ==> a2 \<in> A2
+ ==> (\<Union>x1 \<in> r1``{a1}. \<Union>x2 \<in> 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 \<in> A//r ==> X2 \<in> A//r
- ==> (!!x1 x2. x1 \<in> A ==> x2 \<in> A ==> f x1 x2 \<in> B)
+ "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f
+ ==> X1 \<in> A1//r1 ==> X2 \<in> A2//r2
+ ==> (!!x1 x2. x1 \<in> A1 ==> x2 \<in> A2 ==> f x1 x2 \<in> B)
==> (\<Union>x1 \<in> X1. \<Union>x2 \<in> X2. f x1 x2) \<in> B"
apply (unfold quotient_def)
apply clarify
@@ -230,10 +231,10 @@
by auto
lemma congruent2I:
- "equiv A r
- ==> (!!y z w. w \<in> A ==> (y, z) \<in> r ==> f y w = f z w)
- ==> (!!y z w. w \<in> A ==> (y, z) \<in> r ==> f w y = f w z)
- ==> congruent2 r f"
+ "equiv A1 r1 ==> equiv A2 r2
+ ==> (!!y z w. w \<in> A2 ==> (y,z) \<in> r1 ==> f y w = f z w)
+ ==> (!!y z w. w \<in> A1 ==> (y,z) \<in> 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 \<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 f"
- apply (rule equivA [THEN congruent2I])
+ and congt: "!!y z w. w \<in> A ==> (y,z) \<in> 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)
--- 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
(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(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)
--- 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
(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(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)