628 rtranclp.rtrancl_into_rtrancl converse_rtranclp_into_rtranclp |
628 rtranclp.rtrancl_into_rtrancl converse_rtranclp_into_rtranclp |
629 rtranclp_tranclp_tranclp tranclp_rtranclp_tranclp |
629 rtranclp_tranclp_tranclp tranclp_rtranclp_tranclp |
630 |
630 |
631 declare trancl_into_rtrancl [elim] |
631 declare trancl_into_rtrancl [elim] |
632 |
632 |
|
633 subsection {* The power operation on relations *} |
|
634 |
|
635 text {* @{text "R ^^ n = R O ... O R"}, the n-fold composition of @{text R} *} |
|
636 |
|
637 primrec relpow :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set" (infixr "^^" 80) where |
|
638 "R ^^ 0 = Id" |
|
639 | "R ^^ Suc n = R O (R ^^ n)" |
|
640 |
|
641 notation (latex output) |
|
642 relpow ("(_\<^bsup>_\<^esup>)" [1000] 1000) |
|
643 |
|
644 notation (HTML output) |
|
645 relpow ("(_\<^bsup>_\<^esup>)" [1000] 1000) |
|
646 |
|
647 lemma rel_pow_1 [simp]: |
|
648 "R ^^ 1 = R" |
|
649 by simp |
|
650 |
|
651 lemma rel_pow_0_I: |
|
652 "(x, x) \<in> R ^^ 0" |
|
653 by simp |
|
654 |
|
655 lemma rel_pow_Suc_I: |
|
656 "(x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> (x, z) \<in> R ^^ Suc n" |
|
657 by auto |
|
658 |
|
659 lemma rel_pow_Suc_I2: |
|
660 "(x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> (x, z) \<in> R ^^ Suc n" |
|
661 by (induct n arbitrary: z) (simp, fastsimp) |
|
662 |
|
663 lemma rel_pow_0_E: |
|
664 "(x, y) \<in> R ^^ 0 \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P" |
|
665 by simp |
|
666 |
|
667 lemma rel_pow_Suc_E: |
|
668 "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P" |
|
669 by auto |
|
670 |
|
671 lemma rel_pow_E: |
|
672 "(x, z) \<in> R ^^ n \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P) |
|
673 \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) |
|
674 \<Longrightarrow> P" |
|
675 by (cases n) auto |
|
676 |
|
677 lemma rel_pow_Suc_D2: |
|
678 "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<exists>y. (x, y) \<in> R \<and> (y, z) \<in> R ^^ n)" |
|
679 apply (induct n arbitrary: x z) |
|
680 apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E) |
|
681 apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E) |
|
682 done |
|
683 |
|
684 lemma rel_pow_Suc_E2: |
|
685 "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> P) \<Longrightarrow> P" |
|
686 by (blast dest: rel_pow_Suc_D2) |
|
687 |
|
688 lemma rel_pow_Suc_D2': |
|
689 "\<forall>x y z. (x, y) \<in> R ^^ n \<and> (y, z) \<in> R \<longrightarrow> (\<exists>w. (x, w) \<in> R \<and> (w, z) \<in> R ^^ n)" |
|
690 by (induct n) (simp_all, blast) |
|
691 |
|
692 lemma rel_pow_E2: |
|
693 "(x, z) \<in> R ^^ n \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P) |
|
694 \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P) |
|
695 \<Longrightarrow> P" |
|
696 apply (cases n, simp) |
|
697 apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast) |
|
698 done |
|
699 |
|
700 lemma rtrancl_imp_UN_rel_pow: |
|
701 assumes "p \<in> R^*" |
|
702 shows "p \<in> (\<Union>n. R ^^ n)" |
|
703 proof (cases p) |
|
704 case (Pair x y) |
|
705 with assms have "(x, y) \<in> R^*" by simp |
|
706 then have "(x, y) \<in> (\<Union>n. R ^^ n)" proof induct |
|
707 case base show ?case by (blast intro: rel_pow_0_I) |
|
708 next |
|
709 case step then show ?case by (blast intro: rel_pow_Suc_I) |
|
710 qed |
|
711 with Pair show ?thesis by simp |
|
712 qed |
|
713 |
|
714 lemma rel_pow_imp_rtrancl: |
|
715 assumes "p \<in> R ^^ n" |
|
716 shows "p \<in> R^*" |
|
717 proof (cases p) |
|
718 case (Pair x y) |
|
719 with assms have "(x, y) \<in> R ^^ n" by simp |
|
720 then have "(x, y) \<in> R^*" proof (induct n arbitrary: x y) |
|
721 case 0 then show ?case by simp |
|
722 next |
|
723 case Suc then show ?case |
|
724 by (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl) |
|
725 qed |
|
726 with Pair show ?thesis by simp |
|
727 qed |
|
728 |
|
729 lemma rtrancl_is_UN_rel_pow: |
|
730 "R^* = (\<Union>n. R ^^ n)" |
|
731 by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl) |
|
732 |
|
733 lemma rtrancl_power: |
|
734 "p \<in> R^* \<longleftrightarrow> (\<exists>n. p \<in> R ^^ n)" |
|
735 by (simp add: rtrancl_is_UN_rel_pow) |
|
736 |
|
737 lemma trancl_power: |
|
738 "p \<in> R^+ \<longleftrightarrow> (\<exists>n > 0. p \<in> R ^^ n)" |
|
739 apply (cases p) |
|
740 apply simp |
|
741 apply (rule iffI) |
|
742 apply (drule tranclD2) |
|
743 apply (clarsimp simp: rtrancl_is_UN_rel_pow) |
|
744 apply (rule_tac x="Suc x" in exI) |
|
745 apply (clarsimp simp: rel_comp_def) |
|
746 apply fastsimp |
|
747 apply clarsimp |
|
748 apply (case_tac n, simp) |
|
749 apply clarsimp |
|
750 apply (drule rel_pow_imp_rtrancl) |
|
751 apply (drule rtrancl_into_trancl1) apply auto |
|
752 done |
|
753 |
|
754 lemma rtrancl_imp_rel_pow: |
|
755 "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R ^^ n" |
|
756 by (auto dest: rtrancl_imp_UN_rel_pow) |
|
757 |
|
758 lemma single_valued_rel_pow: |
|
759 fixes R :: "('a * 'a) set" |
|
760 shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)" |
|
761 apply (induct n arbitrary: R) |
|
762 apply simp_all |
|
763 apply (rule single_valuedI) |
|
764 apply (fast dest: single_valuedD elim: rel_pow_Suc_E) |
|
765 done |
633 |
766 |
634 subsection {* Setup of transitivity reasoner *} |
767 subsection {* Setup of transitivity reasoner *} |
635 |
768 |
636 ML {* |
769 ML {* |
637 |
770 |