author obua Tue, 18 May 2004 10:01:44 +0200 changeset 14754 a080eeeaec14 parent 14753 f40b45db8cf0 child 14755 5cc6e6b9e27a
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
 src/HOL/Integ/Bin.thy file | annotate | diff | comparison | revisions src/HOL/IsaMakefile file | annotate | diff | comparison | revisions src/HOL/OrderedGroup.thy file | annotate | diff | comparison | revisions src/HOL/Real/RealDef.thy file | annotate | diff | comparison | revisions src/HOL/Ring_and_Field.thy file | annotate | diff | comparison | revisions
```--- 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")
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")
done

lemma number_of_mult:
@@ -147,8 +145,8 @@
assume eq: "1 + z + z = 0"
have "0 < 1 + (int n + int n)"
-    also have "... = - (1 + z + z)"
+    also have "... = - (1 + z + z)"
also have "... = 0" by (simp add: eq)
finally have "0<0" ..
thus False by blast```
```--- 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 \```
```--- 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 @@

-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 @@

-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 simp
+done
+
+lemma add_cancel_end: "(x + (y + z) = y) = (x = - (z::'a::ab_group_add))"
+apply (subst add_cancel_21[of _ _ _ 0, 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)"
+
+
+
ML {*
```--- 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)"
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)"```
```--- 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 @@
have xy: "- ?x <= ?y"
-    apply (rule add_le_imp_le_left[of "-(pprt a * nprt b + nprt a * pprt b)"])
-    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 (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 (simp_all add: mult_pos_le mult_neg_le)
+    apply (simp_all add: mult_pos_le mult_neg_le)
+    done
have yx: "?y <= ?x"
-    apply (rule add_le_imp_le_right[of _ "-(pprt a * pprt b)"])
+    apply (rule_tac y=0 in order_trans)
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
+	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])