simplified specification of *_abs class
authorhaftmann
Tue Nov 06 13:12:48 2007 +0100 (2007-11-06)
changeset 25307389902f0a0c8
parent 25306 351ca94cabdb
child 25308 fc01c83a466d
simplified specification of *_abs class
src/HOL/OrderedGroup.thy
     1.1 --- a/src/HOL/OrderedGroup.thy	Tue Nov 06 12:06:30 2007 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Tue Nov 06 13:12:48 2007 +0100
     1.3 @@ -746,14 +746,40 @@
     1.4  class pordered_ab_group_add_abs = pordered_ab_group_add + abs +
     1.5    assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
     1.6      and abs_ge_self: "a \<le> \<bar>a\<bar>"
     1.7 -    and abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a"
     1.8      and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
     1.9 -    and abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
    1.10      and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
    1.11 -    and abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
    1.12      and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
    1.13  begin
    1.14  
    1.15 +lemma abs_minus_le_zero: "- \<bar>a\<bar> \<le> 0"
    1.16 +  unfolding neg_le_0_iff_le by simp
    1.17 +
    1.18 +lemma abs_of_nonneg [simp]:
    1.19 +  assumes nonneg: "0 \<le> a"
    1.20 +  shows "\<bar>a\<bar> = a"
    1.21 +proof (rule antisym)
    1.22 +  from nonneg le_imp_neg_le have "- a \<le> 0" by simp
    1.23 +  from this nonneg have "- a \<le> a" by (rule order_trans)
    1.24 +  then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI)
    1.25 +qed (rule abs_ge_self)
    1.26 +
    1.27 +lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
    1.28 +  by (rule antisym)
    1.29 +    (auto intro!: abs_ge_self abs_leI order_trans [of "uminus (abs a)" zero "abs a"])
    1.30 +
    1.31 +lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
    1.32 +proof -
    1.33 +  have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
    1.34 +  proof (rule antisym)
    1.35 +    assume zero: "\<bar>a\<bar> = 0"
    1.36 +    with abs_ge_self show "a \<le> 0" by auto
    1.37 +    from zero have "\<bar>-a\<bar> = 0" by simp
    1.38 +    with abs_ge_self [of "uminus a"] have "- a \<le> 0" by auto
    1.39 +    with neg_le_0_iff_le show "0 \<le> a" by auto
    1.40 +  qed
    1.41 +  then show ?thesis by auto
    1.42 +qed
    1.43 +
    1.44  lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
    1.45    by simp
    1.46  
    1.47 @@ -1213,26 +1239,9 @@
    1.48        by (auto simp add: abs_lattice)
    1.49    next
    1.50      fix a
    1.51 -    show "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
    1.52 -      by (simp add: abs_lattice)
    1.53 -  next
    1.54 -    fix a
    1.55      show "\<bar>-a\<bar> = \<bar>a\<bar>"
    1.56        by (simp add: abs_lattice sup_commute)
    1.57    next
    1.58 -    fix a
    1.59 -    show "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
    1.60 -    apply (simp add: abs_lattice [of "abs a"])
    1.61 -    apply (subst sup_absorb1)
    1.62 -    apply (rule order_trans [of _ zero])
    1.63 -    apply auto
    1.64 -    done
    1.65 -  next
    1.66 -    fix a
    1.67 -    show "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a"
    1.68 -      by (simp add: iffD1 [OF zero_le_iff_zero_nprt]
    1.69 -        iffD1[OF le_zero_iff_pprt_id] abs_prts)
    1.70 -  next
    1.71      fix a b
    1.72      show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (erule abs_leI)
    1.73    next