equal
deleted
inserted
replaced
63 lemma fresh_fun_eqvt_app3: |
63 lemma fresh_fun_eqvt_app3: |
64 assumes e: "eqvt f" |
64 assumes e: "eqvt f" |
65 shows "\<lbrakk>a \<sharp> x; a \<sharp> y; a \<sharp> z\<rbrakk> \<Longrightarrow> a \<sharp> f x y z" |
65 shows "\<lbrakk>a \<sharp> x; a \<sharp> y; a \<sharp> z\<rbrakk> \<Longrightarrow> a \<sharp> f x y z" |
66 using fresh_fun_eqvt_app[OF e] fresh_fun_app by (metis (lifting, full_types)) |
66 using fresh_fun_eqvt_app[OF e] fresh_fun_app by (metis (lifting, full_types)) |
67 |
67 |
68 lemma |
68 lemma substr_simps: |
69 "substr (Var x) y s = (if x = y then s else (Var x))" |
69 "substr (Var x) y s = (if x = y then s else (Var x))" |
70 "substr (App t1 t2) y s = App (substr t1 y s) (substr t2 y s)" |
70 "substr (App t1 t2) y s = App (substr t1 y s) (substr t2 y s)" |
71 "atom x \<sharp> (y, s) \<Longrightarrow> substr (Lam [x]. t) y s = Lam [x]. (substr t y s)" |
71 "atom x \<sharp> (y, s) \<Longrightarrow> substr (Lam [x]. t) y s = Lam [x]. (substr t y s)" |
72 apply (subst substr.simps) apply (simp only: lam_rec.simps) |
72 apply (subst substr.simps) apply (simp only: lam_rec.simps) |
73 apply (subst substr.simps) apply (simp only: lam_rec.simps) |
73 apply (subst substr.simps) apply (simp only: lam_rec.simps) |