# HG changeset patch
# User obua
# Date 1084867304 -7200
# Node ID a080eeeaec14d30b6ceba46d401650b022f86aa2
# Parent  f40b45db8cf06c5724e6f4e194a15da9592dd168
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy

diff -r f40b45db8cf0 -r a080eeeaec14 src/HOL/Integ/Bin.thy
--- a/src/HOL/Integ/Bin.thy	Mon May 17 14:05:06 2004 +0200
+++ b/src/HOL/Integ/Bin.thy	Tue May 18 10:01:44 2004 +0200
@@ -31,7 +31,6 @@
 lemma number_of_pred: "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
 apply (induct_tac "w")
 apply (simp_all add: number_of add_assoc [symmetric]) 
-apply (simp add: add_ac)
 done
 
 lemma number_of_minus: "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)"
@@ -49,7 +48,6 @@
 apply (rule allI)
 apply (induct_tac "w")
 apply (simp_all add: number_of bin_add_BIT_BIT number_of_succ number_of_pred add_ac)
-apply (simp add: add_left_commute [of "1::'a::number_ring"]) 
 done
 
 lemma number_of_mult:
@@ -147,8 +145,8 @@
     assume eq: "1 + z + z = 0"
     have "0 < 1 + (int n + int n)"
       by (simp add: le_imp_0_less add_increasing) 
-    also have "... = - (1 + z + z)"
-      by (simp add: neg add_assoc [symmetric], simp add: add_commute) 
+    also have "... = - (1 + z + z)" 
+      by (simp add: neg add_assoc [symmetric]) 
     also have "... = 0" by (simp add: eq) 
     finally have "0<0" ..
     thus False by blast
diff -r f40b45db8cf0 -r a080eeeaec14 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon May 17 14:05:06 2004 +0200
+++ b/src/HOL/IsaMakefile	Tue May 18 10:01:44 2004 +0200
@@ -95,7 +95,7 @@
   Power.thy PreList.thy Product_Type.ML Product_Type.thy \
   Refute.thy ROOT.ML \
   Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \
-  Relation_Power.thy Ring_and_Field.thy\
+  Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML Ring_and_Field.thy\
   Set.ML Set.thy SetInterval.ML SetInterval.thy \
   Sum_Type.ML Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
   Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
diff -r f40b45db8cf0 -r a080eeeaec14 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Mon May 17 14:05:06 2004 +0200
+++ b/src/HOL/OrderedGroup.thy	Tue May 18 10:01:44 2004 +0200
@@ -9,7 +9,8 @@
 
 header {* Ordered Groups *}
 
-theory OrderedGroup = Inductive + LOrder:
+theory OrderedGroup = Inductive + LOrder
+  files "../Provers/Arith/abel_cancel.ML":
 
 text {*
   The theory of partially ordered groups is taken from the books:
@@ -412,7 +413,7 @@
 lemma add_diff_cancel: "a + b - b = (a::'a::ab_group_add)"
 by (simp add: diff_minus add_ac)
 
-text{*Further subtraction laws for ordered rings*}
+text{*Further subtraction laws*}
 
 lemma less_iff_diff_less_0: "(a < b) = (a - b < (0::'a::pordered_ab_group_add))"
 proof -
@@ -802,6 +803,39 @@
   finally show ?thesis .
 qed
 
+text {* Needed for abelian cancellation simprocs: *}
+
+lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"
+apply (subst add_left_commute)
+apply (subst add_left_cancel)
+apply simp
+done
+
+lemma add_cancel_end: "(x + (y + z) = y) = (x = - (z::'a::ab_group_add))"
+apply (subst add_cancel_21[of _ _ _ 0, simplified])
+apply (simp add: add_right_cancel[symmetric, of "x" "-z" "z", simplified])
+done
+
+lemma less_eqI: "(x::'a::pordered_ab_group_add) - y = x' - y' \<Longrightarrow> (x < y) = (x' < y')"
+by (simp add: less_iff_diff_less_0[of x y] less_iff_diff_less_0[of x' y'])
+
+lemma le_eqI: "(x::'a::pordered_ab_group_add) - y = x' - y' \<Longrightarrow> (y <= x) = (y' <= x')"
+apply (simp add: le_iff_diff_le_0[of y x] le_iff_diff_le_0[of  y' x'])
+apply (simp add: neg_le_iff_le[symmetric, of "y-x" 0] neg_le_iff_le[symmetric, of "y'-x'" 0])
+done
+
+lemma eq_eqI: "(x::'a::ab_group_add) - y = x' - y' \<Longrightarrow> (x = y) = (x' = y')"
+by (simp add: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])
+
+lemma diff_def: "(x::'a::ab_group_add) - y == x + (-y)"
+by (simp add: diff_minus)
+
+lemma add_minus_cancel: "(a::'a::ab_group_add) + (-a + b) = b"
+by (simp add: add_assoc[symmetric])
+
+lemma minus_add_cancel: "-(a::'a::ab_group_add) + (a + b) = b"
+by (simp add: add_assoc[symmetric])
+
 ML {*
 val add_zero_left = thm"add_0";
 val add_zero_right = thm"add_0_right";
diff -r f40b45db8cf0 -r a080eeeaec14 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Mon May 17 14:05:06 2004 +0200
+++ b/src/HOL/Real/RealDef.thy	Tue May 18 10:01:44 2004 +0200
@@ -406,7 +406,7 @@
   have "z + x - (z + y) = (z + -z) + (x - y)"
     by (simp add: diff_minus add_ac) 
   with le show ?thesis 
-    by (simp add: real_le_eq_diff [of x] real_le_eq_diff [of "z+x"])
+    by (simp add: real_le_eq_diff[of x] real_le_eq_diff[of "z+x"] diff_minus)
 qed
 
 lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)"
diff -r f40b45db8cf0 -r a080eeeaec14 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Mon May 17 14:05:06 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy	Tue May 18 10:01:44 2004 +0200
@@ -1365,28 +1365,18 @@
   note addm = add_mono[of "0::'a" _ "0::'a", simplified]
   note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]
   have xy: "- ?x <= ?y"
-    apply (simp add: compare_rls)
-    apply (rule add_le_imp_le_left[of "-(pprt a * nprt b + nprt a * pprt b)"])
-    apply (simp add: add_ac)
-    proof -
-      let ?r = "nprt a * nprt b +(nprt a * nprt b + (nprt a * pprt b + (pprt a * nprt b + (pprt a * pprt b + (pprt a * pprt b +
-	(- (nprt a * pprt b) + - (pprt a * nprt b)))))))"
-      let ?rr = "nprt a * nprt b + nprt a * nprt b + ((nprt a * pprt b) + (- (nprt a * pprt b))) + ((pprt a * nprt b) + - (pprt a * nprt b))
-	+ pprt a * pprt b + pprt a * pprt b"
-      have a:"?r = ?rr" by (simp only: add_ac)      
-      have "0 <= ?rr"
-	apply (simp)
-	apply (rule addm)+
-	apply (simp_all add: mult_neg_le mult_pos_le)
-	done
-      with a show "0 <= ?r" by simp
-    qed
+    apply (simp)
+    apply (rule_tac y="0::'a" in order_trans)
+    apply (rule addm2)+
+    apply (simp_all add: mult_pos_le mult_neg_le)
+    apply (rule addm)+
+    apply (simp_all add: mult_pos_le mult_neg_le)
+    done
   have yx: "?y <= ?x"
     apply (simp add: add_ac)
-    apply (simp add: compare_rls)
-    apply (rule add_le_imp_le_right[of _ "-(pprt a * pprt b)"])
-    apply (simp add: add_ac)
-    apply (rule addm2, (simp add: mult_pos_neg_le mult_pos_neg2_le)+)+
+    apply (rule_tac y=0 in order_trans)
+    apply (rule addm2, (simp add: mult_pos_neg_le mult_pos_neg2_le)+)
+    apply (rule addm, (simp add: mult_pos_neg_le mult_pos_neg2_le)+)
     done
   have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
   have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
@@ -1417,9 +1407,16 @@
     assume "0 <= a * b"
     then show ?thesis
       apply (simp_all add: mulprts abs_prts)
+      apply (simp add: 
+	iff2imp[OF zero_le_iff_zero_nprt]
+	iff2imp[OF le_zero_iff_pprt_id]
+      )
       apply (insert prems)
-      apply (auto simp add: ring_eq_simps iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
-	iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id] order_antisym mult_pos_neg_le[of a b] mult_pos_neg2_le[of b a])
+      apply (auto simp add: 
+	ring_eq_simps 
+	iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_zero_pprt]
+	iff2imp[OF le_zero_iff_pprt_id] iff2imp[OF zero_le_iff_nprt_id] 
+	order_antisym mult_pos_neg_le[of a b] mult_pos_neg2_le[of b a])
       done
   next
     assume "~(0 <= a*b)"