58 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2})) |
58 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2})) |
59 |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2}))) |
59 |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2}))) |
60 *} |
60 *} |
61 print_theorems |
61 print_theorems |
62 |
62 |
63 local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}] |
63 local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}] |
64 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.induct} @{thms fv_rtrm2_fv_rassign.simps} 1) *} |
64 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.induct} @{thms fv_rtrm2_fv_rassign.simps} 1) *} |
65 local_setup {* prove_const_rsp @{binding rbv2_rsp} [@{term rbv2}] |
65 local_setup {* snd o prove_const_rsp @{binding rbv2_rsp} [@{term rbv2}] |
66 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms rbv2.simps} 1) *} |
66 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms rbv2.simps} 1) *} |
67 local_setup {* prove_const_rsp @{binding rVr2_rsp} [@{term rVr2}] |
67 local_setup {* snd o prove_const_rsp @{binding rVr2_rsp} [@{term rVr2}] |
68 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
68 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
69 local_setup {* prove_const_rsp @{binding rAp2_rsp} [@{term rAp2}] |
69 local_setup {* snd o prove_const_rsp @{binding rAp2_rsp} [@{term rAp2}] |
70 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
70 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
71 local_setup {* prove_const_rsp @{binding rLm2_rsp} [@{term rLm2}] |
71 local_setup {* snd o prove_const_rsp @{binding rLm2_rsp} [@{term rLm2}] |
72 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
72 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
73 local_setup {* prove_const_rsp @{binding rLt2_rsp} [@{term rLt2}] |
73 local_setup {* snd o prove_const_rsp @{binding rLt2_rsp} [@{term rLt2}] |
74 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp rbv2_rsp} @{thms alpha2_equivp} 1) *} |
74 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp rbv2_rsp} @{thms alpha2_equivp} 1) *} |
75 local_setup {* prove_const_rsp @{binding permute_rtrm2_rsp} [@{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"}] |
75 local_setup {* snd o prove_const_rsp @{binding permute_rtrm2_rsp} [@{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"}] |
76 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *} |
76 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *} |
77 |
77 |
78 end |
78 end |