equal
deleted
inserted
replaced
380 done |
380 done |
381 |
381 |
382 termination (eqvt) |
382 termination (eqvt) |
383 by lexicographic_order |
383 by lexicographic_order |
384 |
384 |
385 lemma crename_name_eqvt[eqvt]: |
385 thm crename.eqvt nrename.eqvt |
386 shows "p \<bullet> (M[d\<turnstile>c>e]) = (p \<bullet> M)[(p \<bullet> d)\<turnstile>c>(p \<bullet> e)]" |
386 |
387 apply(nominal_induct M avoiding: d e rule: trm.strong_induct) |
|
388 apply(auto) |
|
389 done |
|
390 |
|
391 lemma nrename_name_eqvt[eqvt]: |
|
392 shows "p \<bullet> (M[x\<turnstile>n>y]) = (p \<bullet> M)[(p \<bullet> x)\<turnstile>n>(p \<bullet> y)]" |
|
393 apply(nominal_induct M avoiding: x y rule: trm.strong_induct) |
|
394 apply(auto) |
|
395 done |
|
396 |
387 |
397 nominal_primrec |
388 nominal_primrec |
398 substn :: "trm \<Rightarrow> name \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100) |
389 substn :: "trm \<Rightarrow> name \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100) |
399 where |
390 where |
400 "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)" |
391 "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)" |