equal
deleted
inserted
replaced
259 |
259 |
260 val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') |
260 val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') |
261 |
261 |
262 val {fs, simps, inducts, ...} = info; |
262 val {fs, simps, inducts, ...} = info; |
263 |
263 |
264 val morphism = ProofContext.export_morphism lthy'' lthy |
264 val morphism = Proof_Context.export_morphism lthy'' lthy |
265 val simps_exp = map (Morphism.thm morphism) (the simps) |
265 val simps_exp = map (Morphism.thm morphism) (the simps) |
266 val inducts_exp = map (Morphism.thm morphism) (the inducts) |
266 val inducts_exp = map (Morphism.thm morphism) (the inducts) |
267 |
267 |
268 val (fvs', fv_bns') = chop (length fv_frees) fs |
268 val (fvs', fv_bns') = chop (length fv_frees) fs |
269 |
269 |
332 |
332 |
333 val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') |
333 val (info, lthy'') = prove_termination_fun raw_size_thms (Local_Theory.restore lthy') |
334 |
334 |
335 val {fs, simps, ...} = info; |
335 val {fs, simps, ...} = info; |
336 |
336 |
337 val morphism = ProofContext.export_morphism lthy'' lthy |
337 val morphism = Proof_Context.export_morphism lthy'' lthy |
338 val simps_exp = map (Morphism.thm morphism) (the simps) |
338 val simps_exp = map (Morphism.thm morphism) (the simps) |
339 in |
339 in |
340 (fs, simps_exp, lthy'') |
340 (fs, simps_exp, lthy'') |
341 end |
341 end |
342 |
342 |
465 THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym])))) |
465 THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym])))) |
466 |
466 |
467 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = |
467 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = |
468 HEADGOAL |
468 HEADGOAL |
469 (Object_Logic.full_atomize_tac |
469 (Object_Logic.full_atomize_tac |
470 THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms)) |
470 THEN' (DETERM o (Induct_Tacs.induct_rules_tac ctxt insts ind_thms)) |
471 THEN_ALL_NEW subproof_tac const_names simps ctxt) |
471 THEN_ALL_NEW subproof_tac const_names simps ctxt) |
472 |
472 |
473 fun mk_eqvt_goal pi const arg = |
473 fun mk_eqvt_goal pi const arg = |
474 let |
474 let |
475 val lhs = mk_perm pi (const $ arg) |
475 val lhs = mk_perm pi (const $ arg) |
496 val insts = map (single o SOME) arg_names |
496 val insts = map (single o SOME) arg_names |
497 val const_names = map (fst o dest_Const) consts |
497 val const_names = map (fst o dest_Const) consts |
498 in |
498 in |
499 Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => |
499 Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => |
500 prove_eqvt_tac insts ind_thms const_names simps context) |
500 prove_eqvt_tac insts ind_thms const_names simps context) |
501 |> ProofContext.export ctxt'' ctxt |
501 |> Proof_Context.export ctxt'' ctxt |
502 end |
502 end |
503 |
503 |
504 |
504 |
505 end (* structure *) |
505 end (* structure *) |
506 |
506 |