224 val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_info |
224 val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_info |
225 |
225 |
226 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
226 val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) |
227 val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
227 val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) |
228 |
228 |
229 val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) ((flat fv_eqs) @ (flat fv_bn_eqs)))) |
|
230 |
|
231 |
|
232 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
229 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
233 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
230 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
234 |
231 |
235 val (info, lthy'') = prove_termination (Local_Theory.restore lthy') |
232 val (info, lthy'') = prove_termination (Local_Theory.restore lthy') |
236 |
233 |
254 val lhs = mk_perm pi (const $ arg) |
251 val lhs = mk_perm pi (const $ arg) |
255 val rhs = const $ (mk_perm pi arg) |
252 val rhs = const $ (mk_perm pi arg) |
256 in |
253 in |
257 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
254 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
258 end |
255 end |
|
256 |
|
257 fun subproof_tac const_names simps ctxt = |
|
258 Subgoal.FOCUS (fn {prems, context, ...} => |
|
259 HEADGOAL |
|
260 (simp_tac (HOL_basic_ss addsimps simps) |
|
261 THEN' Nominal_Permeq.eqvt_tac context [] const_names |
|
262 THEN' simp_tac (HOL_basic_ss addsimps (@{thms eqvt_apply[symmetric]} @ prems)))) ctxt |
259 |
263 |
260 fun raw_prove_eqvt consts ind_thms simps ctxt = |
264 fun raw_prove_eqvt consts ind_thms simps ctxt = |
261 if null consts then [] |
265 if null consts then [] |
262 else |
266 else |
263 let |
267 let |
265 val p = Free (p, @{typ perm}) |
269 val p = Free (p, @{typ perm}) |
266 val arg_tys = |
270 val arg_tys = |
267 consts |
271 consts |
268 |> map fastype_of |
272 |> map fastype_of |
269 |> map domain_type |
273 |> map domain_type |
270 val (arg_names, ctxt'') = Variable.variant_fixes (replicate (length arg_tys) "") ctxt' |
274 val (arg_names, ctxt'') = Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt' |
271 val args = map Free (arg_names ~~ arg_tys) |
275 val args = map Free (arg_names ~~ arg_tys) |
272 val goals = map2 (mk_eqvt_goal p) consts args |
276 val goals = map2 (mk_eqvt_goal p) consts args |
273 val insts = map (single o SOME) arg_names |
277 val insts = map (single o SOME) arg_names |
274 val const_names = map (fst o dest_Const) consts |
278 val const_names = map (fst o dest_Const) consts |
|
279 |
275 fun tac ctxt = |
280 fun tac ctxt = |
276 Object_Logic.full_atomize_tac |
281 Object_Logic.full_atomize_tac |
277 THEN' InductTacs.induct_rules_tac ctxt insts ind_thms |
282 THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms)) |
278 THEN_ALL_NEW |
283 THEN_ALL_NEW subproof_tac const_names simps ctxt |
279 (asm_full_simp_tac (HOL_basic_ss addsimps simps) |
|
280 THEN' Nominal_Permeq.eqvt_tac ctxt simps const_names |
|
281 THEN' asm_simp_tac HOL_basic_ss) |
|
282 in |
284 in |
283 Goal.prove_multi ctxt' [] [] goals (fn {context, ...} => (HEADGOAL (tac context))) |
285 Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => (HEADGOAL (tac context))) |
284 |> ProofContext.export ctxt'' ctxt |
286 |> ProofContext.export ctxt'' ctxt |
285 end |
287 end |
286 |
288 |
287 end (* structure *) |
289 end (* structure *) |
288 |
290 |