157 and fresh2: "set bs \<sharp>* c" |
157 and fresh2: "set bs \<sharp>* c" |
158 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
158 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" |
159 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
159 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" |
160 shows "f as x c = f bs y c" |
160 shows "f as x c = f bs y c" |
161 *) |
161 *) |
|
162 |
|
163 lemma supp_zero_perm_zero: |
|
164 shows "supp (p :: perm) = {} \<longleftrightarrow> p = 0" |
|
165 by (metis supp_perm_singleton supp_zero_perm) |
|
166 |
|
167 lemma permute_atom_list_id: |
|
168 shows "p \<bullet> l = l \<longleftrightarrow> supp p \<inter> set l = {}" |
|
169 by (induct l) (auto simp add: supp_Nil supp_perm) |
|
170 |
|
171 lemma Abs_lst_binder_length: |
|
172 shows "[xs]lst. T = [ys]lst. S \<Longrightarrow> length xs = length ys" |
|
173 by (auto simp add: Abs_eq_iff alphas length_eqvt[symmetric] permute_pure) |
|
174 |
|
175 lemma Abs_lst_binder_eq: |
|
176 shows "Abs_lst l T = Abs_lst l S \<longleftrightarrow> T = S" |
|
177 by (rule, simp_all add: Abs_eq_iff2 alphas) |
|
178 (metis fresh_star_zero inf_absorb1 permute_atom_list_id supp_perm_eq |
|
179 supp_zero_perm_zero) |
162 |
180 |
163 nominal_primrec |
181 nominal_primrec |
164 crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm" ("_[_\<turnstile>c>_]" [100,100,100] 100) |
182 crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm" ("_[_\<turnstile>c>_]" [100,100,100] 100) |
165 where |
183 where |
166 "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" |
184 "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" |