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