91 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) |
91 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) |
92 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) |
92 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) |
93 *} |
93 *} |
94 print_theorems |
94 print_theorems |
95 |
95 |
96 thm alpha_rtrm1_alpha_bp.induct |
96 local_setup {* snd o prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}] |
97 local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}] |
|
98 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm1_alpha_bp.inducts(1)} @{thms fv_rtrm1_fv_bp.simps} 1) *} |
97 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm1_alpha_bp.inducts(1)} @{thms fv_rtrm1_fv_bp.simps} 1) *} |
99 local_setup {* prove_const_rsp @{binding rVr1_rsp} [@{term rVr1}] |
98 local_setup {* snd o prove_const_rsp @{binding rVr1_rsp} [@{term rVr1}] |
100 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
99 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
101 local_setup {* prove_const_rsp @{binding rAp1_rsp} [@{term rAp1}] |
100 local_setup {* snd o prove_const_rsp @{binding rAp1_rsp} [@{term rAp1}] |
102 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
101 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
103 local_setup {* prove_const_rsp @{binding rLm1_rsp} [@{term rLm1}] |
102 local_setup {* snd o prove_const_rsp @{binding rLm1_rsp} [@{term rLm1}] |
104 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
103 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
105 local_setup {* prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}] |
104 local_setup {* snd o prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}] |
106 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
105 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
107 local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}] |
106 local_setup {* snd o prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}] |
108 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *} |
107 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *} |
109 |
108 |
110 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
109 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
111 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
110 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
112 |
111 |