1.1 --- a/src/HOL/Integ/IntDef.thy	Thu Apr 08 12:49:23 2004 +0200
     1.2 +++ b/src/HOL/Integ/IntDef.thy	Thu Apr 08 15:14:33 2004 +0200
     1.3 @@ -37,19 +37,19 @@
     1.4    One_int_def:   "1 == int 1"
     1.5  
     1.6    minus_int_def:
     1.7 -    "- z == contents (\<Union>(x,y) \<in> Rep_Integ(z). { Abs_Integ(intrel``{(y,x)}) })"
     1.8 +    "- z == Abs_Integ (\<Union>(x,y) \<in> Rep_Integ z. intrel``{(y,x)})"
     1.9  
    1.10    add_int_def:
    1.11     "z + w ==
    1.12 -       contents (\<Union>(x,y) \<in> Rep_Integ(z). \<Union>(u,v) \<in> Rep_Integ(w).
    1.13 -		 { Abs_Integ(intrel``{(x+u, y+v)}) })"
    1.14 +       Abs_Integ (\<Union>(x,y) \<in> Rep_Integ z. \<Union>(u,v) \<in> Rep_Integ w.
    1.15 +		 intrel``{(x+u, y+v)})"
    1.16  
    1.17    diff_int_def:  "z - (w::int) == z + (-w)"
    1.18  
    1.19    mult_int_def:
    1.20     "z * w ==
    1.21 -       contents (\<Union>(x,y) \<in> Rep_Integ(z). \<Union>(u,v) \<in> Rep_Integ(w).
    1.22 -		 { Abs_Integ(intrel``{(x*u + y*v, x*v + y*u)}) })"
    1.23 +       Abs_Integ (\<Union>(x,y) \<in> Rep_Integ z. \<Union>(u,v) \<in> Rep_Integ w.
    1.24 +		  intrel``{(x*u + y*v, x*v + y*u)})"
    1.25  
    1.26    le_int_def:
    1.27     "z \<le> (w::int) == 
    1.28 @@ -76,7 +76,7 @@
    1.29  
    1.30  
    1.31  text{*All equivalence classes belong to set of representatives*}
    1.32 -lemma intrel_in_integ [simp]: "intrel``{(x,y)} \<in> Integ"
    1.33 +lemma [simp]: "intrel``{(x,y)} \<in> Integ"
    1.34  by (auto simp add: Integ_def intrel_def quotient_def)
    1.35  
    1.36  lemma inj_on_Abs_Integ: "inj_on Abs_Integ Integ"
    1.37 @@ -114,7 +114,7 @@
    1.38  
    1.39  lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
    1.40  proof -
    1.41 -  have "congruent intrel (\<lambda>(x,y). {Abs_Integ (intrel``{(y,x)})})"
    1.42 +  have "congruent intrel (\<lambda>(x,y). intrel``{(y,x)})"
    1.43      by (simp add: congruent_def) 
    1.44    thus ?thesis
    1.45      by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
    1.46 @@ -134,7 +134,7 @@
    1.47        Abs_Integ (intrel``{(x+u, y+v)})"
    1.48  proof -
    1.49    have "congruent2 intrel
    1.50 -        (\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Integ (intrel `` {(x+u, y+v)})}) w) z)"
    1.51 +        (\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z)"
    1.52      by (simp add: congruent2_def)
    1.53    thus ?thesis
    1.54      by (simp add: add_int_def UN_UN_split_split_eq
    1.55 @@ -189,15 +189,17 @@
    1.56  lemma mult_congruent2:
    1.57       "congruent2 intrel
    1.58          (%p1 p2. (%(x,y). (%(u,v).
    1.59 -                    { Abs_Integ(intrel``{(x*u + y*v, x*v + y*u)}) }) p2) p1)"
    1.60 +                    intrel``{(x*u + y*v, x*v + y*u)}) p2) p1)"
    1.61  apply (rule equiv_intrel [THEN congruent2_commuteI])
    1.62 -apply (auto simp add: congruent_def mult_ac)  
    1.63 + apply (force simp add: mult_ac, clarify) 
    1.64 +apply (simp add: congruent_def mult_ac)  
    1.65  apply (rename_tac u v w x y z)
    1.66  apply (subgoal_tac "u*y + x*y = w*y + v*y  &  u*z + x*z = w*z + v*z")
    1.67  apply (simp add: mult_ac, arith)
    1.68  apply (simp add: add_mult_distrib [symmetric])
    1.69  done
    1.70  
    1.71 +
    1.72  lemma mult:
    1.73       "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) =
    1.74        Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})"
    1.75 @@ -391,7 +393,7 @@
    1.76  
    1.77  constdefs
    1.78     nat  :: "int => nat"
    1.79 -    "nat z == contents (\<Union>(x,y) \<in> Rep_Integ(z). { x-y })"
    1.80 +    "nat z == contents (\<Union>(x,y) \<in> Rep_Integ z. { x-y })"
    1.81  
    1.82  lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
    1.83  proof -
    1.84 @@ -689,7 +691,7 @@
    1.85  
    1.86  constdefs
    1.87     of_int :: "int => 'a::ring"
    1.88 -   "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ(z). { of_nat i - of_nat j })"
    1.89 +   "of_int z == contents (\<Union>(i,j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
    1.90  
    1.91  
    1.92  lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"