equal
deleted
inserted
replaced
214 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
214 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
215 apply(blast) |
215 apply(blast) |
216 apply(blast) |
216 apply(blast) |
217 done |
217 done |
218 |
218 |
219 termination |
219 termination (eqvt) |
220 by lexicographic_order |
220 by lexicographic_order |
221 |
221 |
222 nominal_primrec |
222 nominal_primrec |
223 nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm" ("_[_\<turnstile>n>_]" [100,100,100] 100) |
223 nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm" ("_[_\<turnstile>n>_]" [100,100,100] 100) |
224 where |
224 where |
377 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
377 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
378 apply(blast) |
378 apply(blast) |
379 apply(blast) |
379 apply(blast) |
380 done |
380 done |
381 |
381 |
382 termination |
382 termination (eqvt) |
383 by lexicographic_order |
383 by lexicographic_order |
384 |
384 |
385 lemma crename_name_eqvt[eqvt]: |
385 lemma crename_name_eqvt[eqvt]: |
386 shows "p \<bullet> (M[d\<turnstile>c>e]) = (p \<bullet> M)[(p \<bullet> d)\<turnstile>c>(p \<bullet> e)]" |
386 shows "p \<bullet> (M[d\<turnstile>c>e]) = (p \<bullet> M)[(p \<bullet> d)\<turnstile>c>(p \<bullet> e)]" |
387 apply(nominal_induct M avoiding: d e rule: trm.strong_induct) |
387 apply(nominal_induct M avoiding: d e rule: trm.strong_induct) |