63 done |
63 done |
64 |
64 |
65 ML {* |
65 ML {* |
66 fun build_eqvts funs perms simps induct ctxt = |
66 fun build_eqvts funs perms simps induct ctxt = |
67 let |
67 let |
68 val pi = Free ("pi", @{typ perm}); |
68 val pi = Free ("p", @{typ perm}); |
69 val types = map (domain_type o fastype_of) funs; |
69 val types = map (domain_type o fastype_of) funs; |
70 val fv_indnames = Datatype_Prop.make_tnames (map body_type types); |
70 val fv_indnames = Datatype_Prop.make_tnames (map body_type types); |
71 val args = map Free (fv_indnames ~~ types); |
71 val args = map Free (fv_indnames ~~ types); |
72 val perm_at = Const (@{const_name permute}, @{typ "perm \<Rightarrow> atom set \<Rightarrow> atom set"}) |
72 val perm_at = Const (@{const_name permute}, @{typ "perm \<Rightarrow> atom set \<Rightarrow> atom set"}) |
73 fun eqvtc (fv, (arg, perm)) = |
73 fun eqvtc (fv, (arg, perm)) = |
74 HOLogic.mk_eq ((perm_at $ pi $ (fv $ arg)), (fv $ (perm $ pi $ arg))) |
74 HOLogic.mk_eq ((perm_at $ pi $ (fv $ arg)), (fv $ (perm $ pi $ arg))) |
75 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms)))) |
75 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms)))) |
76 fun tac _ = (indtac induct fv_indnames THEN_ALL_NEW |
76 fun tac _ = (indtac induct fv_indnames THEN_ALL_NEW |
77 (asm_full_simp_tac (HOL_ss addsimps |
77 (asm_full_simp_tac (HOL_ss addsimps |
78 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1 |
78 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1 |
|
79 val thm = Goal.prove ctxt ("p" :: fv_indnames) [] gl tac |
|
80 val thms = HOLogic.conj_elims thm |
79 in |
81 in |
80 Goal.prove ctxt ("pi" :: fv_indnames) [] gl tac |
82 Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt |
81 end |
83 end |
82 *} |
84 *} |
83 |
85 |
84 ML {* |
86 local_setup {* |
85 build_eqvts [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)} @{context} |
87 snd o (build_eqvts [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)}) |
86 *} |
88 *} |
87 lemma bv1_eqvt[eqvt]: |
89 |
88 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)" |
90 local_setup {* |
89 apply (induct x) |
91 snd o build_eqvts [@{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} |
90 apply (simp_all add: eqvts atom_eqvt) |
|
91 done |
|
92 |
|
93 ML {* |
|
94 build_eqvts [@{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} @{context} |
|
95 *} |
92 *} |
96 lemma fv_rtrm1_eqvt[eqvt]: |
93 thm eqvts |
97 "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)" |
|
98 "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)" |
|
99 apply (induct t and b) |
|
100 apply (simp_all add: eqvts atom_eqvt) |
|
101 done |
|
102 |
|
103 lemma alpha1_eqvt: |
94 lemma alpha1_eqvt: |
104 "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
95 "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
105 "alpha_bp a b \<Longrightarrow> alpha_bp (pi \<bullet> a) (pi \<bullet> b)" |
96 "alpha_bp a b \<Longrightarrow> alpha_bp (pi \<bullet> a) (pi \<bullet> b)" |
106 apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts) |
97 apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts) |
107 apply (simp_all add:eqvts alpha1_inj) |
98 apply (simp_all add:eqvts alpha1_inj) |