# HG changeset patch # User urbanc # Date 1287776636 0 # Node ID 475dd40cd73440d55c7f13189b50ffd7596f1ab8 # Parent 9563a9cd28d37b902709bc36b5f0a56cca75ea75 deleted two unnecessary lemmas diff -r 9563a9cd28d3 -r 475dd40cd734 MyhillNerode.thy --- a/MyhillNerode.thy Fri Oct 22 10:45:01 2010 +0000 +++ b/MyhillNerode.thy Fri Oct 22 19:43:56 2010 +0000 @@ -38,16 +38,6 @@ apply(metis) by (metis append_assoc) -lemma lang_seq_minus: - shows "(L1; L2) - {[]} = - (if [] \ L1 then L2 - {[]} else {}) \ - (if [] \ L2 then L1 - {[]} else {}) \ ((L1 - {[]}); (L2 - {[]}))" -apply(auto simp add: lang_seq_def) -apply(metis mem_def self_append_conv) -apply(metis mem_def self_append_conv2) -apply(metis mem_def self_append_conv2) -apply(metis mem_def self_append_conv) -done section {* Kleene star for languages defined as least fixed point *} @@ -270,6 +260,8 @@ from f1 f2 show "X = B; A\" by auto qed + + section {* equiv class' definition *} definition @@ -290,9 +282,6 @@ "L1 Quo L2 \ { \x\L2 | x. x \ L1}" - - - lemma lang_eqs_union_of_eqcls: "Lang = \ {X. X \ (UNIV Quo Lang) \ (\ x \ X. x \ Lang)}" proof @@ -468,7 +457,11 @@ qed text {* - arden_variate_valid: proves variation from "X = X;r + Y;ry + \" to "X = Y;(SEQ ry (STAR r)) + \" holds the law of "language of left equiv language of right" + arden_variate_valid: proves variation from + + "X = X;r + Y;ry + \" to "X = Y;(SEQ ry (STAR r)) + \" + + holds the law of "language of left equiv language of right" *} lemma arden_variate_valid: assumes X_not_empty: "X \ {[]}" @@ -504,7 +497,9 @@ qed qed -text {* merge_rhs {(X1, r1), (x2, r2}, (x4, r4), \} {(x1, r1'), (x3, r3'), \} = {(x1, ALT r1 r1'}, (x2, r2), (x3, r3'), (x4, r4), \} *} +text {* + merge_rhs {(X1, r1), (x2, r2}, (x4, r4), \} {(x1, r1'), (x3, r3'), \} = + {(x1, ALT r1 r1'}, (x2, r2), (x3, r3'), (x4, r4), \} *} definition merge_rhs :: "t_equa_rhs \ t_equa_rhs \ t_equa_rhs" where @@ -682,7 +677,7 @@ qed -(* ********************************* BEGIN: proving the initial equation-system satisfies Inv **************************************** *) +text {* ******BEGIN: proving the initial equation-system satisfies Inv ****** *} lemma distinct_rhs_equations: "(X, xrhs) \ equations (UNIV Quo Lang) \ distinct_rhs xrhs" @@ -762,7 +757,8 @@ assume not_empty: "x \ []" hence "\ clist c. x = clist @ [c]" by (case_tac x rule:rev_cases, auto) then obtain clist c where decom: "x = clist @ [c]" by blast - moreover have "\ Y. \Y \ UNIV Quo Lang; Y-c\X; clist \ Y\\ [c] \ L (folds ALT NULL {CHAR c |c. Y-c\X})" + moreover have "\ Y. \Y \ UNIV Quo Lang; Y-c\X; clist \ Y\ + \ [c] \ L (folds ALT NULL {CHAR c |c. Y-c\X})" proof - fix Y assume Y_is_eq_cl: "Y \ UNIV Quo Lang" @@ -775,8 +771,10 @@ hence "\Xa. Xa \ UNIV Quo Lang \ clist @ [c] \ Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\X})" using X_in_equas False not_empty "(1)" decom by (auto dest!:every_eqclass_has_ascendent simp:equations_def equation_rhs_def lang_seq_def) - then obtain Xa where "Xa \ UNIV Quo Lang \ clist @ [c] \ Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\X})" by blast - hence "x \ L {(S, folds ALT NULL {CHAR c |c. S-c\X}) |S. S \ UNIV Quo Lang}" using X_in_equas "(1)" decom + then obtain Xa where + "Xa \ UNIV Quo Lang \ clist @ [c] \ Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\X})" by blast + hence "x \ L {(S, folds ALT NULL {CHAR c |c. S-c\X}) |S. S \ UNIV Quo Lang}" + using X_in_equas "(1)" decom by (auto simp add:equations_def equation_rhs_def intro!:exI[where x = Xa]) thus "x \ L xrhs" using X_in_equas False not_empty unfolding equations_def equation_rhs_def by auto @@ -798,15 +796,13 @@ qed qed -lemma finite_CT_chars: - "finite {CHAR c |c. Xa-c\X}" -by (auto) + lemma no_EMPTY_equations: "(X, xrhs) \ equations CS \ no_EMPTY_rhs xrhs" apply (clarsimp simp add:equations_def equation_rhs_def) apply (simp add:no_EMPTY_rhs_def empty_rhs_def, auto) -apply (subgoal_tac "finite {CHAR c |c. Xa-c\X}", drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_CT_chars)+ +apply (subgoal_tac "finite {CHAR c |c. Xa-c\X}", drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_charset_rS)+ done lemma init_ES_satisfy_ardenable: @@ -837,10 +833,10 @@ qed -(* ********************************* END: proving the initial equation-system satisfies Inv **************************************** *) +text {* *********** END: proving the initial equation-system satisfies Inv ******* *} -(* ***************************** BEGIN: proving every equation-system's iteration step satisfies Inv ******************************* *) +text {* ****** BEGIN: proving every equation-system's iteration step satisfies Inv ***** *} lemma not_T_aux: "\\ TCon (insert a A); x = a\ \ \y. x \ y \ y \ insert a A " @@ -1147,8 +1143,10 @@ thus ?thesis by blast next case False - --"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" - hence "\ yrhs'. Y = L yrhs' \ distinct_rhs yrhs' \ rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" using subst Inv_ES + --"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" + hence "\ yrhs'. Y = L yrhs' \ distinct_rhs yrhs' \ rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" + using subst Inv_ES by (auto intro:ardenable_prop simp add:Inv_def simp del:L_rhs.simps) then obtain yrhs' where Y'_l_eq_r: "Y = L yrhs'" and dist_Y': "distinct_rhs yrhs'" @@ -1183,7 +1181,7 @@ qed qed -(* ****************************** END: proving every equation-system's iteration step satisfies Inv ******************************* *) +text {* ***** END: proving every equation-system's iteration step satisfies Inv ************** *} lemma iteration_conc: assumes history: "Inv X ES" @@ -1265,6 +1263,13 @@ qed qed +text {* definition of a regular language *} + +abbreviation + reg :: "string set => bool" +where + "reg L1 \ (\r::rexp. L r = L1)" + theorem myhill_nerode: assumes finite_CS: "finite (UNIV Quo Lang)" shows "\ (reg::rexp). Lang = L reg" (is "\ r. ?P r") @@ -1301,29 +1306,68 @@ text {* tests by Christian *} -abbreviation - reg :: "string set => bool" +(* Alternative definition for Quo *) +definition + QUOT :: "string set \ (string set) set" where - "reg L1 \ (\r::rexp. L r = L1)" + "QUOT Lang \ (\x. {\x\Lang})" + +lemma test: + "UNIV Quo Lang = QUOT Lang" +by (auto simp add: quot_def QUOT_def) lemma test1: - assumes finite_CS: "finite (UNIV Quo Lang)" + assumes finite_CS: "finite (QUOT Lang)" shows "reg Lang" using finite_CS +unfolding test[symmetric] by (auto dest: myhill_nerode) -lemma t1: "(UNIV Quo {}) = {UNIV}" -apply(simp only: quot_def equiv_class_def equiv_str_def) +lemma t1: "(QUOT {}) = {UNIV}" +apply(simp only: QUOT_def equiv_class_def equiv_str_def) apply(simp) done +lemma t2: "{[]} \ (QUOT {[]})" +apply(simp only: QUOT_def equiv_class_def equiv_str_def) +apply(simp) +apply(simp add: set_eq_iff) +apply(rule_tac x="[]" in exI) +apply(simp) +by (metis eq_commute) + + +lemma t2': "X \ (QUOT {[]})" +apply(simp only: QUOT_def equiv_class_def equiv_str_def) +apply(simp) +apply(simp add: set_eq_iff) +apply(rule_tac x="[]" in exI) +apply(simp) +apply(rule allI) + +by (metis eq_commute) + +oops + +lemma + fixes r :: "rexp" + shows "finite (QUOT (L r))" +apply(induct r) +apply(simp add: t1) +apply(simp add: QUOT_def) +apply(simp add: equiv_class_def equiv_str_def) +apply(rule finite_UN_I) +oops + lemma fixes r :: "rexp" shows "finite (UNIV Quo (L r))" apply(induct r) -apply(simp add: t1) -oops - +prefer 2 +apply(simp add: quot_def) +apply(simp add: equiv_class_def equiv_str_def) +apply(rule finite_UN_I) +apply(simp) end \ No newline at end of file