author | paulson |
Wed, 14 Jun 2000 17:47:18 +0200 | |
changeset 9065 | 15f82c9aa331 |
parent 9043 | ca761fe227d8 |
child 9428 | c8eb573114de |
permissions | -rw-r--r-- |
5078 | 1 |
(* Title : RComplete.thy |
7219 | 2 |
ID : $Id$ |
5078 | 3 |
Author : Jacques D. Fleuriot |
4 |
Copyright : 1998 University of Cambridge |
|
5 |
Description : Completeness theorems for positive |
|
6 |
reals and reals |
|
7 |
*) |
|
8 |
||
5521 | 9 |
claset_ref() := claset() delWrapper "bspec"; |
10 |
||
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
11 |
(*--------------------------------------------------------- |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
12 |
Completeness of reals: use supremum property of |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
13 |
preal and theorems about real_preal. Theorems |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
14 |
previously in Real.ML. |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
15 |
---------------------------------------------------------*) |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
16 |
(*a few lemmas*) |
9043
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
17 |
Goal "ALL x:P. #0 < x ==> \ |
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
18 |
\ ((EX x:P. y < x) = (EX X. real_of_preal X : P & \ |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
19 |
\ y < real_of_preal X))"; |
9065 | 20 |
by (blast_tac (claset() addSDs [bspec, |
21 |
rename_numerals thy real_gt_zero_preal_Ex RS iffD1]) 1); |
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
22 |
qed "real_sup_lemma1"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
23 |
|
9043
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
24 |
Goal "[| ALL x:P. #0 < x; EX x. x: P; EX y. ALL x: P. x < y |] \ |
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
25 |
\ ==> (EX X. X: {w. real_of_preal w : P}) & \ |
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
26 |
\ (EX Y. ALL X: {w. real_of_preal w : P}. X < Y)"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
27 |
by (rtac conjI 1); |
9065 | 28 |
by (blast_tac (claset() addDs [bspec, |
29 |
rename_numerals thy real_gt_zero_preal_Ex RS iffD1]) 1); |
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
30 |
by Auto_tac; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
31 |
by (dtac bspec 1 THEN assume_tac 1); |
7499 | 32 |
by (ftac bspec 1 THEN assume_tac 1); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
33 |
by (dtac real_less_trans 1 THEN assume_tac 1); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
34 |
by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1 |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
35 |
THEN etac exE 1); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
36 |
by (res_inst_tac [("x","ya")] exI 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
37 |
by Auto_tac; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
38 |
by (dres_inst_tac [("x","real_of_preal X")] bspec 1 THEN assume_tac 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
39 |
by (etac real_of_preal_lessD 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
40 |
qed "real_sup_lemma2"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
41 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
42 |
(*------------------------------------------------------------- |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
43 |
Completeness of Positive Reals |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
44 |
-------------------------------------------------------------*) |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
45 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
46 |
(** |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
47 |
Supremum property for the set of positive reals |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
48 |
FIXME: long proof - should be improved - need |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
49 |
only have one case split |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
50 |
**) |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
51 |
|
9043
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
52 |
Goal "[| ALL x:P. (#0::real) < x; EX x. x: P; EX y. ALL x: P. x < y |] \ |
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
53 |
\ ==> (EX S. ALL y. (EX x: P. y < x) = (y < S))"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
54 |
by (res_inst_tac |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
55 |
[("x","real_of_preal (psup({w. real_of_preal w : P}))")] exI 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
56 |
by Auto_tac; |
7499 | 57 |
by (ftac real_sup_lemma2 1 THEN Auto_tac); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
58 |
by (case_tac "#0 < ya" 1); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
59 |
by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1); |
9065 | 60 |
by (dtac (rename_numerals thy real_less_all_real2) 2); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
61 |
by Auto_tac; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
62 |
by (rtac (preal_complete RS spec RS iffD1) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
63 |
by Auto_tac; |
7499 | 64 |
by (ftac real_gt_preal_preal_Ex 1); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
65 |
by Auto_tac; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
66 |
(* second part *) |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
67 |
by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
68 |
by (case_tac "#0 < ya" 1); |
9065 | 69 |
by (auto_tac (claset() addSDs (map (rename_numerals thy) |
70 |
[real_less_all_real2, |
|
71 |
real_gt_zero_preal_Ex RS iffD1]), |
|
72 |
simpset())); |
|
7499 | 73 |
by (ftac real_sup_lemma2 2 THEN Auto_tac); |
74 |
by (ftac real_sup_lemma2 1 THEN Auto_tac); |
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
75 |
by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1); |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
76 |
by (Blast_tac 3); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
77 |
by (ALLGOALS(Blast_tac)); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
78 |
qed "posreal_complete"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
79 |
|
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
80 |
(*-------------------------------------------------------- |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
81 |
Completeness properties using isUb, isLub etc. |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
82 |
-------------------------------------------------------*) |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
83 |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
84 |
Goal "[| isLub R S x; isLub R S y |] ==> x = (y::real)"; |
7499 | 85 |
by (ftac isLub_isUb 1); |
5078 | 86 |
by (forw_inst_tac [("x","y")] isLub_isUb 1); |
87 |
by (blast_tac (claset() addSIs [real_le_anti_sym] |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
88 |
addSDs [isLub_le_isUb]) 1); |
5078 | 89 |
qed "real_isLub_unique"; |
90 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
91 |
Goalw [setle_def,setge_def] "[| (x::real) <=* S'; S <= S' |] ==> x <=* S"; |
5078 | 92 |
by (Blast_tac 1); |
93 |
qed "real_order_restrict"; |
|
94 |
||
95 |
(*---------------------------------------------------------------- |
|
96 |
Completeness theorem for the positive reals(again) |
|
97 |
----------------------------------------------------------------*) |
|
98 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
99 |
Goal "[| ALL x: S. #0 < x; \ |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
100 |
\ EX x. x: S; \ |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
101 |
\ EX u. isUb (UNIV::real set) S u \ |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
102 |
\ |] ==> EX t. isLub (UNIV::real set) S t"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
103 |
by (res_inst_tac |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
104 |
[("x","real_of_preal(psup({w. real_of_preal w : S}))")] exI 1); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
105 |
by (auto_tac (claset(), simpset() addsimps |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
106 |
[isLub_def,leastP_def,isUb_def])); |
5078 | 107 |
by (auto_tac (claset() addSIs [setleI,setgeI] |
9065 | 108 |
addSDs [(rename_numerals thy real_gt_zero_preal_Ex) RS iffD1], |
109 |
simpset())); |
|
5078 | 110 |
by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
111 |
by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
112 |
by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff])); |
5078 | 113 |
by (rtac preal_psup_leI2a 1); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
114 |
by (forw_inst_tac [("y","real_of_preal ya")] setleD 1 THEN assume_tac 1); |
7499 | 115 |
by (ftac real_ge_preal_preal_Ex 1); |
5078 | 116 |
by (Step_tac 1); |
117 |
by (res_inst_tac [("x","y")] exI 1); |
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
118 |
by (blast_tac (claset() addSDs [setleD] addIs [real_of_preal_le_iff RS iffD1]) 1); |
5078 | 119 |
by (forw_inst_tac [("x","x")] bspec 1 THEN assume_tac 1); |
7499 | 120 |
by (ftac isUbD2 1); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
121 |
by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1); |
5588 | 122 |
by (auto_tac (claset() addSDs [isUbD, real_ge_preal_preal_Ex], |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
123 |
simpset() addsimps [real_of_preal_le_iff])); |
5588 | 124 |
by (blast_tac (claset() addSDs [setleD] addSIs [psup_le_ub1] |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
125 |
addIs [real_of_preal_le_iff RS iffD1]) 1); |
5078 | 126 |
qed "posreals_complete"; |
127 |
||
128 |
||
129 |
(*------------------------------- |
|
130 |
Lemmas |
|
131 |
-------------------------------*) |
|
9043
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
132 |
Goal "ALL y : {z. EX x: P. z = x + (-xa) + #1} Int {x. #0 < x}. #0 < y"; |
5078 | 133 |
by Auto_tac; |
134 |
qed "real_sup_lemma3"; |
|
135 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
136 |
Goal "(xa <= S + X + (-Z)) = (xa + (-X) + Z <= (S::real))"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
137 |
by (Auto_tac); |
5078 | 138 |
qed "lemma_le_swap2"; |
139 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
140 |
Goal "[| #0 < (x::real) + (-X) + #1; x < xa |] ==> #0 < xa + (-X) + #1"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
141 |
by (Auto_tac); |
5078 | 142 |
qed "lemma_real_complete1"; |
143 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
144 |
Goal "[| (x::real) + (-X) + #1 <= S; xa < x |] ==> xa + (-X) + #1 <= S"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
145 |
by (Auto_tac); |
5078 | 146 |
qed "lemma_real_complete2"; |
147 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
148 |
Goal "[| (x::real) + (-X) + #1 <= S; xa < x |] ==> xa <= S + X + (-#1)"; (**) |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
149 |
by (Auto_tac); |
5078 | 150 |
qed "lemma_real_complete2a"; |
151 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
152 |
Goal "[| (x::real) + (-X) + #1 <= S; xa <= x |] ==> xa <= S + X + (-#1)"; |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
153 |
by (Auto_tac); |
5078 | 154 |
qed "lemma_real_complete2b"; |
155 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
156 |
(*---------------------------------------------------------- |
5078 | 157 |
reals Completeness (again!) |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
158 |
----------------------------------------------------------*) |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
159 |
Goal "[| EX X. X: S; EX Y. isUb (UNIV::real set) S Y |] \ |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
160 |
\ ==> EX t. isLub (UNIV :: real set) S t"; |
5078 | 161 |
by (Step_tac 1); |
9043
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
162 |
by (subgoal_tac "EX u. u: {z. EX x: S. z = x + (-X) + #1} \ |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
163 |
\ Int {x. #0 < x}" 1); |
9043
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
164 |
by (subgoal_tac "isUb (UNIV::real set) ({z. EX x: S. z = x + (-X) + #1} \ |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
165 |
\ Int {x. #0 < x}) (Y + (-X) + #1)" 1); |
5078 | 166 |
by (cut_inst_tac [("P","S"),("xa","X")] real_sup_lemma3 1); |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
167 |
by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac, |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
168 |
Step_tac]); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
169 |
by (res_inst_tac [("x","t + X + (-#1)")] exI 1); |
5078 | 170 |
by (rtac isLubI2 1); |
171 |
by (rtac setgeI 2 THEN Step_tac 2); |
|
9043
ca761fe227d8
First round of changes, towards installation of simprocs
paulson
parents:
9013
diff
changeset
|
172 |
by (subgoal_tac "isUb (UNIV:: real set) ({z. EX x: S. z = x + (-X) + #1} \ |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
173 |
\ Int {x. #0 < x}) (y + (-X) + #1)" 2); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
174 |
by (dres_inst_tac [("y","(y + (- X) + #1)")] isLub_le_isUb 2 |
5078 | 175 |
THEN assume_tac 2); |
5588 | 176 |
by (full_simp_tac |
177 |
(simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @ |
|
178 |
real_add_ac) 2); |
|
5078 | 179 |
by (rtac (setleI RS isUbI) 1); |
180 |
by (Step_tac 1); |
|
181 |
by (res_inst_tac [("R1.0","x"),("R2.0","y")] real_linear_less2 1); |
|
182 |
by (stac lemma_le_swap2 1); |
|
7499 | 183 |
by (ftac isLubD2 1 THEN assume_tac 2); |
5078 | 184 |
by (Step_tac 1); |
185 |
by (Blast_tac 1); |
|
186 |
by (dtac lemma_real_complete1 1 THEN REPEAT(assume_tac 1)); |
|
187 |
by (stac lemma_le_swap2 1); |
|
7499 | 188 |
by (ftac isLubD2 1 THEN assume_tac 2); |
5078 | 189 |
by (Blast_tac 1); |
190 |
by (rtac lemma_real_complete2b 1); |
|
191 |
by (etac real_less_imp_le 2); |
|
192 |
by (blast_tac (claset() addSIs [isLubD2]) 1 THEN Step_tac 1); |
|
5588 | 193 |
by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1); |
194 |
by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI] |
|
195 |
addIs [real_add_le_mono1]) 1); |
|
196 |
by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI] |
|
197 |
addIs [real_add_le_mono1]) 1); |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
198 |
by (Auto_tac); |
5078 | 199 |
qed "reals_complete"; |
200 |
||
201 |
(*---------------------------------------------------------------- |
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
202 |
Related: Archimedean property of reals |
5078 | 203 |
----------------------------------------------------------------*) |
204 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
205 |
Goal "#0 < x ==> EX n. rinv(real_of_posnat n) < x"; |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
206 |
by (stac real_of_posnat_rinv_Ex_iff 1); |
5078 | 207 |
by (EVERY1[rtac ccontr, Asm_full_simp_tac]); |
208 |
by (fold_tac [real_le_def]); |
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
209 |
by (subgoal_tac "isUb (UNIV::real set) \ |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
210 |
\ {z. EX n. z = x*(real_of_posnat n)} #1" 1); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
211 |
by (subgoal_tac "EX X. X : {z. EX n. z = x*(real_of_posnat n)}" 1); |
5078 | 212 |
by (dtac reals_complete 1); |
213 |
by (auto_tac (claset() addIs [isUbI,setleI],simpset())); |
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
214 |
by (subgoal_tac "ALL m. x*(real_of_posnat(Suc m)) <= t" 1); |
5078 | 215 |
by (asm_full_simp_tac (simpset() addsimps |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
216 |
[real_of_posnat_Suc,real_add_mult_distrib2]) 1); |
5078 | 217 |
by (blast_tac (claset() addIs [isLubD2]) 2); |
5588 | 218 |
by (asm_full_simp_tac |
219 |
(simpset() addsimps [real_le_diff_eq RS sym, real_diff_def]) 1); |
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
220 |
by (subgoal_tac "isUb (UNIV::real set) \ |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
221 |
\ {z. EX n. z = x*(real_of_posnat n)} (t + (-x))" 1); |
5078 | 222 |
by (blast_tac (claset() addSIs [isUbI,setleI]) 2); |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
223 |
by (dres_inst_tac [("y","t+(-x)")] isLub_le_isUb 1); |
5588 | 224 |
by (dres_inst_tac [("x","-t")] real_add_left_le_mono1 2); |
5078 | 225 |
by (auto_tac (claset() addDs [real_le_less_trans, |
5588 | 226 |
(real_minus_zero_less_iff2 RS iffD2)], |
227 |
simpset() addsimps [real_less_not_refl,real_add_assoc RS sym])); |
|
5078 | 228 |
qed "reals_Archimedean"; |
229 |
||
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
230 |
Goal "EX n. (x::real) < real_of_posnat n"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
231 |
by (res_inst_tac [("R1.0","x"),("R2.0","#0")] real_linear_less2 1); |
5078 | 232 |
by (res_inst_tac [("x","0")] exI 1); |
233 |
by (res_inst_tac [("x","0")] exI 2); |
|
234 |
by (auto_tac (claset() addEs [real_less_trans], |
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
235 |
simpset() addsimps [real_of_posnat_one,real_zero_less_one])); |
9065 | 236 |
by (ftac ((rename_numerals thy real_rinv_gt_zero) RS reals_Archimedean) 1); |
5078 | 237 |
by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1); |
9065 | 238 |
by (forw_inst_tac [("y","rinv x")] |
239 |
(rename_numerals thy real_mult_less_mono1) 1); |
|
5078 | 240 |
by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym])); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
241 |
by (dres_inst_tac [("n1","n"),("y","#1")] |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
242 |
(real_of_posnat_less_zero RS real_mult_less_mono2) 1); |
5588 | 243 |
by (auto_tac (claset(), |
9065 | 244 |
simpset() addsimps [rename_numerals thy real_of_posnat_less_zero, |
5588 | 245 |
real_not_refl2 RS not_sym, |
246 |
real_mult_assoc RS sym])); |
|
5078 | 247 |
qed "reals_Archimedean2"; |
248 |
||
249 |
||
250 |
||
251 |
||
252 |