equal
deleted
inserted
replaced
56 fixes pi::"name prm" |
56 fixes pi::"name prm" |
57 shows "pi\<bullet>(vsub t n s) = vsub (pi\<bullet>t) (pi\<bullet>n) (pi\<bullet>s)" |
57 shows "pi\<bullet>(vsub t n s) = vsub (pi\<bullet>t) (pi\<bullet>n) (pi\<bullet>s)" |
58 by (induct t arbitrary: n rule: llam.induct) |
58 by (induct t arbitrary: n rule: llam.induct) |
59 (simp_all add: perm_nat_def) |
59 (simp_all add: perm_nat_def) |
60 |
60 |
61 constdefs |
61 definition freshen :: "llam \<Rightarrow> name \<Rightarrow> llam" where |
62 freshen :: "llam \<Rightarrow> name \<Rightarrow> llam" |
|
63 "freshen t p \<equiv> vsub t 0 (lPar p)" |
62 "freshen t p \<equiv> vsub t 0 (lPar p)" |
64 |
63 |
65 lemma freshen_eqvt[eqvt]: |
64 lemma freshen_eqvt[eqvt]: |
66 fixes pi::"name prm" |
65 fixes pi::"name prm" |
67 shows "pi\<bullet>(freshen t p) = freshen (pi\<bullet>t) (pi\<bullet>p)" |
66 shows "pi\<bullet>(freshen t p) = freshen (pi\<bullet>t) (pi\<bullet>p)" |