equal
deleted
inserted
replaced
221 apply (rule_tac x="(a \<rightleftharpoons> b)" in exI) |
221 apply (rule_tac x="(a \<rightleftharpoons> b)" in exI) |
222 apply (simp add: neq) |
222 apply (simp add: neq) |
223 apply (simp add: Abs_eq_iff alphas supp_atom fresh_star_def neq) |
223 apply (simp add: Abs_eq_iff alphas supp_atom fresh_star_def neq) |
224 done |
224 done |
225 |
225 |
226 nominal_primrec |
226 nominal_function |
227 subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
227 subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
228 where |
228 where |
229 "subst s t (Var x) = (if (s = x) then t else (Var x))" |
229 "subst s t (Var x) = (if (s = x) then t else (Var x))" |
230 | "subst s t (App l r) = App (subst s t l) (subst s t r)" |
230 | "subst s t (App l r) = App (subst s t l) (subst s t r)" |
231 | "atom v \<sharp> (s, t) \<Longrightarrow> subst s t (Lam v b) = Lam v (subst s t b)" |
231 | "atom v \<sharp> (s, t) \<Longrightarrow> subst s t (Lam v b) = Lam v (subst s t b)" |