--- 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
--- 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 @@
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";
--- 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)"
--- 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)"