291 and "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute" |
291 and "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute" |
292 and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute" |
292 and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute" |
293 unfolding fun_rel_def |
293 unfolding fun_rel_def |
294 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt) |
294 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt) |
295 |
295 |
296 lemma abs_exhausts: |
296 lemma Abs_eq_iff: |
|
297 shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y))" |
|
298 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
|
299 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
|
300 by (lifting alphas_abs) |
|
301 |
|
302 lemma Abs_exhausts: |
297 shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1" |
303 shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1" |
298 and "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2" |
304 and "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2" |
299 and "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3" |
305 and "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3" |
300 by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"] |
306 by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"] |
301 prod.exhaust[where 'a="atom set" and 'b="'a"] |
307 prod.exhaust[where 'a="atom set" and 'b="'a"] |
302 prod.exhaust[where 'a="atom list" and 'b="'a"]) |
308 prod.exhaust[where 'a="atom list" and 'b="'a"]) |
303 |
309 |
304 lemma abs_eq_iff: |
|
305 shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (bs, x) \<approx>abs_set (cs, y)" |
|
306 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)" |
|
307 and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)" |
|
308 unfolding alphas_abs by (lifting alphas_abs) |
|
309 |
|
310 instantiation abs_set :: (pt) pt |
310 instantiation abs_set :: (pt) pt |
311 begin |
311 begin |
312 |
312 |
313 quotient_definition |
313 quotient_definition |
314 "permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set" |
314 "permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set" |
315 is |
315 is |
316 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" |
316 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" |
317 |
317 |
318 lemma permute_Abs[simp]: |
318 lemma permute_Abs_set[simp]: |
319 fixes x::"'a::pt" |
319 fixes x::"'a::pt" |
320 shows "(p \<bullet> (Abs_set as x)) = Abs_set (p \<bullet> as) (p \<bullet> x)" |
320 shows "(p \<bullet> (Abs_set as x)) = Abs_set (p \<bullet> as) (p \<bullet> x)" |
321 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) |
321 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) |
322 |
322 |
323 instance |
323 instance |
324 apply(default) |
324 apply(default) |
325 apply(case_tac [!] x rule: abs_exhausts(1)) |
325 apply(case_tac [!] x rule: Abs_exhausts(1)) |
326 apply(simp_all) |
326 apply(simp_all) |
327 done |
327 done |
328 |
328 |
329 end |
329 end |
330 |
330 |
362 shows "(p \<bullet> (Abs_lst as x)) = Abs_lst (p \<bullet> as) (p \<bullet> x)" |
362 shows "(p \<bullet> (Abs_lst as x)) = Abs_lst (p \<bullet> as) (p \<bullet> x)" |
363 by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"]) |
363 by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"]) |
364 |
364 |
365 instance |
365 instance |
366 apply(default) |
366 apply(default) |
367 apply(case_tac [!] x rule: abs_exhausts(3)) |
367 apply(case_tac [!] x rule: Abs_exhausts(3)) |
368 apply(simp_all) |
368 apply(simp_all) |
369 done |
369 done |
370 |
370 |
371 end |
371 end |
372 |
372 |
373 lemmas permute_abs[eqvt] = permute_Abs permute_Abs_res permute_Abs_lst |
373 lemmas permute_Abs[eqvt] = permute_Abs_set permute_Abs_res permute_Abs_lst |
374 |
374 |
375 |
375 |
376 lemma abs_swap1: |
376 lemma Abs_swap1: |
377 assumes a1: "a \<notin> (supp x) - bs" |
377 assumes a1: "a \<notin> (supp x) - bs" |
378 and a2: "b \<notin> (supp x) - bs" |
378 and a2: "b \<notin> (supp x) - bs" |
379 shows "Abs_set bs x = Abs_set ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
379 shows "Abs_set bs x = Abs_set ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
380 and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
380 and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
381 unfolding abs_eq_iff |
381 unfolding Abs_eq_iff |
382 unfolding alphas_abs |
|
383 unfolding alphas |
382 unfolding alphas |
384 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] |
383 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] |
385 unfolding fresh_star_def fresh_def |
384 unfolding fresh_star_def fresh_def |
386 unfolding swap_set_not_in[OF a1 a2] |
385 unfolding swap_set_not_in[OF a1 a2] |
387 using a1 a2 |
386 using a1 a2 |
388 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
387 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
389 (auto simp add: supp_perm swap_atom) |
388 (auto simp add: supp_perm swap_atom) |
390 |
389 |
391 lemma abs_swap2: |
390 lemma Abs_swap2: |
392 assumes a1: "a \<notin> (supp x) - (set bs)" |
391 assumes a1: "a \<notin> (supp x) - (set bs)" |
393 and a2: "b \<notin> (supp x) - (set bs)" |
392 and a2: "b \<notin> (supp x) - (set bs)" |
394 shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
393 shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)" |
395 unfolding abs_eq_iff |
394 unfolding Abs_eq_iff |
396 unfolding alphas_abs |
|
397 unfolding alphas |
395 unfolding alphas |
398 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric] |
396 unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric] |
399 unfolding fresh_star_def fresh_def |
397 unfolding fresh_star_def fresh_def |
400 unfolding swap_set_not_in[OF a1 a2] |
398 unfolding swap_set_not_in[OF a1 a2] |
401 using a1 a2 |
399 using a1 a2 |
402 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
400 by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI) |
403 (auto simp add: supp_perm swap_atom) |
401 (auto simp add: supp_perm swap_atom) |
404 |
402 |
405 lemma abs_supports: |
403 lemma Abs_supports: |
406 shows "((supp x) - as) supports (Abs_set as x)" |
404 shows "((supp x) - as) supports (Abs_set as x)" |
407 and "((supp x) - as) supports (Abs_res as x)" |
405 and "((supp x) - as) supports (Abs_res as x)" |
408 and "((supp x) - set bs) supports (Abs_lst bs x)" |
406 and "((supp x) - set bs) supports (Abs_lst bs x)" |
409 unfolding supports_def |
407 unfolding supports_def |
410 unfolding permute_abs |
408 unfolding permute_Abs |
411 by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric]) |
409 by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric]) |
412 |
410 |
413 function |
411 function |
414 supp_set :: "('a::pt) abs_set \<Rightarrow> atom set" |
412 supp_set :: "('a::pt) abs_set \<Rightarrow> atom set" |
415 where |
413 where |
416 "supp_set (Abs_set as x) = supp x - as" |
414 "supp_set (Abs_set as x) = supp x - as" |
417 apply(case_tac x rule: abs_exhausts(1)) |
415 apply(case_tac x rule: Abs_exhausts(1)) |
418 apply(simp) |
416 apply(simp) |
419 apply(simp add: abs_eq_iff alphas_abs alphas) |
417 apply(simp add: Abs_eq_iff alphas_abs alphas) |
420 done |
418 done |
421 |
419 |
422 termination supp_set |
420 termination supp_set |
423 by (auto intro!: local.termination) |
421 by (auto intro!: local.termination) |
424 |
422 |
425 function |
423 function |
426 supp_res :: "('a::pt) abs_res \<Rightarrow> atom set" |
424 supp_res :: "('a::pt) abs_res \<Rightarrow> atom set" |
427 where |
425 where |
428 "supp_res (Abs_res as x) = supp x - as" |
426 "supp_res (Abs_res as x) = supp x - as" |
429 apply(case_tac x rule: abs_exhausts(2)) |
427 apply(case_tac x rule: Abs_exhausts(2)) |
430 apply(simp) |
428 apply(simp) |
431 apply(simp add: abs_eq_iff alphas_abs alphas) |
429 apply(simp add: Abs_eq_iff alphas_abs alphas) |
432 done |
430 done |
433 |
431 |
434 termination supp_res |
432 termination supp_res |
435 by (auto intro!: local.termination) |
433 by (auto intro!: local.termination) |
436 |
434 |
437 function |
435 function |
438 supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set" |
436 supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set" |
439 where |
437 where |
440 "supp_lst (Abs_lst cs x) = (supp x) - (set cs)" |
438 "supp_lst (Abs_lst cs x) = (supp x) - (set cs)" |
441 apply(case_tac x rule: abs_exhausts(3)) |
439 apply(case_tac x rule: Abs_exhausts(3)) |
442 apply(simp) |
440 apply(simp) |
443 apply(simp add: abs_eq_iff alphas_abs alphas) |
441 apply(simp add: Abs_eq_iff alphas_abs alphas) |
444 done |
442 done |
445 |
443 |
446 termination supp_lst |
444 termination supp_lst |
447 by (auto intro!: local.termination) |
445 by (auto intro!: local.termination) |
448 |
446 |
449 lemma [eqvt]: |
447 lemma [eqvt]: |
450 shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)" |
448 shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)" |
451 and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)" |
449 and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)" |
452 and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)" |
450 and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)" |
453 apply(case_tac x rule: abs_exhausts(1)) |
451 apply(case_tac x rule: Abs_exhausts(1)) |
454 apply(simp add: supp_eqvt Diff_eqvt) |
452 apply(simp add: supp_eqvt Diff_eqvt) |
455 apply(case_tac y rule: abs_exhausts(2)) |
453 apply(case_tac y rule: Abs_exhausts(2)) |
456 apply(simp add: supp_eqvt Diff_eqvt) |
454 apply(simp add: supp_eqvt Diff_eqvt) |
457 apply(case_tac z rule: abs_exhausts(3)) |
455 apply(case_tac z rule: Abs_exhausts(3)) |
458 apply(simp add: supp_eqvt Diff_eqvt set_eqvt) |
456 apply(simp add: supp_eqvt Diff_eqvt set_eqvt) |
459 done |
457 done |
460 |
458 |
461 lemma aux_fresh: |
459 lemma Abs_fresh_aux: |
462 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_set (Abs bs x)" |
460 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_set (Abs bs x)" |
463 and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)" |
461 and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)" |
464 and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)" |
462 and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)" |
465 by (rule_tac [!] fresh_fun_eqvt_app) |
463 by (rule_tac [!] fresh_fun_eqvt_app) |
466 (simp_all only: eqvts_raw) |
464 (simp_all only: eqvts_raw) |
467 |
465 |
468 lemma supp_abs_subset1: |
466 lemma Abs_supp_subset1: |
469 assumes a: "finite (supp x)" |
467 assumes a: "finite (supp x)" |
470 shows "(supp x) - as \<subseteq> supp (Abs_set as x)" |
468 shows "(supp x) - as \<subseteq> supp (Abs_set as x)" |
471 and "(supp x) - as \<subseteq> supp (Abs_res as x)" |
469 and "(supp x) - as \<subseteq> supp (Abs_res as x)" |
472 and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)" |
470 and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)" |
473 unfolding supp_conv_fresh |
471 unfolding supp_conv_fresh |
474 by (auto dest!: aux_fresh) |
472 by (auto dest!: Abs_fresh_aux) |
475 (simp_all add: fresh_def supp_finite_atom_set a) |
473 (simp_all add: fresh_def supp_finite_atom_set a) |
476 |
474 |
477 lemma supp_abs_subset2: |
475 lemma Abs_supp_subset2: |
478 assumes a: "finite (supp x)" |
476 assumes a: "finite (supp x)" |
479 shows "supp (Abs_set as x) \<subseteq> (supp x) - as" |
477 shows "supp (Abs_set as x) \<subseteq> (supp x) - as" |
480 and "supp (Abs_res as x) \<subseteq> (supp x) - as" |
478 and "supp (Abs_res as x) \<subseteq> (supp x) - as" |
481 and "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)" |
479 and "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)" |
482 by (rule_tac [!] supp_is_subset) |
480 by (rule_tac [!] supp_is_subset) |
483 (simp_all add: abs_supports a) |
481 (simp_all add: Abs_supports a) |
484 |
482 |
485 lemma abs_finite_supp: |
483 lemma Abs_finite_supp: |
486 assumes a: "finite (supp x)" |
484 assumes a: "finite (supp x)" |
487 shows "supp (Abs_set as x) = (supp x) - as" |
485 shows "supp (Abs_set as x) = (supp x) - as" |
488 and "supp (Abs_res as x) = (supp x) - as" |
486 and "supp (Abs_res as x) = (supp x) - as" |
489 and "supp (Abs_lst bs x) = (supp x) - (set bs)" |
487 and "supp (Abs_lst bs x) = (supp x) - (set bs)" |
490 by (rule_tac [!] subset_antisym) |
488 by (rule_tac [!] subset_antisym) |
491 (simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a]) |
489 (simp_all add: Abs_supp_subset1[OF a] Abs_supp_subset2[OF a]) |
492 |
490 |
493 lemma supp_abs: |
491 lemma supp_Abs: |
494 fixes x::"'a::fs" |
492 fixes x::"'a::fs" |
495 shows "supp (Abs_set as x) = (supp x) - as" |
493 shows "supp (Abs_set as x) = (supp x) - as" |
496 and "supp (Abs_res as x) = (supp x) - as" |
494 and "supp (Abs_res as x) = (supp x) - as" |
497 and "supp (Abs_lst bs x) = (supp x) - (set bs)" |
495 and "supp (Abs_lst bs x) = (supp x) - (set bs)" |
498 by (rule_tac [!] abs_finite_supp) |
496 by (rule_tac [!] Abs_finite_supp) |
499 (simp_all add: finite_supp) |
497 (simp_all add: finite_supp) |
500 |
498 |
501 instance abs_set :: (fs) fs |
499 instance abs_set :: (fs) fs |
502 apply(default) |
500 apply(default) |
503 apply(case_tac x rule: abs_exhausts(1)) |
501 apply(case_tac x rule: Abs_exhausts(1)) |
504 apply(simp add: supp_abs finite_supp) |
502 apply(simp add: supp_Abs finite_supp) |
505 done |
503 done |
506 |
504 |
507 instance abs_res :: (fs) fs |
505 instance abs_res :: (fs) fs |
508 apply(default) |
506 apply(default) |
509 apply(case_tac x rule: abs_exhausts(2)) |
507 apply(case_tac x rule: Abs_exhausts(2)) |
510 apply(simp add: supp_abs finite_supp) |
508 apply(simp add: supp_Abs finite_supp) |
511 done |
509 done |
512 |
510 |
513 instance abs_lst :: (fs) fs |
511 instance abs_lst :: (fs) fs |
514 apply(default) |
512 apply(default) |
515 apply(case_tac x rule: abs_exhausts(3)) |
513 apply(case_tac x rule: Abs_exhausts(3)) |
516 apply(simp add: supp_abs finite_supp) |
514 apply(simp add: supp_Abs finite_supp) |
517 done |
515 done |
518 |
516 |
519 lemma abs_fresh_iff: |
517 lemma Abs_fresh_iff: |
520 fixes x::"'a::fs" |
518 fixes x::"'a::fs" |
521 shows "a \<sharp> Abs_set bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)" |
519 shows "a \<sharp> Abs_set bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)" |
522 and "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)" |
520 and "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)" |
523 and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)" |
521 and "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)" |
524 unfolding fresh_def |
522 unfolding fresh_def |
525 unfolding supp_abs |
523 unfolding supp_Abs |
526 by auto |
524 by auto |
527 |
525 |
528 lemma Abs_eq_iff: |
526 lemma Abs_fresh_star: |
529 shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y))" |
527 fixes x::"'a::fs" |
530 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
528 shows "as \<sharp>* Abs_set as x" |
531 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
529 and "as \<sharp>* Abs_res as x" |
532 by (lifting alphas_abs) |
530 and "set bs \<sharp>* Abs_lst bs x" |
|
531 unfolding fresh_star_def |
|
532 by(simp_all add: Abs_fresh_iff) |
533 |
533 |
534 |
534 |
535 section {* Infrastructure for building tuples of relations and functions *} |
535 section {* Infrastructure for building tuples of relations and functions *} |
536 |
536 |
537 fun |
537 fun |