310 |
310 |
311 lemma real_alpha: |
311 lemma real_alpha: |
312 "\<lbrakk>t = [(a, b)] \<bullet> s; a \<sharp> [b].s\<rbrakk> \<Longrightarrow> Lam a t = Lam b s" |
312 "\<lbrakk>t = [(a, b)] \<bullet> s; a \<sharp> [b].s\<rbrakk> \<Longrightarrow> Lam a t = Lam b s" |
313 apply (tactic {* procedure_tac @{context} @{thm real_alpha_pre} 1 *}) |
313 apply (tactic {* procedure_tac @{context} @{thm real_alpha_pre} 1 *}) |
314 prefer 2 |
314 prefer 2 |
315 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
315 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
316 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
316 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
317 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
317 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
318 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
318 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
319 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
319 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
320 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
320 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
321 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
321 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
322 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
322 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
323 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
323 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
324 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
324 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
325 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
325 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
326 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
326 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
327 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
327 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
328 apply (tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
328 apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
329 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
329 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
330 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
330 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
331 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
331 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
332 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
332 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
333 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
333 apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
334 apply (simp only: perm_prs) |
334 apply (simp only: perm_prs) |
335 prefer 2 |
335 prefer 2 |
336 apply (tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
336 apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
337 prefer 3 |
337 prefer 3 |
338 apply (tactic {* clean_tac @{context} [quot] 1 *}) |
338 apply (tactic {* clean_tac @{context} 1 *}) |
339 |
|
340 thm all_prs |
|
341 thm REP_ABS_RSP |
|
342 thm ball_reg_eqv_range |
|
343 |
|
344 |
|
345 thm perm_lam_def |
|
346 apply (simp only: perm_prs) |
339 apply (simp only: perm_prs) |
347 |
340 (*apply (tactic {* regularize_tac @{context} 1 *})*) |
348 apply (tactic {* regularize_tac @{context} [quot] 1 *}) |
341 |
349 |
342 done |
350 done |
343 |
351 |
|