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