src/HOL/Arith_Tools.thy
changeset 23901 7392193f9ecf
parent 23881 851c74f1bb69
child 24075 366d4d234814
equal deleted inserted replaced
23900:b25b1444a246 23901:7392193f9ecf
   695 qed
   695 qed
   696 lemma sum_eq:"((x::'a::pordered_ab_group_add) + t = 0) == (x = - t)"
   696 lemma sum_eq:"((x::'a::pordered_ab_group_add) + t = 0) == (x = - t)"
   697   using eq_diff_eq[where a= x and b=t and c=0] by simp
   697   using eq_diff_eq[where a= x and b=t and c=0] by simp
   698 
   698 
   699 
   699 
   700 interpretation class_ordered_field_dense_linear_order: dense_linear_order
   700 interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
   701  ["op <=" "op <"
   701  ["op <=" "op <"
   702    "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"]
   702    "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"]
   703 proof (unfold_locales,
   703 proof (unfold_locales, dlo, dlo, auto)
   704   simp_all only: ordered_field_no_ub ordered_field_no_lb,
       
   705     auto simp add: linorder_not_le)
       
   706   fix x y::'a assume lt: "x < y"
   704   fix x y::'a assume lt: "x < y"
   707   from  less_half_sum[OF lt] show "x < (x + y) /2" by simp
   705   from  less_half_sum[OF lt] show "x < (x + y) /2" by simp
   708 next
   706 next
   709   fix x y::'a assume lt: "x < y"
   707   fix x y::'a assume lt: "x < y"
   710   from  gt_half_sum[OF lt] show "(x + y) /2 < y" by simp
   708   from  gt_half_sum[OF lt] show "(x + y) /2 < y" by simp