# HG changeset patch
# User haftmann
# Date 1291129089 -3600
# Node ID 2ac5af6eb8a8e75ab1d1b97ae1a91485afc08947
# Parent  b117df72e56bbca18e4a3ff69a6fc79eedbb5cb7
adapted proofs to slightly changed definitions of congruent(2)

diff -r b117df72e56b -r 2ac5af6eb8a8 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Nov 29 22:47:55 2010 +0100
+++ b/src/HOL/Int.thy	Tue Nov 30 15:58:09 2010 +0100
@@ -102,7 +102,7 @@
 lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
 proof -
   have "(\<lambda>(x,y). intrel``{(y,x)}) respects intrel"
-    by (simp add: congruent_def) 
+    by (auto simp add: congruent_def)
   thus ?thesis
     by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel])
 qed
@@ -113,7 +113,7 @@
 proof -
   have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). intrel `` {(x+u, y+v)}) w) z) 
         respects2 intrel"
-    by (simp add: congruent2_def)
+    by (auto simp add: congruent2_def)
   thus ?thesis
     by (simp add: add_int_def UN_UN_split_split_eq
                   UN_equiv_class2 [OF equiv_intrel equiv_intrel])
@@ -288,7 +288,7 @@
 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
 proof -
   have "(\<lambda>(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel"
-    by (simp add: congruent_def algebra_simps of_nat_add [symmetric]
+    by (auto simp add: congruent_def) (simp add: algebra_simps of_nat_add [symmetric]
             del: of_nat_add) 
   thus ?thesis
     by (simp add: of_int_def UN_equiv_class [OF equiv_intrel])
@@ -394,7 +394,7 @@
 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
 proof -
   have "(\<lambda>(x,y). {x-y}) respects intrel"
-    by (simp add: congruent_def) arith
+    by (auto simp add: congruent_def)
   thus ?thesis
     by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
 qed
diff -r b117df72e56b -r 2ac5af6eb8a8 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Mon Nov 29 22:47:55 2010 +0100
+++ b/src/HOL/Rat.thy	Tue Nov 30 15:58:09 2010 +0100
@@ -146,7 +146,7 @@
 lemma minus_rat [simp]: "- Fract a b = Fract (- a) b"
 proof -
   have "(\<lambda>x. ratrel `` {(- fst x, snd x)}) respects ratrel"
-    by (simp add: congruent_def)
+    by (simp add: congruent_def split_paired_all)
   then show ?thesis by (simp add: Fract_def minus_rat_def UN_ratrel)
 qed