334 |
334 |
335 (* definition of raw fv_functions *) |
335 (* definition of raw fv_functions *) |
336 val _ = warning "Definition of raw fv-functions"; |
336 val _ = warning "Definition of raw fv-functions"; |
337 val lthy3 = Theory_Target.init NONE thy; |
337 val lthy3 = Theory_Target.init NONE thy; |
338 |
338 |
339 val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = |
339 val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = |
340 if get_STEPS lthy3 > 2 |
340 if get_STEPS lthy3 > 2 |
341 then raw_bn_decls all_raw_tys raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 |
341 then raw_bn_decls all_raw_tys raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3 |
342 else raise TEST lthy3 |
342 else raise TEST lthy3 |
343 |
343 |
344 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = |
344 val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = |
368 |
368 |
369 (* proving equivariance lemmas for bns, fvs and alpha *) |
369 (* proving equivariance lemmas for bns, fvs and alpha *) |
370 val _ = warning "Proving equivariance"; |
370 val _ = warning "Proving equivariance"; |
371 val bn_eqvt = |
371 val bn_eqvt = |
372 if get_STEPS lthy > 6 |
372 if get_STEPS lthy > 6 |
373 then raw_prove_eqvt raw_bn_funs raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4 |
373 then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4 |
374 else raise TEST lthy4 |
374 else raise TEST lthy4 |
375 |
375 |
376 (* noting the bn_eqvt lemmas in a temprorary theory *) |
376 (* noting the bn_eqvt lemmas in a temprorary theory *) |
377 val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
377 val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
378 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4) |
378 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4) |
435 else raise TEST lthy6 |
435 else raise TEST lthy6 |
436 |
436 |
437 val qtys = map #qtyp qty_infos |
437 val qtys = map #qtyp qty_infos |
438 |
438 |
439 (* defining of quotient term-constructors, binding functions, free vars functions *) |
439 (* defining of quotient term-constructors, binding functions, free vars functions *) |
440 val qconstr_descr = |
440 val _ = warning "Defining the quotient constnats" |
|
441 val qconstrs_descr = |
441 flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts) |
442 flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts) |
442 |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs |
443 |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs |
443 |
444 |
444 val qbns_descr = |
445 val qbns_descr = |
445 map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bn_funs |
446 map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns |
446 |
447 |
447 val qfvs_descr = |
448 val qfvs_descr = |
448 map2 (fn n => fn t => (n, t, NoSyn)) qty_names raw_fvs |
449 map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs |
449 |
450 |
450 |
451 val qfv_bns_descr = |
451 val (qs, lthy8) = |
452 map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns |
|
453 |
|
454 (* TODO: probably also needs alpha_bn *) |
|
455 val ((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), lthy8) = |
452 if get_STEPS lthy > 15 |
456 if get_STEPS lthy > 15 |
453 then qconst_defs qtys (qconstr_descr @ qbns_descr @ qfvs_descr) lthy7 |
457 then |
|
458 lthy7 |
|
459 |> qconst_defs qtys qconstrs_descr |
|
460 ||>> qconst_defs qtys qbns_descr |
|
461 ||>> qconst_defs qtys qfvs_descr |
|
462 ||>> qconst_defs qtys qfv_bns_descr |
454 else raise TEST lthy7 |
463 else raise TEST lthy7 |
455 |
464 |
456 val _ = tracing ("raw fvs " ^ commas (map @{make_string} raw_fvs)) |
465 val qconstrs = map #qconst qconstrs_info |
457 val _ = tracing ("raw fv_bns " ^ commas (map @{make_string} raw_fv_bns)) |
466 val qbns = map #qconst qbns_info |
458 |
467 val qfvs = map #qconst qfvs_info |
|
468 val qfv_bns = map #qconst qfv_bns_info |
|
469 |
|
470 (* respectfulness proofs *) |
|
471 |
459 (* HERE *) |
472 (* HERE *) |
460 |
473 |
461 val _ = |
474 val _ = |
462 if get_STEPS lthy > 16 |
475 if get_STEPS lthy > 16 |
463 then true else raise TEST lthy8 |
476 then true else raise TEST lthy8 |
464 |
477 |
465 (* old stuff *) |
478 (* old stuff *) |
466 |
479 |
467 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
|
468 val raw_consts = |
|
469 flat (map (fn (i, (_, _, l)) => |
|
470 map (fn (cname, dts) => |
|
471 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
|
472 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); |
|
473 val dd = map2 (fn x => fn y => (x, y, NoSyn)) const_names raw_consts |
|
474 val (consts, _, lthy8) = quotient_lift_consts_export qtys dd lthy7; |
|
475 val _ = warning "Proving respects"; |
480 val _ = warning "Proving respects"; |
476 |
481 |
477 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
482 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
478 val bns = raw_bn_funs ~~ bn_nos; |
483 val bns = raw_bns ~~ bn_nos; |
479 |
484 |
480 val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8; |
485 val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8; |
481 val (bns_rsp_pre, lthy9) = fold_map ( |
486 val (bns_rsp_pre, lthy9) = fold_map ( |
482 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
487 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
483 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
488 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
502 alpha_bn_rsp_tac) alpha_bn_trms lthy11 |
507 alpha_bn_rsp_tac) alpha_bn_trms lthy11 |
503 fun const_rsp_tac _ = |
508 fun const_rsp_tac _ = |
504 let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a |
509 let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a |
505 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end |
510 in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end |
506 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
511 val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst] |
507 const_rsp_tac) raw_consts lthy11a |
512 const_rsp_tac) all_raw_constrs lthy11a |
508 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) |
513 val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns) |
509 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns) |
514 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns) |
510 val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys dd lthy12; |
515 val (qfv_info, lthy12a) = qconst_defs qtys dd lthy12; |
|
516 val qfv_ts = map #qconst qfv_info |
|
517 val qfv_defs = map #def qfv_info |
511 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |
518 val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts; |
512 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
519 val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs |
513 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bn_funs |
520 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bns |
514 val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys dd lthy12a; |
521 val (qbn_info, lthy12b) = qconst_defs qtys dd lthy12a; |
|
522 val qbn_ts = map #qconst qbn_info |
|
523 val qbn_defs = map #def qbn_info |
515 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms |
524 val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms |
516 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qalpha_bn_names alpha_bn_trms |
525 val dd = map2 (fn x => fn y => (x, y, NoSyn)) qalpha_bn_names alpha_bn_trms |
517 val (qalpha_bn_trms, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys dd lthy12b; |
526 val (qalpha_info, lthy12c) = qconst_defs qtys dd lthy12b; |
|
527 val qalpha_bn_trms = map #qconst qalpha_info |
|
528 val qalphabn_defs = map #def qalpha_info |
|
529 |
518 val _ = warning "Lifting permutations"; |
530 val _ = warning "Lifting permutations"; |
519 val thy = Local_Theory.exit_global lthy12c; |
531 val thy = Local_Theory.exit_global lthy12c; |
520 val perm_names = map (fn x => "permute_" ^ x) qty_names |
532 val perm_names = map (fn x => "permute_" ^ x) qty_names |
521 val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs |
533 val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs |
522 val thy' = define_lifted_perms qtys qty_full_names dd raw_perm_simps thy; |
534 (* use Local_Theory.theory_result *) |
|
535 val thy' = qperm_defs qtys qty_full_names dd raw_perm_simps thy; |
523 val lthy13 = Theory_Target.init NONE thy'; |
536 val lthy13 = Theory_Target.init NONE thy'; |
|
537 |
524 val q_name = space_implode "_" qty_names; |
538 val q_name = space_implode "_" qty_names; |
525 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
539 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
526 val _ = warning "Lifting induction"; |
540 val _ = warning "Lifting induction"; |
527 val constr_names = map (Long_Name.base_name o fst o dest_Const) consts; |
541 val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs; |
528 val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm); |
542 val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm); |
529 fun note_suffix s th ctxt = |
543 fun note_suffix s th ctxt = |
530 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
544 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
531 fun note_simp_suffix s th ctxt = |
545 fun note_simp_suffix s th ctxt = |
532 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
546 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
554 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
568 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
555 val q_eqvt = map (lift_thm qtys lthy19) (bn_eqvt @ fv_eqvt); |
569 val q_eqvt = map (lift_thm qtys lthy19) (bn_eqvt @ fv_eqvt); |
556 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
570 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
557 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
571 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
558 val _ = warning "Supports"; |
572 val _ = warning "Supports"; |
559 val supports = map (prove_supports lthy20 q_perm) consts; |
573 val supports = map (prove_supports lthy20 q_perm) qconstrs; |
560 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); |
574 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); |
561 val thy3 = Local_Theory.exit_global lthy20; |
575 val thy3 = Local_Theory.exit_global lthy20; |
562 val _ = warning "Instantiating FS"; |
576 val _ = warning "Instantiating FS"; |
563 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
577 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
564 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
578 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |