389 Const (lookup ty_trm_assoc ty_str, ty_eq) $ lhs $ rhs |
389 Const (lookup ty_trm_assoc ty_str, ty_eq) $ lhs $ rhs |
390 |> HOLogic.mk_not |
390 |> HOLogic.mk_not |
391 |> HOLogic.mk_Trueprop |
391 |> HOLogic.mk_Trueprop |
392 end |
392 end |
393 |
393 |
394 fun distinct_tac cases_thms distinct_thms = |
394 fun distinct_tac ctxt cases_thms distinct_thms = |
395 rtac notI THEN' eresolve_tac cases_thms |
395 rtac notI THEN' eresolve_tac cases_thms |
396 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
396 THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps distinct_thms) |
397 |
397 |
398 fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info = |
398 fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info = |
399 let |
399 let |
400 val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result |
400 val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result |
401 val RawDtInfo {raw_dt_names, raw_distinct_thms, ...} = raw_dt_info |
401 val RawDtInfo {raw_dt_names, raw_distinct_thms, ...} = raw_dt_info |
405 fun mk_alpha_distinct raw_distinct_trm = |
405 fun mk_alpha_distinct raw_distinct_trm = |
406 let |
406 let |
407 val goal = mk_distinct_goal ty_trm_assoc raw_distinct_trm |
407 val goal = mk_distinct_goal ty_trm_assoc raw_distinct_trm |
408 in |
408 in |
409 Goal.prove ctxt [] [] goal |
409 Goal.prove ctxt [] [] goal |
410 (K (distinct_tac alpha_cases raw_distinct_thms 1)) |
410 (K (distinct_tac ctxt alpha_cases raw_distinct_thms 1)) |
411 end |
411 end |
412 in |
412 in |
413 map (mk_alpha_distinct o prop_of) raw_distinct_thms |
413 map (mk_alpha_distinct o prop_of) raw_distinct_thms |
414 end |
414 end |
415 |
415 |
423 fun mk_simp_rule thm = |
423 fun mk_simp_rule thm = |
424 case (prop_of thm) of |
424 case (prop_of thm) of |
425 @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI} |
425 @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI} |
426 | _ => thm |
426 | _ => thm |
427 |
427 |
428 fun alpha_eq_iff_tac dist_inj intros elims = |
428 fun alpha_eq_iff_tac ctxt dist_inj intros elims = |
429 SOLVED' (asm_full_simp_tac (HOL_ss addsimps intros)) ORELSE' |
429 SOLVED' (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)) ORELSE' |
430 (rtac @{thm iffI} THEN' |
430 (rtac @{thm iffI} THEN' |
431 RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps dist_inj), |
431 RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj), |
432 asm_full_simp_tac (HOL_ss addsimps intros)]) |
432 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)]) |
433 |
433 |
434 fun mk_alpha_eq_iff_goal thm = |
434 fun mk_alpha_eq_iff_goal thm = |
435 let |
435 let |
436 val prop = prop_of thm; |
436 val prop = prop_of thm; |
437 val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); |
437 val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); |
447 val AlphaResult {alpha_intros, alpha_cases, ...} = alpha_result |
447 val AlphaResult {alpha_intros, alpha_cases, ...} = alpha_result |
448 val RawDtInfo {raw_distinct_thms, raw_inject_thms, ...} = raw_dt_info |
448 val RawDtInfo {raw_distinct_thms, raw_inject_thms, ...} = raw_dt_info |
449 |
449 |
450 val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; |
450 val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; |
451 val goals = map mk_alpha_eq_iff_goal thms_imp; |
451 val goals = map mk_alpha_eq_iff_goal thms_imp; |
452 val tac = alpha_eq_iff_tac (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_cases 1; |
452 val tac = alpha_eq_iff_tac ctxt (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_cases 1; |
453 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |
453 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |
454 in |
454 in |
455 Variable.export ctxt' ctxt thms |
455 Variable.export ctxt' ctxt thms |
456 |> map mk_simp_rule |
456 |> map mk_simp_rule |
457 end |
457 end |
468 val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac |
468 val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac |
469 |
469 |
470 val bound_tac = |
470 val bound_tac = |
471 EVERY' [ rtac exi_zero, |
471 EVERY' [ rtac exi_zero, |
472 resolve_tac @{thms alpha_refl}, |
472 resolve_tac @{thms alpha_refl}, |
473 asm_full_simp_tac (HOL_ss addsimps prod_simps) ] |
473 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ] |
474 in |
474 in |
475 resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac] |
475 resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac] |
476 end |
476 end |
477 |
477 |
478 fun raw_prove_refl ctxt alpha_result raw_dt_induct = |
478 fun raw_prove_refl ctxt alpha_result raw_dt_induct = |
507 val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel_def alphas} |
507 val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel_def alphas} |
508 in |
508 in |
509 EVERY' |
509 EVERY' |
510 [ etac exi_neg, |
510 [ etac exi_neg, |
511 resolve_tac @{thms alpha_sym_eqvt}, |
511 resolve_tac @{thms alpha_sym_eqvt}, |
512 asm_full_simp_tac (HOL_ss addsimps prod_simps), |
512 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps), |
513 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, |
513 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, |
514 trans_prem_tac pred_names ctxt] |
514 trans_prem_tac pred_names ctxt] |
515 end |
515 end |
516 |
516 |
517 fun raw_prove_sym ctxt alpha_result alpha_eqvt = |
517 fun raw_prove_sym ctxt alpha_result alpha_eqvt = |
557 fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt = |
557 fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt = |
558 let |
558 let |
559 val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel_def} |
559 val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel_def} |
560 in |
560 in |
561 resolve_tac intros |
561 resolve_tac intros |
562 THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' |
562 THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN' |
563 TRY o EVERY' (* if binders are present *) |
563 TRY o EVERY' (* if binders are present *) |
564 [ etac @{thm exE}, |
564 [ etac @{thm exE}, |
565 etac @{thm exE}, |
565 etac @{thm exE}, |
566 perm_inst_tac ctxt, |
566 perm_inst_tac ctxt, |
567 resolve_tac @{thms alpha_trans_eqvt}, |
567 resolve_tac @{thms alpha_trans_eqvt}, |
568 atac, |
568 atac, |
569 aatac pred_names ctxt, |
569 aatac pred_names ctxt, |
570 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, |
570 eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, |
571 asm_full_simp_tac (HOL_ss addsimps prod_simps) ]) |
571 asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]) |
572 end |
572 end |
573 |
573 |
574 fun prove_trans_tac alpha_result raw_dt_thms alpha_eqvt ctxt = |
574 fun prove_trans_tac alpha_result raw_dt_thms alpha_eqvt ctxt = |
575 let |
575 let |
576 val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, alpha_cases, ...} = alpha_result |
576 val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, alpha_cases, ...} = alpha_result |
577 val alpha_names = alpha_names @ alpha_bn_names |
577 val alpha_names = alpha_names @ alpha_bn_names |
578 |
578 |
579 fun all_cases ctxt = |
579 fun all_cases ctxt = |
580 asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) |
580 asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps raw_dt_thms) |
581 THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt |
581 THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt |
582 in |
582 in |
583 EVERY' [ rtac @{thm allI}, rtac @{thm impI}, |
583 EVERY' [ rtac @{thm allI}, rtac @{thm impI}, |
584 ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ] |
584 ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ] |
585 end |
585 end |
682 |
682 |
683 val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs |
683 val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs |
684 val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns) |
684 val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns) |
685 val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns |
685 val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns |
686 |
686 |
687 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} |
687 val simpset = |
|
688 put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} |
688 @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) |
689 @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) |
689 in |
690 in |
690 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_raw_induct |
691 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_raw_induct |
691 (K (asm_full_simp_tac ss)) ctxt |
692 (K (asm_full_simp_tac simpset)) ctxt |
692 end |
693 end |
693 |
694 |
694 |
695 |
695 (* respectfulness for size *) |
696 (* respectfulness for size *) |
696 |
697 |
702 fun mk_prop ty (x, y) = HOLogic.mk_eq |
703 fun mk_prop ty (x, y) = HOLogic.mk_eq |
703 (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y) |
704 (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y) |
704 |
705 |
705 val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys)) |
706 val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys)) |
706 |
707 |
707 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def |
708 val simpset = |
|
709 put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def |
708 permute_prod_def prod.cases prod.recs}) |
710 permute_prod_def prod.cases prod.recs}) |
709 |
711 |
710 val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss |
712 val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac simpset |
711 in |
713 in |
712 alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt |
714 alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt |
713 end |
715 end |
714 |
716 |
715 |
717 |
716 (* respectfulness for constructors *) |
718 (* respectfulness for constructors *) |
717 |
719 |
718 fun raw_constr_rsp_tac alpha_intros simps = |
720 fun raw_constr_rsp_tac ctxt alpha_intros simps = |
719 let |
721 let |
720 val pre_ss = HOL_ss addsimps @{thms fun_rel_def} |
722 val pre_simpset = put_simpset HOL_ss ctxt addsimps @{thms fun_rel_def} |
721 val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel_def |
723 val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def prod_rel_def |
722 prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps |
724 prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps |
723 in |
725 in |
724 asm_full_simp_tac pre_ss |
726 asm_full_simp_tac pre_simpset |
725 THEN' REPEAT o (resolve_tac @{thms allI impI}) |
727 THEN' REPEAT o (resolve_tac @{thms allI impI}) |
726 THEN' resolve_tac alpha_intros |
728 THEN' resolve_tac alpha_intros |
727 THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss) |
729 THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_simpset) |
728 end |
730 end |
729 |
731 |
730 fun raw_constrs_rsp ctxt alpha_result constrs simps = |
732 fun raw_constrs_rsp ctxt alpha_result constrs simps = |
731 let |
733 let |
732 val AlphaResult {alpha_trms, alpha_tys, alpha_intros, ...} = alpha_result |
734 val AlphaResult {alpha_trms, alpha_tys, alpha_intros, ...} = alpha_result |
797 val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result |
799 val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result |
798 val prems' = flat (map Datatype_Aux.split_conj_thm prems) |
800 val prems' = flat (map Datatype_Aux.split_conj_thm prems) |
799 val prems'' = map (transform_prem1 context (alpha_names @ alpha_bn_names)) prems' |
801 val prems'' = map (transform_prem1 context (alpha_names @ alpha_bn_names)) prems' |
800 in |
802 in |
801 HEADGOAL |
803 HEADGOAL |
802 (simp_tac (HOL_basic_ss addsimps (simps @ prems')) |
804 (simp_tac (put_simpset HOL_basic_ss ctxt addsimps (simps @ prems')) |
803 THEN' TRY o REPEAT_ALL_NEW |
805 THEN' TRY o REPEAT_ALL_NEW |
804 (FIRST' [ rtac @{thm TrueI}, |
806 (FIRST' [ rtac @{thm TrueI}, |
805 rtac @{thm conjI}, |
807 rtac @{thm conjI}, |
806 rtac @{thm refl}, |
808 rtac @{thm refl}, |
807 resolve_tac prems', |
809 resolve_tac prems', |