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 |
229 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
232 val (_, lthy') = Function.add_function all_fun_names all_fun_eqs |
230 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
233 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
231 |
234 |
232 val (info, lthy'') = prove_termination (Local_Theory.restore lthy') |
235 val (info, lthy'') = prove_termination (Local_Theory.restore lthy') |
233 |
236 |
253 in |
256 in |
254 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
257 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
255 end |
258 end |
256 |
259 |
257 fun raw_prove_eqvt consts ind_thms simps ctxt = |
260 fun raw_prove_eqvt consts ind_thms simps ctxt = |
258 let |
261 if null consts then [] |
259 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt |
262 else |
260 val p = Free (p, @{typ perm}) |
263 let |
261 val arg_tys = |
264 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt |
262 consts |
265 val p = Free (p, @{typ perm}) |
263 |> map fastype_of |
266 val arg_tys = |
264 |> map domain_type |
267 consts |
265 val (arg_names, ctxt'') = Variable.variant_fixes (replicate (length arg_tys) "") ctxt' |
268 |> map fastype_of |
266 val args = map Free (arg_names ~~ arg_tys) |
269 |> map domain_type |
267 val goals = map2 (mk_eqvt_goal p) consts args |
270 val (arg_names, ctxt'') = Variable.variant_fixes (replicate (length arg_tys) "") ctxt' |
268 val insts = map (single o SOME) arg_names |
271 val args = map Free (arg_names ~~ arg_tys) |
269 val const_names = map (fst o dest_Const) consts |
272 val goals = map2 (mk_eqvt_goal p) consts args |
270 fun tac ctxt = |
273 val insts = map (single o SOME) arg_names |
271 Object_Logic.full_atomize_tac |
274 val const_names = map (fst o dest_Const) consts |
272 THEN' InductTacs.induct_rules_tac ctxt insts ind_thms |
275 fun tac ctxt = |
273 THEN_ALL_NEW |
276 Object_Logic.full_atomize_tac |
274 (asm_full_simp_tac (HOL_basic_ss addsimps simps) |
277 THEN' InductTacs.induct_rules_tac ctxt insts ind_thms |
275 THEN' Nominal_Permeq.eqvt_tac ctxt simps const_names |
278 THEN_ALL_NEW |
276 THEN' asm_simp_tac HOL_basic_ss) |
279 (asm_full_simp_tac (HOL_basic_ss addsimps simps) |
277 in |
280 THEN' Nominal_Permeq.eqvt_tac ctxt simps const_names |
278 Goal.prove_multi ctxt' [] [] goals (fn {context, ...} => (HEADGOAL (tac context))) |
281 THEN' asm_simp_tac HOL_basic_ss) |
279 |> ProofContext.export ctxt'' ctxt |
282 in |
280 end |
283 Goal.prove_multi ctxt' [] [] goals (fn {context, ...} => (HEADGOAL (tac context))) |
|
284 |> ProofContext.export ctxt'' ctxt |
|
285 end |
281 |
286 |
282 end (* structure *) |
287 end (* structure *) |
283 |
288 |