--- a/src/HOL/Ring_and_Field.thy Fri Feb 05 14:33:50 2010 +0100
+++ b/src/HOL/Ring_and_Field.thy Mon Feb 08 14:06:41 2010 +0100
@@ -2143,100 +2143,6 @@
assumes abs_eq_mult:
"(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0) \<Longrightarrow> \<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
-
-class lattice_ring = ordered_ring + lattice_ab_group_add_abs
-begin
-
-subclass semilattice_inf_ab_group_add ..
-subclass semilattice_sup_ab_group_add ..
-
-end
-
-lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lattice_ring))"
-proof -
- let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
- let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
- have a: "(abs a) * (abs b) = ?x"
- by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps)
- {
- fix u v :: 'a
- have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow>
- u * v = pprt a * pprt b + pprt a * nprt b +
- nprt a * pprt b + nprt a * nprt b"
- apply (subst prts[of u], subst prts[of v])
- apply (simp add: algebra_simps)
- done
- }
- note b = this[OF refl[of a] refl[of b]]
- note addm = add_mono[of "0::'a" _ "0::'a", simplified]
- note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]
- have xy: "- ?x <= ?y"
- apply (simp)
- apply (rule_tac y="0::'a" in order_trans)
- apply (rule addm2)
- apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
- apply (rule addm)
- apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
- done
- have yx: "?y <= ?x"
- apply (simp add:diff_def)
- apply (rule_tac y=0 in order_trans)
- apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
- apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
- done
- have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
- have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
- show ?thesis
- apply (rule abs_leI)
- apply (simp add: i1)
- apply (simp add: i2[simplified minus_le_iff])
- done
-qed
-
-instance lattice_ring \<subseteq> ordered_ring_abs
-proof
- fix a b :: "'a\<Colon> lattice_ring"
- assume "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
- show "abs (a*b) = abs a * abs b"
-proof -
- have s: "(0 <= a*b) | (a*b <= 0)"
- apply (auto)
- apply (rule_tac split_mult_pos_le)
- apply (rule_tac contrapos_np[of "a*b <= 0"])
- apply (simp)
- apply (rule_tac split_mult_neg_le)
- apply (insert prems)
- apply (blast)
- done
- have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
- by (simp add: prts[symmetric])
- show ?thesis
- proof cases
- assume "0 <= a * b"
- then show ?thesis
- apply (simp_all add: mulprts abs_prts)
- apply (insert prems)
- apply (auto simp add:
- algebra_simps
- iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
- iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
- apply(drule (1) mult_nonneg_nonpos[of a b], simp)
- apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
- done
- next
- assume "~(0 <= a*b)"
- with s have "a*b <= 0" by simp
- then show ?thesis
- apply (simp_all add: mulprts abs_prts)
- apply (insert prems)
- apply (auto simp add: algebra_simps)
- apply(drule (1) mult_nonneg_nonneg[of a b],simp)
- apply(drule (1) mult_nonpos_nonpos[of a b],simp)
- done
- qed
-qed
-qed
-
context linordered_idom
begin
@@ -2308,76 +2214,6 @@
apply (simp add: order_less_imp_le)
done
-
-subsection {* Bounds of products via negative and positive Part *}
-
-lemma mult_le_prts:
- assumes
- "a1 <= (a::'a::lattice_ring)"
- "a <= a2"
- "b1 <= b"
- "b <= b2"
- shows
- "a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
-proof -
- have "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
- apply (subst prts[symmetric])+
- apply simp
- done
- then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
- by (simp add: algebra_simps)
- moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
- by (simp_all add: prems mult_mono)
- moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
- proof -
- have "pprt a * nprt b <= pprt a * nprt b2"
- by (simp add: mult_left_mono prems)
- moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
- by (simp add: mult_right_mono_neg prems)
- ultimately show ?thesis
- by simp
- qed
- moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
- proof -
- have "nprt a * pprt b <= nprt a2 * pprt b"
- by (simp add: mult_right_mono prems)
- moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
- by (simp add: mult_left_mono_neg prems)
- ultimately show ?thesis
- by simp
- qed
- moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
- proof -
- have "nprt a * nprt b <= nprt a * nprt b1"
- by (simp add: mult_left_mono_neg prems)
- moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
- by (simp add: mult_right_mono_neg prems)
- ultimately show ?thesis
- by simp
- qed
- ultimately show ?thesis
- by - (rule add_mono | simp)+
-qed
-
-lemma mult_ge_prts:
- assumes
- "a1 <= (a::'a::lattice_ring)"
- "a <= a2"
- "b1 <= b"
- "b <= b2"
- shows
- "a * b >= nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
-proof -
- from prems have a1:"- a2 <= -a" by auto
- from prems have a2: "-a <= -a1" by auto
- from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg]
- have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1" by simp
- then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
- by (simp only: minus_le_iff)
- then show ?thesis by simp
-qed
-
-
code_modulename SML
Ring_and_Field Arith