src/HOL/ex/Dedekind_Real.thy
 changeset 41541 1fa4725c4656 parent 40822 98a5faa5aec0 child 45694 4a8743618257
```     1.1 --- a/src/HOL/ex/Dedekind_Real.thy	Thu Jan 13 21:50:13 2011 +0100
1.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Thu Jan 13 23:50:16 2011 +0100
1.3 @@ -354,30 +354,29 @@
1.4
1.5  text{*Part 2 of Dedekind sections definition*}
1.6  lemma preal_not_mem_mult_set_Ex:
1.7 -   assumes A: "A \<in> preal"
1.8 -       and B: "B \<in> preal"
1.9 -     shows "\<exists>q. 0 < q & q \<notin> mult_set A B"
1.10 +  assumes A: "A \<in> preal"
1.11 +    and B: "B \<in> preal"
1.12 +  shows "\<exists>q. 0 < q & q \<notin> mult_set A B"
1.13  proof -
1.14 -  from preal_exists_bound [OF A]
1.15 -  obtain x where [simp]: "0 < x" "x \<notin> A" by blast
1.16 -  from preal_exists_bound [OF B]
1.17 -  obtain y where [simp]: "0 < y" "y \<notin> B" by blast
1.18 +  from preal_exists_bound [OF A] obtain x where 1 [simp]: "0 < x" "x \<notin> A" by blast
1.19 +  from preal_exists_bound [OF B] obtain y where 2 [simp]: "0 < y" "y \<notin> B" by blast
1.20    show ?thesis
1.21    proof (intro exI conjI)
1.22      show "0 < x*y" by (simp add: mult_pos_pos)
1.23      show "x * y \<notin> mult_set A B"
1.24      proof -
1.25 -      { fix u::rat and v::rat
1.26 -              assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
1.27 -              moreover
1.28 -              with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
1.29 -              moreover
1.30 -              with prems have "0\<le>v"
1.31 -                by (blast intro: preal_imp_pos [OF B]  order_less_imp_le prems)
1.32 -              moreover
1.33 -        from calculation
1.34 -              have "u*v < x*y" by (blast intro: mult_strict_mono prems)
1.35 -              ultimately have False by force }
1.36 +      {
1.37 +        fix u::rat and v::rat
1.38 +        assume u: "u \<in> A" and v: "v \<in> B" and xy: "x*y = u*v"
1.39 +        moreover from A B 1 2 u v have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
1.40 +        moreover
1.41 +        from A B 1 2 u v have "0\<le>v"
1.42 +          by (blast intro: preal_imp_pos [OF B] order_less_imp_le)
1.43 +        moreover
1.44 +        from A B 1 `u < x` `v < y` `0 \<le> v`
1.45 +        have "u*v < x*y" by (blast intro: mult_strict_mono)
1.46 +        ultimately have False by force
1.47 +      }
1.48        thus ?thesis by (auto simp add: mult_set_def)
1.49      qed
1.50    qed
1.51 @@ -473,7 +472,7 @@
1.52        fix x::rat and u::rat and v::rat
1.53        assume upos: "0<u" and "u<1" and v: "v \<in> A"
1.54        have vpos: "0<v" by (rule preal_imp_pos [OF A v])
1.55 -      hence "u*v < 1*v" by (simp only: mult_strict_right_mono prems)
1.56 +      hence "u*v < 1*v" by (simp only: mult_strict_right_mono upos `u < 1` v)
1.57        thus "u * v \<in> A"
1.58          by (force intro: preal_downwards_closed [OF A v] mult_pos_pos
1.59            upos vpos)
1.60 @@ -673,18 +672,19 @@
1.61  proof (cases z rule: int_cases)
1.62    case (nonneg n)
1.63    show ?thesis
1.64 -  proof (simp add: prems, induct n)
1.65 +  proof (simp add: nonneg, induct n)
1.66      case 0
1.67 -      from preal_nonempty [OF A]
1.68 -      show ?case  by force
1.69 +    from preal_nonempty [OF A]
1.70 +    show ?case  by force
1.71 +  next
1.72      case (Suc k)
1.73 -      from this obtain b where "b \<in> A" "b + of_nat k * u \<in> A" ..
1.74 -      hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems)
1.75 -      thus ?case by (force simp add: algebra_simps prems)
1.76 +    then obtain b where b: "b \<in> A" "b + of_nat k * u \<in> A" ..
1.77 +    hence "b + of_int (int k)*u + u \<in> A" by (simp add: assms)
1.78 +    thus ?case by (force simp add: algebra_simps b)
1.79    qed
1.80  next
1.81    case (neg n)
1.82 -  with prems show ?thesis by simp
1.83 +  with assms show ?thesis by simp
1.84  qed
1.85
1.86  lemma Gleason9_34_contra:
1.87 @@ -987,10 +987,9 @@
1.88  proof -
1.89    have "0<a" by (rule preal_imp_pos [OF Rep_preal a])
1.90    moreover
1.91 -  have "a < c" using prems
1.92 -    by (blast intro: not_in_Rep_preal_ub )
1.93 -  ultimately show ?thesis using prems
1.94 -    by (simp add: preal_downwards_closed [OF Rep_preal cb])
1.95 +  have "a < c" using assms by (blast intro: not_in_Rep_preal_ub )
1.96 +  ultimately show ?thesis
1.97 +    using assms by (simp add: preal_downwards_closed [OF Rep_preal cb])
1.98  qed
1.99
1.101 @@ -1225,13 +1224,13 @@
1.102
1.103  lemma preal_trans_lemma:
1.104    assumes "x + y1 = x1 + y"
1.105 -      and "x + y2 = x2 + y"
1.106 +    and "x + y2 = x2 + y"
1.107    shows "x1 + y2 = x2 + (y1::preal)"
1.108  proof -
1.109    have "(x1 + y2) + x = (x + y2) + x1" by (simp add: add_ac)
1.110 -  also have "... = (x2 + y) + x1"  by (simp add: prems)
1.111 +  also have "... = (x2 + y) + x1"  by (simp add: assms)
1.112    also have "... = x2 + (x1 + y)"  by (simp add: add_ac)
1.113 -  also have "... = x2 + (x + y1)"  by (simp add: prems)
1.114 +  also have "... = x2 + (x + y1)"  by (simp add: assms)
1.115    also have "... = (x2 + y1) + x"  by (simp add: add_ac)
1.116    finally have "(x1 + y2) + x = (x2 + y1) + x" .
1.117    thus ?thesis by (rule add_right_imp_eq)
1.118 @@ -1436,20 +1435,20 @@
1.119    assumes eq: "a+b = c+d" and le: "c \<le> a"
1.120    shows "b \<le> (d::preal)"
1.121  proof -
1.122 -  have "c+d \<le> a+d" by (simp add: prems)
1.123 -  hence "a+b \<le> a+d" by (simp add: prems)
1.124 +  have "c+d \<le> a+d" by (simp add: le)
1.125 +  hence "a+b \<le> a+d" by (simp add: eq)
1.126    thus "b \<le> d" by simp
1.127  qed
1.128
1.129  lemma real_le_lemma:
1.130    assumes l: "u1 + v2 \<le> u2 + v1"
1.131 -      and "x1 + v1 = u1 + y1"
1.132 -      and "x2 + v2 = u2 + y2"
1.133 +    and "x1 + v1 = u1 + y1"
1.134 +    and "x2 + v2 = u2 + y2"
1.135    shows "x1 + y2 \<le> x2 + (y1::preal)"
1.136  proof -
1.137 -  have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: prems)
1.138 +  have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: assms)
1.139    hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: add_ac)
1.140 -  also have "... \<le> (x2+y1) + (u2+v1)" by (simp add: prems)
1.141 +  also have "... \<le> (x2+y1) + (u2+v1)" by (simp add: assms)
1.142    finally show ?thesis by simp
1.143  qed
1.144
1.145 @@ -1465,13 +1464,13 @@
1.146
1.147  lemma real_trans_lemma:
1.148    assumes "x + v \<le> u + y"
1.149 -      and "u + v' \<le> u' + v"
1.150 -      and "x2 + v2 = u2 + y2"
1.151 +    and "u + v' \<le> u' + v"
1.152 +    and "x2 + v2 = u2 + y2"
1.153    shows "x + v' \<le> u' + (y::preal)"
1.154  proof -
1.155    have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: add_ac)
1.156 -  also have "... \<le> (u+y) + (u+v')" by (simp add: prems)
1.157 -  also have "... \<le> (u+y) + (u'+v)" by (simp add: prems)
1.158 +  also have "... \<le> (u+y) + (u+v')" by (simp add: assms)
1.159 +  also have "... \<le> (u+y) + (u'+v)" by (simp add: assms)
1.160    also have "... = (u'+y) + (u+v)"  by (simp add: add_ac)
1.161    finally show ?thesis by simp
1.162  qed
1.163 @@ -1947,7 +1946,7 @@
1.164  proof -
1.165    have "\<exists>x. isLub UNIV S x"
1.166      by (rule reals_complete)
1.167 -       (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def prems)
1.168 +       (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def assms)
1.169    thus ?thesis
1.170      by (metis UNIV_I isLub_isUb isLub_le_isUb isUbD isUb_def setleI)
1.171  qed
```