32 EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and |
32 EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and |
33 transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and |
33 transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and |
34 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and |
34 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and |
35 append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and |
35 append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and |
36 append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and |
36 append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and |
37 uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) |
37 uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and |
38 |
38 tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and |
|
39 tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) |
|
40 |
|
41 lemma meta_eq_app: |
|
42 shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x" |
|
43 by auto |
|
44 |
39 (*>*) |
45 (*>*) |
40 |
46 |
41 |
47 |
42 section {* Introduction *} |
48 section {* Introduction *} |
43 |
49 |
883 Much more interesting, however, are the inductive cases. They seem hard to be solved |
889 Much more interesting, however, are the inductive cases. They seem hard to be solved |
884 directly. The reader is invited to try. |
890 directly. The reader is invited to try. |
885 |
891 |
886 Our method will rely on some |
892 Our method will rely on some |
887 \emph{tagging functions} defined over strings. Given the inductive hypothesis, it will |
893 \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. |
894 be easy to prove that the range of these tagging functions is finite |
|
895 (the range of a function @{text f} is defined as @{text "range f \<equiv> f ` UNIV"}). |
889 With this we will be able to infer that the tagging functions, seen as a relation, |
896 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 |
897 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 |
898 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. |
899 implies that @{term "UNIV // \<approx>(L r)"} must also be finite. |
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"}. |
900 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. |
901 We formally define the notion of a \emph{tag-relation} as follows. |
895 |
902 |
896 \begin{definition}[Tag-Relation] Given a tag-function @{text tag}, then two strings @{text x} |
903 \begin{definition}[Tagging-Relation] Given a tag-function @{text tag}, then two strings @{text x} |
897 and @{text y} are tag-related provided |
904 and @{text y} are \emph{tag-related} provided |
898 \begin{center} |
905 \begin{center} |
899 @{text "x =tag= y \<equiv> tag x = tag y"} |
906 @{text "x =tag= y \<equiv> tag x = tag y"} |
900 \end{center} |
907 \end{center} |
901 \end{definition} |
908 \end{definition} |
902 |
909 |
903 \noindent |
910 \noindent |
904 In order to establis finiteness of a set @{text A} we shall use the following powerful |
911 In order to establish finiteness of a set @{text A} we shall use the following powerful |
905 principle from Isabelle/HOL's library. |
912 principle from Isabelle/HOL's library. |
906 % |
913 % |
907 \begin{equation}\label{finiteimageD} |
914 \begin{equation}\label{finiteimageD} |
908 @{thm[mode=IfThen] finite_imageD} |
915 @{thm[mode=IfThen] finite_imageD} |
909 \end{equation} |
916 \end{equation} |
916 \begin{lemma}\label{finone} |
923 \begin{lemma}\label{finone} |
917 @{thm[mode=IfThen] finite_eq_tag_rel} |
924 @{thm[mode=IfThen] finite_eq_tag_rel} |
918 \end{lemma} |
925 \end{lemma} |
919 |
926 |
920 \begin{proof} |
927 \begin{proof} |
921 |
928 We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have |
|
929 @{text "range f"} to be subset of @{term "Pow (range tag)"}, which we know must be |
|
930 finite by assumption. Now @{term "f (UNIV // =tag=)"} is a subset of @{text "range f"}, |
|
931 and so also finite. Injectivity amounts to showing that @{text "X = Y"} under the |
|
932 assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}. |
|
933 From the assumption we can obtain a @{text "x \<in> X"} and @{text "y \<in> Y"} with |
|
934 @{text "tag x = tag y"}. This in turn means that the equivalence classes @{text X} |
|
935 and @{text Y} must be equal.\qed |
922 \end{proof} |
936 \end{proof} |
923 |
937 |
924 \begin{lemma}\label{fintwo} |
938 \begin{lemma}\label{fintwo} |
925 Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, where |
939 Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, where |
926 @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}. |
940 @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}. |
944 are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}, |
958 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 |
959 they must also be @{text "R\<^isub>2"}-related, as we need to show.\qed |
946 \end{proof} |
960 \end{proof} |
947 |
961 |
948 \noindent |
962 \noindent |
949 Stringing Lem.~\ref{finone} and \ref{fintwo} together, means in order to show |
963 Chaining Lem.~\ref{finone} and \ref{fintwo} together, means in order to show |
950 that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging function whose |
964 that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging function whose |
951 range is finite and whose tagging-relation refines @{term "\<approx>(L r)"}. |
965 range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(L r)"}. |
952 |
966 Let us attempt the @{const ALT}-case. |
953 |
967 |
954 @{thm tag_str_ALT_def[where ?L1.0="A" and ?L2.0="B"]} |
968 \begin{proof}[@{const "ALT"}-Case] |
|
969 We take as tagging function |
|
970 |
|
971 \begin{center} |
|
972 @{thm tag_str_ALT_def[where A="A" and B="B", THEN meta_eq_app]} |
|
973 \end{center} |
|
974 |
|
975 \noindent |
|
976 where @{text "A"} and @{text "B"} are some arbitrary languages. |
|
977 We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"} |
|
978 then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of |
|
979 @{term "tag_str_ALT A B"} is a subset of this. It remains to be shown |
|
980 that @{text "=tag\<^isub>A\<^isub>L\<^isub>T="} refines @{text "\<approx>(A \<union> B)"}. |
|
981 |
|
982 \end{proof} |
|
983 |
955 |
984 |
956 @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B"]} |
985 @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B"]} |
957 |
986 |
958 @{thm tag_str_STAR_def[where ?L1.0="A"]} |
987 @{thm tag_str_STAR_def[where ?L1.0="A"]} |
959 *} |
988 *} |