1101 by (etac exE 1); |
1101 by (etac exE 1); |
1102 by (res_inst_tac [("x","x")] exI 1); |
1102 by (res_inst_tac [("x","x")] exI 1); |
1103 by (auto_tac (claset() addSDs [bspec],simpset())); |
1103 by (auto_tac (claset() addSDs [bspec],simpset())); |
1104 qed "preal_sup_not_mem_Ex1"; |
1104 qed "preal_sup_not_mem_Ex1"; |
1105 |
1105 |
1106 Goal "EX Y. (ALL X: P. X < Y) \ |
1106 Goal "EX Y. (ALL X: P. X < Y) ==> {w. EX X: P. w: Rep_preal(X)} < UNIV"; (**) |
1107 \ ==> {w. EX X: P. w: Rep_preal(X)} < UNIV"; (**) |
|
1108 by (dtac preal_sup_not_mem_Ex 1); |
1107 by (dtac preal_sup_not_mem_Ex 1); |
1109 by (auto_tac (claset() addSIs [psubsetI],simpset())); |
1108 by (auto_tac (claset() addSIs [psubsetI],simpset())); |
1110 by (eres_inst_tac [("c","q")] equalityCE 1); |
|
1111 by Auto_tac; |
|
1112 qed "preal_sup_set_not_prat_set"; |
1109 qed "preal_sup_set_not_prat_set"; |
1113 |
1110 |
1114 Goal "EX Y. (ALL X: P. X <= Y) \ |
1111 Goal "EX Y. (ALL X: P. X <= Y) ==> {w. EX X: P. w: Rep_preal(X)} < UNIV"; |
1115 \ ==> {w. EX X: P. w: Rep_preal(X)} < UNIV"; |
|
1116 by (dtac preal_sup_not_mem_Ex1 1); |
1112 by (dtac preal_sup_not_mem_Ex1 1); |
1117 by (auto_tac (claset() addSIs [psubsetI],simpset())); |
1113 by (auto_tac (claset() addSIs [psubsetI],simpset())); |
1118 by (eres_inst_tac [("c","q")] equalityCE 1); |
|
1119 by Auto_tac; |
|
1120 qed "preal_sup_set_not_prat_set1"; |
1114 qed "preal_sup_set_not_prat_set1"; |
1121 |
1115 |
1122 (** Part 3 of Dedekind sections def **) |
1116 (** Part 3 of Dedekind sections def **) |
1123 Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \ |
1117 Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \ |
1124 \ ==> ALL y: {w. EX X: P. w: Rep_preal X}. \ |
1118 \ ==> ALL y: {w. EX X: P. w: Rep_preal X}. \ |
1125 \ ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}"; (**) |
1119 \ ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}"; (**) |
1126 by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset())); |
1120 by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b], simpset())); |
1127 qed "preal_sup_set_lemma3"; |
1121 qed "preal_sup_set_lemma3"; |
1128 |
1122 |
1129 Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \ |
1123 Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \ |
1130 \ ==> ALL y: {w. EX X: P. w: Rep_preal X}. \ |
1124 \ ==> ALL y: {w. EX X: P. w: Rep_preal X}. \ |
1131 \ ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}"; |
1125 \ ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}"; |