author haftmann Thu, 18 Oct 2007 09:20:57 +0200 changeset 25077 c2ec5e589d78 parent 25076 a50b36401c61 child 25078 a1ddc5206cb1
continued localization
 src/HOL/OrderedGroup.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/OrderedGroup.thy	Thu Oct 18 09:20:55 2007 +0200
+++ b/src/HOL/OrderedGroup.thy	Thu Oct 18 09:20:57 2007 +0200
@@ -35,7 +35,6 @@

lemma add_left_commute: "a + (b + c) = b + (a + c)"
-  (*FIXME term_check*)

@@ -52,7 +51,6 @@

lemma mult_left_commute: "a * (b * c) = b * (a * c)"
by (rule mk_left_commute [of "times", OF mult_assoc mult_commute])
-  (*FIXME term_check*)

theorems mult_ac = mult_assoc mult_commute mult_left_commute

@@ -264,6 +262,38 @@
"- (a - b) = b - a"

+lemma add_diff_eq: "a + (b - c) = (a + b) - c"
+
+lemma diff_add_eq: "(a - b) + c = (a + c) - b"
+
+lemma diff_eq_eq: "a - b = c \<longleftrightarrow> a = c + b"
+
+lemma eq_diff_eq: "a = c - b \<longleftrightarrow> a + b = c"
+
+lemma diff_diff_eq: "(a - b) - c = a - (b + c)"
+
+lemma diff_diff_eq2: "a - (b - c) = (a + c) - b"
+
+lemma diff_add_cancel: "a - b + b = a"
+
+lemma add_diff_cancel: "a + b - b = a"
+
+lemmas compare_rls =
+       diff_minus [symmetric]
+       diff_eq_eq eq_diff_eq
+
+lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
+
end

subsection {* (Partially) Ordered Groups *}
@@ -368,6 +398,14 @@
"a + c \<le> b + c \<Longrightarrow> a \<le> b"
by simp

+  "max x y + z = max (x + z) (y + z)"
+  unfolding max_def by auto
+
+  "min x y + z = min (x + z) (y + z)"
+  unfolding min_def by auto
+
end

@@ -388,6 +426,132 @@

end

+begin
+
+lemma max_diff_distrib_left:
+  shows "max x y - z = max (x - z) (y - z)"
+
+lemma min_diff_distrib_left:
+  shows "min x y - z = min (x - z) (y - z)"
+
+lemma le_imp_neg_le:
+  assumes "a \<le> b"
+  shows "-b \<le> -a"
+proof -
+  have "-a+a \<le> -a+b"
+    using `a \<le> b` by (rule add_left_mono)
+  hence "0 \<le> -a+b"
+    by simp
+  hence "0 + (-b) \<le> (-a + b) + (-b)"
+  thus ?thesis
+qed
+
+lemma neg_le_iff_le [simp]: "- b \<le> - a \<longleftrightarrow> a \<le> b"
+proof
+  assume "- b \<le> - a"
+  hence "- (- a) \<le> - (- b)"
+    by (rule le_imp_neg_le)
+  thus "a\<le>b" by simp
+next
+  assume "a\<le>b"
+  thus "-b \<le> -a" by (rule le_imp_neg_le)
+qed
+
+lemma neg_le_0_iff_le [simp]: "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
+  by (subst neg_le_iff_le [symmetric], simp)
+
+lemma neg_0_le_iff_le [simp]: "0 \<le> - a \<longleftrightarrow> a \<le> 0"
+  by (subst neg_le_iff_le [symmetric], simp)
+
+lemma neg_less_iff_less [simp]: "- b < - a \<longleftrightarrow> a < b"
+  by (force simp add: less_le)
+
+lemma neg_less_0_iff_less [simp]: "- a < 0 \<longleftrightarrow> 0 < a"
+  by (subst neg_less_iff_less [symmetric], simp)
+
+lemma neg_0_less_iff_less [simp]: "0 < - a \<longleftrightarrow> a < 0"
+  by (subst neg_less_iff_less [symmetric], simp)
+
+text{*The next several equations can make the simplifier loop!*}
+
+lemma less_minus_iff: "a < - b \<longleftrightarrow> b < - a"
+proof -
+  have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
+  thus ?thesis by simp
+qed
+
+lemma minus_less_iff: "- a < b \<longleftrightarrow> - b < a"
+proof -
+  have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
+  thus ?thesis by simp
+qed
+
+lemma le_minus_iff: "a \<le> - b \<longleftrightarrow> b \<le> - a"
+proof -
+  have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
+  have "(- (- a) <= -b) = (b <= - a)"
+    apply (auto simp only: le_less)
+    apply (drule mm)
+    apply (simp_all)
+    apply (drule mm[simplified], assumption)
+    done
+  then show ?thesis by simp
+qed
+
+lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
+  by (auto simp add: le_less minus_less_iff)
+
+lemma less_iff_diff_less_0: "a < b \<longleftrightarrow> a - b < 0"
+proof -
+  have  "(a < b) = (a + (- b) < b + (-b))"
+  also have "... =  (a - b < 0)" by (simp add: diff_minus)
+  finally show ?thesis .
+qed
+
+lemma diff_less_eq: "a - b < c \<longleftrightarrow> a < c + b"
+apply (subst less_iff_diff_less_0 [of a])
+apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
+done
+
+lemma less_diff_eq: "a < c - b \<longleftrightarrow> a + b < c"
+apply (subst less_iff_diff_less_0 [of "plus a b"])
+apply (subst less_iff_diff_less_0 [of a])
+done
+
+lemma diff_le_eq: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
+
+lemma le_diff_eq: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
+
+lemmas compare_rls =
+       diff_minus [symmetric]
+       diff_less_eq less_diff_eq diff_le_eq le_diff_eq
+       diff_eq_eq eq_diff_eq
+
+text{*This list of rewrites simplifies (in)equalities by bringing subtractions
+  to the top and then moving negative terms to the other side.
+lemmas (in -) compare_rls =
+       diff_minus [symmetric]
+       diff_less_eq less_diff_eq diff_le_eq le_diff_eq
+       diff_eq_eq eq_diff_eq
+
+lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
+
+end
+

@@ -416,17 +580,7 @@
qed
qed

--- {* FIXME continue localization here *}
-
-  shows  "(max x y) + z = max (x+z) (y+z)"
-by (rule max_of_mono [THEN sym], rule add_le_cancel_right)
-
-  shows  "(min x y) + z = min (x+z) (y+z)"
-by (rule min_of_mono [THEN sym], rule add_le_cancel_right)
+-- {* FIXME localize the following *}

@@ -448,147 +602,6 @@
shows "[|0\<le>a; b<c|] ==> b < a + c"
by (insert add_le_less_mono [of 0 a b c], simp)

-lemma max_diff_distrib_left:
-  shows  "(max x y) - z = max (x-z) (y-z)"
-
-lemma min_diff_distrib_left:
-  shows  "(min x y) - z = min (x-z) (y-z)"
-
-
-subsection {* Ordering Rules for Unary Minus *}
-
-lemma le_imp_neg_le:
-proof -
-  have "-a+a \<le> -a+b"
-    using `a \<le> b` by (rule add_left_mono)
-  hence "0 \<le> -a+b"
-    by simp
-  hence "0 + (-b) \<le> (-a + b) + (-b)"
-  thus ?thesis
-qed
-
-lemma neg_le_iff_le [simp]: "(-b \<le> -a) = (a \<le> (b::'a::pordered_ab_group_add))"
-proof
-  assume "- b \<le> - a"
-  hence "- (- a) \<le> - (- b)"
-    by (rule le_imp_neg_le)
-  thus "a\<le>b" by simp
-next
-  assume "a\<le>b"
-  thus "-b \<le> -a" by (rule le_imp_neg_le)
-qed
-
-lemma neg_le_0_iff_le [simp]: "(-a \<le> 0) = (0 \<le> (a::'a::pordered_ab_group_add))"
-by (subst neg_le_iff_le [symmetric], simp)
-
-lemma neg_0_le_iff_le [simp]: "(0 \<le> -a) = (a \<le> (0::'a::pordered_ab_group_add))"
-by (subst neg_le_iff_le [symmetric], simp)
-
-lemma neg_less_iff_less [simp]: "(-b < -a) = (a < (b::'a::pordered_ab_group_add))"
-
-lemma neg_less_0_iff_less [simp]: "(-a < 0) = (0 < (a::'a::pordered_ab_group_add))"
-by (subst neg_less_iff_less [symmetric], simp)
-
-lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::pordered_ab_group_add))"
-by (subst neg_less_iff_less [symmetric], simp)
-
-text{*The next several equations can make the simplifier loop!*}
-
-lemma less_minus_iff: "(a < - b) = (b < - (a::'a::pordered_ab_group_add))"
-proof -
-  have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
-  thus ?thesis by simp
-qed
-
-lemma minus_less_iff: "(- a < b) = (- b < (a::'a::pordered_ab_group_add))"
-proof -
-  have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
-  thus ?thesis by simp
-qed
-
-lemma le_minus_iff: "(a \<le> - b) = (b \<le> - (a::'a::pordered_ab_group_add))"
-proof -
-  have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)
-  have "(- (- a) <= -b) = (b <= - a)"
-    apply (auto simp only: order_le_less)
-    apply (drule mm)
-    apply (simp_all)
-    apply (drule mm[simplified], assumption)
-    done
-  then show ?thesis by simp
-qed
-
-lemma minus_le_iff: "(- a \<le> b) = (- b \<le> (a::'a::pordered_ab_group_add))"
-by (auto simp add: order_le_less minus_less_iff)
-
-lemma add_diff_eq: "a + (b - c) = (a + b) - (c::'a::ab_group_add)"
-
-lemma diff_add_eq: "(a - b) + c = (a + c) - (b::'a::ab_group_add)"
-
-lemma diff_eq_eq: "(a-b = c) = (a = c + (b::'a::ab_group_add))"
-
-lemma eq_diff_eq: "(a = c-b) = (a + (b::'a::ab_group_add) = c)"
-
-lemma diff_diff_eq: "(a - b) - c = a - (b + (c::'a::ab_group_add))"
-
-lemma diff_diff_eq2: "a - (b - c) = (a + c) - (b::'a::ab_group_add)"
-
-
-
-text{*Further subtraction laws*}
-
-lemma less_iff_diff_less_0: "(a < b) = (a - b < (0::'a::pordered_ab_group_add))"
-proof -
-  have  "(a < b) = (a + (- b) < b + (-b))"
-  also have "... =  (a - b < 0)" by (simp add: diff_minus)
-  finally show ?thesis .
-qed
-
-lemma diff_less_eq: "(a-b < c) = (a < c + (b::'a::pordered_ab_group_add))"
-apply (subst less_iff_diff_less_0 [of a])
-apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
-done
-
-lemma less_diff_eq: "(a < c-b) = (a + (b::'a::pordered_ab_group_add) < c)"
-apply (subst less_iff_diff_less_0 [of "a+b"])
-apply (subst less_iff_diff_less_0 [of a])
-done
-
-lemma diff_le_eq: "(a-b \<le> c) = (a \<le> c + (b::'a::pordered_ab_group_add))"
-
-lemma le_diff_eq: "(a \<le> c-b) = (a + (b::'a::pordered_ab_group_add) \<le> c)"
-
-text{*This list of rewrites simplifies (in)equalities by bringing subtractions
-  to the top and then moving negative terms to the other side.
-lemmas compare_rls =
-       diff_minus [symmetric]
-       diff_less_eq less_diff_eq diff_le_eq le_diff_eq
-       diff_eq_eq eq_diff_eq

subsection {* Support for reasoning about signs *}

@@ -657,14 +670,6 @@
done

-subsection{*Lemmas for the @{text cancel_numerals} simproc*}
-
-lemma eq_iff_diff_eq_0: "(a = b) = (a-b = (0::'a::ab_group_add))"
-
-lemma le_iff_diff_le_0: "(a \<le> b) = (a-b \<le> (0::'a::pordered_ab_group_add))"
-

subsection {* Lattice Ordered (Abelian) Groups *}

@@ -979,17 +984,14 @@
lemma nprt_neg: "nprt (-x) = - pprt x"

-lemma iff2imp: "(A=B) \<Longrightarrow> (A \<Longrightarrow> B)"
-by (simp)
-
lemma abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> abs a = (a::'a::lordered_ab_group_abs)"
-by (simp add: iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_pprt_id] abs_prts)
+by (simp add: iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_pprt_id] abs_prts)

lemma abs_of_pos: "0 < (x::'a::lordered_ab_group_abs) ==> abs x = x";
by (rule abs_of_nonneg, rule order_less_imp_le);

lemma abs_of_nonpos [simp]: "a \<le> 0 \<Longrightarrow> abs a = -(a::'a::lordered_ab_group_abs)"
-by (simp add: iff2imp[OF le_zero_iff_zero_pprt] iff2imp[OF zero_le_iff_nprt_id] abs_prts)
+by (simp add: iffD1[OF le_zero_iff_zero_pprt] iffD1[OF zero_le_iff_nprt_id] abs_prts)

lemma abs_of_neg: "(x::'a::lordered_ab_group_abs) <  0 ==>
abs x = - x"
@@ -1139,6 +1141,24 @@
show ?thesis by (rule le_add_right_mono[OF 2 3])
qed

+  fixes i j k :: "'a\<Colon>pordered_ab_semigroup_add"
+  shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
+    and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
+    and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l"
+    and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
+
+  fixes i j k :: "'a\<Colon>pordered_cancel_ab_semigroup_add"
+  shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
+    and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
+    and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l"
+    and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l"
+    and "i < j \<and> k < l \<Longrightarrow> i + k < j + l"