339 (* noting the raw permutations as eqvt theorems *) |
339 (* noting the raw permutations as eqvt theorems *) |
340 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a |
340 val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a |
341 |
341 |
342 (* definition of raw fv_functions *) |
342 (* definition of raw fv_functions *) |
343 val _ = warning "Definition of raw fv-functions"; |
343 val _ = warning "Definition of raw fv-functions"; |
344 val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) = |
344 val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) = |
345 if get_STEPS lthy3 > 2 |
345 if get_STEPS lthy3 > 2 |
346 then raw_bn_decls raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs |
346 then raw_bn_decls raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs |
347 (raw_inject_thms @ raw_distinct_thms) lthy3 |
347 (raw_inject_thms @ raw_distinct_thms) lthy3 |
348 else raise TEST lthy3 |
348 else raise TEST lthy3 |
349 |
349 |
375 |
375 |
376 (* proving equivariance lemmas for bns, fvs, size and alpha *) |
376 (* proving equivariance lemmas for bns, fvs, size and alpha *) |
377 val _ = warning "Proving equivariance"; |
377 val _ = warning "Proving equivariance"; |
378 val bn_eqvt = |
378 val bn_eqvt = |
379 if get_STEPS lthy > 6 |
379 if get_STEPS lthy > 6 |
380 then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_simps) lthy4 |
380 then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_defs @ raw_perm_simps) lthy4 |
381 else raise TEST lthy4 |
381 else raise TEST lthy4 |
382 |
382 |
383 (* noting the bn_eqvt lemmas in a temprorary theory *) |
383 (* noting the bn_eqvt lemmas in a temprorary theory *) |
384 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), bn_eqvt) lthy4) |
384 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), bn_eqvt) lthy4) |
385 |
385 |
437 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 |
437 then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 |
438 else raise TEST lthy6 |
438 else raise TEST lthy6 |
439 |
439 |
440 (* respectfulness proofs *) |
440 (* respectfulness proofs *) |
441 val raw_funs_rsp_aux = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
441 val raw_funs_rsp_aux = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs |
442 raw_bns raw_fv_bns alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6 |
442 raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6 |
443 val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux |
443 val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux |
444 |
444 |
445 val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct |
445 val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct |
446 (raw_size_thms @ raw_size_eqvt) lthy6 |
446 (raw_size_thms @ raw_size_eqvt) lthy6 |
447 |> map mk_funs_rsp |
447 |> map mk_funs_rsp |
532 val (_, lthy9') = lthy9a |
532 val (_, lthy9') = lthy9a |
533 |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) |
533 |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) |
534 ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) |
534 ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) |
535 ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) |
535 ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) |
536 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) |
536 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) |
|
537 ||>> Local_Theory.note ((@{binding "bn_defs"}, []), raw_bn_defs) |
537 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
538 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
538 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
539 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
539 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
540 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
540 ||>> Local_Theory.note ((@{binding "alpha_equivp"}, []), alpha_equivp_thms) |
541 ||>> Local_Theory.note ((@{binding "alpha_equivp"}, []), alpha_equivp_thms) |
541 |
542 |
552 val _ = warning "Proving respects"; |
553 val _ = warning "Proving respects"; |
553 |
554 |
554 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
555 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
555 val bns = raw_bns ~~ bn_nos; |
556 val bns = raw_bns ~~ bn_nos; |
556 |
557 |
557 val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8; |
558 val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_defs (map fst bns) lthy8; |
558 val (bns_rsp_pre, lthy9) = fold_map ( |
559 val (bns_rsp_pre, lthy9) = fold_map ( |
559 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
560 fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ => |
560 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
561 resolve_tac bns_rsp_pre' 1)) bns lthy8; |
561 val bns_rsp = flat (map snd bns_rsp_pre); |
562 val bns_rsp = flat (map snd bns_rsp_pre); |
562 |
563 |
620 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
621 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
621 val q_perm = map (lift_thm qtys lthy14) raw_perm_simps; |
622 val q_perm = map (lift_thm qtys lthy14) raw_perm_simps; |
622 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
623 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
623 val q_fv = map (lift_thm qtys lthy15) raw_fv_defs; |
624 val q_fv = map (lift_thm qtys lthy15) raw_fv_defs; |
624 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
625 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
625 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; |
626 val q_bn = map (lift_thm qtys lthy16) raw_bn_defs; |
626 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
627 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
627 val _ = warning "Lifting eq-iff"; |
628 val _ = warning "Lifting eq-iff"; |
628 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |
629 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |
629 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff |
630 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff |
630 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0 |
631 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0 |