src/HOL/OrderedGroup.thy
 author urbanc Tue Jun 05 09:56:19 2007 +0200 (2007-06-05) changeset 23243 a37d3e6e8323 parent 23181 f52b555f8141 child 23389 aaca6a8e5414 permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
     1 (*  Title:   HOL/OrderedGroup.thy

     2     ID:      $Id$

     3     Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,

     4              with contributions by Jeremy Avigad

     5 *)

     6

     7 header {* Ordered Groups *}

     8

     9 theory OrderedGroup

    10 imports Lattices

    11 uses "~~/src/Provers/Arith/abel_cancel.ML"

    12 begin

    13

    14 text {*

    15   The theory of partially ordered groups is taken from the books:

    16   \begin{itemize}

    17   \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979

    18   \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963

    19   \end{itemize}

    20   Most of the used notions can also be looked up in

    21   \begin{itemize}

    22   \item \url{http://www.mathworld.com} by Eric Weisstein et. al.

    23   \item \emph{Algebra I} by van der Waerden, Springer.

    24   \end{itemize}

    25 *}

    26

    27 subsection {* Semigroups and Monoids *}

    28

    29 class semigroup_add = plus +

    30   assumes add_assoc: "(a \<^loc>+ b) \<^loc>+ c = a \<^loc>+ (b \<^loc>+ c)"

    31

    32 class ab_semigroup_add = semigroup_add +

    33   assumes add_commute: "a \<^loc>+ b = b \<^loc>+ a"

    34

    35 lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ab_semigroup_add))"

    36   by (rule mk_left_commute [of "op +", OF add_assoc add_commute])

    37

    38 theorems add_ac = add_assoc add_commute add_left_commute

    39

    40 class semigroup_mult = times +

    41   assumes mult_assoc: "(a \<^loc>* b) \<^loc>* c = a \<^loc>* (b \<^loc>* c)"

    42

    43 class ab_semigroup_mult = semigroup_mult +

    44   assumes mult_commute: "a \<^loc>* b = b \<^loc>* a"

    45 begin

    46

    47 lemma mult_left_commute: "a \<^loc>* (b \<^loc>* c) = b \<^loc>* (a \<^loc>* c)"

    48   by (rule mk_left_commute [of "op \<^loc>*", OF mult_assoc mult_commute])

    49

    50 end

    51

    52 theorems mult_ac = mult_assoc mult_commute mult_left_commute

    53

    54 class monoid_add = zero + semigroup_add +

    55   assumes add_0_left [simp]: "\<^loc>0 \<^loc>+ a = a" and add_0_right [simp]: "a \<^loc>+ \<^loc>0 = a"

    56

    57 class comm_monoid_add = zero + ab_semigroup_add +

    58   assumes add_0: "\<^loc>0 \<^loc>+ a = a"

    59

    60 instance comm_monoid_add < monoid_add

    61 by intro_classes (insert comm_monoid_add_class.zero_plus.add_0, simp_all add: add_commute, auto)

    62

    63 class monoid_mult = one + semigroup_mult +

    64   assumes mult_1_left [simp]: "\<^loc>1 \<^loc>* a  = a"

    65   assumes mult_1_right [simp]: "a \<^loc>* \<^loc>1 = a"

    66

    67 class comm_monoid_mult = one + ab_semigroup_mult +

    68   assumes mult_1: "\<^loc>1 \<^loc>* a = a"

    69

    70 instance comm_monoid_mult \<subseteq> monoid_mult

    71   by intro_classes (insert mult_1, simp_all add: mult_commute, auto)

    72

    73 class cancel_semigroup_add = semigroup_add +

    74   assumes add_left_imp_eq: "a \<^loc>+ b = a \<^loc>+ c \<Longrightarrow> b = c"

    75   assumes add_right_imp_eq: "b \<^loc>+ a = c \<^loc>+ a \<Longrightarrow> b = c"

    76

    77 class cancel_ab_semigroup_add = ab_semigroup_add +

    78   assumes add_imp_eq: "a \<^loc>+ b = a \<^loc>+ c \<Longrightarrow> b = c"

    79

    80 instance cancel_ab_semigroup_add \<subseteq> cancel_semigroup_add

    81 proof intro_classes

    82   fix a b c :: 'a

    83   assume "a + b = a + c"

    84   then show "b = c" by (rule add_imp_eq)

    85 next

    86   fix a b c :: 'a

    87   assume "b + a = c + a"

    88   then have "a + b = a + c" by (simp only: add_commute)

    89   then show "b = c" by (rule add_imp_eq)

    90 qed

    91

    92 lemma add_left_cancel [simp]:

    93   "a + b = a + c \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"

    94   by (blast dest: add_left_imp_eq)

    95

    96 lemma add_right_cancel [simp]:

    97   "b + a = c + a \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"

    98   by (blast dest: add_right_imp_eq)

    99

   100 subsection {* Groups *}

   101

   102 class ab_group_add = minus + comm_monoid_add +

   103   assumes ab_left_minus: "uminus a \<^loc>+ a = \<^loc>0"

   104   assumes ab_diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"

   105

   106 class group_add = minus + monoid_add +

   107   assumes left_minus [simp]: "uminus a \<^loc>+ a = \<^loc>0"

   108   assumes diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"

   109

   110 instance ab_group_add < group_add

   111 by intro_classes (simp_all add: ab_left_minus ab_diff_minus)

   112

   113 instance ab_group_add \<subseteq> cancel_ab_semigroup_add

   114 proof intro_classes

   115   fix a b c :: 'a

   116   assume "a + b = a + c"

   117   then have "uminus a + a + b = uminus a + a + c" unfolding add_assoc by simp

   118   then show "b = c" by simp

   119 qed

   120

   121 lemma minus_add_cancel: "-(a::'a::group_add) + (a+b) = b"

   122 by(simp add:add_assoc[symmetric])

   123

   124 lemma minus_zero[simp]: "-(0::'a::group_add) = 0"

   125 proof -

   126   have "-(0::'a::group_add) = - 0 + (0+0)" by(simp only: add_0_right)

   127   also have "\<dots> = 0" by(rule minus_add_cancel)

   128   finally show ?thesis .

   129 qed

   130

   131 lemma minus_minus[simp]: "- (-(a::'a::group_add)) = a"

   132 proof -

   133   have "-(-a) = -(-a) + (-a + a)" by simp

   134   also have "\<dots> = a" by(rule minus_add_cancel)

   135   finally show ?thesis .

   136 qed

   137

   138 lemma right_minus[simp]: "a + - a = (0::'a::group_add)"

   139 proof -

   140   have "a + -a = -(-a) + -a" by simp

   141   also have "\<dots> = 0" thm group_add.left_minus by(rule left_minus)

   142   finally show ?thesis .

   143 qed

   144

   145 lemma right_minus_eq: "(a - b = 0) = (a = (b::'a::group_add))"

   146 proof

   147   assume "a - b = 0"

   148   have "a = (a - b) + b" by (simp add:diff_minus add_assoc)

   149   also have "\<dots> = b" using a - b = 0 by simp

   150   finally show "a = b" .

   151 next

   152   assume "a = b" thus "a - b = 0" by (simp add: diff_minus)

   153 qed

   154

   155 lemma equals_zero_I: assumes "a+b = 0" shows "-a = (b::'a::group_add)"

   156 proof -

   157   have "- a = -a + (a+b)" using assms by simp

   158   also have "\<dots> = b" by(simp add:add_assoc[symmetric])

   159   finally show ?thesis .

   160 qed

   161

   162 lemma diff_self[simp]: "(a::'a::group_add) - a = 0"

   163 by(simp add: diff_minus)

   164

   165 lemma diff_0 [simp]: "(0::'a::group_add) - a = -a"

   166 by (simp add: diff_minus)

   167

   168 lemma diff_0_right [simp]: "a - (0::'a::group_add) = a"

   169 by (simp add: diff_minus)

   170

   171 lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::group_add)"

   172 by (simp add: diff_minus)

   173

   174 lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::group_add))"

   175 proof

   176   assume "- a = - b"

   177   hence "- (- a) = - (- b)"

   178     by simp

   179   thus "a=b" by simp

   180 next

   181   assume "a=b"

   182   thus "-a = -b" by simp

   183 qed

   184

   185 lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::group_add))"

   186 by (subst neg_equal_iff_equal [symmetric], simp)

   187

   188 lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::group_add))"

   189 by (subst neg_equal_iff_equal [symmetric], simp)

   190

   191 text{*The next two equations can make the simplifier loop!*}

   192

   193 lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::group_add))"

   194 proof -

   195   have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal)

   196   thus ?thesis by (simp add: eq_commute)

   197 qed

   198

   199 lemma minus_equation_iff: "(- a = b) = (- (b::'a::group_add) = a)"

   200 proof -

   201   have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal)

   202   thus ?thesis by (simp add: eq_commute)

   203 qed

   204

   205 lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ab_group_add)"

   206 apply (rule equals_zero_I)

   207 apply (simp add: add_ac)

   208 done

   209

   210 lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ab_group_add)"

   211 by (simp add: diff_minus add_commute)

   212

   213 subsection {* (Partially) Ordered Groups *}

   214

   215 class pordered_ab_semigroup_add = order + ab_semigroup_add +

   216   assumes add_left_mono: "a \<sqsubseteq> b \<Longrightarrow> c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b"

   217

   218 class pordered_cancel_ab_semigroup_add =

   219   pordered_ab_semigroup_add + cancel_ab_semigroup_add

   220

   221 class pordered_ab_semigroup_add_imp_le = pordered_cancel_ab_semigroup_add +

   222   assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b \<Longrightarrow> a \<sqsubseteq> b"

   223

   224 class pordered_ab_group_add = ab_group_add + pordered_ab_semigroup_add

   225

   226 instance pordered_ab_group_add \<subseteq> pordered_ab_semigroup_add_imp_le

   227 proof

   228   fix a b c :: 'a

   229   assume "c + a \<le> c + b"

   230   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)

   231   hence "((-c) + c) + a \<le> ((-c) + c) + b" by (simp only: add_assoc)

   232   thus "a \<le> b" by simp

   233 qed

   234

   235 class ordered_cancel_ab_semigroup_add = pordered_cancel_ab_semigroup_add + linorder

   236

   237 instance ordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add_imp_le

   238 proof

   239   fix a b c :: 'a

   240   assume le: "c + a <= c + b"

   241   show "a <= b"

   242   proof (rule ccontr)

   243     assume w: "~ a \<le> b"

   244     hence "b <= a" by (simp add: linorder_not_le)

   245     hence le2: "c+b <= c+a" by (rule add_left_mono)

   246     have "a = b"

   247       apply (insert le)

   248       apply (insert le2)

   249       apply (drule order_antisym, simp_all)

   250       done

   251     with w  show False

   252       by (simp add: linorder_not_le [symmetric])

   253   qed

   254 qed

   255

   256 lemma add_right_mono: "a \<le> (b::'a::pordered_ab_semigroup_add) ==> a + c \<le> b + c"

   257   by (simp add: add_commute [of _ c] add_left_mono)

   258

   259 text {* non-strict, in both arguments *}

   260 lemma add_mono:

   261      "[|a \<le> b;  c \<le> d|] ==> a + c \<le> b + (d::'a::pordered_ab_semigroup_add)"

   262   apply (erule add_right_mono [THEN order_trans])

   263   apply (simp add: add_commute add_left_mono)

   264   done

   265

   266 lemma add_strict_left_mono:

   267      "a < b ==> c + a < c + (b::'a::pordered_cancel_ab_semigroup_add)"

   268  by (simp add: order_less_le add_left_mono)

   269

   270 lemma add_strict_right_mono:

   271      "a < b ==> a + c < b + (c::'a::pordered_cancel_ab_semigroup_add)"

   272  by (simp add: add_commute [of _ c] add_strict_left_mono)

   273

   274 text{*Strict monotonicity in both arguments*}

   275 lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)"

   276 apply (erule add_strict_right_mono [THEN order_less_trans])

   277 apply (erule add_strict_left_mono)

   278 done

   279

   280 lemma add_less_le_mono:

   281      "[| a<b; c\<le>d |] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)"

   282 apply (erule add_strict_right_mono [THEN order_less_le_trans])

   283 apply (erule add_left_mono)

   284 done

   285

   286 lemma add_le_less_mono:

   287      "[| a\<le>b; c<d |] ==> a + c < b + (d::'a::pordered_cancel_ab_semigroup_add)"

   288 apply (erule add_right_mono [THEN order_le_less_trans])

   289 apply (erule add_strict_left_mono)

   290 done

   291

   292 lemma add_less_imp_less_left:

   293       assumes less: "c + a < c + b"  shows "a < (b::'a::pordered_ab_semigroup_add_imp_le)"

   294 proof -

   295   from less have le: "c + a <= c + b" by (simp add: order_le_less)

   296   have "a <= b"

   297     apply (insert le)

   298     apply (drule add_le_imp_le_left)

   299     by (insert le, drule add_le_imp_le_left, assumption)

   300   moreover have "a \<noteq> b"

   301   proof (rule ccontr)

   302     assume "~(a \<noteq> b)"

   303     then have "a = b" by simp

   304     then have "c + a = c + b" by simp

   305     with less show "False"by simp

   306   qed

   307   ultimately show "a < b" by (simp add: order_le_less)

   308 qed

   309

   310 lemma add_less_imp_less_right:

   311       "a + c < b + c ==> a < (b::'a::pordered_ab_semigroup_add_imp_le)"

   312 apply (rule add_less_imp_less_left [of c])

   313 apply (simp add: add_commute)

   314 done

   315

   316 lemma add_less_cancel_left [simp]:

   317     "(c+a < c+b) = (a < (b::'a::pordered_ab_semigroup_add_imp_le))"

   318 by (blast intro: add_less_imp_less_left add_strict_left_mono)

   319

   320 lemma add_less_cancel_right [simp]:

   321     "(a+c < b+c) = (a < (b::'a::pordered_ab_semigroup_add_imp_le))"

   322 by (blast intro: add_less_imp_less_right add_strict_right_mono)

   323

   324 lemma add_le_cancel_left [simp]:

   325     "(c+a \<le> c+b) = (a \<le> (b::'a::pordered_ab_semigroup_add_imp_le))"

   326 by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono)

   327

   328 lemma add_le_cancel_right [simp]:

   329     "(a+c \<le> b+c) = (a \<le> (b::'a::pordered_ab_semigroup_add_imp_le))"

   330 by (simp add: add_commute[of a c] add_commute[of b c])

   331

   332 lemma add_le_imp_le_right:

   333       "a + c \<le> b + c ==> a \<le> (b::'a::pordered_ab_semigroup_add_imp_le)"

   334 by simp

   335

   336 lemma add_increasing:

   337   fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"

   338   shows  "[|0\<le>a; b\<le>c|] ==> b \<le> a + c"

   339 by (insert add_mono [of 0 a b c], simp)

   340

   341 lemma add_increasing2:

   342   fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"

   343   shows  "[|0\<le>c; b\<le>a|] ==> b \<le> a + c"

   344 by (simp add:add_increasing add_commute[of a])

   345

   346 lemma add_strict_increasing:

   347   fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"

   348   shows "[|0<a; b\<le>c|] ==> b < a + c"

   349 by (insert add_less_le_mono [of 0 a b c], simp)

   350

   351 lemma add_strict_increasing2:

   352   fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"

   353   shows "[|0\<le>a; b<c|] ==> b < a + c"

   354 by (insert add_le_less_mono [of 0 a b c], simp)

   355

   356 lemma max_add_distrib_left:

   357   fixes z :: "'a::pordered_ab_semigroup_add_imp_le"

   358   shows  "(max x y) + z = max (x+z) (y+z)"

   359 by (rule max_of_mono [THEN sym], rule add_le_cancel_right)

   360

   361 lemma min_add_distrib_left:

   362   fixes z :: "'a::pordered_ab_semigroup_add_imp_le"

   363   shows  "(min x y) + z = min (x+z) (y+z)"

   364 by (rule min_of_mono [THEN sym], rule add_le_cancel_right)

   365

   366 lemma max_diff_distrib_left:

   367   fixes z :: "'a::pordered_ab_group_add"

   368   shows  "(max x y) - z = max (x-z) (y-z)"

   369 by (simp add: diff_minus, rule max_add_distrib_left)

   370

   371 lemma min_diff_distrib_left:

   372   fixes z :: "'a::pordered_ab_group_add"

   373   shows  "(min x y) - z = min (x-z) (y-z)"

   374 by (simp add: diff_minus, rule min_add_distrib_left)

   375

   376

   377 subsection {* Ordering Rules for Unary Minus *}

   378

   379 lemma le_imp_neg_le:

   380       assumes "a \<le> (b::'a::{pordered_ab_semigroup_add_imp_le, ab_group_add})" shows "-b \<le> -a"

   381 proof -

   382   have "-a+a \<le> -a+b"

   383     by (rule add_left_mono)

   384   hence "0 \<le> -a+b"

   385     by simp

   386   hence "0 + (-b) \<le> (-a + b) + (-b)"

   387     by (rule add_right_mono)

   388   thus ?thesis

   389     by (simp add: add_assoc)

   390 qed

   391

   392 lemma neg_le_iff_le [simp]: "(-b \<le> -a) = (a \<le> (b::'a::pordered_ab_group_add))"

   393 proof

   394   assume "- b \<le> - a"

   395   hence "- (- a) \<le> - (- b)"

   396     by (rule le_imp_neg_le)

   397   thus "a\<le>b" by simp

   398 next

   399   assume "a\<le>b"

   400   thus "-b \<le> -a" by (rule le_imp_neg_le)

   401 qed

   402

   403 lemma neg_le_0_iff_le [simp]: "(-a \<le> 0) = (0 \<le> (a::'a::pordered_ab_group_add))"

   404 by (subst neg_le_iff_le [symmetric], simp)

   405

   406 lemma neg_0_le_iff_le [simp]: "(0 \<le> -a) = (a \<le> (0::'a::pordered_ab_group_add))"

   407 by (subst neg_le_iff_le [symmetric], simp)

   408

   409 lemma neg_less_iff_less [simp]: "(-b < -a) = (a < (b::'a::pordered_ab_group_add))"

   410 by (force simp add: order_less_le)

   411

   412 lemma neg_less_0_iff_less [simp]: "(-a < 0) = (0 < (a::'a::pordered_ab_group_add))"

   413 by (subst neg_less_iff_less [symmetric], simp)

   414

   415 lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::pordered_ab_group_add))"

   416 by (subst neg_less_iff_less [symmetric], simp)

   417

   418 text{*The next several equations can make the simplifier loop!*}

   419

   420 lemma less_minus_iff: "(a < - b) = (b < - (a::'a::pordered_ab_group_add))"

   421 proof -

   422   have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)

   423   thus ?thesis by simp

   424 qed

   425

   426 lemma minus_less_iff: "(- a < b) = (- b < (a::'a::pordered_ab_group_add))"

   427 proof -

   428   have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)

   429   thus ?thesis by simp

   430 qed

   431

   432 lemma le_minus_iff: "(a \<le> - b) = (b \<le> - (a::'a::pordered_ab_group_add))"

   433 proof -

   434   have mm: "!! a (b::'a). (-(-a)) < -b \<Longrightarrow> -(-b) < -a" by (simp only: minus_less_iff)

   435   have "(- (- a) <= -b) = (b <= - a)"

   436     apply (auto simp only: order_le_less)

   437     apply (drule mm)

   438     apply (simp_all)

   439     apply (drule mm[simplified], assumption)

   440     done

   441   then show ?thesis by simp

   442 qed

   443

   444 lemma minus_le_iff: "(- a \<le> b) = (- b \<le> (a::'a::pordered_ab_group_add))"

   445 by (auto simp add: order_le_less minus_less_iff)

   446

   447 lemma add_diff_eq: "a + (b - c) = (a + b) - (c::'a::ab_group_add)"

   448 by (simp add: diff_minus add_ac)

   449

   450 lemma diff_add_eq: "(a - b) + c = (a + c) - (b::'a::ab_group_add)"

   451 by (simp add: diff_minus add_ac)

   452

   453 lemma diff_eq_eq: "(a-b = c) = (a = c + (b::'a::ab_group_add))"

   454 by (auto simp add: diff_minus add_assoc)

   455

   456 lemma eq_diff_eq: "(a = c-b) = (a + (b::'a::ab_group_add) = c)"

   457 by (auto simp add: diff_minus add_assoc)

   458

   459 lemma diff_diff_eq: "(a - b) - c = a - (b + (c::'a::ab_group_add))"

   460 by (simp add: diff_minus add_ac)

   461

   462 lemma diff_diff_eq2: "a - (b - c) = (a + c) - (b::'a::ab_group_add)"

   463 by (simp add: diff_minus add_ac)

   464

   465 lemma diff_add_cancel: "a - b + b = (a::'a::ab_group_add)"

   466 by (simp add: diff_minus add_ac)

   467

   468 lemma add_diff_cancel: "a + b - b = (a::'a::ab_group_add)"

   469 by (simp add: diff_minus add_ac)

   470

   471 text{*Further subtraction laws*}

   472

   473 lemma less_iff_diff_less_0: "(a < b) = (a - b < (0::'a::pordered_ab_group_add))"

   474 proof -

   475   have  "(a < b) = (a + (- b) < b + (-b))"

   476     by (simp only: add_less_cancel_right)

   477   also have "... =  (a - b < 0)" by (simp add: diff_minus)

   478   finally show ?thesis .

   479 qed

   480

   481 lemma diff_less_eq: "(a-b < c) = (a < c + (b::'a::pordered_ab_group_add))"

   482 apply (subst less_iff_diff_less_0 [of a])

   483 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])

   484 apply (simp add: diff_minus add_ac)

   485 done

   486

   487 lemma less_diff_eq: "(a < c-b) = (a + (b::'a::pordered_ab_group_add) < c)"

   488 apply (subst less_iff_diff_less_0 [of "a+b"])

   489 apply (subst less_iff_diff_less_0 [of a])

   490 apply (simp add: diff_minus add_ac)

   491 done

   492

   493 lemma diff_le_eq: "(a-b \<le> c) = (a \<le> c + (b::'a::pordered_ab_group_add))"

   494 by (auto simp add: order_le_less diff_less_eq diff_add_cancel add_diff_cancel)

   495

   496 lemma le_diff_eq: "(a \<le> c-b) = (a + (b::'a::pordered_ab_group_add) \<le> c)"

   497 by (auto simp add: order_le_less less_diff_eq diff_add_cancel add_diff_cancel)

   498

   499 text{*This list of rewrites simplifies (in)equalities by bringing subtractions

   500   to the top and then moving negative terms to the other side.

   501   Use with @{text add_ac}*}

   502 lemmas compare_rls =

   503        diff_minus [symmetric]

   504        add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2

   505        diff_less_eq less_diff_eq diff_le_eq le_diff_eq

   506        diff_eq_eq eq_diff_eq

   507

   508 subsection {* Support for reasoning about signs *}

   509

   510 lemma add_pos_pos: "0 <

   511     (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add})

   512       ==> 0 < y ==> 0 < x + y"

   513 apply (subgoal_tac "0 + 0 < x + y")

   514 apply simp

   515 apply (erule add_less_le_mono)

   516 apply (erule order_less_imp_le)

   517 done

   518

   519 lemma add_pos_nonneg: "0 <

   520     (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add})

   521       ==> 0 <= y ==> 0 < x + y"

   522 apply (subgoal_tac "0 + 0 < x + y")

   523 apply simp

   524 apply (erule add_less_le_mono, assumption)

   525 done

   526

   527 lemma add_nonneg_pos: "0 <=

   528     (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add})

   529       ==> 0 < y ==> 0 < x + y"

   530 apply (subgoal_tac "0 + 0 < x + y")

   531 apply simp

   532 apply (erule add_le_less_mono, assumption)

   533 done

   534

   535 lemma add_nonneg_nonneg: "0 <=

   536     (x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add})

   537       ==> 0 <= y ==> 0 <= x + y"

   538 apply (subgoal_tac "0 + 0 <= x + y")

   539 apply simp

   540 apply (erule add_mono, assumption)

   541 done

   542

   543 lemma add_neg_neg: "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add})

   544     < 0 ==> y < 0 ==> x + y < 0"

   545 apply (subgoal_tac "x + y < 0 + 0")

   546 apply simp

   547 apply (erule add_less_le_mono)

   548 apply (erule order_less_imp_le)

   549 done

   550

   551 lemma add_neg_nonpos:

   552     "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) < 0

   553       ==> y <= 0 ==> x + y < 0"

   554 apply (subgoal_tac "x + y < 0 + 0")

   555 apply simp

   556 apply (erule add_less_le_mono, assumption)

   557 done

   558

   559 lemma add_nonpos_neg:

   560     "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) <= 0

   561       ==> y < 0 ==> x + y < 0"

   562 apply (subgoal_tac "x + y < 0 + 0")

   563 apply simp

   564 apply (erule add_le_less_mono, assumption)

   565 done

   566

   567 lemma add_nonpos_nonpos:

   568     "(x::'a::{comm_monoid_add,pordered_cancel_ab_semigroup_add}) <= 0

   569       ==> y <= 0 ==> x + y <= 0"

   570 apply (subgoal_tac "x + y <= 0 + 0")

   571 apply simp

   572 apply (erule add_mono, assumption)

   573 done

   574

   575 subsection{*Lemmas for the @{text cancel_numerals} simproc*}

   576

   577 lemma eq_iff_diff_eq_0: "(a = b) = (a-b = (0::'a::ab_group_add))"

   578 by (simp add: compare_rls)

   579

   580 lemma le_iff_diff_le_0: "(a \<le> b) = (a-b \<le> (0::'a::pordered_ab_group_add))"

   581 by (simp add: compare_rls)

   582

   583

   584 subsection {* Lattice Ordered (Abelian) Groups *}

   585

   586 class lordered_ab_group_meet = pordered_ab_group_add + lower_semilattice

   587

   588 class lordered_ab_group_join = pordered_ab_group_add + upper_semilattice

   589

   590 class lordered_ab_group = pordered_ab_group_add + lattice

   591

   592 instance lordered_ab_group \<subseteq> lordered_ab_group_meet by default

   593 instance lordered_ab_group \<subseteq> lordered_ab_group_join by default

   594

   595 lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + (c::'a::{pordered_ab_group_add, lower_semilattice}))"

   596 apply (rule order_antisym)

   597 apply (simp_all add: le_infI)

   598 apply (rule add_le_imp_le_left [of "-a"])

   599 apply (simp only: add_assoc[symmetric], simp)

   600 apply rule

   601 apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+

   602 done

   603

   604 lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a+ (c::'a::{pordered_ab_group_add, upper_semilattice}))"

   605 apply (rule order_antisym)

   606 apply (rule add_le_imp_le_left [of "-a"])

   607 apply (simp only: add_assoc[symmetric], simp)

   608 apply rule

   609 apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+

   610 apply (rule le_supI)

   611 apply (simp_all)

   612 done

   613

   614 lemma add_inf_distrib_right: "inf a b + (c::'a::lordered_ab_group) = inf (a+c) (b+c)"

   615 proof -

   616   have "c + inf a b = inf (c+a) (c+b)" by (simp add: add_inf_distrib_left)

   617   thus ?thesis by (simp add: add_commute)

   618 qed

   619

   620 lemma add_sup_distrib_right: "sup a b + (c::'a::lordered_ab_group) = sup (a+c) (b+c)"

   621 proof -

   622   have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)

   623   thus ?thesis by (simp add: add_commute)

   624 qed

   625

   626 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left

   627

   628 lemma inf_eq_neg_sup: "inf a (b\<Colon>'a\<Colon>lordered_ab_group) = - sup (-a) (-b)"

   629 proof (rule inf_unique)

   630   fix a b :: 'a

   631   show "- sup (-a) (-b) \<le> a" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"])

   632     (simp, simp add: add_sup_distrib_left)

   633 next

   634   fix a b :: 'a

   635   show "- sup (-a) (-b) \<le> b" by (rule add_le_imp_le_right [of _ "sup (-a) (-b)"])

   636     (simp, simp add: add_sup_distrib_left)

   637 next

   638   fix a b c :: 'a

   639   assume "a \<le> b" "a \<le> c"

   640   then show "a \<le> - sup (-b) (-c)" by (subst neg_le_iff_le [symmetric])

   641     (simp add: le_supI)

   642 qed

   643

   644 lemma sup_eq_neg_inf: "sup a (b\<Colon>'a\<Colon>lordered_ab_group) = - inf (-a) (-b)"

   645 proof (rule sup_unique)

   646   fix a b :: 'a

   647   show "a \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"])

   648     (simp, simp add: add_inf_distrib_left)

   649 next

   650   fix a b :: 'a

   651   show "b \<le> - inf (-a) (-b)" by (rule add_le_imp_le_right [of _ "inf (-a) (-b)"])

   652     (simp, simp add: add_inf_distrib_left)

   653 next

   654   fix a b c :: 'a

   655   assume "a \<le> c" "b \<le> c"

   656   then show "- inf (-a) (-b) \<le> c" by (subst neg_le_iff_le [symmetric])

   657     (simp add: le_infI)

   658 qed

   659

   660 lemma add_eq_inf_sup: "a + b = sup a b + inf a (b\<Colon>'a\<Colon>lordered_ab_group)"

   661 proof -

   662   have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)

   663   hence "0 = sup 0 (b-a) + inf (a-b) 0" by (simp add: inf_eq_neg_sup)

   664   hence "0 = (-a + sup a b) + (inf a b + (-b))"

   665     apply (simp add: add_sup_distrib_left add_inf_distrib_right)

   666     by (simp add: diff_minus add_commute)

   667   thus ?thesis

   668     apply (simp add: compare_rls)

   669     apply (subst add_left_cancel[symmetric, of "a+b" "sup a b + inf a b" "-a"])

   670     apply (simp only: add_assoc, simp add: add_assoc[symmetric])

   671     done

   672 qed

   673

   674 subsection {* Positive Part, Negative Part, Absolute Value *}

   675

   676 definition

   677   nprt :: "'a \<Rightarrow> ('a::lordered_ab_group)" where

   678   "nprt x = inf x 0"

   679

   680 definition

   681   pprt :: "'a \<Rightarrow> ('a::lordered_ab_group)" where

   682   "pprt x = sup x 0"

   683

   684 lemma prts: "a = pprt a + nprt a"

   685 by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])

   686

   687 lemma zero_le_pprt[simp]: "0 \<le> pprt a"

   688 by (simp add: pprt_def)

   689

   690 lemma nprt_le_zero[simp]: "nprt a \<le> 0"

   691 by (simp add: nprt_def)

   692

   693 lemma le_eq_neg: "(a \<le> -b) = (a + b \<le> (0::_::lordered_ab_group))" (is "?l = ?r")

   694 proof -

   695   have a: "?l \<longrightarrow> ?r"

   696     apply (auto)

   697     apply (rule add_le_imp_le_right[of _ "-b" _])

   698     apply (simp add: add_assoc)

   699     done

   700   have b: "?r \<longrightarrow> ?l"

   701     apply (auto)

   702     apply (rule add_le_imp_le_right[of _ "b" _])

   703     apply (simp)

   704     done

   705   from a b show ?thesis by blast

   706 qed

   707

   708 lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)

   709 lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)

   710

   711 lemma pprt_eq_id[simp]: "0 <= x \<Longrightarrow> pprt x = x"

   712   by (simp add: pprt_def le_iff_sup sup_aci)

   713

   714 lemma nprt_eq_id[simp]: "x <= 0 \<Longrightarrow> nprt x = x"

   715   by (simp add: nprt_def le_iff_inf inf_aci)

   716

   717 lemma pprt_eq_0[simp]: "x <= 0 \<Longrightarrow> pprt x = 0"

   718   by (simp add: pprt_def le_iff_sup sup_aci)

   719

   720 lemma nprt_eq_0[simp]: "0 <= x \<Longrightarrow> nprt x = 0"

   721   by (simp add: nprt_def le_iff_inf inf_aci)

   722

   723 lemma sup_0_imp_0: "sup a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"

   724 proof -

   725   {

   726     fix a::'a

   727     assume hyp: "sup a (-a) = 0"

   728     hence "sup a (-a) + a = a" by (simp)

   729     hence "sup (a+a) 0 = a" by (simp add: add_sup_distrib_right)

   730     hence "sup (a+a) 0 <= a" by (simp)

   731     hence "0 <= a" by (blast intro: order_trans inf_sup_ord)

   732   }

   733   note p = this

   734   assume hyp:"sup a (-a) = 0"

   735   hence hyp2:"sup (-a) (-(-a)) = 0" by (simp add: sup_commute)

   736   from p[OF hyp] p[OF hyp2] show "a = 0" by simp

   737 qed

   738

   739 lemma inf_0_imp_0: "inf a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"

   740 apply (simp add: inf_eq_neg_sup)

   741 apply (simp add: sup_commute)

   742 apply (erule sup_0_imp_0)

   743 done

   744

   745 lemma inf_0_eq_0[simp]: "(inf a (-a) = 0) = (a = (0::'a::lordered_ab_group))"

   746 by (auto, erule inf_0_imp_0)

   747

   748 lemma sup_0_eq_0[simp]: "(sup a (-a) = 0) = (a = (0::'a::lordered_ab_group))"

   749 by (auto, erule sup_0_imp_0)

   750

   751 lemma zero_le_double_add_iff_zero_le_single_add[simp]: "(0 \<le> a + a) = (0 \<le> (a::'a::lordered_ab_group))"

   752 proof

   753   assume "0 <= a + a"

   754   hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)

   755   have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_") by (simp add: add_sup_inf_distribs inf_aci)

   756   hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)

   757   hence "inf a 0 = 0" by (simp only: add_right_cancel)

   758   then show "0 <= a" by (simp add: le_iff_inf inf_commute)

   759 next

   760   assume a: "0 <= a"

   761   show "0 <= a + a" by (simp add: add_mono[OF a a, simplified])

   762 qed

   763

   764 lemma double_add_le_zero_iff_single_add_le_zero[simp]: "(a + a <= 0) = ((a::'a::lordered_ab_group) <= 0)"

   765 proof -

   766   have "(a + a <= 0) = (0 <= -(a+a))" by (subst le_minus_iff, simp)

   767   moreover have "\<dots> = (a <= 0)" by (simp add: zero_le_double_add_iff_zero_le_single_add)

   768   ultimately show ?thesis by blast

   769 qed

   770

   771 lemma double_add_less_zero_iff_single_less_zero[simp]: "(a+a<0) = ((a::'a::{pordered_ab_group_add,linorder}) < 0)" (is ?s)

   772 proof cases

   773   assume a: "a < 0"

   774   thus ?s by (simp add:  add_strict_mono[OF a a, simplified])

   775 next

   776   assume "~(a < 0)"

   777   hence a:"0 <= a" by (simp)

   778   hence "0 <= a+a" by (simp add: add_mono[OF a a, simplified])

   779   hence "~(a+a < 0)" by simp

   780   with a show ?thesis by simp

   781 qed

   782

   783 class lordered_ab_group_abs = lordered_ab_group +

   784   assumes abs_lattice: "abs x = sup x (uminus x)"

   785

   786 lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)"

   787 by (simp add: abs_lattice)

   788

   789 lemma abs_eq_0[simp]: "(abs a = 0) = (a = (0::'a::lordered_ab_group_abs))"

   790 by (simp add: abs_lattice)

   791

   792 lemma abs_0_eq[simp]: "(0 = abs a) = (a = (0::'a::lordered_ab_group_abs))"

   793 proof -

   794   have "(0 = abs a) = (abs a = 0)" by (simp only: eq_ac)

   795   thus ?thesis by simp

   796 qed

   797

   798 lemma neg_inf_eq_sup[simp]: "- inf a (b::_::lordered_ab_group) = sup (-a) (-b)"

   799 by (simp add: inf_eq_neg_sup)

   800

   801 lemma neg_sup_eq_inf[simp]: "- sup a (b::_::lordered_ab_group) = inf (-a) (-b)"

   802 by (simp del: neg_inf_eq_sup add: sup_eq_neg_inf)

   803

   804 lemma sup_eq_if: "sup a (-a) = (if a < 0 then -a else (a::'a::{lordered_ab_group, linorder}))"

   805 proof -

   806   note b = add_le_cancel_right[of a a "-a",symmetric,simplified]

   807   have c: "a + a = 0 \<Longrightarrow> -a = a" by (rule add_right_imp_eq[of _ a], simp)

   808   show ?thesis by (auto simp add: max_def b linorder_not_less sup_max)

   809 qed

   810

   811 lemma abs_if_lattice: "\<bar>a\<bar> = (if a < 0 then -a else (a::'a::{lordered_ab_group_abs, linorder}))"

   812 proof -

   813   show ?thesis by (simp add: abs_lattice sup_eq_if)

   814 qed

   815

   816 lemma abs_ge_zero[simp]: "0 \<le> abs (a::'a::lordered_ab_group_abs)"

   817 proof -

   818   have a:"a <= abs a" and b:"-a <= abs a" by (auto simp add: abs_lattice)

   819   show ?thesis by (rule add_mono[OF a b, simplified])

   820 qed

   821

   822 lemma abs_le_zero_iff [simp]: "(abs a \<le> (0::'a::lordered_ab_group_abs)) = (a = 0)"

   823 proof

   824   assume "abs a <= 0"

   825   hence "abs a = 0" by (auto dest: order_antisym)

   826   thus "a = 0" by simp

   827 next

   828   assume "a = 0"

   829   thus "abs a <= 0" by simp

   830 qed

   831

   832 lemma zero_less_abs_iff [simp]: "(0 < abs a) = (a \<noteq> (0::'a::lordered_ab_group_abs))"

   833 by (simp add: order_less_le)

   834

   835 lemma abs_not_less_zero [simp]: "~ abs a < (0::'a::lordered_ab_group_abs)"

   836 proof -

   837   have a:"!! x (y::_::order). x <= y \<Longrightarrow> ~(y < x)" by auto

   838   show ?thesis by (simp add: a)

   839 qed

   840

   841 lemma abs_ge_self: "a \<le> abs (a::'a::lordered_ab_group_abs)"

   842 by (simp add: abs_lattice)

   843

   844 lemma abs_ge_minus_self: "-a \<le> abs (a::'a::lordered_ab_group_abs)"

   845 by (simp add: abs_lattice)

   846

   847 lemma abs_prts: "abs (a::_::lordered_ab_group_abs) = pprt a - nprt a"

   848 apply (simp add: pprt_def nprt_def diff_minus)

   849 apply (simp add: add_sup_inf_distribs sup_aci abs_lattice[symmetric])

   850 apply (subst sup_absorb2, auto)

   851 done

   852

   853 lemma abs_minus_cancel [simp]: "abs (-a) = abs(a::'a::lordered_ab_group_abs)"

   854 by (simp add: abs_lattice sup_commute)

   855

   856 lemma abs_idempotent [simp]: "abs (abs a) = abs (a::'a::lordered_ab_group_abs)"

   857 apply (simp add: abs_lattice[of "abs a"])

   858 apply (subst sup_absorb1)

   859 apply (rule order_trans[of _ 0])

   860 by auto

   861

   862 lemma abs_minus_commute:

   863   fixes a :: "'a::lordered_ab_group_abs"

   864   shows "abs (a-b) = abs(b-a)"

   865 proof -

   866   have "abs (a-b) = abs (- (a-b))" by (simp only: abs_minus_cancel)

   867   also have "... = abs(b-a)" by simp

   868   finally show ?thesis .

   869 qed

   870

   871 lemma zero_le_iff_zero_nprt: "(0 \<le> a) = (nprt a = 0)"

   872 by (simp add: le_iff_inf nprt_def inf_commute)

   873

   874 lemma le_zero_iff_zero_pprt: "(a \<le> 0) = (pprt a = 0)"

   875 by (simp add: le_iff_sup pprt_def sup_commute)

   876

   877 lemma le_zero_iff_pprt_id: "(0 \<le> a) = (pprt a = a)"

   878 by (simp add: le_iff_sup pprt_def sup_commute)

   879

   880 lemma zero_le_iff_nprt_id: "(a \<le> 0) = (nprt a = a)"

   881 by (simp add: le_iff_inf nprt_def inf_commute)

   882

   883 lemma pprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> pprt a <= pprt b"

   884   by (simp add: le_iff_sup pprt_def sup_aci)

   885

   886 lemma nprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"

   887   by (simp add: le_iff_inf nprt_def inf_aci)

   888

   889 lemma pprt_neg: "pprt (-x) = - nprt x"

   890   by (simp add: pprt_def nprt_def)

   891

   892 lemma nprt_neg: "nprt (-x) = - pprt x"

   893   by (simp add: pprt_def nprt_def)

   894

   895 lemma iff2imp: "(A=B) \<Longrightarrow> (A \<Longrightarrow> B)"

   896 by (simp)

   897

   898 lemma abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> abs a = (a::'a::lordered_ab_group_abs)"

   899 by (simp add: iff2imp[OF zero_le_iff_zero_nprt] iff2imp[OF le_zero_iff_pprt_id] abs_prts)

   900

   901 lemma abs_of_pos: "0 < (x::'a::lordered_ab_group_abs) ==> abs x = x";

   902 by (rule abs_of_nonneg, rule order_less_imp_le);

   903

   904 lemma abs_of_nonpos [simp]: "a \<le> 0 \<Longrightarrow> abs a = -(a::'a::lordered_ab_group_abs)"

   905 by (simp add: iff2imp[OF le_zero_iff_zero_pprt] iff2imp[OF zero_le_iff_nprt_id] abs_prts)

   906

   907 lemma abs_of_neg: "(x::'a::lordered_ab_group_abs) <  0 ==>

   908   abs x = - x"

   909 by (rule abs_of_nonpos, rule order_less_imp_le)

   910

   911 lemma abs_leI: "[|a \<le> b; -a \<le> b|] ==> abs a \<le> (b::'a::lordered_ab_group_abs)"

   912 by (simp add: abs_lattice le_supI)

   913

   914 lemma le_minus_self_iff: "(a \<le> -a) = (a \<le> (0::'a::lordered_ab_group))"

   915 proof -

   916   from add_le_cancel_left[of "-a" "a+a" "0"] have "(a <= -a) = (a+a <= 0)"

   917     by (simp add: add_assoc[symmetric])

   918   thus ?thesis by simp

   919 qed

   920

   921 lemma minus_le_self_iff: "(-a \<le> a) = (0 \<le> (a::'a::lordered_ab_group))"

   922 proof -

   923   from add_le_cancel_left[of "-a" "0" "a+a"] have "(-a <= a) = (0 <= a+a)"

   924     by (simp add: add_assoc[symmetric])

   925   thus ?thesis by simp

   926 qed

   927

   928 lemma abs_le_D1: "abs a \<le> b ==> a \<le> (b::'a::lordered_ab_group_abs)"

   929 by (insert abs_ge_self, blast intro: order_trans)

   930

   931 lemma abs_le_D2: "abs a \<le> b ==> -a \<le> (b::'a::lordered_ab_group_abs)"

   932 by (insert abs_le_D1 [of "-a"], simp)

   933

   934 lemma abs_le_iff: "(abs a \<le> b) = (a \<le> b & -a \<le> (b::'a::lordered_ab_group_abs))"

   935 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)

   936

   937 lemma abs_triangle_ineq: "abs(a+b) \<le> abs a + abs(b::'a::lordered_ab_group_abs)"

   938 proof -

   939   have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")

   940     by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)

   941   have a:"a+b <= sup ?m ?n" by (simp)

   942   have b:"-a-b <= ?n" by (simp)

   943   have c:"?n <= sup ?m ?n" by (simp)

   944   from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)

   945   have e:"-a-b = -(a+b)" by (simp add: diff_minus)

   946   from a d e have "abs(a+b) <= sup ?m ?n"

   947     by (drule_tac abs_leI, auto)

   948   with g[symmetric] show ?thesis by simp

   949 qed

   950

   951 lemma abs_triangle_ineq2: "abs (a::'a::lordered_ab_group_abs) -

   952     abs b <= abs (a - b)"

   953   apply (simp add: compare_rls)

   954   apply (subgoal_tac "abs a = abs (a - b + b)")

   955   apply (erule ssubst)

   956   apply (rule abs_triangle_ineq)

   957   apply (rule arg_cong);back;

   958   apply (simp add: compare_rls)

   959 done

   960

   961 lemma abs_triangle_ineq3:

   962     "abs(abs (a::'a::lordered_ab_group_abs) - abs b) <= abs (a - b)"

   963   apply (subst abs_le_iff)

   964   apply auto

   965   apply (rule abs_triangle_ineq2)

   966   apply (subst abs_minus_commute)

   967   apply (rule abs_triangle_ineq2)

   968 done

   969

   970 lemma abs_triangle_ineq4: "abs ((a::'a::lordered_ab_group_abs) - b) <=

   971     abs a + abs b"

   972 proof -;

   973   have "abs(a - b) = abs(a + - b)"

   974     by (subst diff_minus, rule refl)

   975   also have "... <= abs a + abs (- b)"

   976     by (rule abs_triangle_ineq)

   977   finally show ?thesis

   978     by simp

   979 qed

   980

   981 lemma abs_diff_triangle_ineq:

   982      "\<bar>(a::'a::lordered_ab_group_abs) + b - (c+d)\<bar> \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>"

   983 proof -

   984   have "\<bar>a + b - (c+d)\<bar> = \<bar>(a-c) + (b-d)\<bar>" by (simp add: diff_minus add_ac)

   985   also have "... \<le> \<bar>a-c\<bar> + \<bar>b-d\<bar>" by (rule abs_triangle_ineq)

   986   finally show ?thesis .

   987 qed

   988

   989 lemma abs_add_abs[simp]:

   990 fixes a:: "'a::{lordered_ab_group_abs}"

   991 shows "abs(abs a + abs b) = abs a + abs b" (is "?L = ?R")

   992 proof (rule order_antisym)

   993   show "?L \<ge> ?R" by(rule abs_ge_self)

   994 next

   995   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)

   996   also have "\<dots> = ?R" by simp

   997   finally show "?L \<le> ?R" .

   998 qed

   999

  1000 text {* Needed for abelian cancellation simprocs: *}

  1001

  1002 lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"

  1003 apply (subst add_left_commute)

  1004 apply (subst add_left_cancel)

  1005 apply simp

  1006 done

  1007

  1008 lemma add_cancel_end: "(x + (y + z) = y) = (x = - (z::'a::ab_group_add))"

  1009 apply (subst add_cancel_21[of _ _ _ 0, simplified])

  1010 apply (simp add: add_right_cancel[symmetric, of "x" "-z" "z", simplified])

  1011 done

  1012

  1013 lemma less_eqI: "(x::'a::pordered_ab_group_add) - y = x' - y' \<Longrightarrow> (x < y) = (x' < y')"

  1014 by (simp add: less_iff_diff_less_0[of x y] less_iff_diff_less_0[of x' y'])

  1015

  1016 lemma le_eqI: "(x::'a::pordered_ab_group_add) - y = x' - y' \<Longrightarrow> (y <= x) = (y' <= x')"

  1017 apply (simp add: le_iff_diff_le_0[of y x] le_iff_diff_le_0[of  y' x'])

  1018 apply (simp add: neg_le_iff_le[symmetric, of "y-x" 0] neg_le_iff_le[symmetric, of "y'-x'" 0])

  1019 done

  1020

  1021 lemma eq_eqI: "(x::'a::ab_group_add) - y = x' - y' \<Longrightarrow> (x = y) = (x' = y')"

  1022 by (simp add: eq_iff_diff_eq_0[of x y] eq_iff_diff_eq_0[of x' y'])

  1023

  1024 lemma diff_def: "(x::'a::ab_group_add) - y == x + (-y)"

  1025 by (simp add: diff_minus)

  1026

  1027 lemma add_minus_cancel: "(a::'a::ab_group_add) + (-a + b) = b"

  1028 by (simp add: add_assoc[symmetric])

  1029

  1030 lemma  le_add_right_mono:

  1031   assumes

  1032   "a <= b + (c::'a::pordered_ab_group_add)"

  1033   "c <= d"

  1034   shows "a <= b + d"

  1035   apply (rule_tac order_trans[where y = "b+c"])

  1036   apply (simp_all add: prems)

  1037   done

  1038

  1039 lemmas group_eq_simps =

  1040   mult_ac

  1041   add_ac

  1042   add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2

  1043   diff_eq_eq eq_diff_eq

  1044

  1045 lemma estimate_by_abs:

  1046 "a + b <= (c::'a::lordered_ab_group_abs) \<Longrightarrow> a <= c + abs b"

  1047 proof -

  1048   assume 1: "a+b <= c"

  1049   have 2: "a <= c+(-b)"

  1050     apply (insert 1)

  1051     apply (drule_tac add_right_mono[where c="-b"])

  1052     apply (simp add: group_eq_simps)

  1053     done

  1054   have 3: "(-b) <= abs b" by (rule abs_ge_minus_self)

  1055   show ?thesis by (rule le_add_right_mono[OF 2 3])

  1056 qed

  1057

  1058

  1059 subsection {* Tools setup *}

  1060

  1061 text{*Simplification of @{term "x-y < 0"}, etc.*}

  1062 lemmas diff_less_0_iff_less = less_iff_diff_less_0 [symmetric]

  1063 lemmas diff_eq_0_iff_eq = eq_iff_diff_eq_0 [symmetric]

  1064 lemmas diff_le_0_iff_le = le_iff_diff_le_0 [symmetric]

  1065 declare diff_less_0_iff_less [simp]

  1066 declare diff_eq_0_iff_eq [simp]

  1067 declare diff_le_0_iff_le [simp]

  1068

  1069 ML {*

  1070 structure ab_group_add_cancel = Abel_Cancel(

  1071 struct

  1072

  1073 (* term order for abelian groups *)

  1074

  1075 fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')

  1076       [@{const_name HOL.zero}, @{const_name HOL.plus},

  1077         @{const_name HOL.uminus}, @{const_name HOL.minus}]

  1078   | agrp_ord _ = ~1;

  1079

  1080 fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);

  1081

  1082 local

  1083   val ac1 = mk_meta_eq @{thm add_assoc};

  1084   val ac2 = mk_meta_eq @{thm add_commute};

  1085   val ac3 = mk_meta_eq @{thm add_left_commute};

  1086   fun solve_add_ac thy _ (_ $(Const (@{const_name HOL.plus},_)$ _ $_)$ _) =

  1087         SOME ac1

  1088     | solve_add_ac thy _ (_ $x$ (Const (@{const_name HOL.plus},_) $y$ z)) =

  1089         if termless_agrp (y, x) then SOME ac3 else NONE

  1090     | solve_add_ac thy _ (_ $x$ y) =

  1091         if termless_agrp (y, x) then SOME ac2 else NONE

  1092     | solve_add_ac thy _ _ = NONE

  1093 in

  1094   val add_ac_proc = Simplifier.simproc @{theory}

  1095     "add_ac_proc" ["x + y::'a::ab_semigroup_add"] solve_add_ac;

  1096 end;

  1097

  1098 val cancel_ss = HOL_basic_ss settermless termless_agrp

  1099   addsimprocs [add_ac_proc] addsimps

  1100   [@{thm add_0_left}, @{thm add_0_right}, @{thm diff_def},

  1101    @{thm minus_add_distrib}, @{thm minus_minus}, @{thm minus_zero},

  1102    @{thm right_minus}, @{thm left_minus}, @{thm add_minus_cancel},

  1103    @{thm minus_add_cancel}];

  1104

  1105 val eq_reflection = @{thm eq_reflection};

  1106

  1107 val thy_ref = Theory.self_ref @{theory};

  1108

  1109 val T = TFree("'a", ["OrderedGroup.ab_group_add"]);

  1110

  1111 val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];

  1112

  1113 val dest_eqI =

  1114   fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;

  1115

  1116 end);

  1117 *}

  1118

  1119 ML_setup {*

  1120   Addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv];

  1121 *}

  1122

  1123 end