113 val induct = @{thm alpha_rtrm2_alpha_rassign.inducts(2)} |
113 val induct = @{thm alpha_rtrm2_alpha_rassign.inducts(2)} |
114 val fv_simps = @{thms rbv2.simps} |
114 val fv_simps = @{thms rbv2.simps} |
115 *} |
115 *} |
116 *) |
116 *) |
117 |
117 |
|
118 ML {* |
|
119 fun build_eqvts bind funs perms simps induct ctxt = |
|
120 let |
|
121 val pi = Free ("p", @{typ perm}); |
|
122 val types = map (domain_type o fastype_of) funs; |
|
123 val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types)); |
|
124 val args = map Free (indnames ~~ types); |
|
125 val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"} |
|
126 fun eqvtc (fnctn, (arg, perm)) = |
|
127 HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg))) |
|
128 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms)))) |
|
129 fun tac _ = (Datatype_Aux.indtac induct indnames THEN_ALL_NEW |
|
130 (asm_full_simp_tac (HOL_ss addsimps |
|
131 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1 |
|
132 val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac |
|
133 val thms = HOLogic.conj_elims thm |
|
134 in |
|
135 Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt |
118 end |
136 end |
|
137 *} |
|
138 |
|
139 |
|
140 ML {* |
|
141 fun build_alpha_eqvts funs perms simps induct ctxt = |
|
142 let |
|
143 val pi = Free ("p", @{typ perm}); |
|
144 val types = map (domain_type o fastype_of) funs; |
|
145 val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types)); |
|
146 val indnames2 = Name.variant_list ("p" :: indnames) (Datatype_Prop.make_tnames (map body_type types)); |
|
147 val args = map Free (indnames ~~ types); |
|
148 val args2 = map Free (indnames2 ~~ types); |
|
149 fun eqvtc ((alpha, perm), (arg, arg2)) = |
|
150 HOLogic.mk_imp (alpha $ arg $ arg2, |
|
151 (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2))) |
|
152 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2)))) |
|
153 fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
|
154 (asm_full_simp_tac (HOL_ss addsimps |
|
155 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) |
|
156 THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
|
157 (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW |
|
158 (asm_full_simp_tac (HOL_ss addsimps |
|
159 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps))) |
|
160 ) 1 |
|
161 val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac |
|
162 in |
|
163 map (fn x => mp OF [x]) (HOLogic.conj_elims thm) |
|
164 end |
|
165 *} |
|
166 |
|
167 |
|
168 end |