71 ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), rsp_thms) |
71 ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), rsp_thms) |
72 |> Local_Theory.note ((bind, []), user_thms) |
72 |> Local_Theory.note ((bind, []), user_thms) |
73 end |
73 end |
74 *} |
74 *} |
75 |
75 |
76 |
76 ML {* |
77 |
77 fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct |
78 ML {* |
78 *} |
79 fun fvbv_rsp_tac induct fvbv_simps = |
79 |
80 ((((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
80 ML {* |
81 (TRY o rtac @{thm TrueI})) THEN_ALL_NEW |
81 fun fvbv_rsp_tac induct fvbv_simps ctxt = |
82 asm_full_simp_tac |
82 ind_tac induct THEN_ALL_NEW |
83 (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) |
83 (TRY o rtac @{thm TrueI}) THEN_ALL_NEW |
84 THEN_ALL_NEW (REPEAT o eresolve_tac [conjE, exE] THEN' |
84 asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
85 asm_full_simp_tac |
85 asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) THEN_ALL_NEW |
86 (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)))) |
86 REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW |
87 *} |
87 asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW |
88 |
88 TRY o blast_tac (claset_of ctxt) |
|
89 *} |
89 |
90 |
90 ML {* |
91 ML {* |
91 fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt) |
92 fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt) |
92 fun all_eqvts ctxt = |
93 fun all_eqvts ctxt = |
93 Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt |
94 Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt |
120 ML_prf {* |
121 ML_prf {* |
121 val induct = @{thm alpha_rtrm2_alpha_rassign.inducts(2)} |
122 val induct = @{thm alpha_rtrm2_alpha_rassign.inducts(2)} |
122 val fv_simps = @{thms rbv2.simps} |
123 val fv_simps = @{thms rbv2.simps} |
123 *} |
124 *} |
124 *) |
125 *) |
125 |
|
126 ML {* |
|
127 fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct |
|
128 *} |
|
129 |
126 |
130 ML {* |
127 ML {* |
131 fun build_eqvts_tac induct simps ctxt inds _ = (Datatype_Aux.indtac induct inds THEN_ALL_NEW |
128 fun build_eqvts_tac induct simps ctxt inds _ = (Datatype_Aux.indtac induct inds THEN_ALL_NEW |
132 (asm_full_simp_tac (HOL_ss addsimps |
129 (asm_full_simp_tac (HOL_ss addsimps |
133 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1 |
130 (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1 |
217 ML {* |
214 ML {* |
218 fun build_bv_eqvt simps inducts (t, n) ctxt = |
215 fun build_bv_eqvt simps inducts (t, n) ctxt = |
219 build_eqvts Binding.empty [t] (build_eqvts_tac (nth inducts n) simps ctxt) ctxt |
216 build_eqvts Binding.empty [t] (build_eqvts_tac (nth inducts n) simps ctxt) ctxt |
220 *} |
217 *} |
221 |
218 |
222 end |
219 ML {* |
|
220 fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt = |
|
221 let |
|
222 val (fvs_alphas, ls) = split_list fv_alphas_lst; |
|
223 val (fv_ts, alpha_ts) = split_list fvs_alphas; |
|
224 val tys = map (domain_type o fastype_of) alpha_ts; |
|
225 val names = Datatype_Prop.make_tnames tys; |
|
226 val names2 = Name.variant_list names names; |
|
227 val args = map Free (names ~~ tys); |
|
228 val args2 = map Free (names2 ~~ tys); |
|
229 fun mk_fv_rsp arg arg2 (fv, alpha) = HOLogic.mk_eq ((fv $ arg), (fv $ arg2)); |
|
230 fun fv_rsp_arg (((fv, alpha), (arg, arg2)), l) = |
|
231 HOLogic.mk_imp ( |
|
232 (alpha $ arg $ arg2), |
|
233 (foldr1 HOLogic.mk_conj |
|
234 (HOLogic.mk_eq (fv $ arg, fv $ arg2) :: |
|
235 (map (mk_fv_rsp arg arg2) l)))); |
|
236 val nobn_eqs = map fv_rsp_arg (((fv_ts ~~ alpha_ts) ~~ (args ~~ args2)) ~~ ls); |
|
237 fun mk_fv_rsp_bn arg arg2 (fv, alpha) = |
|
238 HOLogic.mk_imp ( |
|
239 (alpha $ arg $ arg2), |
|
240 HOLogic.mk_eq ((fv $ arg), (fv $ arg2))); |
|
241 fun fv_rsp_arg_bn ((arg, arg2), l) = |
|
242 map (mk_fv_rsp_bn arg arg2) l; |
|
243 val bn_eqs = flat (map fv_rsp_arg_bn ((args ~~ args2) ~~ ls)); |
|
244 val (_, add_alphas) = chop (length (nobn_eqs @ bn_eqs)) all_alphas; |
|
245 val atys = map (domain_type o fastype_of) add_alphas; |
|
246 val anames = Name.variant_list (names @ names2) (Datatype_Prop.make_tnames atys); |
|
247 val aargs = map Free (anames ~~ atys); |
|
248 val aeqs = map2 (fn alpha => fn arg => HOLogic.mk_imp (alpha $ arg $ arg, @{term True})) |
|
249 add_alphas aargs; |
|
250 val eq = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (nobn_eqs @ bn_eqs @ aeqs)); |
|
251 val th = Goal.prove ctxt (names @ names2) [] eq tac; |
|
252 val ths = HOLogic.conj_elims th; |
|
253 val (ths_nobn, ths_bn) = chop (length ls) ths; |
|
254 fun project (th, l) = |
|
255 Project_Rule.projects ctxt (1 upto (length l + 1)) (hd (Project_Rule.projections ctxt th)) |
|
256 val ths_nobn_pr = map project (ths_nobn ~~ ls); |
|
257 in |
|
258 (flat ths_nobn_pr @ ths_bn) |
|
259 end |
|
260 *} |
|
261 |
|
262 |
|
263 end |