equal
deleted
inserted
replaced
25 thm let_rec.perm_simps |
25 thm let_rec.perm_simps |
26 thm let_rec.eq_iff |
26 thm let_rec.eq_iff |
27 thm let_rec.fv_bn_eqvt |
27 thm let_rec.fv_bn_eqvt |
28 thm let_rec.size_eqvt |
28 thm let_rec.size_eqvt |
29 |
29 |
30 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
|
31 by (simp add: permute_pure) |
|
32 |
30 |
33 nominal_primrec |
31 nominal_primrec |
34 height_trm :: "trm \<Rightarrow> nat" |
32 height_trm :: "trm \<Rightarrow> nat" |
35 and height_bp :: "bp \<Rightarrow> nat" |
33 and height_bp :: "bp \<Rightarrow> nat" |
36 where |
34 where |
54 apply (simp add: alphas) |
52 apply (simp add: alphas) |
55 apply clarify |
53 apply clarify |
56 apply (rule trans) |
54 apply (rule trans) |
57 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
55 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
58 apply (simp add: pure_supp fresh_star_def) |
56 apply (simp add: pure_supp fresh_star_def) |
59 apply (simp only: eqvts) |
57 apply(simp add: eqvt_at_def) |
60 apply (simp add: eqvt_at_def) |
58 apply(perm_simp) |
|
59 apply (simp add: permute_fun_def) |
61 done |
60 done |
62 |
61 |
63 termination by lexicographic_order |
62 termination by lexicographic_order |
64 |
63 |
65 end |
64 end |