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.100  lemma less_add_left_le1:
   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