src/HOL/Real/PReal.thy
changeset 14377 f454b3004f8f
parent 14369 c50188fe6366
child 14378 69c4d5997669
     1.1 --- a/src/HOL/Real/PReal.thy	Thu Feb 05 04:30:38 2004 +0100
     1.2 +++ b/src/HOL/Real/PReal.thy	Thu Feb 05 10:45:28 2004 +0100
     1.3 @@ -386,17 +386,18 @@
     1.4    proof (intro exI conjI)
     1.5      show "0 < x*y" by (simp add: mult_pos)
     1.6      show "x * y \<notin> mult_set A B"
     1.7 -    proof (auto simp add: mult_set_def)
     1.8 -      fix u::rat and v::rat
     1.9 -      assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
    1.10 -      moreover
    1.11 -      with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
    1.12 -      moreover
    1.13 -      with prems have "0\<le>v"
    1.14 -        by (blast intro: preal_imp_pos [OF B]  order_less_imp_le prems)
    1.15 -      moreover
    1.16 -      hence "u*v < x*y" by (blast intro: mult_strict_mono prems)
    1.17 -      ultimately show False by force
    1.18 +    proof -
    1.19 +      { fix u::rat and v::rat
    1.20 +	assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
    1.21 +	moreover
    1.22 +	with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
    1.23 +	moreover
    1.24 +	with prems have "0\<le>v"
    1.25 +	  by (blast intro: preal_imp_pos [OF B]  order_less_imp_le prems)
    1.26 +	moreover
    1.27 +	hence "u*v < x*y" by (blast intro: mult_strict_mono prems)
    1.28 +	ultimately have False by force}
    1.29 +      thus ?thesis by (auto simp add: mult_set_def)
    1.30      qed
    1.31    qed
    1.32  qed
    1.33 @@ -646,14 +647,15 @@
    1.34    proof (intro exI conjI)
    1.35      show "0 < inverse x" by simp
    1.36      show "inverse x \<notin> inverse_set A"
    1.37 -    proof (auto simp add: inverse_set_def)
    1.38 -      fix y::rat 
    1.39 -      assume ygt: "inverse x < y"
    1.40 -      have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt])
    1.41 -      have iyless: "inverse y < x" 
    1.42 -        by (simp add: inverse_less_imp_less [of x] ygt)
    1.43 -      show "inverse y \<in> A"
    1.44 -        by (simp add: preal_downwards_closed [OF A x] iyless) 
    1.45 +    proof -
    1.46 +      { fix y::rat 
    1.47 +	assume ygt: "inverse x < y"
    1.48 +	have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt])
    1.49 +	have iyless: "inverse y < x" 
    1.50 +	  by (simp add: inverse_less_imp_less [of x] ygt)
    1.51 +	have "inverse y \<in> A"
    1.52 +	  by (simp add: preal_downwards_closed [OF A x] iyless)}
    1.53 +     thus ?thesis by (auto simp add: inverse_set_def)
    1.54      qed
    1.55    qed
    1.56  qed