403 (Local_Theory.restore lthy_tmp) |
403 (Local_Theory.restore lthy_tmp) |
404 else raise TEST lthy4 |
404 else raise TEST lthy4 |
405 |
405 |
406 val lthy_tmp' = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) |
406 val lthy_tmp' = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) |
407 |
407 |
408 val (alpha_eqvt, _) = |
408 val (alpha_eqvt, lthy_tmp'') = |
409 if get_STEPS lthy > 8 |
409 if get_STEPS lthy > 8 |
410 then Nominal_Eqvt.equivariance false alpha_trms alpha_induct alpha_intros lthy_tmp' |
410 then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy_tmp' |
411 else raise TEST lthy4 |
411 else raise TEST lthy4 |
412 |
412 |
|
413 (* proving alpha equivalence *) |
|
414 val _ = warning "Proving equivalence" |
|
415 |
|
416 val alpha_sym_thms = |
|
417 if get_STEPS lthy > 9 |
|
418 then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy_tmp'' |
|
419 else raise TEST lthy4 |
|
420 |
|
421 val alpha_trans_thms = |
|
422 if get_STEPS lthy > 10 |
|
423 then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) |
|
424 alpha_intros alpha_induct alpha_cases lthy_tmp'' |
|
425 else raise TEST lthy4 |
|
426 |
|
427 |
|
428 val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms)) |
|
429 val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms)) |
|
430 |
413 val _ = |
431 val _ = |
414 if get_STEPS lthy > 9 |
432 if get_STEPS lthy > 11 |
415 then true else raise TEST lthy4 |
433 then true else raise TEST lthy4 |
416 |
|
417 (* proving alpha equivalence *) |
|
418 val _ = warning "Proving equivalence"; |
|
419 |
434 |
420 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos |
435 val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos |
421 |
436 |
422 val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4; |
437 val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4; |
423 val alpha_equivp = |
438 val alpha_equivp = |
424 if !cheat_equivp then map (equivp_hack lthy4) alpha_trms |
439 if !cheat_equivp then map (equivp_hack lthy4) alpha_trms |
425 else build_equivps alpha_trms reflps alpha_induct |
440 else build_equivps alpha_trms reflps alpha_induct |
426 inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4; |
441 inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4; |
|
442 |
427 val qty_binds = map (fn (_, b, _, _) => b) dts; |
443 val qty_binds = map (fn (_, b, _, _) => b) dts; |
428 val qty_names = map Name.of_binding qty_binds; |
444 val qty_names = map Name.of_binding qty_binds; |
429 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
445 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
430 val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp lthy4; |
446 val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_trms alpha_equivp lthy4; |
431 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
447 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |