168 apply (erule alpha.cases) |
168 apply (erule alpha.cases) |
169 apply (simp_all add: rlam.inject alpha_refl) |
169 apply (simp_all add: rlam.inject alpha_refl) |
170 done |
170 done |
171 |
171 |
172 ML {* val qty = @{typ "lam"} *} |
172 ML {* val qty = @{typ "lam"} *} |
173 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *} |
|
174 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *} |
173 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *} |
175 |
174 |
176 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
175 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
177 ML {* val consts = lookup_quot_consts defs *} |
|
178 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
176 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} |
179 ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
177 ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] [quot] *} |
180 |
178 |
181 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)" |
179 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)" |
182 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) |
180 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) |
183 done |
181 done |
184 |
182 |
335 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
333 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
336 apply (simp only: perm_prs) |
334 apply (simp only: perm_prs) |
337 prefer 2 |
335 prefer 2 |
338 apply (tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
336 apply (tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
339 prefer 3 |
337 prefer 3 |
340 apply (tactic {* clean_tac @{context} [quot] defs 1 *}) |
338 apply (tactic {* clean_tac @{context} [quot] 1 *}) |
341 |
339 |
342 thm all_prs |
340 thm all_prs |
343 thm REP_ABS_RSP |
341 thm REP_ABS_RSP |
344 thm ball_reg_eqv_range |
342 thm ball_reg_eqv_range |
345 |
343 |