Add dense_le, dense_le_bounded, field_le_mult_one_interval.
authorhoelzl
Thu Mar 04 18:42:39 2010 +0100 (2010-03-04)
changeset 35579cc9a5a0ab5ea
parent 35578 384ad08a1d1b
child 35580 0f74806cab22
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
src/HOL/Fields.thy
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Fields.thy	Thu Mar 04 17:28:45 2010 +0100
     1.2 +++ b/src/HOL/Fields.thy	Thu Mar 04 18:42:39 2010 +0100
     1.3 @@ -1034,30 +1034,33 @@
     1.4    apply (simp add: order_less_imp_le)
     1.5  done
     1.6  
     1.7 -
     1.8  lemma field_le_epsilon:
     1.9 -  fixes x y :: "'a :: {division_by_zero,linordered_field}"
    1.10 +  fixes x y :: "'a\<Colon>linordered_field"
    1.11    assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
    1.12    shows "x \<le> y"
    1.13 -proof (rule ccontr)
    1.14 -  obtain two :: 'a where two: "two = 1 + 1" by simp
    1.15 -  assume "\<not> x \<le> y"
    1.16 -  then have yx: "y < x" by simp
    1.17 -  then have "y + - y < x + - y" by (rule add_strict_right_mono)
    1.18 -  then have "x - y > 0" by (simp add: diff_minus)
    1.19 -  then have "(x - y) / two > 0"
    1.20 -    by (rule divide_pos_pos) (simp add: two)
    1.21 -  then have "x \<le> y + (x - y) / two" by (rule e)
    1.22 -  also have "... = (x - y + two * y) / two"
    1.23 -    by (simp add: add_divide_distrib two)
    1.24 -  also have "... = (x + y) / two" 
    1.25 -    by (simp add: two algebra_simps)
    1.26 -  also have "... < x" using yx
    1.27 -    by (simp add: two pos_divide_less_eq algebra_simps)
    1.28 -  finally have "x < x" .
    1.29 -  then show False ..
    1.30 +proof (rule dense_le)
    1.31 +  fix t assume "t < x"
    1.32 +  hence "0 < x - t" by (simp add: less_diff_eq)
    1.33 +  from e[OF this]
    1.34 +  show "t \<le> y" by (simp add: field_simps)
    1.35  qed
    1.36  
    1.37 +lemma field_le_mult_one_interval:
    1.38 +  fixes x :: "'a\<Colon>{linordered_field,division_by_zero}"
    1.39 +  assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
    1.40 +  shows "x \<le> y"
    1.41 +proof (cases "0 < x")
    1.42 +  assume "0 < x"
    1.43 +  thus ?thesis
    1.44 +    using dense_le_bounded[of 0 1 "y/x"] *
    1.45 +    unfolding le_divide_eq if_P[OF `0 < x`] by simp
    1.46 +next
    1.47 +  assume "\<not>0 < x" hence "x \<le> 0" by simp
    1.48 +  obtain s::'a where s: "0 < s" "s < 1" using dense[of 0 "1\<Colon>'a"] by auto
    1.49 +  hence "x \<le> s * x" using mult_le_cancel_right[of 1 x s] `x \<le> 0` by auto
    1.50 +  also note *[OF s]
    1.51 +  finally show ?thesis .
    1.52 +qed
    1.53  
    1.54  code_modulename SML
    1.55    Fields Arith
     2.1 --- a/src/HOL/Orderings.thy	Thu Mar 04 17:28:45 2010 +0100
     2.2 +++ b/src/HOL/Orderings.thy	Thu Mar 04 18:42:39 2010 +0100
     2.3 @@ -1097,7 +1097,43 @@
     2.4    assumes gt_ex: "\<exists>y. x < y" 
     2.5    and lt_ex: "\<exists>y. y < x"
     2.6    and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
     2.7 +begin
     2.8  
     2.9 +lemma dense_le:
    2.10 +  fixes y z :: 'a
    2.11 +  assumes "\<And>x. x < y \<Longrightarrow> x \<le> z"
    2.12 +  shows "y \<le> z"
    2.13 +proof (rule ccontr)
    2.14 +  assume "\<not> ?thesis"
    2.15 +  hence "z < y" by simp
    2.16 +  from dense[OF this]
    2.17 +  obtain x where "x < y" and "z < x" by safe
    2.18 +  moreover have "x \<le> z" using assms[OF `x < y`] .
    2.19 +  ultimately show False by auto
    2.20 +qed
    2.21 +
    2.22 +lemma dense_le_bounded:
    2.23 +  fixes x y z :: 'a
    2.24 +  assumes "x < y"
    2.25 +  assumes *: "\<And>w. \<lbrakk> x < w ; w < y \<rbrakk> \<Longrightarrow> w \<le> z"
    2.26 +  shows "y \<le> z"
    2.27 +proof (rule dense_le)
    2.28 +  fix w assume "w < y"
    2.29 +  from dense[OF `x < y`] obtain u where "x < u" "u < y" by safe
    2.30 +  from linear[of u w]
    2.31 +  show "w \<le> z"
    2.32 +  proof (rule disjE)
    2.33 +    assume "u \<le> w"
    2.34 +    from less_le_trans[OF `x < u` `u \<le> w`] `w < y`
    2.35 +    show "w \<le> z" by (rule *)
    2.36 +  next
    2.37 +    assume "w \<le> u"
    2.38 +    from `w \<le> u` *[OF `x < u` `u < y`]
    2.39 +    show "w \<le> z" by (rule order_trans)
    2.40 +  qed
    2.41 +qed
    2.42 +
    2.43 +end
    2.44  
    2.45  subsection {* Wellorders *}
    2.46