510 inductive_set relcomp :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75) |
510 inductive_set relcomp :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75) |
511 for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set" |
511 for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set" |
512 where |
512 where |
513 relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s" |
513 relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s" |
514 |
514 |
515 abbreviation pred_comp (infixr "OO" 75) where |
515 notation relcompp (infixr "OO" 75) |
516 "pred_comp \<equiv> relcompp" |
516 |
517 |
517 lemmas relcomppI = relcompp.intros |
518 lemmas pred_compI = relcompp.intros |
|
519 |
518 |
520 text {* |
519 text {* |
521 For historic reasons, the elimination rules are not wholly corresponding. |
520 For historic reasons, the elimination rules are not wholly corresponding. |
522 Feel free to consolidate this. |
521 Feel free to consolidate this. |
523 *} |
522 *} |
524 |
523 |
525 inductive_cases relcompEpair: "(a, c) \<in> r O s" |
524 inductive_cases relcompEpair: "(a, c) \<in> r O s" |
526 inductive_cases pred_compE [elim!]: "(r OO s) a c" |
525 inductive_cases relcomppE [elim!]: "(r OO s) a c" |
527 |
526 |
528 lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow> |
527 lemma relcompE [elim!]: "xz \<in> r O s \<Longrightarrow> |
529 (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s \<Longrightarrow> P) \<Longrightarrow> P" |
528 (\<And>x y z. xz = (x, z) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, z) \<in> s \<Longrightarrow> P) \<Longrightarrow> P" |
530 by (cases xz) (simp, erule relcompEpair, iprover) |
529 by (cases xz) (simp, erule relcompEpair, iprover) |
531 |
530 |
532 lemmas pred_comp_relcomp_eq = relcompp_relcomp_eq |
|
533 |
|
534 lemma R_O_Id [simp]: |
531 lemma R_O_Id [simp]: |
535 "R O Id = R" |
532 "R O Id = R" |
536 by fast |
533 by fast |
537 |
534 |
538 lemma Id_O_R [simp]: |
535 lemma Id_O_R [simp]: |
541 |
538 |
542 lemma relcomp_empty1 [simp]: |
539 lemma relcomp_empty1 [simp]: |
543 "{} O R = {}" |
540 "{} O R = {}" |
544 by blast |
541 by blast |
545 |
542 |
546 lemma pred_comp_bot1 [simp]: |
543 lemma relcompp_bot1 [simp]: |
547 "\<bottom> OO R = \<bottom>" |
544 "\<bottom> OO R = \<bottom>" |
548 by (fact relcomp_empty1 [to_pred]) |
545 by (fact relcomp_empty1 [to_pred]) |
549 |
546 |
550 lemma relcomp_empty2 [simp]: |
547 lemma relcomp_empty2 [simp]: |
551 "R O {} = {}" |
548 "R O {} = {}" |
552 by blast |
549 by blast |
553 |
550 |
554 lemma pred_comp_bot2 [simp]: |
551 lemma relcompp_bot2 [simp]: |
555 "R OO \<bottom> = \<bottom>" |
552 "R OO \<bottom> = \<bottom>" |
556 by (fact relcomp_empty2 [to_pred]) |
553 by (fact relcomp_empty2 [to_pred]) |
557 |
554 |
558 lemma O_assoc: |
555 lemma O_assoc: |
559 "(R O S) O T = R O (S O T)" |
556 "(R O S) O T = R O (S O T)" |
560 by blast |
557 by blast |
561 |
558 |
562 |
559 |
563 lemma pred_comp_assoc: |
560 lemma relcompp_assoc: |
564 "(r OO s) OO t = r OO (s OO t)" |
561 "(r OO s) OO t = r OO (s OO t)" |
565 by (fact O_assoc [to_pred]) |
562 by (fact O_assoc [to_pred]) |
566 |
563 |
567 lemma trans_O_subset: |
564 lemma trans_O_subset: |
568 "trans r \<Longrightarrow> r O r \<subseteq> r" |
565 "trans r \<Longrightarrow> r O r \<subseteq> r" |
569 by (unfold trans_def) blast |
566 by (unfold trans_def) blast |
570 |
567 |
571 lemma transp_pred_comp_less_eq: |
568 lemma transp_relcompp_less_eq: |
572 "transp r \<Longrightarrow> r OO r \<le> r " |
569 "transp r \<Longrightarrow> r OO r \<le> r " |
573 by (fact trans_O_subset [to_pred]) |
570 by (fact trans_O_subset [to_pred]) |
574 |
571 |
575 lemma relcomp_mono: |
572 lemma relcomp_mono: |
576 "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s" |
573 "r' \<subseteq> r \<Longrightarrow> s' \<subseteq> s \<Longrightarrow> r' O s' \<subseteq> r O s" |
577 by blast |
574 by blast |
578 |
575 |
579 lemma pred_comp_mono: |
576 lemma relcompp_mono: |
580 "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s " |
577 "r' \<le> r \<Longrightarrow> s' \<le> s \<Longrightarrow> r' OO s' \<le> r OO s " |
581 by (fact relcomp_mono [to_pred]) |
578 by (fact relcomp_mono [to_pred]) |
582 |
579 |
583 lemma relcomp_subset_Sigma: |
580 lemma relcomp_subset_Sigma: |
584 "r \<subseteq> A \<times> B \<Longrightarrow> s \<subseteq> B \<times> C \<Longrightarrow> r O s \<subseteq> A \<times> C" |
581 "r \<subseteq> A \<times> B \<Longrightarrow> s \<subseteq> B \<times> C \<Longrightarrow> r O s \<subseteq> A \<times> C" |
586 |
583 |
587 lemma relcomp_distrib [simp]: |
584 lemma relcomp_distrib [simp]: |
588 "R O (S \<union> T) = (R O S) \<union> (R O T)" |
585 "R O (S \<union> T) = (R O S) \<union> (R O T)" |
589 by auto |
586 by auto |
590 |
587 |
591 lemma pred_comp_distrib [simp]: |
588 lemma relcompp_distrib [simp]: |
592 "R OO (S \<squnion> T) = R OO S \<squnion> R OO T" |
589 "R OO (S \<squnion> T) = R OO S \<squnion> R OO T" |
593 by (fact relcomp_distrib [to_pred]) |
590 by (fact relcomp_distrib [to_pred]) |
594 |
591 |
595 lemma relcomp_distrib2 [simp]: |
592 lemma relcomp_distrib2 [simp]: |
596 "(S \<union> T) O R = (S O R) \<union> (T O R)" |
593 "(S \<union> T) O R = (S O R) \<union> (T O R)" |
597 by auto |
594 by auto |
598 |
595 |
599 lemma pred_comp_distrib2 [simp]: |
596 lemma relcompp_distrib2 [simp]: |
600 "(S \<squnion> T) OO R = S OO R \<squnion> T OO R" |
597 "(S \<squnion> T) OO R = S OO R \<squnion> T OO R" |
601 by (fact relcomp_distrib2 [to_pred]) |
598 by (fact relcomp_distrib2 [to_pred]) |
602 |
599 |
603 lemma relcomp_UNION_distrib: |
600 lemma relcomp_UNION_distrib: |
604 "s O UNION I r = (\<Union>i\<in>I. s O r i) " |
601 "s O UNION I r = (\<Union>i\<in>I. s O r i) " |
677 by (fact converse_converse [to_pred]) |
674 by (fact converse_converse [to_pred]) |
678 |
675 |
679 lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1" |
676 lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1" |
680 by blast |
677 by blast |
681 |
678 |
682 lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1" |
679 lemma converse_relcompp: "(r OO s)^--1 = s^--1 OO r^--1" |
683 by (iprover intro: order_antisym conversepI pred_compI |
680 by (iprover intro: order_antisym conversepI relcomppI |
684 elim: pred_compE dest: conversepD) |
681 elim: relcomppE dest: conversepD) |
685 |
682 |
686 lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1" |
683 lemma converse_Int: "(r \<inter> s)^-1 = r^-1 \<inter> s^-1" |
687 by blast |
684 by blast |
688 |
685 |
689 lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1" |
686 lemma converse_meet: "(r \<sqinter> s)^--1 = r^--1 \<sqinter> s^--1" |