src/HOL/Real/PReal.thy
author paulson
Thu Jan 01 21:47:07 2004 +0100 (2004-01-01)
changeset 14335 9c0b5e081037
parent 12018 ec054019c910
child 14365 3d4df8c166ae
permissions -rw-r--r--
conversion of Real/PReal to Isar script;
type "complex" is now in class "field"
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@14335
    10
theory PReal = PRat:
paulson@5078
    11
paulson@7825
    12
typedef preal = "{A::prat set. {} < A & A < UNIV &
paulson@14335
    13
                               (\<forall>y \<in> A. ((\<forall>z. z < y --> z \<in> A) &
paulson@14335
    14
                                        (\<exists>u \<in> A. y < u)))}"
paulson@14335
    15
apply (rule exI) 
paulson@14335
    16
apply (rule preal_1) 
paulson@14335
    17
done
paulson@14335
    18
paulson@14335
    19
paulson@14335
    20
instance preal :: ord ..
paulson@14335
    21
instance preal :: plus ..
paulson@14335
    22
instance preal :: times ..
paulson@14335
    23
paulson@5078
    24
paulson@5078
    25
constdefs
paulson@14335
    26
  preal_of_prat :: "prat => preal"
paulson@7077
    27
   "preal_of_prat q     == Abs_preal({x::prat. x < q})"
paulson@5078
    28
paulson@14335
    29
  pinv       :: "preal => preal"
paulson@14335
    30
  "pinv(R)   == Abs_preal({w. \<exists>y. w < y & qinv y \<notin> Rep_preal(R)})"
paulson@5078
    31
paulson@14335
    32
  psup       :: "preal set => preal"
paulson@14335
    33
  "psup(P)   == Abs_preal({w. \<exists>X \<in> P. w \<in> Rep_preal(X)})"
paulson@5078
    34
paulson@14335
    35
defs (overloaded)
paulson@5078
    36
paulson@14335
    37
  preal_add_def:
paulson@14335
    38
    "R + S == Abs_preal({w. \<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). w = x + y})"
paulson@5078
    39
paulson@14335
    40
  preal_mult_def:
paulson@14335
    41
    "R * S == Abs_preal({w. \<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). w = x * y})"
paulson@5078
    42
paulson@14335
    43
  preal_less_def:
paulson@12018
    44
    "R < (S::preal) == Rep_preal(R) < Rep_preal(S)"
paulson@5078
    45
paulson@14335
    46
  preal_le_def:
paulson@14335
    47
    "R \<le> (S::preal) == Rep_preal(R) \<subseteq> Rep_preal(S)"
paulson@14335
    48
paulson@14335
    49
paulson@14335
    50
lemma inj_on_Abs_preal: "inj_on Abs_preal preal"
paulson@14335
    51
apply (rule inj_on_inverseI)
paulson@14335
    52
apply (erule Abs_preal_inverse)
paulson@14335
    53
done
paulson@14335
    54
paulson@14335
    55
declare inj_on_Abs_preal [THEN inj_on_iff, simp]
paulson@14335
    56
paulson@14335
    57
lemma inj_Rep_preal: "inj(Rep_preal)"
paulson@14335
    58
apply (rule inj_on_inverseI)
paulson@14335
    59
apply (rule Rep_preal_inverse)
paulson@14335
    60
done
paulson@14335
    61
paulson@14335
    62
lemma empty_not_mem_preal [simp]: "{} \<notin> preal"
paulson@14335
    63
by (unfold preal_def, fast)
paulson@14335
    64
paulson@14335
    65
lemma one_set_mem_preal: "{x::prat. x < prat_of_pnat (Abs_pnat (Suc 0))} \<in> preal"
paulson@14335
    66
apply (unfold preal_def)
paulson@14335
    67
apply (rule preal_1)
paulson@14335
    68
done
paulson@14335
    69
paulson@14335
    70
declare one_set_mem_preal [simp]
paulson@14335
    71
paulson@14335
    72
lemma preal_psubset_empty: "x \<in> preal ==> {} < x"
paulson@14335
    73
by (unfold preal_def, fast)
paulson@14335
    74
paulson@14335
    75
lemma Rep_preal_psubset_empty: "{} < Rep_preal x"
paulson@14335
    76
by (rule Rep_preal [THEN preal_psubset_empty])
paulson@14335
    77
paulson@14335
    78
lemma mem_Rep_preal_Ex: "\<exists>x. x \<in> Rep_preal X"
paulson@14335
    79
apply (cut_tac x = X in Rep_preal_psubset_empty)
paulson@14335
    80
apply (auto intro: equals0I [symmetric] simp add: psubset_def)
paulson@14335
    81
done
paulson@14335
    82
paulson@14335
    83
lemma prealI1:
paulson@14335
    84
      "[| {} < A; A < UNIV;
paulson@14335
    85
               (\<forall>y \<in> A. ((\<forall>z. z < y --> z \<in> A) &
paulson@14335
    86
                         (\<exists>u \<in> A. y < u))) |] ==> A \<in> preal"
paulson@14335
    87
apply (unfold preal_def, fast)
paulson@14335
    88
done
paulson@14335
    89
paulson@14335
    90
lemma prealI2:
paulson@14335
    91
      "[| {} < A; A < UNIV;
paulson@14335
    92
               \<forall>y \<in> A. (\<forall>z. z < y --> z \<in> A);
paulson@14335
    93
               \<forall>y \<in> A. (\<exists>u \<in> A. y < u) |] ==> A \<in> preal"
paulson@14335
    94
paulson@14335
    95
apply (unfold preal_def, best)
paulson@14335
    96
done
paulson@14335
    97
paulson@14335
    98
lemma prealE_lemma:
paulson@14335
    99
      "A \<in> preal ==> {} < A & A < UNIV &
paulson@14335
   100
                          (\<forall>y \<in> A. ((\<forall>z. z < y --> z \<in> A) &
paulson@14335
   101
                                   (\<exists>u \<in> A. y < u)))"
paulson@14335
   102
apply (unfold preal_def, fast)
paulson@14335
   103
done
paulson@14335
   104
paulson@14335
   105
declare prealI1 [intro!] prealI2 [intro!]
paulson@14335
   106
paulson@14335
   107
declare Abs_preal_inverse [simp]
paulson@14335
   108
paulson@14335
   109
paulson@14335
   110
lemma prealE_lemma1: "A \<in> preal ==> {} < A"
paulson@14335
   111
by (unfold preal_def, fast)
paulson@14335
   112
paulson@14335
   113
lemma prealE_lemma2: "A \<in> preal ==> A < UNIV"
paulson@14335
   114
by (unfold preal_def, fast)
paulson@14335
   115
paulson@14335
   116
lemma prealE_lemma3: "A \<in> preal ==> \<forall>y \<in> A. (\<forall>z. z < y --> z \<in> A)"
paulson@14335
   117
by (unfold preal_def, fast)
paulson@14335
   118
paulson@14335
   119
lemma prealE_lemma3a: "[| A \<in> preal; y \<in> A |] ==> (\<forall>z. z < y --> z \<in> A)"
paulson@14335
   120
by (fast dest!: prealE_lemma3)
paulson@14335
   121
paulson@14335
   122
lemma prealE_lemma3b: "[| A \<in> preal; y \<in> A; z < y |] ==> z \<in> A"
paulson@14335
   123
by (fast dest!: prealE_lemma3a)
paulson@14335
   124
paulson@14335
   125
lemma prealE_lemma4: "A \<in> preal ==> \<forall>y \<in> A. (\<exists>u \<in> A. y < u)"
paulson@14335
   126
by (unfold preal_def, fast)
paulson@14335
   127
paulson@14335
   128
lemma prealE_lemma4a: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
paulson@14335
   129
by (fast dest!: prealE_lemma4)
paulson@14335
   130
paulson@14335
   131
lemma not_mem_Rep_preal_Ex: "\<exists>x. x\<notin> Rep_preal X"
paulson@14335
   132
apply (cut_tac x = X in Rep_preal)
paulson@14335
   133
apply (drule prealE_lemma2)
paulson@14335
   134
apply (auto simp add: psubset_def)
paulson@14335
   135
done
paulson@14335
   136
paulson@14335
   137
paulson@14335
   138
subsection{*@{term preal_of_prat}: the Injection from prat to preal*}
paulson@14335
   139
paulson@14335
   140
text{*A few lemmas*}
paulson@14335
   141
paulson@14335
   142
lemma lemma_prat_less_set_mem_preal: "{u::prat. u < y} \<in> preal"
paulson@14335
   143
apply (cut_tac qless_Ex)
paulson@14335
   144
apply (auto intro: prat_less_trans elim!: prat_less_irrefl)
paulson@14335
   145
apply (blast dest: prat_dense)
paulson@14335
   146
done
paulson@14335
   147
paulson@14335
   148
lemma lemma_prat_set_eq: "{u::prat. u < x} = {x. x < y} ==> x = y"
paulson@14335
   149
apply (insert prat_linear [of x y], safe)
paulson@14335
   150
apply (drule_tac [2] prat_dense, erule_tac [2] exE)
paulson@14335
   151
apply (drule prat_dense, erule exE)
paulson@14335
   152
apply (blast dest: prat_less_not_sym)
paulson@14335
   153
apply (blast dest: prat_less_not_sym)
paulson@14335
   154
done
paulson@14335
   155
paulson@14335
   156
lemma inj_preal_of_prat: "inj(preal_of_prat)"
paulson@14335
   157
apply (rule inj_onI)
paulson@14335
   158
apply (unfold preal_of_prat_def)
paulson@14335
   159
apply (drule inj_on_Abs_preal [THEN inj_onD])
paulson@14335
   160
apply (rule lemma_prat_less_set_mem_preal)
paulson@14335
   161
apply (rule lemma_prat_less_set_mem_preal)
paulson@14335
   162
apply (erule lemma_prat_set_eq)
paulson@14335
   163
done
paulson@14335
   164
paulson@14335
   165
paulson@14335
   166
subsection{*Theorems for Ordering*}
paulson@14335
   167
paulson@14335
   168
text{*A positive fraction not in a positive real is an upper bound.
paulson@14335
   169
 Gleason p. 122 - Remark (1)*}
paulson@14335
   170
paulson@14335
   171
lemma not_in_preal_ub: "x \<notin> Rep_preal(R) ==> \<forall>y \<in> Rep_preal(R). y < x"
paulson@14335
   172
apply (cut_tac x1 = R in Rep_preal [THEN prealE_lemma]) 
paulson@14335
   173
apply (blast intro: not_less_not_eq_prat_less)
paulson@14335
   174
done
paulson@14335
   175
paulson@14335
   176
paulson@14335
   177
text{*@{text preal_less} is a strict order: nonreflexive and transitive *}
paulson@14335
   178
paulson@14335
   179
lemma preal_less_not_refl: "~ (x::preal) < x"
paulson@14335
   180
apply (unfold preal_less_def)
paulson@14335
   181
apply (simp (no_asm) add: psubset_def)
paulson@14335
   182
done
paulson@14335
   183
paulson@14335
   184
lemmas preal_less_irrefl = preal_less_not_refl [THEN notE, standard]
paulson@14335
   185
paulson@14335
   186
lemma preal_not_refl2: "!!(x::preal). x < y ==> x \<noteq> y"
paulson@14335
   187
by (auto simp add: preal_less_not_refl)
paulson@14335
   188
paulson@14335
   189
lemma preal_less_trans: "!!(x::preal). [| x < y; y < z |] ==> x < z"
paulson@14335
   190
apply (unfold preal_less_def)
paulson@14335
   191
apply (auto dest: subsetD equalityI simp add: psubset_def)
paulson@14335
   192
done
paulson@14335
   193
paulson@14335
   194
lemma preal_less_not_sym: "!! (q1::preal). q1 < q2 ==> ~ q2 < q1"
paulson@14335
   195
apply (rule notI)
paulson@14335
   196
apply (drule preal_less_trans, assumption)
paulson@14335
   197
apply (simp add: preal_less_not_refl)
paulson@14335
   198
done
paulson@14335
   199
paulson@14335
   200
(* [| x < y;  ~P ==> y < x |] ==> P *)
paulson@14335
   201
lemmas preal_less_asym = preal_less_not_sym [THEN contrapos_np, standard]
paulson@14335
   202
paulson@14335
   203
lemma preal_linear:
paulson@14335
   204
      "(x::preal) < y | x = y | y < x"
paulson@14335
   205
apply (unfold preal_less_def)
paulson@14335
   206
apply (auto dest!: inj_Rep_preal [THEN injD] simp add: psubset_def)
paulson@14335
   207
apply (rule prealE_lemma3b, rule Rep_preal, assumption)
paulson@14335
   208
apply (fast dest: not_in_preal_ub)
paulson@14335
   209
done
paulson@14335
   210
paulson@14335
   211
paulson@14335
   212
subsection{*Properties of Addition*}
paulson@14335
   213
paulson@14335
   214
lemma preal_add_commute: "(x::preal) + y = y + x"
paulson@14335
   215
apply (unfold preal_add_def)
paulson@14335
   216
apply (rule_tac f = Abs_preal in arg_cong)
paulson@14335
   217
apply (blast intro: prat_add_commute [THEN subst])
paulson@14335
   218
done
paulson@14335
   219
paulson@14335
   220
text{*Addition of two positive reals gives a positive real*}
paulson@14335
   221
paulson@14335
   222
text{*Lemmas for proving positive reals addition set in @{typ preal}*}
paulson@14335
   223
paulson@14335
   224
text{*Part 1 of Dedekind sections definition*}
paulson@14335
   225
lemma preal_add_set_not_empty:
paulson@14335
   226
     "{} < {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}"
paulson@14335
   227
apply (cut_tac mem_Rep_preal_Ex mem_Rep_preal_Ex)
paulson@14335
   228
apply (auto intro!: psubsetI)
paulson@14335
   229
done
paulson@14335
   230
paulson@14335
   231
text{*Part 2 of Dedekind sections definition*}
paulson@14335
   232
lemma preal_not_mem_add_set_Ex:
paulson@14335
   233
     "\<exists>q. q  \<notin> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}"
paulson@14335
   234
apply (cut_tac X = R in not_mem_Rep_preal_Ex)
paulson@14335
   235
apply (cut_tac X = S in not_mem_Rep_preal_Ex, clarify) 
paulson@14335
   236
apply (drule not_in_preal_ub)+
paulson@14335
   237
apply (rule_tac x = "x+xa" in exI)
paulson@14335
   238
apply (auto dest!: bspec) 
paulson@14335
   239
apply (drule prat_add_less_mono)
paulson@14335
   240
apply (auto simp add: prat_less_not_refl)
paulson@14335
   241
done
paulson@14335
   242
paulson@14335
   243
lemma preal_add_set_not_prat_set:
paulson@14335
   244
     "{w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y} < UNIV"
paulson@14335
   245
apply (auto intro!: psubsetI)
paulson@14335
   246
apply (cut_tac R = R and S = S in preal_not_mem_add_set_Ex, auto)
paulson@14335
   247
done
paulson@14335
   248
paulson@14335
   249
text{*Part 3 of Dedekind sections definition*}
paulson@14335
   250
lemma preal_add_set_lemma3:
paulson@14335
   251
     "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}.
paulson@14335
   252
         \<forall>z. z < y --> z \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x+y}"
paulson@14335
   253
apply auto
paulson@14335
   254
apply (frule prat_mult_qinv_less_1)
paulson@14335
   255
apply (frule_tac x = x 
paulson@14335
   256
       in prat_mult_less2_mono1 [of _ "prat_of_pnat (Abs_pnat (Suc 0))"])
paulson@14335
   257
apply (frule_tac x = ya 
paulson@14335
   258
       in prat_mult_less2_mono1 [of _ "prat_of_pnat (Abs_pnat (Suc 0))"])
paulson@14335
   259
apply simp
paulson@14335
   260
apply (drule Rep_preal [THEN prealE_lemma3a])+
paulson@14335
   261
apply (erule allE)+
paulson@14335
   262
apply auto
paulson@14335
   263
apply (rule bexI)+
paulson@14335
   264
apply (auto simp add: prat_add_mult_distrib2 [symmetric] 
paulson@14335
   265
      prat_add_assoc [symmetric] prat_mult_assoc)
paulson@14335
   266
done
paulson@14335
   267
paulson@14335
   268
lemma preal_add_set_lemma4:
paulson@14335
   269
     "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}.
paulson@14335
   270
          \<exists>u \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y}. y < u"
paulson@14335
   271
apply auto
paulson@14335
   272
apply (drule Rep_preal [THEN prealE_lemma4a])
paulson@14335
   273
apply (auto intro: prat_add_less2_mono1)
paulson@14335
   274
done
paulson@14335
   275
paulson@14335
   276
lemma preal_mem_add_set:
paulson@14335
   277
     "{w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x + y} \<in> preal"
paulson@14335
   278
apply (rule prealI2)
paulson@14335
   279
apply (rule preal_add_set_not_empty)
paulson@14335
   280
apply (rule preal_add_set_not_prat_set)
paulson@14335
   281
apply (rule preal_add_set_lemma3)
paulson@14335
   282
apply (rule preal_add_set_lemma4)
paulson@14335
   283
done
paulson@14335
   284
paulson@14335
   285
lemma preal_add_assoc: "((x::preal) + y) + z = x + (y + z)"
paulson@14335
   286
apply (unfold preal_add_def)
paulson@14335
   287
apply (rule_tac f = Abs_preal in arg_cong)
paulson@14335
   288
apply (simp (no_asm) add: preal_mem_add_set [THEN Abs_preal_inverse])
paulson@14335
   289
apply (auto simp add: prat_add_ac)
paulson@14335
   290
apply (rule bexI)
paulson@14335
   291
apply (auto intro!: exI simp add: prat_add_ac)
paulson@14335
   292
done
paulson@14335
   293
paulson@14335
   294
lemma preal_add_left_commute: "x + (y + z) = y + ((x + z)::preal)"
paulson@14335
   295
  apply (rule mk_left_commute [of "op +"])
paulson@14335
   296
  apply (rule preal_add_assoc)
paulson@14335
   297
  apply (rule preal_add_commute)
paulson@14335
   298
  done
paulson@14335
   299
paulson@14335
   300
(* Positive Reals addition is an AC operator *)
paulson@14335
   301
lemmas preal_add_ac = preal_add_assoc preal_add_commute preal_add_left_commute
paulson@14335
   302
paulson@14335
   303
paulson@14335
   304
subsection{*Properties of Multiplication*}
paulson@14335
   305
paulson@14335
   306
text{*Proofs essentially same as for addition*}
paulson@14335
   307
paulson@14335
   308
lemma preal_mult_commute: "(x::preal) * y = y * x"
paulson@14335
   309
apply (unfold preal_mult_def)
paulson@14335
   310
apply (rule_tac f = Abs_preal in arg_cong)
paulson@14335
   311
apply (blast intro: prat_mult_commute [THEN subst])
paulson@14335
   312
done
paulson@14335
   313
paulson@14335
   314
text{*Multiplication of two positive reals gives a positive real.}
paulson@14335
   315
paulson@14335
   316
text{*Lemmas for proving positive reals multiplication set in @{typ preal}*}
paulson@14335
   317
paulson@14335
   318
text{*Part 1 of Dedekind sections definition*}
paulson@14335
   319
lemma preal_mult_set_not_empty:
paulson@14335
   320
     "{} < {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}"
paulson@14335
   321
apply (cut_tac mem_Rep_preal_Ex mem_Rep_preal_Ex)
paulson@14335
   322
apply (auto intro!: psubsetI)
paulson@14335
   323
done
paulson@14335
   324
paulson@14335
   325
text{*Part 2 of Dedekind sections definition*}
paulson@14335
   326
lemma preal_not_mem_mult_set_Ex:
paulson@14335
   327
     "\<exists>q. q  \<notin> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}"
paulson@14335
   328
apply (cut_tac X = R in not_mem_Rep_preal_Ex)
paulson@14335
   329
apply (cut_tac X = S in not_mem_Rep_preal_Ex)
paulson@14335
   330
apply (erule exE)+
paulson@14335
   331
apply (drule not_in_preal_ub)+
paulson@14335
   332
apply (rule_tac x = "x*xa" in exI)
paulson@14335
   333
apply (auto, (erule ballE)+, auto)
paulson@14335
   334
apply (drule prat_mult_less_mono)
paulson@14335
   335
apply (auto simp add: prat_less_not_refl)
paulson@14335
   336
done
paulson@14335
   337
paulson@14335
   338
lemma preal_mult_set_not_prat_set:
paulson@14335
   339
     "{w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y} < UNIV"
paulson@14335
   340
apply (auto intro!: psubsetI)
paulson@14335
   341
apply (cut_tac R = R and S = S in preal_not_mem_mult_set_Ex, auto)
paulson@14335
   342
done
paulson@14335
   343
paulson@14335
   344
text{*Part 3 of Dedekind sections definition*}
paulson@14335
   345
lemma preal_mult_set_lemma3:
paulson@14335
   346
     "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}.
paulson@14335
   347
         \<forall>z. z < y --> z \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x*y}"
paulson@14335
   348
apply auto
paulson@14335
   349
apply (frule_tac x = "qinv (ya)" in prat_mult_left_less2_mono1)
paulson@14335
   350
apply (simp add: prat_mult_ac)
paulson@14335
   351
apply (drule Rep_preal [THEN prealE_lemma3a])
paulson@14335
   352
apply (erule allE)
paulson@14335
   353
apply (rule bexI)+
paulson@14335
   354
apply (auto simp add: prat_mult_assoc)
paulson@14335
   355
done
paulson@14335
   356
paulson@14335
   357
lemma preal_mult_set_lemma4:
paulson@14335
   358
     "\<forall>y \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}.
paulson@14335
   359
          \<exists>u \<in> {w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y}. y < u"
paulson@14335
   360
apply auto
paulson@14335
   361
apply (drule Rep_preal [THEN prealE_lemma4a])
paulson@14335
   362
apply (auto intro: prat_mult_less2_mono1)
paulson@14335
   363
done
paulson@14335
   364
paulson@14335
   365
lemma preal_mem_mult_set:
paulson@14335
   366
     "{w. \<exists>x \<in> Rep_preal R. \<exists>y \<in> Rep_preal S. w = x * y} \<in> preal"
paulson@14335
   367
apply (rule prealI2)
paulson@14335
   368
apply (rule preal_mult_set_not_empty)
paulson@14335
   369
apply (rule preal_mult_set_not_prat_set)
paulson@14335
   370
apply (rule preal_mult_set_lemma3)
paulson@14335
   371
apply (rule preal_mult_set_lemma4)
paulson@14335
   372
done
paulson@14335
   373
paulson@14335
   374
lemma preal_mult_assoc: "((x::preal) * y) * z = x * (y * z)"
paulson@14335
   375
apply (unfold preal_mult_def)
paulson@14335
   376
apply (rule_tac f = Abs_preal in arg_cong)
paulson@14335
   377
apply (simp (no_asm) add: preal_mem_mult_set [THEN Abs_preal_inverse])
paulson@14335
   378
apply (auto simp add: prat_mult_ac)
paulson@14335
   379
apply (rule bexI)
paulson@14335
   380
apply (auto intro!: exI simp add: prat_mult_ac)
paulson@14335
   381
done
paulson@14335
   382
paulson@14335
   383
lemma preal_mult_left_commute: "x * (y * z) = y * ((x * z)::preal)"
paulson@14335
   384
  apply (rule mk_left_commute [of "op *"])
paulson@14335
   385
  apply (rule preal_mult_assoc)
paulson@14335
   386
  apply (rule preal_mult_commute)
paulson@14335
   387
  done
paulson@14335
   388
paulson@14335
   389
(* Positive Reals multiplication is an AC operator *)
paulson@14335
   390
lemmas preal_mult_ac =
paulson@14335
   391
       preal_mult_assoc preal_mult_commute preal_mult_left_commute
paulson@14335
   392
paulson@14335
   393
(* Positive Real 1 is the multiplicative identity element *)
paulson@14335
   394
(* long *)
paulson@14335
   395
lemma preal_mult_1:
paulson@14335
   396
      "(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) * z = z"
paulson@14335
   397
apply (unfold preal_of_prat_def preal_mult_def)
paulson@14335
   398
apply (rule Rep_preal_inverse [THEN subst])
paulson@14335
   399
apply (rule_tac f = Abs_preal in arg_cong)
paulson@14335
   400
apply (rule one_set_mem_preal [THEN Abs_preal_inverse, THEN ssubst])
paulson@14335
   401
apply (auto simp add: Rep_preal_inverse)
paulson@14335
   402
apply (drule Rep_preal [THEN prealE_lemma4a]) 
paulson@14335
   403
apply (erule bexE) 
paulson@14335
   404
apply (drule prat_mult_less_mono)
paulson@14335
   405
apply (auto dest: Rep_preal [THEN prealE_lemma3a])
paulson@14335
   406
apply (frule Rep_preal [THEN prealE_lemma4a]) 
paulson@14335
   407
apply (erule bexE) 
paulson@14335
   408
apply (frule_tac x = "qinv (u)" in prat_mult_less2_mono1)
paulson@14335
   409
apply (rule exI, auto, rule_tac x = u in bexI)
paulson@14335
   410
apply (auto simp add: prat_mult_assoc)
paulson@14335
   411
done
paulson@14335
   412
paulson@14335
   413
lemma preal_mult_1_right:
paulson@14335
   414
     "z * (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0)))) = z"
paulson@14335
   415
apply (rule preal_mult_commute [THEN subst])
paulson@14335
   416
apply (rule preal_mult_1)
paulson@14335
   417
done
paulson@14335
   418
paulson@14335
   419
paulson@14335
   420
subsection{*Distribution of Multiplication across Addition*}
paulson@14335
   421
paulson@14335
   422
lemma mem_Rep_preal_addD:
paulson@14335
   423
      "z \<in> Rep_preal(R+S) ==>
paulson@14335
   424
            \<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x + y"
paulson@14335
   425
apply (unfold preal_add_def)
paulson@14335
   426
apply (drule preal_mem_add_set [THEN Abs_preal_inverse, THEN subst], fast)
paulson@14335
   427
done
paulson@14335
   428
paulson@14335
   429
lemma mem_Rep_preal_addI:
paulson@14335
   430
      "\<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x + y
paulson@14335
   431
       ==> z \<in> Rep_preal(R+S)"
paulson@14335
   432
apply (unfold preal_add_def)
paulson@14335
   433
apply (rule preal_mem_add_set [THEN Abs_preal_inverse, THEN ssubst], fast)
paulson@14335
   434
done
paulson@14335
   435
paulson@14335
   436
lemma mem_Rep_preal_add_iff:
paulson@14335
   437
     "(z \<in> Rep_preal(R+S)) = (\<exists>x \<in> Rep_preal(R).
paulson@14335
   438
                                  \<exists>y \<in> Rep_preal(S). z = x + y)"
paulson@14335
   439
apply (fast intro!: mem_Rep_preal_addD mem_Rep_preal_addI)
paulson@14335
   440
done
paulson@14335
   441
paulson@14335
   442
lemma mem_Rep_preal_multD:
paulson@14335
   443
      "z \<in> Rep_preal(R*S) ==>
paulson@14335
   444
            \<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x * y"
paulson@14335
   445
apply (unfold preal_mult_def)
paulson@14335
   446
apply (drule preal_mem_mult_set [THEN Abs_preal_inverse, THEN subst], fast)
paulson@14335
   447
done
paulson@14335
   448
paulson@14335
   449
lemma mem_Rep_preal_multI:
paulson@14335
   450
      "\<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x * y
paulson@14335
   451
       ==> z \<in> Rep_preal(R*S)"
paulson@14335
   452
apply (unfold preal_mult_def)
paulson@14335
   453
apply (rule preal_mem_mult_set [THEN Abs_preal_inverse, THEN ssubst], fast)
paulson@14335
   454
done
paulson@14335
   455
paulson@14335
   456
lemma mem_Rep_preal_mult_iff:
paulson@14335
   457
     "(z \<in> Rep_preal(R*S)) =
paulson@14335
   458
      (\<exists>x \<in> Rep_preal(R). \<exists>y \<in> Rep_preal(S). z = x * y)"
paulson@14335
   459
by (fast intro!: mem_Rep_preal_multD mem_Rep_preal_multI)
paulson@14335
   460
paulson@14335
   461
lemma lemma_add_mult_mem_Rep_preal:
paulson@14335
   462
     "[| xb \<in> Rep_preal z1; xc \<in> Rep_preal z2; ya:
paulson@14335
   463
                   Rep_preal w; yb \<in> Rep_preal w |] ==>
paulson@14335
   464
                   xb * ya + xc * yb \<in> Rep_preal (z1 * w + z2 * w)"
paulson@14335
   465
by (fast intro: mem_Rep_preal_addI mem_Rep_preal_multI)
paulson@14335
   466
paulson@14335
   467
lemma lemma_add_mult_mem_Rep_preal1:
paulson@14335
   468
     "[| xb \<in> Rep_preal z1; xc \<in> Rep_preal z2; ya:
paulson@14335
   469
                   Rep_preal w; yb \<in> Rep_preal w |] ==>
paulson@14335
   470
                   yb*(xb + xc) \<in> Rep_preal (w*(z1 + z2))"
paulson@14335
   471
by (fast intro: mem_Rep_preal_addI mem_Rep_preal_multI)
paulson@14335
   472
paulson@14335
   473
lemma lemma_preal_add_mult_distrib:
paulson@14335
   474
     "x \<in> Rep_preal (w * z1 + w * z2) ==>
paulson@14335
   475
               x \<in> Rep_preal (w * (z1 + z2))"
paulson@14335
   476
apply (auto dest!: mem_Rep_preal_addD mem_Rep_preal_multD)
paulson@14335
   477
apply (frule_tac ya = xa and yb = xb and xb = ya and xc = yb in lemma_add_mult_mem_Rep_preal1, auto)
paulson@14335
   478
apply (rule_tac x = xa and y = xb in prat_linear_less2)
paulson@14335
   479
apply (drule_tac b = ya and c = yb in lemma_prat_add_mult_mono)
paulson@14335
   480
apply (rule Rep_preal [THEN prealE_lemma3b])
paulson@14335
   481
apply (auto simp add: prat_add_mult_distrib2)
paulson@14335
   482
apply (drule_tac ya = xb and yb = xa and xc = ya and xb = yb in lemma_add_mult_mem_Rep_preal1, auto)
paulson@14335
   483
apply (drule_tac b = yb and c = ya in lemma_prat_add_mult_mono)
paulson@14335
   484
apply (rule Rep_preal [THEN prealE_lemma3b])
paulson@14335
   485
apply (erule_tac V = "xb * ya + xb * yb \<in> Rep_preal (w * (z1 + z2))" in thin_rl)
paulson@14335
   486
apply (auto simp add: prat_add_mult_distrib prat_add_commute preal_add_ac)
paulson@14335
   487
done
paulson@14335
   488
paulson@14335
   489
lemma lemma_preal_add_mult_distrib2:
paulson@14335
   490
     "x \<in> Rep_preal (w * (z1 + z2)) ==>
paulson@14335
   491
               x \<in> Rep_preal (w * z1 + w * z2)"
paulson@14335
   492
by (auto dest!: mem_Rep_preal_addD mem_Rep_preal_multD
paulson@14335
   493
         intro!: bexI mem_Rep_preal_addI mem_Rep_preal_multI 
paulson@14335
   494
         simp add: prat_add_mult_distrib2)
paulson@14335
   495
paulson@14335
   496
lemma preal_add_mult_distrib2: "(w * ((z1::preal) + z2)) = (w * z1) + (w * z2)"
paulson@14335
   497
apply (rule inj_Rep_preal [THEN injD])
paulson@14335
   498
apply (fast intro: lemma_preal_add_mult_distrib lemma_preal_add_mult_distrib2)
paulson@14335
   499
done
paulson@14335
   500
paulson@14335
   501
lemma preal_add_mult_distrib: "(((z1::preal) + z2) * w) = (z1 * w) + (z2 * w)"
paulson@14335
   502
apply (simp (no_asm) add: preal_mult_commute preal_add_mult_distrib2)
paulson@14335
   503
done
paulson@14335
   504
paulson@14335
   505
paulson@14335
   506
subsection{*Existence of Inverse, a Positive Real*}
paulson@14335
   507
paulson@14335
   508
lemma qinv_not_mem_Rep_preal_Ex: "\<exists>y. qinv(y) \<notin>  Rep_preal X"
paulson@14335
   509
apply (cut_tac X = X in not_mem_Rep_preal_Ex)
paulson@14335
   510
apply (erule exE, cut_tac x = x in prat_as_inverse_ex, auto)
paulson@14335
   511
done
paulson@14335
   512
paulson@14335
   513
lemma lemma_preal_mem_inv_set_ex:
paulson@14335
   514
     "\<exists>q. q \<in> {x. \<exists>y. x < y & qinv y \<notin>  Rep_preal A}"
paulson@14335
   515
apply (cut_tac X = A in qinv_not_mem_Rep_preal_Ex, auto)
paulson@14335
   516
apply (cut_tac y = y in qless_Ex, fast)
paulson@14335
   517
done
paulson@14335
   518
paulson@14335
   519
text{*Part 1 of Dedekind sections definition*}
paulson@14335
   520
lemma preal_inv_set_not_empty: "{} < {x. \<exists>y. x < y & qinv y \<notin>  Rep_preal A}"
paulson@14335
   521
apply (cut_tac lemma_preal_mem_inv_set_ex)
paulson@14335
   522
apply (auto intro!: psubsetI)
paulson@14335
   523
done
paulson@14335
   524
paulson@14335
   525
text{*Part 2 of Dedekind sections definition*}
paulson@14335
   526
lemma qinv_mem_Rep_preal_Ex: "\<exists>y. qinv(y) \<in>  Rep_preal X"
paulson@14335
   527
apply (cut_tac X = X in mem_Rep_preal_Ex)
paulson@14335
   528
apply (erule exE, cut_tac x = x in prat_as_inverse_ex, auto)
paulson@14335
   529
done
paulson@14335
   530
paulson@14335
   531
lemma preal_not_mem_inv_set_Ex:
paulson@14335
   532
     "\<exists>x. x \<notin> {x. \<exists>y. x < y & qinv y \<notin>  Rep_preal A}"
paulson@14335
   533
apply (rule ccontr)
paulson@14335
   534
apply (cut_tac X = A in qinv_mem_Rep_preal_Ex, auto)
paulson@14335
   535
apply (erule allE, clarify) 
paulson@14335
   536
apply (drule qinv_prat_less, drule not_in_preal_ub)
paulson@14335
   537
apply (erule_tac x = "qinv y" in ballE)
paulson@14335
   538
apply (drule prat_less_trans)
paulson@14335
   539
apply (auto simp add: prat_less_not_refl)
paulson@14335
   540
done
paulson@14335
   541
paulson@14335
   542
lemma preal_inv_set_not_prat_set:
paulson@14335
   543
     "{x. \<exists>y. x < y & qinv y \<notin>  Rep_preal A} < UNIV"
paulson@14335
   544
apply (auto intro!: psubsetI)
paulson@14335
   545
apply (cut_tac A = A in preal_not_mem_inv_set_Ex, auto)
paulson@14335
   546
done
paulson@14335
   547
paulson@14335
   548
text{*Part 3 of Dedekind sections definition*}
paulson@14335
   549
lemma preal_inv_set_lemma3:
paulson@14335
   550
     "\<forall>y \<in> {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A}.
paulson@14335
   551
        \<forall>z. z < y --> z \<in> {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A}"
paulson@14335
   552
apply auto
paulson@14335
   553
apply (rule_tac x = ya in exI)
paulson@14335
   554
apply (auto intro: prat_less_trans)
paulson@14335
   555
done
paulson@14335
   556
paulson@14335
   557
lemma preal_inv_set_lemma4:
paulson@14335
   558
     "\<forall>y \<in> {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A}.
paulson@14335
   559
        Bex {x. \<exists>y. x < y & qinv y \<notin> Rep_preal A} (op < y)"
paulson@14335
   560
by (blast dest: prat_dense)
paulson@14335
   561
paulson@14335
   562
lemma preal_mem_inv_set: "{x. \<exists>y. x < y & qinv(y) \<notin> Rep_preal(A)} \<in> preal"
paulson@14335
   563
apply (rule prealI2)
paulson@14335
   564
apply (rule preal_inv_set_not_empty)
paulson@14335
   565
apply (rule preal_inv_set_not_prat_set)
paulson@14335
   566
apply (rule preal_inv_set_lemma3)
paulson@14335
   567
apply (rule preal_inv_set_lemma4)
paulson@14335
   568
done
paulson@14335
   569
paulson@14335
   570
(*more lemmas for inverse *)
paulson@14335
   571
lemma preal_mem_mult_invD:
paulson@14335
   572
     "x \<in> Rep_preal(pinv(A)*A) ==>
paulson@14335
   573
      x \<in> Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))"
paulson@14335
   574
apply (auto dest!: mem_Rep_preal_multD simp add: pinv_def preal_of_prat_def)
paulson@14335
   575
apply (drule preal_mem_inv_set [THEN Abs_preal_inverse, THEN subst])
paulson@14335
   576
apply (auto dest!: not_in_preal_ub)
paulson@14335
   577
apply (drule prat_mult_less_mono, blast, auto)
paulson@14335
   578
done
paulson@14335
   579
paulson@14335
   580
subsection{*Gleason's Lemma 9-3.4, page 122*}
paulson@14335
   581
paulson@14335
   582
lemma lemma1_gleason9_34:
paulson@14335
   583
     "\<forall>xa \<in> Rep_preal(A). xa + x \<in> Rep_preal(A) ==>
paulson@14335
   584
             \<exists>xb \<in> Rep_preal(A). xb + (prat_of_pnat p)*x \<in> Rep_preal(A)"
paulson@14335
   585
apply (cut_tac mem_Rep_preal_Ex)
paulson@14335
   586
apply (induct_tac "p" rule: pnat_induct)
paulson@14335
   587
apply (auto simp add: pnat_one_def pSuc_is_plus_one prat_add_mult_distrib 
paulson@14335
   588
                      prat_of_pnat_add prat_add_assoc [symmetric])
paulson@14335
   589
done
paulson@14335
   590
paulson@14335
   591
lemma lemma1b_gleason9_34:
paulson@14335
   592
     "Abs_prat (ratrel `` {(y, z)}) < 
paulson@14335
   593
      xb +
paulson@14335
   594
      Abs_prat (ratrel `` {(x*y, Abs_pnat (Suc 0))}) * 
paulson@14335
   595
      Abs_prat (ratrel `` {(w, x)})"
paulson@14335
   596
apply (rule_tac j =
paulson@14335
   597
        "Abs_prat (ratrel `` 
paulson@14335
   598
           { (x * y, Abs_pnat (Suc 0))}) * Abs_prat (ratrel `` {(w, x)})" 
paulson@14335
   599
       in prat_le_less_trans)
paulson@14335
   600
apply (rule_tac [2] prat_self_less_add_right)
paulson@14335
   601
apply (auto intro: lemma_Abs_prat_le3 
paulson@14335
   602
            simp add: prat_mult pre_lemma_gleason9_34b pnat_mult_assoc)
paulson@14335
   603
done
paulson@14335
   604
paulson@14335
   605
lemma lemma_gleason9_34a:
paulson@14335
   606
     "\<forall>xa \<in> Rep_preal(A). xa + x \<in> Rep_preal(A) ==> False"
paulson@14335
   607
apply (cut_tac X = A in not_mem_Rep_preal_Ex)
paulson@14335
   608
apply (erule exE)
paulson@14335
   609
apply (drule not_in_preal_ub)
paulson@14335
   610
apply (rule_tac z = x in eq_Abs_prat)
paulson@14335
   611
apply (rule_tac z = xa in eq_Abs_prat)
paulson@14335
   612
apply (drule_tac p = "y*xb" in lemma1_gleason9_34)
paulson@14335
   613
apply (erule bexE)
paulson@14335
   614
apply (cut_tac x = y and y = xb and w = xaa and z = ya and xb = xba in lemma1b_gleason9_34)
paulson@14335
   615
apply (drule_tac x = "xba + prat_of_pnat (y * xb) * x" in bspec)
paulson@14335
   616
apply (auto intro: prat_less_asym simp add: prat_of_pnat_def)
paulson@14335
   617
done
paulson@14335
   618
paulson@14335
   619
lemma lemma_gleason9_34: "\<exists>r \<in> Rep_preal(R). r + x \<notin> Rep_preal(R)"
paulson@14335
   620
apply (rule ccontr)
paulson@14335
   621
apply (blast intro: lemma_gleason9_34a)
paulson@14335
   622
done
paulson@14335
   623
paulson@14335
   624
paulson@14335
   625
subsection{*Gleason's Lemma 9-3.6*}
paulson@14335
   626
paulson@14335
   627
lemma lemma1_gleason9_36: "r + r*qinv(xa)*Q3 = r*qinv(xa)*(xa + Q3)"
paulson@14335
   628
apply (simp (no_asm_use) add: prat_add_mult_distrib2 prat_mult_assoc)
paulson@14335
   629
done
paulson@14335
   630
paulson@14335
   631
lemma lemma2_gleason9_36: "r*qinv(xa)*(xa*x) = r*x"
paulson@14335
   632
apply (simp (no_asm_use) add: prat_mult_ac)
paulson@14335
   633
done
paulson@14335
   634
paulson@14335
   635
(*** FIXME: long! ***)
paulson@14335
   636
lemma lemma_gleason9_36:
paulson@14335
   637
     "prat_of_pnat 1 < x ==> \<exists>r \<in> Rep_preal(A). r*x \<notin> Rep_preal(A)"
paulson@14335
   638
apply (rule_tac X1 = A in mem_Rep_preal_Ex [THEN exE])
paulson@14335
   639
apply (rule_tac Q = "xa*x \<in> Rep_preal (A) " in excluded_middle [THEN disjE])
paulson@14335
   640
apply fast
paulson@14335
   641
apply (drule_tac x = xa in prat_self_less_mult_right)
paulson@14335
   642
apply (erule prat_lessE)
paulson@14335
   643
apply (cut_tac R = A and x = Q3 in lemma_gleason9_34)
paulson@14335
   644
apply (drule sym, auto)
paulson@14335
   645
apply (frule not_in_preal_ub)
paulson@14335
   646
apply (drule_tac x = "xa + Q3" in bspec, assumption)
paulson@14335
   647
apply (drule prat_add_right_less_cancel)
paulson@14335
   648
apply (drule_tac x = "qinv (xa) *Q3" in prat_mult_less2_mono1)
paulson@14335
   649
apply (drule_tac x = r in prat_add_less2_mono2)
paulson@14335
   650
apply (simp add: prat_mult_assoc [symmetric] lemma1_gleason9_36)
paulson@14335
   651
apply (drule sym)
paulson@14335
   652
apply (auto simp add: lemma2_gleason9_36)
paulson@14335
   653
apply (rule_tac x = r in bexI)
paulson@14335
   654
apply (rule notI)
paulson@14335
   655
apply (drule_tac y = "r*x" in Rep_preal [THEN prealE_lemma3b], auto)
paulson@14335
   656
done
paulson@14335
   657
paulson@14335
   658
lemma lemma_gleason9_36a:
paulson@14335
   659
     "prat_of_pnat (Abs_pnat (Suc 0)) < x ==>
paulson@14335
   660
      \<exists>r \<in> Rep_preal(A). r*x \<notin> Rep_preal(A)"
paulson@14335
   661
apply (rule lemma_gleason9_36)
paulson@14335
   662
apply (simp (no_asm_simp) add: pnat_one_def)
paulson@14335
   663
done
paulson@14335
   664
paulson@14335
   665
paulson@14335
   666
subsection{*Existence of Inverse: Part 2*}
paulson@14335
   667
lemma preal_mem_mult_invI:
paulson@14335
   668
     "x \<in> Rep_preal(preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))
paulson@14335
   669
      ==> x \<in> Rep_preal(pinv(A)*A)"
paulson@14335
   670
apply (auto intro!: mem_Rep_preal_multI simp add: pinv_def preal_of_prat_def)
paulson@14335
   671
apply (rule preal_mem_inv_set [THEN Abs_preal_inverse, THEN ssubst])
paulson@14335
   672
apply (drule prat_qinv_gt_1)
paulson@14335
   673
apply (drule_tac A = A in lemma_gleason9_36a, auto)
paulson@14335
   674
apply (drule Rep_preal [THEN prealE_lemma4a])
paulson@14335
   675
apply (auto, drule qinv_prat_less)
paulson@14335
   676
apply (rule_tac x = "qinv (u) *x" in exI)
paulson@14335
   677
apply (rule conjI)
paulson@14335
   678
apply (rule_tac x = "qinv (r) *x" in exI)
paulson@14335
   679
apply (auto intro: prat_mult_less2_mono1 simp add: qinv_mult_eq qinv_qinv)
paulson@14335
   680
apply (rule_tac x = u in bexI)
paulson@14335
   681
apply (auto simp add: prat_mult_assoc prat_mult_left_commute)
paulson@14335
   682
done
paulson@14335
   683
paulson@14335
   684
lemma preal_mult_inv:
paulson@14335
   685
     "pinv(A)*A = (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))"
paulson@14335
   686
apply (rule inj_Rep_preal [THEN injD])
paulson@14335
   687
apply (fast dest: preal_mem_mult_invD preal_mem_mult_invI)
paulson@14335
   688
done
paulson@14335
   689
paulson@14335
   690
lemma preal_mult_inv_right:
paulson@14335
   691
     "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat (Suc 0))))"
paulson@14335
   692
apply (rule preal_mult_commute [THEN subst])
paulson@14335
   693
apply (rule preal_mult_inv)
paulson@14335
   694
done
paulson@14335
   695
paulson@14335
   696
paulson@14335
   697
text{*Theorems needing @{text lemma_gleason9_34}*}
paulson@14335
   698
paulson@14335
   699
lemma Rep_preal_self_subset: "Rep_preal (R1) \<subseteq> Rep_preal(R1 + R2)"
paulson@14335
   700
apply (cut_tac X = R2 in mem_Rep_preal_Ex)
paulson@14335
   701
apply (auto intro!: bexI 
paulson@14335
   702
            intro: Rep_preal [THEN prealE_lemma3b] prat_self_less_add_left 
paulson@14335
   703
                   mem_Rep_preal_addI)
paulson@14335
   704
done
paulson@14335
   705
paulson@14335
   706
lemma Rep_preal_sum_not_subset: "~ Rep_preal (R1 + R2) \<subseteq> Rep_preal(R1)"
paulson@14335
   707
apply (cut_tac X = R2 in mem_Rep_preal_Ex)
paulson@14335
   708
apply (erule exE)
paulson@14335
   709
apply (cut_tac R = R1 in lemma_gleason9_34)
paulson@14335
   710
apply (auto intro: mem_Rep_preal_addI)
paulson@14335
   711
done
paulson@14335
   712
paulson@14335
   713
lemma Rep_preal_sum_not_eq: "Rep_preal (R1 + R2) \<noteq> Rep_preal(R1)"
paulson@14335
   714
apply (rule notI)
paulson@14335
   715
apply (erule equalityE)
paulson@14335
   716
apply (simp add: Rep_preal_sum_not_subset)
paulson@14335
   717
done
paulson@14335
   718
paulson@14335
   719
text{*at last, Gleason prop. 9-3.5(iii) page 123*}
paulson@14335
   720
lemma preal_self_less_add_left: "(R1::preal) < R1 + R2"
paulson@14335
   721
apply (unfold preal_less_def psubset_def)
paulson@14335
   722
apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym])
paulson@14335
   723
done
paulson@14335
   724
paulson@14335
   725
lemma preal_self_less_add_right: "(R1::preal) < R2 + R1"
paulson@14335
   726
apply (simp add: preal_add_commute preal_self_less_add_left)
paulson@14335
   727
done
paulson@14335
   728
paulson@14335
   729
paulson@14335
   730
subsection{*The @{text "\<le>"} Ordering*}
paulson@14335
   731
paulson@14335
   732
lemma preal_less_le_iff: "(~(w < z)) = (z \<le> (w::preal))"
paulson@14335
   733
apply (unfold preal_le_def psubset_def preal_less_def)
paulson@14335
   734
apply (insert preal_linear [of w z])
paulson@14335
   735
apply (auto simp add: preal_less_def psubset_def)
paulson@14335
   736
done
paulson@14335
   737
paulson@14335
   738
lemma preal_le_iff_less_or_eq:
paulson@14335
   739
     "((x::preal) \<le> y) = (x < y | x = y)"
paulson@14335
   740
apply (unfold preal_le_def preal_less_def psubset_def)
paulson@14335
   741
apply (auto intro: inj_Rep_preal [THEN injD])
paulson@14335
   742
done
paulson@14335
   743
paulson@14335
   744
lemma preal_le_refl: "w \<le> (w::preal)"
paulson@14335
   745
apply (simp add: preal_le_def)
paulson@14335
   746
done
paulson@14335
   747
paulson@14335
   748
lemma preal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::preal)"
paulson@14335
   749
apply (simp add: preal_le_iff_less_or_eq) 
paulson@14335
   750
apply (blast intro: preal_less_trans)
paulson@14335
   751
done
paulson@14335
   752
paulson@14335
   753
lemma preal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::preal)"
paulson@14335
   754
apply (simp add: preal_le_iff_less_or_eq) 
paulson@14335
   755
apply (blast intro: preal_less_asym)
paulson@14335
   756
done
paulson@14335
   757
paulson@14335
   758
lemma preal_neq_iff: "(w \<noteq> z) = (w<z | z < (w::preal))"
paulson@14335
   759
apply (insert preal_linear [of w z])
paulson@14335
   760
apply (auto elim: preal_less_irrefl)
paulson@14335
   761
done
paulson@14335
   762
paulson@14335
   763
(* Axiom 'order_less_le' of class 'order': *)
paulson@14335
   764
lemma preal_less_le: "((w::preal) < z) = (w \<le> z & w \<noteq> z)"
paulson@14335
   765
apply (simp (no_asm) add: preal_less_le_iff [symmetric] preal_neq_iff)
paulson@14335
   766
apply (blast elim!: preal_less_asym)
paulson@14335
   767
done
paulson@14335
   768
paulson@14335
   769
instance preal :: order
paulson@14335
   770
proof qed
paulson@14335
   771
 (assumption |
paulson@14335
   772
  rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
paulson@14335
   773
paulson@14335
   774
lemma preal_le_linear: "x <= y | y <= (x::preal)"
paulson@14335
   775
apply (insert preal_linear [of x y]) 
paulson@14335
   776
apply (auto simp add: order_less_le) 
paulson@14335
   777
done
paulson@14335
   778
paulson@14335
   779
instance preal :: linorder
paulson@14335
   780
  by (intro_classes, rule preal_le_linear)
paulson@14335
   781
paulson@14335
   782
paulson@14335
   783
subsection{*Gleason prop. 9-3.5(iv), page 123*}
paulson@14335
   784
paulson@14335
   785
text{*Proving @{term "A < B ==> \<exists>D. A + D = B"}*}
paulson@14335
   786
paulson@14335
   787
text{*Define the claimed D and show that it is a positive real*}
paulson@14335
   788
paulson@14335
   789
text{*Part 1 of Dedekind sections definition*}
paulson@14335
   790
lemma lemma_ex_mem_less_left_add1:
paulson@14335
   791
     "A < B ==>
paulson@14335
   792
      \<exists>q. q \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}"
paulson@14335
   793
apply (unfold preal_less_def psubset_def)
paulson@14335
   794
apply (clarify) 
paulson@14335
   795
apply (drule_tac x1 = B in Rep_preal [THEN prealE_lemma4a])
paulson@14335
   796
apply (auto simp add: prat_less_def)
paulson@14335
   797
done
paulson@14335
   798
paulson@14335
   799
lemma preal_less_set_not_empty:
paulson@14335
   800
     "A < B ==> {} < {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}"
paulson@14335
   801
apply (drule lemma_ex_mem_less_left_add1)
paulson@14335
   802
apply (auto intro!: psubsetI)
paulson@14335
   803
done
paulson@14335
   804
paulson@14335
   805
text{*Part 2 of Dedekind sections definition*}
paulson@14335
   806
lemma lemma_ex_not_mem_less_left_add1:
paulson@14335
   807
     "\<exists>q. q \<notin> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}"
paulson@14335
   808
apply (cut_tac X = B in not_mem_Rep_preal_Ex)
paulson@14335
   809
apply (erule exE)
paulson@14335
   810
apply (rule_tac x = x in exI, auto)
paulson@14335
   811
apply (cut_tac x = x and y = n in prat_self_less_add_right)
paulson@14335
   812
apply (auto dest: Rep_preal [THEN prealE_lemma3b])
paulson@14335
   813
done
paulson@14335
   814
paulson@14335
   815
lemma preal_less_set_not_prat_set:
paulson@14335
   816
     "{d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)} < UNIV"
paulson@14335
   817
apply (auto intro!: psubsetI)
paulson@14335
   818
apply (cut_tac A = A and B = B in lemma_ex_not_mem_less_left_add1, auto)
paulson@14335
   819
done
paulson@14335
   820
paulson@14335
   821
text{*Part 3 of Dedekind sections definition*}
paulson@14335
   822
lemma preal_less_set_lemma3:
paulson@14335
   823
     "A < B ==> \<forall>y \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}.
paulson@14335
   824
     \<forall>z. z < y --> z \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}"
paulson@14335
   825
apply auto
paulson@14335
   826
apply (drule_tac x = n in prat_add_less2_mono2)
paulson@14335
   827
apply (drule Rep_preal [THEN prealE_lemma3b], auto)
paulson@14335
   828
done
paulson@14335
   829
paulson@14335
   830
lemma preal_less_set_lemma4:
paulson@14335
   831
     "A < B ==> \<forall>y \<in> {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}.
paulson@14335
   832
        Bex {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)} (op < y)"
paulson@14335
   833
apply auto
paulson@14335
   834
apply (drule Rep_preal [THEN prealE_lemma4a])
paulson@14335
   835
apply (auto simp add: prat_less_def prat_add_assoc)
paulson@14335
   836
done
paulson@14335
   837
paulson@14335
   838
lemma preal_mem_less_set:
paulson@14335
   839
     "!! (A::preal). A < B ==>
paulson@14335
   840
      {d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}: preal"
paulson@14335
   841
apply (rule prealI2)
paulson@14335
   842
apply (rule preal_less_set_not_empty)
paulson@14335
   843
apply (rule_tac [2] preal_less_set_not_prat_set)
paulson@14335
   844
apply (rule_tac [2] preal_less_set_lemma3)
paulson@14335
   845
apply (rule_tac [3] preal_less_set_lemma4, auto)
paulson@14335
   846
done
paulson@14335
   847
paulson@14335
   848
text{*proving that @{term "A + D \<le> B"}*}
paulson@14335
   849
lemma preal_less_add_left_subsetI:
paulson@14335
   850
       "!! (A::preal). A < B ==>
paulson@14335
   851
          A + Abs_preal({d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}) \<le> B"
paulson@14335
   852
apply (unfold preal_le_def)
paulson@14335
   853
apply (rule subsetI)
paulson@14335
   854
apply (drule mem_Rep_preal_addD)
paulson@14335
   855
apply (auto simp add: preal_mem_less_set [THEN Abs_preal_inverse])
paulson@14335
   856
apply (drule not_in_preal_ub)
paulson@14335
   857
apply (drule bspec, assumption)
paulson@14335
   858
apply (drule_tac x = y in prat_add_less2_mono1)
paulson@14335
   859
apply (drule_tac x1 = B in Rep_preal [THEN prealE_lemma3b], auto)
paulson@14335
   860
done
paulson@14335
   861
paulson@14335
   862
subsection{*proving that @{term "B \<le> A + D"} --- trickier*}
paulson@14335
   863
paulson@14335
   864
lemma lemma_sum_mem_Rep_preal_ex:
paulson@14335
   865
     "x \<in> Rep_preal(B) ==> \<exists>e. x + e \<in> Rep_preal(B)"
paulson@14335
   866
apply (drule Rep_preal [THEN prealE_lemma4a])
paulson@14335
   867
apply (auto simp add: prat_less_def)
paulson@14335
   868
done
paulson@14335
   869
paulson@14335
   870
lemma preal_less_add_left_subsetI2:
paulson@14335
   871
       "!! (A::preal). A < B ==>
paulson@14335
   872
          B \<le> A + Abs_preal({d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)})"
paulson@14335
   873
apply (unfold preal_le_def)
paulson@14335
   874
apply (rule subsetI)
paulson@14335
   875
apply (rule_tac Q = "x \<in> Rep_preal (A) " in excluded_middle [THEN disjE])
paulson@14335
   876
apply (rule mem_Rep_preal_addI)
paulson@14335
   877
apply (drule lemma_sum_mem_Rep_preal_ex)
paulson@14335
   878
apply (erule exE)
paulson@14335
   879
apply (cut_tac R = A and x = e in lemma_gleason9_34, erule bexE)
paulson@14335
   880
apply (drule not_in_preal_ub, drule bspec, assumption)
paulson@14335
   881
apply (erule prat_lessE)
paulson@14335
   882
apply (rule_tac x = r in bexI)
paulson@14335
   883
apply (rule_tac x = Q3 in bexI)
paulson@14335
   884
apply (cut_tac [4] Rep_preal_self_subset)
paulson@14335
   885
apply (auto simp add: preal_mem_less_set [THEN Abs_preal_inverse])
paulson@14335
   886
apply (rule_tac x = "r+e" in exI)
paulson@14335
   887
apply (simp add: prat_add_ac)
paulson@14335
   888
done
paulson@14335
   889
paulson@14335
   890
(*** required proof ***)
paulson@14335
   891
lemma preal_less_add_left:
paulson@14335
   892
     "!! (A::preal). A < B ==>
paulson@14335
   893
          A + Abs_preal({d. \<exists>n. n \<notin> Rep_preal(A) & n + d \<in> Rep_preal(B)}) = B"
paulson@14335
   894
apply (blast intro: preal_le_anti_sym preal_less_add_left_subsetI preal_less_add_left_subsetI2)
paulson@14335
   895
done
paulson@14335
   896
paulson@14335
   897
lemma preal_less_add_left_Ex: "!! (A::preal). A < B ==> \<exists>D. A + D = B"
paulson@14335
   898
by (fast dest: preal_less_add_left)
paulson@14335
   899
paulson@14335
   900
lemma preal_add_less2_mono1: "!!(A::preal). A < B ==> A + C < B + C"
paulson@14335
   901
apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_assoc)
paulson@14335
   902
apply (rule_tac y1 = D in preal_add_commute [THEN subst])
paulson@14335
   903
apply (auto intro: preal_self_less_add_left simp add: preal_add_assoc [symmetric])
paulson@14335
   904
done
paulson@14335
   905
paulson@14335
   906
lemma preal_add_less2_mono2: "!!(A::preal). A < B ==> C + A < C + B"
paulson@14335
   907
by (auto intro: preal_add_less2_mono1 simp add: preal_add_commute)
paulson@14335
   908
paulson@14335
   909
lemma preal_mult_less_mono1:
paulson@14335
   910
      "!!(q1::preal). q1 < q2 ==> q1 * x < q2 * x"
paulson@14335
   911
apply (drule preal_less_add_left_Ex)
paulson@14335
   912
apply (auto simp add: preal_add_mult_distrib preal_self_less_add_left)
paulson@14335
   913
done
paulson@14335
   914
paulson@14335
   915
lemma preal_mult_left_less_mono1: "!!(q1::preal). q1 < q2  ==> x * q1 < x * q2"
paulson@14335
   916
by (auto dest: preal_mult_less_mono1 simp add: preal_mult_commute)
paulson@14335
   917
paulson@14335
   918
lemma preal_mult_left_le_mono1: "!!(q1::preal). q1 \<le> q2  ==> x * q1 \<le> x * q2"
paulson@14335
   919
apply (simp add: preal_le_iff_less_or_eq) 
paulson@14335
   920
apply (blast intro!: preal_mult_left_less_mono1)
paulson@14335
   921
done
paulson@14335
   922
paulson@14335
   923
lemma preal_mult_le_mono1: "!!(q1::preal). q1 \<le> q2  ==> q1 * x \<le> q2 * x"
paulson@14335
   924
by (auto dest: preal_mult_left_le_mono1 simp add: preal_mult_commute)
paulson@14335
   925
paulson@14335
   926
lemma preal_add_left_le_mono1: "!!(q1::preal). q1 \<le> q2  ==> x + q1 \<le> x + q2"
paulson@14335
   927
apply (simp add: preal_le_iff_less_or_eq) 
paulson@14335
   928
apply (auto intro!: preal_add_less2_mono1 simp add: preal_add_commute)
paulson@14335
   929
done
paulson@14335
   930
paulson@14335
   931
lemma preal_add_le_mono1: "!!(q1::preal). q1 \<le> q2  ==> q1 + x \<le> q2 + x"
paulson@14335
   932
by (auto dest: preal_add_left_le_mono1 simp add: preal_add_commute)
paulson@14335
   933
paulson@14335
   934
lemma preal_add_right_less_cancel: "!!(A::preal). A + C < B + C ==> A < B"
paulson@14335
   935
apply (cut_tac preal_linear)
paulson@14335
   936
apply (auto elim: preal_less_irrefl)
paulson@14335
   937
apply (drule_tac A = B and C = C in preal_add_less2_mono1)
paulson@14335
   938
apply (fast dest: preal_less_trans elim: preal_less_irrefl)
paulson@14335
   939
done
paulson@14335
   940
paulson@14335
   941
lemma preal_add_left_less_cancel: "!!(A::preal). C + A < C + B ==> A < B"
paulson@14335
   942
by (auto elim: preal_add_right_less_cancel simp add: preal_add_commute)
paulson@14335
   943
paulson@14335
   944
lemma preal_add_less_iff1 [simp]: "((A::preal) + C < B + C) = (A < B)"
paulson@14335
   945
by (blast intro: preal_add_less2_mono1 preal_add_right_less_cancel)
paulson@14335
   946
paulson@14335
   947
lemma preal_add_less_iff2 [simp]: "(C + (A::preal) < C + B) = (A < B)"
paulson@14335
   948
by (blast intro: preal_add_less2_mono2 preal_add_left_less_cancel)
paulson@14335
   949
paulson@14335
   950
lemma preal_add_less_mono:
paulson@14335
   951
     "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)"
paulson@14335
   952
apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_ac)
paulson@14335
   953
apply (rule preal_add_assoc [THEN subst])
paulson@14335
   954
apply (rule preal_self_less_add_right)
paulson@14335
   955
done
paulson@14335
   956
paulson@14335
   957
lemma preal_mult_less_mono:
paulson@14335
   958
     "[| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::preal)"
paulson@14335
   959
apply (auto dest!: preal_less_add_left_Ex simp add: preal_add_mult_distrib preal_add_mult_distrib2 preal_self_less_add_left preal_add_assoc preal_mult_ac)
paulson@14335
   960
done
paulson@14335
   961
paulson@14335
   962
lemma preal_add_right_cancel: "(A::preal) + C = B + C ==> A = B"
paulson@14335
   963
apply (cut_tac preal_linear [of A B], safe)
paulson@14335
   964
apply (drule_tac [!] C = C in preal_add_less2_mono1)
paulson@14335
   965
apply (auto elim: preal_less_irrefl)
paulson@14335
   966
done
paulson@14335
   967
paulson@14335
   968
lemma preal_add_left_cancel: "!!(A::preal). C + A = C + B ==> A = B"
paulson@14335
   969
by (auto intro: preal_add_right_cancel simp add: preal_add_commute)
paulson@14335
   970
paulson@14335
   971
lemma preal_add_left_cancel_iff [simp]: "(C + A = C + B) = ((A::preal) = B)"
paulson@14335
   972
by (fast intro: preal_add_left_cancel)
paulson@14335
   973
paulson@14335
   974
lemma preal_add_right_cancel_iff [simp]: "(A + C = B + C) = ((A::preal) = B)"
paulson@14335
   975
by (fast intro: preal_add_right_cancel)
paulson@14335
   976
paulson@14335
   977
paulson@14335
   978
paulson@14335
   979
subsection{*Completeness of type @{typ preal}*}
paulson@14335
   980
paulson@14335
   981
text{*Prove that supremum is a cut*}
paulson@14335
   982
paulson@14335
   983
lemma preal_sup_mem_Ex:
paulson@14335
   984
     "\<exists>X. X \<in> P ==> \<exists>q.  q \<in> {w. \<exists>X. X \<in> P & w \<in> Rep_preal X}"
paulson@14335
   985
apply safe
paulson@14335
   986
apply (cut_tac X = X in mem_Rep_preal_Ex, auto)
paulson@14335
   987
done
paulson@14335
   988
paulson@14335
   989
text{*Part 1 of Dedekind sections definition*}
paulson@14335
   990
lemma preal_sup_set_not_empty:
paulson@14335
   991
     "\<exists>(X::preal). X \<in> P ==>
paulson@14335
   992
          {} < {w. \<exists>X \<in> P. w \<in> Rep_preal X}"
paulson@14335
   993
apply (drule preal_sup_mem_Ex)
paulson@14335
   994
apply (auto intro!: psubsetI)
paulson@14335
   995
done
paulson@14335
   996
paulson@14335
   997
text{*Part 2 of Dedekind sections definition*}
paulson@14335
   998
lemma preal_sup_not_mem_Ex:
paulson@14335
   999
     "\<exists>Y. (\<forall>X \<in> P. X < Y)
paulson@14335
  1000
          ==> \<exists>q. q \<notin> {w. \<exists>X. X \<in> P & w \<in> Rep_preal(X)}"
paulson@14335
  1001
apply (unfold preal_less_def)
paulson@14335
  1002
apply (auto simp add: psubset_def)
paulson@14335
  1003
apply (cut_tac X = Y in not_mem_Rep_preal_Ex)
paulson@14335
  1004
apply (erule exE)
paulson@14335
  1005
apply (rule_tac x = x in exI)
paulson@14335
  1006
apply (auto dest!: bspec)
paulson@14335
  1007
done
paulson@14335
  1008
paulson@14335
  1009
lemma preal_sup_not_mem_Ex1:
paulson@14335
  1010
     "\<exists>Y. (\<forall>X \<in> P. X \<le> Y)
paulson@14335
  1011
          ==> \<exists>q. q \<notin> {w. \<exists>X. X \<in> P & w \<in> Rep_preal(X)}"
paulson@14335
  1012
apply (unfold preal_le_def, safe)
paulson@14335
  1013
apply (cut_tac X = Y in not_mem_Rep_preal_Ex)
paulson@14335
  1014
apply (erule exE)
paulson@14335
  1015
apply (rule_tac x = x in exI)
paulson@14335
  1016
apply (auto dest!: bspec)
paulson@14335
  1017
done
paulson@14335
  1018
paulson@14335
  1019
lemma preal_sup_set_not_prat_set:
paulson@14335
  1020
     "\<exists>Y. (\<forall>X \<in> P. X < Y) ==> {w. \<exists>X \<in> P. w \<in> Rep_preal(X)} < UNIV"
paulson@14335
  1021
apply (drule preal_sup_not_mem_Ex)
paulson@14335
  1022
apply (auto intro!: psubsetI)
paulson@14335
  1023
done
paulson@14335
  1024
paulson@14335
  1025
lemma preal_sup_set_not_prat_set1:
paulson@14335
  1026
     "\<exists>Y. (\<forall>X \<in> P. X \<le> Y) ==> {w. \<exists>X \<in> P. w \<in> Rep_preal(X)} < UNIV"
paulson@14335
  1027
apply (drule preal_sup_not_mem_Ex1)
paulson@14335
  1028
apply (auto intro!: psubsetI)
paulson@14335
  1029
done
paulson@14335
  1030
paulson@14335
  1031
text{*Part 3 of Dedekind sections definition*}
paulson@14335
  1032
lemma preal_sup_set_lemma3:
paulson@14335
  1033
     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
paulson@14335
  1034
          ==> \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
paulson@14335
  1035
              \<forall>z. z < y --> z \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}"
paulson@14335
  1036
apply (auto elim: Rep_preal [THEN prealE_lemma3b])
paulson@14335
  1037
done
paulson@14335
  1038
paulson@14335
  1039
lemma preal_sup_set_lemma3_1:
paulson@14335
  1040
     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X \<le> Y) |]
paulson@14335
  1041
          ==> \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
paulson@14335
  1042
              \<forall>z. z < y --> z \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}"
paulson@14335
  1043
apply (auto elim: Rep_preal [THEN prealE_lemma3b])
paulson@14335
  1044
done
paulson@14335
  1045
paulson@14335
  1046
lemma preal_sup_set_lemma4:
paulson@14335
  1047
     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
paulson@14335
  1048
          ==>  \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
paulson@14335
  1049
              Bex {w. \<exists>X \<in> P. w \<in> Rep_preal X} (op < y)"
paulson@14335
  1050
apply (blast dest: Rep_preal [THEN prealE_lemma4a])
paulson@14335
  1051
done
paulson@14335
  1052
paulson@14335
  1053
lemma preal_sup_set_lemma4_1:
paulson@14335
  1054
     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X \<le> Y) |]
paulson@14335
  1055
          ==>  \<forall>y \<in> {w. \<exists>X \<in> P. w \<in> Rep_preal X}.
paulson@14335
  1056
              Bex {w. \<exists>X \<in> P. w \<in> Rep_preal X} (op < y)"
paulson@14335
  1057
apply (blast dest: Rep_preal [THEN prealE_lemma4a])
paulson@14335
  1058
done
paulson@14335
  1059
paulson@14335
  1060
lemma preal_sup:
paulson@14335
  1061
     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
paulson@14335
  1062
          ==> {w. \<exists>X \<in> P. w \<in> Rep_preal(X)}: preal"
paulson@14335
  1063
apply (rule prealI2)
paulson@14335
  1064
apply (rule preal_sup_set_not_empty)
paulson@14335
  1065
apply (rule_tac [2] preal_sup_set_not_prat_set)
paulson@14335
  1066
apply (rule_tac [3] preal_sup_set_lemma3)
paulson@14335
  1067
apply (rule_tac [5] preal_sup_set_lemma4, auto)
paulson@14335
  1068
done
paulson@14335
  1069
paulson@14335
  1070
lemma preal_sup1:
paulson@14335
  1071
     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X \<le> Y) |]
paulson@14335
  1072
          ==> {w. \<exists>X \<in> P. w \<in> Rep_preal(X)}: preal"
paulson@14335
  1073
apply (rule prealI2)
paulson@14335
  1074
apply (rule preal_sup_set_not_empty)
paulson@14335
  1075
apply (rule_tac [2] preal_sup_set_not_prat_set1)
paulson@14335
  1076
apply (rule_tac [3] preal_sup_set_lemma3_1)
paulson@14335
  1077
apply (rule_tac [5] preal_sup_set_lemma4_1, auto)
paulson@14335
  1078
done
paulson@14335
  1079
paulson@14335
  1080
lemma preal_psup_leI: "\<exists>Y. (\<forall>X \<in> P. X < Y) ==> \<forall>x \<in> P. x \<le> psup P"
paulson@14335
  1081
apply (unfold psup_def)
paulson@14335
  1082
apply (auto simp add: preal_le_def)
paulson@14335
  1083
apply (rule preal_sup [THEN Abs_preal_inverse, THEN ssubst], auto)
paulson@14335
  1084
done
paulson@14335
  1085
paulson@14335
  1086
lemma preal_psup_leI2: "\<exists>Y. (\<forall>X \<in> P. X \<le> Y) ==> \<forall>x \<in> P. x \<le> psup P"
paulson@14335
  1087
apply (unfold psup_def)
paulson@14335
  1088
apply (auto simp add: preal_le_def)
paulson@14335
  1089
apply (rule preal_sup1 [THEN Abs_preal_inverse, THEN ssubst])
paulson@14335
  1090
apply (auto simp add: preal_le_def)
paulson@14335
  1091
done
paulson@14335
  1092
paulson@14335
  1093
lemma preal_psup_leI2b:
paulson@14335
  1094
     "[| \<exists>Y. (\<forall>X \<in> P. X < Y); x \<in> P |] ==> x \<le> psup P"
paulson@14335
  1095
apply (blast dest!: preal_psup_leI)
paulson@14335
  1096
done
paulson@14335
  1097
paulson@14335
  1098
lemma preal_psup_leI2a:
paulson@14335
  1099
     "[| \<exists>Y. (\<forall>X \<in> P. X \<le> Y); x \<in> P |] ==> x \<le> psup P"
paulson@14335
  1100
apply (blast dest!: preal_psup_leI2)
paulson@14335
  1101
done
paulson@14335
  1102
paulson@14335
  1103
lemma psup_le_ub: "[| \<exists>X. X \<in> P; \<forall>X \<in> P. X < Y |] ==> psup P \<le> Y"
paulson@14335
  1104
apply (unfold psup_def)
paulson@14335
  1105
apply (auto simp add: preal_le_def)
paulson@14335
  1106
apply (drule preal_sup [OF exI exI, THEN Abs_preal_inverse, THEN subst])
paulson@14335
  1107
apply (rotate_tac [2] 1)
paulson@14335
  1108
prefer 2 apply assumption
paulson@14335
  1109
apply (auto dest!: bspec simp add: preal_less_def psubset_def)
paulson@14335
  1110
done
paulson@14335
  1111
paulson@14335
  1112
lemma psup_le_ub1: "[| \<exists>X. X \<in> P; \<forall>X \<in> P. X \<le> Y |] ==> psup P \<le> Y"
paulson@14335
  1113
apply (unfold psup_def)
paulson@14335
  1114
apply (auto simp add: preal_le_def)
paulson@14335
  1115
apply (drule preal_sup1 [OF exI exI, THEN Abs_preal_inverse, THEN subst])
paulson@14335
  1116
apply (rotate_tac [2] 1)
paulson@14335
  1117
prefer 2 apply assumption
paulson@14335
  1118
apply (auto dest!: bspec simp add: preal_less_def psubset_def preal_le_def)
paulson@14335
  1119
done
paulson@14335
  1120
paulson@14335
  1121
text{*Supremum property*}
paulson@14335
  1122
lemma preal_complete:
paulson@14335
  1123
     "[|\<exists>(X::preal). X \<in> P; \<exists>Y. (\<forall>X \<in> P. X < Y) |]
paulson@14335
  1124
          ==> (\<forall>Y. (\<exists>X \<in> P. Y < X) = (Y < psup P))"
paulson@14335
  1125
apply (frule preal_sup [THEN Abs_preal_inverse], fast)
paulson@14335
  1126
apply (auto simp add: psup_def preal_less_def)
paulson@14335
  1127
apply (cut_tac x = Xa and y = Ya in preal_linear)
paulson@14335
  1128
apply (auto dest: psubsetD simp add: preal_less_def)
paulson@14335
  1129
done
paulson@14335
  1130
paulson@14335
  1131
paulson@14335
  1132
subsection{*The Embadding from @{typ prat} into @{typ preal}*}
paulson@14335
  1133
paulson@14335
  1134
lemma lemma_preal_rat_less: "x < z1 + z2 ==> x * z1 * qinv (z1 + z2) < z1"
paulson@14335
  1135
apply (drule_tac x = "z1 * qinv (z1 + z2) " in prat_mult_less2_mono1)
paulson@14335
  1136
apply (simp add: prat_mult_ac)
paulson@14335
  1137
done
paulson@14335
  1138
paulson@14335
  1139
lemma lemma_preal_rat_less2: "x < z1 + z2 ==> x * z2 * qinv (z1 + z2) < z2"
paulson@14335
  1140
apply (subst prat_add_commute)
paulson@14335
  1141
apply (drule prat_add_commute [THEN subst])
paulson@14335
  1142
apply (erule lemma_preal_rat_less)
paulson@14335
  1143
done
paulson@14335
  1144
paulson@14335
  1145
lemma preal_of_prat_add:
paulson@14335
  1146
      "preal_of_prat ((z1::prat) + z2) =
paulson@14335
  1147
       preal_of_prat z1 + preal_of_prat z2"
paulson@14335
  1148
apply (unfold preal_of_prat_def preal_add_def)
paulson@14335
  1149
apply (rule_tac f = Abs_preal in arg_cong)
paulson@14335
  1150
apply (auto intro: prat_add_less_mono 
paulson@14335
  1151
            simp add: lemma_prat_less_set_mem_preal [THEN Abs_preal_inverse])
paulson@14335
  1152
apply (rule_tac x = "x*z1*qinv (z1+z2) " in exI, rule conjI)
paulson@14335
  1153
apply (erule lemma_preal_rat_less)
paulson@14335
  1154
apply (rule_tac x = "x*z2*qinv (z1+z2) " in exI, rule conjI)
paulson@14335
  1155
apply (erule lemma_preal_rat_less2)
paulson@14335
  1156
apply (simp add: prat_add_mult_distrib [symmetric] 
paulson@14335
  1157
                 prat_add_mult_distrib2 [symmetric] prat_mult_ac)
paulson@14335
  1158
done
paulson@14335
  1159
paulson@14335
  1160
lemma lemma_preal_rat_less3: "x < xa ==> x*z1*qinv(xa) < z1"
paulson@14335
  1161
apply (drule_tac x = "z1 * qinv xa" in prat_mult_less2_mono1)
paulson@14335
  1162
apply (drule prat_mult_left_commute [THEN subst])
paulson@14335
  1163
apply (simp add: prat_mult_ac)
paulson@14335
  1164
done
paulson@14335
  1165
paulson@14335
  1166
lemma lemma_preal_rat_less4: "xa < z1 * z2 ==> xa*z2*qinv(z1*z2) < z2"
paulson@14335
  1167
apply (drule_tac x = "z2 * qinv (z1*z2) " in prat_mult_less2_mono1)
paulson@14335
  1168
apply (drule prat_mult_left_commute [THEN subst])
paulson@14335
  1169
apply (simp add: prat_mult_ac)
paulson@14335
  1170
done
paulson@14335
  1171
paulson@14335
  1172
lemma preal_of_prat_mult:
paulson@14335
  1173
      "preal_of_prat ((z1::prat) * z2) =
paulson@14335
  1174
       preal_of_prat z1 * preal_of_prat z2"
paulson@14335
  1175
apply (unfold preal_of_prat_def preal_mult_def)
paulson@14335
  1176
apply (rule_tac f = Abs_preal in arg_cong)
paulson@14335
  1177
apply (auto intro: prat_mult_less_mono 
paulson@14335
  1178
            simp add: lemma_prat_less_set_mem_preal [THEN Abs_preal_inverse])
paulson@14335
  1179
apply (drule prat_dense, safe)
paulson@14335
  1180
apply (rule_tac x = "x*z1*qinv (xa) " in exI, rule conjI)
paulson@14335
  1181
apply (erule lemma_preal_rat_less3)
paulson@14335
  1182
apply (rule_tac x = " xa*z2*qinv (z1*z2) " in exI, rule conjI)
paulson@14335
  1183
apply (erule lemma_preal_rat_less4)
paulson@14335
  1184
apply (simp add: qinv_mult_eq [symmetric] prat_mult_ac)
paulson@14335
  1185
apply (simp add: prat_mult_assoc [symmetric])
paulson@14335
  1186
done
paulson@14335
  1187
paulson@14335
  1188
lemma preal_of_prat_less_iff [simp]:
paulson@14335
  1189
      "(preal_of_prat p < preal_of_prat q) = (p < q)"
paulson@14335
  1190
apply (unfold preal_of_prat_def preal_less_def)
paulson@14335
  1191
apply (auto dest!: lemma_prat_set_eq elim: prat_less_trans 
paulson@14335
  1192
        simp add: lemma_prat_less_set_mem_preal psubset_def prat_less_not_refl)
paulson@14335
  1193
apply (rule_tac x = p and y = q in prat_linear_less2)
paulson@14335
  1194
apply (auto intro: prat_less_irrefl)
paulson@14335
  1195
done
paulson@14335
  1196
paulson@14335
  1197
paulson@14335
  1198
ML
paulson@14335
  1199
{*
paulson@14335
  1200
val inj_on_Abs_preal = thm"inj_on_Abs_preal";
paulson@14335
  1201
val inj_Rep_preal = thm"inj_Rep_preal";
paulson@14335
  1202
val empty_not_mem_preal = thm"empty_not_mem_preal";
paulson@14335
  1203
val one_set_mem_preal = thm"one_set_mem_preal";
paulson@14335
  1204
val preal_psubset_empty = thm"preal_psubset_empty";
paulson@14335
  1205
val mem_Rep_preal_Ex = thm"mem_Rep_preal_Ex";
paulson@14335
  1206
val inj_preal_of_prat = thm"inj_preal_of_prat";
paulson@14335
  1207
val not_in_preal_ub = thm"not_in_preal_ub";
paulson@14335
  1208
val preal_less_not_refl = thm"preal_less_not_refl";
paulson@14335
  1209
val preal_less_trans = thm"preal_less_trans";
paulson@14335
  1210
val preal_less_not_sym = thm"preal_less_not_sym";
paulson@14335
  1211
val preal_linear = thm"preal_linear";
paulson@14335
  1212
val preal_add_commute = thm"preal_add_commute";
paulson@14335
  1213
val preal_add_set_not_empty = thm"preal_add_set_not_empty";
paulson@14335
  1214
val preal_not_mem_add_set_Ex = thm"preal_not_mem_add_set_Ex";
paulson@14335
  1215
val preal_add_set_not_prat_set = thm"preal_add_set_not_prat_set";
paulson@14335
  1216
val preal_mem_add_set = thm"preal_mem_add_set";
paulson@14335
  1217
val preal_add_assoc = thm"preal_add_assoc";
paulson@14335
  1218
val preal_add_left_commute = thm"preal_add_left_commute";
paulson@14335
  1219
val preal_mult_commute = thm"preal_mult_commute";
paulson@14335
  1220
val preal_mult_set_not_empty = thm"preal_mult_set_not_empty";
paulson@14335
  1221
val preal_not_mem_mult_set_Ex = thm"preal_not_mem_mult_set_Ex";
paulson@14335
  1222
val preal_mult_set_not_prat_set = thm"preal_mult_set_not_prat_set";
paulson@14335
  1223
val preal_mem_mult_set = thm"preal_mem_mult_set";
paulson@14335
  1224
val preal_mult_assoc = thm"preal_mult_assoc";
paulson@14335
  1225
val preal_mult_left_commute = thm"preal_mult_left_commute";
paulson@14335
  1226
val preal_mult_1 = thm"preal_mult_1";
paulson@14335
  1227
val preal_mult_1_right = thm"preal_mult_1_right";
paulson@14335
  1228
val mem_Rep_preal_addD = thm"mem_Rep_preal_addD";
paulson@14335
  1229
val mem_Rep_preal_addI = thm"mem_Rep_preal_addI";
paulson@14335
  1230
val mem_Rep_preal_add_iff = thm"mem_Rep_preal_add_iff";
paulson@14335
  1231
val mem_Rep_preal_multD = thm"mem_Rep_preal_multD";
paulson@14335
  1232
val mem_Rep_preal_multI = thm"mem_Rep_preal_multI";
paulson@14335
  1233
val mem_Rep_preal_mult_iff = thm"mem_Rep_preal_mult_iff";
paulson@14335
  1234
val preal_add_mult_distrib2 = thm"preal_add_mult_distrib2";
paulson@14335
  1235
val preal_add_mult_distrib = thm"preal_add_mult_distrib";
paulson@14335
  1236
val qinv_not_mem_Rep_preal_Ex = thm"qinv_not_mem_Rep_preal_Ex";
paulson@14335
  1237
val preal_inv_set_not_empty = thm"preal_inv_set_not_empty";
paulson@14335
  1238
val qinv_mem_Rep_preal_Ex = thm"qinv_mem_Rep_preal_Ex";
paulson@14335
  1239
val preal_not_mem_inv_set_Ex = thm"preal_not_mem_inv_set_Ex";
paulson@14335
  1240
val preal_inv_set_not_prat_set = thm"preal_inv_set_not_prat_set";
paulson@14335
  1241
val preal_mem_inv_set = thm"preal_mem_inv_set";
paulson@14335
  1242
val preal_mem_mult_invD = thm"preal_mem_mult_invD";
paulson@14335
  1243
val preal_mem_mult_invI = thm"preal_mem_mult_invI";
paulson@14335
  1244
val preal_mult_inv = thm"preal_mult_inv";
paulson@14335
  1245
val preal_mult_inv_right = thm"preal_mult_inv_right";
paulson@14335
  1246
val Rep_preal_self_subset = thm"Rep_preal_self_subset";
paulson@14335
  1247
val Rep_preal_sum_not_subset = thm"Rep_preal_sum_not_subset";
paulson@14335
  1248
val Rep_preal_sum_not_eq = thm"Rep_preal_sum_not_eq";
paulson@14335
  1249
val preal_self_less_add_left = thm"preal_self_less_add_left";
paulson@14335
  1250
val preal_self_less_add_right = thm"preal_self_less_add_right";
paulson@14335
  1251
val preal_less_le_iff = thm"preal_less_le_iff";
paulson@14335
  1252
val preal_le_refl = thm"preal_le_refl";
paulson@14335
  1253
val preal_le_trans = thm"preal_le_trans";
paulson@14335
  1254
val preal_le_anti_sym = thm"preal_le_anti_sym";
paulson@14335
  1255
val preal_neq_iff = thm"preal_neq_iff";
paulson@14335
  1256
val preal_less_le = thm"preal_less_le";
paulson@14335
  1257
val psubset_trans = thm"psubset_trans";
paulson@14335
  1258
val preal_less_set_not_empty = thm"preal_less_set_not_empty";
paulson@14335
  1259
val preal_less_set_not_prat_set = thm"preal_less_set_not_prat_set";
paulson@14335
  1260
val preal_mem_less_set = thm"preal_mem_less_set";
paulson@14335
  1261
val preal_less_add_left_subsetI = thm"preal_less_add_left_subsetI";
paulson@14335
  1262
val preal_less_add_left_subsetI2 = thm"preal_less_add_left_subsetI2";
paulson@14335
  1263
val preal_less_add_left = thm"preal_less_add_left";
paulson@14335
  1264
val preal_less_add_left_Ex = thm"preal_less_add_left_Ex";
paulson@14335
  1265
val preal_add_less2_mono1 = thm"preal_add_less2_mono1";
paulson@14335
  1266
val preal_add_less2_mono2 = thm"preal_add_less2_mono2";
paulson@14335
  1267
val preal_mult_less_mono1 = thm"preal_mult_less_mono1";
paulson@14335
  1268
val preal_mult_left_less_mono1 = thm"preal_mult_left_less_mono1";
paulson@14335
  1269
val preal_mult_left_le_mono1 = thm"preal_mult_left_le_mono1";
paulson@14335
  1270
val preal_mult_le_mono1 = thm"preal_mult_le_mono1";
paulson@14335
  1271
val preal_add_left_le_mono1 = thm"preal_add_left_le_mono1";
paulson@14335
  1272
val preal_add_le_mono1 = thm"preal_add_le_mono1";
paulson@14335
  1273
val preal_add_right_less_cancel = thm"preal_add_right_less_cancel";
paulson@14335
  1274
val preal_add_left_less_cancel = thm"preal_add_left_less_cancel";
paulson@14335
  1275
val preal_add_less_iff1 = thm"preal_add_less_iff1";
paulson@14335
  1276
val preal_add_less_iff2 = thm"preal_add_less_iff2";
paulson@14335
  1277
val preal_add_less_mono = thm"preal_add_less_mono";
paulson@14335
  1278
val preal_mult_less_mono = thm"preal_mult_less_mono";
paulson@14335
  1279
val preal_add_right_cancel = thm"preal_add_right_cancel";
paulson@14335
  1280
val preal_add_left_cancel = thm"preal_add_left_cancel";
paulson@14335
  1281
val preal_add_left_cancel_iff = thm"preal_add_left_cancel_iff";
paulson@14335
  1282
val preal_add_right_cancel_iff = thm"preal_add_right_cancel_iff";
paulson@14335
  1283
val preal_sup_mem_Ex = thm"preal_sup_mem_Ex";
paulson@14335
  1284
val preal_sup_set_not_empty = thm"preal_sup_set_not_empty";
paulson@14335
  1285
val preal_sup_not_mem_Ex = thm"preal_sup_not_mem_Ex";
paulson@14335
  1286
val preal_sup_not_mem_Ex1 = thm"preal_sup_not_mem_Ex1";
paulson@14335
  1287
val preal_sup_set_not_prat_set = thm"preal_sup_set_not_prat_set";
paulson@14335
  1288
val preal_sup_set_not_prat_set1 = thm"preal_sup_set_not_prat_set1";
paulson@14335
  1289
val preal_sup = thm"preal_sup";
paulson@14335
  1290
val preal_sup1 = thm"preal_sup1";
paulson@14335
  1291
val preal_psup_leI = thm"preal_psup_leI";
paulson@14335
  1292
val preal_psup_leI2 = thm"preal_psup_leI2";
paulson@14335
  1293
val preal_psup_leI2b = thm"preal_psup_leI2b";
paulson@14335
  1294
val preal_psup_leI2a = thm"preal_psup_leI2a";
paulson@14335
  1295
val psup_le_ub = thm"psup_le_ub";
paulson@14335
  1296
val psup_le_ub1 = thm"psup_le_ub1";
paulson@14335
  1297
val preal_complete = thm"preal_complete";
paulson@14335
  1298
val preal_of_prat_add = thm"preal_of_prat_add";
paulson@14335
  1299
val preal_of_prat_mult = thm"preal_of_prat_mult";
paulson@14335
  1300
paulson@14335
  1301
val preal_add_ac = thms"preal_add_ac";
paulson@14335
  1302
val preal_mult_ac = thms"preal_mult_ac";
paulson@14335
  1303
*}
paulson@14335
  1304
paulson@5078
  1305
end