equal
deleted
inserted
replaced
45 thm trm.fv_bn_eqvt |
45 thm trm.fv_bn_eqvt |
46 thm trm.size_eqvt |
46 thm trm.size_eqvt |
47 thm trm.supp |
47 thm trm.supp |
48 thm trm.supp[simplified] |
48 thm trm.supp[simplified] |
49 |
49 |
50 nominal_primrec |
50 nominal_function |
51 crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm" ("_[_\<turnstile>c>_]" [100,100,100] 100) |
51 crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm" ("_[_\<turnstile>c>_]" [100,100,100] 100) |
52 where |
52 where |
53 "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" |
53 "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" |
54 | "atom a \<sharp> (d, e) \<Longrightarrow> (Cut <a>.M (x).N)[d\<turnstile>c>e] = Cut <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e])" |
54 | "atom a \<sharp> (d, e) \<Longrightarrow> (Cut <a>.M (x).N)[d\<turnstile>c>e] = Cut <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e])" |
55 | "(NotR (x).M a)[d\<turnstile>c>e] = (if a=d then NotR (x).(M[d\<turnstile>c>e]) e else NotR (x).(M[d\<turnstile>c>e]) a)" |
55 | "(NotR (x).M a)[d\<turnstile>c>e] = (if a=d then NotR (x).(M[d\<turnstile>c>e]) e else NotR (x).(M[d\<turnstile>c>e]) a)" |
250 done |
250 done |
251 |
251 |
252 termination (eqvt) |
252 termination (eqvt) |
253 by lexicographic_order |
253 by lexicographic_order |
254 |
254 |
255 nominal_primrec |
255 nominal_function |
256 nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm" ("_[_\<turnstile>n>_]" [100,100,100] 100) |
256 nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm" ("_[_\<turnstile>n>_]" [100,100,100] 100) |
257 where |
257 where |
258 "(Ax x a)[u\<turnstile>n>v] = (if x=u then Ax v a else Ax x a)" |
258 "(Ax x a)[u\<turnstile>n>v] = (if x=u then Ax v a else Ax x a)" |
259 | "atom x \<sharp> (u, v) \<Longrightarrow> (Cut <a>.M (x).N)[u\<turnstile>n>v] = Cut <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v])" |
259 | "atom x \<sharp> (u, v) \<Longrightarrow> (Cut <a>.M (x).N)[u\<turnstile>n>v] = Cut <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v])" |
260 | "atom x \<sharp> (u, v) \<Longrightarrow> (NotR (x).M a)[u\<turnstile>n>v] = NotR (x).(M[u\<turnstile>n>v]) a" |
260 | "atom x \<sharp> (u, v) \<Longrightarrow> (NotR (x).M a)[u\<turnstile>n>v] = NotR (x).(M[u\<turnstile>n>v]) a" |
447 by lexicographic_order |
447 by lexicographic_order |
448 |
448 |
449 thm crename.eqvt nrename.eqvt |
449 thm crename.eqvt nrename.eqvt |
450 |
450 |
451 |
451 |
452 nominal_primrec |
452 nominal_function |
453 substn :: "trm \<Rightarrow> name \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100) |
453 substn :: "trm \<Rightarrow> name \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100) |
454 where |
454 where |
455 "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)" |
455 "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)" |
456 | "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){y:=<c>.P} = |
456 | "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){y:=<c>.P} = |
457 (if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))" |
457 (if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))" |