src/HOL/PReal.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 35050 9f841f20dca6
child 35216 7641e8d831d2
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     1 (*  Title:      HOL/PReal.thy
     2     Author:     Jacques D. Fleuriot, University of Cambridge
     3 
     4 The positive reals as Dedekind sections of positive
     5 rationals. Fundamentals of Abstract Analysis [Gleason- p. 121]
     6 provides some of the definitions.
     7 *)
     8 
     9 header {* Positive real numbers *}
    10 
    11 theory PReal
    12 imports Rational 
    13 begin
    14 
    15 text{*Could be generalized and moved to @{text Groups}*}
    16 lemma add_eq_exists: "\<exists>x. a+x = (b::rat)"
    17 by (rule_tac x="b-a" in exI, simp)
    18 
    19 definition
    20   cut :: "rat set => bool" where
    21   [code del]: "cut A = ({} \<subset> A &
    22             A < {r. 0 < r} &
    23             (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
    24 
    25 lemma interval_empty_iff:
    26   "{y. (x::'a::dense_linorder) < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
    27   by (auto dest: dense)
    28 
    29 
    30 lemma cut_of_rat: 
    31   assumes q: "0 < q" shows "cut {r::rat. 0 < r & r < q}" (is "cut ?A")
    32 proof -
    33   from q have pos: "?A < {r. 0 < r}" by force
    34   have nonempty: "{} \<subset> ?A"
    35   proof
    36     show "{} \<subseteq> ?A" by simp
    37     show "{} \<noteq> ?A"
    38       by (force simp only: q eq_commute [of "{}"] interval_empty_iff)
    39   qed
    40   show ?thesis
    41     by (simp add: cut_def pos nonempty,
    42         blast dest: dense intro: order_less_trans)
    43 qed
    44 
    45 
    46 typedef preal = "{A. cut A}"
    47   by (blast intro: cut_of_rat [OF zero_less_one])
    48 
    49 definition
    50   preal_of_rat :: "rat => preal" where
    51   "preal_of_rat q = Abs_preal {x::rat. 0 < x & x < q}"
    52 
    53 definition
    54   psup :: "preal set => preal" where
    55   [code del]: "psup P = Abs_preal (\<Union>X \<in> P. Rep_preal X)"
    56 
    57 definition
    58   add_set :: "[rat set,rat set] => rat set" where
    59   "add_set A B = {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x + y}"
    60 
    61 definition
    62   diff_set :: "[rat set,rat set] => rat set" where
    63   [code del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
    64 
    65 definition
    66   mult_set :: "[rat set,rat set] => rat set" where
    67   "mult_set A B = {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x * y}"
    68 
    69 definition
    70   inverse_set :: "rat set => rat set" where
    71   [code del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
    72 
    73 instantiation preal :: "{ord, plus, minus, times, inverse, one}"
    74 begin
    75 
    76 definition
    77   preal_less_def [code del]:
    78     "R < S == Rep_preal R < Rep_preal S"
    79 
    80 definition
    81   preal_le_def [code del]:
    82     "R \<le> S == Rep_preal R \<subseteq> Rep_preal S"
    83 
    84 definition
    85   preal_add_def:
    86     "R + S == Abs_preal (add_set (Rep_preal R) (Rep_preal S))"
    87 
    88 definition
    89   preal_diff_def:
    90     "R - S == Abs_preal (diff_set (Rep_preal R) (Rep_preal S))"
    91 
    92 definition
    93   preal_mult_def:
    94     "R * S == Abs_preal (mult_set (Rep_preal R) (Rep_preal S))"
    95 
    96 definition
    97   preal_inverse_def:
    98     "inverse R == Abs_preal (inverse_set (Rep_preal R))"
    99 
   100 definition "R / S = R * inverse (S\<Colon>preal)"
   101 
   102 definition
   103   preal_one_def:
   104     "1 == preal_of_rat 1"
   105 
   106 instance ..
   107 
   108 end
   109 
   110 
   111 text{*Reduces equality on abstractions to equality on representatives*}
   112 declare Abs_preal_inject [simp]
   113 declare Abs_preal_inverse [simp]
   114 
   115 lemma rat_mem_preal: "0 < q ==> {r::rat. 0 < r & r < q} \<in> preal"
   116 by (simp add: preal_def cut_of_rat)
   117 
   118 lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
   119 by (unfold preal_def cut_def, blast)
   120 
   121 lemma preal_Ex_mem: "A \<in> preal \<Longrightarrow> \<exists>x. x \<in> A"
   122 by (drule preal_nonempty, fast)
   123 
   124 lemma preal_imp_psubset_positives: "A \<in> preal ==> A < {r. 0 < r}"
   125 by (force simp add: preal_def cut_def)
   126 
   127 lemma preal_exists_bound: "A \<in> preal ==> \<exists>x. 0 < x & x \<notin> A"
   128 by (drule preal_imp_psubset_positives, auto)
   129 
   130 lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
   131 by (unfold preal_def cut_def, blast)
   132 
   133 lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
   134 by (unfold preal_def cut_def, blast)
   135 
   136 text{*Relaxing the final premise*}
   137 lemma preal_downwards_closed':
   138      "[| A \<in> preal; y \<in> A; 0 < z; z \<le> y |] ==> z \<in> A"
   139 apply (simp add: order_le_less)
   140 apply (blast intro: preal_downwards_closed)
   141 done
   142 
   143 text{*A positive fraction not in a positive real is an upper bound.
   144  Gleason p. 122 - Remark (1)*}
   145 
   146 lemma not_in_preal_ub:
   147   assumes A: "A \<in> preal"
   148     and notx: "x \<notin> A"
   149     and y: "y \<in> A"
   150     and pos: "0 < x"
   151   shows "y < x"
   152 proof (cases rule: linorder_cases)
   153   assume "x<y"
   154   with notx show ?thesis
   155     by (simp add:  preal_downwards_closed [OF A y] pos)
   156 next
   157   assume "x=y"
   158   with notx and y show ?thesis by simp
   159 next
   160   assume "y<x"
   161   thus ?thesis .
   162 qed
   163 
   164 text {* preal lemmas instantiated to @{term "Rep_preal X"} *}
   165 
   166 lemma mem_Rep_preal_Ex: "\<exists>x. x \<in> Rep_preal X"
   167 by (rule preal_Ex_mem [OF Rep_preal])
   168 
   169 lemma Rep_preal_exists_bound: "\<exists>x>0. x \<notin> Rep_preal X"
   170 by (rule preal_exists_bound [OF Rep_preal])
   171 
   172 lemmas not_in_Rep_preal_ub = not_in_preal_ub [OF Rep_preal]
   173 
   174 
   175 
   176 subsection{*@{term preal_of_prat}: the Injection from prat to preal*}
   177 
   178 lemma rat_less_set_mem_preal: "0 < y ==> {u::rat. 0 < u & u < y} \<in> preal"
   179 by (simp add: preal_def cut_of_rat)
   180 
   181 lemma rat_subset_imp_le:
   182      "[|{u::rat. 0 < u & u < x} \<subseteq> {u. 0 < u & u < y}; 0<x|] ==> x \<le> y"
   183 apply (simp add: linorder_not_less [symmetric])
   184 apply (blast dest: dense intro: order_less_trans)
   185 done
   186 
   187 lemma rat_set_eq_imp_eq:
   188      "[|{u::rat. 0 < u & u < x} = {u. 0 < u & u < y};
   189         0 < x; 0 < y|] ==> x = y"
   190 by (blast intro: rat_subset_imp_le order_antisym)
   191 
   192 
   193 
   194 subsection{*Properties of Ordering*}
   195 
   196 instance preal :: order
   197 proof
   198   fix w :: preal
   199   show "w \<le> w" by (simp add: preal_le_def)
   200 next
   201   fix i j k :: preal
   202   assume "i \<le> j" and "j \<le> k"
   203   then show "i \<le> k" by (simp add: preal_le_def)
   204 next
   205   fix z w :: preal
   206   assume "z \<le> w" and "w \<le> z"
   207   then show "z = w" by (simp add: preal_le_def Rep_preal_inject)
   208 next
   209   fix z w :: preal
   210   show "z < w \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
   211   by (auto simp add: preal_le_def preal_less_def Rep_preal_inject)
   212 qed  
   213 
   214 lemma preal_imp_pos: "[|A \<in> preal; r \<in> A|] ==> 0 < r"
   215 by (insert preal_imp_psubset_positives, blast)
   216 
   217 instance preal :: linorder
   218 proof
   219   fix x y :: preal
   220   show "x <= y | y <= x"
   221     apply (auto simp add: preal_le_def)
   222     apply (rule ccontr)
   223     apply (blast dest: not_in_Rep_preal_ub intro: preal_imp_pos [OF Rep_preal]
   224              elim: order_less_asym)
   225     done
   226 qed
   227 
   228 instantiation preal :: distrib_lattice
   229 begin
   230 
   231 definition
   232   "(inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = min"
   233 
   234 definition
   235   "(sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = max"
   236 
   237 instance
   238   by intro_classes
   239     (auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
   240 
   241 end
   242 
   243 subsection{*Properties of Addition*}
   244 
   245 lemma preal_add_commute: "(x::preal) + y = y + x"
   246 apply (unfold preal_add_def add_set_def)
   247 apply (rule_tac f = Abs_preal in arg_cong)
   248 apply (force simp add: add_commute)
   249 done
   250 
   251 text{*Lemmas for proving that addition of two positive reals gives
   252  a positive real*}
   253 
   254 lemma empty_psubset_nonempty: "a \<in> A ==> {} \<subset> A"
   255 by blast
   256 
   257 text{*Part 1 of Dedekind sections definition*}
   258 lemma add_set_not_empty:
   259      "[|A \<in> preal; B \<in> preal|] ==> {} \<subset> add_set A B"
   260 apply (drule preal_nonempty)+
   261 apply (auto simp add: add_set_def)
   262 done
   263 
   264 text{*Part 2 of Dedekind sections definition.  A structured version of
   265 this proof is @{text preal_not_mem_mult_set_Ex} below.*}
   266 lemma preal_not_mem_add_set_Ex:
   267      "[|A \<in> preal; B \<in> preal|] ==> \<exists>q>0. q \<notin> add_set A B"
   268 apply (insert preal_exists_bound [of A] preal_exists_bound [of B], auto) 
   269 apply (rule_tac x = "x+xa" in exI)
   270 apply (simp add: add_set_def, clarify)
   271 apply (drule (3) not_in_preal_ub)+
   272 apply (force dest: add_strict_mono)
   273 done
   274 
   275 lemma add_set_not_rat_set:
   276    assumes A: "A \<in> preal" 
   277        and B: "B \<in> preal"
   278      shows "add_set A B < {r. 0 < r}"
   279 proof
   280   from preal_imp_pos [OF A] preal_imp_pos [OF B]
   281   show "add_set A B \<subseteq> {r. 0 < r}" by (force simp add: add_set_def) 
   282 next
   283   show "add_set A B \<noteq> {r. 0 < r}"
   284     by (insert preal_not_mem_add_set_Ex [OF A B], blast) 
   285 qed
   286 
   287 text{*Part 3 of Dedekind sections definition*}
   288 lemma add_set_lemma3:
   289      "[|A \<in> preal; B \<in> preal; u \<in> add_set A B; 0 < z; z < u|] 
   290       ==> z \<in> add_set A B"
   291 proof (unfold add_set_def, clarify)
   292   fix x::rat and y::rat
   293   assume A: "A \<in> preal" 
   294     and B: "B \<in> preal"
   295     and [simp]: "0 < z"
   296     and zless: "z < x + y"
   297     and x:  "x \<in> A"
   298     and y:  "y \<in> B"
   299   have xpos [simp]: "0<x" by (rule preal_imp_pos [OF A x])
   300   have ypos [simp]: "0<y" by (rule preal_imp_pos [OF B y])
   301   have xypos [simp]: "0 < x+y" by (simp add: pos_add_strict)
   302   let ?f = "z/(x+y)"
   303   have fless: "?f < 1" by (simp add: zless pos_divide_less_eq)
   304   show "\<exists>x' \<in> A. \<exists>y'\<in>B. z = x' + y'"
   305   proof (intro bexI)
   306     show "z = x*?f + y*?f"
   307       by (simp add: left_distrib [symmetric] divide_inverse mult_ac
   308           order_less_imp_not_eq2)
   309   next
   310     show "y * ?f \<in> B"
   311     proof (rule preal_downwards_closed [OF B y])
   312       show "0 < y * ?f"
   313         by (simp add: divide_inverse zero_less_mult_iff)
   314     next
   315       show "y * ?f < y"
   316         by (insert mult_strict_left_mono [OF fless ypos], simp)
   317     qed
   318   next
   319     show "x * ?f \<in> A"
   320     proof (rule preal_downwards_closed [OF A x])
   321       show "0 < x * ?f"
   322         by (simp add: divide_inverse zero_less_mult_iff)
   323     next
   324       show "x * ?f < x"
   325         by (insert mult_strict_left_mono [OF fless xpos], simp)
   326     qed
   327   qed
   328 qed
   329 
   330 text{*Part 4 of Dedekind sections definition*}
   331 lemma add_set_lemma4:
   332      "[|A \<in> preal; B \<in> preal; y \<in> add_set A B|] ==> \<exists>u \<in> add_set A B. y < u"
   333 apply (auto simp add: add_set_def)
   334 apply (frule preal_exists_greater [of A], auto) 
   335 apply (rule_tac x="u + y" in exI)
   336 apply (auto intro: add_strict_left_mono)
   337 done
   338 
   339 lemma mem_add_set:
   340      "[|A \<in> preal; B \<in> preal|] ==> add_set A B \<in> preal"
   341 apply (simp (no_asm_simp) add: preal_def cut_def)
   342 apply (blast intro!: add_set_not_empty add_set_not_rat_set
   343                      add_set_lemma3 add_set_lemma4)
   344 done
   345 
   346 lemma preal_add_assoc: "((x::preal) + y) + z = x + (y + z)"
   347 apply (simp add: preal_add_def mem_add_set Rep_preal)
   348 apply (force simp add: add_set_def add_ac)
   349 done
   350 
   351 instance preal :: ab_semigroup_add
   352 proof
   353   fix a b c :: preal
   354   show "(a + b) + c = a + (b + c)" by (rule preal_add_assoc)
   355   show "a + b = b + a" by (rule preal_add_commute)
   356 qed
   357 
   358 lemma preal_add_left_commute: "x + (y + z) = y + ((x + z)::preal)"
   359 by (rule add_left_commute)
   360 
   361 text{* Positive Real addition is an AC operator *}
   362 lemmas preal_add_ac = preal_add_assoc preal_add_commute preal_add_left_commute
   363 
   364 
   365 subsection{*Properties of Multiplication*}
   366 
   367 text{*Proofs essentially same as for addition*}
   368 
   369 lemma preal_mult_commute: "(x::preal) * y = y * x"
   370 apply (unfold preal_mult_def mult_set_def)
   371 apply (rule_tac f = Abs_preal in arg_cong)
   372 apply (force simp add: mult_commute)
   373 done
   374 
   375 text{*Multiplication of two positive reals gives a positive real.*}
   376 
   377 text{*Lemmas for proving positive reals multiplication set in @{typ preal}*}
   378 
   379 text{*Part 1 of Dedekind sections definition*}
   380 lemma mult_set_not_empty:
   381      "[|A \<in> preal; B \<in> preal|] ==> {} \<subset> mult_set A B"
   382 apply (insert preal_nonempty [of A] preal_nonempty [of B]) 
   383 apply (auto simp add: mult_set_def)
   384 done
   385 
   386 text{*Part 2 of Dedekind sections definition*}
   387 lemma preal_not_mem_mult_set_Ex:
   388    assumes A: "A \<in> preal" 
   389        and B: "B \<in> preal"
   390      shows "\<exists>q. 0 < q & q \<notin> mult_set A B"
   391 proof -
   392   from preal_exists_bound [OF A]
   393   obtain x where [simp]: "0 < x" "x \<notin> A" by blast
   394   from preal_exists_bound [OF B]
   395   obtain y where [simp]: "0 < y" "y \<notin> B" by blast
   396   show ?thesis
   397   proof (intro exI conjI)
   398     show "0 < x*y" by (simp add: mult_pos_pos)
   399     show "x * y \<notin> mult_set A B"
   400     proof -
   401       { fix u::rat and v::rat
   402               assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
   403               moreover
   404               with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
   405               moreover
   406               with prems have "0\<le>v"
   407                 by (blast intro: preal_imp_pos [OF B]  order_less_imp_le prems)
   408               moreover
   409         from calculation
   410               have "u*v < x*y" by (blast intro: mult_strict_mono prems)
   411               ultimately have False by force }
   412       thus ?thesis by (auto simp add: mult_set_def)
   413     qed
   414   qed
   415 qed
   416 
   417 lemma mult_set_not_rat_set:
   418   assumes A: "A \<in> preal" 
   419     and B: "B \<in> preal"
   420   shows "mult_set A B < {r. 0 < r}"
   421 proof
   422   show "mult_set A B \<subseteq> {r. 0 < r}"
   423     by (force simp add: mult_set_def
   424       intro: preal_imp_pos [OF A] preal_imp_pos [OF B] mult_pos_pos)
   425   show "mult_set A B \<noteq> {r. 0 < r}"
   426     using preal_not_mem_mult_set_Ex [OF A B] by blast
   427 qed
   428 
   429 
   430 
   431 text{*Part 3 of Dedekind sections definition*}
   432 lemma mult_set_lemma3:
   433      "[|A \<in> preal; B \<in> preal; u \<in> mult_set A B; 0 < z; z < u|] 
   434       ==> z \<in> mult_set A B"
   435 proof (unfold mult_set_def, clarify)
   436   fix x::rat and y::rat
   437   assume A: "A \<in> preal" 
   438     and B: "B \<in> preal"
   439     and [simp]: "0 < z"
   440     and zless: "z < x * y"
   441     and x:  "x \<in> A"
   442     and y:  "y \<in> B"
   443   have [simp]: "0<y" by (rule preal_imp_pos [OF B y])
   444   show "\<exists>x' \<in> A. \<exists>y' \<in> B. z = x' * y'"
   445   proof
   446     show "\<exists>y'\<in>B. z = (z/y) * y'"
   447     proof
   448       show "z = (z/y)*y"
   449         by (simp add: divide_inverse mult_commute [of y] mult_assoc
   450                       order_less_imp_not_eq2)
   451       show "y \<in> B" by fact
   452     qed
   453   next
   454     show "z/y \<in> A"
   455     proof (rule preal_downwards_closed [OF A x])
   456       show "0 < z/y"
   457         by (simp add: zero_less_divide_iff)
   458       show "z/y < x" by (simp add: pos_divide_less_eq zless)
   459     qed
   460   qed
   461 qed
   462 
   463 text{*Part 4 of Dedekind sections definition*}
   464 lemma mult_set_lemma4:
   465      "[|A \<in> preal; B \<in> preal; y \<in> mult_set A B|] ==> \<exists>u \<in> mult_set A B. y < u"
   466 apply (auto simp add: mult_set_def)
   467 apply (frule preal_exists_greater [of A], auto) 
   468 apply (rule_tac x="u * y" in exI)
   469 apply (auto intro: preal_imp_pos [of A] preal_imp_pos [of B] 
   470                    mult_strict_right_mono)
   471 done
   472 
   473 
   474 lemma mem_mult_set:
   475      "[|A \<in> preal; B \<in> preal|] ==> mult_set A B \<in> preal"
   476 apply (simp (no_asm_simp) add: preal_def cut_def)
   477 apply (blast intro!: mult_set_not_empty mult_set_not_rat_set
   478                      mult_set_lemma3 mult_set_lemma4)
   479 done
   480 
   481 lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)"
   482 apply (simp add: preal_mult_def mem_mult_set Rep_preal)
   483 apply (force simp add: mult_set_def mult_ac)
   484 done
   485 
   486 instance preal :: ab_semigroup_mult
   487 proof
   488   fix a b c :: preal
   489   show "(a * b) * c = a * (b * c)" by (rule preal_mult_assoc)
   490   show "a * b = b * a" by (rule preal_mult_commute)
   491 qed
   492 
   493 lemma preal_mult_left_commute: "x * (y * z) = y * ((x * z)::preal)"
   494 by (rule mult_left_commute)
   495 
   496 
   497 text{* Positive Real multiplication is an AC operator *}
   498 lemmas preal_mult_ac =
   499        preal_mult_assoc preal_mult_commute preal_mult_left_commute
   500 
   501 
   502 text{* Positive real 1 is the multiplicative identity element *}
   503 
   504 lemma preal_mult_1: "(1::preal) * z = z"
   505 unfolding preal_one_def
   506 proof (induct z)
   507   fix A :: "rat set"
   508   assume A: "A \<in> preal"
   509   have "{w. \<exists>u. 0 < u \<and> u < 1 & (\<exists>v \<in> A. w = u * v)} = A" (is "?lhs = A")
   510   proof
   511     show "?lhs \<subseteq> A"
   512     proof clarify
   513       fix x::rat and u::rat and v::rat
   514       assume upos: "0<u" and "u<1" and v: "v \<in> A"
   515       have vpos: "0<v" by (rule preal_imp_pos [OF A v])
   516       hence "u*v < 1*v" by (simp only: mult_strict_right_mono prems)
   517       thus "u * v \<in> A"
   518         by (force intro: preal_downwards_closed [OF A v] mult_pos_pos 
   519           upos vpos)
   520     qed
   521   next
   522     show "A \<subseteq> ?lhs"
   523     proof clarify
   524       fix x::rat
   525       assume x: "x \<in> A"
   526       have xpos: "0<x" by (rule preal_imp_pos [OF A x])
   527       from preal_exists_greater [OF A x]
   528       obtain v where v: "v \<in> A" and xlessv: "x < v" ..
   529       have vpos: "0<v" by (rule preal_imp_pos [OF A v])
   530       show "\<exists>u. 0 < u \<and> u < 1 \<and> (\<exists>v\<in>A. x = u * v)"
   531       proof (intro exI conjI)
   532         show "0 < x/v"
   533           by (simp add: zero_less_divide_iff xpos vpos)
   534         show "x / v < 1"
   535           by (simp add: pos_divide_less_eq vpos xlessv)
   536         show "\<exists>v'\<in>A. x = (x / v) * v'"
   537         proof
   538           show "x = (x/v)*v"
   539             by (simp add: divide_inverse mult_assoc vpos
   540                           order_less_imp_not_eq2)
   541           show "v \<in> A" by fact
   542         qed
   543       qed
   544     qed
   545   qed
   546   thus "preal_of_rat 1 * Abs_preal A = Abs_preal A"
   547     by (simp add: preal_of_rat_def preal_mult_def mult_set_def 
   548                   rat_mem_preal A)
   549 qed
   550 
   551 instance preal :: comm_monoid_mult
   552 by intro_classes (rule preal_mult_1)
   553 
   554 lemma preal_mult_1_right: "z * (1::preal) = z"
   555 by (rule mult_1_right)
   556 
   557 
   558 subsection{*Distribution of Multiplication across Addition*}
   559 
   560 lemma mem_Rep_preal_add_iff:
   561       "(z \<in> Rep_preal(R+S)) = (\<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. z = x + y)"
   562 apply (simp add: preal_add_def mem_add_set Rep_preal)
   563 apply (simp add: add_set_def) 
   564 done
   565 
   566 lemma mem_Rep_preal_mult_iff:
   567       "(z \<in> Rep_preal(R*S)) = (\<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. z = x * y)"
   568 apply (simp add: preal_mult_def mem_mult_set Rep_preal)
   569 apply (simp add: mult_set_def) 
   570 done
   571 
   572 lemma distrib_subset1:
   573      "Rep_preal (w * (x + y)) \<subseteq> Rep_preal (w * x + w * y)"
   574 apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff)
   575 apply (force simp add: right_distrib)
   576 done
   577 
   578 lemma preal_add_mult_distrib_mean:
   579   assumes a: "a \<in> Rep_preal w"
   580     and b: "b \<in> Rep_preal w"
   581     and d: "d \<in> Rep_preal x"
   582     and e: "e \<in> Rep_preal y"
   583   shows "\<exists>c \<in> Rep_preal w. a * d + b * e = c * (d + e)"
   584 proof
   585   let ?c = "(a*d + b*e)/(d+e)"
   586   have [simp]: "0<a" "0<b" "0<d" "0<e" "0<d+e"
   587     by (blast intro: preal_imp_pos [OF Rep_preal] a b d e pos_add_strict)+
   588   have cpos: "0 < ?c"
   589     by (simp add: zero_less_divide_iff zero_less_mult_iff pos_add_strict)
   590   show "a * d + b * e = ?c * (d + e)"
   591     by (simp add: divide_inverse mult_assoc order_less_imp_not_eq2)
   592   show "?c \<in> Rep_preal w"
   593   proof (cases rule: linorder_le_cases)
   594     assume "a \<le> b"
   595     hence "?c \<le> b"
   596       by (simp add: pos_divide_le_eq right_distrib mult_right_mono
   597                     order_less_imp_le)
   598     thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal b cpos])
   599   next
   600     assume "b \<le> a"
   601     hence "?c \<le> a"
   602       by (simp add: pos_divide_le_eq right_distrib mult_right_mono
   603                     order_less_imp_le)
   604     thus ?thesis by (rule preal_downwards_closed' [OF Rep_preal a cpos])
   605   qed
   606 qed
   607 
   608 lemma distrib_subset2:
   609      "Rep_preal (w * x + w * y) \<subseteq> Rep_preal (w * (x + y))"
   610 apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_mult_iff)
   611 apply (drule_tac w=w and x=x and y=y in preal_add_mult_distrib_mean, auto)
   612 done
   613 
   614 lemma preal_add_mult_distrib2: "(w * ((x::preal) + y)) = (w * x) + (w * y)"
   615 apply (rule Rep_preal_inject [THEN iffD1])
   616 apply (rule equalityI [OF distrib_subset1 distrib_subset2])
   617 done
   618 
   619 lemma preal_add_mult_distrib: "(((x::preal) + y) * w) = (x * w) + (y * w)"
   620 by (simp add: preal_mult_commute preal_add_mult_distrib2)
   621 
   622 instance preal :: comm_semiring
   623 by intro_classes (rule preal_add_mult_distrib)
   624 
   625 
   626 subsection{*Existence of Inverse, a Positive Real*}
   627 
   628 lemma mem_inv_set_ex:
   629   assumes A: "A \<in> preal" shows "\<exists>x y. 0 < x & x < y & inverse y \<notin> A"
   630 proof -
   631   from preal_exists_bound [OF A]
   632   obtain x where [simp]: "0<x" "x \<notin> A" by blast
   633   show ?thesis
   634   proof (intro exI conjI)
   635     show "0 < inverse (x+1)"
   636       by (simp add: order_less_trans [OF _ less_add_one]) 
   637     show "inverse(x+1) < inverse x"
   638       by (simp add: less_imp_inverse_less less_add_one)
   639     show "inverse (inverse x) \<notin> A"
   640       by (simp add: order_less_imp_not_eq2)
   641   qed
   642 qed
   643 
   644 text{*Part 1 of Dedekind sections definition*}
   645 lemma inverse_set_not_empty:
   646      "A \<in> preal ==> {} \<subset> inverse_set A"
   647 apply (insert mem_inv_set_ex [of A])
   648 apply (auto simp add: inverse_set_def)
   649 done
   650 
   651 text{*Part 2 of Dedekind sections definition*}
   652 
   653 lemma preal_not_mem_inverse_set_Ex:
   654    assumes A: "A \<in> preal"  shows "\<exists>q. 0 < q & q \<notin> inverse_set A"
   655 proof -
   656   from preal_nonempty [OF A]
   657   obtain x where x: "x \<in> A" and  xpos [simp]: "0<x" ..
   658   show ?thesis
   659   proof (intro exI conjI)
   660     show "0 < inverse x" by simp
   661     show "inverse x \<notin> inverse_set A"
   662     proof -
   663       { fix y::rat 
   664         assume ygt: "inverse x < y"
   665         have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt])
   666         have iyless: "inverse y < x" 
   667           by (simp add: inverse_less_imp_less [of x] ygt)
   668         have "inverse y \<in> A"
   669           by (simp add: preal_downwards_closed [OF A x] iyless)}
   670      thus ?thesis by (auto simp add: inverse_set_def)
   671     qed
   672   qed
   673 qed
   674 
   675 lemma inverse_set_not_rat_set:
   676    assumes A: "A \<in> preal"  shows "inverse_set A < {r. 0 < r}"
   677 proof
   678   show "inverse_set A \<subseteq> {r. 0 < r}"  by (force simp add: inverse_set_def)
   679 next
   680   show "inverse_set A \<noteq> {r. 0 < r}"
   681     by (insert preal_not_mem_inverse_set_Ex [OF A], blast)
   682 qed
   683 
   684 text{*Part 3 of Dedekind sections definition*}
   685 lemma inverse_set_lemma3:
   686      "[|A \<in> preal; u \<in> inverse_set A; 0 < z; z < u|] 
   687       ==> z \<in> inverse_set A"
   688 apply (auto simp add: inverse_set_def)
   689 apply (auto intro: order_less_trans)
   690 done
   691 
   692 text{*Part 4 of Dedekind sections definition*}
   693 lemma inverse_set_lemma4:
   694      "[|A \<in> preal; y \<in> inverse_set A|] ==> \<exists>u \<in> inverse_set A. y < u"
   695 apply (auto simp add: inverse_set_def)
   696 apply (drule dense [of y]) 
   697 apply (blast intro: order_less_trans)
   698 done
   699 
   700 
   701 lemma mem_inverse_set:
   702      "A \<in> preal ==> inverse_set A \<in> preal"
   703 apply (simp (no_asm_simp) add: preal_def cut_def)
   704 apply (blast intro!: inverse_set_not_empty inverse_set_not_rat_set
   705                      inverse_set_lemma3 inverse_set_lemma4)
   706 done
   707 
   708 
   709 subsection{*Gleason's Lemma 9-3.4, page 122*}
   710 
   711 lemma Gleason9_34_exists:
   712   assumes A: "A \<in> preal"
   713     and "\<forall>x\<in>A. x + u \<in> A"
   714     and "0 \<le> z"
   715   shows "\<exists>b\<in>A. b + (of_int z) * u \<in> A"
   716 proof (cases z rule: int_cases)
   717   case (nonneg n)
   718   show ?thesis
   719   proof (simp add: prems, induct n)
   720     case 0
   721       from preal_nonempty [OF A]
   722       show ?case  by force 
   723     case (Suc k)
   724       from this obtain b where "b \<in> A" "b + of_nat k * u \<in> A" ..
   725       hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems)
   726       thus ?case by (force simp add: algebra_simps prems) 
   727   qed
   728 next
   729   case (neg n)
   730   with prems show ?thesis by simp
   731 qed
   732 
   733 lemma Gleason9_34_contra:
   734   assumes A: "A \<in> preal"
   735     shows "[|\<forall>x\<in>A. x + u \<in> A; 0 < u; 0 < y; y \<notin> A|] ==> False"
   736 proof (induct u, induct y)
   737   fix a::int and b::int
   738   fix c::int and d::int
   739   assume bpos [simp]: "0 < b"
   740     and dpos [simp]: "0 < d"
   741     and closed: "\<forall>x\<in>A. x + (Fract c d) \<in> A"
   742     and upos: "0 < Fract c d"
   743     and ypos: "0 < Fract a b"
   744     and notin: "Fract a b \<notin> A"
   745   have cpos [simp]: "0 < c" 
   746     by (simp add: zero_less_Fract_iff [OF dpos, symmetric] upos) 
   747   have apos [simp]: "0 < a" 
   748     by (simp add: zero_less_Fract_iff [OF bpos, symmetric] ypos) 
   749   let ?k = "a*d"
   750   have frle: "Fract a b \<le> Fract ?k 1 * (Fract c d)" 
   751   proof -
   752     have "?thesis = ((a * d * b * d) \<le> c * b * (a * d * b * d))"
   753       by (simp add: mult_rat le_rat order_less_imp_not_eq2 mult_ac) 
   754     moreover
   755     have "(1 * (a * d * b * d)) \<le> c * b * (a * d * b * d)"
   756       by (rule mult_mono, 
   757           simp_all add: int_one_le_iff_zero_less zero_less_mult_iff 
   758                         order_less_imp_le)
   759     ultimately
   760     show ?thesis by simp
   761   qed
   762   have k: "0 \<le> ?k" by (simp add: order_less_imp_le zero_less_mult_iff)  
   763   from Gleason9_34_exists [OF A closed k]
   764   obtain z where z: "z \<in> A" 
   765              and mem: "z + of_int ?k * Fract c d \<in> A" ..
   766   have less: "z + of_int ?k * Fract c d < Fract a b"
   767     by (rule not_in_preal_ub [OF A notin mem ypos])
   768   have "0<z" by (rule preal_imp_pos [OF A z])
   769   with frle and less show False by (simp add: Fract_of_int_eq) 
   770 qed
   771 
   772 
   773 lemma Gleason9_34:
   774   assumes A: "A \<in> preal"
   775     and upos: "0 < u"
   776   shows "\<exists>r \<in> A. r + u \<notin> A"
   777 proof (rule ccontr, simp)
   778   assume closed: "\<forall>r\<in>A. r + u \<in> A"
   779   from preal_exists_bound [OF A]
   780   obtain y where y: "y \<notin> A" and ypos: "0 < y" by blast
   781   show False
   782     by (rule Gleason9_34_contra [OF A closed upos ypos y])
   783 qed
   784 
   785 
   786 
   787 subsection{*Gleason's Lemma 9-3.6*}
   788 
   789 lemma lemma_gleason9_36:
   790   assumes A: "A \<in> preal"
   791     and x: "1 < x"
   792   shows "\<exists>r \<in> A. r*x \<notin> A"
   793 proof -
   794   from preal_nonempty [OF A]
   795   obtain y where y: "y \<in> A" and  ypos: "0<y" ..
   796   show ?thesis 
   797   proof (rule classical)
   798     assume "~(\<exists>r\<in>A. r * x \<notin> A)"
   799     with y have ymem: "y * x \<in> A" by blast 
   800     from ypos mult_strict_left_mono [OF x]
   801     have yless: "y < y*x" by simp 
   802     let ?d = "y*x - y"
   803     from yless have dpos: "0 < ?d" and eq: "y + ?d = y*x" by auto
   804     from Gleason9_34 [OF A dpos]
   805     obtain r where r: "r\<in>A" and notin: "r + ?d \<notin> A" ..
   806     have rpos: "0<r" by (rule preal_imp_pos [OF A r])
   807     with dpos have rdpos: "0 < r + ?d" by arith
   808     have "~ (r + ?d \<le> y + ?d)"
   809     proof
   810       assume le: "r + ?d \<le> y + ?d" 
   811       from ymem have yd: "y + ?d \<in> A" by (simp add: eq)
   812       have "r + ?d \<in> A" by (rule preal_downwards_closed' [OF A yd rdpos le])
   813       with notin show False by simp
   814     qed
   815     hence "y < r" by simp
   816     with ypos have  dless: "?d < (r * ?d)/y"
   817       by (simp add: pos_less_divide_eq mult_commute [of ?d]
   818                     mult_strict_right_mono dpos)
   819     have "r + ?d < r*x"
   820     proof -
   821       have "r + ?d < r + (r * ?d)/y" by (simp add: dless)
   822       also with ypos have "... = (r/y) * (y + ?d)"
   823         by (simp only: algebra_simps divide_inverse, simp)
   824       also have "... = r*x" using ypos
   825         by (simp add: times_divide_eq_left) 
   826       finally show "r + ?d < r*x" .
   827     qed
   828     with r notin rdpos
   829     show "\<exists>r\<in>A. r * x \<notin> A" by (blast dest:  preal_downwards_closed [OF A])
   830   qed  
   831 qed
   832 
   833 subsection{*Existence of Inverse: Part 2*}
   834 
   835 lemma mem_Rep_preal_inverse_iff:
   836       "(z \<in> Rep_preal(inverse R)) = 
   837        (0 < z \<and> (\<exists>y. z < y \<and> inverse y \<notin> Rep_preal R))"
   838 apply (simp add: preal_inverse_def mem_inverse_set Rep_preal)
   839 apply (simp add: inverse_set_def) 
   840 done
   841 
   842 lemma Rep_preal_of_rat:
   843      "0 < q ==> Rep_preal (preal_of_rat q) = {x. 0 < x \<and> x < q}"
   844 by (simp add: preal_of_rat_def rat_mem_preal) 
   845 
   846 lemma subset_inverse_mult_lemma:
   847   assumes xpos: "0 < x" and xless: "x < 1"
   848   shows "\<exists>r u y. 0 < r & r < y & inverse y \<notin> Rep_preal R & 
   849     u \<in> Rep_preal R & x = r * u"
   850 proof -
   851   from xpos and xless have "1 < inverse x" by (simp add: one_less_inverse_iff)
   852   from lemma_gleason9_36 [OF Rep_preal this]
   853   obtain r where r: "r \<in> Rep_preal R" 
   854              and notin: "r * (inverse x) \<notin> Rep_preal R" ..
   855   have rpos: "0<r" by (rule preal_imp_pos [OF Rep_preal r])
   856   from preal_exists_greater [OF Rep_preal r]
   857   obtain u where u: "u \<in> Rep_preal R" and rless: "r < u" ..
   858   have upos: "0<u" by (rule preal_imp_pos [OF Rep_preal u])
   859   show ?thesis
   860   proof (intro exI conjI)
   861     show "0 < x/u" using xpos upos
   862       by (simp add: zero_less_divide_iff)  
   863     show "x/u < x/r" using xpos upos rpos
   864       by (simp add: divide_inverse mult_less_cancel_left rless) 
   865     show "inverse (x / r) \<notin> Rep_preal R" using notin
   866       by (simp add: divide_inverse mult_commute) 
   867     show "u \<in> Rep_preal R" by (rule u) 
   868     show "x = x / u * u" using upos 
   869       by (simp add: divide_inverse mult_commute) 
   870   qed
   871 qed
   872 
   873 lemma subset_inverse_mult: 
   874      "Rep_preal(preal_of_rat 1) \<subseteq> Rep_preal(inverse R * R)"
   875 apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff 
   876                       mem_Rep_preal_mult_iff)
   877 apply (blast dest: subset_inverse_mult_lemma) 
   878 done
   879 
   880 lemma inverse_mult_subset_lemma:
   881   assumes rpos: "0 < r" 
   882     and rless: "r < y"
   883     and notin: "inverse y \<notin> Rep_preal R"
   884     and q: "q \<in> Rep_preal R"
   885   shows "r*q < 1"
   886 proof -
   887   have "q < inverse y" using rpos rless
   888     by (simp add: not_in_preal_ub [OF Rep_preal notin] q)
   889   hence "r * q < r/y" using rpos
   890     by (simp add: divide_inverse mult_less_cancel_left)
   891   also have "... \<le> 1" using rpos rless
   892     by (simp add: pos_divide_le_eq)
   893   finally show ?thesis .
   894 qed
   895 
   896 lemma inverse_mult_subset:
   897      "Rep_preal(inverse R * R) \<subseteq> Rep_preal(preal_of_rat 1)"
   898 apply (auto simp add: Bex_def Rep_preal_of_rat mem_Rep_preal_inverse_iff 
   899                       mem_Rep_preal_mult_iff)
   900 apply (simp add: zero_less_mult_iff preal_imp_pos [OF Rep_preal]) 
   901 apply (blast intro: inverse_mult_subset_lemma) 
   902 done
   903 
   904 lemma preal_mult_inverse: "inverse R * R = (1::preal)"
   905 unfolding preal_one_def
   906 apply (rule Rep_preal_inject [THEN iffD1])
   907 apply (rule equalityI [OF inverse_mult_subset subset_inverse_mult]) 
   908 done
   909 
   910 lemma preal_mult_inverse_right: "R * inverse R = (1::preal)"
   911 apply (rule preal_mult_commute [THEN subst])
   912 apply (rule preal_mult_inverse)
   913 done
   914 
   915 
   916 text{*Theorems needing @{text Gleason9_34}*}
   917 
   918 lemma Rep_preal_self_subset: "Rep_preal (R) \<subseteq> Rep_preal(R + S)"
   919 proof 
   920   fix r
   921   assume r: "r \<in> Rep_preal R"
   922   have rpos: "0<r" by (rule preal_imp_pos [OF Rep_preal r])
   923   from mem_Rep_preal_Ex 
   924   obtain y where y: "y \<in> Rep_preal S" ..
   925   have ypos: "0<y" by (rule preal_imp_pos [OF Rep_preal y])
   926   have ry: "r+y \<in> Rep_preal(R + S)" using r y
   927     by (auto simp add: mem_Rep_preal_add_iff)
   928   show "r \<in> Rep_preal(R + S)" using r ypos rpos 
   929     by (simp add:  preal_downwards_closed [OF Rep_preal ry]) 
   930 qed
   931 
   932 lemma Rep_preal_sum_not_subset: "~ Rep_preal (R + S) \<subseteq> Rep_preal(R)"
   933 proof -
   934   from mem_Rep_preal_Ex 
   935   obtain y where y: "y \<in> Rep_preal S" ..
   936   have ypos: "0<y" by (rule preal_imp_pos [OF Rep_preal y])
   937   from  Gleason9_34 [OF Rep_preal ypos]
   938   obtain r where r: "r \<in> Rep_preal R" and notin: "r + y \<notin> Rep_preal R" ..
   939   have "r + y \<in> Rep_preal (R + S)" using r y
   940     by (auto simp add: mem_Rep_preal_add_iff)
   941   thus ?thesis using notin by blast
   942 qed
   943 
   944 lemma Rep_preal_sum_not_eq: "Rep_preal (R + S) \<noteq> Rep_preal(R)"
   945 by (insert Rep_preal_sum_not_subset, blast)
   946 
   947 text{*at last, Gleason prop. 9-3.5(iii) page 123*}
   948 lemma preal_self_less_add_left: "(R::preal) < R + S"
   949 apply (unfold preal_less_def less_le)
   950 apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym])
   951 done
   952 
   953 lemma preal_self_less_add_right: "(R::preal) < S + R"
   954 by (simp add: preal_add_commute preal_self_less_add_left)
   955 
   956 lemma preal_not_eq_self: "x \<noteq> x + (y::preal)"
   957 by (insert preal_self_less_add_left [of x y], auto)
   958 
   959 
   960 subsection{*Subtraction for Positive Reals*}
   961 
   962 text{*Gleason prop. 9-3.5(iv), page 123: proving @{prop "A < B ==> \<exists>D. A + D =
   963 B"}. We define the claimed @{term D} and show that it is a positive real*}
   964 
   965 text{*Part 1 of Dedekind sections definition*}
   966 lemma diff_set_not_empty:
   967      "R < S ==> {} \<subset> diff_set (Rep_preal S) (Rep_preal R)"
   968 apply (auto simp add: preal_less_def diff_set_def elim!: equalityE) 
   969 apply (frule_tac x1 = S in Rep_preal [THEN preal_exists_greater])
   970 apply (drule preal_imp_pos [OF Rep_preal], clarify)
   971 apply (cut_tac a=x and b=u in add_eq_exists, force) 
   972 done
   973 
   974 text{*Part 2 of Dedekind sections definition*}
   975 lemma diff_set_nonempty:
   976      "\<exists>q. 0 < q & q \<notin> diff_set (Rep_preal S) (Rep_preal R)"
   977 apply (cut_tac X = S in Rep_preal_exists_bound)
   978 apply (erule exE)
   979 apply (rule_tac x = x in exI, auto)
   980 apply (simp add: diff_set_def) 
   981 apply (auto dest: Rep_preal [THEN preal_downwards_closed])
   982 done
   983 
   984 lemma diff_set_not_rat_set:
   985   "diff_set (Rep_preal S) (Rep_preal R) < {r. 0 < r}" (is "?lhs < ?rhs")
   986 proof
   987   show "?lhs \<subseteq> ?rhs" by (auto simp add: diff_set_def) 
   988   show "?lhs \<noteq> ?rhs" using diff_set_nonempty by blast
   989 qed
   990 
   991 text{*Part 3 of Dedekind sections definition*}
   992 lemma diff_set_lemma3:
   993      "[|R < S; u \<in> diff_set (Rep_preal S) (Rep_preal R); 0 < z; z < u|] 
   994       ==> z \<in> diff_set (Rep_preal S) (Rep_preal R)"
   995 apply (auto simp add: diff_set_def) 
   996 apply (rule_tac x=x in exI) 
   997 apply (drule Rep_preal [THEN preal_downwards_closed], auto)
   998 done
   999 
  1000 text{*Part 4 of Dedekind sections definition*}
  1001 lemma diff_set_lemma4:
  1002      "[|R < S; y \<in> diff_set (Rep_preal S) (Rep_preal R)|] 
  1003       ==> \<exists>u \<in> diff_set (Rep_preal S) (Rep_preal R). y < u"
  1004 apply (auto simp add: diff_set_def) 
  1005 apply (drule Rep_preal [THEN preal_exists_greater], clarify) 
  1006 apply (cut_tac a="x+y" and b=u in add_eq_exists, clarify)  
  1007 apply (rule_tac x="y+xa" in exI) 
  1008 apply (auto simp add: add_ac)
  1009 done
  1010 
  1011 lemma mem_diff_set:
  1012      "R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
  1013 apply (unfold preal_def cut_def)
  1014 apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
  1015                      diff_set_lemma3 diff_set_lemma4)
  1016 done
  1017 
  1018 lemma mem_Rep_preal_diff_iff:
  1019       "R < S ==>
  1020        (z \<in> Rep_preal(S-R)) = 
  1021        (\<exists>x. 0 < x & 0 < z & x \<notin> Rep_preal R & x + z \<in> Rep_preal S)"
  1022 apply (simp add: preal_diff_def mem_diff_set Rep_preal)
  1023 apply (force simp add: diff_set_def) 
  1024 done
  1025 
  1026 
  1027 text{*proving that @{term "R + D \<le> S"}*}
  1028 
  1029 lemma less_add_left_lemma:
  1030   assumes Rless: "R < S"
  1031     and a: "a \<in> Rep_preal R"
  1032     and cb: "c + b \<in> Rep_preal S"
  1033     and "c \<notin> Rep_preal R"
  1034     and "0 < b"
  1035     and "0 < c"
  1036   shows "a + b \<in> Rep_preal S"
  1037 proof -
  1038   have "0<a" by (rule preal_imp_pos [OF Rep_preal a])
  1039   moreover
  1040   have "a < c" using prems
  1041     by (blast intro: not_in_Rep_preal_ub ) 
  1042   ultimately show ?thesis using prems
  1043     by (simp add: preal_downwards_closed [OF Rep_preal cb]) 
  1044 qed
  1045 
  1046 lemma less_add_left_le1:
  1047        "R < (S::preal) ==> R + (S-R) \<le> S"
  1048 apply (auto simp add: Bex_def preal_le_def mem_Rep_preal_add_iff 
  1049                       mem_Rep_preal_diff_iff)
  1050 apply (blast intro: less_add_left_lemma) 
  1051 done
  1052 
  1053 subsection{*proving that @{term "S \<le> R + D"} --- trickier*}
  1054 
  1055 lemma lemma_sum_mem_Rep_preal_ex:
  1056      "x \<in> Rep_preal S ==> \<exists>e. 0 < e & x + e \<in> Rep_preal S"
  1057 apply (drule Rep_preal [THEN preal_exists_greater], clarify) 
  1058 apply (cut_tac a=x and b=u in add_eq_exists, auto) 
  1059 done
  1060 
  1061 lemma less_add_left_lemma2:
  1062   assumes Rless: "R < S"
  1063     and x:     "x \<in> Rep_preal S"
  1064     and xnot: "x \<notin>  Rep_preal R"
  1065   shows "\<exists>u v z. 0 < v & 0 < z & u \<in> Rep_preal R & z \<notin> Rep_preal R & 
  1066                      z + v \<in> Rep_preal S & x = u + v"
  1067 proof -
  1068   have xpos: "0<x" by (rule preal_imp_pos [OF Rep_preal x])
  1069   from lemma_sum_mem_Rep_preal_ex [OF x]
  1070   obtain e where epos: "0 < e" and xe: "x + e \<in> Rep_preal S" by blast
  1071   from  Gleason9_34 [OF Rep_preal epos]
  1072   obtain r where r: "r \<in> Rep_preal R" and notin: "r + e \<notin> Rep_preal R" ..
  1073   with x xnot xpos have rless: "r < x" by (blast intro: not_in_Rep_preal_ub)
  1074   from add_eq_exists [of r x]
  1075   obtain y where eq: "x = r+y" by auto
  1076   show ?thesis 
  1077   proof (intro exI conjI)
  1078     show "r \<in> Rep_preal R" by (rule r)
  1079     show "r + e \<notin> Rep_preal R" by (rule notin)
  1080     show "r + e + y \<in> Rep_preal S" using xe eq by (simp add: add_ac)
  1081     show "x = r + y" by (simp add: eq)
  1082     show "0 < r + e" using epos preal_imp_pos [OF Rep_preal r]
  1083       by simp
  1084     show "0 < y" using rless eq by arith
  1085   qed
  1086 qed
  1087 
  1088 lemma less_add_left_le2: "R < (S::preal) ==> S \<le> R + (S-R)"
  1089 apply (auto simp add: preal_le_def)
  1090 apply (case_tac "x \<in> Rep_preal R")
  1091 apply (cut_tac Rep_preal_self_subset [of R], force)
  1092 apply (auto simp add: Bex_def mem_Rep_preal_add_iff mem_Rep_preal_diff_iff)
  1093 apply (blast dest: less_add_left_lemma2)
  1094 done
  1095 
  1096 lemma less_add_left: "R < (S::preal) ==> R + (S-R) = S"
  1097 by (blast intro: antisym [OF less_add_left_le1 less_add_left_le2])
  1098 
  1099 lemma less_add_left_Ex: "R < (S::preal) ==> \<exists>D. R + D = S"
  1100 by (fast dest: less_add_left)
  1101 
  1102 lemma preal_add_less2_mono1: "R < (S::preal) ==> R + T < S + T"
  1103 apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc)
  1104 apply (rule_tac y1 = D in preal_add_commute [THEN subst])
  1105 apply (auto intro: preal_self_less_add_left simp add: preal_add_assoc [symmetric])
  1106 done
  1107 
  1108 lemma preal_add_less2_mono2: "R < (S::preal) ==> T + R < T + S"
  1109 by (auto intro: preal_add_less2_mono1 simp add: preal_add_commute [of T])
  1110 
  1111 lemma preal_add_right_less_cancel: "R + T < S + T ==> R < (S::preal)"
  1112 apply (insert linorder_less_linear [of R S], auto)
  1113 apply (drule_tac R = S and T = T in preal_add_less2_mono1)
  1114 apply (blast dest: order_less_trans) 
  1115 done
  1116 
  1117 lemma preal_add_left_less_cancel: "T + R < T + S ==> R <  (S::preal)"
  1118 by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute [of T])
  1119 
  1120 lemma preal_add_less_cancel_right: "((R::preal) + T < S + T) = (R < S)"
  1121 by (blast intro: preal_add_less2_mono1 preal_add_right_less_cancel)
  1122 
  1123 lemma preal_add_less_cancel_left: "(T + (R::preal) < T + S) = (R < S)"
  1124 by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel)
  1125 
  1126 lemma preal_add_le_cancel_right: "((R::preal) + T \<le> S + T) = (R \<le> S)"
  1127 by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_right) 
  1128 
  1129 lemma preal_add_le_cancel_left: "(T + (R::preal) \<le> T + S) = (R \<le> S)"
  1130 by (simp add: linorder_not_less [symmetric] preal_add_less_cancel_left) 
  1131 
  1132 lemma preal_add_less_mono:
  1133      "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)"
  1134 apply (auto dest!: less_add_left_Ex simp add: preal_add_ac)
  1135 apply (rule preal_add_assoc [THEN subst])
  1136 apply (rule preal_self_less_add_right)
  1137 done
  1138 
  1139 lemma preal_add_right_cancel: "(R::preal) + T = S + T ==> R = S"
  1140 apply (insert linorder_less_linear [of R S], safe)
  1141 apply (drule_tac [!] T = T in preal_add_less2_mono1, auto)
  1142 done
  1143 
  1144 lemma preal_add_left_cancel: "C + A = C + B ==> A = (B::preal)"
  1145 by (auto intro: preal_add_right_cancel simp add: preal_add_commute)
  1146 
  1147 lemma preal_add_left_cancel_iff: "(C + A = C + B) = ((A::preal) = B)"
  1148 by (fast intro: preal_add_left_cancel)
  1149 
  1150 lemma preal_add_right_cancel_iff: "(A + C = B + C) = ((A::preal) = B)"
  1151 by (fast intro: preal_add_right_cancel)
  1152 
  1153 lemmas preal_cancels =
  1154     preal_add_less_cancel_right preal_add_less_cancel_left
  1155     preal_add_le_cancel_right preal_add_le_cancel_left
  1156     preal_add_left_cancel_iff preal_add_right_cancel_iff
  1157 
  1158 instance preal :: linordered_cancel_ab_semigroup_add
  1159 proof
  1160   fix a b c :: preal
  1161   show "a + b = a + c \<Longrightarrow> b = c" by (rule preal_add_left_cancel)
  1162   show "a \<le> b \<Longrightarrow> c + a \<le> c + b" by (simp only: preal_add_le_cancel_left)
  1163 qed
  1164 
  1165 
  1166 subsection{*Completeness of type @{typ preal}*}
  1167 
  1168 text{*Prove that supremum is a cut*}
  1169 
  1170 text{*Part 1 of Dedekind sections definition*}
  1171 
  1172 lemma preal_sup_set_not_empty:
  1173      "P \<noteq> {} ==> {} \<subset> (\<Union>X \<in> P. Rep_preal(X))"
  1174 apply auto
  1175 apply (cut_tac X = x in mem_Rep_preal_Ex, auto)
  1176 done
  1177 
  1178 
  1179 text{*Part 2 of Dedekind sections definition*}
  1180 
  1181 lemma preal_sup_not_exists:
  1182      "\<forall>X \<in> P. X \<le> Y ==> \<exists>q. 0 < q & q \<notin> (\<Union>X \<in> P. Rep_preal(X))"
  1183 apply (cut_tac X = Y in Rep_preal_exists_bound)
  1184 apply (auto simp add: preal_le_def)
  1185 done
  1186 
  1187 lemma preal_sup_set_not_rat_set:
  1188      "\<forall>X \<in> P. X \<le> Y ==> (\<Union>X \<in> P. Rep_preal(X)) < {r. 0 < r}"
  1189 apply (drule preal_sup_not_exists)
  1190 apply (blast intro: preal_imp_pos [OF Rep_preal])  
  1191 done
  1192 
  1193 text{*Part 3 of Dedekind sections definition*}
  1194 lemma preal_sup_set_lemma3:
  1195      "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y; u \<in> (\<Union>X \<in> P. Rep_preal(X)); 0 < z; z < u|]
  1196       ==> z \<in> (\<Union>X \<in> P. Rep_preal(X))"
  1197 by (auto elim: Rep_preal [THEN preal_downwards_closed])
  1198 
  1199 text{*Part 4 of Dedekind sections definition*}
  1200 lemma preal_sup_set_lemma4:
  1201      "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y; y \<in> (\<Union>X \<in> P. Rep_preal(X)) |]
  1202           ==> \<exists>u \<in> (\<Union>X \<in> P. Rep_preal(X)). y < u"
  1203 by (blast dest: Rep_preal [THEN preal_exists_greater])
  1204 
  1205 lemma preal_sup:
  1206      "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
  1207 apply (unfold preal_def cut_def)
  1208 apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
  1209                      preal_sup_set_lemma3 preal_sup_set_lemma4)
  1210 done
  1211 
  1212 lemma preal_psup_le:
  1213      "[| \<forall>X \<in> P. X \<le> Y;  x \<in> P |] ==> x \<le> psup P"
  1214 apply (simp (no_asm_simp) add: preal_le_def) 
  1215 apply (subgoal_tac "P \<noteq> {}") 
  1216 apply (auto simp add: psup_def preal_sup) 
  1217 done
  1218 
  1219 lemma psup_le_ub: "[| P \<noteq> {}; \<forall>X \<in> P. X \<le> Y |] ==> psup P \<le> Y"
  1220 apply (simp (no_asm_simp) add: preal_le_def)
  1221 apply (simp add: psup_def preal_sup) 
  1222 apply (auto simp add: preal_le_def)
  1223 done
  1224 
  1225 text{*Supremum property*}
  1226 lemma preal_complete:
  1227      "[| P \<noteq> {}; \<forall>X \<in> P. X \<le> Y |] ==> (\<exists>X \<in> P. Z < X) = (Z < psup P)"
  1228 apply (simp add: preal_less_def psup_def preal_sup)
  1229 apply (auto simp add: preal_le_def)
  1230 apply (rename_tac U) 
  1231 apply (cut_tac x = U and y = Z in linorder_less_linear)
  1232 apply (auto simp add: preal_less_def)
  1233 done
  1234 
  1235 
  1236 subsection{*The Embedding from @{typ rat} into @{typ preal}*}
  1237 
  1238 lemma preal_of_rat_add_lemma1:
  1239      "[|x < y + z; 0 < x; 0 < y|] ==> x * y * inverse (y + z) < (y::rat)"
  1240 apply (frule_tac c = "y * inverse (y + z) " in mult_strict_right_mono)
  1241 apply (simp add: zero_less_mult_iff) 
  1242 apply (simp add: mult_ac)
  1243 done
  1244 
  1245 lemma preal_of_rat_add_lemma2:
  1246   assumes "u < x + y"
  1247     and "0 < x"
  1248     and "0 < y"
  1249     and "0 < u"
  1250   shows "\<exists>v w::rat. w < y & 0 < v & v < x & 0 < w & u = v + w"
  1251 proof (intro exI conjI)
  1252   show "u * x * inverse(x+y) < x" using prems 
  1253     by (simp add: preal_of_rat_add_lemma1) 
  1254   show "u * y * inverse(x+y) < y" using prems 
  1255     by (simp add: preal_of_rat_add_lemma1 add_commute [of x]) 
  1256   show "0 < u * x * inverse (x + y)" using prems
  1257     by (simp add: zero_less_mult_iff) 
  1258   show "0 < u * y * inverse (x + y)" using prems
  1259     by (simp add: zero_less_mult_iff) 
  1260   show "u = u * x * inverse (x + y) + u * y * inverse (x + y)" using prems
  1261     by (simp add: left_distrib [symmetric] right_distrib [symmetric] mult_ac)
  1262 qed
  1263 
  1264 lemma preal_of_rat_add:
  1265      "[| 0 < x; 0 < y|] 
  1266       ==> preal_of_rat ((x::rat) + y) = preal_of_rat x + preal_of_rat y"
  1267 apply (unfold preal_of_rat_def preal_add_def)
  1268 apply (simp add: rat_mem_preal) 
  1269 apply (rule_tac f = Abs_preal in arg_cong)
  1270 apply (auto simp add: add_set_def) 
  1271 apply (blast dest: preal_of_rat_add_lemma2) 
  1272 done
  1273 
  1274 lemma preal_of_rat_mult_lemma1:
  1275      "[|x < y; 0 < x; 0 < z|] ==> x * z * inverse y < (z::rat)"
  1276 apply (frule_tac c = "z * inverse y" in mult_strict_right_mono)
  1277 apply (simp add: zero_less_mult_iff)
  1278 apply (subgoal_tac "y * (z * inverse y) = z * (y * inverse y)")
  1279 apply (simp_all add: mult_ac)
  1280 done
  1281 
  1282 lemma preal_of_rat_mult_lemma2: 
  1283   assumes xless: "x < y * z"
  1284     and xpos: "0 < x"
  1285     and ypos: "0 < y"
  1286   shows "x * z * inverse y * inverse z < (z::rat)"
  1287 proof -
  1288   have "0 < y * z" using prems by simp
  1289   hence zpos:  "0 < z" using prems by (simp add: zero_less_mult_iff)
  1290   have "x * z * inverse y * inverse z = x * inverse y * (z * inverse z)"
  1291     by (simp add: mult_ac)
  1292   also have "... = x/y" using zpos
  1293     by (simp add: divide_inverse)
  1294   also from xless have "... < z"
  1295     by (simp add: pos_divide_less_eq [OF ypos] mult_commute)
  1296   finally show ?thesis .
  1297 qed
  1298 
  1299 lemma preal_of_rat_mult_lemma3:
  1300   assumes uless: "u < x * y"
  1301     and "0 < x"
  1302     and "0 < y"
  1303     and "0 < u"
  1304   shows "\<exists>v w::rat. v < x & w < y & 0 < v & 0 < w & u = v * w"
  1305 proof -
  1306   from dense [OF uless] 
  1307   obtain r where "u < r" "r < x * y" by blast
  1308   thus ?thesis
  1309   proof (intro exI conjI)
  1310   show "u * x * inverse r < x" using prems 
  1311     by (simp add: preal_of_rat_mult_lemma1) 
  1312   show "r * y * inverse x * inverse y < y" using prems
  1313     by (simp add: preal_of_rat_mult_lemma2)
  1314   show "0 < u * x * inverse r" using prems
  1315     by (simp add: zero_less_mult_iff) 
  1316   show "0 < r * y * inverse x * inverse y" using prems
  1317     by (simp add: zero_less_mult_iff) 
  1318   have "u * x * inverse r * (r * y * inverse x * inverse y) =
  1319         u * (r * inverse r) * (x * inverse x) * (y * inverse y)"
  1320     by (simp only: mult_ac)
  1321   thus "u = u * x * inverse r * (r * y * inverse x * inverse y)" using prems
  1322     by simp
  1323   qed
  1324 qed
  1325 
  1326 lemma preal_of_rat_mult:
  1327      "[| 0 < x; 0 < y|] 
  1328       ==> preal_of_rat ((x::rat) * y) = preal_of_rat x * preal_of_rat y"
  1329 apply (unfold preal_of_rat_def preal_mult_def)
  1330 apply (simp add: rat_mem_preal) 
  1331 apply (rule_tac f = Abs_preal in arg_cong)
  1332 apply (auto simp add: zero_less_mult_iff mult_strict_mono mult_set_def) 
  1333 apply (blast dest: preal_of_rat_mult_lemma3) 
  1334 done
  1335 
  1336 lemma preal_of_rat_less_iff:
  1337       "[| 0 < x; 0 < y|] ==> (preal_of_rat x < preal_of_rat y) = (x < y)"
  1338 by (force simp add: preal_of_rat_def preal_less_def rat_mem_preal) 
  1339 
  1340 lemma preal_of_rat_le_iff:
  1341       "[| 0 < x; 0 < y|] ==> (preal_of_rat x \<le> preal_of_rat y) = (x \<le> y)"
  1342 by (simp add: preal_of_rat_less_iff linorder_not_less [symmetric]) 
  1343 
  1344 lemma preal_of_rat_eq_iff:
  1345       "[| 0 < x; 0 < y|] ==> (preal_of_rat x = preal_of_rat y) = (x = y)"
  1346 by (simp add: preal_of_rat_le_iff order_eq_iff) 
  1347 
  1348 end