1.1 --- a/src/ZF/Integ/EquivClass.thy	Fri Sep 03 22:40:57 2004 +0200
     1.2 +++ b/src/ZF/Integ/EquivClass.thy	Mon Sep 06 15:57:58 2004 +0200
     1.3 @@ -17,9 +17,18 @@
     1.4    congruent  :: "[i,i=>i]=>o"
     1.5        "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
     1.6  
     1.7 -  congruent2 :: "[i,[i,i]=>i]=>o"
     1.8 -      "congruent2(r,b) == ALL y1 z1 y2 z2.
     1.9 -           <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)"
    1.10 +  congruent2 :: "[i,i,[i,i]=>i]=>o"
    1.11 +      "congruent2(r1,r2,b) == ALL y1 z1 y2 z2.
    1.12 +           <y1,z1>:r1 --> <y2,z2>:r2 --> b(y1,y2) = b(z1,z2)"
    1.13 +
    1.14 +syntax
    1.15 +  RESPECTS ::"[i=>i, i] => o"  (infixr "respects" 80)
    1.16 +  RESPECTS2 ::"[i=>i, i] => o"  (infixr "respects2 " 80)
    1.17 +    --{*Abbreviation for the common case where the relations are identical*}
    1.18 +
    1.19 +translations
    1.20 +  "f respects r" == "congruent(r,f)"
    1.21 +  "f respects2 r" => "congruent2(r,r,f)"
    1.22  
    1.23  subsection{*Suppes, Theorem 70:
    1.24      @{term r} is an equiv relation iff @{term "converse(r) O r = r"}*}
    1.25 @@ -28,19 +37,16 @@
    1.26  
    1.27  lemma sym_trans_comp_subset:
    1.28      "[| sym(r); trans(r) |] ==> converse(r) O r <= r"
    1.29 -apply (unfold trans_def sym_def, blast)
    1.30 -done
    1.31 +by (unfold trans_def sym_def, blast)
    1.32  
    1.33  lemma refl_comp_subset:
    1.34      "[| refl(A,r); r <= A*A |] ==> r <= converse(r) O r"
    1.35 -apply (unfold refl_def, blast)
    1.36 -done
    1.37 +by (unfold refl_def, blast)
    1.38  
    1.39  lemma equiv_comp_eq:
    1.40      "equiv(A,r) ==> converse(r) O r = r"
    1.41  apply (unfold equiv_def)
    1.42 -apply (blast del: subsetI
    1.43 -             intro!: sym_trans_comp_subset refl_comp_subset)
    1.44 +apply (blast del: subsetI intro!: sym_trans_comp_subset refl_comp_subset)
    1.45  done
    1.46  
    1.47  (*second half*)
    1.48 @@ -124,7 +130,7 @@
    1.49  
    1.50  (*Conversion rule*)
    1.51  lemma UN_equiv_class:
    1.52 -    "[| equiv(A,r);  congruent(r,b);  a: A |] ==> (UN x:r``{a}. b(x)) = b(a)"
    1.53 +    "[| equiv(A,r);  b respects r;  a: A |] ==> (UN x:r``{a}. b(x)) = b(a)"
    1.54  apply (subgoal_tac "\<forall>x \<in> r``{a}. b(x) = b(a)") 
    1.55   apply simp
    1.56   apply (blast intro: equiv_class_self)  
    1.57 @@ -133,7 +139,7 @@
    1.58  
    1.59  (*type checking of  UN x:r``{a}. b(x) *)
    1.60  lemma UN_equiv_class_type:
    1.61 -    "[| equiv(A,r);  congruent(r,b);  X: A//r;  !!x.  x : A ==> b(x) : B |]
    1.62 +    "[| equiv(A,r);  b respects r;  X: A//r;  !!x.  x : A ==> b(x) : B |]
    1.63       ==> (UN x:X. b(x)) : B"
    1.64  apply (unfold quotient_def, safe)
    1.65  apply (simp (no_asm_simp) add: UN_equiv_class)
    1.66 @@ -143,7 +149,7 @@
    1.67    major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
    1.68  *)
    1.69  lemma UN_equiv_class_inject:
    1.70 -    "[| equiv(A,r);   congruent(r,b);
    1.71 +    "[| equiv(A,r);   b respects r;
    1.72          (UN x:X. b(x))=(UN y:Y. b(y));  X: A//r;  Y: A//r;
    1.73          !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |]
    1.74       ==> X=Y"
    1.75 @@ -156,28 +162,28 @@
    1.76  subsection{*Defining Binary Operations upon Equivalence Classes*}
    1.77  
    1.78  lemma congruent2_implies_congruent:
    1.79 -    "[| equiv(A,r);  congruent2(r,b);  a: A |] ==> congruent(r,b(a))"
    1.80 +    "[| equiv(A,r1);  congruent2(r1,r2,b);  a: A |] ==> congruent(r2,b(a))"
    1.81  by (unfold congruent_def congruent2_def equiv_def refl_def, blast)
    1.82  
    1.83  lemma congruent2_implies_congruent_UN:
    1.84 -    "[| equiv(A,r);  congruent2(r,b);  a: A |] ==>
    1.85 -     congruent(r, %x1. UN x2:r``{a}. b(x1,x2))"
    1.86 +    "[| equiv(A1,r1);  equiv(A2,r2);  congruent2(r1,r2,b);  a: A2 |] ==>
    1.87 +     congruent(r1, %x1. \<Union>x2 \<in> r2``{a}. b(x1,x2))"
    1.88  apply (unfold congruent_def, safe)
    1.89  apply (frule equiv_type [THEN subsetD], assumption)
    1.90  apply clarify 
    1.91 -apply (simp add: UN_equiv_class [of A r] congruent2_implies_congruent)
    1.92 +apply (simp add: UN_equiv_class congruent2_implies_congruent)
    1.93  apply (unfold congruent2_def equiv_def refl_def, blast)
    1.94  done
    1.95  
    1.96  lemma UN_equiv_class2:
    1.97 -    "[| equiv(A,r);  congruent2(r,b);  a1: A;  a2: A |]
    1.98 -     ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)"
    1.99 -by (simp add: UN_equiv_class [of A r] congruent2_implies_congruent
   1.100 +    "[| equiv(A1,r1);  equiv(A2,r2);  congruent2(r1,r2,b);  a1: A1;  a2: A2 |]
   1.101 +     ==> (\<Union>x1 \<in> r1``{a1}. \<Union>x2 \<in> r2``{a2}. b(x1,x2)) = b(a1,a2)"
   1.102 +by (simp add: UN_equiv_class congruent2_implies_congruent
   1.103                congruent2_implies_congruent_UN)
   1.104  
   1.105  (*type checking*)
   1.106  lemma UN_equiv_class_type2:
   1.107 -    "[| equiv(A,r);  congruent2(r,b);
   1.108 +    "[| equiv(A,r);  b respects2 r;
   1.109          X1: A//r;  X2: A//r;
   1.110          !!x1 x2.  [| x1: A; x2: A |] ==> b(x1,x2) : B
   1.111       |] ==> (UN x1:X1. UN x2:X2. b(x1,x2)) : B"
   1.112 @@ -190,10 +196,10 @@
   1.113  (*Suggested by John Harrison -- the two subproofs may be MUCH simpler
   1.114    than the direct proof*)
   1.115  lemma congruent2I:
   1.116 -    "[| equiv(A,r);
   1.117 -        !! y z w. [| w: A;  <y,z> : r |] ==> b(y,w) = b(z,w);
   1.118 -        !! y z w. [| w: A;  <y,z> : r |] ==> b(w,y) = b(w,z)
   1.119 -     |] ==> congruent2(r,b)"
   1.120 +    "[|  equiv(A1,r1);  equiv(A2,r2);  
   1.121 +        !! y z w. [| w \<in> A2;  <y,z> \<in> r1 |] ==> b(y,w) = b(z,w);
   1.122 +        !! y z w. [| w \<in> A1;  <y,z> \<in> r2 |] ==> b(w,y) = b(w,z)
   1.123 +     |] ==> congruent2(r1,r2,b)"
   1.124  apply (unfold congruent2_def equiv_def refl_def, safe)
   1.125  apply (blast intro: trans) 
   1.126  done
   1.127 @@ -202,9 +208,9 @@
   1.128   assumes equivA: "equiv(A,r)"
   1.129       and commute: "!! y z. [| y: A;  z: A |] ==> b(y,z) = b(z,y)"
   1.130       and congt:   "!! y z w. [| w: A;  <y,z>: r |] ==> b(w,y) = b(w,z)"
   1.131 - shows "congruent2(r,b)"
   1.132 + shows "b respects2 r"
   1.133  apply (insert equivA [THEN equiv_type, THEN subsetD]) 
   1.134 -apply (rule congruent2I [OF equivA])
   1.135 +apply (rule congruent2I [OF equivA equivA])
   1.136  apply (rule commute [THEN trans])
   1.137  apply (rule_tac [3] commute [THEN trans, symmetric])
   1.138  apply (rule_tac [5] sym) 

     2.1 --- a/src/ZF/Integ/Int.thy	Fri Sep 03 22:40:57 2004 +0200
     2.2 +++ b/src/ZF/Integ/Int.thy	Mon Sep 06 15:57:58 2004 +0200
     2.3 @@ -202,7 +202,7 @@
     2.4  
     2.5  subsection{*@{term zminus}: unary negation on @{term int}*}
     2.6  
     2.7 -lemma zminus_congruent: "congruent(intrel, %<x,y>. intrel``{<y,x>})"
     2.8 +lemma zminus_congruent: "(%<x,y>. intrel``{<y,x>}) respects intrel"
     2.9  by (auto simp add: congruent_def add_ac)
    2.10  
    2.11  lemma raw_zminus_type: "z : int ==> raw_zminus(z) : int"
    2.12 @@ -276,7 +276,7 @@
    2.13  lemma nat_of_intify [simp]: "nat_of(intify(z)) = nat_of(z)"
    2.14  by (simp add: nat_of_def)
    2.15  
    2.16 -lemma nat_of_congruent: "congruent(intrel, \<lambda>x. (\<lambda>\<langle>x,y\<rangle>. x #- y)(x))"
    2.17 +lemma nat_of_congruent: "(\<lambda>x. (\<lambda>\<langle>x,y\<rangle>. x #- y)(x)) respects intrel"
    2.18  by (auto simp add: congruent_def split add: nat_diff_split)
    2.19  
    2.20  lemma raw_nat_of: 
    2.21 @@ -369,9 +369,9 @@
    2.22  
    2.23  text{*Congruence Property for Addition*}
    2.24  lemma zadd_congruent2: 
    2.25 -    "congruent2(intrel, %z1 z2.                       
    2.26 -          let <x1,y1>=z1; <x2,y2>=z2                  
    2.27 -                            in intrel``{<x1#+x2, y1#+y2>})"
    2.28 +    "(%z1 z2. let <x1,y1>=z1; <x2,y2>=z2                  
    2.29 +                            in intrel``{<x1#+x2, y1#+y2>})
    2.30 +     respects2 intrel"
    2.31  apply (simp add: congruent2_def)
    2.32  (*Proof via congruent2_commuteI seems longer*)
    2.33  apply safe
    2.34 @@ -396,7 +396,8 @@
    2.35    "[| x1\<in>nat; y1\<in>nat;  x2\<in>nat; y2\<in>nat |]               
    2.36     ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) =   
    2.37         intrel `` {<x1#+x2, y1#+y2>}"
    2.38 -apply (simp add: raw_zadd_def UN_equiv_class2 [OF equiv_intrel zadd_congruent2])
    2.39 +apply (simp add: raw_zadd_def 
    2.40 +             UN_equiv_class2 [OF equiv_intrel equiv_intrel zadd_congruent2])
    2.41  apply (simp add: Let_def)
    2.42  done
    2.43  
    2.44 @@ -482,9 +483,9 @@
    2.45  
    2.46  text{*Congruence property for multiplication*}
    2.47  lemma zmult_congruent2:
    2.48 -    "congruent2(intrel, %p1 p2.                  
    2.49 -                split(%x1 y1. split(%x2 y2.      
    2.50 -                    intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))"
    2.51 +    "(%p1 p2. split(%x1 y1. split(%x2 y2.      
    2.52 +                    intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))
    2.53 +     respects2 intrel"
    2.54  apply (rule equiv_intrel [THEN congruent2_commuteI], auto)
    2.55  (*Proof that zmult is congruent in one argument*)
    2.56  apply (rename_tac x y)
    2.57 @@ -508,7 +509,8 @@
    2.58       "[| x1\<in>nat; y1\<in>nat;  x2\<in>nat; y2\<in>nat |]     
    2.59        ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) =      
    2.60            intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}"
    2.61 -by (simp add: raw_zmult_def UN_equiv_class2 [OF equiv_intrel zmult_congruent2])
    2.62 +by (simp add: raw_zmult_def 
    2.63 +           UN_equiv_class2 [OF equiv_intrel equiv_intrel zmult_congruent2])
    2.64  
    2.65  lemma zmult: 
    2.66       "[| x1\<in>nat; y1\<in>nat;  x2\<in>nat; y2\<in>nat |]