28 val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> |
28 val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> |
29 term list -> thm -> thm list -> Proof.context -> thm list |
29 term list -> thm -> thm list -> Proof.context -> thm list |
30 val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list |
30 val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list |
31 val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list |
31 val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list |
32 |
32 |
33 val resolve_fun_rel: thm -> thm |
33 val mk_funs_rsp: thm -> thm |
|
34 val mk_alpha_permute_rsp: thm -> thm |
34 end |
35 end |
35 |
36 |
36 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
37 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
37 struct |
38 struct |
38 |
39 |
557 end |
558 end |
558 |
559 |
559 |
560 |
560 (** proves the equivp predicate for all alphas **) |
561 (** proves the equivp predicate for all alphas **) |
561 |
562 |
562 val equivp_intro = |
563 val transp_def' = |
563 @{lemma "[|!x. R x x; !x y. R x y --> R y x; !x y. R x y --> (!z. R y z --> R x z)|] ==> equivp R" |
564 @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" |
564 by (rule equivpI, unfold reflp_def symp_def transp_def, blast+)} |
565 by (rule eq_reflection, auto simp add: transp_def)} |
565 |
566 |
566 fun raw_prove_equivp alphas refl symm trans ctxt = |
567 fun raw_prove_equivp alphas refl symm trans ctxt = |
567 let |
568 let |
568 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars |
569 val refl' = map (fold_rule @{thms reflp_def} o atomize) refl |
569 val refl' = map atomize refl |
570 val symm' = map (fold_rule @{thms symp_def} o atomize) symm |
570 val symm' = map atomize symm |
571 val trans' = map (fold_rule [transp_def'] o atomize) trans |
571 val trans' = map atomize trans |
572 |
572 fun prep_goal t = |
573 fun prep_goal t = |
573 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) |
574 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) |
574 in |
575 in |
575 Goal.prove_multi ctxt [] [] (map prep_goal alphas) |
576 Goal.prove_multi ctxt [] [] (map prep_goal alphas) |
576 (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac equivp_intro THEN' |
577 (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' |
577 RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans'])))) |
578 RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans'])))) |
578 end |
579 end |
579 |
580 |
580 |
581 |
581 (* proves that alpha_raw implies alpha_bn *) |
582 (* proves that alpha_raw implies alpha_bn *) |
611 |
612 |
612 fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt = |
613 fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt = |
613 let |
614 let |
614 val arg_ty = domain_type o fastype_of |
615 val arg_ty = domain_type o fastype_of |
615 val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms |
616 val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms |
616 |
617 fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y) |
617 val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) fvs |
618 |
618 val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) bns |
619 val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs |
619 val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => HOLogic.mk_eq (t2 $ x, t2 $ y))) alpha_bn_trms fv_bns |
620 val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns) |
|
621 val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns |
620 |
622 |
621 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} |
623 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} |
622 @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) |
624 @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) |
623 in |
625 in |
624 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct |
626 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct |
688 (K (HEADGOAL |
690 (K (HEADGOAL |
689 (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps))) |
691 (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps))) |
690 end |
692 end |
691 |
693 |
692 |
694 |
693 (* resolve with @{thm fun_relI} *) |
695 (* transformation of the natural rsp-lemmas into the standard form *) |
694 |
696 |
695 fun resolve_fun_rel thm = |
697 val fun_rsp = @{lemma |
696 let |
698 "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp} |
697 val fun_rel = @{thm fun_relI} |
699 |
698 val thm' = forall_intr_vars thm |
700 fun mk_funs_rsp thm = |
699 val cinsts = Thm.match (cprem_of fun_rel 1, cprop_of thm') |
701 thm |
700 val fun_rel' = Thm.instantiate cinsts fun_rel |
702 |> atomize |
701 in |
703 |> single |
702 thm' COMP fun_rel' |
704 |> curry (op OF) fun_rsp |
703 end |
705 |
|
706 |
|
707 val permute_rsp = @{lemma |
|
708 "(!x y p. R x y --> R (permute p x) (permute p y)) |
|
709 ==> ((op =) ===> R ===> R) permute permute" by simp} |
|
710 |
|
711 fun mk_alpha_permute_rsp thm = |
|
712 thm |
|
713 |> atomize |
|
714 |> single |
|
715 |> curry (op OF) permute_rsp |
|
716 |
704 |
717 |
705 |
718 |
706 end (* structure *) |
719 end (* structure *) |
707 |
720 |