equal
deleted
inserted
replaced
26 val raw_prove_equivp: term list -> thm list -> thm list -> thm list -> Proof.context -> thm list |
26 val raw_prove_equivp: term list -> thm list -> thm list -> thm list -> Proof.context -> thm list |
27 val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
27 val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
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 |
|
32 val resolve_fun_rel: thm -> thm |
31 end |
33 end |
32 |
34 |
33 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
35 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
34 struct |
36 struct |
35 |
37 |
602 alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_induct |
604 alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_induct |
603 (raw_prove_bn_imp_tac alpha_names alpha_intros) ctxt |
605 (raw_prove_bn_imp_tac alpha_names alpha_intros) ctxt |
604 end |
606 end |
605 |
607 |
606 |
608 |
607 (* helper lemmas for respectfulness for fv_raw / bn_raw *) |
609 (* respectfulness for fv_raw / bn_raw *) |
608 |
610 |
609 fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt = |
611 fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt = |
610 let |
612 let |
611 val arg_ty = domain_type o fastype_of |
613 val arg_ty = domain_type o fastype_of |
612 val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms |
614 val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms |
620 in |
622 in |
621 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct |
623 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct |
622 (K (asm_full_simp_tac ss)) ctxt |
624 (K (asm_full_simp_tac ss)) ctxt |
623 end |
625 end |
624 |
626 |
625 (* helper lemmas for respectfulness for size *) |
627 (* respectfulness for size *) |
626 |
628 |
627 fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt = |
629 fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt = |
628 let |
630 let |
629 val arg_tys = map (domain_type o fastype_of) all_alpha_trms |
631 val arg_tys = map (domain_type o fastype_of) all_alpha_trms |
630 |
632 |
639 val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss |
641 val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss |
640 in |
642 in |
641 alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt |
643 alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt |
642 end |
644 end |
643 |
645 |
|
646 |
|
647 (* resolve with @{thm fun_relI} *) |
|
648 |
|
649 fun resolve_fun_rel thm = |
|
650 let |
|
651 val fun_rel = @{thm fun_relI} |
|
652 val thm' = forall_intr_vars thm |
|
653 val cinsts = Thm.match (cprem_of fun_rel 1, cprop_of thm') |
|
654 val fun_rel' = Thm.instantiate cinsts fun_rel |
|
655 in |
|
656 thm' COMP fun_rel' |
|
657 end |
|
658 |
|
659 |
644 end (* structure *) |
660 end (* structure *) |
645 |
661 |