49 "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)" |
49 "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)" |
50 "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)" |
50 "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)" |
51 apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts) |
51 apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts) |
52 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
52 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
53 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj) |
53 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj) |
54 apply (rule alpha_gen_atom_eqvt) |
54 apply (erule alpha_gen_compose_eqvt) |
55 apply (simp add: rfv_eqvt) |
55 apply (simp_all add: rfv_eqvt eqvts atom_eqvt) |
56 apply assumption |
56 apply (erule alpha_gen_compose_eqvt) |
57 apply (rule alpha_gen_atom_eqvt) |
57 apply (simp_all add: rfv_eqvt eqvts atom_eqvt) |
58 apply (simp add: rfv_eqvt) |
58 apply (erule alpha_gen_compose_eqvt) |
59 apply assumption |
59 apply (simp_all add: rfv_eqvt eqvts atom_eqvt) |
60 apply (rule alpha_gen_atom_eqvt) |
|
61 apply (simp add: rfv_eqvt) |
|
62 apply assumption |
|
63 done |
60 done |
64 |
61 |
65 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []), |
62 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []), |
66 (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}] |
63 (build_equivps [@{term alpha_rkind}, @{term alpha_rty}, @{term alpha_rtrm}] |
67 @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} |
64 @{thm rkind_rty_rtrm.induct} @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} |