src/HOL/Library/Lattice_Algebras.thy
 changeset 60698 29e8bdc41f90 parent 60500 903bb1495239 child 61546 53bb4172c7f7
```     1.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Thu Jul 09 00:39:49 2015 +0200
1.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Thu Jul 09 00:40:57 2015 +0200
1.3 @@ -145,7 +145,8 @@
1.4  lemma nprt_le_zero[simp]: "nprt a \<le> 0"
1.6
1.7 -lemma le_eq_neg: "a \<le> - b \<longleftrightarrow> a + b \<le> 0" (is "?l = ?r")
1.8 +lemma le_eq_neg: "a \<le> - b \<longleftrightarrow> a + b \<le> 0"
1.9 +  (is "?l = ?r")
1.10  proof
1.11    assume ?l
1.12    then show ?r
1.13 @@ -177,25 +178,24 @@
1.14  lemma nprt_eq_0 [simp, no_atp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
1.15    by (simp add: nprt_def inf_absorb2)
1.16
1.17 -lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
1.18 +lemma sup_0_imp_0:
1.19 +  assumes "sup a (- a) = 0"
1.20 +  shows "a = 0"
1.21  proof -
1.22 -  {
1.23 -    fix a :: 'a
1.24 -    assume hyp: "sup a (- a) = 0"
1.25 -    then have "sup a (- a) + a = a"
1.26 +  have p: "0 \<le> a" if "sup a (- a) = 0" for a :: 'a
1.27 +  proof -
1.28 +    from that have "sup a (- a) + a = a"
1.29        by simp
1.30      then have "sup (a + a) 0 = a"
1.32      then have "sup (a + a) 0 \<le> a"
1.33        by simp
1.34 -    then have "0 \<le> a"
1.35 +    then show ?thesis
1.36        by (blast intro: order_trans inf_sup_ord)
1.37 -  }
1.38 -  note p = this
1.39 -  assume hyp:"sup a (-a) = 0"
1.40 -  then have hyp2:"sup (-a) (-(-a)) = 0"
1.41 +  qed
1.42 +  from assms have **: "sup (-a) (-(-a)) = 0"
1.44 -  from p[OF hyp] p[OF hyp2] show "a = 0"
1.45 +  from p[OF assms] p[OF **] show "a = 0"
1.46      by simp
1.47  qed
1.48
1.49 @@ -217,49 +217,50 @@
1.50    apply simp
1.51    done
1.52
1.54 -  "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
1.55 +lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
1.56 +  (is "?lhs \<longleftrightarrow> ?rhs")
1.57  proof
1.58 -  assume "0 \<le> a + a"
1.59 -  then have a: "inf (a + a) 0 = 0"
1.60 -    by (simp add: inf_commute inf_absorb1)
1.61 -  have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a"  (is "?l=_")
1.63 -  then have "?l = 0 + inf a 0"
1.65 -  then have "inf a 0 = 0"
1.66 -    by (simp only: add_right_cancel)
1.67 -  then show "0 \<le> a"
1.68 -    unfolding le_iff_inf by (simp add: inf_commute)
1.69 -next
1.70 -  assume a: "0 \<le> a"
1.71 -  show "0 \<le> a + a"
1.73 +  show ?rhs if ?lhs
1.74 +  proof -
1.75 +    from that have a: "inf (a + a) 0 = 0"
1.76 +      by (simp add: inf_commute inf_absorb1)
1.77 +    have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a"  (is "?l=_")
1.79 +    then have "?l = 0 + inf a 0"
1.81 +    then have "inf a 0 = 0"
1.82 +      by (simp only: add_right_cancel)
1.83 +    then show ?thesis
1.84 +      unfolding le_iff_inf by (simp add: inf_commute)
1.85 +  qed
1.86 +  show ?lhs if ?rhs
1.88  qed
1.89
1.90  lemma double_zero [simp]: "a + a = 0 \<longleftrightarrow> a = 0"
1.91 +  (is "?lhs \<longleftrightarrow> ?rhs")
1.92  proof
1.93 -  assume assm: "a + a = 0"
1.94 -  then have "a + a + - a = - a"
1.95 -    by simp
1.96 -  then have "a + (a + - a) = - a"
1.97 -    by (simp only: add.assoc)
1.98 -  then have a: "- a = a"
1.99 -    by simp
1.100 -  show "a = 0"
1.101 -    apply (rule antisym)
1.102 -    apply (unfold neg_le_iff_le [symmetric, of a])
1.103 -    unfolding a
1.104 -    apply simp
1.106 -    unfolding assm
1.107 -    unfolding le_less
1.108 -    apply simp_all
1.109 -    done
1.110 -next
1.111 -  assume "a = 0"
1.112 -  then show "a + a = 0"
1.113 -    by simp
1.114 +  show ?rhs if ?lhs
1.115 +  proof -
1.116 +    from that have "a + a + - a = - a"
1.117 +      by simp
1.118 +    then have "a + (a + - a) = - a"
1.119 +      by (simp only: add.assoc)
1.120 +    then have a: "- a = a"
1.121 +      by simp
1.122 +    show ?thesis
1.123 +      apply (rule antisym)
1.124 +      apply (unfold neg_le_iff_le [symmetric, of a])
1.125 +      unfolding a
1.126 +      apply simp
1.128 +      unfolding that
1.129 +      unfolding le_less
1.130 +      apply simp_all
1.131 +      done
1.132 +  qed
1.133 +  show ?lhs if ?rhs
1.134 +    using that by simp
1.135  qed
1.136
1.137  lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a"
1.138 @@ -281,19 +282,17 @@
1.139      done
1.140  qed
1.141
1.143 -  "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
1.144 +lemma double_add_le_zero_iff_single_add_le_zero [simp]: "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
1.145  proof -
1.146    have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)"
1.147 -    by (subst le_minus_iff, simp)
1.148 +    by (subst le_minus_iff) simp
1.149    moreover have "\<dots> \<longleftrightarrow> a \<le> 0"
1.151    ultimately show ?thesis
1.152      by blast
1.153  qed
1.154
1.156 -  "a + a < 0 \<longleftrightarrow> a < 0"
1.157 +lemma double_add_less_zero_iff_single_less_zero [simp]: "a + a < 0 \<longleftrightarrow> a < 0"
1.158  proof -
1.159    have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)"
1.160      by (subst less_minus_iff) simp
1.161 @@ -316,8 +315,8 @@
1.162
1.163  lemma minus_le_self_iff: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
1.164  proof -
1.165 -  from add_le_cancel_left [of "uminus a" zero "plus a a"]
1.166    have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a"
1.167 +    using add_le_cancel_left [of "uminus a" zero "plus a a"]
1.169    then show ?thesis
1.170      by simp
1.171 @@ -370,15 +369,14 @@
1.172
1.174  proof
1.175 -  have abs_ge_zero [simp]: "\<And>a. 0 \<le> \<bar>a\<bar>"
1.176 +  have abs_ge_zero [simp]: "0 \<le> \<bar>a\<bar>" for a
1.177    proof -
1.178 -    fix a b
1.179      have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>"
1.180        by (auto simp add: abs_lattice)
1.181      show "0 \<le> \<bar>a\<bar>"
1.182        by (rule add_mono [OF a b, simplified])
1.183    qed
1.184 -  have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
1.185 +  have abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" for a b
1.186      by (simp add: abs_lattice le_supI)
1.187    fix a b
1.188    show "0 \<le> \<bar>a\<bar>"
1.189 @@ -387,15 +385,12 @@
1.190      by (auto simp add: abs_lattice)
1.191    show "\<bar>-a\<bar> = \<bar>a\<bar>"
1.192      by (simp add: abs_lattice sup_commute)
1.193 -  {
1.194 -    assume "a \<le> b"
1.195 -    then show "- a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
1.196 -      by (rule abs_leI)
1.197 -  }
1.198 +  show "- a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" if "a \<le> b"
1.199 +    using that by (rule abs_leI)
1.200    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
1.201    proof -
1.202      have g: "\<bar>a\<bar> + \<bar>b\<bar> = sup (a + b) (sup (- a - b) (sup (- a + b) (a + (- b))))"
1.203 -      (is "_=sup ?m ?n")
1.204 +      (is "_ = sup ?m ?n")
1.206      have a: "a + b \<le> sup ?m ?n"
1.207        by simp
1.208 @@ -420,25 +415,23 @@
1.209  end
1.210
1.211  lemma sup_eq_if:
1.212 -  fixes a :: "'a::{lattice_ab_group_add, linorder}"
1.213 +  fixes a :: "'a::{lattice_ab_group_add,linorder}"
1.214    shows "sup a (- a) = (if a < 0 then - a else a)"
1.215 -proof -
1.216 -  note add_le_cancel_right [of a a "- a", symmetric, simplified]
1.217 -  moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
1.218 -  then show ?thesis by (auto simp: sup_max max.absorb1 max.absorb2)
1.219 -qed
1.220 +  using add_le_cancel_right [of a a "- a", symmetric, simplified]
1.221 +    and add_le_cancel_right [of "-a" a a, symmetric, simplified]
1.222 +  by (auto simp: sup_max max.absorb1 max.absorb2)
1.223
1.224  lemma abs_if_lattice:
1.225 -  fixes a :: "'a::{lattice_ab_group_add_abs, linorder}"
1.226 +  fixes a :: "'a::{lattice_ab_group_add_abs,linorder}"
1.227    shows "\<bar>a\<bar> = (if a < 0 then - a else a)"
1.228    by auto
1.229
1.230  lemma estimate_by_abs:
1.231    fixes a b c :: "'a::lattice_ab_group_add_abs"
1.232 -  shows "a + b \<le> c \<Longrightarrow> a \<le> c + \<bar>b\<bar>"
1.233 +  assumes "a + b \<le> c"
1.234 +  shows "a \<le> c + \<bar>b\<bar>"
1.235  proof -
1.236 -  assume "a + b \<le> c"
1.237 -  then have "a \<le> c + (- b)"
1.238 +  from assms have "a \<le> c + (- b)"
1.240    have "- b \<le> \<bar>b\<bar>"
1.241      by (rule abs_ge_minus_self)
1.242 @@ -464,15 +457,12 @@
1.243    let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
1.244    have a: "\<bar>a\<bar> * \<bar>b\<bar> = ?x"
1.245      by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps)
1.246 -  {
1.247 -    fix u v :: 'a
1.248 -    have bh: "u = a \<Longrightarrow> v = b \<Longrightarrow>
1.249 -              u * v = pprt a * pprt b + pprt a * nprt b +
1.250 -                      nprt a * pprt b + nprt a * nprt b"
1.251 -      apply (subst prts[of u], subst prts[of v])
1.252 -      apply (simp add: algebra_simps)
1.253 -      done
1.254 -  }
1.255 +  have bh: "u = a \<Longrightarrow> v = b \<Longrightarrow>
1.256 +            u * v = pprt a * pprt b + pprt a * nprt b +
1.257 +                    nprt a * pprt b + nprt a * nprt b" for u v :: 'a
1.258 +    apply (subst prts[of u], subst prts[of v])
1.259 +    apply (simp add: algebra_simps)
1.260 +    done
1.261    note b = this[OF refl[of a] refl[of b]]
1.262    have xy: "- ?x \<le> ?y"
1.263      apply simp
1.264 @@ -552,9 +542,7 @@
1.265      pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
1.266  proof -
1.267    have "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
1.268 -    apply (subst prts[symmetric])+
1.269 -    apply simp
1.270 -    done
1.271 +    by (subst prts[symmetric])+ simp
1.272    then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
1.274    moreover have "pprt a * pprt b \<le> pprt a2 * pprt b2"
1.275 @@ -587,9 +575,7 @@
1.276        by simp
1.277    qed
1.278    ultimately show ?thesis
1.279 -    apply -
1.280 -    apply (rule add_mono | simp)+
1.281 -    done
1.282 +    by - (rule add_mono | simp)+
1.283  qed
1.284
1.285  lemma mult_ge_prts:
1.286 @@ -607,7 +593,8 @@
1.287      by auto
1.288    from mult_le_prts[of "- a2" "- a" "- a1" "b1" b "b2",
1.289      OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg]
1.290 -  have le: "- (a * b) \<le> - nprt a1 * pprt b2 + - nprt a2 * nprt b2 +
1.291 +  have le: "- (a * b) \<le>
1.292 +    - nprt a1 * pprt b2 + - nprt a2 * nprt b2 +
1.293      - pprt a1 * pprt b1 + - pprt a2 * nprt b1"
1.294      by simp
1.295    then have "- (- nprt a1 * pprt b2 + - nprt a2 * nprt b2 +
```