equal
deleted
inserted
replaced
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 |