tuned proofs;
authorwenzelm
Wed Mar 08 10:50:59 2017 +0100 (2017-03-08)
changeset 65151a7394aa4d21c
parent 65150 fa299b4e50c3
child 65152 a920012ae16a
tuned proofs;
src/HOL/Library/Lattice_Algebras.thy
     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.11  class semilattice_inf_ab_group_add = ordered_ab_group_add + semilattice_inf
    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.19    apply (simp only: add.assoc [symmetric], simp add: diff_le_eq add.commute)
    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.27 -  apply (simp add: le_diff_eq add.commute)
    1.28 +   apply (rule add_le_imp_le_left [of "uminus a"])
    1.29 +   apply (simp only: add.assoc [symmetric], simp)
    1.30 +   apply (simp add: le_diff_eq add.commute)
    1.31    apply (rule le_supI)
    1.32 -  apply (rule add_le_imp_le_left [of "a"], simp only: add.assoc[symmetric], simp)+
    1.33 +   apply (rule add_le_imp_le_left [of "a"], simp only: add.assoc[symmetric], simp)+
    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.40        (simp, simp add: add_inf_distrib_left)
    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.66    by (simp add: nprt_def)
    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.76 -    apply (simp add: add.assoc)
    1.77 -    done
    1.78 +  assume ?lhs
    1.79 +  show ?rhs
    1.80 +    by (rule add_le_imp_le_right[of _ "uminus b" _]) (simp add: add.assoc \<open>?lhs\<close>)
    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.90 +    by (rule add_le_imp_le_right[of _ "b" _]) (simp add: \<open>?rhs\<close>)
    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.106      by (simp add: sup_commute)
   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.150 -      unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a]
   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.180 +      zero_le_double_add_iff_zero_le_single_add)
   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.202        apply (metis add_uminus_conv_diff d sup_commute uminus_add_conv_diff)
   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