558 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)" |
558 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)" |
559 unfolding prod_fv.simps |
559 unfolding prod_fv.simps |
560 by (perm_simp) (rule refl) |
560 by (perm_simp) (rule refl) |
561 |
561 |
562 |
562 |
563 |
563 (* Below seems to be not needed *) |
564 |
564 |
565 section {* BELOW is stuff that may or may not be needed *} |
565 (* |
566 |
|
567 lemma supp_atom_image: |
|
568 fixes as::"'a::at_base set" |
|
569 shows "supp (atom ` as) = supp as" |
|
570 apply(simp add: supp_def) |
|
571 apply(simp add: image_eqvt) |
|
572 apply(simp add: eqvts_raw) |
|
573 apply(simp add: atom_image_cong) |
|
574 done |
|
575 |
|
576 lemma swap_atom_image_fresh: |
|
577 "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn" |
|
578 apply (simp add: fresh_def) |
|
579 apply (simp add: supp_atom_image) |
|
580 apply (fold fresh_def) |
|
581 apply (simp add: swap_fresh_fresh) |
|
582 done |
|
583 |
|
584 (* TODO: The following lemmas can be moved somewhere... *) |
|
585 |
|
586 lemma Abs_eq_iff: |
566 lemma Abs_eq_iff: |
587 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
567 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
588 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
568 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
589 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
569 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
590 by (lifting alphas_abs) |
570 by (lifting alphas_abs) |
596 lemma split_prs2[quot_preserve]: |
576 lemma split_prs2[quot_preserve]: |
597 assumes q1: "Quotient R1 Abs1 Rep1" |
577 assumes q1: "Quotient R1 Abs1 Rep1" |
598 and q2: "Quotient R2 Abs2 Rep2" |
578 and q2: "Quotient R2 Abs2 Rep2" |
599 shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split" |
579 shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split" |
600 by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
580 by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
601 |
581 *) |
602 lemma alphas2: |
|
603 "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) = |
|
604 (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 |
|
605 \<and> pi \<bullet> bs = cs)" |
|
606 "(bs, x1, x2) \<approx>res (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) = |
|
607 (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2)" |
|
608 "(bsl, x1, x2) \<approx>lst (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (csl, y1, y2) = |
|
609 (f1 x1 \<union> f2 x2 - set bsl = f1 y1 \<union> f2 y2 - set csl \<and> (f1 x1 \<union> f2 x2 - set bsl) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 |
|
610 \<and> pi \<bullet> bsl = csl)" |
|
611 by (simp_all add: alphas) |
|
612 |
|
613 lemma alphas3: |
|
614 "(bsl, x1, x2, x3) \<approx>lst (\<lambda>(x1, y1, z1) (x2, y2, z2). R1 x1 x2 \<and> R2 y1 y2 \<and> R3 z1 z2) (\<lambda>(a, b, c). f1 a \<union> (f2 b \<union> f3 c)) pi (csl, y1, y2, y3) = (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl = f1 y1 \<union> (f2 y2 \<union> f3 y3) - set csl \<and> |
|
615 (f1 x1 \<union> (f2 x2 \<union> f3 x3) - set bsl) \<sharp>* pi \<and> |
|
616 R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 \<and> R3 (pi \<bullet> x3) y3 \<and> pi \<bullet> bsl = csl)" |
|
617 by (simp add: alphas) |
|
618 |
582 |
619 |
583 |
620 end |
584 end |
621 |
585 |