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.5    by (simp add: nprt_def)
     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.31        by (simp add: add_sup_distrib_right)
    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.43      by (simp add: sup_commute)
    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.53 -lemma zero_le_double_add_iff_zero_le_single_add [simp]:
    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.62 -    by (simp add: add_sup_inf_distribs inf_aci)
    1.63 -  then have "?l = 0 + inf a 0"
    1.64 -    by (simp add: a, simp add: inf_commute)
    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.72 -    by (simp add: add_mono[OF a a, simplified])
    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.78 +      by (simp add: add_sup_inf_distribs inf_aci)
    1.79 +    then have "?l = 0 + inf a 0"
    1.80 +      by (simp add: a, simp add: inf_commute)
    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.87 +    by (simp add: add_mono[OF that that, simplified])
    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.105 -    unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a]
   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.127 +      unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a]
   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.142 -lemma double_add_le_zero_iff_single_add_le_zero [simp]:
   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.150      by (simp only: minus_add_distrib zero_le_double_add_iff_zero_le_single_add) simp
   1.151    ultimately show ?thesis
   1.152      by blast
   1.153  qed
   1.154  
   1.155 -lemma double_add_less_zero_iff_single_less_zero [simp]:
   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.168      by (simp add: add.assoc[symmetric])
   1.169    then show ?thesis
   1.170      by simp
   1.171 @@ -370,15 +369,14 @@
   1.172  
   1.173  subclass ordered_ab_group_add_abs
   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.205        by (simp add: abs_lattice add_sup_inf_distribs ac_simps)
   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.239      by (simp add: algebra_simps)
   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.273      by (simp add: algebra_simps)
   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 +