17 -> string (* defname *) |
17 -> string (* defname *) |
18 -> ((string * typ) * mixfix) list |
18 -> ((string * typ) * mixfix) list |
19 -> term list |
19 -> term list |
20 -> local_theory |
20 -> local_theory |
21 -> ((thm (* goalstate *) |
21 -> ((thm (* goalstate *) |
22 * (thm -> Nominal_Function_Common.nominal_function_result) (* proof continuation *) |
22 * (Proof.context -> thm -> Nominal_Function_Common.nominal_function_result) (* proof continuation *) |
23 ) * local_theory) |
23 ) * local_theory) |
24 end |
24 end |
25 |
25 |
26 structure Nominal_Function_Mutual: NOMINAL_FUNCTION_MUTUAL = |
26 structure Nominal_Function_Mutual: NOMINAL_FUNCTION_MUTUAL = |
27 struct |
27 struct |
328 val goal = fold_conj_balanced (map2 mk_goal acc_prems (fs ~~ argss)) |
328 val goal = fold_conj_balanced (map2 mk_goal acc_prems (fs ~~ argss)) |
329 |> HOLogic.mk_Trueprop |
329 |> HOLogic.mk_Trueprop |
330 |
330 |
331 val induct_thm = case induct_thms of |
331 val induct_thm = case induct_thms of |
332 [thm] => thm |
332 [thm] => thm |
333 |> Drule.gen_all (Variable.maxidx_of ctxt') |
333 |> Variable.gen_all ctxt' |
334 |> Thm.permute_prems 0 1 |
334 |> Thm.permute_prems 0 1 |
335 |> (fn thm => atomize_rule ctxt' (length (Thm.prems_of thm) - 1) thm) |
335 |> (fn thm => atomize_rule ctxt' (length (Thm.prems_of thm) - 1) thm) |
336 | thms => thms |
336 | thms => thms |
337 |> map (Drule.gen_all (Variable.maxidx_of ctxt')) |
337 |> map (Variable.gen_all ctxt') |
338 |> map (Rule_Cases.add_consumes 1) |
338 |> map (Rule_Cases.add_consumes 1) |
339 |> snd o Rule_Cases.strict_mutual_rule ctxt' |
339 |> snd o Rule_Cases.strict_mutual_rule ctxt' |
340 |> atomize_concl ctxt' |
340 |> atomize_concl ctxt' |
341 |
341 |
342 fun tac ctxt thm = |
342 fun tac ctxt thm = |
343 rtac (Drule.gen_all (Variable.maxidx_of ctxt) thm) THEN_ALL_NEW assume_tac ctxt |
343 resolve_tac ctxt [Variable.gen_all ctxt thm] |
|
344 THEN_ALL_NEW assume_tac ctxt |
344 in |
345 in |
345 Goal.prove ctxt' (flat arg_namess) [] goal |
346 Goal.prove ctxt' (flat arg_namess) [] goal |
346 (fn {context = ctxt'', ...} => |
347 (fn {context = ctxt'', ...} => |
347 HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map (tac ctxt'') eqvts_thms))) |
348 HEADGOAL (DETERM o (resolve_tac ctxt'' [induct_thm]) THEN' |
|
349 RANGE (map (tac ctxt'') eqvts_thms))) |
348 |> singleton (Proof_Context.export ctxt' ctxt) |
350 |> singleton (Proof_Context.export ctxt' ctxt) |
349 |> split_conj_thm |
351 |> split_conj_thm |
350 |> map (fn th => th RS mp) |
352 |> map (fn th => th RS mp) |
351 end |
353 end |
352 |
354 |
439 |> map (subst_all case_sum_exp) |
441 |> map (subst_all case_sum_exp) |
440 |
442 |
441 val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy''') = |
443 val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy''') = |
442 Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy'' |
444 Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy'' |
443 |
445 |
444 val mutual_cont = mk_partial_rules_mutual lthy''' cont mutual' |
446 fun mutual_cont ctxt = mk_partial_rules_mutual lthy''' (cont ctxt) mutual' |
445 |
447 |
446 (* proof of equivalence between graph and auxiliary graph *) |
448 (* proof of equivalence between graph and auxiliary graph *) |
447 val x = Var(("x", 0), ST) |
449 val x = Var(("x", 0), ST) |
448 val y = Var(("y", 1), RST) |
450 val y = Var(("y", 1), RST) |
449 val G_aux_prem = HOLogic.mk_Trueprop (G_aux $ x $ y) |
451 val G_aux_prem = HOLogic.mk_Trueprop (G_aux $ x $ y) |
472 val simp_thms = @{thms sum.sel sum.inject sum.case sum.distinct o_apply} |
474 val simp_thms = @{thms sum.sel sum.inject sum.case sum.distinct o_apply} |
473 val simpset0 = put_simpset HOL_basic_ss lthy''' addsimps simp_thms |
475 val simpset0 = put_simpset HOL_basic_ss lthy''' addsimps simp_thms |
474 val simpset1 = put_simpset HOL_ss lthy''' addsimps simp_thms |
476 val simpset1 = put_simpset HOL_ss lthy''' addsimps simp_thms |
475 |
477 |
476 val inj_thm = Goal.prove lthy''' [] [] goal_inj |
478 val inj_thm = Goal.prove lthy''' [] [] goal_inj |
477 (K (HEADGOAL (DETERM o etac G_aux_induct THEN_ALL_NEW asm_simp_tac simpset1))) |
479 (K (HEADGOAL (DETERM o eresolve_tac lthy''' [G_aux_induct] |
|
480 THEN_ALL_NEW asm_simp_tac simpset1))) |
478 |
481 |
479 fun aux_tac thm = |
482 fun aux_tac thm = |
480 rtac (Drule.gen_all (Variable.maxidx_of lthy''') thm) THEN_ALL_NEW |
483 resolve_tac lthy''' [Variable.gen_all lthy''' thm] THEN_ALL_NEW |
481 asm_full_simp_tac (simpset1 addsimps [inj_thm]) |
484 asm_full_simp_tac (simpset1 addsimps [inj_thm]) |
482 |
485 |
483 val iff1_thm = Goal.prove lthy''' [] [] goal_iff1 |
486 val iff1_thm = Goal.prove lthy''' [] [] goal_iff1 |
484 (K (HEADGOAL (DETERM o etac G_aux_induct THEN' RANGE (map aux_tac GIntro_thms)))) |
487 (K (HEADGOAL (DETERM o eresolve_tac lthy''' [G_aux_induct] |
485 |> Drule.gen_all (Variable.maxidx_of lthy''') |
488 THEN' RANGE (map aux_tac GIntro_thms)))) |
|
489 |> Variable.gen_all lthy''' |
486 val iff2_thm = Goal.prove lthy''' [] [] goal_iff2 |
490 val iff2_thm = Goal.prove lthy''' [] [] goal_iff2 |
487 (K (HEADGOAL (DETERM o etac G_induct THEN' RANGE |
491 (K (HEADGOAL (DETERM o eresolve_tac lthy''' [G_induct] THEN' RANGE |
488 (map (aux_tac o simplify simpset0) GIntro_aux_thms)))) |
492 (map (aux_tac o simplify simpset0) GIntro_aux_thms)))) |
489 |> Drule.gen_all (Variable.maxidx_of lthy''') |
493 |> Variable.gen_all lthy''' |
490 |
494 |
491 val iff_thm = Goal.prove lthy''' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (G, G_aux))) |
495 val iff_thm = Goal.prove lthy''' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (G, G_aux))) |
492 (K (HEADGOAL (EVERY' ((map rtac @{thms ext ext iffI}) @ [etac iff2_thm, etac iff1_thm])))) |
496 (K (HEADGOAL (EVERY' ((map (resolve_tac lthy''' o single) @{thms ext ext iffI}) @ |
|
497 [eresolve_tac lthy''' [iff2_thm], eresolve_tac lthy''' [iff1_thm]])))) |
493 |
498 |
494 val tac = HEADGOAL (simp_tac (put_simpset HOL_basic_ss lthy''' addsimps [iff_thm])) |
499 val tac = HEADGOAL (simp_tac (put_simpset HOL_basic_ss lthy''' addsimps [iff_thm])) |
495 val goalstate' = |
500 val goalstate' = |
496 case (SINGLE tac) goalstate of |
501 case (SINGLE tac) goalstate of |
497 NONE => error "auxiliary equivalence proof failed" |
502 NONE => error "auxiliary equivalence proof failed" |