src/HOL/SupInf.thy
changeset 36777 be5461582d0f
parent 36007 095b1022e2ae
child 37765 26bdfb7b680b
     1.1 --- a/src/HOL/SupInf.thy	Sun May 09 14:21:44 2010 -0700
     1.2 +++ b/src/HOL/SupInf.thy	Sun May 09 17:47:43 2010 -0700
     1.3 @@ -74,7 +74,7 @@
     1.4  lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
     1.5    fixes x :: real
     1.6    shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
     1.7 -  by (metis Sup_upper real_le_trans)
     1.8 +  by (metis Sup_upper order_trans)
     1.9  
    1.10  lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
    1.11    fixes z :: real
    1.12 @@ -86,7 +86,7 @@
    1.13    shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a) 
    1.14          \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
    1.15    by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
    1.16 -        insert_not_empty real_le_antisym)
    1.17 +        insert_not_empty order_antisym)
    1.18  
    1.19  lemma Sup_le:
    1.20    fixes S :: "real set"
    1.21 @@ -109,28 +109,28 @@
    1.22      apply (simp add: max_def)
    1.23      apply (rule Sup_eq_maximum)
    1.24      apply (rule insertI1)
    1.25 -    apply (metis Sup_upper [OF _ z] insertE real_le_linear real_le_trans)
    1.26 +    apply (metis Sup_upper [OF _ z] insertE linear order_trans)
    1.27      done
    1.28  next
    1.29    case False
    1.30    hence 1:"a < Sup X" by simp
    1.31    have "Sup X \<le> Sup (insert a X)"
    1.32      apply (rule Sup_least)
    1.33 -    apply (metis empty_psubset_nonempty psubset_eq x)
    1.34 +    apply (metis ex_in_conv x)
    1.35      apply (rule Sup_upper_EX) 
    1.36      apply blast
    1.37 -    apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
    1.38 +    apply (metis insert_iff linear order_refl order_trans z)
    1.39      done
    1.40    moreover 
    1.41    have "Sup (insert a X) \<le> Sup X"
    1.42      apply (rule Sup_least)
    1.43      apply blast
    1.44 -    apply (metis False Sup_upper insertE real_le_linear z) 
    1.45 +    apply (metis False Sup_upper insertE linear z)
    1.46      done
    1.47    ultimately have "Sup (insert a X) = Sup X"
    1.48      by (blast intro:  antisym )
    1.49    thus ?thesis
    1.50 -    by (metis 1 min_max.le_iff_sup real_less_def)
    1.51 +    by (metis 1 min_max.le_iff_sup less_le)
    1.52  qed
    1.53  
    1.54  lemma Sup_insert_if: 
    1.55 @@ -177,7 +177,7 @@
    1.56    fixes S :: "real set"
    1.57    assumes fS: "finite S" and Se: "S \<noteq> {}"
    1.58    shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
    1.59 -by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS real_le_trans)
    1.60 +by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS order_trans)
    1.61  
    1.62  lemma Sup_finite_gt_iff: 
    1.63    fixes S :: "real set"
    1.64 @@ -291,19 +291,19 @@
    1.65  lemma Inf_lower2:
    1.66    fixes x :: real
    1.67    shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
    1.68 -  by (metis Inf_lower real_le_trans)
    1.69 +  by (metis Inf_lower order_trans)
    1.70  
    1.71  lemma Inf_real_iff:
    1.72    fixes z :: real
    1.73    shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y"
    1.74 -  by (metis Inf_greatest Inf_lower less_le_not_le real_le_linear 
    1.75 +  by (metis Inf_greatest Inf_lower less_le_not_le linear
    1.76              order_less_le_trans)
    1.77  
    1.78  lemma Inf_eq:
    1.79    fixes a :: real
    1.80    shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a"
    1.81    by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
    1.82 -        insert_absorb insert_not_empty real_le_antisym)
    1.83 +        insert_absorb insert_not_empty order_antisym)
    1.84  
    1.85  lemma Inf_ge: 
    1.86    fixes S :: "real set"
    1.87 @@ -324,27 +324,27 @@
    1.88    case True
    1.89    thus ?thesis
    1.90      by (simp add: min_def)
    1.91 -       (blast intro: Inf_eq_minimum real_le_refl real_le_trans z)
    1.92 +       (blast intro: Inf_eq_minimum order_trans z)
    1.93  next
    1.94    case False
    1.95    hence 1:"Inf X < a" by simp
    1.96    have "Inf (insert a X) \<le> Inf X"
    1.97      apply (rule Inf_greatest)
    1.98 -    apply (metis empty_psubset_nonempty psubset_eq x)
    1.99 +    apply (metis ex_in_conv x)
   1.100      apply (rule Inf_lower_EX)
   1.101      apply (erule insertI2)
   1.102 -    apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
   1.103 +    apply (metis insert_iff linear order_refl order_trans z)
   1.104      done
   1.105    moreover 
   1.106    have "Inf X \<le> Inf (insert a X)"
   1.107      apply (rule Inf_greatest)
   1.108      apply blast
   1.109 -    apply (metis False Inf_lower insertE real_le_linear z) 
   1.110 +    apply (metis False Inf_lower insertE linear z) 
   1.111      done
   1.112    ultimately have "Inf (insert a X) = Inf X"
   1.113      by (blast intro:  antisym )
   1.114    thus ?thesis
   1.115 -    by (metis False min_max.inf_absorb2 real_le_linear)
   1.116 +    by (metis False min_max.inf_absorb2 linear)
   1.117  qed
   1.118  
   1.119  lemma Inf_insert_if: 
   1.120 @@ -377,13 +377,13 @@
   1.121  lemma Inf_finite_ge_iff: 
   1.122    fixes S :: "real set"
   1.123    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
   1.124 -by (metis Inf_finite_Min Inf_finite_in Min_le real_le_trans)
   1.125 +by (metis Inf_finite_Min Inf_finite_in Min_le order_trans)
   1.126  
   1.127  lemma Inf_finite_le_iff:
   1.128    fixes S :: "real set"
   1.129    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
   1.130  by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
   1.131 -          real_le_antisym real_le_linear)
   1.132 +          order_antisym linear)
   1.133  
   1.134  lemma Inf_finite_gt_iff: 
   1.135    fixes S :: "real set"
   1.136 @@ -417,7 +417,7 @@
   1.137    also have "... \<le> e" 
   1.138      apply (rule Sup_asclose) 
   1.139      apply (auto simp add: S)
   1.140 -    apply (metis abs_minus_add_cancel b add_commute real_diff_def) 
   1.141 +    apply (metis abs_minus_add_cancel b add_commute diff_def)
   1.142      done
   1.143    finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
   1.144    thus ?thesis
   1.145 @@ -474,13 +474,13 @@
   1.146  proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
   1.147    show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   1.148      by (rule SupInf.Sup_upper [where z=b], auto)
   1.149 -       (metis `a < b` `\<not> P b` real_le_linear real_less_def)
   1.150 +       (metis `a < b` `\<not> P b` linear less_le)
   1.151  next
   1.152    show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
   1.153      apply (rule SupInf.Sup_least) 
   1.154      apply (auto simp add: )
   1.155      apply (metis less_le_not_le)
   1.156 -    apply (metis `a<b` `~ P b` real_le_linear real_less_def) 
   1.157 +    apply (metis `a<b` `~ P b` linear less_le)
   1.158      done
   1.159  next
   1.160    fix x
   1.161 @@ -495,7 +495,7 @@
   1.162      assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
   1.163      thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
   1.164        by (rule_tac z="b" in SupInf.Sup_upper, auto) 
   1.165 -         (metis `a<b` `~ P b` real_le_linear real_less_def) 
   1.166 +         (metis `a<b` `~ P b` linear less_le)
   1.167  qed
   1.168  
   1.169  end