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