1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Tue Jan 27 09:44:14 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Jan 27 15:39:51 2004 +0100
     1.3 @@ -82,7 +82,7 @@
     1.4                                 Y \<in> Rep_hypreal(Q) &
     1.5                                 {n::nat. X n < Y n} \<in> FreeUltrafilterNat"
     1.6    hypreal_le_def:
     1.7 -  "P <= (Q::hypreal) == ~(Q < P)"
     1.8 +  "P \<le> (Q::hypreal) == ~(Q < P)"
     1.9  
    1.10    hrabs_def:  "abs (r::hypreal) == (if 0 \<le> r then r else -r)"
    1.11  
    1.12 @@ -149,7 +149,7 @@
    1.13  done
    1.14  
    1.15  lemma FreeUltrafilterNat_subset:
    1.16 -     "[| X: FreeUltrafilterNat;  X <= Y |]  
    1.17 +     "[| X: FreeUltrafilterNat;  X \<subseteq> Y |]  
    1.18        ==> Y \<in> FreeUltrafilterNat"
    1.19  apply (cut_tac FreeUltrafilterNat_mem)
    1.20  apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD2)
    1.21 @@ -227,21 +227,20 @@
    1.22  
    1.23  text{*Proving that @{term hyprel} is an equivalence relation*}
    1.24  
    1.25 -lemma hyprel_iff: "((X,Y): hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)"
    1.26 +lemma hyprel_iff: "((X,Y) \<in> hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)"
    1.27  by (unfold hyprel_def, fast)
    1.28  
    1.29 -lemma hyprel_refl: "(x,x): hyprel"
    1.30 +lemma hyprel_refl: "(x,x) \<in> hyprel"
    1.31  apply (unfold hyprel_def)
    1.32  apply (auto simp add: FreeUltrafilterNat_Nat_set)
    1.33  done
    1.34  
    1.35 -lemma hyprel_sym [rule_format (no_asm)]: "(x,y): hyprel --> (y,x):hyprel"
    1.36 +lemma hyprel_sym [rule_format (no_asm)]: "(x,y) \<in> hyprel --> (y,x) \<in> hyprel"
    1.37  by (simp add: hyprel_def eq_commute)
    1.38  
    1.39  lemma hyprel_trans: 
    1.40 -      "[|(x,y): hyprel; (y,z):hyprel|] ==> (x,z):hyprel"
    1.41 -apply (unfold hyprel_def, auto, ultra)
    1.42 -done
    1.43 +      "[|(x,y) \<in> hyprel; (y,z) \<in> hyprel|] ==> (x,z) \<in> hyprel"
    1.44 +by (unfold hyprel_def, auto, ultra)
    1.45  
    1.46  lemma equiv_hyprel: "equiv UNIV hyprel"
    1.47  apply (simp add: equiv_def refl_def sym_def trans_def hyprel_refl)
    1.48 @@ -536,7 +535,7 @@
    1.49  
    1.50  subsection{*Trichotomy: the hyperreals are Linearly Ordered*}
    1.51  
    1.52 -lemma lemma_hyprel_0_mem: "\<exists>x. x: hyprel `` {%n. 0}"
    1.53 +lemma lemma_hyprel_0_mem: "\<exists>x. x \<in> hyprel `` {%n. 0}"
    1.54  apply (unfold hyprel_def)
    1.55  apply (rule_tac x = "%n. 0" in exI, safe)
    1.56  apply (auto intro!: FreeUltrafilterNat_Nat_set)
    1.57 @@ -588,64 +587,57 @@
    1.58  lemma hypreal_neq_iff: "((w::hypreal) \<noteq> z) = (w<z | z<w)"
    1.59  by (cut_tac hypreal_linear, blast)
    1.60  
    1.61 -lemma hypreal_linear_less2: "!!(x::hypreal). [| x < y ==> P;  x = y ==> P;  
    1.62 -           y < x ==> P |] ==> P"
    1.63 -apply (cut_tac x = x and y = y in hypreal_linear, auto)
    1.64 -done
    1.65 -
    1.66  
    1.67  subsection{*Properties of The @{text "\<le>"} Relation*}
    1.68  
    1.69  lemma hypreal_le: 
    1.70 -      "(Abs_hypreal(hyprel``{%n. X n}) <=  
    1.71 -            Abs_hypreal(hyprel``{%n. Y n})) =  
    1.72 -       ({n. X n <= Y n} \<in> FreeUltrafilterNat)"
    1.73 -apply (unfold hypreal_le_def real_le_def)
    1.74 -apply (auto simp add: hypreal_less)
    1.75 +      "(Abs_hypreal(hyprel``{%n. X n}) \<le> Abs_hypreal(hyprel``{%n. Y n})) =  
    1.76 +       ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
    1.77 +apply (auto simp add: hypreal_less hypreal_le_def linorder_not_less[symmetric])
    1.78  apply (ultra+)
    1.79  done
    1.80  
    1.81 -lemma hypreal_le_imp_less_or_eq: "!!(x::hypreal). x <= y ==> x < y | x = y"
    1.82 +lemma hypreal_le_imp_less_or_eq: "!!(x::hypreal). x \<le> y ==> x < y | x = y"
    1.83  apply (unfold hypreal_le_def)
    1.84  apply (cut_tac hypreal_linear)
    1.85  apply (fast elim: hypreal_less_irrefl hypreal_less_asym)
    1.86  done
    1.87  
    1.88 -lemma hypreal_less_or_eq_imp_le: "z<w | z=w ==> z <=(w::hypreal)"
    1.89 +lemma hypreal_less_or_eq_imp_le: "z<w | z=w ==> z \<le>(w::hypreal)"
    1.90  apply (unfold hypreal_le_def)
    1.91  apply (cut_tac hypreal_linear)
    1.92  apply (fast elim: hypreal_less_irrefl hypreal_less_asym)
    1.93  done
    1.94  
    1.95 -lemma hypreal_le_eq_less_or_eq: "(x <= (y::hypreal)) = (x < y | x=y)"
    1.96 +lemma hypreal_le_eq_less_or_eq: "(x \<le> (y::hypreal)) = (x < y | x=y)"
    1.97  by (blast intro!: hypreal_less_or_eq_imp_le dest: hypreal_le_imp_less_or_eq) 
    1.98  
    1.99  lemmas hypreal_le_less = hypreal_le_eq_less_or_eq
   1.100  
   1.101 -lemma hypreal_le_refl: "w <= (w::hypreal)"
   1.102 +lemma hypreal_le_refl: "w \<le> (w::hypreal)"
   1.103  by (simp add: hypreal_le_eq_less_or_eq)
   1.104  
   1.105  (* Axiom 'linorder_linear' of class 'linorder': *)
   1.106 -lemma hypreal_le_linear: "(z::hypreal) <= w | w <= z"
   1.107 +lemma hypreal_le_linear: "(z::hypreal) \<le> w | w \<le> z"
   1.108  apply (simp add: hypreal_le_less)
   1.109  apply (cut_tac hypreal_linear, blast)
   1.110  done
   1.111  
   1.112 -lemma hypreal_le_trans: "[| i <= j; j <= k |] ==> i <= (k::hypreal)"
   1.113 +lemma hypreal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypreal)"
   1.114  apply (drule hypreal_le_imp_less_or_eq) 
   1.115  apply (drule hypreal_le_imp_less_or_eq) 
   1.116  apply (rule hypreal_less_or_eq_imp_le) 
   1.117  apply (blast intro: hypreal_less_trans) 
   1.118  done
   1.119  
   1.120 -lemma hypreal_le_anti_sym: "[| z <= w; w <= z |] ==> z = (w::hypreal)"
   1.121 +lemma hypreal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypreal)"
   1.122  apply (drule hypreal_le_imp_less_or_eq) 
   1.123  apply (drule hypreal_le_imp_less_or_eq) 
   1.124  apply (fast elim: hypreal_less_irrefl hypreal_less_asym)
   1.125  done
   1.126  
   1.127  (* Axiom 'order_less_le' of class 'order': *)
   1.128 -lemma hypreal_less_le: "((w::hypreal) < z) = (w <= z & w \<noteq> z)"
   1.129 +lemma hypreal_less_le: "((w::hypreal) < z) = (w \<le> z & w \<noteq> z)"
   1.130  apply (simp add: hypreal_le_def hypreal_neq_iff)
   1.131  apply (blast intro: hypreal_less_asym)
   1.132  done
   1.133 @@ -794,9 +786,8 @@
   1.134  done
   1.135  
   1.136  lemma hypreal_of_real_le_iff [simp]: 
   1.137 -     "(hypreal_of_real z1 <= hypreal_of_real z2) = (z1 <= z2)"
   1.138 -apply (unfold hypreal_le_def real_le_def, auto)
   1.139 -done
   1.140 +     "(hypreal_of_real z1 \<le> hypreal_of_real z2) = (z1 \<le> z2)"
   1.141 +by (force simp add: hypreal_less hypreal_le_def linorder_not_less[symmetric])
   1.142  
   1.143  lemma hypreal_of_real_eq_iff [simp]:
   1.144       "(hypreal_of_real z1 = hypreal_of_real z2) = (z1 = z2)"
   1.145 @@ -952,8 +943,6 @@
   1.146  val hypreal_eq_minus_iff3 = thm "hypreal_eq_minus_iff3";
   1.147  val hypreal_not_eq_minus_iff = thm "hypreal_not_eq_minus_iff";
   1.148  val hypreal_linear = thm "hypreal_linear";
   1.149 -val hypreal_neq_iff = thm "hypreal_neq_iff";
   1.150 -val hypreal_linear_less2 = thm "hypreal_linear_less2";
   1.151  val hypreal_le = thm "hypreal_le";
   1.152  val hypreal_le_imp_less_or_eq = thm "hypreal_le_imp_less_or_eq";
   1.153  val hypreal_le_eq_less_or_eq = thm "hypreal_le_eq_less_or_eq";