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.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.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.22 +  apply (rule le_supI)
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.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.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.48    hence "0 = (-a + sup a b) + (inf a b + (-b))"
1.50 -  thus ?thesis by (simp add: algebra_simps)
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.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.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.96  qed
1.97
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.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.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.126 -    apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
1.127 +    apply simp
1.129      done
1.130    have yx: "?y <= ?x"
1.133 -    apply (simp_all add: mult_nonneg_nonpos mult_nonpos_nonneg)
1.134 +    apply simp
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 +
```