equal
deleted
inserted
replaced
27 by (metis List.finite_set image_set supp_finite_set_at_base supp_set) |
27 by (metis List.finite_set image_set supp_finite_set_at_base supp_set) |
28 |
28 |
29 lemma atom_image_set_eq_supp: "atom ` set xs = supp xs" |
29 lemma atom_image_set_eq_supp: "atom ` set xs = supp xs" |
30 by (metis image_set set_map_atom_eq_supp) |
30 by (metis image_set set_map_atom_eq_supp) |
31 |
31 |
32 nominal_primrec (in name_subst) |
32 nominal_function (in name_subst) |
33 subst :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [120,120,120] 120) |
33 subst :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [120,120,120] 120) |
34 where |
34 where |
35 "(Var x)[xs::=t] = name_subst x xs t" |
35 "(Var x)[xs::=t] = name_subst x xs t" |
36 | "(s \<cdot> t)[xs::=u] = s[xs::=u] \<cdot> t[xs::=u]" |
36 | "(s \<cdot> t)[xs::=u] = s[xs::=u] \<cdot> t[xs::=u]" |
37 | "\<lbrakk>supp xs \<sharp>* ys; supp xs \<sharp>* u\<rbrakk> \<Longrightarrow> (Lam xs. t)[ys::=u] = Lam xs. t[ys::=u]" |
37 | "\<lbrakk>supp xs \<sharp>* ys; supp xs \<sharp>* u\<rbrakk> \<Longrightarrow> (Lam xs. t)[ys::=u] = Lam xs. t[ys::=u]" |