equal
deleted
inserted
replaced
73 using a |
73 using a |
74 apply(induct rule: alpha_bn_inducts) |
74 apply(induct rule: alpha_bn_inducts) |
75 apply(simp add: trm_assn.perm_bn_simps) |
75 apply(simp add: trm_assn.perm_bn_simps) |
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) |
|
79 done |
78 done |
80 |
79 |
81 |
80 |
82 function |
81 function |
83 apply_assn :: "(trm \<Rightarrow> nat) \<Rightarrow> assn \<Rightarrow> nat" |
82 apply_assn :: "(trm \<Rightarrow> nat) \<Rightarrow> assn \<Rightarrow> nat" |
93 termination by lexicographic_order |
92 termination by lexicographic_order |
94 |
93 |
95 lemma [eqvt]: |
94 lemma [eqvt]: |
96 "p \<bullet> (apply_assn f a) = apply_assn (p \<bullet> f) (p \<bullet> a)" |
95 "p \<bullet> (apply_assn f a) = apply_assn (p \<bullet> f) (p \<bullet> a)" |
97 apply(induct f a rule: apply_assn.induct) |
96 apply(induct f a rule: apply_assn.induct) |
98 apply simp_all |
97 apply simp |
|
98 apply(simp only: apply_assn.simps trm_assn.perm_simps) |
99 apply(perm_simp) |
99 apply(perm_simp) |
100 apply rule |
100 apply(simp) |
101 apply(perm_simp) |
|
102 apply simp |
|
103 done |
101 done |
104 |
102 |
105 lemma alpha_bn_apply_assn: |
103 lemma alpha_bn_apply_assn: |
106 assumes "alpha_bn as bs" |
104 assumes "alpha_bn as bs" |
107 shows "apply_assn f as = apply_assn f bs" |
105 shows "apply_assn f as = apply_assn f bs" |
153 |
151 |
154 lemma [eqvt]: |
152 lemma [eqvt]: |
155 "p \<bullet> (apply_assn2 f a) = apply_assn2 (p \<bullet> f) (p \<bullet> a)" |
153 "p \<bullet> (apply_assn2 f a) = apply_assn2 (p \<bullet> f) (p \<bullet> a)" |
156 apply(induct f a rule: apply_assn2.induct) |
154 apply(induct f a rule: apply_assn2.induct) |
157 apply simp_all |
155 apply simp_all |
158 apply(perm_simp) |
|
159 apply rule |
|
160 done |
156 done |
161 |
157 |
162 lemma bn_apply_assn2: "bn (apply_assn2 f as) = bn as" |
158 lemma bn_apply_assn2: "bn (apply_assn2 f as) = bn as" |
163 apply (induct as rule: trm_assn.inducts(2)) |
159 apply (induct as rule: trm_assn.inducts(2)) |
164 apply (rule TrueI) |
160 apply (rule TrueI) |