600 Free ("pi", permT) $ Free (x, T))) |
600 Free ("pi", permT) $ Free (x, T))) |
601 end) (rep_set_names'' ~~ recTs' ~~ perm_indnames'))))) |
601 end) (rep_set_names'' ~~ recTs' ~~ perm_indnames'))))) |
602 (fn _ => EVERY |
602 (fn _ => EVERY |
603 [indtac rep_induct [] 1, |
603 [indtac rep_induct [] 1, |
604 ALLGOALS (simp_tac (global_simpset_of thy4 addsimps |
604 ALLGOALS (simp_tac (global_simpset_of thy4 addsimps |
605 (symmetric perm_fun_def :: abs_perm))), |
605 (Thm.symmetric perm_fun_def :: abs_perm))), |
606 ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])), |
606 ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])), |
607 length new_type_names)); |
607 length new_type_names)); |
608 |
608 |
609 val perm_closed_thmss = map mk_perm_closed atoms; |
609 val perm_closed_thmss = map mk_perm_closed atoms; |
610 |
610 |
925 (fn _ => EVERY |
925 (fn _ => EVERY |
926 [simp_tac (global_simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1, |
926 [simp_tac (global_simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1, |
927 simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @ |
927 simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @ |
928 constr_defs @ perm_closed_thms)) 1, |
928 constr_defs @ perm_closed_thms)) 1, |
929 TRY (simp_tac (HOL_basic_ss addsimps |
929 TRY (simp_tac (HOL_basic_ss addsimps |
930 (symmetric perm_fun_def :: abs_perm)) 1), |
930 (Thm.symmetric perm_fun_def :: abs_perm)) 1), |
931 TRY (simp_tac (HOL_basic_ss addsimps |
931 TRY (simp_tac (HOL_basic_ss addsimps |
932 (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @ |
932 (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @ |
933 perm_closed_thms)) 1)]) |
933 perm_closed_thms)) 1)]) |
934 end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss) |
934 end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss) |
935 end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss); |
935 end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss); |
1075 (fn {prems, ...} => EVERY |
1075 (fn {prems, ...} => EVERY |
1076 [rtac indrule_lemma' 1, |
1076 [rtac indrule_lemma' 1, |
1077 (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1, |
1077 (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1, |
1078 EVERY (map (fn (prem, r) => (EVERY |
1078 EVERY (map (fn (prem, r) => (EVERY |
1079 [REPEAT (eresolve_tac Abs_inverse_thms' 1), |
1079 [REPEAT (eresolve_tac Abs_inverse_thms' 1), |
1080 simp_tac (HOL_basic_ss addsimps [symmetric r]) 1, |
1080 simp_tac (HOL_basic_ss addsimps [Thm.symmetric r]) 1, |
1081 DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) |
1081 DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) |
1082 (prems ~~ constr_defs))]); |
1082 (prems ~~ constr_defs))]); |
1083 |
1083 |
1084 val case_names_induct = mk_case_names_induct descr''; |
1084 val case_names_induct = mk_case_names_induct descr''; |
1085 |
1085 |
1639 [(cterm_of thy11 S, |
1639 [(cterm_of thy11 S, |
1640 cterm_of thy11 (Const ("Nominal.supp", |
1640 cterm_of thy11 (Const ("Nominal.supp", |
1641 fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))] |
1641 fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))] |
1642 supports_fresh) 1, |
1642 supports_fresh) 1, |
1643 simp_tac (HOL_basic_ss addsimps |
1643 simp_tac (HOL_basic_ss addsimps |
1644 [supports_def, symmetric fresh_def, fresh_prod]) 1, |
1644 [supports_def, Thm.symmetric fresh_def, fresh_prod]) 1, |
1645 REPEAT_DETERM (resolve_tac [allI, impI] 1), |
1645 REPEAT_DETERM (resolve_tac [allI, impI] 1), |
1646 REPEAT_DETERM (etac conjE 1), |
1646 REPEAT_DETERM (etac conjE 1), |
1647 rtac unique 1, |
1647 rtac unique 1, |
1648 SUBPROOF (fn {prems = prems', params = [(_, a), (_, b)], ...} => EVERY |
1648 SUBPROOF (fn {prems = prems', params = [(_, a), (_, b)], ...} => EVERY |
1649 [cut_facts_tac [rec_prem] 1, |
1649 [cut_facts_tac [rec_prem] 1, |
1653 asm_simp_tac (HOL_ss addsimps |
1653 asm_simp_tac (HOL_ss addsimps |
1654 (prems' @ perm_swap @ perm_fresh_fresh)) 1]) context 1, |
1654 (prems' @ perm_swap @ perm_fresh_fresh)) 1]) context 1, |
1655 rtac rec_prem 1, |
1655 rtac rec_prem 1, |
1656 simp_tac (HOL_ss addsimps (fs_name :: |
1656 simp_tac (HOL_ss addsimps (fs_name :: |
1657 supp_prod :: finite_Un :: finite_prems)) 1, |
1657 supp_prod :: finite_Un :: finite_prems)) 1, |
1658 simp_tac (HOL_ss addsimps (symmetric fresh_def :: |
1658 simp_tac (HOL_ss addsimps (Thm.symmetric fresh_def :: |
1659 fresh_prod :: fresh_prems)) 1] |
1659 fresh_prod :: fresh_prems)) 1] |
1660 end)) |
1660 end)) |
1661 end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ eqvt_ths) |
1661 end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ eqvt_ths) |
1662 end) (dt_atomTs ~~ rec_equiv_thms' ~~ finite_premss); |
1662 end) (dt_atomTs ~~ rec_equiv_thms' ~~ finite_premss); |
1663 |
1663 |
1744 maps (fn ((_, finite_ths), finite_th) => |
1744 maps (fn ((_, finite_ths), finite_th) => |
1745 [cut_facts_tac (finite_th :: finite_ths) 1, |
1745 [cut_facts_tac (finite_th :: finite_ths) 1, |
1746 asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1]) |
1746 asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1]) |
1747 (finite_thss ~~ finite_ctxt_ths) @ |
1747 (finite_thss ~~ finite_ctxt_ths) @ |
1748 maps (fn ((_, idxss), elim) => maps (fn idxs => |
1748 maps (fn ((_, idxss), elim) => maps (fn idxs => |
1749 [full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff]) 1, |
1749 [full_simp_tac (HOL_ss addsimps [Thm.symmetric fresh_def, supp_prod, Un_iff]) 1, |
1750 REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1), |
1750 REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1), |
1751 rtac ex1I 1, |
1751 rtac ex1I 1, |
1752 (resolve_tac rec_intrs THEN_ALL_NEW atac) 1, |
1752 (resolve_tac rec_intrs THEN_ALL_NEW atac) 1, |
1753 rotate_tac ~1 1, |
1753 rotate_tac ~1 1, |
1754 ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac |
1754 ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac |