140 |
141 |
141 end |
142 end |
142 |
143 |
143 section {* type definition for the quotient type *} |
144 section {* type definition for the quotient type *} |
144 |
145 |
145 ML {* |
146 use "quotient.ML" |
146 (* constructs the term \<lambda>(c::rty \<Rightarrow> bool). \<exists>x. c = rel x *) |
|
147 fun typedef_term rel rty lthy = |
|
148 let |
|
149 val [x, c] = [("x", rty), ("c", rty --> @{typ bool})] |
|
150 |> Variable.variant_frees lthy [rel] |
|
151 |> map Free |
|
152 in |
|
153 lambda c |
|
154 (HOLogic.exists_const rty $ |
|
155 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
|
156 end |
|
157 *} |
|
158 |
|
159 ML {* |
|
160 (* makes the new type definitions and proves non-emptyness*) |
|
161 fun typedef_make (qty_name, mx, rel, rty) lthy = |
|
162 let |
|
163 val typedef_tac = |
|
164 EVERY1 [rewrite_goal_tac @{thms mem_def}, |
|
165 rtac @{thm exI}, |
|
166 rtac @{thm exI}, |
|
167 rtac @{thm refl}] |
|
168 val tfrees = map fst (Term.add_tfreesT rty []) |
|
169 in |
|
170 LocalTheory.theory_result |
|
171 (Typedef.add_typedef false NONE |
|
172 (qty_name, tfrees, mx) |
|
173 (typedef_term rel rty lthy) |
|
174 NONE typedef_tac) lthy |
|
175 end |
|
176 *} |
|
177 |
|
178 ML {* |
|
179 (* tactic to prove the QUOT_TYPE theorem for the new type *) |
|
180 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
|
181 let |
|
182 val unfold_mem = MetaSimplifier.rewrite_rule @{thms mem_def} |
|
183 val rep_thm = #Rep typedef_info |> unfold_mem |
|
184 val rep_inv = #Rep_inverse typedef_info |
|
185 val abs_inv = #Abs_inverse typedef_info |> unfold_mem |
|
186 val rep_inj = #Rep_inject typedef_info |
|
187 in |
|
188 EVERY1 [rtac @{thm QUOT_TYPE.intro}, |
|
189 rtac equiv_thm, |
|
190 rtac rep_thm, |
|
191 rtac rep_inv, |
|
192 rtac abs_inv, |
|
193 rtac @{thm exI}, |
|
194 rtac @{thm refl}, |
|
195 rtac rep_inj] |
|
196 end |
|
197 *} |
|
198 |
|
199 ML {* |
|
200 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = |
|
201 let |
|
202 val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT) |
|
203 val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep) |
|
204 |> Syntax.check_term lthy |
|
205 in |
|
206 Goal.prove lthy [] [] goal |
|
207 (K (typedef_quot_type_tac equiv_thm typedef_info)) |
|
208 end |
|
209 *} |
|
210 |
|
211 ML {* |
|
212 (* proves the quotient theorem *) |
|
213 fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = |
|
214 let |
|
215 val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT) |
|
216 val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |
|
217 |> Syntax.check_term lthy |
|
218 |
|
219 val typedef_quotient_thm_tac = |
|
220 EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]), |
|
221 rtac @{thm QUOT_TYPE.QUOTIENT}, |
|
222 rtac quot_type_thm] |
|
223 in |
|
224 Goal.prove lthy [] [] goal |
|
225 (K typedef_quotient_thm_tac) |
|
226 end |
|
227 *} |
|
228 |
|
229 text {* two wrappers for define and note *} |
|
230 ML {* |
|
231 fun make_def (name, mx, rhs) lthy = |
|
232 let |
|
233 val ((rhs, (_ , thm)), lthy') = |
|
234 LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy |
|
235 in |
|
236 ((rhs, thm), lthy') |
|
237 end |
|
238 *} |
|
239 |
|
240 ML {* |
|
241 fun note_thm (name, thm) lthy = |
|
242 let |
|
243 val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy |
|
244 in |
|
245 (thm', lthy') |
|
246 end |
|
247 *} |
|
248 |
147 |
249 ML {* |
148 ML {* |
250 val no_vars = Thm.rule_attribute (fn context => fn th => |
149 val no_vars = Thm.rule_attribute (fn context => fn th => |
251 let |
150 let |
252 val ctxt = Variable.set_body false (Context.proof_of context); |
151 val ctxt = Variable.set_body false (Context.proof_of context); |
253 val ((_, [th']), _) = Variable.import true [th] ctxt; |
152 val ((_, [th']), _) = Variable.import true [th] ctxt; |
254 in th' end); |
153 in th' end); |
255 *} |
154 *} |
256 |
|
257 ML {* |
|
258 fun typedef_main (qty_name, mx, rel, rty, equiv_thm) lthy = |
|
259 let |
|
260 (* generates typedef *) |
|
261 val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy |
|
262 |
|
263 (* abs and rep functions *) |
|
264 val abs_ty = #abs_type typedef_info |
|
265 val rep_ty = #rep_type typedef_info |
|
266 val abs_name = #Abs_name typedef_info |
|
267 val rep_name = #Rep_name typedef_info |
|
268 val abs = Const (abs_name, rep_ty --> abs_ty) |
|
269 val rep = Const (rep_name, abs_ty --> rep_ty) |
|
270 |
|
271 (* ABS and REP definitions *) |
|
272 val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT ) |
|
273 val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT ) |
|
274 val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs) |
|
275 val REP_trm = Syntax.check_term lthy1 (REP_const $ rep) |
|
276 val ABS_name = Binding.prefix_name "ABS_" qty_name |
|
277 val REP_name = Binding.prefix_name "REP_" qty_name |
|
278 val (((ABS, ABS_def), (REP, REP_def)), lthy2) = |
|
279 lthy1 |> make_def (ABS_name, NoSyn, ABS_trm) |
|
280 ||>> make_def (REP_name, NoSyn, REP_trm) |
|
281 |
|
282 (* quot_type theorem *) |
|
283 val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2 |
|
284 val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name |
|
285 |
|
286 (* quotient theorem *) |
|
287 val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 |
|
288 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name |
|
289 |
|
290 (* interpretation *) |
|
291 val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) |
|
292 val ((_, [eqn1pre]), lthy3) = Variable.import true [ABS_def] lthy2; |
|
293 val eqn1i = Thm.prop_of (symmetric eqn1pre) |
|
294 val ((_, [eqn2pre]), lthy4) = Variable.import true [REP_def] lthy3; |
|
295 val eqn2i = Thm.prop_of (symmetric eqn2pre) |
|
296 |
|
297 val exp_morphism = ProofContext.export_morphism lthy4 (ProofContext.init (ProofContext.theory_of lthy4)); |
|
298 val exp_term = Morphism.term exp_morphism; |
|
299 val exp = Morphism.thm exp_morphism; |
|
300 |
|
301 val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN |
|
302 ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))) |
|
303 val mthdt = Method.Basic (fn _ => mthd) |
|
304 val bymt = Proof.global_terminal_proof (mthdt, NONE) |
|
305 val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true), |
|
306 Expression.Named [ |
|
307 ("R", rel), |
|
308 ("Abs", abs), |
|
309 ("Rep", rep) |
|
310 ]))] |
|
311 in |
|
312 lthy4 |
|
313 |> note_thm (quot_thm_name, quot_thm) |
|
314 ||>> note_thm (quotient_thm_name, quotient_thm) |
|
315 ||> LocalTheory.theory (fn thy => |
|
316 let |
|
317 val global_eqns = map exp_term [eqn2i, eqn1i]; |
|
318 (* Not sure if the following context should not be used *) |
|
319 val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4; |
|
320 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
|
321 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) |
|
322 end |
|
323 *} |
|
324 |
|
325 |
155 |
326 section {* various tests for quotient types*} |
156 section {* various tests for quotient types*} |
327 datatype trm = |
157 datatype trm = |
328 var "nat" |
158 var "nat" |
329 | app "trm" "trm" |
159 | app "trm" "trm" |