373 then mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases |
373 then mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases |
374 else raise TEST lthy4 |
374 else raise TEST lthy4 |
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 raw_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_defs @ 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 raw_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]), raw_bn_eqvt) lthy4) |
385 |
385 |
386 val fv_eqvt = |
386 val raw_fv_eqvt = |
387 if get_STEPS lthy > 7 |
387 if get_STEPS lthy > 7 |
388 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) |
388 then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) |
389 (Local_Theory.restore lthy_tmp) |
389 (Local_Theory.restore lthy_tmp) |
390 else raise TEST lthy4 |
390 else raise TEST lthy4 |
391 |
391 |
395 (Local_Theory.restore lthy_tmp) |
395 (Local_Theory.restore lthy_tmp) |
396 |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]}) |
396 |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]}) |
397 |> map (fn thm => thm RS @{thm sym}) |
397 |> map (fn thm => thm RS @{thm sym}) |
398 else raise TEST lthy4 |
398 else raise TEST lthy4 |
399 |
399 |
400 val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), fv_eqvt) lthy_tmp) |
400 val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_fv_eqvt) lthy_tmp) |
401 |
401 |
402 val (alpha_eqvt, lthy6) = |
402 val (alpha_eqvt, lthy6) = |
403 if get_STEPS lthy > 9 |
403 if get_STEPS lthy > 9 |
404 then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 |
404 then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5 |
405 else raise TEST lthy4 |
405 else raise TEST lthy4 |
537 ||>> Local_Theory.note ((@{binding "bn_defs"}, []), raw_bn_defs) |
537 ||>> Local_Theory.note ((@{binding "bn_defs"}, []), raw_bn_defs) |
538 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
538 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
539 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
539 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
540 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
540 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
541 ||>> Local_Theory.note ((@{binding "alpha_equivp"}, []), alpha_equivp_thms) |
541 ||>> Local_Theory.note ((@{binding "alpha_equivp"}, []), alpha_equivp_thms) |
|
542 ||>> Local_Theory.note ((@{binding "fv_eqvt"}, []), raw_fv_eqvt) |
|
543 ||>> Local_Theory.note ((@{binding "bn_eqvt"}, []), raw_bn_eqvt) |
|
544 ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt) |
542 |
545 |
543 val _ = |
546 val _ = |
544 if get_STEPS lthy > 20 |
547 if get_STEPS lthy > 20 |
545 then true else raise TEST lthy9' |
548 then true else raise TEST lthy9' |
546 |
549 |
634 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1 |
637 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1 |
635 val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2 |
638 val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2 |
636 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
639 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
637 val q_dis = map (lift_thm qtys lthy18) alpha_distincts; |
640 val q_dis = map (lift_thm qtys lthy18) alpha_distincts; |
638 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
641 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
639 val q_eqvt = map (lift_thm qtys lthy19) (bn_eqvt @ fv_eqvt); |
642 val q_eqvt = map (lift_thm qtys lthy19) (raw_bn_eqvt @ raw_fv_eqvt); |
640 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
643 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
641 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
644 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
642 val _ = warning "Supports"; |
645 val _ = warning "Supports"; |
643 val supports = map (prove_supports lthy20 q_perm) qconstrs; |
646 val supports = map (prove_supports lthy20 q_perm) qconstrs; |
644 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); |
647 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); |