
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 [] \<in> L1 then L2 - {[]} else {}) \<union> 
-           (if [] \<in> L2 then L1 - {[]} else {}) \<union> ((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\<star>" by auto
 qed
 
+
+
 section {* equiv class' definition *}
 
 definition 
@@ -290,9 +282,6 @@
   "L1 Quo L2 \<equiv> { \<lbrakk>x\<rbrakk>L2 | x. x \<in> L1}" 
 
 
-
-
-
 lemma lang_eqs_union_of_eqcls: 
   "Lang = \<Union> {X. X \<in> (UNIV Quo Lang) \<and> (\<forall> x \<in> X. x \<in> Lang)}"
 proof
@@ -468,7 +457,11 @@
 qed
 
 text {*
-  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" 
+  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" 
 *}
 lemma arden_variate_valid:
   assumes X_not_empty: "X \<noteq> {[]}"
@@ -504,7 +497,9 @@
   qed
 qed
 
-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>} *}  
+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>} *}  
 definition 
   merge_rhs :: "t_equa_rhs \<Rightarrow> t_equa_rhs \<Rightarrow> 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) \<in> equations (UNIV Quo Lang) \<Longrightarrow> distinct_rhs xrhs"
@@ -762,7 +757,8 @@
         assume not_empty: "x \<noteq> []"
         hence "\<exists> 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 "\<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})"
+        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})"
         proof -
           fix Y
           assume Y_is_eq_cl: "Y \<in> UNIV Quo Lang"
@@ -775,8 +771,10 @@
         hence "\<exists>Xa. Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>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 \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" by blast
-        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
+        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
+        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
           by (auto simp add:equations_def equation_rhs_def intro!:exI[where x = Xa])
         thus "x \<in> 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\<rightarrow>X}"
-by (auto)
+
 
 lemma no_EMPTY_equations:
   "(X, xrhs) \<in> equations CS \<Longrightarrow> 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\<rightarrow>X}", drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_CT_chars)+
+apply (subgoal_tac "finite {CHAR c |c. Xa-c\<rightarrow>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: "\<lbrakk>\<not> TCon (insert a A); x = a\<rbrakk>
        \<Longrightarrow> \<exists>y. x \<noteq> y \<and> y \<in> 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 "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> 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 "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> 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 \<equiv> (\<exists>r::rexp. L r = L1)"
+
 theorem myhill_nerode: 
   assumes finite_CS: "finite (UNIV Quo Lang)"
   shows   "\<exists> (reg::rexp). Lang = L reg" (is "\<exists> r. ?P r")
@@ -1301,29 +1306,68 @@
 
 text {* tests by Christian *}
 
-abbreviation
-  reg :: "string set => bool"
+(* Alternative definition for Quo *)
+definition 
+  QUOT :: "string set \<Rightarrow> (string set) set"  
 where
-  "reg L1 \<equiv> (\<exists>r::rexp. L r = L1)"
+  "QUOT Lang \<equiv> (\<Union>x. {\<lbrakk>x\<rbrakk>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: "{[]} \<in> (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 \<in> (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




