# HG changeset patch
# User haftmann
# Date 1192692057 -7200
# Node ID c2ec5e589d78659014180e8145065020ca5420d5
# Parent  a50b36401c616468e2ac87e1e115647034eddc11
continued localization

diff -r a50b36401c61 -r c2ec5e589d78 src/HOL/OrderedGroup.thy
--- 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)"
   by (rule mk_left_commute [of "plus", OF add_assoc add_commute])
-  (*FIXME term_check*)
 
 theorems add_ac = add_assoc add_commute add_left_commute
 
@@ -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"
   by (simp add: diff_minus add_commute)
 
+lemma add_diff_eq: "a + (b - c) = (a + b) - c"
+  by (simp add: diff_minus add_ac)
+
+lemma diff_add_eq: "(a - b) + c = (a + c) - b"
+  by (simp add: diff_minus add_ac)
+
+lemma diff_eq_eq: "a - b = c \<longleftrightarrow> a = c + b"
+  by (auto simp add: diff_minus add_assoc)
+
+lemma eq_diff_eq: "a = c - b \<longleftrightarrow> a + b = c"
+  by (auto simp add: diff_minus add_assoc)
+
+lemma diff_diff_eq: "(a - b) - c = a - (b + c)"
+  by (simp add: diff_minus add_ac)
+
+lemma diff_diff_eq2: "a - (b - c) = (a + c) - b"
+  by (simp add: diff_minus add_ac)
+
+lemma diff_add_cancel: "a - b + b = a"
+  by (simp add: diff_minus add_ac)
+
+lemma add_diff_cancel: "a + b - b = a"
+  by (simp add: diff_minus add_ac)
+
+lemmas compare_rls =
+       diff_minus [symmetric]
+       add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
+       diff_eq_eq eq_diff_eq
+
+lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
+  by (simp add: compare_rls)
+
 end
 
 subsection {* (Partially) Ordered Groups *} 
@@ -368,6 +398,14 @@
   "a + c \<le> b + c \<Longrightarrow> a \<le> b"
   by simp
 
+lemma max_add_distrib_left:
+  "max x y + z = max (x + z) (y + z)"
+  unfolding max_def by auto
+
+lemma min_add_distrib_left:
+  "min x y + z = min (x + z) (y + z)"
+  unfolding min_def by auto
+
 end
 
 class pordered_ab_group_add =
@@ -388,6 +426,132 @@
 
 end
 
+context pordered_ab_group_add
+begin
+
+lemma max_diff_distrib_left:
+  shows "max x y - z = max (x - z) (y - z)"
+  by (simp add: diff_minus, rule max_add_distrib_left) 
+
+lemma min_diff_distrib_left:
+  shows "min x y - z = min (x - z) (y - z)"
+  by (simp add: diff_minus, rule min_add_distrib_left) 
+
+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)"
+    by (rule add_right_mono) 
+  thus ?thesis
+    by (simp add: add_assoc)
+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))"  
+    by (simp only: add_less_cancel_right)
+  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])
+apply (simp add: diff_minus add_ac)
+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])
+apply (simp add: diff_minus add_ac)
+done
+
+lemma diff_le_eq: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
+  by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel)
+
+lemma le_diff_eq: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
+  by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
+
+lemmas compare_rls =
+       diff_minus [symmetric]
+       add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
+       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.
+  Use with @{text add_ac}*}
+lemmas (in -) compare_rls =
+       diff_minus [symmetric]
+       add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
+       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"
+  by (simp add: compare_rls)
+
+end
+
 class ordered_ab_semigroup_add =
   linorder + pordered_ab_semigroup_add
 
@@ -416,17 +580,7 @@
   qed
 qed
 
--- {* FIXME continue localization here *}
-
-lemma max_add_distrib_left:
-  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
-  shows  "(max x y) + z = max (x+z) (y+z)"
-by (rule max_of_mono [THEN sym], rule add_le_cancel_right)
-
-lemma min_add_distrib_left:
-  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
-  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 *}
 
 lemma add_increasing:
   fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
@@ -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:
-  fixes z :: "'a::pordered_ab_group_add"
-  shows  "(max x y) - z = max (x-z) (y-z)"
-by (simp add: diff_minus, rule max_add_distrib_left) 
-
-lemma min_diff_distrib_left:
-  fixes z :: "'a::pordered_ab_group_add"
-  shows  "(min x y) - z = min (x-z) (y-z)"
-by (simp add: diff_minus, rule min_add_distrib_left) 
-
-
-subsection {* Ordering Rules for Unary Minus *}
-
-lemma le_imp_neg_le:
-  assumes "a \<le> (b::'a::{pordered_ab_semigroup_add_imp_le, ab_group_add})" 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)"
-    by (rule add_right_mono) 
-  thus ?thesis
-    by (simp add: add_assoc)
-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))"
-by (force simp add: order_less_le) 
-
-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)"
-by (simp add: diff_minus add_ac)
-
-lemma diff_add_eq: "(a - b) + c = (a + c) - (b::'a::ab_group_add)"
-by (simp add: diff_minus add_ac)
-
-lemma diff_eq_eq: "(a-b = c) = (a = c + (b::'a::ab_group_add))"
-by (auto simp add: diff_minus add_assoc)
-
-lemma eq_diff_eq: "(a = c-b) = (a + (b::'a::ab_group_add) = c)"
-by (auto simp add: diff_minus add_assoc)
-
-lemma diff_diff_eq: "(a - b) - c = a - (b + (c::'a::ab_group_add))"
-by (simp add: diff_minus add_ac)
-
-lemma diff_diff_eq2: "a - (b - c) = (a + c) - (b::'a::ab_group_add)"
-by (simp add: diff_minus add_ac)
-
-lemma diff_add_cancel: "a - b + b = (a::'a::ab_group_add)"
-by (simp add: diff_minus add_ac)
-
-lemma add_diff_cancel: "a + b - b = (a::'a::ab_group_add)"
-by (simp add: diff_minus add_ac)
-
-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))"  
-    by (simp only: add_less_cancel_right)
-  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])
-apply (simp add: diff_minus add_ac)
-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])
-apply (simp add: diff_minus add_ac)
-done
-
-lemma diff_le_eq: "(a-b \<le> c) = (a \<le> c + (b::'a::pordered_ab_group_add))"
-by (auto simp add: order_le_less diff_less_eq diff_add_cancel add_diff_cancel)
-
-lemma le_diff_eq: "(a \<le> c-b) = (a + (b::'a::pordered_ab_group_add) \<le> c)"
-by (auto simp add: order_le_less less_diff_eq diff_add_cancel add_diff_cancel)
-
-text{*This list of rewrites simplifies (in)equalities by bringing subtractions
-  to the top and then moving negative terms to the other side.
-  Use with @{text add_ac}*}
-lemmas compare_rls =
-       diff_minus [symmetric]
-       add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
-       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 @@
 apply (erule add_mono, assumption)
 done
 
-subsection{*Lemmas for the @{text cancel_numerals} simproc*}
-
-lemma eq_iff_diff_eq_0: "(a = b) = (a-b = (0::'a::ab_group_add))"
-by (simp add: compare_rls)
-
-lemma le_iff_diff_le_0: "(a \<le> b) = (a-b \<le> (0::'a::pordered_ab_group_add))"
-by (simp add: compare_rls)
-
 
 subsection {* Lattice Ordered (Abelian) Groups *}
 
@@ -979,17 +984,14 @@
 lemma nprt_neg: "nprt (-x) = - pprt x"
   by (simp add: pprt_def nprt_def)
 
-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
 
+lemma add_mono_thms_ordered_semiring [noatp]:
+  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"
+by (rule add_mono, clarify+)+
+
+lemma add_mono_thms_ordered_field [noatp]:
+  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"
+by (auto intro: add_strict_right_mono add_strict_left_mono
+  add_less_le_mono add_le_less_mono add_strict_mono)
+
 
 subsection {* Tools setup *}
 
@@ -1187,7 +1207,7 @@
   
 val thy_ref = Theory.check_thy @{theory};
 
-val T = TFree("'a", ["OrderedGroup.ab_group_add"]);
+val T = @{typ "'a\<Colon>ab_group_add"};
 
 val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];