449 notation |
449 notation |
450 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
450 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
451 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
451 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
452 thm alpha_rtrm4_alpha_rtrm4_list.intros |
452 thm alpha_rtrm4_alpha_rtrm4_list.intros |
453 |
453 |
454 (*local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} *) |
454 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} |
|
455 thm alpha4_inj |
455 |
456 |
456 lemma alpha4_eqvt: |
457 lemma alpha4_eqvt: |
457 "t \<approx>4 s \<Longrightarrow> (pi \<bullet> t) \<approx>4 (pi \<bullet> s)" |
458 "t \<approx>4 s \<Longrightarrow> (pi \<bullet> t) \<approx>4 (pi \<bullet> s)" |
458 "a \<approx>4l b \<Longrightarrow> (pi \<bullet> a) \<approx>4l (pi \<bullet> b)" |
459 "a \<approx>4l b \<Longrightarrow> (pi \<bullet> a) \<approx>4l (pi \<bullet> b)" |
459 sorry |
460 sorry |
460 |
461 |
461 (*local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), |
462 (* |
462 (build_equivps [@{term alpha_rtrm4}, @{term alpha_rassigns}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject rassigns.inject} @{thms alpha4_inj} @{thms rtrm4.distinct rassigns.distinct} @{thms alpha_rtrm4.cases alpha_rassigns.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}*) |
463 prove alpha4_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] ("x","y","z")) *} |
|
464 apply (tactic {* |
|
465 transp_tac @{thm rtrm4.induct} @{thms alpha4_inj} @{thms rtrm4.inject list.inject} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha1_eqvt} 1 *}) |
|
466 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []), |
|
467 (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases list.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *} |
|
468 *) |
|
469 |
|
470 |
463 |
471 |
464 |
472 |
465 lemma alpha4_equivp: "equivp alpha_rtrm4" sorry |
473 lemma alpha4_equivp: "equivp alpha_rtrm4" sorry |
466 lemma alpha4list_equivp: "equivp alpha_rtrm4_list" sorry |
474 lemma alpha4list_equivp: "equivp alpha_rtrm4_list" sorry |
467 |
475 |