740 |
740 |
741 lemma finite_Init_rhs: |
741 lemma finite_Init_rhs: |
742 assumes finite: "finite CS" |
742 assumes finite: "finite CS" |
743 shows "finite (Init_rhs CS X)" |
743 shows "finite (Init_rhs CS X)" |
744 proof- |
744 proof- |
745 have "finite {Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" (is "finite ?A") |
745 def S \<equiv> "{(Y, c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" |
746 proof - |
746 def h \<equiv> "\<lambda> (Y, c). Trn Y (CHAR c)" |
747 def S \<equiv> "{(Y, c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" |
747 have "finite (CS \<times> (UNIV::char set))" using finite by auto |
748 def h \<equiv> "\<lambda> (Y, c). Trn Y (CHAR c)" |
748 then have "finite S" using S_def |
749 have "finite (CS \<times> (UNIV::char set))" using finite by auto |
749 by (rule_tac B = "CS \<times> UNIV" in finite_subset) (auto) |
750 hence "finite S" using S_def |
750 moreover have "{Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X} = h ` S" |
751 by (rule_tac B = "CS \<times> UNIV" in finite_subset, auto) |
751 unfolding S_def h_def image_def by auto |
752 moreover have "?A = h ` S" by (auto simp: S_def h_def image_def) |
752 ultimately |
753 ultimately show ?thesis |
753 have "finite {Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" by auto |
754 by auto |
754 then show "finite (Init_rhs CS X)" unfolding Init_rhs_def transition_def by simp |
755 qed |
|
756 thus ?thesis by (simp add:Init_rhs_def transition_def) |
|
757 qed |
755 qed |
758 |
756 |
759 lemma Init_ES_satisfies_invariant: |
757 lemma Init_ES_satisfies_invariant: |
760 assumes finite_CS: "finite (UNIV // \<approx>A)" |
758 assumes finite_CS: "finite (UNIV // \<approx>A)" |
761 shows "invariant (Init (UNIV // \<approx>A))" |
759 shows "invariant (Init (UNIV // \<approx>A))" |
1043 qed |
1041 qed |
1044 |
1042 |
1045 lemma iteration_step_measure: |
1043 lemma iteration_step_measure: |
1046 assumes Inv_ES: "invariant ES" |
1044 assumes Inv_ES: "invariant ES" |
1047 and X_in_ES: "(X, xrhs) \<in> ES" |
1045 and X_in_ES: "(X, xrhs) \<in> ES" |
1048 and not_T: "Cond ES " |
1046 and Cnd: "Cond ES " |
1049 shows "(Iter X ES, ES) \<in> measure card" |
1047 shows "(Iter X ES, ES) \<in> measure card" |
1050 proof - |
1048 proof - |
1051 have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) |
1049 have fin: "finite ES" using Inv_ES unfolding invariant_def by simp |
1052 then obtain Y yrhs |
1050 then obtain Y yrhs |
1053 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1051 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1054 using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto) |
1052 using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto) |
1055 then have "(Y, yrhs) \<in> ES " "X \<noteq> Y" |
1053 then have "(Y, yrhs) \<in> ES " "X \<noteq> Y" |
1056 using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def |
1054 using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def |
1057 by auto |
1055 by auto |
1058 then show "(Iter X ES, ES) \<in> measure card" |
1056 then show "(Iter X ES, ES) \<in> measure card" |
1059 apply(rule IterI2) |
1057 apply(rule IterI2) |
1060 apply(rule Remove_in_card_measure) |
1058 apply(rule Remove_in_card_measure) |
1061 apply(simp_all add: finite_ES) |
1059 apply(simp_all add: fin) |
1062 done |
1060 done |
1063 qed |
1061 qed |
1064 |
1062 |
1065 lemma iteration_step_invariant: |
1063 lemma iteration_step_invariant: |
1066 assumes Inv_ES: "invariant ES" |
1064 assumes Inv_ES: "invariant ES" |
1067 and X_in_ES: "(X, xrhs) \<in> ES" |
1065 and X_in_ES: "(X, xrhs) \<in> ES" |
1068 and not_T: "Cond ES" |
1066 and Cnd: "Cond ES" |
1069 shows "invariant (Iter X ES)" |
1067 shows "invariant (Iter X ES)" |
1070 proof - |
1068 proof - |
1071 have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) |
1069 have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) |
1072 then obtain Y yrhs |
1070 then obtain Y yrhs |
1073 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1071 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1074 using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto) |
1072 using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto) |
1075 then have "(Y, yrhs) \<in> ES" "X \<noteq> Y" |
1073 then have "(Y, yrhs) \<in> ES" "X \<noteq> Y" |
1076 using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def |
1074 using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def |
1077 by auto |
1075 by auto |
1078 then show "invariant (Iter X ES)" |
1076 then show "invariant (Iter X ES)" |
1079 proof(rule IterI2) |
1077 proof(rule IterI2) |
1086 qed |
1084 qed |
1087 |
1085 |
1088 lemma iteration_step_ex: |
1086 lemma iteration_step_ex: |
1089 assumes Inv_ES: "invariant ES" |
1087 assumes Inv_ES: "invariant ES" |
1090 and X_in_ES: "(X, xrhs) \<in> ES" |
1088 and X_in_ES: "(X, xrhs) \<in> ES" |
1091 and not_T: "Cond ES" |
1089 and Cnd: "Cond ES" |
1092 shows "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" |
1090 shows "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" |
1093 proof - |
1091 proof - |
1094 have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) |
1092 have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) |
1095 then obtain Y yrhs |
1093 then obtain Y yrhs |
1096 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1094 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1097 using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto) |
1095 using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto) |
1098 then have "(Y, yrhs) \<in> ES " "X \<noteq> Y" |
1096 then have "(Y, yrhs) \<in> ES " "X \<noteq> Y" |
1099 using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def |
1097 using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def |
1100 by auto |
1098 by auto |
1101 then show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" |
1099 then show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" |
1102 apply(rule IterI2) |
1100 apply(rule IterI2) |
1153 lemma last_cl_exists_rexp: |
1151 lemma last_cl_exists_rexp: |
1154 assumes Inv_ES: "invariant {(X, xrhs)}" |
1152 assumes Inv_ES: "invariant {(X, xrhs)}" |
1155 shows "\<exists>r::rexp. L r = X" |
1153 shows "\<exists>r::rexp. L r = X" |
1156 proof- |
1154 proof- |
1157 def A \<equiv> "Arden X xrhs" |
1155 def A \<equiv> "Arden X xrhs" |
1158 have eq: "{Lam r | r. Lam r \<in> A} = A" |
1156 have "rhss xrhs \<subseteq> {X}" using Inv_ES |
1159 proof - |
1157 unfolding valid_eqs_def invariant_def rhss_def lhss_def |
1160 have "rhss A = {}" using Inv_ES |
1158 by auto |
1161 unfolding A_def valid_eqs_def invariant_def lhss_def |
1159 then have "rhss A = {}" unfolding A_def |
1162 by (simp add: Arden_removes_cl) |
1160 by (simp add: Arden_removes_cl) |
1163 thus ?thesis unfolding A_def rhss_def |
1161 then have eq: "{Lam r | r. Lam r \<in> A} = A" unfolding rhss_def |
1164 apply(auto simp only:) |
1162 by (auto, case_tac x, auto) |
1165 apply(case_tac x) |
1163 |
1166 apply(auto) |
|
1167 done |
|
1168 qed |
|
1169 have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def |
1164 have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def |
1170 using Arden_keeps_finite by auto |
1165 using Arden_keeps_finite by auto |
1171 then have "finite {r. Lam r \<in> A}" by (rule finite_Lam) |
1166 then have fin: "finite {r. Lam r \<in> A}" by (rule finite_Lam) |
1172 then have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in> A})" |
1167 |
1173 by auto |
1168 have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def |
1174 also have "\<dots> = L A" by (simp add: eq) |
1169 by simp |
1175 also have "\<dots> = X" |
1170 then have "X = L A" using Inv_ES |
1176 proof - |
1171 unfolding A_def invariant_def ardenable_def finite_rhs_def rhs_nonempty_def |
1177 have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def |
1172 by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn) |
1178 by auto |
1173 then have "X = L {Lam r | r. Lam r \<in> A}" using eq by simp |
1179 moreover |
1174 then have "X = L (\<Uplus>{r. Lam r \<in> A})" using fin by auto |
1180 from Inv_ES have "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})" |
|
1181 unfolding invariant_def ardenable_def finite_rhs_def |
|
1182 by(simp add: rexp_of_empty) |
|
1183 moreover |
|
1184 from Inv_ES have "finite xrhs" unfolding invariant_def finite_rhs_def |
|
1185 by simp |
|
1186 ultimately show "L A = X" unfolding A_def |
|
1187 by (rule Arden_keeps_eq[symmetric]) |
|
1188 qed |
|
1189 finally have "L (\<Uplus>{r. Lam r \<in> A}) = X" . |
|
1190 then show "\<exists>r::rexp. L r = X" by blast |
1175 then show "\<exists>r::rexp. L r = X" by blast |
1191 qed |
1176 qed |
1192 |
1177 |
1193 lemma every_eqcl_has_reg: |
1178 lemma every_eqcl_has_reg: |
1194 assumes finite_CS: "finite (UNIV // \<approx>A)" |
1179 assumes finite_CS: "finite (UNIV // \<approx>A)" |
1214 |
1199 |
1215 theorem Myhill_Nerode1: |
1200 theorem Myhill_Nerode1: |
1216 assumes finite_CS: "finite (UNIV // \<approx>A)" |
1201 assumes finite_CS: "finite (UNIV // \<approx>A)" |
1217 shows "\<exists>r::rexp. A = L r" |
1202 shows "\<exists>r::rexp. A = L r" |
1218 proof - |
1203 proof - |
1219 have f: "finite (finals A)" |
1204 have fin: "finite (finals A)" |
1220 using finals_in_partitions finite_CS by (rule finite_subset) |
1205 using finals_in_partitions finite_CS by (rule finite_subset) |
1221 have "\<forall>X \<in> (UNIV // \<approx>A). \<exists>r::rexp. X = L r" |
1206 have "\<forall>X \<in> (UNIV // \<approx>A). \<exists>r::rexp. X = L r" |
1222 using finite_CS every_eqcl_has_reg by blast |
1207 using finite_CS every_eqcl_has_reg by blast |
1223 then have a: "\<forall>X \<in> finals A. \<exists>r::rexp. X = L r" |
1208 then have a: "\<forall>X \<in> finals A. \<exists>r::rexp. X = L r" |
1224 using finals_in_partitions by auto |
1209 using finals_in_partitions by auto |
1225 then obtain rs::"rexp set" where "\<Union> (finals A) = \<Union>(L ` rs)" "finite rs" |
1210 then obtain rs::"rexp set" where "\<Union> (finals A) = \<Union>(L ` rs)" "finite rs" |
1226 using f by (auto dest: bchoice_finite_set) |
1211 using fin by (auto dest: bchoice_finite_set) |
1227 then have "A = L (\<Uplus>rs)" |
1212 then have "A = L (\<Uplus>rs)" |
1228 unfolding lang_is_union_of_finals[symmetric] by simp |
1213 unfolding lang_is_union_of_finals[symmetric] by simp |
1229 then show "\<exists>r::rexp. A = L r" by blast |
1214 then show "\<exists>r::rexp. A = L r" by blast |
1230 qed |
1215 qed |
1231 |
1216 |