src/HOL/OrderedGroup.thy
changeset 16775 c1b87ef4a1c3
parent 16417 9bc16273c2d4
child 17085 5b57f995a179
     1.1 --- a/src/HOL/OrderedGroup.thy	Tue Jul 12 12:49:46 2005 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Tue Jul 12 17:56:03 2005 +0200
     1.3 @@ -1,6 +1,7 @@
     1.4  (*  Title:   HOL/OrderedGroup.thy
     1.5      ID:      $Id$
     1.6 -    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel
     1.7 +    Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
     1.8 +             with contributions by Jeremy Avigad
     1.9  *)
    1.10  
    1.11  header {* Ordered Groups *}
    1.12 @@ -466,6 +467,72 @@
    1.13         diff_less_eq less_diff_eq diff_le_eq le_diff_eq
    1.14         diff_eq_eq eq_diff_eq
    1.15  
    1.16 +subsection {* Support for reasoning about signs *}
    1.17 +
    1.18 +lemma add_pos_pos: "0 < 
    1.19 +    (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) 
    1.20 +      ==> 0 < y ==> 0 < x + y"
    1.21 +apply (subgoal_tac "0 + 0 < x + y")
    1.22 +apply simp
    1.23 +apply (erule add_less_le_mono)
    1.24 +apply (erule order_less_imp_le)
    1.25 +done
    1.26 +
    1.27 +lemma add_pos_nonneg: "0 < 
    1.28 +    (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) 
    1.29 +      ==> 0 <= y ==> 0 < x + y"
    1.30 +apply (subgoal_tac "0 + 0 < x + y")
    1.31 +apply simp
    1.32 +apply (erule add_less_le_mono, assumption)
    1.33 +done
    1.34 +
    1.35 +lemma add_nonneg_pos: "0 <= 
    1.36 +    (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) 
    1.37 +      ==> 0 < y ==> 0 < x + y"
    1.38 +apply (subgoal_tac "0 + 0 < x + y")
    1.39 +apply simp
    1.40 +apply (erule add_le_less_mono, assumption)
    1.41 +done
    1.42 +
    1.43 +lemma add_nonneg_nonneg: "0 <= 
    1.44 +    (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) 
    1.45 +      ==> 0 <= y ==> 0 <= x + y"
    1.46 +apply (subgoal_tac "0 + 0 <= x + y")
    1.47 +apply simp
    1.48 +apply (erule add_mono, assumption)
    1.49 +done
    1.50 +
    1.51 +lemma add_neg_neg: "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add})
    1.52 +    < 0 ==> y < 0 ==> x + y < 0"
    1.53 +apply (subgoal_tac "x + y < 0 + 0")
    1.54 +apply simp
    1.55 +apply (erule add_less_le_mono)
    1.56 +apply (erule order_less_imp_le)
    1.57 +done
    1.58 +
    1.59 +lemma add_neg_nonpos: 
    1.60 +    "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) < 0 
    1.61 +      ==> y <= 0 ==> x + y < 0"
    1.62 +apply (subgoal_tac "x + y < 0 + 0")
    1.63 +apply simp
    1.64 +apply (erule add_less_le_mono, assumption)
    1.65 +done
    1.66 +
    1.67 +lemma add_nonpos_neg: 
    1.68 +    "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) <= 0 
    1.69 +      ==> y < 0 ==> x + y < 0"
    1.70 +apply (subgoal_tac "x + y < 0 + 0")
    1.71 +apply simp
    1.72 +apply (erule add_le_less_mono, assumption)
    1.73 +done
    1.74 +
    1.75 +lemma add_nonpos_nonpos: 
    1.76 +    "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) <= 0 
    1.77 +      ==> y <= 0 ==> x + y <= 0"
    1.78 +apply (subgoal_tac "x + y <= 0 + 0")
    1.79 +apply simp
    1.80 +apply (erule add_mono, assumption)
    1.81 +done
    1.82  
    1.83  subsection{*Lemmas for the @{text cancel_numerals} simproc*}
    1.84  
    1.85 @@ -702,16 +769,6 @@
    1.86    show ?thesis by (simp add: abs_lattice join_eq_if)
    1.87  qed
    1.88  
    1.89 -lemma abs_eq [simp]:
    1.90 -  fixes a :: "'a::{lordered_ab_group_abs, linorder}"
    1.91 -  shows  "0 \<le> a ==> abs a = a"
    1.92 -by (simp add: abs_if_lattice linorder_not_less [symmetric]) 
    1.93 -
    1.94 -lemma abs_minus_eq [simp]: 
    1.95 -  fixes a :: "'a::{lordered_ab_group_abs, linorder}"
    1.96 -  shows "a < 0 ==> abs a = -a"
    1.97 -by (simp add: abs_if_lattice linorder_not_less [symmetric])
    1.98 -
    1.99  lemma abs_ge_zero[simp]: "0 \<le> abs (a::'a::lordered_ab_group_abs)"
   1.100  proof -
   1.101    have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice meet_join_le)
   1.102 @@ -800,12 +857,19 @@
   1.103  lemma iff2imp: "(A=B) \<Longrightarrow> (A \<Longrightarrow> B)"
   1.104  by (simp)
   1.105  
   1.106 -lemma imp_abs_id: "0 \<le> a \<Longrightarrow> abs a = (a::'a::lordered_ab_group_abs)"
   1.107 +lemma abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> abs a = (a::'a::lordered_ab_group_abs)"
   1.108  by (simp add: iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_pprt_id] abs_prts)
   1.109  
   1.110 -lemma imp_abs_neg_id: "a \<le> 0 \<Longrightarrow> abs a = -(a::'a::lordered_ab_group_abs)"
   1.111 +lemma abs_of_pos: "0 < (x::'a::lordered_ab_group_abs) ==> abs x = x";
   1.112 +by (rule abs_of_nonneg, rule order_less_imp_le);
   1.113 +
   1.114 +lemma abs_of_nonpos [simp]: "a \<le> 0 \<Longrightarrow> abs a = -(a::'a::lordered_ab_group_abs)"
   1.115  by (simp add: iff2imp[OF le_zero_iff_zero_pprt] iff2imp[OF zero_le_iff_nprt_id] abs_prts)
   1.116  
   1.117 +lemma abs_of_neg: "(x::'a::lordered_ab_group_abs) <  0 ==> 
   1.118 +  abs x = - x"
   1.119 +by (rule abs_of_nonpos, rule order_less_imp_le)
   1.120 +
   1.121  lemma abs_leI: "[|a \<le> b; -a \<le> b|] ==> abs a \<le> (b::'a::lordered_ab_group_abs)"
   1.122  by (simp add: abs_lattice join_imp_le)
   1.123  
   1.124 @@ -847,6 +911,36 @@
   1.125    with g[symmetric] show ?thesis by simp
   1.126  qed
   1.127  
   1.128 +lemma abs_triangle_ineq2: "abs (a::'a::lordered_ab_group_abs) - 
   1.129 +    abs b <= abs (a - b)"
   1.130 +  apply (simp add: compare_rls)
   1.131 +  apply (subgoal_tac "abs a = abs (a - b + b)")
   1.132 +  apply (erule ssubst)
   1.133 +  apply (rule abs_triangle_ineq)
   1.134 +  apply (rule arg_cong);back;
   1.135 +  apply (simp add: compare_rls)
   1.136 +done
   1.137 +
   1.138 +lemma abs_triangle_ineq3: 
   1.139 +    "abs(abs (a::'a::lordered_ab_group_abs) - abs b) <= abs (a - b)"
   1.140 +  apply (subst abs_le_iff)
   1.141 +  apply auto
   1.142 +  apply (rule abs_triangle_ineq2)
   1.143 +  apply (subst abs_minus_commute)
   1.144 +  apply (rule abs_triangle_ineq2)
   1.145 +done
   1.146 +
   1.147 +lemma abs_triangle_ineq4: "abs ((a::'a::lordered_ab_group_abs) - b) <= 
   1.148 +    abs a + abs b"
   1.149 +proof -;
   1.150 +  have "abs(a - b) = abs(a + - b)"
   1.151 +    by (subst diff_minus, rule refl)
   1.152 +  also have "... <= abs a + abs (- b)"
   1.153 +    by (rule abs_triangle_ineq)
   1.154 +  finally show ?thesis
   1.155 +    by simp
   1.156 +qed
   1.157 +
   1.158  lemma abs_diff_triangle_ineq:
   1.159       "\<bar>(a::'a::lordered_ab_group_abs) + b - (c+d)\<bar> \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>"
   1.160  proof -
   1.161 @@ -927,14 +1021,6 @@
   1.162    show ?thesis by (rule le_add_right_mono[OF 2 3])
   1.163  qed
   1.164  
   1.165 -lemma abs_of_ge_0: "0 <= (y::'a::lordered_ab_group_abs) \<Longrightarrow> abs y = y"
   1.166 -proof -
   1.167 -  assume 1:"0 <= y"
   1.168 -  have 2:"-y <= 0" by (simp add: 1)
   1.169 -  from 1 2 have 3:"-y <= y" by (simp only:)
   1.170 -  show ?thesis by (simp add: abs_lattice ge_imp_join_eq[OF 3])
   1.171 -qed
   1.172 -
   1.173  ML {*
   1.174  val add_zero_left = thm"add_0";
   1.175  val add_zero_right = thm"add_0_right";
   1.176 @@ -1068,8 +1154,8 @@
   1.177  val le_zero_iff_pprt_id = thm "le_zero_iff_pprt_id";
   1.178  val zero_le_iff_nprt_id = thm "zero_le_iff_nprt_id";
   1.179  val iff2imp = thm "iff2imp";
   1.180 -val imp_abs_id = thm "imp_abs_id";
   1.181 -val imp_abs_neg_id = thm "imp_abs_neg_id";
   1.182 +(* val imp_abs_id = thm "imp_abs_id";
   1.183 +val imp_abs_neg_id = thm "imp_abs_neg_id"; *)
   1.184  val abs_leI = thm "abs_leI";
   1.185  val le_minus_self_iff = thm "le_minus_self_iff";
   1.186  val minus_le_self_iff = thm "minus_le_self_iff";