src/HOL/Hyperreal/HyperDef.thy
changeset 14387 e96d5c42c4b0
parent 14378 69c4d5997669
child 14421 ee97b6463cb4
     1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Sat Feb 14 02:06:12 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Sun Feb 15 10:46:37 2004 +0100
     1.3 @@ -504,8 +504,7 @@
     1.4        "(Abs_hypreal(hyprel``{%n. X n}) \<le> Abs_hypreal(hyprel``{%n. Y n})) =  
     1.5         ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
     1.6  apply (unfold hypreal_le_def)
     1.7 -apply (auto intro!: lemma_hyprel_refl)
     1.8 -apply (ultra)
     1.9 +apply (auto intro!: lemma_hyprel_refl, ultra)
    1.10  done
    1.11  
    1.12  lemma hypreal_le_refl: "w \<le> (w::hypreal)"
    1.13 @@ -517,21 +516,18 @@
    1.14  apply (rule eq_Abs_hypreal [of i])
    1.15  apply (rule eq_Abs_hypreal [of j])
    1.16  apply (rule eq_Abs_hypreal [of k])
    1.17 -apply (simp add: hypreal_le) 
    1.18 -apply ultra
    1.19 +apply (simp add: hypreal_le, ultra)
    1.20  done
    1.21  
    1.22  lemma hypreal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypreal)"
    1.23  apply (rule eq_Abs_hypreal [of z])
    1.24  apply (rule eq_Abs_hypreal [of w])
    1.25 -apply (simp add: hypreal_le) 
    1.26 -apply ultra
    1.27 +apply (simp add: hypreal_le, ultra)
    1.28  done
    1.29  
    1.30  (* Axiom 'order_less_le' of class 'order': *)
    1.31  lemma hypreal_less_le: "((w::hypreal) < z) = (w \<le> z & w \<noteq> z)"
    1.32 -apply (simp add: hypreal_less_def)
    1.33 -done
    1.34 +by (simp add: hypreal_less_def)
    1.35  
    1.36  instance hypreal :: order
    1.37  proof qed
    1.38 @@ -543,8 +539,7 @@
    1.39  lemma hypreal_le_linear: "(z::hypreal) \<le> w | w \<le> z"
    1.40  apply (rule eq_Abs_hypreal [of z])
    1.41  apply (rule eq_Abs_hypreal [of w])
    1.42 -apply (auto simp add: hypreal_le) 
    1.43 -apply ultra
    1.44 +apply (auto simp add: hypreal_le, ultra)
    1.45  done
    1.46  
    1.47  instance hypreal :: linorder 
    1.48 @@ -565,8 +560,7 @@
    1.49  apply (rule eq_Abs_hypreal [of y])
    1.50  apply (rule eq_Abs_hypreal [of z])
    1.51  apply (auto simp add: hypreal_zero_def hypreal_le hypreal_mult 
    1.52 -                      linorder_not_le [symmetric])
    1.53 -apply ultra 
    1.54 +                      linorder_not_le [symmetric], ultra) 
    1.55  done
    1.56  
    1.57  
    1.58 @@ -590,7 +584,7 @@
    1.59    by (rule Ring_and_Field.mult_1_right)
    1.60  
    1.61  lemma hypreal_mult_minus_1 [simp]: "(- (1::hypreal)) * z = -z"
    1.62 -by (simp)
    1.63 +by simp
    1.64  
    1.65  lemma hypreal_mult_minus_1_right [simp]: "z * (- (1::hypreal)) = -z"
    1.66  by (subst hypreal_mult_commute, simp)
    1.67 @@ -613,12 +607,10 @@
    1.68  by (auto dest: hypreal_eq_minus_iff [THEN iffD2])
    1.69  
    1.70  lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
    1.71 -apply auto
    1.72 -done
    1.73 +by auto
    1.74      
    1.75  lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
    1.76 -apply auto
    1.77 -done
    1.78 +by auto
    1.79  
    1.80  lemma hypreal_mult_not_0: "[| x \<noteq> 0; y \<noteq> 0 |] ==> x * y \<noteq> (0::hypreal)"
    1.81  by simp
    1.82 @@ -725,8 +717,7 @@
    1.83  lemma hypreal_less: 
    1.84        "(Abs_hypreal(hyprel``{%n. X n}) < Abs_hypreal(hyprel``{%n. Y n})) =  
    1.85         ({n. X n < Y n} \<in> FreeUltrafilterNat)"
    1.86 -apply (auto simp add: hypreal_le linorder_not_le [symmetric]) 
    1.87 -apply ultra+
    1.88 +apply (auto simp add: hypreal_le linorder_not_le [symmetric], ultra+)
    1.89  done
    1.90  
    1.91  lemma hypreal_zero_num: "0 = Abs_hypreal (hyprel `` {%n. 0})"
    1.92 @@ -773,7 +764,7 @@
    1.93  
    1.94  lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} |  
    1.95        (\<exists>y. {n::nat. x = real n} = {y})"
    1.96 -by (force)
    1.97 +by force
    1.98  
    1.99  lemma lemma_finite_omega_set: "finite {n::nat. x = real n}"
   1.100  by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto)
   1.101 @@ -794,7 +785,7 @@
   1.102  lemma lemma_epsilon_empty_singleton_disj:
   1.103       "{n::nat. x = inverse(real(Suc n))} = {} |  
   1.104        (\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})"
   1.105 -by (auto)
   1.106 +by auto
   1.107  
   1.108  lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}"
   1.109  by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto)