113 by (blast_tac (claset() addIs [set_ext] addEs [swap]) 1); |
113 by (blast_tac (claset() addIs [set_ext] addEs [swap]) 1); |
114 qed "not_mem_Rep_preal_Ex"; |
114 qed "not_mem_Rep_preal_Ex"; |
115 |
115 |
116 (** preal_of_prat: the injection from prat to preal **) |
116 (** preal_of_prat: the injection from prat to preal **) |
117 (** A few lemmas **) |
117 (** A few lemmas **) |
118 Goal "{} < {xa::prat. xa < y}"; |
|
119 by (cut_facts_tac [qless_Ex] 1); |
|
120 by (auto_tac (claset() addEs [equalityCE], |
|
121 simpset() addsimps [psubset_def])); |
|
122 qed "lemma_prat_less_set_Ex"; |
|
123 |
118 |
124 Goal "{xa::prat. xa < y} : preal"; |
119 Goal "{xa::prat. xa < y} : preal"; |
125 by (cut_facts_tac [qless_Ex] 1); |
120 by (cut_facts_tac [qless_Ex] 1); |
126 by Safe_tac; |
121 by (auto_tac (claset() addIs[prat_less_trans] |
127 by (rtac lemma_prat_less_set_Ex 1); |
122 addSEs [equalityCE, prat_less_irrefl], |
128 by (auto_tac (claset() addIs [prat_less_trans], |
123 simpset())); |
129 simpset() addsimps [psubset_def])); |
124 by (blast_tac (claset() addDs [prat_dense]) 1); |
130 by (eres_inst_tac [("c","y")] equalityCE 1); |
|
131 by (auto_tac (claset() addDs [prat_less_irrefl],simpset())); |
|
132 by (dres_inst_tac [("q1.0","ya")] prat_dense 1); |
|
133 by (Fast_tac 1); |
|
134 qed "lemma_prat_less_set_mem_preal"; |
125 qed "lemma_prat_less_set_mem_preal"; |
135 |
126 |
136 Goal "!!(x::prat). {xa. xa < x} = {x. x < y} ==> x = y"; |
127 Goal "!!(x::prat). {xa. xa < x} = {x. x < y} ==> x = y"; |
137 by (cut_inst_tac [("q1.0","x"),("q2.0","y")] prat_linear 1); |
128 by (cut_inst_tac [("q1.0","x"),("q2.0","y")] prat_linear 1); |
138 by Auto_tac; |
129 by Auto_tac; |
|
130 by (dtac prat_dense 2 THEN etac exE 2); |
139 by (dtac prat_dense 1 THEN etac exE 1); |
131 by (dtac prat_dense 1 THEN etac exE 1); |
140 by (eres_inst_tac [("c","xa")] equalityCE 1); |
132 by (auto_tac (claset() addDs [prat_less_not_sym] addSEs [equalityCE], |
141 by (auto_tac (claset() addDs [prat_less_not_sym],simpset())); |
133 simpset())); |
142 by (dtac prat_dense 1 THEN etac exE 1); |
|
143 by (eres_inst_tac [("c","xa")] equalityCE 1); |
|
144 by (auto_tac (claset() addDs [prat_less_not_sym],simpset())); |
|
145 qed "lemma_prat_set_eq"; |
134 qed "lemma_prat_set_eq"; |
146 |
135 |
147 Goal "inj(preal_of_prat)"; |
136 Goal "inj(preal_of_prat)"; |
148 by (rtac injI 1); |
137 by (rtac injI 1); |
149 by (rewtac preal_of_prat_def); |
138 by (rewtac preal_of_prat_def); |