cleaned up some proofs
authorhuffman
Sun Mar 28 10:34:02 2010 -0700 (2010-03-28)
changeset 36007095b1022e2ae
parent 36002 f4f343500249
child 36008 23dfa8678c7c
cleaned up some proofs
src/HOL/SupInf.thy
     1.1 --- a/src/HOL/SupInf.thy	Sun Mar 28 17:43:09 2010 +0200
     1.2 +++ b/src/HOL/SupInf.thy	Sun Mar 28 10:34:02 2010 -0700
     1.3 @@ -106,10 +106,10 @@
     1.4  proof (cases "Sup X \<le> a")
     1.5    case True
     1.6    thus ?thesis
     1.7 -    apply (simp add: max_def) 
     1.8 +    apply (simp add: max_def)
     1.9      apply (rule Sup_eq_maximum)
    1.10 -    apply (metis insertCI)
    1.11 -    apply (metis Sup_upper insertE le_iff_sup real_le_linear real_le_trans sup_absorb1 z)     
    1.12 +    apply (rule insertI1)
    1.13 +    apply (metis Sup_upper [OF _ z] insertE real_le_linear real_le_trans)
    1.14      done
    1.15  next
    1.16    case False
    1.17 @@ -177,7 +177,7 @@
    1.18    fixes S :: "real set"
    1.19    assumes fS: "finite S" and Se: "S \<noteq> {}"
    1.20    shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
    1.21 -by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS le_iff_sup real_le_trans) 
    1.22 +by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS real_le_trans)
    1.23  
    1.24  lemma Sup_finite_gt_iff: 
    1.25    fixes S :: "real set"
    1.26 @@ -331,8 +331,8 @@
    1.27    have "Inf (insert a X) \<le> Inf X"
    1.28      apply (rule Inf_greatest)
    1.29      apply (metis empty_psubset_nonempty psubset_eq x)
    1.30 -    apply (rule Inf_lower_EX) 
    1.31 -    apply (blast intro: elim:) 
    1.32 +    apply (rule Inf_lower_EX)
    1.33 +    apply (erule insertI2)
    1.34      apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
    1.35      done
    1.36    moreover