src/HOL/Arith_Tools.thy
 changeset 23901 7392193f9ecf parent 23881 851c74f1bb69 child 24075 366d4d234814
equal 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`