36 unfolding lang_seq_def |
36 unfolding lang_seq_def |
37 apply(auto) |
37 apply(auto) |
38 apply(metis) |
38 apply(metis) |
39 by (metis append_assoc) |
39 by (metis append_assoc) |
40 |
40 |
41 lemma lang_seq_minus: |
|
42 shows "(L1; L2) - {[]} = |
|
43 (if [] \<in> L1 then L2 - {[]} else {}) \<union> |
|
44 (if [] \<in> L2 then L1 - {[]} else {}) \<union> ((L1 - {[]}); (L2 - {[]}))" |
|
45 apply(auto simp add: lang_seq_def) |
|
46 apply(metis mem_def self_append_conv) |
|
47 apply(metis mem_def self_append_conv2) |
|
48 apply(metis mem_def self_append_conv2) |
|
49 apply(metis mem_def self_append_conv) |
|
50 done |
|
51 |
41 |
52 section {* Kleene star for languages defined as least fixed point *} |
42 section {* Kleene star for languages defined as least fixed point *} |
53 |
43 |
54 inductive_set |
44 inductive_set |
55 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
45 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
268 from as2 nemp |
258 from as2 nemp |
269 have f2: "X \<subseteq> B; A\<star>" using arden_aux1 by auto |
259 have f2: "X \<subseteq> B; A\<star>" using arden_aux1 by auto |
270 from f1 f2 show "X = B; A\<star>" by auto |
260 from f1 f2 show "X = B; A\<star>" by auto |
271 qed |
261 qed |
272 |
262 |
|
263 |
|
264 |
273 section {* equiv class' definition *} |
265 section {* equiv class' definition *} |
274 |
266 |
275 definition |
267 definition |
276 equiv_str :: "string \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> bool" ("_ \<equiv>_\<equiv> _" [100, 100, 100] 100) |
268 equiv_str :: "string \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> bool" ("_ \<equiv>_\<equiv> _" [100, 100, 100] 100) |
277 where |
269 where |
286 |
278 |
287 definition |
279 definition |
288 quot :: "string set \<Rightarrow> string set \<Rightarrow> (string set) set" ("_ Quo _" [100, 100] 100) |
280 quot :: "string set \<Rightarrow> string set \<Rightarrow> (string set) set" ("_ Quo _" [100, 100] 100) |
289 where |
281 where |
290 "L1 Quo L2 \<equiv> { \<lbrakk>x\<rbrakk>L2 | x. x \<in> L1}" |
282 "L1 Quo L2 \<equiv> { \<lbrakk>x\<rbrakk>L2 | x. x \<in> L1}" |
291 |
|
292 |
|
293 |
|
294 |
283 |
295 |
284 |
296 lemma lang_eqs_union_of_eqcls: |
285 lemma lang_eqs_union_of_eqcls: |
297 "Lang = \<Union> {X. X \<in> (UNIV Quo Lang) \<and> (\<forall> x \<in> X. x \<in> Lang)}" |
286 "Lang = \<Union> {X. X \<in> (UNIV Quo Lang) \<and> (\<forall> x \<in> X. x \<in> Lang)}" |
298 proof |
287 proof |
466 by (auto simp:arden_variate_def del_x_paired_def seq_rhs_r_def image_def) |
455 by (auto simp:arden_variate_def del_x_paired_def seq_rhs_r_def image_def) |
467 qed |
456 qed |
468 qed |
457 qed |
469 |
458 |
470 text {* |
459 text {* |
471 arden_variate_valid: proves variation from "X = X;r + Y;ry + \<dots>" to "X = Y;(SEQ ry (STAR r)) + \<dots>" holds the law of "language of left equiv language of right" |
460 arden_variate_valid: proves variation from |
|
461 |
|
462 "X = X;r + Y;ry + \<dots>" to "X = Y;(SEQ ry (STAR r)) + \<dots>" |
|
463 |
|
464 holds the law of "language of left equiv language of right" |
472 *} |
465 *} |
473 lemma arden_variate_valid: |
466 lemma arden_variate_valid: |
474 assumes X_not_empty: "X \<noteq> {[]}" |
467 assumes X_not_empty: "X \<noteq> {[]}" |
475 and l_eq_r: "X = L rhs" |
468 and l_eq_r: "X = L rhs" |
476 and dist: "distinct_rhs rhs" |
469 and dist: "distinct_rhs rhs" |
502 by (simp add:arden_variate_def seq_rhs_r_prop1 del:L_rhs.simps) |
495 by (simp add:arden_variate_def seq_rhs_r_prop1 del:L_rhs.simps) |
503 qed |
496 qed |
504 qed |
497 qed |
505 qed |
498 qed |
506 |
499 |
507 text {* merge_rhs {(X1, r1), (x2, r2}, (x4, r4), \<dots>} {(x1, r1'), (x3, r3'), \<dots>} = {(x1, ALT r1 r1'}, (x2, r2), (x3, r3'), (x4, r4), \<dots>} *} |
500 text {* |
|
501 merge_rhs {(X1, r1), (x2, r2}, (x4, r4), \<dots>} {(x1, r1'), (x3, r3'), \<dots>} = |
|
502 {(x1, ALT r1 r1'}, (x2, r2), (x3, r3'), (x4, r4), \<dots>} *} |
508 definition |
503 definition |
509 merge_rhs :: "t_equa_rhs \<Rightarrow> t_equa_rhs \<Rightarrow> t_equa_rhs" |
504 merge_rhs :: "t_equa_rhs \<Rightarrow> t_equa_rhs \<Rightarrow> t_equa_rhs" |
510 where |
505 where |
511 "merge_rhs rhs rhs' \<equiv> {(X, r). (\<exists> r1 r2. ((X,r1) \<in> rhs \<and> (X, r2) \<in> rhs') \<and> r = ALT r1 r2) \<or> |
506 "merge_rhs rhs rhs' \<equiv> {(X, r). (\<exists> r1 r2. ((X,r1) \<in> rhs \<and> (X, r2) \<in> rhs') \<and> r = ALT r1 r2) \<or> |
512 (\<exists> r1. (X, r1) \<in> rhs \<and> (\<not> (\<exists> r2. (X, r2) \<in> rhs')) \<and> r = r1) \<or> |
507 (\<exists> r1. (X, r1) \<in> rhs \<and> (\<not> (\<exists> r2. (X, r2) \<in> rhs')) \<and> r = r1) \<or> |
680 qed |
675 qed |
681 qed |
676 qed |
682 qed |
677 qed |
683 |
678 |
684 |
679 |
685 (* ********************************* BEGIN: proving the initial equation-system satisfies Inv **************************************** *) |
680 text {* ******BEGIN: proving the initial equation-system satisfies Inv ****** *} |
686 |
681 |
687 lemma distinct_rhs_equations: |
682 lemma distinct_rhs_equations: |
688 "(X, xrhs) \<in> equations (UNIV Quo Lang) \<Longrightarrow> distinct_rhs xrhs" |
683 "(X, xrhs) \<in> equations (UNIV Quo Lang) \<Longrightarrow> distinct_rhs xrhs" |
689 by (auto simp: equations_def equation_rhs_def distinct_rhs_def empty_rhs_def dest:no_two_cls_inters) |
684 by (auto simp: equations_def equation_rhs_def distinct_rhs_def empty_rhs_def dest:no_two_cls_inters) |
690 |
685 |
760 unfolding equations_def equation_rhs_def by auto |
755 unfolding equations_def equation_rhs_def by auto |
761 next |
756 next |
762 assume not_empty: "x \<noteq> []" |
757 assume not_empty: "x \<noteq> []" |
763 hence "\<exists> clist c. x = clist @ [c]" by (case_tac x rule:rev_cases, auto) |
758 hence "\<exists> clist c. x = clist @ [c]" by (case_tac x rule:rev_cases, auto) |
764 then obtain clist c where decom: "x = clist @ [c]" by blast |
759 then obtain clist c where decom: "x = clist @ [c]" by blast |
765 moreover have "\<And> Y. \<lbrakk>Y \<in> UNIV Quo Lang; Y-c\<rightarrow>X; clist \<in> Y\<rbrakk>\<Longrightarrow> [c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})" |
760 moreover have "\<And> Y. \<lbrakk>Y \<in> UNIV Quo Lang; Y-c\<rightarrow>X; clist \<in> Y\<rbrakk> |
|
761 \<Longrightarrow> [c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})" |
766 proof - |
762 proof - |
767 fix Y |
763 fix Y |
768 assume Y_is_eq_cl: "Y \<in> UNIV Quo Lang" |
764 assume Y_is_eq_cl: "Y \<in> UNIV Quo Lang" |
769 and Y_CT_X: "Y-c\<rightarrow>X" |
765 and Y_CT_X: "Y-c\<rightarrow>X" |
770 and clist_in_Y: "clist \<in> Y" |
766 and clist_in_Y: "clist \<in> Y" |
773 by (auto simp :fold_alt_null_eqs) |
769 by (auto simp :fold_alt_null_eqs) |
774 qed |
770 qed |
775 hence "\<exists>Xa. Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" |
771 hence "\<exists>Xa. Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" |
776 using X_in_equas False not_empty "(1)" decom |
772 using X_in_equas False not_empty "(1)" decom |
777 by (auto dest!:every_eqclass_has_ascendent simp:equations_def equation_rhs_def lang_seq_def) |
773 by (auto dest!:every_eqclass_has_ascendent simp:equations_def equation_rhs_def lang_seq_def) |
778 then obtain Xa where "Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" by blast |
774 then obtain Xa where |
779 hence "x \<in> L {(S, folds ALT NULL {CHAR c |c. S-c\<rightarrow>X}) |S. S \<in> UNIV Quo Lang}" using X_in_equas "(1)" decom |
775 "Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" by blast |
|
776 hence "x \<in> L {(S, folds ALT NULL {CHAR c |c. S-c\<rightarrow>X}) |S. S \<in> UNIV Quo Lang}" |
|
777 using X_in_equas "(1)" decom |
780 by (auto simp add:equations_def equation_rhs_def intro!:exI[where x = Xa]) |
778 by (auto simp add:equations_def equation_rhs_def intro!:exI[where x = Xa]) |
781 thus "x \<in> L xrhs" using X_in_equas False not_empty unfolding equations_def equation_rhs_def |
779 thus "x \<in> L xrhs" using X_in_equas False not_empty unfolding equations_def equation_rhs_def |
782 by auto |
780 by auto |
783 qed |
781 qed |
784 qed |
782 qed |
796 by (auto intro:"(2_1)" "(2_2)" simp:equations_def equation_rhs_def lang_seq_def) |
794 by (auto intro:"(2_1)" "(2_2)" simp:equations_def equation_rhs_def lang_seq_def) |
797 qed |
795 qed |
798 qed |
796 qed |
799 qed |
797 qed |
800 |
798 |
801 lemma finite_CT_chars: |
799 |
802 "finite {CHAR c |c. Xa-c\<rightarrow>X}" |
|
803 by (auto) |
|
804 |
800 |
805 lemma no_EMPTY_equations: |
801 lemma no_EMPTY_equations: |
806 "(X, xrhs) \<in> equations CS \<Longrightarrow> no_EMPTY_rhs xrhs" |
802 "(X, xrhs) \<in> equations CS \<Longrightarrow> no_EMPTY_rhs xrhs" |
807 apply (clarsimp simp add:equations_def equation_rhs_def) |
803 apply (clarsimp simp add:equations_def equation_rhs_def) |
808 apply (simp add:no_EMPTY_rhs_def empty_rhs_def, auto) |
804 apply (simp add:no_EMPTY_rhs_def empty_rhs_def, auto) |
809 apply (subgoal_tac "finite {CHAR c |c. Xa-c\<rightarrow>X}", drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_CT_chars)+ |
805 apply (subgoal_tac "finite {CHAR c |c. Xa-c\<rightarrow>X}", drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_charset_rS)+ |
810 done |
806 done |
811 |
807 |
812 lemma init_ES_satisfy_ardenable: |
808 lemma init_ES_satisfy_ardenable: |
813 "(X, xrhs) \<in> equations (UNIV Quo Lang) \<Longrightarrow> ardenable (X, xrhs)" |
809 "(X, xrhs) \<in> equations (UNIV Quo Lang) \<Longrightarrow> ardenable (X, xrhs)" |
814 unfolding ardenable_def |
810 unfolding ardenable_def |
835 by (auto intro!:init_ES_satisfy_ardenable) |
831 by (auto intro!:init_ES_satisfy_ardenable) |
836 ultimately show ?thesis by (simp add:Inv_def) |
832 ultimately show ?thesis by (simp add:Inv_def) |
837 qed |
833 qed |
838 |
834 |
839 |
835 |
840 (* ********************************* END: proving the initial equation-system satisfies Inv **************************************** *) |
836 text {* *********** END: proving the initial equation-system satisfies Inv ******* *} |
841 |
837 |
842 |
838 |
843 (* ***************************** BEGIN: proving every equation-system's iteration step satisfies Inv ******************************* *) |
839 text {* ****** BEGIN: proving every equation-system's iteration step satisfies Inv ***** *} |
844 |
840 |
845 lemma not_T_aux: "\<lbrakk>\<not> TCon (insert a A); x = a\<rbrakk> |
841 lemma not_T_aux: "\<lbrakk>\<not> TCon (insert a A); x = a\<rbrakk> |
846 \<Longrightarrow> \<exists>y. x \<noteq> y \<and> y \<in> insert a A " |
842 \<Longrightarrow> \<exists>y. x \<noteq> y \<and> y \<in> insert a A " |
847 apply (case_tac "insert a A = {a}") |
843 apply (case_tac "insert a A = {a}") |
848 by (auto simp:TCon_def) |
844 by (auto simp:TCon_def) |
1145 by (auto elim:non_empty_card_prop[rule_format] simp:Inv_def) |
1141 by (auto elim:non_empty_card_prop[rule_format] simp:Inv_def) |
1146 qed |
1142 qed |
1147 thus ?thesis by blast |
1143 thus ?thesis by blast |
1148 next |
1144 next |
1149 case False |
1145 case False |
1150 --"in this situation, we pick a equation and using ardenable to get a rhs without itself in it, then use equas_subst to form a new equation-system" |
1146 --"in this situation, we pick a equation and using ardenable to get a |
1151 hence "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" using subst Inv_ES |
1147 rhs without itself in it, then use equas_subst to form a new equation-system" |
|
1148 hence "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" |
|
1149 using subst Inv_ES |
1152 by (auto intro:ardenable_prop simp add:Inv_def simp del:L_rhs.simps) |
1150 by (auto intro:ardenable_prop simp add:Inv_def simp del:L_rhs.simps) |
1153 then obtain yrhs' where Y'_l_eq_r: "Y = L yrhs'" |
1151 then obtain yrhs' where Y'_l_eq_r: "Y = L yrhs'" |
1154 and dist_Y': "distinct_rhs yrhs'" |
1152 and dist_Y': "distinct_rhs yrhs'" |
1155 and cls_holds_but_Y: "rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" by blast |
1153 and cls_holds_but_Y: "rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" by blast |
1156 hence "?P (equas_subst ES Y yrhs')" |
1154 hence "?P (equas_subst ES Y yrhs')" |
1181 qed |
1179 qed |
1182 thus ?thesis by blast |
1180 thus ?thesis by blast |
1183 qed |
1181 qed |
1184 qed |
1182 qed |
1185 |
1183 |
1186 (* ****************************** END: proving every equation-system's iteration step satisfies Inv ******************************* *) |
1184 text {* ***** END: proving every equation-system's iteration step satisfies Inv ************** *} |
1187 |
1185 |
1188 lemma iteration_conc: |
1186 lemma iteration_conc: |
1189 assumes history: "Inv X ES" |
1187 assumes history: "Inv X ES" |
1190 shows "\<exists> ES'. Inv X ES' \<and> TCon ES'" (is "\<exists> ES'. ?P ES'") |
1188 shows "\<exists> ES'. Inv X ES' \<and> TCon ES'" (is "\<exists> ES'. ?P ES'") |
1191 proof (cases "TCon ES") |
1189 proof (cases "TCon ES") |
1263 hence "?E r" using X_eq_rhs' by (auto simp add:lang_seq_def) |
1261 hence "?E r" using X_eq_rhs' by (auto simp add:lang_seq_def) |
1264 thus ?thesis by blast |
1262 thus ?thesis by blast |
1265 qed |
1263 qed |
1266 qed |
1264 qed |
1267 |
1265 |
|
1266 text {* definition of a regular language *} |
|
1267 |
|
1268 abbreviation |
|
1269 reg :: "string set => bool" |
|
1270 where |
|
1271 "reg L1 \<equiv> (\<exists>r::rexp. L r = L1)" |
|
1272 |
1268 theorem myhill_nerode: |
1273 theorem myhill_nerode: |
1269 assumes finite_CS: "finite (UNIV Quo Lang)" |
1274 assumes finite_CS: "finite (UNIV Quo Lang)" |
1270 shows "\<exists> (reg::rexp). Lang = L reg" (is "\<exists> r. ?P r") |
1275 shows "\<exists> (reg::rexp). Lang = L reg" (is "\<exists> r. ?P r") |
1271 proof - |
1276 proof - |
1272 have has_r_each: "\<forall>C\<in>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. \<exists>(r::rexp). C = L r" using finite_CS |
1277 have has_r_each: "\<forall>C\<in>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}. \<exists>(r::rexp). C = L r" using finite_CS |
1299 qed |
1304 qed |
1300 |
1305 |
1301 |
1306 |
1302 text {* tests by Christian *} |
1307 text {* tests by Christian *} |
1303 |
1308 |
1304 abbreviation |
1309 (* Alternative definition for Quo *) |
1305 reg :: "string set => bool" |
1310 definition |
1306 where |
1311 QUOT :: "string set \<Rightarrow> (string set) set" |
1307 "reg L1 \<equiv> (\<exists>r::rexp. L r = L1)" |
1312 where |
|
1313 "QUOT Lang \<equiv> (\<Union>x. {\<lbrakk>x\<rbrakk>Lang})" |
|
1314 |
|
1315 lemma test: |
|
1316 "UNIV Quo Lang = QUOT Lang" |
|
1317 by (auto simp add: quot_def QUOT_def) |
1308 |
1318 |
1309 lemma test1: |
1319 lemma test1: |
1310 assumes finite_CS: "finite (UNIV Quo Lang)" |
1320 assumes finite_CS: "finite (QUOT Lang)" |
1311 shows "reg Lang" |
1321 shows "reg Lang" |
1312 using finite_CS |
1322 using finite_CS |
|
1323 unfolding test[symmetric] |
1313 by (auto dest: myhill_nerode) |
1324 by (auto dest: myhill_nerode) |
1314 |
1325 |
1315 lemma t1: "(UNIV Quo {}) = {UNIV}" |
1326 lemma t1: "(QUOT {}) = {UNIV}" |
1316 apply(simp only: quot_def equiv_class_def equiv_str_def) |
1327 apply(simp only: QUOT_def equiv_class_def equiv_str_def) |
1317 apply(simp) |
1328 apply(simp) |
1318 done |
1329 done |
|
1330 |
|
1331 lemma t2: "{[]} \<in> (QUOT {[]})" |
|
1332 apply(simp only: QUOT_def equiv_class_def equiv_str_def) |
|
1333 apply(simp) |
|
1334 apply(simp add: set_eq_iff) |
|
1335 apply(rule_tac x="[]" in exI) |
|
1336 apply(simp) |
|
1337 by (metis eq_commute) |
|
1338 |
|
1339 |
|
1340 lemma t2': "X \<in> (QUOT {[]})" |
|
1341 apply(simp only: QUOT_def equiv_class_def equiv_str_def) |
|
1342 apply(simp) |
|
1343 apply(simp add: set_eq_iff) |
|
1344 apply(rule_tac x="[]" in exI) |
|
1345 apply(simp) |
|
1346 apply(rule allI) |
|
1347 |
|
1348 by (metis eq_commute) |
|
1349 |
|
1350 oops |
|
1351 |
|
1352 lemma |
|
1353 fixes r :: "rexp" |
|
1354 shows "finite (QUOT (L r))" |
|
1355 apply(induct r) |
|
1356 apply(simp add: t1) |
|
1357 apply(simp add: QUOT_def) |
|
1358 apply(simp add: equiv_class_def equiv_str_def) |
|
1359 apply(rule finite_UN_I) |
|
1360 oops |
1319 |
1361 |
1320 lemma |
1362 lemma |
1321 fixes r :: "rexp" |
1363 fixes r :: "rexp" |
1322 shows "finite (UNIV Quo (L r))" |
1364 shows "finite (UNIV Quo (L r))" |
1323 apply(induct r) |
1365 apply(induct r) |
1324 apply(simp add: t1) |
1366 prefer 2 |
1325 oops |
1367 apply(simp add: quot_def) |
1326 |
1368 apply(simp add: equiv_class_def equiv_str_def) |
|
1369 apply(rule finite_UN_I) |
|
1370 apply(simp) |
1327 |
1371 |
1328 |
1372 |
1329 end |
1373 end |