46 "\<lbrakk>rel_fun R1 (rel_fun R2 (op =)) P Q; a \<in> A; b \<in> B; A \<subseteq> {(x, y). R1 x y}; B \<subseteq> {(x, y). R2 x y}\<rbrakk> \<Longrightarrow> |
46 "\<lbrakk>rel_fun R1 (rel_fun R2 (op =)) P Q; a \<in> A; b \<in> B; A \<subseteq> {(x, y). R1 x y}; B \<subseteq> {(x, y). R2 x y}\<rbrakk> \<Longrightarrow> |
47 P (fst a) (fst b) \<longleftrightarrow> Q (snd a) (snd b)" |
47 P (fst a) (fst b) \<longleftrightarrow> Q (snd a) (snd b)" |
48 unfolding rel_fun_def by (blast dest!: Collect_splitD) |
48 unfolding rel_fun_def by (blast dest!: Collect_splitD) |
49 |
49 |
50 definition collect where |
50 definition collect where |
51 "collect F x = (\<Union>f \<in> F. f x)" |
51 "collect F x = (\<Union>f \<in> F. f x)" |
52 |
52 |
53 lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y" |
53 lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y" |
54 by simp |
54 by simp |
55 |
55 |
56 lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z" |
56 lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z" |
57 by simp |
57 by simp |
58 |
58 |
59 lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f" |
59 lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f" |
60 unfolding bij_def inj_on_def by auto blast |
60 unfolding bij_def inj_on_def by auto blast |
61 |
61 |
62 (* Operator: *) |
62 (* Operator: *) |
63 definition "Gr A f = {(a, f a) | a. a \<in> A}" |
63 definition "Gr A f = {(a, f a) | a. a \<in> A}" |
64 |
64 |
65 definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)" |
65 definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)" |
69 |
69 |
70 lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)" |
70 lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)" |
71 by (rule ext) (auto simp only: comp_apply collect_def) |
71 by (rule ext) (auto simp only: comp_apply collect_def) |
72 |
72 |
73 definition convol ("\<langle>(_,/ _)\<rangle>") where |
73 definition convol ("\<langle>(_,/ _)\<rangle>") where |
74 "\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)" |
74 "\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)" |
75 |
75 |
76 lemma fst_convol: |
76 lemma fst_convol: "fst \<circ> \<langle>f, g\<rangle> = f" |
77 "fst \<circ> \<langle>f, g\<rangle> = f" |
77 apply(rule ext) |
78 apply(rule ext) |
78 unfolding convol_def by simp |
79 unfolding convol_def by simp |
79 |
80 |
80 lemma snd_convol: "snd \<circ> \<langle>f, g\<rangle> = g" |
81 lemma snd_convol: |
81 apply(rule ext) |
82 "snd \<circ> \<langle>f, g\<rangle> = g" |
82 unfolding convol_def by simp |
83 apply(rule ext) |
|
84 unfolding convol_def by simp |
|
85 |
83 |
86 lemma convol_mem_GrpI: |
84 lemma convol_mem_GrpI: |
87 "x \<in> A \<Longrightarrow> \<langle>id, g\<rangle> x \<in> (Collect (split (Grp A g)))" |
85 "x \<in> A \<Longrightarrow> \<langle>id, g\<rangle> x \<in> (Collect (split (Grp A g)))" |
88 unfolding convol_def Grp_def by auto |
86 unfolding convol_def Grp_def by auto |
89 |
87 |
90 definition csquare where |
88 definition csquare where |
91 "csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))" |
89 "csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))" |
92 |
90 |
93 lemma eq_alt: "op = = Grp UNIV id" |
91 lemma eq_alt: "op = = Grp UNIV id" |
94 unfolding Grp_def by auto |
92 unfolding Grp_def by auto |
95 |
93 |
96 lemma leq_conversepI: "R = op = \<Longrightarrow> R \<le> R^--1" |
94 lemma leq_conversepI: "R = op = \<Longrightarrow> R \<le> R^--1" |
97 by auto |
95 by auto |
98 |
96 |
99 lemma leq_OOI: "R = op = \<Longrightarrow> R \<le> R OO R" |
97 lemma leq_OOI: "R = op = \<Longrightarrow> R \<le> R OO R" |
101 |
99 |
102 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)" |
100 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)" |
103 unfolding Grp_def by auto |
101 unfolding Grp_def by auto |
104 |
102 |
105 lemma Grp_UNIV_id: "f = id \<Longrightarrow> (Grp UNIV f)^--1 OO Grp UNIV f = Grp UNIV f" |
103 lemma Grp_UNIV_id: "f = id \<Longrightarrow> (Grp UNIV f)^--1 OO Grp UNIV f = Grp UNIV f" |
106 unfolding Grp_def by auto |
104 unfolding Grp_def by auto |
107 |
105 |
108 lemma Grp_UNIV_idI: "x = y \<Longrightarrow> Grp UNIV id x y" |
106 lemma Grp_UNIV_idI: "x = y \<Longrightarrow> Grp UNIV id x y" |
109 unfolding Grp_def by auto |
107 unfolding Grp_def by auto |
110 |
108 |
111 lemma Grp_mono: "A \<le> B \<Longrightarrow> Grp A f \<le> Grp B f" |
109 lemma Grp_mono: "A \<le> B \<Longrightarrow> Grp A f \<le> Grp B f" |
112 unfolding Grp_def by auto |
110 unfolding Grp_def by auto |
113 |
111 |
114 lemma GrpI: "\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> Grp A f x y" |
112 lemma GrpI: "\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> Grp A f x y" |
115 unfolding Grp_def by auto |
113 unfolding Grp_def by auto |
116 |
114 |
117 lemma GrpE: "Grp A f x y \<Longrightarrow> (\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R" |
115 lemma GrpE: "Grp A f x y \<Longrightarrow> (\<lbrakk>f x = y; x \<in> A\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R" |
118 unfolding Grp_def by auto |
116 unfolding Grp_def by auto |
119 |
117 |
120 lemma Collect_split_Grp_eqD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z" |
118 lemma Collect_split_Grp_eqD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z" |
121 unfolding Grp_def comp_def by auto |
119 unfolding Grp_def comp_def by auto |
122 |
120 |
123 lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> A" |
121 lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> A" |
124 unfolding Grp_def comp_def by auto |
122 unfolding Grp_def comp_def by auto |
125 |
123 |
126 definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)" |
124 definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)" |
127 |
125 |
128 lemma pick_middlep: |
126 lemma pick_middlep: |
129 "(P OO Q) a c \<Longrightarrow> P a (pick_middlep P Q a c) \<and> Q (pick_middlep P Q a c) c" |
127 "(P OO Q) a c \<Longrightarrow> P a (pick_middlep P Q a c) \<and> Q (pick_middlep P Q a c) c" |
130 unfolding pick_middlep_def apply(rule someI_ex) by auto |
128 unfolding pick_middlep_def apply(rule someI_ex) by auto |
131 |
129 |
132 definition fstOp where "fstOp P Q ac = (fst ac, pick_middlep P Q (fst ac) (snd ac))" |
130 definition fstOp where |
133 definition sndOp where "sndOp P Q ac = (pick_middlep P Q (fst ac) (snd ac), (snd ac))" |
131 "fstOp P Q ac = (fst ac, pick_middlep P Q (fst ac) (snd ac))" |
|
132 |
|
133 definition sndOp where |
|
134 "sndOp P Q ac = (pick_middlep P Q (fst ac) (snd ac), (snd ac))" |
134 |
135 |
135 lemma fstOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (split P)" |
136 lemma fstOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> fstOp P Q ac \<in> Collect (split P)" |
136 unfolding fstOp_def mem_Collect_eq |
137 unfolding fstOp_def mem_Collect_eq |
137 by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct1]) |
138 by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct1]) |
138 |
139 |
139 lemma fst_fstOp: "fst bc = (fst \<circ> fstOp P Q) bc" |
140 lemma fst_fstOp: "fst bc = (fst \<circ> fstOp P Q) bc" |
140 unfolding comp_def fstOp_def by simp |
141 unfolding comp_def fstOp_def by simp |
141 |
142 |
142 lemma snd_sndOp: "snd bc = (snd \<circ> sndOp P Q) bc" |
143 lemma snd_sndOp: "snd bc = (snd \<circ> sndOp P Q) bc" |
143 unfolding comp_def sndOp_def by simp |
144 unfolding comp_def sndOp_def by simp |
144 |
145 |
145 lemma sndOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (split Q)" |
146 lemma sndOp_in: "ac \<in> Collect (split (P OO Q)) \<Longrightarrow> sndOp P Q ac \<in> Collect (split Q)" |
146 unfolding sndOp_def mem_Collect_eq |
147 unfolding sndOp_def mem_Collect_eq |
147 by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2]) |
148 by (subst (asm) surjective_pairing, unfold prod.case) (erule pick_middlep[THEN conjunct2]) |
148 |
149 |
149 lemma csquare_fstOp_sndOp: |
150 lemma csquare_fstOp_sndOp: |
150 "csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)" |
151 "csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)" |
151 unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp |
152 unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp |
152 |
153 |
153 lemma snd_fst_flip: "snd xy = (fst \<circ> (%(x, y). (y, x))) xy" |
154 lemma snd_fst_flip: "snd xy = (fst \<circ> (%(x, y). (y, x))) xy" |
154 by (simp split: prod.split) |
155 by (simp split: prod.split) |
155 |
156 |
156 lemma fst_snd_flip: "fst xy = (snd \<circ> (%(x, y). (y, x))) xy" |
157 lemma fst_snd_flip: "fst xy = (snd \<circ> (%(x, y). (y, x))) xy" |
157 by (simp split: prod.split) |
158 by (simp split: prod.split) |
158 |
159 |
159 lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)" |
160 lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)" |
160 by auto |
161 by auto |
161 |
162 |
162 lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (split A) \<subseteq> Collect (split B)" |
163 lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (split A) \<subseteq> Collect (split B)" |
163 by auto |
164 by auto |
164 |
165 |
165 lemma Collect_split_mono_strong: |
166 lemma Collect_split_mono_strong: |
166 "\<lbrakk>X = fst ` A; Y = snd ` A; \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b; A \<subseteq> Collect (split P)\<rbrakk> \<Longrightarrow> |
167 "\<lbrakk>X = fst ` A; Y = snd ` A; \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b; A \<subseteq> Collect (split P)\<rbrakk> \<Longrightarrow> |
167 A \<subseteq> Collect (split Q)" |
168 A \<subseteq> Collect (split Q)" |
168 by fastforce |
169 by fastforce |
169 |
170 |
170 |
171 |
171 lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b" |
172 lemma predicate2_eqD: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b" |
172 by simp |
173 by simp |
173 |
174 |
174 lemma case_sum_o_inj: |
175 lemma case_sum_o_inj: "case_sum f g \<circ> Inl = f" "case_sum f g \<circ> Inr = g" |
175 "case_sum f g \<circ> Inl = f" |
176 by auto |
176 "case_sum f g \<circ> Inr = g" |
177 |
177 by auto |
178 lemma map_sum_o_inj: "map_sum f g o Inl = Inl o f" "map_sum f g o Inr = Inr o g" |
178 |
179 by auto |
179 lemma map_sum_o_inj: |
|
180 "map_sum f g o Inl = Inl o f" |
|
181 "map_sum f g o Inr = Inr o g" |
|
182 by auto |
|
183 |
180 |
184 lemma card_order_csum_cone_cexp_def: |
181 lemma card_order_csum_cone_cexp_def: |
185 "card_order r \<Longrightarrow> ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 \<union> {Inr ()})|" |
182 "card_order r \<Longrightarrow> ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 \<union> {Inr ()})|" |
186 unfolding cexp_def cone_def Field_csum Field_card_of by (auto dest: Field_card_order) |
183 unfolding cexp_def cone_def Field_csum Field_card_of by (auto dest: Field_card_order) |
187 |
184 |
188 lemma If_the_inv_into_in_Func: |
185 lemma If_the_inv_into_in_Func: |
189 "\<lbrakk>inj_on g C; C \<subseteq> B \<union> {x}\<rbrakk> \<Longrightarrow> |
186 "\<lbrakk>inj_on g C; C \<subseteq> B \<union> {x}\<rbrakk> \<Longrightarrow> |
190 (\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<in> Func UNIV (B \<union> {x})" |
187 (\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<in> Func UNIV (B \<union> {x})" |
191 unfolding Func_def by (auto dest: the_inv_into_into) |
188 unfolding Func_def by (auto dest: the_inv_into_into) |
192 |
189 |
193 lemma If_the_inv_into_f_f: |
190 lemma If_the_inv_into_f_f: |
194 "\<lbrakk>i \<in> C; inj_on g C\<rbrakk> \<Longrightarrow> |
191 "\<lbrakk>i \<in> C; inj_on g C\<rbrakk> \<Longrightarrow> ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<circ> g) i = id i" |
195 ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<circ> g) i = id i" |
192 unfolding Func_def by (auto elim: the_inv_into_f_f) |
196 unfolding Func_def by (auto elim: the_inv_into_f_f) |
|
197 |
193 |
198 lemma the_inv_f_o_f_id: "inj f \<Longrightarrow> (the_inv f \<circ> f) z = id z" |
194 lemma the_inv_f_o_f_id: "inj f \<Longrightarrow> (the_inv f \<circ> f) z = id z" |
199 by (simp add: the_inv_f_f) |
195 by (simp add: the_inv_f_f) |
200 |
196 |
201 lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y" |
197 lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y" |