src/HOL/Library/Lattice_Algebras.thy
 changeset 41528 276078f01ada parent 37884 314a88278715 child 46986 8198cbff1771
```     1.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Wed Jan 12 16:41:49 2011 +0100
1.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Wed Jan 12 17:14:27 2011 +0100
1.3 @@ -253,7 +253,7 @@
1.4    "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
1.5  proof -
1.6    have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)" by (subst le_minus_iff, simp)
1.8 +  moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by simp
1.9    ultimately show ?thesis by blast
1.10  qed
1.11
1.12 @@ -261,7 +261,7 @@
1.13    "a + a < 0 \<longleftrightarrow> a < 0"
1.14  proof -
1.15    have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)" by (subst less_minus_iff, simp)
1.17 +  moreover have "\<dots> \<longleftrightarrow> a < 0" by simp
1.18    ultimately show ?thesis by blast
1.19  qed
1.20
1.21 @@ -428,7 +428,7 @@
1.22  instance lattice_ring \<subseteq> ordered_ring_abs
1.23  proof
1.24    fix a b :: "'a\<Colon> lattice_ring"
1.25 -  assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
1.26 +  assume a: "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
1.27    show "abs (a*b) = abs a * abs b"
1.28    proof -
1.29      have s: "(0 <= a*b) | (a*b <= 0)"
1.30 @@ -437,7 +437,7 @@
1.31        apply (rule_tac contrapos_np[of "a*b <= 0"])
1.32        apply (simp)
1.33        apply (rule_tac split_mult_neg_le)
1.34 -      apply (insert prems)
1.35 +      apply (insert a)
1.36        apply (blast)
1.37        done
1.38      have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
1.39 @@ -447,7 +447,7 @@
1.40        assume "0 <= a * b"
1.41        then show ?thesis
1.42          apply (simp_all add: mulprts abs_prts)
1.43 -        apply (insert prems)
1.44 +        apply (insert a)
1.46            algebra_simps
1.47            iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
1.48 @@ -460,7 +460,7 @@
1.49        with s have "a*b <= 0" by simp
1.50        then show ?thesis
1.51          apply (simp_all add: mulprts abs_prts)
1.52 -        apply (insert prems)
1.53 +        apply (insert a)
1.54          apply (auto simp add: algebra_simps)
1.55          apply(drule (1) mult_nonneg_nonneg[of a b],simp)
1.56          apply(drule (1) mult_nonpos_nonpos[of a b],simp)
1.57 @@ -485,31 +485,31 @@
1.58    then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
1.60    moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
1.61 -    by (simp_all add: prems mult_mono)
1.62 +    by (simp_all add: assms mult_mono)
1.63    moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
1.64    proof -
1.65      have "pprt a * nprt b <= pprt a * nprt b2"
1.66 -      by (simp add: mult_left_mono prems)
1.67 +      by (simp add: mult_left_mono assms)
1.68      moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
1.69 -      by (simp add: mult_right_mono_neg prems)
1.70 +      by (simp add: mult_right_mono_neg assms)
1.71      ultimately show ?thesis
1.72        by simp
1.73    qed
1.74    moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
1.75    proof -
1.76      have "nprt a * pprt b <= nprt a2 * pprt b"
1.77 -      by (simp add: mult_right_mono prems)
1.78 +      by (simp add: mult_right_mono assms)
1.79      moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
1.80 -      by (simp add: mult_left_mono_neg prems)
1.81 +      by (simp add: mult_left_mono_neg assms)
1.82      ultimately show ?thesis
1.83        by simp
1.84    qed
1.85    moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
1.86    proof -
1.87      have "nprt a * nprt b <= nprt a * nprt b1"
1.88 -      by (simp add: mult_left_mono_neg prems)
1.89 +      by (simp add: mult_left_mono_neg assms)
1.90      moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
1.91 -      by (simp add: mult_right_mono_neg prems)
1.92 +      by (simp add: mult_right_mono_neg assms)
1.93      ultimately show ?thesis
1.94        by simp
1.95    qed
1.96 @@ -526,9 +526,9 @@
1.97    shows
1.98    "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
1.99  proof -
1.100 -  from prems have a1:"- a2 <= -a" by auto
1.101 -  from prems have a2: "-a <= -a1" by auto
1.102 -  from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg]
1.103 +  from assms have a1:"- a2 <= -a" by auto
1.104 +  from assms have a2: "-a <= -a1" by auto
1.105 +  from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg]
1.106    have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp
1.107    then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
1.108      by (simp only: minus_le_iff)
```