tuned proof
authorhaftmann
Mon Jan 19 08:16:42 2009 +0100 (2009-01-19)
changeset 295575362cc5ee3a8
parent 29556 7c128276aa93
child 29558 9846af6c6d6a
tuned proof
src/HOL/OrderedGroup.thy
     1.1 --- a/src/HOL/OrderedGroup.thy	Sun Jan 18 21:40:53 2009 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Mon Jan 19 08:16:42 2009 +0100
     1.3 @@ -1231,7 +1231,7 @@
     1.4  qed
     1.5  
     1.6  subclass pordered_ab_group_add_abs
     1.7 -proof -
     1.8 +proof
     1.9    have abs_ge_zero [simp]: "\<And>a. 0 \<le> \<bar>a\<bar>"
    1.10    proof -
    1.11      fix a b
    1.12 @@ -1240,37 +1240,26 @@
    1.13    qed
    1.14    have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
    1.15      by (simp add: abs_lattice le_supI)
    1.16 -  show ?thesis
    1.17 -  proof
    1.18 -    fix a
    1.19 -    show "0 \<le> \<bar>a\<bar>" by simp
    1.20 -  next
    1.21 -    fix a
    1.22 -    show "a \<le> \<bar>a\<bar>"
    1.23 -      by (auto simp add: abs_lattice)
    1.24 -  next
    1.25 -    fix a
    1.26 -    show "\<bar>-a\<bar> = \<bar>a\<bar>"
    1.27 -      by (simp add: abs_lattice sup_commute)
    1.28 -  next
    1.29 -    fix a b
    1.30 -    show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (erule abs_leI)
    1.31 -  next
    1.32 -    fix a b
    1.33 -    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
    1.34 -    proof -
    1.35 -      have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
    1.36 -        by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus)
    1.37 -      have a:"a+b <= sup ?m ?n" by (simp)
    1.38 -      have b:"-a-b <= ?n" by (simp) 
    1.39 -      have c:"?n <= sup ?m ?n" by (simp)
    1.40 -      from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
    1.41 -      have e:"-a-b = -(a+b)" by (simp add: diff_minus)
    1.42 -      from a d e have "abs(a+b) <= sup ?m ?n" 
    1.43 -        by (drule_tac abs_leI, auto)
    1.44 -      with g[symmetric] show ?thesis by simp
    1.45 -    qed
    1.46 -  qed auto
    1.47 +  fix a b
    1.48 +  show "0 \<le> \<bar>a\<bar>" by simp
    1.49 +  show "a \<le> \<bar>a\<bar>"
    1.50 +    by (auto simp add: abs_lattice)
    1.51 +  show "\<bar>-a\<bar> = \<bar>a\<bar>"
    1.52 +    by (simp add: abs_lattice sup_commute)
    1.53 +  show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (fact abs_leI)
    1.54 +  show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
    1.55 +  proof -
    1.56 +    have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
    1.57 +      by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus)
    1.58 +    have a:"a+b <= sup ?m ?n" by (simp)
    1.59 +    have b:"-a-b <= ?n" by (simp) 
    1.60 +    have c:"?n <= sup ?m ?n" by (simp)
    1.61 +    from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
    1.62 +    have e:"-a-b = -(a+b)" by (simp add: diff_minus)
    1.63 +    from a d e have "abs(a+b) <= sup ?m ?n" 
    1.64 +      by (drule_tac abs_leI, auto)
    1.65 +    with g[symmetric] show ?thesis by simp
    1.66 +  qed
    1.67  qed
    1.68  
    1.69  end