882 \noindent |
882 \noindent |
883 Much more interesting, however, are the inductive cases. They seem hard to be solved |
883 Much more interesting, however, are the inductive cases. They seem hard to be solved |
884 directly. The reader is invited to try. |
884 directly. The reader is invited to try. |
885 |
885 |
886 Our method will rely on some |
886 Our method will rely on some |
887 \emph{tagging} functions of strings. Given the inductive hypothesis, it will |
887 \emph{tagging functions} defined over strings. Given the inductive hypothesis, it will |
888 be easy to prove that the range of these tagging functions is finite. |
888 be easy to prove that the range of these tagging functions is finite. |
889 With this we will be able to infer that the tagging functions, seen as a relation, |
889 With this we will be able to infer that the tagging functions, seen as a relation, |
890 give rise to finitely many equivalence classes of @{const UNIV}. Finally we |
890 give rise to finitely many equivalence classes of @{const UNIV}. Finally we |
891 will show that the tagging relation is more refined than @{term "\<approx>(L r)"}, which |
891 will show that the tagging relation is more refined than @{term "\<approx>(L r)"}, which |
892 implies that @{term "UNIV // \<approx>(L r)"} must also be finite. For this we define the |
892 implies that @{term "UNIV // \<approx>(L r)"} must also be finite. |
893 notion of a \emph{tag-relation} (which is often also called a kernel relation). |
893 A relation @{text "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}. |
|
894 We also define formally the notion of a \emph{tag-relation} as follows. |
894 |
895 |
895 \begin{definition}[Tag-Relation] Given a tag-function @{text tag}, then two strings @{text x} |
896 \begin{definition}[Tag-Relation] Given a tag-function @{text tag}, then two strings @{text x} |
896 and @{text y} are tag-related provided |
897 and @{text y} are tag-related provided |
897 \begin{center} |
898 \begin{center} |
898 @{text "x =tag= y \<equiv> tag x = tag y"} |
899 @{text "x =tag= y \<equiv> tag x = tag y"} |
899 \end{center} |
900 \end{center} |
900 \end{definition} |
901 \end{definition} |
|
902 |
|
903 \noindent |
|
904 In order to establis finiteness of a set @{text A} we shall use the following powerful |
|
905 principle from Isabelle/HOL's library. |
|
906 % |
|
907 \begin{equation}\label{finiteimageD} |
|
908 @{thm[mode=IfThen] finite_imageD} |
|
909 \end{equation} |
|
910 |
|
911 \noindent |
|
912 It states that if an image of a set under an injective function @{text f} (over this set) |
|
913 is finite, then @{text A} itself must be finite. We can use it to establish the following |
|
914 two lemmas. |
901 |
915 |
902 \begin{lemma}\label{finone} |
916 \begin{lemma}\label{finone} |
903 @{thm[mode=IfThen] finite_eq_tag_rel} |
917 @{thm[mode=IfThen] finite_eq_tag_rel} |
904 \end{lemma} |
918 \end{lemma} |
905 |
919 |
906 \begin{proof} |
920 \begin{proof} |
907 |
921 |
908 \end{proof} |
922 \end{proof} |
909 |
923 |
910 \noindent |
|
911 |
|
912 |
|
913 \begin{lemma}\label{fintwo} |
924 \begin{lemma}\label{fintwo} |
914 Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, then |
925 Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, where |
915 if @{thm (prem 1) refined_partition_finite[where A="UNIV" and ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]} |
926 @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}. |
916 and @{thm (prem 2) refined_partition_finite[where A="UNIV" and ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]} |
927 If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]} |
917 then @{thm (concl) refined_partition_finite[where A="UNIV" and ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}. |
928 then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}. |
918 \end{lemma} |
929 \end{lemma} |
919 |
930 |
920 \begin{proof} |
931 \begin{proof} |
921 |
932 We prove this lemma again using \eqref{finiteimageD}. For this we set @{text f} to |
|
933 be @{text "X \<mapsto>"}~@{term "{R\<^isub>1 `` {x} | x. x \<in> X}"}. It is easy to see that |
|
934 @{text "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{text "Pow (UNIV // R\<^isub>1)"}, |
|
935 which is finite by assumption. What remains to be shown is that @{text f} is injective |
|
936 on @{term "UNIV // R\<^isub>2"}. This is equivalent to showing that two equivalence |
|
937 classes, say @{text "X"} and @{text Y}, in @{term "UNIV // R\<^isub>2"} are equal, provided |
|
938 @{text "f X = f Y"}. For @{text "X = Y"} to be equal, we have to find two elements |
|
939 @{text "x \<in> X"} and @{text "y \<in> Y"} such that they are @{text R\<^isub>2} related. |
|
940 We know there exists a @{text x} with @{term "X = R\<^isub>2 `` {x}"} |
|
941 and @{text "x \<in> X"}. From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f X"} |
|
942 and further @{term "R\<^isub>1 ``{x} \<in> f Y"}. From this we can obtain a @{text y} |
|
943 such that @{term "R\<^isub>1 `` {x} = R\<^isub>1 `` {y}"} holds. This means @{text x} and @{text y} |
|
944 are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}, |
|
945 they must also be @{text "R\<^isub>2"}-related, as we need to show.\qed |
922 \end{proof} |
946 \end{proof} |
923 |
947 |
924 \noindent |
948 \noindent |
925 Stringing Lem.~\ref{finone} and \ref{fintwo} together, means in order to show |
949 Stringing Lem.~\ref{finone} and \ref{fintwo} together, means in order to show |
926 that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging function whose |
950 that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging function whose |