src/HOL/Integ/Equiv.ML
changeset 972 e61b058d58d2
parent 925 15539deb6863
child 1045 0cdf86973c49
     1.1 --- a/src/HOL/Integ/Equiv.ML	Thu Mar 23 15:39:13 1995 +0100
     1.2 +++ b/src/HOL/Integ/Equiv.ML	Fri Mar 24 12:30:35 1995 +0100
     1.3 @@ -19,24 +19,24 @@
     1.4  by (fast_tac (comp_cs addSEs [converseD]) 1);
     1.5  qed "sym_trans_comp_subset";
     1.6  
     1.7 -val [major,minor]=goal Equiv.thy "[|<x,y>:r; z=<x,y>|] ==>  z:r";
     1.8 +val [major,minor]=goal Equiv.thy "[|(x,y):r; z=(x,y)|] ==>  z:r";
     1.9  by (simp_tac (prod_ss addsimps [minor]) 1);
    1.10  by (rtac major 1);
    1.11  qed "BreakPair";
    1.12  
    1.13 -val [major]=goal Equiv.thy "[|? x y. <x,y>:r & z=<x,y>|] ==>  z:r";
    1.14 +val [major]=goal Equiv.thy "[|? x y. (x,y):r & z=(x,y)|] ==>  z:r";
    1.15  by (resolve_tac [major RS exE] 1);
    1.16  by (etac exE 1);
    1.17  by (etac conjE 1);
    1.18  by (asm_simp_tac (prod_ss addsimps [minor]) 1);
    1.19  qed "BreakPair1";
    1.20  
    1.21 -val [major,minor]=goal Equiv.thy "[|z:r; z=<x,y>|] ==> <x,y>:r";
    1.22 +val [major,minor]=goal Equiv.thy "[|z:r; z=(x,y)|] ==> (x,y):r";
    1.23  by (simp_tac (prod_ss addsimps [minor RS sym]) 1);
    1.24  by (rtac major 1);
    1.25  qed "BuildPair";
    1.26  
    1.27 -val [major]=goal Equiv.thy "[|? z:r. <x,y>=z|] ==> <x,y>:r";
    1.28 +val [major]=goal Equiv.thy "[|? z:r. (x,y)=z|] ==> (x,y):r";
    1.29  by (resolve_tac [major RS bexE] 1);
    1.30  by (asm_simp_tac (prod_ss addsimps []) 1);
    1.31  qed "BuildPair1";
    1.32 @@ -65,7 +65,7 @@
    1.33  goalw Equiv.thy [equiv_def,refl_def,sym_def,trans_def]
    1.34      "!!A r. [| converse(r) O r = r;  Domain(r) = A |] ==> equiv A r";
    1.35  by (etac equalityE 1);
    1.36 -by (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r" 1);
    1.37 +by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
    1.38  by (safe_tac set_cs);
    1.39  by (fast_tac (set_cs addSIs [converseI] addIs [compI]) 3);
    1.40  by (fast_tac (set_cs addSIs [converseI] addIs [compI] addSEs [DomainE]) 2);
    1.41 @@ -84,14 +84,14 @@
    1.42  
    1.43  (*Lemma for the next result*)
    1.44  goalw Equiv.thy [equiv_def,trans_def,sym_def]
    1.45 -    "!!A r. [| equiv A r;  <a,b>: r |] ==> r^^{a} <= r^^{b}";
    1.46 +    "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} <= r^^{b}";
    1.47  by (safe_tac rel_cs);
    1.48  by (rtac ImageI 1);
    1.49  by (fast_tac rel_cs 2);
    1.50  by (fast_tac rel_cs 1);
    1.51  qed "equiv_class_subset";
    1.52  
    1.53 -goal Equiv.thy "!!A r. [| equiv A r;  <a,b>: r |] ==> r^^{a} = r^^{b}";
    1.54 +goal Equiv.thy "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} = r^^{b}";
    1.55  by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
    1.56  by (rewrite_goals_tac [equiv_def,sym_def]);
    1.57  by (fast_tac rel_cs 1);
    1.58 @@ -105,18 +105,18 @@
    1.59  
    1.60  (*Lemma for the next result*)
    1.61  goalw Equiv.thy [equiv_def,refl_def]
    1.62 -    "!!A r. [| equiv A r;  r^^{b} <= r^^{a};  b: A |] ==> <a,b>: r";
    1.63 +    "!!A r. [| equiv A r;  r^^{b} <= r^^{a};  b: A |] ==> (a,b): r";
    1.64  by (fast_tac rel_cs 1);
    1.65  qed "subset_equiv_class";
    1.66  
    1.67  val prems = goal Equiv.thy
    1.68 -    "[| r^^{a} = r^^{b};  equiv A r;  b: A |] ==> <a,b>: r";
    1.69 +    "[| r^^{a} = r^^{b};  equiv A r;  b: A |] ==> (a,b): r";
    1.70  by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1));
    1.71  qed "eq_equiv_class";
    1.72  
    1.73  (*thus r^^{a} = r^^{b} as well*)
    1.74  goalw Equiv.thy [equiv_def,trans_def,sym_def]
    1.75 -    "!!A r. [| equiv A r;  x: (r^^{a} Int r^^{b}) |] ==> <a,b>: r";
    1.76 +    "!!A r. [| equiv A r;  x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
    1.77  by (fast_tac rel_cs 1);
    1.78  qed "equiv_class_nondisjoint";
    1.79  
    1.80 @@ -126,7 +126,7 @@
    1.81  qed "equiv_type";
    1.82  
    1.83  goal Equiv.thy
    1.84 -    "!!A r. equiv A r ==> (<x,y>: r) = (r^^{x} = r^^{y} & x:A & y:A)";
    1.85 +    "!!A r. equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
    1.86  by (safe_tac rel_cs);
    1.87  by ((rtac equiv_class_eq 1) THEN (assume_tac 1) THEN (assume_tac 1));
    1.88  by ((rtac eq_equiv_class 3) THEN 
    1.89 @@ -138,7 +138,7 @@
    1.90  qed "equiv_class_eq_iff";
    1.91  
    1.92  goal Equiv.thy
    1.93 -    "!!A r. [| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = (<x,y>: r)";
    1.94 +    "!!A r. [| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
    1.95  by (safe_tac rel_cs);
    1.96  by ((rtac eq_equiv_class 1) THEN 
    1.97      (assume_tac 1) THEN (assume_tac 1) THEN (assume_tac 1));
    1.98 @@ -227,7 +227,7 @@
    1.99  val _::_::prems = goalw Equiv.thy [quotient_def]
   1.100      "[| equiv A r;   congruent r b;  \
   1.101  \       (UN x:X. b(x))=(UN y:Y. b(y));  X: A/r;  Y: A/r;  \
   1.102 -\       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |] 	\
   1.103 +\       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |] 	\
   1.104  \    ==> X=Y";
   1.105  by (cut_facts_tac prems 1);
   1.106  by (safe_tac rel_cs);
   1.107 @@ -286,8 +286,8 @@
   1.108    than the direct proof*)
   1.109  val prems = goalw Equiv.thy [congruent2_def,equiv_def,refl_def]
   1.110      "[| equiv A r;	\
   1.111 -\       !! y z w. [| w: A;  <y,z> : r |] ==> b y w = b z w;      \
   1.112 -\       !! y z w. [| w: A;  <y,z> : r |] ==> b w y = b w z       \
   1.113 +\       !! y z w. [| w: A;  (y,z) : r |] ==> b y w = b z w;      \
   1.114 +\       !! y z w. [| w: A;  (y,z) : r |] ==> b w y = b w z       \
   1.115  \    |] ==> congruent2 r b";
   1.116  by (cut_facts_tac prems 1);
   1.117  by (safe_tac rel_cs);
   1.118 @@ -299,7 +299,7 @@
   1.119  val [equivA,commute,congt] = goal Equiv.thy
   1.120      "[| equiv A r;	\
   1.121  \       !! y z. [| y: A;  z: A |] ==> b y z = b z y;        \
   1.122 -\       !! y z w. [| w: A;  <y,z>: r |] ==> b w y = b w z	\
   1.123 +\       !! y z w. [| w: A;  (y,z): r |] ==> b w y = b w z	\
   1.124  \    |] ==> congruent2 r b";
   1.125  by (resolve_tac [equivA RS congruent2I] 1);
   1.126  by (rtac (commute RS trans) 1);