187 lemma reflpD [dest?]: |
183 lemma reflpD [dest?]: |
188 assumes "reflp r" |
184 assumes "reflp r" |
189 shows "r x x" |
185 shows "r x x" |
190 using assms by (auto elim: reflpE) |
186 using assms by (auto elim: reflpE) |
191 |
187 |
192 lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \<inter> B) (r \<inter> s)" |
188 lemma refl_on_Int: "refl_on A r \<Longrightarrow> refl_on B s \<Longrightarrow> refl_on (A \<inter> B) (r \<inter> s)" |
193 by (unfold refl_on_def) blast |
189 unfolding refl_on_def by blast |
194 |
190 |
195 lemma reflp_inf: |
191 lemma reflp_inf: "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<sqinter> s)" |
196 "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<sqinter> s)" |
|
197 by (auto intro: reflpI elim: reflpE) |
192 by (auto intro: reflpI elim: reflpE) |
198 |
193 |
199 lemma refl_on_Un: "refl_on A r ==> refl_on B s ==> refl_on (A \<union> B) (r \<union> s)" |
194 lemma refl_on_Un: "refl_on A r \<Longrightarrow> refl_on B s \<Longrightarrow> refl_on (A \<union> B) (r \<union> s)" |
200 by (unfold refl_on_def) blast |
195 unfolding refl_on_def by blast |
201 |
196 |
202 lemma reflp_sup: |
197 lemma reflp_sup: "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<squnion> s)" |
203 "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<squnion> s)" |
|
204 by (auto intro: reflpI elim: reflpE) |
198 by (auto intro: reflpI elim: reflpE) |
205 |
199 |
206 lemma refl_on_INTER: |
200 lemma refl_on_INTER: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (INTER S A) (INTER S r)" |
207 "ALL x:S. refl_on (A x) (r x) ==> refl_on (INTER S A) (INTER S r)" |
201 unfolding refl_on_def by fast |
208 by (unfold refl_on_def) fast |
202 |
209 |
203 lemma refl_on_UNION: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (UNION S A) (UNION S r)" |
210 lemma refl_on_UNION: |
204 unfolding refl_on_def by blast |
211 "ALL x:S. refl_on (A x) (r x) \<Longrightarrow> refl_on (UNION S A) (UNION S r)" |
|
212 by (unfold refl_on_def) blast |
|
213 |
205 |
214 lemma refl_on_empty [simp]: "refl_on {} {}" |
206 lemma refl_on_empty [simp]: "refl_on {} {}" |
215 by (simp add:refl_on_def) |
207 by (simp add: refl_on_def) |
216 |
208 |
217 lemma refl_on_def' [nitpick_unfold, code]: |
209 lemma refl_on_def' [nitpick_unfold, code]: |
218 "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)" |
210 "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)" |
219 by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2) |
211 by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2) |
220 |
212 |
221 lemma reflp_equality [simp]: "reflp op =" |
213 lemma reflp_equality [simp]: "reflp op =" |
222 by(simp add: reflp_def) |
214 by (simp add: reflp_def) |
223 |
215 |
224 lemma reflp_mono: "\<lbrakk> reflp R; \<And>x y. R x y \<longrightarrow> Q x y \<rbrakk> \<Longrightarrow> reflp Q" |
216 lemma reflp_mono: "reflp R \<Longrightarrow> (\<And>x y. R x y \<longrightarrow> Q x y) \<Longrightarrow> reflp Q" |
225 by(auto intro: reflpI dest: reflpD) |
217 by (auto intro: reflpI dest: reflpD) |
226 |
218 |
227 |
219 |
228 subsubsection \<open>Irreflexivity\<close> |
220 subsubsection \<open>Irreflexivity\<close> |
229 |
221 |
230 definition irrefl :: "'a rel \<Rightarrow> bool" |
222 definition irrefl :: "'a rel \<Rightarrow> bool" |
231 where |
223 where "irrefl r \<longleftrightarrow> (\<forall>a. (a, a) \<notin> r)" |
232 "irrefl r \<longleftrightarrow> (\<forall>a. (a, a) \<notin> r)" |
|
233 |
224 |
234 definition irreflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
225 definition irreflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
235 where |
226 where "irreflp R \<longleftrightarrow> (\<forall>a. \<not> R a a)" |
236 "irreflp R \<longleftrightarrow> (\<forall>a. \<not> R a a)" |
227 |
237 |
228 lemma irreflp_irrefl_eq [pred_set_conv]: "irreflp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> irrefl R" |
238 lemma irreflp_irrefl_eq [pred_set_conv]: |
|
239 "irreflp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> irrefl R" |
|
240 by (simp add: irrefl_def irreflp_def) |
229 by (simp add: irrefl_def irreflp_def) |
241 |
230 |
242 lemma irreflI [intro?]: |
231 lemma irreflI [intro?]: "(\<And>a. (a, a) \<notin> R) \<Longrightarrow> irrefl R" |
243 "(\<And>a. (a, a) \<notin> R) \<Longrightarrow> irrefl R" |
|
244 by (simp add: irrefl_def) |
232 by (simp add: irrefl_def) |
245 |
233 |
246 lemma irreflpI [intro?]: |
234 lemma irreflpI [intro?]: "(\<And>a. \<not> R a a) \<Longrightarrow> irreflp R" |
247 "(\<And>a. \<not> R a a) \<Longrightarrow> irreflp R" |
|
248 by (fact irreflI [to_pred]) |
235 by (fact irreflI [to_pred]) |
249 |
236 |
250 lemma irrefl_distinct [code]: |
237 lemma irrefl_distinct [code]: "irrefl r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<noteq> b)" |
251 "irrefl r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<noteq> b)" |
|
252 by (auto simp add: irrefl_def) |
238 by (auto simp add: irrefl_def) |
253 |
239 |
254 |
240 |
255 subsubsection \<open>Asymmetry\<close> |
241 subsubsection \<open>Asymmetry\<close> |
256 |
242 |
257 inductive asym :: "'a rel \<Rightarrow> bool" |
243 inductive asym :: "'a rel \<Rightarrow> bool" |
258 where |
244 where asymI: "irrefl R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R" |
259 asymI: "irrefl R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R" |
|
260 |
245 |
261 inductive asymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
246 inductive asymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
262 where |
247 where asympI: "irreflp R \<Longrightarrow> (\<And>a b. R a b \<Longrightarrow> \<not> R b a) \<Longrightarrow> asymp R" |
263 asympI: "irreflp R \<Longrightarrow> (\<And>a b. R a b \<Longrightarrow> \<not> R b a) \<Longrightarrow> asymp R" |
248 |
264 |
249 lemma asymp_asym_eq [pred_set_conv]: "asymp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> asym R" |
265 lemma asymp_asym_eq [pred_set_conv]: |
|
266 "asymp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> asym R" |
|
267 by (auto intro!: asymI asympI elim: asym.cases asymp.cases simp add: irreflp_irrefl_eq) |
250 by (auto intro!: asymI asympI elim: asym.cases asymp.cases simp add: irreflp_irrefl_eq) |
268 |
251 |
269 |
252 |
270 subsubsection \<open>Symmetry\<close> |
253 subsubsection \<open>Symmetry\<close> |
271 |
254 |
272 definition sym :: "'a rel \<Rightarrow> bool" |
255 definition sym :: "'a rel \<Rightarrow> bool" |
273 where |
256 where "sym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r)" |
274 "sym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r)" |
|
275 |
257 |
276 definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
258 definition symp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
277 where |
259 where "symp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> r y x)" |
278 "symp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> r y x)" |
260 |
279 |
261 lemma symp_sym_eq [pred_set_conv]: "symp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym r" |
280 lemma symp_sym_eq [pred_set_conv]: |
|
281 "symp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym r" |
|
282 by (simp add: sym_def symp_def) |
262 by (simp add: sym_def symp_def) |
283 |
263 |
284 lemma symI [intro?]: |
264 lemma symI [intro?]: "(\<And>a b. (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r) \<Longrightarrow> sym r" |
285 "(\<And>a b. (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r) \<Longrightarrow> sym r" |
|
286 by (unfold sym_def) iprover |
265 by (unfold sym_def) iprover |
287 |
266 |
288 lemma sympI [intro?]: |
267 lemma sympI [intro?]: "(\<And>a b. r a b \<Longrightarrow> r b a) \<Longrightarrow> symp r" |
289 "(\<And>a b. r a b \<Longrightarrow> r b a) \<Longrightarrow> symp r" |
|
290 by (fact symI [to_pred]) |
268 by (fact symI [to_pred]) |
291 |
269 |
292 lemma symE: |
270 lemma symE: |
293 assumes "sym r" and "(b, a) \<in> r" |
271 assumes "sym r" and "(b, a) \<in> r" |
294 obtains "(a, b) \<in> r" |
272 obtains "(a, b) \<in> r" |
307 lemma sympD [dest?]: |
285 lemma sympD [dest?]: |
308 assumes "symp r" and "r b a" |
286 assumes "symp r" and "r b a" |
309 shows "r a b" |
287 shows "r a b" |
310 using assms by (rule symD [to_pred]) |
288 using assms by (rule symD [to_pred]) |
311 |
289 |
312 lemma sym_Int: |
290 lemma sym_Int: "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<inter> s)" |
313 "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<inter> s)" |
|
314 by (fast intro: symI elim: symE) |
291 by (fast intro: symI elim: symE) |
315 |
292 |
316 lemma symp_inf: |
293 lemma symp_inf: "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<sqinter> s)" |
317 "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<sqinter> s)" |
|
318 by (fact sym_Int [to_pred]) |
294 by (fact sym_Int [to_pred]) |
319 |
295 |
320 lemma sym_Un: |
296 lemma sym_Un: "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<union> s)" |
321 "sym r \<Longrightarrow> sym s \<Longrightarrow> sym (r \<union> s)" |
|
322 by (fast intro: symI elim: symE) |
297 by (fast intro: symI elim: symE) |
323 |
298 |
324 lemma symp_sup: |
299 lemma symp_sup: "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<squnion> s)" |
325 "symp r \<Longrightarrow> symp s \<Longrightarrow> symp (r \<squnion> s)" |
|
326 by (fact sym_Un [to_pred]) |
300 by (fact sym_Un [to_pred]) |
327 |
301 |
328 lemma sym_INTER: |
302 lemma sym_INTER: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (INTER S r)" |
329 "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (INTER S r)" |
|
330 by (fast intro: symI elim: symE) |
303 by (fast intro: symI elim: symE) |
331 |
304 |
332 lemma symp_INF: |
305 lemma symp_INF: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFIMUM S r)" |
333 "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (INFIMUM S r)" |
|
334 by (fact sym_INTER [to_pred]) |
306 by (fact sym_INTER [to_pred]) |
335 |
307 |
336 lemma sym_UNION: |
308 lemma sym_UNION: "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (UNION S r)" |
337 "\<forall>x\<in>S. sym (r x) \<Longrightarrow> sym (UNION S r)" |
|
338 by (fast intro: symI elim: symE) |
309 by (fast intro: symI elim: symE) |
339 |
310 |
340 lemma symp_SUP: |
311 lemma symp_SUP: "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPREMUM S r)" |
341 "\<forall>x\<in>S. symp (r x) \<Longrightarrow> symp (SUPREMUM S r)" |
|
342 by (fact sym_UNION [to_pred]) |
312 by (fact sym_UNION [to_pred]) |
343 |
313 |
344 |
314 |
345 subsubsection \<open>Antisymmetry\<close> |
315 subsubsection \<open>Antisymmetry\<close> |
346 |
316 |
347 definition antisym :: "'a rel \<Rightarrow> bool" |
317 definition antisym :: "'a rel \<Rightarrow> bool" |
348 where |
318 where "antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)" |
349 "antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)" |
|
350 |
319 |
351 abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
320 abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
352 where -- \<open>FIXME proper logical operation\<close> |
321 where "antisymP r \<equiv> antisym {(x, y). r x y}" (* FIXME proper logical operation *) |
353 "antisymP r \<equiv> antisym {(x, y). r x y}" |
322 |
354 |
323 lemma antisymI [intro?]: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r" |
355 lemma antisymI [intro?]: |
324 unfolding antisym_def by iprover |
356 "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r" |
325 |
357 by (unfold antisym_def) iprover |
326 lemma antisymD [dest?]: "antisym r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r \<Longrightarrow> a = b" |
358 |
327 unfolding antisym_def by iprover |
359 lemma antisymD [dest?]: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b" |
328 |
360 by (unfold antisym_def) iprover |
329 lemma antisym_subset: "r \<subseteq> s \<Longrightarrow> antisym s \<Longrightarrow> antisym r" |
361 |
330 unfolding antisym_def by blast |
362 lemma antisym_subset: "r \<subseteq> s ==> antisym s ==> antisym r" |
|
363 by (unfold antisym_def) blast |
|
364 |
331 |
365 lemma antisym_empty [simp]: "antisym {}" |
332 lemma antisym_empty [simp]: "antisym {}" |
366 by (unfold antisym_def) blast |
333 unfolding antisym_def by blast |
367 |
334 |
368 lemma antisymP_equality [simp]: "antisymP op =" |
335 lemma antisymP_equality [simp]: "antisymP op =" |
369 by(auto intro: antisymI) |
336 by (auto intro: antisymI) |
370 |
337 |
371 |
338 |
372 subsubsection \<open>Transitivity\<close> |
339 subsubsection \<open>Transitivity\<close> |
373 |
340 |
374 definition trans :: "'a rel \<Rightarrow> bool" |
341 definition trans :: "'a rel \<Rightarrow> bool" |
375 where |
342 where "trans r \<longleftrightarrow> (\<forall>x y z. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (x, z) \<in> r)" |
376 "trans r \<longleftrightarrow> (\<forall>x y z. (x, y) \<in> r \<longrightarrow> (y, z) \<in> r \<longrightarrow> (x, z) \<in> r)" |
|
377 |
343 |
378 definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
344 definition transp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
379 where |
345 where "transp r \<longleftrightarrow> (\<forall>x y z. r x y \<longrightarrow> r y z \<longrightarrow> r x z)" |
380 "transp r \<longleftrightarrow> (\<forall>x y z. r x y \<longrightarrow> r y z \<longrightarrow> r x z)" |
346 |
381 |
347 lemma transp_trans_eq [pred_set_conv]: "transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans r" |
382 lemma transp_trans_eq [pred_set_conv]: |
|
383 "transp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> trans r" |
|
384 by (simp add: trans_def transp_def) |
348 by (simp add: trans_def transp_def) |
385 |
349 |
386 lemma transI [intro?]: |
350 lemma transI [intro?]: "(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r" |
387 "(\<And>x y z. (x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r) \<Longrightarrow> trans r" |
|
388 by (unfold trans_def) iprover |
351 by (unfold trans_def) iprover |
389 |
352 |
390 lemma transpI [intro?]: |
353 lemma transpI [intro?]: "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r" |
391 "(\<And>x y z. r x y \<Longrightarrow> r y z \<Longrightarrow> r x z) \<Longrightarrow> transp r" |
|
392 by (fact transI [to_pred]) |
354 by (fact transI [to_pred]) |
393 |
355 |
394 lemma transE: |
356 lemma transE: |
395 assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r" |
357 assumes "trans r" and "(x, y) \<in> r" and "(y, z) \<in> r" |
396 obtains "(x, z) \<in> r" |
358 obtains "(x, z) \<in> r" |
409 lemma transpD [dest?]: |
371 lemma transpD [dest?]: |
410 assumes "transp r" and "r x y" and "r y z" |
372 assumes "transp r" and "r x y" and "r y z" |
411 shows "r x z" |
373 shows "r x z" |
412 using assms by (rule transD [to_pred]) |
374 using assms by (rule transD [to_pred]) |
413 |
375 |
414 lemma trans_Int: |
376 lemma trans_Int: "trans r \<Longrightarrow> trans s \<Longrightarrow> trans (r \<inter> s)" |
415 "trans r \<Longrightarrow> trans s \<Longrightarrow> trans (r \<inter> s)" |
|
416 by (fast intro: transI elim: transE) |
377 by (fast intro: transI elim: transE) |
417 |
378 |
418 lemma transp_inf: |
379 lemma transp_inf: "transp r \<Longrightarrow> transp s \<Longrightarrow> transp (r \<sqinter> s)" |
419 "transp r \<Longrightarrow> transp s \<Longrightarrow> transp (r \<sqinter> s)" |
|
420 by (fact trans_Int [to_pred]) |
380 by (fact trans_Int [to_pred]) |
421 |
381 |
422 lemma trans_INTER: |
382 lemma trans_INTER: "\<forall>x\<in>S. trans (r x) \<Longrightarrow> trans (INTER S r)" |
423 "\<forall>x\<in>S. trans (r x) \<Longrightarrow> trans (INTER S r)" |
|
424 by (fast intro: transI elim: transD) |
383 by (fast intro: transI elim: transD) |
425 |
384 |
426 (* FIXME thm trans_INTER [to_pred] *) |
385 (* FIXME thm trans_INTER [to_pred] *) |
427 |
386 |
428 lemma trans_join [code]: |
387 lemma trans_join [code]: "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)" |
429 "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)" |
|
430 by (auto simp add: trans_def) |
388 by (auto simp add: trans_def) |
431 |
389 |
432 lemma transp_trans: |
390 lemma transp_trans: "transp r \<longleftrightarrow> trans {(x, y). r x y}" |
433 "transp r \<longleftrightarrow> trans {(x, y). r x y}" |
|
434 by (simp add: trans_def transp_def) |
391 by (simp add: trans_def transp_def) |
435 |
392 |
436 lemma transp_equality [simp]: "transp op =" |
393 lemma transp_equality [simp]: "transp op =" |
437 by(auto intro: transpI) |
394 by (auto intro: transpI) |
438 |
395 |
439 |
396 |
440 subsubsection \<open>Totality\<close> |
397 subsubsection \<open>Totality\<close> |
441 |
398 |
442 definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" |
399 definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" |
443 where |
400 where "total_on A r \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x \<noteq> y \<longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r)" |
444 "total_on A r \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x \<noteq> y \<longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r)" |
|
445 |
401 |
446 abbreviation "total \<equiv> total_on UNIV" |
402 abbreviation "total \<equiv> total_on UNIV" |
447 |
403 |
448 lemma total_on_empty [simp]: "total_on {} r" |
404 lemma total_on_empty [simp]: "total_on {} r" |
449 by (simp add: total_on_def) |
405 by (simp add: total_on_def) |
450 |
406 |
451 |
407 |
452 subsubsection \<open>Single valued relations\<close> |
408 subsubsection \<open>Single valued relations\<close> |
453 |
409 |
454 definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool" |
410 definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool" |
455 where |
411 where "single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))" |
456 "single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))" |
|
457 |
412 |
458 abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
413 abbreviation single_valuedP :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" |
459 where -- \<open>FIXME proper logical operation\<close> |
414 where "single_valuedP r \<equiv> single_valued {(x, y). r x y}" (* FIXME proper logical operation *) |
460 "single_valuedP r \<equiv> single_valued {(x, y). r x y}" |
415 |
461 |
416 lemma single_valuedI: "\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z) \<Longrightarrow> single_valued r" |
462 lemma single_valuedI: |
417 unfolding single_valued_def . |
463 "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r" |
418 |
464 by (unfold single_valued_def) |
419 lemma single_valuedD: "single_valued r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, z) \<in> r \<Longrightarrow> y = z" |
465 |
|
466 lemma single_valuedD: |
|
467 "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z" |
|
468 by (simp add: single_valued_def) |
420 by (simp add: single_valued_def) |
469 |
421 |
470 lemma single_valued_empty[simp]: "single_valued {}" |
422 lemma single_valued_empty[simp]: "single_valued {}" |
471 by(simp add: single_valued_def) |
423 by (simp add: single_valued_def) |
472 |
424 |
473 lemma single_valued_subset: |
425 lemma single_valued_subset: "r \<subseteq> s \<Longrightarrow> single_valued s \<Longrightarrow> single_valued r" |
474 "r \<subseteq> s ==> single_valued s ==> single_valued r" |
426 unfolding single_valued_def by blast |
475 by (unfold single_valued_def) blast |
|
476 |
427 |
477 |
428 |
478 subsection \<open>Relation operations\<close> |
429 subsection \<open>Relation operations\<close> |
479 |
430 |
480 subsubsection \<open>The identity relation\<close> |
431 subsubsection \<open>The identity relation\<close> |
481 |
432 |
482 definition Id :: "'a rel" |
433 definition Id :: "'a rel" |
483 where |
434 where [code del]: "Id = {p. \<exists>x. p = (x, x)}" |
484 [code del]: "Id = {p. \<exists>x. p = (x, x)}" |
435 |
485 |
436 lemma IdI [intro]: "(a, a) \<in> Id" |
486 lemma IdI [intro]: "(a, a) : Id" |
|
487 by (simp add: Id_def) |
437 by (simp add: Id_def) |
488 |
438 |
489 lemma IdE [elim!]: "p : Id ==> (!!x. p = (x, x) ==> P) ==> P" |
439 lemma IdE [elim!]: "p \<in> Id \<Longrightarrow> (\<And>x. p = (x, x) \<Longrightarrow> P) \<Longrightarrow> P" |
490 by (unfold Id_def) (iprover elim: CollectE) |
440 unfolding Id_def by (iprover elim: CollectE) |
491 |
441 |
492 lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)" |
442 lemma pair_in_Id_conv [iff]: "(a, b) \<in> Id \<longleftrightarrow> a = b" |
493 by (unfold Id_def) blast |
443 unfolding Id_def by blast |
494 |
444 |
495 lemma refl_Id: "refl Id" |
445 lemma refl_Id: "refl Id" |
496 by (simp add: refl_on_def) |
446 by (simp add: refl_on_def) |
497 |
447 |
498 lemma antisym_Id: "antisym Id" |
448 lemma antisym_Id: "antisym Id" |
522 |
472 |
523 |
473 |
524 subsubsection \<open>Diagonal: identity over a set\<close> |
474 subsubsection \<open>Diagonal: identity over a set\<close> |
525 |
475 |
526 definition Id_on :: "'a set \<Rightarrow> 'a rel" |
476 definition Id_on :: "'a set \<Rightarrow> 'a rel" |
527 where |
477 where "Id_on A = (\<Union>x\<in>A. {(x, x)})" |
528 "Id_on A = (\<Union>x\<in>A. {(x, x)})" |
|
529 |
478 |
530 lemma Id_on_empty [simp]: "Id_on {} = {}" |
479 lemma Id_on_empty [simp]: "Id_on {} = {}" |
531 by (simp add: Id_on_def) |
|
532 |
|
533 lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A" |
|
534 by (simp add: Id_on_def) |
480 by (simp add: Id_on_def) |
535 |
481 |
536 lemma Id_onI [intro!]: "a : A ==> (a, a) : Id_on A" |
482 lemma Id_on_eqI: "a = b \<Longrightarrow> a \<in> A \<Longrightarrow> (a, b) \<in> Id_on A" |
|
483 by (simp add: Id_on_def) |
|
484 |
|
485 lemma Id_onI [intro!]: "a \<in> A \<Longrightarrow> (a, a) \<in> Id_on A" |
537 by (rule Id_on_eqI) (rule refl) |
486 by (rule Id_on_eqI) (rule refl) |
538 |
487 |
539 lemma Id_onE [elim!]: |
488 lemma Id_onE [elim!]: "c \<in> Id_on A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> c = (x, x) \<Longrightarrow> P) \<Longrightarrow> P" |
540 "c : Id_on A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P" |
|
541 \<comment> \<open>The general elimination rule.\<close> |
489 \<comment> \<open>The general elimination rule.\<close> |
542 by (unfold Id_on_def) (iprover elim!: UN_E singletonE) |
490 unfolding Id_on_def by (iprover elim!: UN_E singletonE) |
543 |
491 |
544 lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)" |
492 lemma Id_on_iff: "(x, y) \<in> Id_on A \<longleftrightarrow> x = y \<and> x \<in> A" |
545 by blast |
493 by blast |
546 |
494 |
547 lemma Id_on_def' [nitpick_unfold]: |
495 lemma Id_on_def' [nitpick_unfold]: "Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)" |
548 "Id_on {x. A x} = Collect (\<lambda>(x, y). x = y \<and> A x)" |
|
549 by auto |
496 by auto |
550 |
497 |
551 lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A" |
498 lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A" |
552 by blast |
499 by blast |
553 |
500 |
554 lemma refl_on_Id_on: "refl_on A (Id_on A)" |
501 lemma refl_on_Id_on: "refl_on A (Id_on A)" |
555 by (rule refl_onI [OF Id_on_subset_Times Id_onI]) |
502 by (rule refl_onI [OF Id_on_subset_Times Id_onI]) |
556 |
503 |
557 lemma antisym_Id_on [simp]: "antisym (Id_on A)" |
504 lemma antisym_Id_on [simp]: "antisym (Id_on A)" |
558 by (unfold antisym_def) blast |
505 unfolding antisym_def by blast |
559 |
506 |
560 lemma sym_Id_on [simp]: "sym (Id_on A)" |
507 lemma sym_Id_on [simp]: "sym (Id_on A)" |
561 by (rule symI) clarify |
508 by (rule symI) clarify |
562 |
509 |
563 lemma trans_Id_on [simp]: "trans (Id_on A)" |
510 lemma trans_Id_on [simp]: "trans (Id_on A)" |
564 by (fast intro: transI elim: transD) |
511 by (fast intro: transI elim: transD) |
565 |
512 |
566 lemma single_valued_Id_on [simp]: "single_valued (Id_on A)" |
513 lemma single_valued_Id_on [simp]: "single_valued (Id_on A)" |
567 by (unfold single_valued_def) blast |
514 unfolding single_valued_def by blast |
568 |
515 |
569 |
516 |
570 subsubsection \<open>Composition\<close> |
517 subsubsection \<open>Composition\<close> |
571 |
518 |
572 inductive_set relcomp :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75) |
519 inductive_set relcomp :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75) |
573 for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set" |
520 for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set" |
574 where |
521 where relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s" |
575 relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s" |
|
576 |
522 |
577 notation relcompp (infixr "OO" 75) |
523 notation relcompp (infixr "OO" 75) |
578 |
524 |
579 lemmas relcomppI = relcompp.intros |
525 lemmas relcomppI = relcompp.intros |
580 |
526 |
586 inductive_cases relcompEpair: "(a, c) \<in> r O s" |
532 inductive_cases relcompEpair: "(a, c) \<in> r O s" |
587 inductive_cases relcomppE [elim!]: "(r OO s) a c" |
533 inductive_cases relcomppE [elim!]: "(r OO s) a c" |
588 |
534 |
589 lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow> |
535 lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow> |
590 (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s \<Longrightarrow> P) \<Longrightarrow> P" |
536 (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s \<Longrightarrow> P) \<Longrightarrow> P" |
591 by (cases xz) (simp, erule relcompEpair, iprover) |
537 apply (cases xz) |
592 |
538 apply simp |
593 lemma R_O_Id [simp]: |
539 apply (erule relcompEpair) |
594 "R O Id = R" |
540 apply iprover |
|
541 done |
|
542 |
|
543 lemma R_O_Id [simp]: "R O Id = R" |
595 by fast |
544 by fast |
596 |
545 |
597 lemma Id_O_R [simp]: |
546 lemma Id_O_R [simp]: "Id O R = R" |
598 "Id O R = R" |
|
599 by fast |
547 by fast |
600 |
548 |
601 lemma relcomp_empty1 [simp]: |
549 lemma relcomp_empty1 [simp]: "{} O R = {}" |
602 "{} O R = {}" |
550 by blast |
603 by blast |
551 |
604 |
552 lemma relcompp_bot1 [simp]: "\<bottom> OO R = \<bottom>" |
605 lemma relcompp_bot1 [simp]: |
|
606 "\<bottom> OO R = \<bottom>" |
|
607 by (fact relcomp_empty1 [to_pred]) |
553 by (fact relcomp_empty1 [to_pred]) |
608 |
554 |
609 lemma relcomp_empty2 [simp]: |
555 lemma relcomp_empty2 [simp]: "R O {} = {}" |
610 "R O {} = {}" |
556 by blast |
611 by blast |
557 |
612 |
558 lemma relcompp_bot2 [simp]: "R OO \<bottom> = \<bottom>" |
613 lemma relcompp_bot2 [simp]: |
|
614 "R OO \<bottom> = \<bottom>" |
|
615 by (fact relcomp_empty2 [to_pred]) |
559 by (fact relcomp_empty2 [to_pred]) |
616 |
560 |
617 lemma O_assoc: |
561 lemma O_assoc: "(R O S) O T = R O (S O T)" |
618 "(R O S) O T = R O (S O T)" |
562 by blast |
619 by blast |
563 |
620 |
564 lemma relcompp_assoc: "(r OO s) OO t = r OO (s OO t)" |
621 lemma relcompp_assoc: |
|
622 "(r OO s) OO t = r OO (s OO t)" |
|
623 by (fact O_assoc [to_pred]) |
565 by (fact O_assoc [to_pred]) |
624 |
566 |
625 lemma trans_O_subset: |
567 lemma trans_O_subset: "trans r \<Longrightarrow> r O r \<subseteq> r" |
626 "trans r \<Longrightarrow> r O r \<subseteq> r" |
|
627 by (unfold trans_def) blast |
568 by (unfold trans_def) blast |
628 |
569 |
629 lemma transp_relcompp_less_eq: |
570 lemma transp_relcompp_less_eq: "transp r \<Longrightarrow> r OO r \<le> r " |
630 "transp r \<Longrightarrow> r OO r \<le> r " |
|
631 by (fact trans_O_subset [to_pred]) |
571 by (fact trans_O_subset [to_pred]) |
632 |
572 |
633 lemma relcomp_mono: |
573 lemma relcomp_mono: "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s" |
634 "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s" |
574 by blast |
635 by blast |
575 |
636 |
576 lemma relcompp_mono: "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s " |
637 lemma relcompp_mono: |
|
638 "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s " |
|
639 by (fact relcomp_mono [to_pred]) |
577 by (fact relcomp_mono [to_pred]) |
640 |
578 |
641 lemma relcomp_subset_Sigma: |
579 lemma relcomp_subset_Sigma: "r \<subseteq> A \<times> B \<Longrightarrow> s \<subseteq> B \<times> C \<Longrightarrow> r O s \<subseteq> A \<times> C" |
642 "r \<subseteq> A \<times> B \<Longrightarrow> s \<subseteq> B \<times> C \<Longrightarrow> r O s \<subseteq> A \<times> C" |
580 by blast |
643 by blast |
581 |
644 |
582 lemma relcomp_distrib [simp]: "R O (S \<union> T) = (R O S) \<union> (R O T)" |
645 lemma relcomp_distrib [simp]: |
583 by auto |
646 "R O (S \<union> T) = (R O S) \<union> (R O T)" |
584 |
647 by auto |
585 lemma relcompp_distrib [simp]: "R OO (S \<squnion> T) = R OO S \<squnion> R OO T" |
648 |
|
649 lemma relcompp_distrib [simp]: |
|
650 "R OO (S \<squnion> T) = R OO S \<squnion> R OO T" |
|
651 by (fact relcomp_distrib [to_pred]) |
586 by (fact relcomp_distrib [to_pred]) |
652 |
587 |
653 lemma relcomp_distrib2 [simp]: |
588 lemma relcomp_distrib2 [simp]: "(S \<union> T) O R = (S O R) \<union> (T O R)" |
654 "(S \<union> T) O R = (S O R) \<union> (T O R)" |
589 by auto |
655 by auto |
590 |
656 |
591 lemma relcompp_distrib2 [simp]: "(S \<squnion> T) OO R = S OO R \<squnion> T OO R" |
657 lemma relcompp_distrib2 [simp]: |
|
658 "(S \<squnion> T) OO R = S OO R \<squnion> T OO R" |
|
659 by (fact relcomp_distrib2 [to_pred]) |
592 by (fact relcomp_distrib2 [to_pred]) |
660 |
593 |
661 lemma relcomp_UNION_distrib: |
594 lemma relcomp_UNION_distrib: "s O UNION I r = (\<Union>i\<in>I. s O r i) " |
662 "s O UNION I r = (\<Union>i\<in>I. s O r i) " |
|
663 by auto |
595 by auto |
664 |
596 |
665 (* FIXME thm relcomp_UNION_distrib [to_pred] *) |
597 (* FIXME thm relcomp_UNION_distrib [to_pred] *) |
666 |
598 |
667 lemma relcomp_UNION_distrib2: |
599 lemma relcomp_UNION_distrib2: "UNION I r O s = (\<Union>i\<in>I. r i O s) " |
668 "UNION I r O s = (\<Union>i\<in>I. r i O s) " |
|
669 by auto |
600 by auto |
670 |
601 |
671 (* FIXME thm relcomp_UNION_distrib2 [to_pred] *) |
602 (* FIXME thm relcomp_UNION_distrib2 [to_pred] *) |
672 |
603 |
673 lemma single_valued_relcomp: |
604 lemma single_valued_relcomp: "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)" |
674 "single_valued r \<Longrightarrow> single_valued s \<Longrightarrow> single_valued (r O s)" |
605 unfolding single_valued_def by blast |
675 by (unfold single_valued_def) blast |
606 |
676 |
607 lemma relcomp_unfold: "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}" |
677 lemma relcomp_unfold: |
|
678 "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}" |
|
679 by (auto simp add: set_eq_iff) |
608 by (auto simp add: set_eq_iff) |
680 |
609 |
681 lemma relcompp_apply: "(R OO S) a c \<longleftrightarrow> (\<exists>b. R a b \<and> S b c)" |
610 lemma relcompp_apply: "(R OO S) a c \<longleftrightarrow> (\<exists>b. R a b \<and> S b c)" |
682 unfolding relcomp_unfold [to_pred] .. |
611 unfolding relcomp_unfold [to_pred] .. |
683 |
612 |
684 lemma eq_OO: "op= OO R = R" |
613 lemma eq_OO: "op= OO R = R" |
685 by blast |
614 by blast |
686 |
615 |
687 lemma OO_eq: "R OO op = = R" |
616 lemma OO_eq: "R OO op = = R" |
688 by blast |
617 by blast |
689 |
618 |
690 |
619 |
691 subsubsection \<open>Converse\<close> |
620 subsubsection \<open>Converse\<close> |
692 |
621 |
693 inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" ("(_\<inverse>)" [1000] 999) |
622 inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" ("(_\<inverse>)" [1000] 999) |
694 for r :: "('a \<times> 'b) set" |
623 for r :: "('a \<times> 'b) set" |
695 where |
624 where "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>" |
696 "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>" |
625 |
697 |
626 notation conversep ("(_\<inverse>\<inverse>)" [1000] 1000) |
698 notation |
|
699 conversep ("(_\<inverse>\<inverse>)" [1000] 1000) |
|
700 |
627 |
701 notation (ASCII) |
628 notation (ASCII) |
702 converse ("(_^-1)" [1000] 999) and |
629 converse ("(_^-1)" [1000] 999) and |
703 conversep ("(_^--1)" [1000] 1000) |
630 conversep ("(_^--1)" [1000] 1000) |
704 |
631 |
705 lemma converseI [sym]: |
632 lemma converseI [sym]: "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>" |
706 "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>" |
|
707 by (fact converse.intros) |
633 by (fact converse.intros) |
708 |
634 |
709 lemma conversepI (* CANDIDATE [sym] *): |
635 lemma conversepI (* CANDIDATE [sym] *): "r a b \<Longrightarrow> r\<inverse>\<inverse> b a" |
710 "r a b \<Longrightarrow> r\<inverse>\<inverse> b a" |
|
711 by (fact conversep.intros) |
636 by (fact conversep.intros) |
712 |
637 |
713 lemma converseD [sym]: |
638 lemma converseD [sym]: "(a, b) \<in> r\<inverse> \<Longrightarrow> (b, a) \<in> r" |
714 "(a, b) \<in> r\<inverse> \<Longrightarrow> (b, a) \<in> r" |
|
715 by (erule converse.cases) iprover |
639 by (erule converse.cases) iprover |
716 |
640 |
717 lemma conversepD (* CANDIDATE [sym] *): |
641 lemma conversepD (* CANDIDATE [sym] *): "r\<inverse>\<inverse> b a \<Longrightarrow> r a b" |
718 "r\<inverse>\<inverse> b a \<Longrightarrow> r a b" |
|
719 by (fact converseD [to_pred]) |
642 by (fact converseD [to_pred]) |
720 |
643 |
721 lemma converseE [elim!]: |
644 lemma converseE [elim!]: "yx \<in> r\<inverse> \<Longrightarrow> (\<And>x y. yx = (y, x) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> P) \<Longrightarrow> P" |
722 \<comment> \<open>More general than \<open>converseD\<close>, as it ``splits'' the member of the relation.\<close> |
645 \<comment> \<open>More general than \<open>converseD\<close>, as it ``splits'' the member of the relation.\<close> |
723 "yx \<in> r\<inverse> \<Longrightarrow> (\<And>x y. yx = (y, x) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> P) \<Longrightarrow> P" |
646 apply (cases yx) |
724 by (cases yx) (simp, erule converse.cases, iprover) |
647 apply simp |
|
648 apply (erule converse.cases) |
|
649 apply iprover |
|
650 done |
725 |
651 |
726 lemmas conversepE [elim!] = conversep.cases |
652 lemmas conversepE [elim!] = conversep.cases |
727 |
653 |
728 lemma converse_iff [iff]: |
654 lemma converse_iff [iff]: "(a, b) \<in> r\<inverse> \<longleftrightarrow> (b, a) \<in> r" |
729 "(a, b) \<in> r\<inverse> \<longleftrightarrow> (b, a) \<in> r" |
|
730 by (auto intro: converseI) |
655 by (auto intro: converseI) |
731 |
656 |
732 lemma conversep_iff [iff]: |
657 lemma conversep_iff [iff]: "r\<inverse>\<inverse> a b = r b a" |
733 "r\<inverse>\<inverse> a b = r b a" |
|
734 by (fact converse_iff [to_pred]) |
658 by (fact converse_iff [to_pred]) |
735 |
659 |
736 lemma converse_converse [simp]: |
660 lemma converse_converse [simp]: "(r\<inverse>)\<inverse> = r" |
737 "(r\<inverse>)\<inverse> = r" |
|
738 by (simp add: set_eq_iff) |
661 by (simp add: set_eq_iff) |
739 |
662 |
740 lemma conversep_conversep [simp]: |
663 lemma conversep_conversep [simp]: "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r" |
741 "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r" |
|
742 by (fact converse_converse [to_pred]) |
664 by (fact converse_converse [to_pred]) |
743 |
665 |
744 lemma converse_empty[simp]: "{}\<inverse> = {}" |
666 lemma converse_empty[simp]: "{}\<inverse> = {}" |
745 by auto |
667 by auto |
746 |
668 |
747 lemma converse_UNIV[simp]: "UNIV\<inverse> = UNIV" |
669 lemma converse_UNIV[simp]: "UNIV\<inverse> = UNIV" |
748 by auto |
670 by auto |
749 |
671 |
750 lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1" |
672 lemma converse_relcomp: "(r O s)\<inverse> = s\<inverse> O r\<inverse>" |
751 by blast |
673 by blast |
752 |
674 |
753 lemma converse_relcompp: "(r OO s)^--1 = s^--1 OO r^--1" |
675 lemma converse_relcompp: "(r OO s)\<inverse>\<inverse> = s\<inverse>\<inverse> OO r\<inverse>\<inverse>" |
754 by (iprover intro: order_antisym conversepI relcomppI |
676 by (iprover intro: order_antisym conversepI relcomppI elim: relcomppE dest: conversepD) |
755 elim: relcomppE dest: conversepD) |
677 |
756 |
678 lemma converse_Int: "(r \<inter> s)\<inverse> = r\<inverse> \<inter> s\<inverse>" |
757 lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1" |
679 by blast |
758 by blast |
680 |
759 |
681 lemma converse_meet: "(r \<sqinter> s)\<inverse>\<inverse> = r\<inverse>\<inverse> \<sqinter> s\<inverse>\<inverse>" |
760 lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1" |
|
761 by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD) |
682 by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD) |
762 |
683 |
763 lemma converse_Un: "(r \<union> s)^-1 = r^-1 \<union> s^-1" |
684 lemma converse_Un: "(r \<union> s)\<inverse> = r\<inverse> \<union> s\<inverse>" |
764 by blast |
685 by blast |
765 |
686 |
766 lemma converse_join: "(r \<squnion> s)^--1 = r^--1 \<squnion> s^--1" |
687 lemma converse_join: "(r \<squnion> s)\<inverse>\<inverse> = r\<inverse>\<inverse> \<squnion> s\<inverse>\<inverse>" |
767 by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD) |
688 by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD) |
768 |
689 |
769 lemma converse_INTER: "(INTER S r)^-1 = (INT x:S. (r x)^-1)" |
690 lemma converse_INTER: "(INTER S r)\<inverse> = (INT x:S. (r x)\<inverse>)" |
770 by fast |
691 by fast |
771 |
692 |
772 lemma converse_UNION: "(UNION S r)^-1 = (UN x:S. (r x)^-1)" |
693 lemma converse_UNION: "(UNION S r)\<inverse> = (UN x:S. (r x)\<inverse>)" |
773 by blast |
694 by blast |
774 |
695 |
775 lemma converse_mono[simp]: "r^-1 \<subseteq> s ^-1 \<longleftrightarrow> r \<subseteq> s" |
696 lemma converse_mono[simp]: "r\<inverse> \<subseteq> s \<inverse> \<longleftrightarrow> r \<subseteq> s" |
776 by auto |
697 by auto |
777 |
698 |
778 lemma conversep_mono[simp]: "r^--1 \<le> s ^--1 \<longleftrightarrow> r \<le> s" |
699 lemma conversep_mono[simp]: "r\<inverse>\<inverse> \<le> s \<inverse>\<inverse> \<longleftrightarrow> r \<le> s" |
779 by (fact converse_mono[to_pred]) |
700 by (fact converse_mono[to_pred]) |
780 |
701 |
781 lemma converse_inject[simp]: "r^-1 = s ^-1 \<longleftrightarrow> r = s" |
702 lemma converse_inject[simp]: "r\<inverse> = s \<inverse> \<longleftrightarrow> r = s" |
782 by auto |
703 by auto |
783 |
704 |
784 lemma conversep_inject[simp]: "r^--1 = s ^--1 \<longleftrightarrow> r = s" |
705 lemma conversep_inject[simp]: "r\<inverse>\<inverse> = s \<inverse>\<inverse> \<longleftrightarrow> r = s" |
785 by (fact converse_inject[to_pred]) |
706 by (fact converse_inject[to_pred]) |
786 |
707 |
787 lemma converse_subset_swap: "r \<subseteq> s ^-1 = (r ^-1 \<subseteq> s)" |
708 lemma converse_subset_swap: "r \<subseteq> s \<inverse> = (r \<inverse> \<subseteq> s)" |
788 by auto |
709 by auto |
789 |
710 |
790 lemma conversep_le_swap: "r \<le> s ^--1 = (r ^--1 \<le> s)" |
711 lemma conversep_le_swap: "r \<le> s \<inverse>\<inverse> = (r \<inverse>\<inverse> \<le> s)" |
791 by (fact converse_subset_swap[to_pred]) |
712 by (fact converse_subset_swap[to_pred]) |
792 |
713 |
793 lemma converse_Id [simp]: "Id^-1 = Id" |
714 lemma converse_Id [simp]: "Id\<inverse> = Id" |
794 by blast |
715 by blast |
795 |
716 |
796 lemma converse_Id_on [simp]: "(Id_on A)^-1 = Id_on A" |
717 lemma converse_Id_on [simp]: "(Id_on A)\<inverse> = Id_on A" |
797 by blast |
718 by blast |
798 |
719 |
799 lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r" |
720 lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r" |
800 by (unfold refl_on_def) auto |
721 by (auto simp: refl_on_def) |
801 |
722 |
802 lemma sym_converse [simp]: "sym (converse r) = sym r" |
723 lemma sym_converse [simp]: "sym (converse r) = sym r" |
803 by (unfold sym_def) blast |
724 unfolding sym_def by blast |
804 |
725 |
805 lemma antisym_converse [simp]: "antisym (converse r) = antisym r" |
726 lemma antisym_converse [simp]: "antisym (converse r) = antisym r" |
806 by (unfold antisym_def) blast |
727 unfolding antisym_def by blast |
807 |
728 |
808 lemma trans_converse [simp]: "trans (converse r) = trans r" |
729 lemma trans_converse [simp]: "trans (converse r) = trans r" |
809 by (unfold trans_def) blast |
730 unfolding trans_def by blast |
810 |
731 |
811 lemma sym_conv_converse_eq: "sym r = (r^-1 = r)" |
732 lemma sym_conv_converse_eq: "sym r \<longleftrightarrow> r\<inverse> = r" |
812 by (unfold sym_def) fast |
733 unfolding sym_def by fast |
813 |
734 |
814 lemma sym_Un_converse: "sym (r \<union> r^-1)" |
735 lemma sym_Un_converse: "sym (r \<union> r\<inverse>)" |
815 by (unfold sym_def) blast |
736 unfolding sym_def by blast |
816 |
737 |
817 lemma sym_Int_converse: "sym (r \<inter> r^-1)" |
738 lemma sym_Int_converse: "sym (r \<inter> r\<inverse>)" |
818 by (unfold sym_def) blast |
739 unfolding sym_def by blast |
819 |
740 |
820 lemma total_on_converse [simp]: "total_on A (r^-1) = total_on A r" |
741 lemma total_on_converse [simp]: "total_on A (r\<inverse>) = total_on A r" |
821 by (auto simp: total_on_def) |
742 by (auto simp: total_on_def) |
822 |
743 |
823 lemma finite_converse [iff]: "finite (r^-1) = finite r" |
744 lemma finite_converse [iff]: "finite (r\<inverse>) = finite r" |
824 unfolding converse_def conversep_iff using [[simproc add: finite_Collect]] |
745 unfolding converse_def conversep_iff using [[simproc add: finite_Collect]] |
825 by (auto elim: finite_imageD simp: inj_on_def) |
746 by (auto elim: finite_imageD simp: inj_on_def) |
826 |
747 |
827 lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>" |
748 lemma conversep_noteq [simp]: "(op \<noteq>)\<inverse>\<inverse> = op \<noteq>" |
828 by (auto simp add: fun_eq_iff) |
749 by (auto simp add: fun_eq_iff) |
829 |
750 |
830 lemma conversep_eq [simp]: "(op =)^--1 = op =" |
751 lemma conversep_eq [simp]: "(op =)\<inverse>\<inverse> = op =" |
831 by (auto simp add: fun_eq_iff) |
752 by (auto simp add: fun_eq_iff) |
832 |
753 |
833 lemma converse_unfold [code]: |
754 lemma converse_unfold [code]: "r\<inverse> = {(y, x). (x, y) \<in> r}" |
834 "r\<inverse> = {(y, x). (x, y) \<in> r}" |
|
835 by (simp add: set_eq_iff) |
755 by (simp add: set_eq_iff) |
836 |
756 |
837 |
757 |
838 subsubsection \<open>Domain, range and field\<close> |
758 subsubsection \<open>Domain, range and field\<close> |
839 |
759 |
840 inductive_set Domain :: "('a \<times> 'b) set \<Rightarrow> 'a set" |
760 inductive_set Domain :: "('a \<times> 'b) set \<Rightarrow> 'a set" for r :: "('a \<times> 'b) set" |
841 for r :: "('a \<times> 'b) set" |
761 where DomainI [intro]: "(a, b) \<in> r \<Longrightarrow> a \<in> Domain r" |
842 where |
|
843 DomainI [intro]: "(a, b) \<in> r \<Longrightarrow> a \<in> Domain r" |
|
844 |
762 |
845 lemmas DomainPI = Domainp.DomainI |
763 lemmas DomainPI = Domainp.DomainI |
846 |
764 |
847 inductive_cases DomainE [elim!]: "a \<in> Domain r" |
765 inductive_cases DomainE [elim!]: "a \<in> Domain r" |
848 inductive_cases DomainpE [elim!]: "Domainp r a" |
766 inductive_cases DomainpE [elim!]: "Domainp r a" |
849 |
767 |
850 inductive_set Range :: "('a \<times> 'b) set \<Rightarrow> 'b set" |
768 inductive_set Range :: "('a \<times> 'b) set \<Rightarrow> 'b set" for r :: "('a \<times> 'b) set" |
851 for r :: "('a \<times> 'b) set" |
769 where RangeI [intro]: "(a, b) \<in> r \<Longrightarrow> b \<in> Range r" |
852 where |
|
853 RangeI [intro]: "(a, b) \<in> r \<Longrightarrow> b \<in> Range r" |
|
854 |
770 |
855 lemmas RangePI = Rangep.RangeI |
771 lemmas RangePI = Rangep.RangeI |
856 |
772 |
857 inductive_cases RangeE [elim!]: "b \<in> Range r" |
773 inductive_cases RangeE [elim!]: "b \<in> Range r" |
858 inductive_cases RangepE [elim!]: "Rangep r b" |
774 inductive_cases RangepE [elim!]: "Rangep r b" |
859 |
775 |
860 definition Field :: "'a rel \<Rightarrow> 'a set" |
776 definition Field :: "'a rel \<Rightarrow> 'a set" |
861 where |
777 where "Field r = Domain r \<union> Range r" |
862 "Field r = Domain r \<union> Range r" |
778 |
863 |
779 lemma Domain_fst [code]: "Domain r = fst ` r" |
864 lemma Domain_fst [code]: |
|
865 "Domain r = fst ` r" |
|
866 by force |
780 by force |
867 |
781 |
868 lemma Range_snd [code]: |
782 lemma Range_snd [code]: "Range r = snd ` r" |
869 "Range r = snd ` r" |
|
870 by force |
783 by force |
871 |
784 |
872 lemma fst_eq_Domain: "fst ` R = Domain R" |
785 lemma fst_eq_Domain: "fst ` R = Domain R" |
873 by force |
786 by force |
874 |
787 |
1128 |
1033 |
1129 lemma Id_on_fold: |
1034 lemma Id_on_fold: |
1130 assumes "finite A" |
1035 assumes "finite A" |
1131 shows "Id_on A = Finite_Set.fold (\<lambda>x. Set.insert (Pair x x)) {} A" |
1036 shows "Id_on A = Finite_Set.fold (\<lambda>x. Set.insert (Pair x x)) {} A" |
1132 proof - |
1037 proof - |
1133 interpret comp_fun_commute "\<lambda>x. Set.insert (Pair x x)" by standard auto |
1038 interpret comp_fun_commute "\<lambda>x. Set.insert (Pair x x)" |
1134 show ?thesis using assms unfolding Id_on_def by (induct A) simp_all |
1039 by standard auto |
|
1040 from assms show ?thesis |
|
1041 unfolding Id_on_def by (induct A) simp_all |
1135 qed |
1042 qed |
1136 |
1043 |
1137 lemma comp_fun_commute_Image_fold: |
1044 lemma comp_fun_commute_Image_fold: |
1138 "comp_fun_commute (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)" |
1045 "comp_fun_commute (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)" |
1139 proof - |
1046 proof - |
1140 interpret comp_fun_idem Set.insert |
1047 interpret comp_fun_idem Set.insert |
1141 by (fact comp_fun_idem_insert) |
1048 by (fact comp_fun_idem_insert) |
1142 show ?thesis |
1049 show ?thesis |
1143 by standard (auto simp add: fun_eq_iff comp_fun_commute split:prod.split) |
1050 by standard (auto simp add: fun_eq_iff comp_fun_commute split: prod.split) |
1144 qed |
1051 qed |
1145 |
1052 |
1146 lemma Image_fold: |
1053 lemma Image_fold: |
1147 assumes "finite R" |
1054 assumes "finite R" |
1148 shows "R `` S = Finite_Set.fold (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) {} R" |
1055 shows "R `` S = Finite_Set.fold (\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A) {} R" |
1149 proof - |
1056 proof - |
1150 interpret comp_fun_commute "(\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)" |
1057 interpret comp_fun_commute "(\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)" |
1151 by (rule comp_fun_commute_Image_fold) |
1058 by (rule comp_fun_commute_Image_fold) |
1152 have *: "\<And>x F. Set.insert x F `` S = (if fst x \<in> S then Set.insert (snd x) (F `` S) else (F `` S))" |
1059 have *: "\<And>x F. Set.insert x F `` S = (if fst x \<in> S then Set.insert (snd x) (F `` S) else (F `` S))" |
1153 by (force intro: rev_ImageI) |
1060 by (force intro: rev_ImageI) |
1154 show ?thesis using assms by (induct R) (auto simp: *) |
1061 show ?thesis |
|
1062 using assms by (induct R) (auto simp: *) |
1155 qed |
1063 qed |
1156 |
1064 |
1157 lemma insert_relcomp_union_fold: |
1065 lemma insert_relcomp_union_fold: |
1158 assumes "finite S" |
1066 assumes "finite S" |
1159 shows "{x} O S \<union> X = Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') X S" |
1067 shows "{x} O S \<union> X = Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') X S" |
1160 proof - |
1068 proof - |
1161 interpret comp_fun_commute "\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A'" |
1069 interpret comp_fun_commute "\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A'" |
1162 proof - |
1070 proof - |
1163 interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert) |
1071 interpret comp_fun_idem Set.insert |
|
1072 by (fact comp_fun_idem_insert) |
1164 show "comp_fun_commute (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A')" |
1073 show "comp_fun_commute (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A')" |
1165 by standard (auto simp add: fun_eq_iff split:prod.split) |
1074 by standard (auto simp add: fun_eq_iff split: prod.split) |
1166 qed |
1075 qed |
1167 have *: "{x} O S = {(x', z). x' = fst x \<and> (snd x,z) \<in> S}" by (auto simp: relcomp_unfold intro!: exI) |
1076 have *: "{x} O S = {(x', z). x' = fst x \<and> (snd x, z) \<in> S}" |
1168 show ?thesis unfolding * |
1077 by (auto simp: relcomp_unfold intro!: exI) |
1169 using \<open>finite S\<close> by (induct S) (auto split: prod.split) |
1078 show ?thesis |
|
1079 unfolding * using \<open>finite S\<close> by (induct S) (auto split: prod.split) |
1170 qed |
1080 qed |
1171 |
1081 |
1172 lemma insert_relcomp_fold: |
1082 lemma insert_relcomp_fold: |
1173 assumes "finite S" |
1083 assumes "finite S" |
1174 shows "Set.insert x R O S = |
1084 shows "Set.insert x R O S = |
1175 Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') (R O S) S" |
1085 Finite_Set.fold (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A') (R O S) S" |
1176 proof - |
1086 proof - |
1177 have "Set.insert x R O S = ({x} O S) \<union> (R O S)" by auto |
1087 have "Set.insert x R O S = ({x} O S) \<union> (R O S)" |
1178 then show ?thesis by (auto simp: insert_relcomp_union_fold[OF assms]) |
1088 by auto |
|
1089 then show ?thesis |
|
1090 by (auto simp: insert_relcomp_union_fold [OF assms]) |
1179 qed |
1091 qed |
1180 |
1092 |
1181 lemma comp_fun_commute_relcomp_fold: |
1093 lemma comp_fun_commute_relcomp_fold: |
1182 assumes "finite S" |
1094 assumes "finite S" |
1183 shows "comp_fun_commute (\<lambda>(x,y) A. |
1095 shows "comp_fun_commute (\<lambda>(x,y) A. |
1184 Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S)" |
1096 Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S)" |
1185 proof - |
1097 proof - |
1186 have *: "\<And>a b A. |
1098 have *: "\<And>a b A. |
1187 Finite_Set.fold (\<lambda>(w, z) A'. if b = w then Set.insert (a, z) A' else A') A S = {(a,b)} O S \<union> A" |
1099 Finite_Set.fold (\<lambda>(w, z) A'. if b = w then Set.insert (a, z) A' else A') A S = {(a,b)} O S \<union> A" |
1188 by (auto simp: insert_relcomp_union_fold[OF assms] cong: if_cong) |
1100 by (auto simp: insert_relcomp_union_fold[OF assms] cong: if_cong) |
1189 show ?thesis by standard (auto simp: *) |
1101 show ?thesis |
|
1102 by standard (auto simp: *) |
1190 qed |
1103 qed |
1191 |
1104 |
1192 lemma relcomp_fold: |
1105 lemma relcomp_fold: |
1193 assumes "finite R" |
1106 assumes "finite R" "finite S" |
1194 assumes "finite S" |
1107 shows "R O S = Finite_Set.fold |
1195 shows "R O S = Finite_Set.fold |
|
1196 (\<lambda>(x,y) A. Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S) {} R" |
1108 (\<lambda>(x,y) A. Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S) {} R" |
1197 using assms by (induct R) |
1109 using assms |
|
1110 by (induct R) |
1198 (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold |
1111 (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold |
1199 cong: if_cong) |
1112 cong: if_cong) |
1200 |
1113 |
1201 text \<open>Misc\<close> |
1114 text \<open>Misc\<close> |
1202 |
1115 |
1203 abbreviation (input) transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
1116 abbreviation (input) transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
1204 where \<comment> \<open>FIXME drop\<close> |
1117 where "transP r \<equiv> trans {(x, y). r x y}" (* FIXME drop *) |
1205 "transP r \<equiv> trans {(x, y). r x y}" |
1118 |
1206 |
1119 abbreviation (input) "RangeP \<equiv> Rangep" |
1207 abbreviation (input) |
1120 abbreviation (input) "DomainP \<equiv> Domainp" |
1208 "RangeP \<equiv> Rangep" |
|
1209 |
|
1210 abbreviation (input) |
|
1211 "DomainP \<equiv> Domainp" |
|
1212 |
|
1213 |
1121 |
1214 end |
1122 end |