37 unfolding convol_def Grp_def by auto |
37 unfolding convol_def Grp_def by auto |
38 |
38 |
39 definition csquare where |
39 definition csquare where |
40 "csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))" |
40 "csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))" |
41 |
41 |
42 (* The pullback of sets *) |
|
43 definition thePull where |
|
44 "thePull B1 B2 f1 f2 = {(b1,b2). b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2}" |
|
45 |
|
46 lemma wpull_thePull: |
|
47 "wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd" |
|
48 unfolding wpull_def thePull_def by auto |
|
49 |
|
50 lemma wppull_thePull: |
|
51 assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2" |
|
52 shows |
|
53 "\<exists> j. \<forall> a' \<in> thePull B1 B2 f1 f2. |
|
54 j a' \<in> A \<and> |
|
55 e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')" |
|
56 (is "\<exists> j. \<forall> a' \<in> ?A'. ?phi a' (j a')") |
|
57 proof(rule bchoice[of ?A' ?phi], default) |
|
58 fix a' assume a': "a' \<in> ?A'" |
|
59 hence "fst a' \<in> B1" unfolding thePull_def by auto |
|
60 moreover |
|
61 from a' have "snd a' \<in> B2" unfolding thePull_def by auto |
|
62 moreover have "f1 (fst a') = f2 (snd a')" |
|
63 using a' unfolding csquare_def thePull_def by auto |
|
64 ultimately show "\<exists> ja'. ?phi a' ja'" |
|
65 using assms unfolding wppull_def by blast |
|
66 qed |
|
67 |
|
68 lemma wpull_wppull: |
|
69 assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and |
|
70 1: "\<forall> a' \<in> A'. j a' \<in> A \<and> e1 (p1 (j a')) = e1 (p1' a') \<and> e2 (p2 (j a')) = e2 (p2' a')" |
|
71 shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2" |
|
72 unfolding wppull_def proof safe |
|
73 fix b1 b2 |
|
74 assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2" and f: "f1 b1 = f2 b2" |
|
75 then obtain a' where a': "a' \<in> A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'" |
|
76 using wp unfolding wpull_def by blast |
|
77 show "\<exists>a\<in>A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2" |
|
78 apply (rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto |
|
79 qed |
|
80 |
|
81 lemma wppull_id: "\<lbrakk>wpull UNIV UNIV UNIV f1 f2 p1 p2; e1 = id; e2 = id\<rbrakk> \<Longrightarrow> |
|
82 wppull UNIV UNIV UNIV f1 f2 e1 e2 p1 p2" |
|
83 by (erule wpull_wppull) auto |
|
84 |
|
85 lemma eq_alt: "op = = Grp UNIV id" |
42 lemma eq_alt: "op = = Grp UNIV id" |
86 unfolding Grp_def by auto |
43 unfolding Grp_def by auto |
87 |
44 |
88 lemma leq_conversepI: "R = op = \<Longrightarrow> R \<le> R^--1" |
45 lemma leq_conversepI: "R = op = \<Longrightarrow> R \<le> R^--1" |
89 by auto |
46 by auto |
90 |
47 |
91 lemma eq_OOI: "R = op = \<Longrightarrow> R = R OO R" |
48 lemma leq_OOI: "R = op = \<Longrightarrow> R \<le> R OO R" |
92 by auto |
49 by auto |
93 |
50 |
94 lemma OO_Grp_alt: "(Grp A f)^--1 OO Grp A g = (\<lambda>x y. \<exists>z. z \<in> A \<and> f z = x \<and> g z = y)" |
51 lemma OO_Grp_alt: "(Grp A f)^--1 OO Grp A g = (\<lambda>x y. \<exists>z. z \<in> A \<and> f z = x \<and> g z = y)" |
95 unfolding Grp_def by auto |
52 unfolding Grp_def by auto |
96 |
53 |
139 by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct2]) |
96 by (subst (asm) surjective_pairing, unfold prod.cases) (erule pick_middlep[THEN conjunct2]) |
140 |
97 |
141 lemma csquare_fstOp_sndOp: |
98 lemma csquare_fstOp_sndOp: |
142 "csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)" |
99 "csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)" |
143 unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp |
100 unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp |
144 |
|
145 lemma wppull_fstOp_sndOp: |
|
146 shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q)) |
|
147 snd fst fst snd (fstOp P Q) (sndOp P Q)" |
|
148 using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto |
|
149 |
101 |
150 lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy" |
102 lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy" |
151 by (simp split: prod.split) |
103 by (simp split: prod.split) |
152 |
104 |
153 lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy" |
105 lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy" |