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.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
```