# HG changeset patch
# User paulson
# Date 1081430073 -7200
# Node ID 43e44c8b03abb592687b3d29b0a85f89080d657c
# Parent  716c9def561470aeed270fed30d79d4081c09bd6
tidied

diff -r 716c9def5614 -r 43e44c8b03ab src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Thu Apr 08 12:49:23 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy	Thu Apr 08 15:14:33 2004 +0200
@@ -37,19 +37,19 @@
   One_int_def:   "1 == int 1"
 
   minus_int_def:
-    "- z == contents (\<Union>(x,y) \<in> Rep_Integ(z). { Abs_Integ(intrel``{(y,x)}) })"
+    "- z == Abs_Integ (\<Union>(x,y) \<in> Rep_Integ z. intrel``{(y,x)})"
 
   add_int_def:
    "z + w ==
-       contents (\<Union>(x,y) \<in> Rep_Integ(z). \<Union>(u,v) \<in> Rep_Integ(w).
-		 { Abs_Integ(intrel``{(x+u, y+v)}) })"
+       Abs_Integ (\<Union>(x,y) \<in> Rep_Integ z. \<Union>(u,v) \<in> Rep_Integ w.
+		 intrel``{(x+u, y+v)})"
 
   diff_int_def:  "z - (w::int) == z + (-w)"
 
   mult_int_def:
    "z * w ==
-       contents (\<Union>(x,y) \<in> Rep_Integ(z). \<Union>(u,v) \<in> Rep_Integ(w).
-		 { Abs_Integ(intrel``{(x*u + y*v, x*v + y*u)}) })"
+       Abs_Integ (\<Union>(x,y) \<in> Rep_Integ z. \<Union>(u,v) \<in> Rep_Integ w.
+		  intrel``{(x*u + y*v, x*v + y*u)})"
 
   le_int_def:
    "z \<le> (w::int) == 
@@ -76,7 +76,7 @@
 
 
 text{*All equivalence classes belong to set of representatives*}
-lemma intrel_in_integ [simp]: "intrel``{(x,y)} \<in> Integ"
+lemma [simp]: "intrel``{(x,y)} \<in> Integ"
 by (auto simp add: Integ_def intrel_def quotient_def)
 
 lemma inj_on_Abs_Integ: "inj_on Abs_Integ Integ"
@@ -114,7 +114,7 @@
 
 lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
 proof -
-  have "congruent intrel (\<lambda>(x,y). {Abs_Integ (intrel``{(y,x)})})"
+  have "congruent intrel (\<lambda>(x,y). intrel``{(y,x)})"
     by (simp add: congruent_def) 
   thus ?thesis
     by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
@@ -134,7 +134,7 @@
       Abs_Integ (intrel``{(x+u, y+v)})"
 proof -
   have "congruent2 intrel
-        (\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Integ (intrel `` {(x+u, y+v)})}) w) z)"
+        (\<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
@@ -189,15 +189,17 @@
 lemma mult_congruent2:
      "congruent2 intrel
         (%p1 p2. (%(x,y). (%(u,v).
-                    { Abs_Integ(intrel``{(x*u + y*v, x*v + y*u)}) }) p2) p1)"
+                    intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)"
 apply (rule equiv_intrel [THEN congruent2_commuteI])
-apply (auto simp add: congruent_def mult_ac)  
+ apply (force simp add: mult_ac, clarify) 
+apply (simp add: congruent_def mult_ac)  
 apply (rename_tac u v w x y z)
 apply (subgoal_tac "u*y + x*y = w*y + v*y  &  u*z + x*z = w*z + v*z")
 apply (simp add: mult_ac, arith)
 apply (simp add: add_mult_distrib [symmetric])
 done
 
+
 lemma mult:
      "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) =
       Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})"
@@ -391,7 +393,7 @@
 
 constdefs
    nat  :: "int => nat"
-    "nat z == contents (\<Union>(x,y) \<in> Rep_Integ(z). { x-y })"
+    "nat z == contents (\<Union>(x,y) \<in> Rep_Integ z. { x-y })"
 
 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
 proof -
@@ -689,7 +691,7 @@
 
 constdefs
    of_int :: "int => 'a::ring"
-   "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ(z). { of_nat i - of_nat j })"
+   "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
 
 
 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"