289 (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) |
289 (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) |
290 end |
290 end |
291 *} |
291 *} |
292 |
292 |
293 |
293 |
294 lemma equivp_hack: "equivp x" |
294 |
295 sorry |
|
296 ML {* |
|
297 fun equivp_hack ctxt rel = |
|
298 let |
|
299 val thy = ProofContext.theory_of ctxt |
|
300 val ty = domain_type (fastype_of rel) |
|
301 val cty = ctyp_of thy ty |
|
302 val ct = cterm_of thy rel |
|
303 in |
|
304 Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack} |
|
305 end |
|
306 *} |
|
307 |
|
308 ML {* val cheat_equivp = Unsynchronized.ref false *} |
|
309 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
295 ML {* val cheat_fv_rsp = Unsynchronized.ref false *} |
310 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} |
296 ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *} |
311 ML {* val cheat_supp_eq = Unsynchronized.ref false *} |
297 ML {* val cheat_supp_eq = Unsynchronized.ref false *} |
312 |
298 |
313 |
299 |
461 (* old stuff *) |
447 (* old stuff *) |
462 val _ = |
448 val _ = |
463 if get_STEPS lthy > 14 |
449 if get_STEPS lthy > 14 |
464 then true else raise TEST lthy4 |
450 then true else raise TEST lthy4 |
465 |
451 |
466 val alpha_equivp = |
|
467 if !cheat_equivp then map (equivp_hack lthy4) alpha_trms |
|
468 else build_equivps alpha_trms alpha_refl_thms alpha_induct |
|
469 inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4; |
|
470 |
|
471 val qty_binds = map (fn (_, b, _, _) => b) dts; |
452 val qty_binds = map (fn (_, b, _, _) => b) dts; |
472 val qty_names = map Name.of_binding qty_binds; |
453 val qty_names = map Name.of_binding qty_binds; |
473 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
454 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
474 val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp lthy4; |
455 val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp_thms lthy4; |
475 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
456 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
476 val raw_consts = |
457 val raw_consts = |
477 flat (map (fn (i, (_, _, l)) => |
458 flat (map (fn (i, (_, _, l)) => |
478 map (fn (cname, dts) => |
459 map (fn (cname, dts) => |
479 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
460 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
502 val fv_rsp = flat (map snd fv_rsp_pre); |
483 val fv_rsp = flat (map snd fv_rsp_pre); |
503 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs |
484 val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty raw_perm_funs |
504 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
485 (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10; |
505 fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
486 fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy |
506 else |
487 else |
507 let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts @ alpha_bn_distincts) alpha_equivp exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; |
488 let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts @ alpha_bn_distincts) alpha_equivp_thms exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end; |
508 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
489 val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
509 alpha_bn_rsp_tac) alpha_bn_trms lthy11 |
490 alpha_bn_rsp_tac) alpha_bn_trms lthy11 |
510 fun const_rsp_tac _ = |
491 fun const_rsp_tac _ = |
511 let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a |
492 let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a |
512 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end |
493 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end |