# HG changeset patch
# User huffman
# Date 1181173475 -7200
# Node ID c95a4f6b3881ec08b5823915d3c3cdc530541f9e
# Parent  07ae93e58fead3e1ad917f3ca25e257071603b4b
instance preal :: ordered_cancel_ab_semigroup_add

diff -r 07ae93e58fea -r c95a4f6b3881 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Wed Jun 06 23:06:29 2007 +0200
+++ b/src/HOL/Real/PReal.thy	Thu Jun 07 01:44:35 2007 +0200
@@ -1128,6 +1128,16 @@
     preal_add_le_cancel_right preal_add_le_cancel_left
     preal_add_left_cancel_iff preal_add_right_cancel_iff
 
+instance preal :: ordered_cancel_ab_semigroup_add
+proof
+  fix a b c :: preal
+  show "a + b + c = a + (b + c)" by (rule preal_add_assoc)
+  show "a + b = b + a" by (rule preal_add_commute)
+  show "a + b = a + c \<Longrightarrow> b = c" by (rule preal_add_left_cancel)
+  show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
+    by (simp only: preal_add_le_cancel_left)
+qed
+
 
 subsection{*Completeness of type @{typ preal}*}