131 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) |
131 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) |
132 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) |
132 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) |
133 *} |
133 *} |
134 print_theorems |
134 print_theorems |
135 |
135 |
136 local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} @{term fv_rtrm1} |
136 thm alpha_rtrm1_alpha_bp.induct |
137 (fn _ => fv_rsp_tac @{thms alpha_rtrm1_alpha_bp.inducts} @{thms fv_rtrm1_fv_bp.simps} 1) *} |
137 local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}] |
138 local_setup {* prove_const_rsp @{binding rVr1_rsp} @{term rVr1} |
138 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm1_alpha_bp.inducts(1)} @{thms fv_rtrm1_fv_bp.simps} 1) *} |
|
139 local_setup {* prove_const_rsp @{binding rVr1_rsp} [@{term rVr1}] |
139 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
140 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
140 local_setup {* prove_const_rsp @{binding rAp1_rsp} @{term rAp1} |
141 local_setup {* prove_const_rsp @{binding rAp1_rsp} [@{term rAp1}] |
141 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
142 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
142 local_setup {* prove_const_rsp @{binding rLm1_rsp} @{term rLm1} |
143 local_setup {* prove_const_rsp @{binding rLm1_rsp} [@{term rLm1}] |
143 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
144 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
144 local_setup {* prove_const_rsp @{binding rLt1_rsp} @{term rLt1} |
145 local_setup {* prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}] |
145 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
146 (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *} |
146 local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"} |
147 local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}] |
147 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *} |
148 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *} |
148 |
149 |
149 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
150 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
150 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
151 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
151 |
152 |
324 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2})) |
325 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2})) |
325 |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2}))) |
326 |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2}))) |
326 *} |
327 *} |
327 print_theorems |
328 print_theorems |
328 |
329 |
329 (*local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} @{term fv_rtrm2} |
330 local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}] |
330 (fn _ => fv_rsp_tac @{thms alpha_rtrm2_alpha_rassign.inducts} @{thms fv_rtrm2_fv_rassign.simps} 1) *} *) |
331 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.induct} @{thms fv_rtrm2_fv_rassign.simps} 1) *} |
331 lemma fv_rtrm2_rsp: "x \<approx>2 y \<Longrightarrow> fv_rtrm2 x = fv_rtrm2 y" sorry |
332 local_setup {* prove_const_rsp @{binding rbv2_rsp} [@{term rbv2}] |
332 lemma bv2_rsp: "x \<approx>2b y \<Longrightarrow> rbv2 x = rbv2 y" sorry |
333 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms rbv2.simps} 1) *} |
333 |
334 local_setup {* prove_const_rsp @{binding rVr2_rsp} [@{term rVr2}] |
334 local_setup {* prove_const_rsp @{binding rVr2_rsp} @{term rVr2} |
|
335 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
335 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
336 local_setup {* prove_const_rsp @{binding rAp2_rsp} @{term rAp2} |
336 local_setup {* prove_const_rsp @{binding rAp2_rsp} [@{term rAp2}] |
337 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
337 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
338 local_setup {* prove_const_rsp @{binding rLm2_rsp} @{term rLm2} |
338 local_setup {* prove_const_rsp @{binding rLm2_rsp} [@{term rLm2}] |
339 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
339 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *} |
340 local_setup {* prove_const_rsp @{binding rLt2_rsp} @{term rLt2} |
340 local_setup {* prove_const_rsp @{binding rLt2_rsp} [@{term rLt2}] |
341 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp bv2_rsp} @{thms alpha2_equivp} 1) *} |
341 (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp rbv2_rsp} @{thms alpha2_equivp} 1) *} |
342 local_setup {* prove_const_rsp @{binding permute_rtrm2_rsp} @{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"} |
342 local_setup {* prove_const_rsp @{binding permute_rtrm2_rsp} [@{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"}] |
343 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *} |
343 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *} |
344 |
344 |
345 |
345 |
346 section {*** lets with many assignments ***} |
346 section {*** lets with many assignments ***} |
347 |
347 |