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.7 -  moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by (simp add: zero_le_double_add_iff_zero_le_single_add)
     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.16 -  moreover have "\<dots> \<longleftrightarrow> a < 0" by (simp add: zero_less_double_add_iff_zero_less_single_add)
    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.45          apply (auto simp add: 
    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.59      by (simp add: algebra_simps)
    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)