equal
deleted
inserted
replaced
192 apply(assumption) |
192 apply(assumption) |
193 apply(simp) |
193 apply(simp) |
194 done |
194 done |
195 |
195 |
196 quotient_definition |
196 quotient_definition |
197 "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs" |
197 "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs" |
198 as |
198 is |
199 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |
199 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |
200 |
200 |
201 lemma [quot_respect]: |
201 lemma [quot_respect]: |
202 shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair" |
202 shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair" |
203 apply(clarsimp) |
203 apply(clarsimp) |
204 apply(rule exI) |
204 apply(rule exI) |
232 instantiation abs :: (pt) pt |
232 instantiation abs :: (pt) pt |
233 begin |
233 begin |
234 |
234 |
235 quotient_definition |
235 quotient_definition |
236 "permute_abs::perm \<Rightarrow> ('a::pt abs) \<Rightarrow> 'a abs" |
236 "permute_abs::perm \<Rightarrow> ('a::pt abs) \<Rightarrow> 'a abs" |
237 as |
237 is |
238 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" |
238 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" |
239 |
239 |
240 lemma permute_ABS [simp]: |
240 lemma permute_ABS [simp]: |
241 fixes x::"'a::pt" (* ??? has to be 'a \<dots> 'b does not work *) |
241 fixes x::"'a::pt" (* ??? has to be 'a \<dots> 'b does not work *) |
242 shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)" |
242 shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)" |
250 |
250 |
251 end |
251 end |
252 |
252 |
253 quotient_definition |
253 quotient_definition |
254 "supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool" |
254 "supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool" |
255 as |
255 is |
256 "supp_abs_fun" |
256 "supp_abs_fun" |
257 |
257 |
258 lemma supp_Abs_fun_simp: |
258 lemma supp_Abs_fun_simp: |
259 shows "supp_Abs_fun (Abs bs x) = (supp x) - bs" |
259 shows "supp_Abs_fun (Abs bs x) = (supp x) - bs" |
260 by (lifting supp_abs_fun.simps(1)) |
260 by (lifting supp_abs_fun.simps(1)) |