328 val _ = warning "Distinct theorems"; |
328 val _ = warning "Distinct theorems"; |
329 val alpha_distincts = |
329 val alpha_distincts = |
330 mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys |
330 mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys |
331 |
331 |
332 (* definition of alpha_eq_iff lemmas *) |
332 (* definition of alpha_eq_iff lemmas *) |
333 (* they have a funny shape for the simplifier *) |
333 (* they have a funny shape for the simplifier ---- CHECK WHETHER NEEDED*) |
334 val _ = warning "Eq-iff theorems"; |
334 val _ = warning "Eq-iff theorems"; |
335 val (alpha_eq_iff_simps, alpha_eq_iff) = |
335 val (alpha_eq_iff_simps, alpha_eq_iff) = |
336 if get_STEPS lthy > 5 |
336 if get_STEPS lthy > 5 |
337 then mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases |
337 then mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases |
338 else raise TEST lthy4 |
338 else raise TEST lthy4 |
400 if get_STEPS lthy > 14 |
400 if get_STEPS lthy > 14 |
401 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 |
401 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 |
402 else raise TEST lthy6 |
402 else raise TEST lthy6 |
403 |
403 |
404 (* respectfulness proofs *) |
404 (* respectfulness proofs *) |
405 val raw_funs_rsp_aux = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
405 val raw_funs_rsp_aux = |
406 raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6 |
406 if get_STEPS lthy > 15 |
407 val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux |
407 then raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
408 |
408 raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6 |
409 val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct |
409 else raise TEST lthy6 |
410 (raw_size_thms @ raw_size_eqvt) lthy6 |
410 |
411 |> map mk_funs_rsp |
411 val raw_funs_rsp = |
412 |
412 if get_STEPS lthy > 16 |
413 val raw_constrs_rsp = raw_constrs_rsp raw_constrs alpha_trms alpha_intros |
413 then map mk_funs_rsp raw_funs_rsp_aux |
414 (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 |
414 else raise TEST lthy6 |
415 |
415 |
416 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt |
416 val raw_size_rsp = |
417 |
417 if get_STEPS lthy > 17 |
418 val alpha_bn_rsp = raw_alpha_bn_rsp alpha_bn_equivp_thms alpha_bn_imp_thms |
418 then |
|
419 raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct |
|
420 (raw_size_thms @ raw_size_eqvt) lthy6 |
|
421 |> map mk_funs_rsp |
|
422 else raise TEST lthy6 |
|
423 |
|
424 val raw_constrs_rsp = |
|
425 if get_STEPS lthy > 18 |
|
426 then raw_constrs_rsp raw_constrs alpha_trms alpha_intros |
|
427 (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 |
|
428 else raise TEST lthy6 |
|
429 |
|
430 val alpha_permute_rsp = |
|
431 if get_STEPS lthy > 19 |
|
432 then map mk_alpha_permute_rsp alpha_eqvt |
|
433 else raise TEST lthy6 |
|
434 |
|
435 val alpha_bn_rsp = |
|
436 if get_STEPS lthy > 20 |
|
437 then raw_alpha_bn_rsp alpha_bn_equivp_thms alpha_bn_imp_thms |
|
438 else raise TEST lthy6 |
419 |
439 |
420 (* noting the quot_respects lemmas *) |
440 (* noting the quot_respects lemmas *) |
421 val (_, lthy6a) = |
441 val (_, lthy6a) = |
422 if get_STEPS lthy > 15 |
442 if get_STEPS lthy > 21 |
423 then Local_Theory.note ((Binding.empty, [rsp_attrib]), |
443 then Local_Theory.note ((Binding.empty, [rsp_attrib]), |
424 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6 |
444 raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6 |
425 else raise TEST lthy6 |
445 else raise TEST lthy6 |
426 |
446 |
427 (* defining the quotient type *) |
447 (* defining the quotient type *) |
428 val _ = warning "Declaring the quotient types" |
448 val _ = warning "Declaring the quotient types" |
429 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
449 val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts |
430 |
450 |
431 val (qty_infos, lthy7) = |
451 val (qty_infos, lthy7) = |
432 if get_STEPS lthy > 16 |
452 if get_STEPS lthy > 22 |
433 then define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a |
453 then define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a |
434 else raise TEST lthy6a |
454 else raise TEST lthy6a |
435 |
455 |
436 val qtys = map #qtyp qty_infos |
456 val qtys = map #qtyp qty_infos |
437 val qty_full_names = map (fst o dest_Type) qtys |
457 val qty_full_names = map (fst o dest_Type) qtys |
460 |
480 |
461 val qsize_descr = |
481 val qsize_descr = |
462 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms |
482 map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms |
463 |
483 |
464 val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = |
484 val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = |
465 if get_STEPS lthy > 17 |
485 if get_STEPS lthy > 23 |
466 then |
486 then |
467 lthy7 |
487 lthy7 |
468 |> define_qconsts qtys qconstrs_descr |
488 |> define_qconsts qtys qconstrs_descr |
469 ||>> define_qconsts qtys qbns_descr |
489 ||>> define_qconsts qtys qbns_descr |
470 ||>> define_qconsts qtys qfvs_descr |
490 ||>> define_qconsts qtys qfvs_descr |
472 ||>> define_qconsts qtys qalpha_bns_descr |
492 ||>> define_qconsts qtys qalpha_bns_descr |
473 else raise TEST lthy7 |
493 else raise TEST lthy7 |
474 |
494 |
475 (* definition of the quotient permfunctions and pt-class *) |
495 (* definition of the quotient permfunctions and pt-class *) |
476 val lthy9 = |
496 val lthy9 = |
477 if get_STEPS lthy > 18 |
497 if get_STEPS lthy > 24 |
478 then define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8 |
498 then define_qperms qtys qty_full_names tvs qperm_descr raw_perm_laws lthy8 |
479 else raise TEST lthy8 |
499 else raise TEST lthy8 |
480 |
500 |
481 val lthy9a = |
501 val lthy9a = |
482 if get_STEPS lthy > 19 |
502 if get_STEPS lthy > 25 |
483 then define_qsizes qtys qty_full_names tvs qsize_descr lthy9 |
503 then define_qsizes qtys qty_full_names tvs qsize_descr lthy9 |
484 else raise TEST lthy9 |
504 else raise TEST lthy9 |
485 |
505 |
486 val qconstrs = map #qconst qconstrs_info |
506 val qconstrs = map #qconst qconstrs_info |
487 val qbns = map #qconst qbns_info |
507 val qbns = map #qconst qbns_info |
494 |
514 |
495 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
515 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
496 prod.cases} |
516 prod.cases} |
497 |
517 |
498 val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = |
518 val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = |
499 if get_STEPS lthy > 20 |
519 if get_STEPS lthy > 26 |
500 then |
520 then |
501 lthy9a |
521 lthy9a |
502 |> lift_thms qtys [] alpha_distincts |
522 |> lift_thms qtys [] alpha_distincts |
503 ||>> lift_thms qtys eq_iff_simps alpha_eq_iff |
523 ||>> lift_thms qtys eq_iff_simps alpha_eq_iff |
504 ||>> lift_thms qtys [] raw_fv_defs |
524 ||>> lift_thms qtys [] raw_fv_defs |
506 ||>> lift_thms qtys [] raw_perm_simps |
526 ||>> lift_thms qtys [] raw_perm_simps |
507 ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) |
527 ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) |
508 else raise TEST lthy9a |
528 else raise TEST lthy9a |
509 |
529 |
510 val (((qsize_eqvt, [qinduct]), qexhausts), lthyB) = |
530 val (((qsize_eqvt, [qinduct]), qexhausts), lthyB) = |
511 if get_STEPS lthy > 20 |
531 if get_STEPS lthy > 27 |
512 then |
532 then |
513 lthyA |
533 lthyA |
514 |> lift_thms qtys [] raw_size_eqvt |
534 |> lift_thms qtys [] raw_size_eqvt |
515 ||>> lift_thms qtys [] [raw_induct_thm] |
535 ||>> lift_thms qtys [] [raw_induct_thm] |
516 ||>> lift_thms qtys [] raw_exhaust_thms |
536 ||>> lift_thms qtys [] raw_exhaust_thms |