src/HOL/Ring_and_Field.thy
changeset 24422 c0b5ff9e9e4d
parent 24286 7619080e49f0
child 24427 bc5cf3b09ff3
     1.1 --- a/src/HOL/Ring_and_Field.thy	Fri Aug 24 14:14:17 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Aug 24 14:14:18 2007 +0200
     1.3 @@ -325,6 +325,11 @@
     1.4    (*previously ordered_semiring*)
     1.5    assumes zero_less_one [simp]: "\<^loc>0 \<sqsubset> \<^loc>1"
     1.6  
     1.7 +lemma pos_add_strict:
     1.8 +  fixes a b c :: "'a\<Colon>ordered_semidom"
     1.9 +  shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
    1.10 +  using add_strict_mono [of 0 a b c] by simp
    1.11 +
    1.12  class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + lordered_ab_group + abs_if
    1.13    (*previously ordered_ring*)
    1.14  
    1.15 @@ -1878,8 +1883,15 @@
    1.16  lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::ordered_field) < b"
    1.17  by (simp add: field_simps zero_less_two)
    1.18  
    1.19 -lemma dense: "a < b ==> \<exists>r::'a::ordered_field. a < r & r < b"
    1.20 -by (blast intro!: less_half_sum gt_half_sum)
    1.21 +instance ordered_field < dense_linear_order
    1.22 +proof
    1.23 +  fix x y :: 'a
    1.24 +  have "x < x + 1" by simp
    1.25 +  then show "\<exists>y. x < y" .. 
    1.26 +  have "x - 1 < x" by simp
    1.27 +  then show "\<exists>y. y < x" ..
    1.28 +  show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
    1.29 +qed
    1.30  
    1.31  
    1.32  subsection {* Absolute Value *}