# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260394991 -3600
# Node ID bb276771d85c474e2ec4d8076907c53131c0b5d9
# Parent  217db3103f6a4e93a790b841652d13ea058d229e
Finished one proof in IntEx2.

diff -r 217db3103f6a -r bb276771d85c Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Wed Dec 09 22:05:11 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Wed Dec 09 22:43:11 2009 +0100
@@ -202,11 +202,19 @@
 qed
 
 
+lemma plus_raw_rsp_lo:
+  "\<And>a b c d. a \<approx> b \<Longrightarrow> c \<approx> d \<Longrightarrow> plus_raw a c \<approx> plus_raw b d"
+by auto
+
 lemma add:
      "(ABS_int (x,y)) + (ABS_int (u,v)) =
       (ABS_int (x+u, y+v))"
 apply(simp add: plus_int_def)
-sorry
+apply(fold plus_raw.simps)
+apply(rule Quotient_rel_abs[OF Quotient_int])
+apply(rule plus_raw_rsp_lo)
+apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
+done
 
 lemma int_def: "of_nat m = ABS_int (m, 0)"
 apply(induct m)
diff -r 217db3103f6a -r bb276771d85c Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Wed Dec 09 22:05:11 2009 +0100
+++ b/Quot/QuotScript.thy	Wed Dec 09 22:43:11 2009 +0100
@@ -510,7 +510,7 @@
 lemma rep_abs_rsp_left:
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
-  shows "R x1 (Rep (Abs x2))"
+  shows "R (Rep (Abs x1)) x2"
 using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])