202 and "(\<And>as (x::'a::pt). P3 (Abs_lst as x)) \<Longrightarrow> P3 x3" |
202 and "(\<And>as (x::'a::pt). P3 (Abs_lst as x)) \<Longrightarrow> P3 x3" |
203 by (lifting prod.induct[where 'a="atom set" and 'b="'a"] |
203 by (lifting prod.induct[where 'a="atom set" and 'b="'a"] |
204 prod.induct[where 'a="atom set" and 'b="'a"] |
204 prod.induct[where 'a="atom set" and 'b="'a"] |
205 prod.induct[where 'a="atom list" and 'b="'a"]) |
205 prod.induct[where 'a="atom list" and 'b="'a"]) |
206 |
206 |
|
207 lemma abs_eq_iff: |
|
208 shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)" |
|
209 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)" |
|
210 and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)" |
|
211 apply(simp_all) |
|
212 apply(lifting alphas_abs) |
|
213 done |
|
214 |
207 instantiation abs_gen :: (pt) pt |
215 instantiation abs_gen :: (pt) pt |
208 begin |
216 begin |
209 |
217 |
210 quotient_definition |
218 quotient_definition |
211 "permute_abs_gen::perm \<Rightarrow> ('a::pt abs_gen) \<Rightarrow> 'a abs_gen" |
219 "permute_abs_gen::perm \<Rightarrow> ('a::pt abs_gen) \<Rightarrow> 'a abs_gen" |
267 |
275 |
268 end |
276 end |
269 |
277 |
270 lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst |
278 lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst |
271 |
279 |
|
280 lemma abs_swap1: |
|
281 assumes a1: "a \<notin> (supp x) - bs" |
|
282 and a2: "b \<notin> (supp x) - bs" |
|
283 shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
|
284 and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
|
285 unfolding abs_eq_iff |
|
286 unfolding alphas_abs |
|
287 unfolding alphas |
|
288 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] |
|
289 unfolding fresh_star_def fresh_def |
|
290 unfolding swap_set_not_in[OF a1 a2] |
|
291 using a1 a2 |
|
292 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
|
293 (auto simp add: supp_perm swap_atom) |
|
294 |
|
295 lemma abs_swap2: |
|
296 assumes a1: "a \<notin> (supp x) - (set bs)" |
|
297 and a2: "b \<notin> (supp x) - (set bs)" |
|
298 shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
|
299 unfolding abs_eq_iff |
|
300 unfolding alphas_abs |
|
301 unfolding alphas |
|
302 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric] |
|
303 unfolding fresh_star_def fresh_def |
|
304 unfolding swap_set_not_in[OF a1 a2] |
|
305 using a1 a2 |
|
306 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
|
307 (auto simp add: supp_perm swap_atom) |
|
308 |
|
309 lemma abs_supports: |
|
310 shows "((supp x) - as) supports (Abs as x)" |
|
311 and "((supp x) - as) supports (Abs_res as x)" |
|
312 and "((supp x) - (set bs)) supports (Abs_lst bs x)" |
|
313 unfolding supports_def |
|
314 unfolding permute_abs |
|
315 by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric]) |
272 |
316 |
273 quotient_definition |
317 quotient_definition |
274 "supp_gen :: ('a::pt) abs_gen \<Rightarrow> atom set" |
318 "supp_gen :: ('a::pt) abs_gen \<Rightarrow> atom set" |
275 is |
319 is |
276 "aux_set" |
320 "aux_set" |
308 and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)" |
352 and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)" |
309 and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)" |
353 and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)" |
310 apply(rule_tac [!] fresh_fun_eqvt_app) |
354 apply(rule_tac [!] fresh_fun_eqvt_app) |
311 apply(simp_all add: eqvts_raw) |
355 apply(simp_all add: eqvts_raw) |
312 done |
356 done |
313 |
|
314 lemma abs_eq_iff: |
|
315 shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)" |
|
316 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)" |
|
317 and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)" |
|
318 apply(simp_all) |
|
319 apply(lifting alphas_abs) |
|
320 done |
|
321 |
|
322 lemma abs_swap1: |
|
323 assumes a1: "a \<notin> (supp x) - bs" |
|
324 and a2: "b \<notin> (supp x) - bs" |
|
325 shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
|
326 and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
|
327 unfolding abs_eq_iff |
|
328 unfolding alphas_abs |
|
329 unfolding alphas |
|
330 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] |
|
331 unfolding fresh_star_def fresh_def |
|
332 unfolding swap_set_not_in[OF a1 a2] |
|
333 using a1 a2 |
|
334 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
|
335 (auto simp add: supp_perm swap_atom) |
|
336 |
|
337 lemma abs_swap2: |
|
338 assumes a1: "a \<notin> (supp x) - (set bs)" |
|
339 and a2: "b \<notin> (supp x) - (set bs)" |
|
340 shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
|
341 unfolding abs_eq_iff |
|
342 unfolding alphas_abs |
|
343 unfolding alphas |
|
344 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric] |
|
345 unfolding fresh_star_def fresh_def |
|
346 unfolding swap_set_not_in[OF a1 a2] |
|
347 using a1 a2 |
|
348 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
|
349 (auto simp add: supp_perm swap_atom) |
|
350 |
|
351 lemma abs_supports: |
|
352 shows "((supp x) - as) supports (Abs as x)" |
|
353 and "((supp x) - as) supports (Abs_res as x)" |
|
354 and "((supp x) - (set bs)) supports (Abs_lst bs x)" |
|
355 unfolding supports_def |
|
356 unfolding permute_abs |
|
357 by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric]) |
|
358 |
357 |
359 lemma supp_abs_subset1: |
358 lemma supp_abs_subset1: |
360 assumes a: "finite (supp x)" |
359 assumes a: "finite (supp x)" |
361 shows "(supp x) - as \<subseteq> supp (Abs as x)" |
360 shows "(supp x) - as \<subseteq> supp (Abs as x)" |
362 and "(supp x) - as \<subseteq> supp (Abs_res as x)" |
361 and "(supp x) - as \<subseteq> supp (Abs_res as x)" |