src/HOL/Real/PReal.thy
changeset 14378 69c4d5997669
parent 14377 f454b3004f8f
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Real/PReal.thy	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Real/PReal.thy	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -700,7 +700,7 @@
     1.4    assumes A: "A \<in> preal"
     1.5        and "\<forall>x\<in>A. x + u \<in> A"
     1.6        and "0 \<le> z"
     1.7 -     shows "\<exists>b\<in>A. b + (rat z) * u \<in> A"
     1.8 +     shows "\<exists>b\<in>A. b + (of_int z) * u \<in> A"
     1.9  proof (cases z rule: int_cases)
    1.10    case (nonneg n)
    1.11    show ?thesis
    1.12 @@ -709,8 +709,8 @@
    1.13        from preal_nonempty [OF A]
    1.14        show ?case  by force 
    1.15      case (Suc k)
    1.16 -      from this obtain b where "b \<in> A" "b + rat (int k) * u \<in> A" ..
    1.17 -      hence "b + rat (int k)*u + u \<in> A" by (simp add: prems)
    1.18 +      from this obtain b where "b \<in> A" "b + of_int (int k) * u \<in> A" ..
    1.19 +      hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems)
    1.20        thus ?case by (force simp add: left_distrib add_ac prems) 
    1.21    qed
    1.22  next
    1.23 @@ -718,7 +718,6 @@
    1.24    with prems show ?thesis by simp
    1.25  qed
    1.26  
    1.27 -
    1.28  lemma Gleason9_34_contra:
    1.29    assumes A: "A \<in> preal"
    1.30      shows "[|\<forall>x\<in>A. x + u \<in> A; 0 < u; 0 < y; y \<notin> A|] ==> False"
    1.31 @@ -736,10 +735,10 @@
    1.32    have apos [simp]: "0 < a" 
    1.33      by (simp add: zero_less_Fract_iff [OF bpos, symmetric] ypos) 
    1.34    let ?k = "a*d"
    1.35 -  have frle: "Fract a b \<le> rat ?k * (Fract c d)" 
    1.36 +  have frle: "Fract a b \<le> Fract ?k 1 * (Fract c d)" 
    1.37    proof -
    1.38      have "?thesis = ((a * d * b * d) \<le> c * b * (a * d * b * d))"
    1.39 -      by (simp add: rat_def mult_rat le_rat order_less_imp_not_eq2 mult_ac) 
    1.40 +      by (simp add: mult_rat le_rat order_less_imp_not_eq2 mult_ac) 
    1.41      moreover
    1.42      have "(1 * (a * d * b * d)) \<le> c * b * (a * d * b * d)"
    1.43        by (rule mult_mono, 
    1.44 @@ -751,11 +750,11 @@
    1.45    have k: "0 \<le> ?k" by (simp add: order_less_imp_le zero_less_mult_iff)  
    1.46    from Gleason9_34_exists [OF A closed k]
    1.47    obtain z where z: "z \<in> A" 
    1.48 -             and mem: "z + rat ?k * Fract c d \<in> A" ..
    1.49 -  have less: "z + rat ?k * Fract c d < Fract a b"
    1.50 +             and mem: "z + of_int ?k * Fract c d \<in> A" ..
    1.51 +  have less: "z + of_int ?k * Fract c d < Fract a b"
    1.52      by (rule not_in_preal_ub [OF A notin mem ypos])
    1.53    have "0<z" by (rule preal_imp_pos [OF A z])
    1.54 -  with frle and less show False by arith 
    1.55 +  with frle and less show False by (simp add: Fract_of_int_eq) 
    1.56  qed
    1.57  
    1.58