src/HOL/Library/Lattice_Algebras.thy
 changeset 65151 a7394aa4d21c parent 61546 53bb4172c7f7 child 68406 6beb45f6cf67
```     1.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Wed Mar 08 10:29:40 2017 +0100
1.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Wed Mar 08 10:50:59 2017 +0100
1.3 @@ -3,7 +3,7 @@
1.4  section \<open>Various algebraic structures combined with a lattice\<close>
1.5
1.6  theory Lattice_Algebras
1.7 -imports Complex_Main
1.8 +  imports Complex_Main
1.9  begin
1.10
1.12 @@ -11,7 +11,7 @@
1.13
1.14  lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + c)"
1.15    apply (rule antisym)
1.16 -  apply (simp_all add: le_infI)
1.17 +   apply (simp_all add: le_infI)
1.18    apply (rule add_le_imp_le_left [of "uminus a"])
1.20    done
1.21 @@ -31,11 +31,11 @@
1.22
1.23  lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a + c)"
1.24    apply (rule antisym)
1.25 -  apply (rule add_le_imp_le_left [of "uminus a"])
1.26 -  apply (simp only: add.assoc [symmetric], simp)
1.28 +   apply (rule add_le_imp_le_left [of "uminus a"])
1.29 +   apply (simp only: add.assoc [symmetric], simp)
1.31    apply (rule le_supI)
1.34    done
1.35
1.36  lemma add_sup_distrib_right: "sup a b + c = sup (a + c) (b + c)"
1.37 @@ -80,9 +80,8 @@
1.38    show "b \<le> - inf (- a) (- b)"
1.39      by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
1.41 -  assume "a \<le> c" "b \<le> c"
1.42 -  then show "- inf (- a) (- b) \<le> c"
1.43 -    by (subst neg_le_iff_le [symmetric]) (simp add: le_infI)
1.44 +  show "- inf (- a) (- b) \<le> c" if "a \<le> c" "b \<le> c"
1.45 +    using that by (subst neg_le_iff_le [symmetric]) (simp add: le_infI)
1.46  qed
1.47
1.48  lemma neg_inf_eq_sup: "- inf a b = sup (- a) (- b)"
1.49 @@ -121,12 +120,12 @@
1.50  lemma pprt_neg: "pprt (- x) = - nprt x"
1.51  proof -
1.52    have "sup (- x) 0 = sup (- x) (- 0)"
1.53 -    unfolding minus_zero ..
1.54 +    by (simp only: minus_zero)
1.55    also have "\<dots> = - inf x 0"
1.56 -    unfolding neg_inf_eq_sup ..
1.57 +    by (simp only: neg_inf_eq_sup)
1.58    finally have "sup (- x) 0 = - inf x 0" .
1.59    then show ?thesis
1.60 -    unfolding pprt_def nprt_def .
1.61 +    by (simp only: pprt_def nprt_def)
1.62  qed
1.63
1.64  lemma nprt_neg: "nprt (- x) = - pprt x"
1.65 @@ -146,21 +145,15 @@
1.67
1.68  lemma le_eq_neg: "a \<le> - b \<longleftrightarrow> a + b \<le> 0"
1.69 -  (is "?l = ?r")
1.70 +  (is "?lhs = ?rhs")
1.71  proof
1.72 -  assume ?l
1.73 -  then show ?r
1.74 -    apply -
1.75 -    apply (rule add_le_imp_le_right[of _ "uminus b" _])
1.77 -    done
1.78 +  assume ?lhs
1.79 +  show ?rhs
1.81  next
1.82 -  assume ?r
1.83 -  then show ?l
1.84 -    apply -
1.85 -    apply (rule add_le_imp_le_right[of _ "b" _])
1.86 -    apply simp
1.87 -    done
1.88 +  assume ?rhs
1.89 +  show ?lhs
1.91  qed
1.92
1.93  lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)
1.94 @@ -182,7 +175,7 @@
1.95    assumes "sup a (- a) = 0"
1.96    shows "a = 0"
1.97  proof -
1.98 -  have p: "0 \<le> a" if "sup a (- a) = 0" for a :: 'a
1.99 +  have pos: "0 \<le> a" if "sup a (- a) = 0" for a :: 'a
1.100    proof -
1.101      from that have "sup a (- a) + a = a"
1.102        by simp
1.103 @@ -195,7 +188,7 @@
1.104    qed
1.105    from assms have **: "sup (-a) (-(-a)) = 0"
1.107 -  from p[OF assms] p[OF **] show "a = 0"
1.108 +  from pos[OF assms] pos[OF **] show "a = 0"
1.109      by simp
1.110  qed
1.111
1.112 @@ -206,14 +199,14 @@
1.113    done
1.114
1.115  lemma inf_0_eq_0 [simp, no_atp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
1.116 -  apply rule
1.117 -  apply (erule inf_0_imp_0)
1.118 +  apply (rule iffI)
1.119 +   apply (erule inf_0_imp_0)
1.120    apply simp
1.121    done
1.122
1.123  lemma sup_0_eq_0 [simp, no_atp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
1.124 -  apply rule
1.125 -  apply (erule sup_0_imp_0)
1.126 +  apply (rule iffI)
1.127 +   apply (erule sup_0_imp_0)
1.128    apply simp
1.129    done
1.130
1.131 @@ -238,49 +231,11 @@
1.132  qed
1.133
1.134  lemma double_zero [simp]: "a + a = 0 \<longleftrightarrow> a = 0"
1.135 -  (is "?lhs \<longleftrightarrow> ?rhs")
1.136 -proof
1.137 -  show ?rhs if ?lhs
1.138 -  proof -
1.139 -    from that have "a + a + - a = - a"
1.140 -      by simp
1.141 -    then have "a + (a + - a) = - a"
1.142 -      by (simp only: add.assoc)
1.143 -    then have a: "- a = a"
1.144 -      by simp
1.145 -    show ?thesis
1.146 -      apply (rule antisym)
1.147 -      apply (unfold neg_le_iff_le [symmetric, of a])
1.148 -      unfolding a
1.149 -      apply simp
1.151 -      unfolding that
1.152 -      unfolding le_less
1.153 -      apply simp_all
1.154 -      done
1.155 -  qed
1.156 -  show ?lhs if ?rhs
1.157 -    using that by simp
1.158 -qed
1.159 +  using add_nonneg_eq_0_iff eq_iff by auto
1.160
1.161  lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a"
1.162 -proof (cases "a = 0")
1.163 -  case True
1.164 -  then show ?thesis by auto
1.165 -next
1.166 -  case False
1.167 -  then show ?thesis
1.168 -    unfolding less_le
1.169 -    apply simp
1.170 -    apply rule
1.171 -    apply clarify
1.172 -    apply rule
1.173 -    apply assumption
1.174 -    apply (rule notI)
1.175 -    unfolding double_zero [symmetric, of a]
1.176 -    apply blast
1.177 -    done
1.178 -qed
1.179 +  by (meson le_less_trans less_add_same_cancel2 less_le_not_le
1.181
1.182  lemma double_add_le_zero_iff_single_add_le_zero [simp]: "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
1.183  proof -
1.184 @@ -302,7 +257,10 @@
1.185      by blast
1.186  qed
1.187
1.188 -declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp] diff_inf_eq_sup [simp] diff_sup_eq_inf [simp]
1.189 +declare neg_inf_eq_sup [simp]
1.190 +  and neg_sup_eq_inf [simp]
1.191 +  and diff_inf_eq_sup [simp]
1.192 +  and diff_sup_eq_inf [simp]
1.193
1.194  lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0"
1.195  proof -
1.196 @@ -405,7 +363,7 @@
1.197      from a d e have "\<bar>a + b\<bar> \<le> sup ?m ?n"
1.198        apply -
1.199        apply (drule abs_leI)
1.200 -      apply (simp_all only: algebra_simps minus_add)
1.201 +       apply (simp_all only: algebra_simps minus_add)
1.203        done
1.204      with g[symmetric] show ?thesis by simp
1.205 @@ -606,15 +564,13 @@
1.206
1.207  instance int :: lattice_ring
1.208  proof
1.209 -  fix k :: int
1.210 -  show "\<bar>k\<bar> = sup k (- k)"
1.211 +  show "\<bar>k\<bar> = sup k (- k)" for k :: int
1.212      by (auto simp add: sup_int_def)
1.213  qed
1.214
1.215  instance real :: lattice_ring
1.216  proof
1.217 -  fix a :: real
1.218 -  show "\<bar>a\<bar> = sup a (- a)"
1.219 +  show "\<bar>a\<bar> = sup a (- a)" for a :: real
1.220      by (auto simp add: sup_real_def)
1.221  qed
1.222
```