diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Mon Jul 20 11:21:59 2015 +0100 +++ b/Nominal/Ex/Lambda.thy Sat Mar 19 21:06:48 2016 +0000 @@ -72,23 +72,6 @@ unfolding Ident_def by simp -thm lam.strong_induct - -lemma alpha_lam_raw_eqvt[eqvt]: "p \ (alpha_lam_raw x y) = alpha_lam_raw (p \ x) (p \ y)" - unfolding alpha_lam_raw_def - by perm_simp rule - -lemma abs_lam_eqvt[eqvt]: "(p \ abs_lam t) = abs_lam (p \ t)" -proof - - have "alpha_lam_raw (rep_lam (abs_lam t)) t" - using rep_abs_rsp_left Quotient3_lam equivp_reflp lam_equivp by metis - then have "alpha_lam_raw (p \ rep_lam (abs_lam t)) (p \ t)" - unfolding alpha_lam_raw_eqvt[symmetric] permute_pure . - then have "abs_lam (p \ rep_lam (abs_lam t)) = abs_lam (p \ t)" - using Quotient3_rel Quotient3_lam by metis - thus ?thesis using permute_lam_def id_apply map_fun_apply by metis -qed - section {* Simple examples from Norrish 2004 *}