416 val ((fsum, G, GIntro_thms, G_induct, goalstate, cont), lthy') = |
416 val ((fsum, G, GIntro_thms, G_induct, goalstate, cont), lthy') = |
417 Nominal_Function_Core.prepare_nominal_function config defname [((n, T), NoSyn)] qglrs lthy |
417 Nominal_Function_Core.prepare_nominal_function config defname [((n, T), NoSyn)] qglrs lthy |
418 |
418 |
419 val (mutual' as Mutual {n', parts, ST, RST, ...}, lthy'') = define_projections fixes mutual fsum lthy' |
419 val (mutual' as Mutual {n', parts, ST, RST, ...}, lthy'') = define_projections fixes mutual fsum lthy' |
420 |
420 |
421 val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual' |
|
422 |
|
423 (* XXX *) |
|
424 |
|
425 (* defining the auxiliary graph *) |
421 (* defining the auxiliary graph *) |
426 fun mk_cases (MutualPart {i', fvar as (n, T), ...}) = |
422 fun mk_cases (MutualPart {i', fvar as (n, T), ...}) = |
427 let |
423 let |
428 val (tys, ty) = strip_type T |
424 val (tys, ty) = strip_type T |
429 val fun_var = Free (n ^ "_aux", HOLogic.mk_tupleT tys --> ty) |
425 val fun_var = Free (n ^ "_aux", HOLogic.mk_tupleT tys --> ty) |
444 |> map (subst_all sum_case_exp) |
440 |> map (subst_all sum_case_exp) |
445 |
441 |
446 val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy''') = |
442 val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy''') = |
447 Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy'' |
443 Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy'' |
448 |
444 |
|
445 val mutual_cont = mk_partial_rules_mutual lthy''' cont mutual' |
|
446 |
449 (* proof of equivalence between graph and auxiliary graph *) |
447 (* proof of equivalence between graph and auxiliary graph *) |
450 val x = Var(("x", 0), ST) |
448 val x = Var(("x", 0), ST) |
451 val y = Var(("y", 1), RST) |
449 val y = Var(("y", 1), RST) |
452 val G_aux_prem = HOLogic.mk_Trueprop (G_aux $ x $ y) |
450 val G_aux_prem = HOLogic.mk_Trueprop (G_aux $ x $ y) |
453 val G_prem = HOLogic.mk_Trueprop (G $ x $ y) |
451 val G_prem = HOLogic.mk_Trueprop (G $ x $ y) |