382 cases=cases, termination=mtermination, |
384 cases=cases, termination=mtermination, |
383 domintros=mdomintros, eqvts=meqvt_funs } |
385 domintros=mdomintros, eqvts=meqvt_funs } |
384 end |
386 end |
385 |
387 |
386 (* nominal *) |
388 (* nominal *) |
|
389 fun subst_all s (Q $ Abs(_, _, t)) = |
|
390 let |
|
391 val vs = map Free (Term.add_frees s []) |
|
392 in |
|
393 fold Logic.all vs (subst_bound (s, t)) |
|
394 end |
|
395 |
|
396 fun mk_comp_dummy t s = Const (@{const_name comp}, dummyT) $ t $ s |
|
397 |
|
398 fun all v t = |
|
399 let |
|
400 val T = Term.fastype_of v |
|
401 in |
|
402 Logic.all_const T $ absdummy T (abstract_over (v, t)) |
|
403 end |
|
404 |
|
405 (* nominal *) |
387 fun prepare_nominal_function_mutual config defname fixes eqss lthy = |
406 fun prepare_nominal_function_mutual config defname fixes eqss lthy = |
388 let |
407 let |
389 val mutual as Mutual {fsum_var=(n, T), qglrs, ...} = |
408 val mutual as Mutual {fsum_var=(n, T), qglrs, ...} = |
390 analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss) |
409 analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss) |
391 |
410 |
392 val ((fsum, goalstate, cont), lthy') = |
411 val ((fsum, G, GIntro_thms, G_induct, goalstate, cont), lthy') = |
393 Nominal_Function_Core.prepare_nominal_function config defname [((n, T), NoSyn)] qglrs lthy |
412 Nominal_Function_Core.prepare_nominal_function config defname [((n, T), NoSyn)] qglrs lthy |
394 |
413 |
395 val (mutual', lthy'') = define_projections fixes mutual fsum lthy' |
414 val (mutual' as Mutual {n', parts, ST, RST, ...}, lthy'') = define_projections fixes mutual fsum lthy' |
396 |
415 |
397 val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual' |
416 val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual' |
398 in |
417 |
399 ((goalstate, mutual_cont), lthy'') |
418 (* XXX *) |
|
419 |
|
420 (* defining the auxiliary graph *) |
|
421 fun mk_cases (MutualPart {i', fvar as (n, T), ...}) = |
|
422 let |
|
423 val (tys, ty) = strip_type T |
|
424 val fun_var = Free (n ^ "_aux", HOLogic.mk_tupleT tys --> ty) |
|
425 val inj_fun = absdummy dummyT (SumTree.mk_inj RST n' i' (Bound 0)) |
|
426 in |
|
427 Syntax.check_term lthy'' (mk_comp_dummy inj_fun fun_var) |
|
428 end |
|
429 |
|
430 val sum_case_exp = map mk_cases parts |
|
431 |> SumTree.mk_sumcases RST |
|
432 |
|
433 val (G_name, G_type) = dest_Free G |
|
434 val G_name_aux = G_name ^ "_aux" |
|
435 val subst = [(G, Free (G_name_aux, G_type))] |
|
436 val GIntros_aux = GIntro_thms |
|
437 |> map prop_of |
|
438 |> map (Term.subst_free subst) |
|
439 |> map (subst_all sum_case_exp) |
|
440 |
|
441 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'' |
|
443 |
|
444 (* proof of equivalence between graph and auxiliary graph *) |
|
445 val x = Var(("x", 0), ST) |
|
446 val y = Var(("y", 1), RST) |
|
447 val G_aux_prem = HOLogic.mk_Trueprop (G_aux $ x $ y) |
|
448 val G_prem = HOLogic.mk_Trueprop (G $ x $ y) |
|
449 |
|
450 fun mk_inj_goal (MutualPart {i', ...}) = |
|
451 let |
|
452 val injs = SumTree.mk_inj ST n' i' (Bound 0) |
|
453 val projs = y |
|
454 |> SumTree.mk_proj RST n' i' |
|
455 |> SumTree.mk_inj RST n' i' |
|
456 in |
|
457 Const (@{const_name "All"}, dummyT) $ absdummy dummyT |
|
458 (HOLogic.mk_imp (HOLogic.mk_eq(x, injs), HOLogic.mk_eq(projs, y))) |
|
459 end |
|
460 |
|
461 val goal_inj = Logic.mk_implies (G_aux_prem, |
|
462 HOLogic.mk_Trueprop (fold_conj (map mk_inj_goal parts))) |
|
463 |> all x |> all y |
|
464 |> Syntax.check_term lthy''' |
|
465 val goal_iff1 = Logic.mk_implies (G_aux_prem, G_prem) |
|
466 |> all x |> all y |
|
467 val goal_iff2 = Logic.mk_implies (G_prem, G_aux_prem) |
|
468 |> all x |> all y |
|
469 |
|
470 val simp_thms = @{thms Projl.simps Projr.simps sum.inject sum.cases sum.distinct o_apply} |
|
471 val ss0 = HOL_basic_ss addsimps simp_thms |
|
472 val ss1 = HOL_ss addsimps simp_thms |
|
473 |
|
474 val inj_thm = Goal.prove lthy''' [] [] goal_inj |
|
475 (K (HEADGOAL (DETERM o etac G_aux_induct THEN_ALL_NEW asm_simp_tac ss1))) |
|
476 |
|
477 fun aux_tac thm = |
|
478 rtac (Drule.gen_all thm) THEN_ALL_NEW (asm_full_simp_tac (ss1 addsimps [inj_thm])) |
|
479 |
|
480 val iff1_thm = Goal.prove lthy''' [] [] goal_iff1 |
|
481 (K (HEADGOAL (DETERM o etac G_aux_induct THEN' RANGE (map aux_tac GIntro_thms)))) |
|
482 |> Drule.gen_all |
|
483 val iff2_thm = Goal.prove lthy''' [] [] goal_iff2 |
|
484 (K (HEADGOAL (DETERM o etac G_induct THEN' RANGE (map (aux_tac o simplify ss0) GIntro_aux_thms)))) |
|
485 |> Drule.gen_all |
|
486 |
|
487 val iff_thm = Goal.prove lthy''' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (G, G_aux))) |
|
488 (K (HEADGOAL (EVERY' ((map rtac @{thms ext ext iffI}) @ [etac iff2_thm, etac iff1_thm])))) |
|
489 |
|
490 val tac = HEADGOAL (simp_tac (HOL_basic_ss addsimps [iff_thm])) |
|
491 val goalstate' = |
|
492 case (SINGLE tac) goalstate of |
|
493 NONE => error "auxiliary equivalence proof failed" |
|
494 | SOME st => st |
|
495 in |
|
496 ((goalstate', mutual_cont), lthy''') |
400 end |
497 end |
401 |
498 |
402 end |
499 end |