src/HOL/Library/Lattice_Algebras.thy
changeset 54230 b1d955791529
parent 53240 07593a0a27f4
child 54863 82acc20ded73
     1.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Thu Oct 31 16:54:22 2013 +0100
     1.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Fri Nov 01 18:51:14 2013 +0100
     1.3 @@ -13,9 +13,7 @@
     1.4    apply (rule antisym)
     1.5    apply (simp_all add: le_infI)
     1.6    apply (rule add_le_imp_le_left [of "uminus a"])
     1.7 -  apply (simp only: add_assoc [symmetric], simp)
     1.8 -  apply rule
     1.9 -  apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+
    1.10 +  apply (simp only: add_assoc [symmetric], simp add: diff_le_eq add.commute)
    1.11    done
    1.12  
    1.13  lemma add_inf_distrib_right: "inf a b + c = inf (a + c) (b + c)"
    1.14 @@ -33,11 +31,10 @@
    1.15  lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a + c)"
    1.16    apply (rule antisym)
    1.17    apply (rule add_le_imp_le_left [of "uminus a"])
    1.18 -  apply (simp only: add_assoc[symmetric], simp)
    1.19 -  apply rule
    1.20 +  apply (simp only: add_assoc [symmetric], simp)
    1.21 +  apply (simp add: le_diff_eq add.commute)
    1.22 +  apply (rule le_supI)
    1.23    apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
    1.24 -  apply (rule le_supI)
    1.25 -  apply (simp_all)
    1.26    done
    1.27  
    1.28  lemma add_sup_distrib_right: "sup a b + c = sup (a+c) (b+c)"
    1.29 @@ -87,9 +84,15 @@
    1.30  lemma neg_inf_eq_sup: "- inf a b = sup (-a) (-b)"
    1.31    by (simp add: inf_eq_neg_sup)
    1.32  
    1.33 +lemma diff_inf_eq_sup: "a - inf b c = a + sup (- b) (- c)"
    1.34 +  using neg_inf_eq_sup [of b c, symmetric] by simp
    1.35 +
    1.36  lemma neg_sup_eq_inf: "- sup a b = inf (-a) (-b)"
    1.37    by (simp add: sup_eq_neg_inf)
    1.38  
    1.39 +lemma diff_sup_eq_inf: "a - sup b c = a + inf (- b) (- c)"
    1.40 +  using neg_sup_eq_inf [of b c, symmetric] by simp
    1.41 +
    1.42  lemma add_eq_inf_sup: "a + b = sup a b + inf a b"
    1.43  proof -
    1.44    have "0 = - inf 0 (a-b) + inf (a-b) 0"
    1.45 @@ -97,8 +100,8 @@
    1.46    hence "0 = sup 0 (b-a) + inf (a-b) 0"
    1.47      by (simp add: inf_eq_neg_sup)
    1.48    hence "0 = (-a + sup a b) + (inf a b + (-b))"
    1.49 -    by (simp add: add_sup_distrib_left add_inf_distrib_right) (simp add: algebra_simps)
    1.50 -  thus ?thesis by (simp add: algebra_simps)
    1.51 +    by (simp only: add_sup_distrib_left add_inf_distrib_right) simp
    1.52 +  then show ?thesis by (simp add: algebra_simps)
    1.53  qed
    1.54  
    1.55  
    1.56 @@ -251,7 +254,7 @@
    1.57      apply assumption
    1.58      apply (rule notI)
    1.59      unfolding double_zero [symmetric, of a]
    1.60 -    apply simp
    1.61 +    apply blast
    1.62      done
    1.63  qed
    1.64  
    1.65 @@ -259,7 +262,8 @@
    1.66    "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
    1.67  proof -
    1.68    have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)" by (subst le_minus_iff, simp)
    1.69 -  moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by simp
    1.70 +  moreover have "\<dots> \<longleftrightarrow> a \<le> 0"
    1.71 +    by (simp only: minus_add_distrib zero_le_double_add_iff_zero_le_single_add) simp
    1.72    ultimately show ?thesis by blast
    1.73  qed
    1.74  
    1.75 @@ -267,11 +271,12 @@
    1.76    "a + a < 0 \<longleftrightarrow> a < 0"
    1.77  proof -
    1.78    have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)" by (subst less_minus_iff, simp)
    1.79 -  moreover have "\<dots> \<longleftrightarrow> a < 0" by simp
    1.80 +  moreover have "\<dots> \<longleftrightarrow> a < 0"
    1.81 +    by (simp only: minus_add_distrib zero_less_double_add_iff_zero_less_single_add) simp
    1.82    ultimately show ?thesis by blast
    1.83  qed
    1.84  
    1.85 -declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp]
    1.86 +declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp] diff_inf_eq_sup [simp] diff_sup_eq_inf [simp]
    1.87  
    1.88  lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0"
    1.89  proof -
    1.90 @@ -326,7 +331,7 @@
    1.91    then have "0 \<le> sup a (- a)" unfolding abs_lattice .
    1.92    then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
    1.93    then show ?thesis
    1.94 -    by (simp add: add_sup_inf_distribs sup_aci pprt_def nprt_def diff_minus abs_lattice)
    1.95 +    by (simp add: add_sup_inf_distribs ac_simps pprt_def nprt_def abs_lattice)
    1.96  qed
    1.97  
    1.98  subclass ordered_ab_group_add_abs
    1.99 @@ -355,16 +360,17 @@
   1.100    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   1.101    proof -
   1.102      have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
   1.103 -      by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)
   1.104 +      by (simp add: abs_lattice add_sup_inf_distribs sup_aci ac_simps)
   1.105      have a: "a + b <= sup ?m ?n" by simp
   1.106      have b: "- a - b <= ?n" by simp
   1.107      have c: "?n <= sup ?m ?n" by simp
   1.108      from b c have d: "-a-b <= sup ?m ?n" by (rule order_trans)
   1.109 -    have e:"-a-b = -(a+b)" by (simp add: diff_minus)
   1.110 +    have e:"-a-b = -(a+b)" by simp
   1.111      from a d e have "abs(a+b) <= sup ?m ?n"
   1.112        apply -
   1.113        apply (drule abs_leI)
   1.114 -      apply auto
   1.115 +      apply (simp_all only: algebra_simps ac_simps minus_add)
   1.116 +      apply (metis add_uminus_conv_diff d sup_commute uminus_add_conv_diff)
   1.117        done
   1.118      with g[symmetric] show ?thesis by simp
   1.119    qed
   1.120 @@ -421,14 +427,12 @@
   1.121    }
   1.122    note b = this[OF refl[of a] refl[of b]]
   1.123    have xy: "- ?x <= ?y"
   1.124 -    apply (simp)
   1.125 -    apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
   1.126 -    apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
   1.127 +    apply simp
   1.128 +    apply (metis (full_types) add_increasing add_uminus_conv_diff lattice_ab_group_add_class.minus_le_self_iff minus_add_distrib mult_nonneg_nonneg mult_nonpos_nonpos nprt_le_zero zero_le_pprt)
   1.129      done
   1.130    have yx: "?y <= ?x"
   1.131 -    apply (simp add:diff_minus)
   1.132 -    apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
   1.133 -    apply (simp_all add: mult_nonneg_nonpos mult_nonpos_nonneg)
   1.134 +    apply simp
   1.135 +    apply (metis (full_types) add_nonpos_nonpos add_uminus_conv_diff lattice_ab_group_add_class.le_minus_self_iff minus_add_distrib mult_nonneg_nonpos mult_nonpos_nonneg nprt_le_zero zero_le_pprt)
   1.136      done
   1.137    have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
   1.138    have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
   1.139 @@ -549,7 +553,7 @@
   1.140      by simp
   1.141    then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
   1.142      by (simp only: minus_le_iff)
   1.143 -  then show ?thesis by simp
   1.144 +  then show ?thesis by (simp add: algebra_simps)
   1.145  qed
   1.146  
   1.147  instance int :: lattice_ring
   1.148 @@ -567,3 +571,4 @@
   1.149  qed
   1.150  
   1.151  end
   1.152 +