equal
deleted
inserted
replaced
212 quotient_definition |
212 quotient_definition |
213 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1" |
213 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1" |
214 as |
214 as |
215 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1" |
215 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1" |
216 |
216 |
|
217 lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted] |
|
218 |
217 instance |
219 instance |
218 apply default |
220 apply default |
219 apply(induct_tac [!] x rule: trm1_bp_inducts(1)) |
221 apply(induct_tac [!] x rule: trm1_bp_inducts(1)) |
220 apply(simp_all add: permute_rtrm1_permute_bp.simps[quot_lifted]) |
222 apply(simp_all) |
221 done |
223 done |
222 |
224 |
223 end |
225 end |
224 |
|
225 lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted] |
|
226 |
226 |
227 lemmas fv_trm1 = rfv_trm1_rfv_bp.simps[quot_lifted] |
227 lemmas fv_trm1 = rfv_trm1_rfv_bp.simps[quot_lifted] |
228 |
228 |
229 lemmas fv_trm1_eqvt = rfv_trm1_eqvt[quot_lifted] |
229 lemmas fv_trm1_eqvt = rfv_trm1_eqvt[quot_lifted] |
230 |
230 |