306 sorry |
306 sorry |
307 |
307 |
308 lemma perm_prs2: "(id ---> option_map ABS_lam) ((id ---> option_map REP_lam) ([b].(s::lam))) = [b].s" |
308 lemma perm_prs2: "(id ---> option_map ABS_lam) ((id ---> option_map REP_lam) ([b].(s::lam))) = [b].s" |
309 sorry |
309 sorry |
310 |
310 |
311 lemma real_alpha: |
311 lemma real_alpha_lift: |
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} [quot] [rel_refl] [trans2] 1 *}) |
316 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
316 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) |
317 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
317 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) |
318 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
318 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) |
319 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
319 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) |
320 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
320 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) |
321 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
321 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) |
322 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
322 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) |
323 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
323 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) |
324 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
324 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) |
325 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
325 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) |
326 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
326 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) |
327 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
327 apply (tactic {* inj_repabs_tac @{context} [quot] [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} [quot] [rel_refl] [trans2] 1 *}) |
329 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
329 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) |
330 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
330 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) |
331 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
331 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) |
332 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
332 apply (tactic {* inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *}) |
333 apply (tactic {* inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
333 apply (tactic {* inj_repabs_tac @{context} [quot] [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} [quot] [rel_refl] [trans2] 1 *}) |
337 prefer 3 |
337 prefer 3 |
338 apply (tactic {* clean_tac @{context} [quot] 1 *}) |
338 apply (tactic {* clean_tac @{context} [quot] 1 *}) |
339 |
339 |
340 thm all_prs |
340 thm all_prs |
341 thm REP_ABS_RSP |
341 thm REP_ABS_RSP |
342 thm ball_reg_eqv_range |
342 thm ball_reg_eqv_range |
343 |
343 |
344 |
344 |
345 thm perm_lam_def |
345 thm perm_lam_def |
346 apply (simp only: perm_prs) |
346 apply (simp only: perm_prs) |
347 |
347 (*apply (tactic {* regularize_tac @{context} [quot] 1 *})*) |
348 apply (tactic {* regularize_tac @{context} [quot] 1 *}) |
348 sorry |
349 |
349 |
350 done |
350 done |
351 |
351 |