author | fleuriot |
Thu, 01 Jun 2000 11:22:27 +0200 | |
changeset 9013 | 9dd0274f76af |
parent 7583 | d1b40e0464b1 |
child 9043 | ca761fe227d8 |
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*) |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
17 |
Goal "! x:P. #0 < x ==> \ |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
18 |
\ ((? x:P. y < x) = (? X. real_of_preal X : P & \ |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
19 |
\ y < real_of_preal X))"; |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
20 |
by (blast_tac (claset() addSDs [bspec,rename_numerals thy |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
21 |
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 |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
24 |
Goal "[| ! x:P. #0 < x; ? x. x: P; ? y. !x: P. x < y |] \ |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
25 |
\ ==> (? X. X: {w. real_of_preal w : P}) & \ |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
26 |
\ (? Y. !X: {w. real_of_preal w : P}. X < Y)"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
27 |
by (rtac conjI 1); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
28 |
by (blast_tac (claset() addDs [bspec, rename_numerals thy |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
29 |
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 |
|
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
52 |
Goal "[| ! x:P. (#0::real) < x; ? x. x: P; ? y. !x: P. x < y |] \ |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
53 |
\ ==> (? S. !y. (? x: P. y < x) = (y < S))"; |
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); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
60 |
by (dtac (full_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); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
69 |
by (auto_tac (claset() addSDs (map (full_rename_numerals |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
70 |
thy) [real_less_all_real2,real_gt_zero_preal_Ex RS iffD1]), |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
71 |
simpset())); |
7499 | 72 |
by (ftac real_sup_lemma2 2 THEN Auto_tac); |
73 |
by (ftac real_sup_lemma2 1 THEN Auto_tac); |
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
74 |
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
|
75 |
by (Blast_tac 3); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
76 |
by (ALLGOALS(Blast_tac)); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
77 |
qed "posreal_complete"; |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
78 |
|
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 |
Completeness properties using isUb, isLub etc. |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
81 |
-------------------------------------------------------*) |
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
82 |
|
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
83 |
Goal "[| isLub R S x; isLub R S y |] ==> x = (y::real)"; |
7499 | 84 |
by (ftac isLub_isUb 1); |
5078 | 85 |
by (forw_inst_tac [("x","y")] isLub_isUb 1); |
86 |
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
|
87 |
addSDs [isLub_le_isUb]) 1); |
5078 | 88 |
qed "real_isLub_unique"; |
89 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
90 |
Goalw [setle_def,setge_def] "[| (x::real) <=* S'; S <= S' |] ==> x <=* S"; |
5078 | 91 |
by (Blast_tac 1); |
92 |
qed "real_order_restrict"; |
|
93 |
||
94 |
(*---------------------------------------------------------------- |
|
95 |
Completeness theorem for the positive reals(again) |
|
96 |
----------------------------------------------------------------*) |
|
97 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
98 |
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
|
99 |
\ EX x. x: S; \ |
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
100 |
\ 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
|
101 |
\ |] ==> 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
|
102 |
by (res_inst_tac |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
103 |
[("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
|
104 |
by (auto_tac (claset(), simpset() addsimps |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
105 |
[isLub_def,leastP_def,isUb_def])); |
5078 | 106 |
by (auto_tac (claset() addSIs [setleI,setgeI] |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
107 |
addSDs [(rename_numerals thy real_gt_zero_preal_Ex) |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
108 |
RS iffD1],simpset())); |
5078 | 109 |
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
|
110 |
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
|
111 |
by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff])); |
5078 | 112 |
by (rtac preal_psup_leI2a 1); |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
113 |
by (forw_inst_tac [("y","real_of_preal ya")] setleD 1 THEN assume_tac 1); |
7499 | 114 |
by (ftac real_ge_preal_preal_Ex 1); |
5078 | 115 |
by (Step_tac 1); |
116 |
by (res_inst_tac [("x","y")] exI 1); |
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
117 |
by (blast_tac (claset() addSDs [setleD] addIs [real_of_preal_le_iff RS iffD1]) 1); |
5078 | 118 |
by (forw_inst_tac [("x","x")] bspec 1 THEN assume_tac 1); |
7499 | 119 |
by (ftac isUbD2 1); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
120 |
by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1); |
5588 | 121 |
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
|
122 |
simpset() addsimps [real_of_preal_le_iff])); |
5588 | 123 |
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
|
124 |
addIs [real_of_preal_le_iff RS iffD1]) 1); |
5078 | 125 |
qed "posreals_complete"; |
126 |
||
127 |
||
128 |
(*------------------------------- |
|
129 |
Lemmas |
|
130 |
-------------------------------*) |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
131 |
Goal "! y : {z. ? x: P. z = x + (-xa) + #1} Int {x. #0 < x}. #0 < y"; |
5078 | 132 |
by Auto_tac; |
133 |
qed "real_sup_lemma3"; |
|
134 |
||
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
135 |
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
|
136 |
by (Auto_tac); |
5078 | 137 |
qed "lemma_le_swap2"; |
138 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
139 |
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
|
140 |
by (Auto_tac); |
5078 | 141 |
qed "lemma_real_complete1"; |
142 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
143 |
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
|
144 |
by (Auto_tac); |
5078 | 145 |
qed "lemma_real_complete2"; |
146 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
147 |
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
|
148 |
by (Auto_tac); |
5078 | 149 |
qed "lemma_real_complete2a"; |
150 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
151 |
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
|
152 |
by (Auto_tac); |
5078 | 153 |
qed "lemma_real_complete2b"; |
154 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
155 |
(*---------------------------------------------------------- |
5078 | 156 |
reals Completeness (again!) |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
157 |
----------------------------------------------------------*) |
7127
48e235179ffb
added parentheses to cope with a possible reduction of the precedence of unary
paulson
parents:
7077
diff
changeset
|
158 |
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
|
159 |
\ ==> EX t. isLub (UNIV :: real set) S t"; |
5078 | 160 |
by (Step_tac 1); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
161 |
by (subgoal_tac "? u. u: {z. ? x: S. z = x + (-X) + #1} \ |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
162 |
\ Int {x. #0 < x}" 1); |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
163 |
by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + (-X) + #1} \ |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
164 |
\ Int {x. #0 < x}) (Y + (-X) + #1)" 1); |
5078 | 165 |
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
|
166 |
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
|
167 |
Step_tac]); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
168 |
by (res_inst_tac [("x","t + X + (-#1)")] exI 1); |
5078 | 169 |
by (rtac isLubI2 1); |
170 |
by (rtac setgeI 2 THEN Step_tac 2); |
|
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
171 |
by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + (-X) + #1} \ |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
172 |
\ 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
|
173 |
by (dres_inst_tac [("y","(y + (- X) + #1)")] isLub_le_isUb 2 |
5078 | 174 |
THEN assume_tac 2); |
5588 | 175 |
by (full_simp_tac |
176 |
(simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @ |
|
177 |
real_add_ac) 2); |
|
5078 | 178 |
by (rtac (setleI RS isUbI) 1); |
179 |
by (Step_tac 1); |
|
180 |
by (res_inst_tac [("R1.0","x"),("R2.0","y")] real_linear_less2 1); |
|
181 |
by (stac lemma_le_swap2 1); |
|
7499 | 182 |
by (ftac isLubD2 1 THEN assume_tac 2); |
5078 | 183 |
by (Step_tac 1); |
184 |
by (Blast_tac 1); |
|
185 |
by (dtac lemma_real_complete1 1 THEN REPEAT(assume_tac 1)); |
|
186 |
by (stac lemma_le_swap2 1); |
|
7499 | 187 |
by (ftac isLubD2 1 THEN assume_tac 2); |
5078 | 188 |
by (Blast_tac 1); |
189 |
by (rtac lemma_real_complete2b 1); |
|
190 |
by (etac real_less_imp_le 2); |
|
191 |
by (blast_tac (claset() addSIs [isLubD2]) 1 THEN Step_tac 1); |
|
5588 | 192 |
by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1); |
193 |
by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI] |
|
194 |
addIs [real_add_le_mono1]) 1); |
|
195 |
by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI] |
|
196 |
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
|
197 |
by (Auto_tac); |
5078 | 198 |
qed "reals_complete"; |
199 |
||
200 |
(*---------------------------------------------------------------- |
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
201 |
Related: Archimedean property of reals |
5078 | 202 |
----------------------------------------------------------------*) |
203 |
||
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
204 |
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
|
205 |
by (stac real_of_posnat_rinv_Ex_iff 1); |
5078 | 206 |
by (EVERY1[rtac ccontr, Asm_full_simp_tac]); |
207 |
by (fold_tac [real_le_def]); |
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
208 |
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
|
209 |
\ {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
|
210 |
by (subgoal_tac "EX X. X : {z. EX n. z = x*(real_of_posnat n)}" 1); |
5078 | 211 |
by (dtac reals_complete 1); |
212 |
by (auto_tac (claset() addIs [isUbI,setleI],simpset())); |
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
213 |
by (subgoal_tac "ALL m. x*(real_of_posnat(Suc m)) <= t" 1); |
5078 | 214 |
by (asm_full_simp_tac (simpset() addsimps |
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
215 |
[real_of_posnat_Suc,real_add_mult_distrib2]) 1); |
5078 | 216 |
by (blast_tac (claset() addIs [isLubD2]) 2); |
5588 | 217 |
by (asm_full_simp_tac |
218 |
(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
|
219 |
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
|
220 |
\ {z. EX n. z = x*(real_of_posnat n)} (t + (-x))" 1); |
5078 | 221 |
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
|
222 |
by (dres_inst_tac [("y","t+(-x)")] isLub_le_isUb 1); |
5588 | 223 |
by (dres_inst_tac [("x","-t")] real_add_left_le_mono1 2); |
5078 | 224 |
by (auto_tac (claset() addDs [real_le_less_trans, |
5588 | 225 |
(real_minus_zero_less_iff2 RS iffD2)], |
226 |
simpset() addsimps [real_less_not_refl,real_add_assoc RS sym])); |
|
5078 | 227 |
qed "reals_Archimedean"; |
228 |
||
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
229 |
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
|
230 |
by (res_inst_tac [("R1.0","x"),("R2.0","#0")] real_linear_less2 1); |
5078 | 231 |
by (res_inst_tac [("x","0")] exI 1); |
232 |
by (res_inst_tac [("x","0")] exI 2); |
|
233 |
by (auto_tac (claset() addEs [real_less_trans], |
|
7077
60b098bb8b8a
heavily revised by Jacques: coercions have alphabetic names;
paulson
parents:
5588
diff
changeset
|
234 |
simpset() addsimps [real_of_posnat_one,real_zero_less_one])); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
235 |
by (forward_tac [((full_rename_numerals thy real_rinv_gt_zero) |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
236 |
RS reals_Archimedean)] 1); |
5078 | 237 |
by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1); |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
238 |
by (forw_inst_tac [("y","rinv x")] |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
239 |
(full_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(), |
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
244 |
simpset() addsimps [rename_numerals thy |
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
7583
diff
changeset
|
245 |
real_of_posnat_less_zero, |
5588 | 246 |
real_not_refl2 RS not_sym, |
247 |
real_mult_assoc RS sym])); |
|
5078 | 248 |
qed "reals_Archimedean2"; |
249 |
||
250 |
||
251 |
||
252 |
||
253 |