equal
deleted
inserted
replaced
76 apply(simp add: trm_assn.perm_bn_simps) |
76 apply(simp add: trm_assn.perm_bn_simps) |
77 apply(simp add: trm_assn.bn_defs) |
77 apply(simp add: trm_assn.bn_defs) |
78 apply(simp add: atom_eqvt) |
78 apply(simp add: atom_eqvt) |
79 done |
79 done |
80 |
80 |
81 |
|
82 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
|
83 by (simp add: permute_pure) |
|
84 |
81 |
85 function |
82 function |
86 apply_assn :: "(trm \<Rightarrow> nat) \<Rightarrow> assn \<Rightarrow> nat" |
83 apply_assn :: "(trm \<Rightarrow> nat) \<Rightarrow> assn \<Rightarrow> nat" |
87 where |
84 where |
88 "apply_assn f ANil = (0 :: nat)" |
85 "apply_assn f ANil = (0 :: nat)" |