477 |
477 |
478 lemma [quot_respect]: |
478 lemma [quot_respect]: |
479 shows "(op= ===> op= ===> alpha_abs_set) Pair Pair" |
479 shows "(op= ===> op= ===> alpha_abs_set) Pair Pair" |
480 and "(op= ===> op= ===> alpha_abs_res) Pair Pair" |
480 and "(op= ===> op= ===> alpha_abs_res) Pair Pair" |
481 and "(op= ===> op= ===> alpha_abs_lst) Pair Pair" |
481 and "(op= ===> op= ===> alpha_abs_lst) Pair Pair" |
482 unfolding fun_rel_def |
482 unfolding rel_fun_def |
483 by (auto intro: alphas_abs_refl) |
483 by (auto intro: alphas_abs_refl) |
484 |
484 |
485 lemma [quot_respect]: |
485 lemma [quot_respect]: |
486 shows "(op= ===> alpha_abs_set ===> alpha_abs_set) permute permute" |
486 shows "(op= ===> alpha_abs_set ===> alpha_abs_set) permute permute" |
487 and "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute" |
487 and "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute" |
488 and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute" |
488 and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute" |
489 unfolding fun_rel_def |
489 unfolding rel_fun_def |
490 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt) |
490 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt) |
491 |
491 |
492 lemma Abs_eq_iff: |
492 lemma Abs_eq_iff: |
493 shows "[bs]set. x = [bs']set. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (bs', y))" |
493 shows "[bs]set. x = [bs']set. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (bs', y))" |
494 and "[bs]res. x = [bs']res. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (bs', y))" |
494 and "[bs]res. x = [bs']res. y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (bs', y))" |
1043 "prod_fv fv1 fv2 (x, y) = fv1 x \<union> fv2 y" |
1043 "prod_fv fv1 fv2 (x, y) = fv1 x \<union> fv2 y" |
1044 |
1044 |
1045 definition |
1045 definition |
1046 prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)" |
1046 prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)" |
1047 where |
1047 where |
1048 "prod_alpha = prod_rel" |
1048 "prod_alpha = rel_prod" |
1049 |
1049 |
1050 lemma [quot_respect]: |
1050 lemma [quot_respect]: |
1051 shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv" |
1051 shows "((R1 ===> op =) ===> (R2 ===> op =) ===> rel_prod R1 R2 ===> op =) prod_fv prod_fv" |
1052 unfolding fun_rel_def |
1052 unfolding rel_fun_def |
1053 unfolding prod_rel_def |
1053 unfolding rel_prod_def |
1054 by auto |
1054 by auto |
1055 |
1055 |
1056 lemma [quot_preserve]: |
1056 lemma [quot_preserve]: |
1057 assumes q1: "Quotient3 R1 abs1 rep1" |
1057 assumes q1: "Quotient3 R1 abs1 rep1" |
1058 and q2: "Quotient3 R2 abs2 rep2" |
1058 and q2: "Quotient3 R2 abs2 rep2" |
1059 shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_pair rep1 rep2 ---> id) prod_fv = prod_fv" |
1059 shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_prod rep1 rep2 ---> id) prod_fv = prod_fv" |
1060 by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) |
1060 by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) |
1061 |
1061 |
1062 lemma [mono]: |
1062 lemma [mono]: |
1063 shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D" |
1063 shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D" |
1064 unfolding prod_alpha_def |
1064 unfolding prod_alpha_def |
1065 by auto |
1065 by auto |
1066 |
1066 |
1067 lemma [eqvt]: |
1067 lemma [eqvt]: |
1068 shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)" |
1068 shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)" |
1069 unfolding prod_alpha_def |
1069 unfolding prod_alpha_def |
1070 unfolding prod_rel_def |
1070 unfolding rel_prod_def |
1071 by (perm_simp) (rule refl) |
1071 by (perm_simp) (rule refl) |
1072 |
1072 |
1073 lemma [eqvt]: |
1073 lemma [eqvt]: |
1074 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)" |
1074 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)" |
1075 unfolding prod_fv.simps |
1075 unfolding prod_fv.simps |