401 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) lthy_tmp |
401 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) lthy_tmp |
402 else raise TEST lthy4 |
402 else raise TEST lthy4 |
403 |
403 |
404 val (_, lthy_tmp') = Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp |
404 val (_, lthy_tmp') = Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp |
405 |
405 |
406 val (alpha_eqvt, lthy6a) = |
406 |
|
407 |
|
408 val (alpha_eqvt, _) = |
407 if get_STEPS lthy > 8 |
409 if get_STEPS lthy > 8 |
408 then Nominal_Eqvt.equivariance alpha_trms alpha_induct alpha_intros lthy_tmp' |
410 then Nominal_Eqvt.equivariance false alpha_trms alpha_induct alpha_intros lthy_tmp' |
409 else raise TEST lthy4 |
411 else raise TEST lthy4 |
|
412 |
|
413 (* |
|
414 val _ = tracing ("bn_eqvts\n" ^ cat_lines (map @{make_string} bn_eqvt)) |
|
415 val _ = tracing ("fv_eqvts\n" ^ cat_lines (map @{make_string} fv_eqvt)) |
|
416 val _ = tracing ("alpha_eqvts\n" ^ cat_lines (map @{make_string} alpha_eqvt)) |
|
417 *) |
410 |
418 |
411 val _ = |
419 val _ = |
412 if get_STEPS lthy > 9 |
420 if get_STEPS lthy > 9 |
413 then true else raise TEST lthy4 |
421 then true else raise TEST lthy4 |
414 |
422 |
415 (* proving alpha equivalence *) |
423 (* proving alpha equivalence *) |
416 val _ = warning "Proving equivalence"; |
424 val _ = warning "Proving equivalence"; |
417 |
425 |
418 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos |
426 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos |
419 |
427 |
420 val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy6a; |
428 val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4; |
421 val alpha_equivp = |
429 val alpha_equivp = |
422 if !cheat_equivp then map (equivp_hack lthy6a) alpha_trms |
430 if !cheat_equivp then map (equivp_hack lthy4) alpha_trms |
423 else build_equivps alpha_trms reflps alpha_induct |
431 else build_equivps alpha_trms reflps alpha_induct |
424 inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy6a; |
432 inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4; |
425 val qty_binds = map (fn (_, b, _, _) => b) dts; |
433 val qty_binds = map (fn (_, b, _, _) => b) dts; |
426 val qty_names = map Name.of_binding qty_binds; |
434 val qty_names = map Name.of_binding qty_binds; |
427 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
435 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
428 val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp lthy6a; |
436 val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp lthy4; |
429 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
437 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
430 val raw_consts = |
438 val raw_consts = |
431 flat (map (fn (i, (_, _, l)) => |
439 flat (map (fn (i, (_, _, l)) => |
432 map (fn (cname, dts) => |
440 map (fn (cname, dts) => |
433 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
441 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |