equal
deleted
inserted
replaced
93 Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt |
93 Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt |
94 val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) |
94 val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) |
95 *} |
95 *} |
96 |
96 |
97 ML {* |
97 ML {* |
98 fun constr_rsp_tac inj rsp equivps = |
98 fun constr_rsp_tac inj rsp = |
99 let |
|
100 val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps |
|
101 in |
|
102 REPEAT o rtac impI THEN' |
99 REPEAT o rtac impI THEN' |
103 simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW |
100 simp_tac (HOL_ss addsimps inj) THEN' split_conjs THEN_ALL_NEW |
104 (asm_simp_tac HOL_ss THEN_ALL_NEW ( |
101 (asm_simp_tac HOL_ss THEN_ALL_NEW ( |
105 rtac @{thm exI[of _ "0 :: perm"]} THEN' |
102 REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW |
106 asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @ |
103 simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW |
107 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
104 asm_full_simp_tac (HOL_ss addsimps (rsp @ |
|
105 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left})) |
108 )) |
106 )) |
109 end |
|
110 *} |
107 *} |
111 |
108 |
112 (* Testing code |
109 (* Testing code |
113 local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}] |
110 local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}] |
114 (fn _ => fv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms fv_rtrm2_fv_rassign.simps} 1) *}*) |
111 (fn _ => fv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms fv_rtrm2_fv_rassign.simps} 1) *}*) |