equal
deleted
inserted
replaced
105 using assms |
105 using assms |
106 apply (induct rule: alpha_bn_inducts) |
106 apply (induct rule: alpha_bn_inducts) |
107 apply simp_all |
107 apply simp_all |
108 done |
108 done |
109 |
109 |
110 nominal_primrec |
110 nominal_function |
111 height_trm :: "trm \<Rightarrow> nat" |
111 height_trm :: "trm \<Rightarrow> nat" |
112 where |
112 where |
113 "height_trm (Var x) = 1" |
113 "height_trm (Var x) = 1" |
114 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
114 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
115 | "height_trm (Lam v b) = 1 + (height_trm b)" |
115 | "height_trm (Lam v b) = 1 + (height_trm b)" |
158 apply (induct as rule: trm_assn.inducts(2)) |
158 apply (induct as rule: trm_assn.inducts(2)) |
159 apply (rule TrueI) |
159 apply (rule TrueI) |
160 apply (simp_all add: trm_assn.bn_defs) |
160 apply (simp_all add: trm_assn.bn_defs) |
161 done |
161 done |
162 |
162 |
163 nominal_primrec |
163 nominal_function |
164 subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
164 subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
165 where |
165 where |
166 "subst s t (Var x) = (if (s = x) then t else (Var x))" |
166 "subst s t (Var x) = (if (s = x) then t else (Var x))" |
167 | "subst s t (App l r) = App (subst s t l) (subst s t r)" |
167 | "subst s t (App l r) = App (subst s t l) (subst s t r)" |
168 | "atom v \<sharp> (s, t) \<Longrightarrow> subst s t (Lam v b) = Lam v (subst s t b)" |
168 | "atom v \<sharp> (s, t) \<Longrightarrow> subst s t (Lam v b) = Lam v (subst s t b)" |