# HG changeset patch # User haftmann # Date 1232349402 -3600 # Node ID 5362cc5ee3a87b07b81247dbb03c5ba782b0b803 # Parent 7c128276aa938d6bb482d189617c9832facff254 tuned proof diff -r 7c128276aa93 -r 5362cc5ee3a8 src/HOL/OrderedGroup.thy --- a/src/HOL/OrderedGroup.thy Sun Jan 18 21:40:53 2009 +0100 +++ b/src/HOL/OrderedGroup.thy Mon Jan 19 08:16:42 2009 +0100 @@ -1231,7 +1231,7 @@ qed subclass pordered_ab_group_add_abs -proof - +proof have abs_ge_zero [simp]: "\a. 0 \ \a\" proof - fix a b @@ -1240,37 +1240,26 @@ qed have abs_leI: "\a b. a \ b \ - a \ b \ \a\ \ b" by (simp add: abs_lattice le_supI) - show ?thesis - proof - fix a - show "0 \ \a\" by simp - next - fix a - show "a \ \a\" - by (auto simp add: abs_lattice) - next - fix a - show "\-a\ = \a\" - by (simp add: abs_lattice sup_commute) - next - fix a b - show "a \ b \ - a \ b \ \a\ \ b" by (erule abs_leI) - next - fix a b - show "\a + b\ \ \a\ + \b\" - proof - - have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n") - by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus) - have a:"a+b <= sup ?m ?n" by (simp) - have b:"-a-b <= ?n" by (simp) - have c:"?n <= sup ?m ?n" by (simp) - from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans) - have e:"-a-b = -(a+b)" by (simp add: diff_minus) - from a d e have "abs(a+b) <= sup ?m ?n" - by (drule_tac abs_leI, auto) - with g[symmetric] show ?thesis by simp - qed - qed auto + fix a b + show "0 \ \a\" by simp + show "a \ \a\" + by (auto simp add: abs_lattice) + show "\-a\ = \a\" + by (simp add: abs_lattice sup_commute) + show "a \ b \ - a \ b \ \a\ \ b" by (fact abs_leI) + show "\a + b\ \ \a\ + \b\" + proof - + have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n") + by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus) + have a:"a+b <= sup ?m ?n" by (simp) + have b:"-a-b <= ?n" by (simp) + have c:"?n <= sup ?m ?n" by (simp) + from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans) + have e:"-a-b = -(a+b)" by (simp add: diff_minus) + from a d e have "abs(a+b) <= sup ?m ?n" + by (drule_tac abs_leI, auto) + with g[symmetric] show ?thesis by simp + qed qed end