44 thm fv_rtrm1_fv_bp.simps |
44 thm fv_rtrm1_fv_bp.simps |
45 |
45 |
46 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *} |
46 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *} |
47 thm alpha1_inj |
47 thm alpha1_inj |
48 |
48 |
49 lemma alpha_bp_refl: "alpha_bp a a" |
|
50 apply induct |
|
51 apply (simp_all add: alpha1_inj) |
|
52 done |
|
53 |
|
54 lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)" |
|
55 apply rule |
|
56 apply (induct a b rule: alpha_rtrm1_alpha_bp.inducts(2)) |
|
57 apply (simp_all add: alpha_bp_refl) |
|
58 done |
|
59 |
|
60 lemma alpha_bp_eq: "alpha_bp = (op =)" |
|
61 apply (rule ext)+ |
|
62 apply (rule alpha_bp_eq_eq) |
|
63 done |
|
64 |
|
65 ML {* |
|
66 fun build_eqvts bind funs perms simps induct ctxt = |
|
67 let |
|
68 val pi = Free ("p", @{typ perm}); |
|
69 val types = map (domain_type o fastype_of) funs; |
|
70 val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types)); |
|
71 val args = map Free (indnames ~~ types); |
|
72 val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"} |
|
73 fun eqvtc (fnctn, (arg, perm)) = |
|
74 HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg))) |
|
75 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms)))) |
|
76 fun tac _ = (indtac induct indnames THEN_ALL_NEW |
|
77 (asm_full_simp_tac (HOL_ss addsimps |
|
78 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1 |
|
79 val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac |
|
80 val thms = HOLogic.conj_elims thm |
|
81 in |
|
82 Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt |
|
83 end |
|
84 *} |
|
85 |
|
86 local_setup {* |
49 local_setup {* |
87 snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)}) |
50 snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)}) |
88 *} |
51 *} |
89 |
52 |
90 local_setup {* |
53 local_setup {* |
91 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct} |
54 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct} |
92 *} |
55 *} |
93 |
56 |
94 ML {* |
|
95 fun build_alpha_eqvts funs perms simps induct ctxt = |
|
96 let |
|
97 val pi = Free ("p", @{typ perm}); |
|
98 val types = map (domain_type o fastype_of) funs; |
|
99 val indnames = Name.variant_list ["pi"] (Datatype_Prop.make_tnames (map body_type types)); |
|
100 val indnames2 = Name.variant_list ("pi" :: indnames) (Datatype_Prop.make_tnames (map body_type types)); |
|
101 val args = map Free (indnames ~~ types); |
|
102 val args2 = map Free (indnames2 ~~ types); |
|
103 fun eqvtc ((alpha, perm), (arg, arg2)) = |
|
104 HOLogic.mk_imp (alpha $ arg $ arg2, |
|
105 (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) |
|
106 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) |
|
107 fun tac _ = (rtac induct THEN_ALL_NEW |
|
108 (asm_full_simp_tac (HOL_ss addsimps |
|
109 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) |
|
110 THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
|
111 (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW |
|
112 (asm_full_simp_tac (HOL_ss addsimps |
|
113 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) |
|
114 ) 1 |
|
115 val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac |
|
116 in |
|
117 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
|
118 end |
|
119 *} |
|
120 |
57 |
121 local_setup {* |
58 local_setup {* |
122 (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []), |
59 (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []), |
123 build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt)) |
60 build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt)) |
124 *} |
61 *} |
668 thm alpha_rtrm6.intros |
616 thm alpha_rtrm6.intros |
669 |
617 |
670 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *} |
618 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_inj}, []), (build_alpha_inj @{thms alpha_rtrm6.intros} @{thms rtrm6.distinct rtrm6.inject} @{thms alpha_rtrm6.cases} ctxt)) ctxt)) *} |
671 thm alpha6_inj |
619 thm alpha6_inj |
672 |
620 |
673 lemma alpha6_eqvt: |
621 local_setup {* |
674 "xa \<approx>6 y \<Longrightarrow> (x \<bullet> xa) \<approx>6 (x \<bullet> y)" |
622 snd o (build_eqvts @{binding rbv6_eqvt} [@{term rbv6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] (@{thms rbv6.simps permute_rtrm6.simps}) @{thm rtrm6.induct}) |
675 sorry |
623 *} |
|
624 |
|
625 local_setup {* |
|
626 snd o build_eqvts @{binding fv_rtrm6_eqvt} [@{term fv_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] (@{thms fv_rtrm6.simps permute_rtrm6.simps}) @{thm rtrm6.induct} |
|
627 *} |
|
628 |
|
629 local_setup {* |
|
630 (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_eqvt}, []), |
|
631 build_alpha_eqvts [@{term alpha_rtrm6}] [@{term "permute :: perm \<Rightarrow> rtrm6 \<Rightarrow> rtrm6"}] @{thms permute_rtrm6.simps alpha6_inj} @{thm alpha_rtrm6.induct} ctxt) ctxt)) |
|
632 *} |
676 |
633 |
677 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []), |
634 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha6_equivp}, []), |
678 (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *} |
635 (build_equivps [@{term alpha_rtrm6}] @{thm rtrm6.induct} @{thm alpha_rtrm6.induct} @{thms rtrm6.inject} @{thms alpha6_inj} @{thms rtrm6.distinct} @{thms alpha_rtrm6.cases} @{thms alpha6_eqvt} ctxt)) ctxt)) *} |
679 thm alpha6_equivp |
636 thm alpha6_equivp |
680 |
637 |