diff -r 440a01d100eb -r a761b8ac8488 MyhillNerode.thy
--- a/MyhillNerode.thy	Sat Oct 23 12:51:38 2010 +0000
+++ b/MyhillNerode.thy	Sun Oct 24 01:17:44 2010 +0000
@@ -281,9 +281,8 @@
 where
   "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)}"
+  "Lang = (\<Union> {X. X \<in> (UNIV Quo Lang) \<and> (\<forall> x \<in> X. x \<in> Lang)})"
 proof
   show "Lang \<subseteq> \<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}"
   proof
@@ -305,6 +304,7 @@
     by auto
 qed
 
+
 lemma empty_notin_CS: "{} \<notin> UNIV Quo Lang"
 apply (clarsimp simp:quot_def equiv_class_def)
 by (rule_tac x = x in exI, auto simp:equiv_str_def)
@@ -317,7 +317,7 @@
 definition 
   CT :: "string set \<Rightarrow> char \<Rightarrow> string set \<Rightarrow> bool" ("_-_\<rightarrow>_" [99,99]99)
 where
-  "X-c\<rightarrow>Y \<equiv> ((X;{[c]}) \<subseteq> Y)"
+  "X-c\<rightarrow>Y \<equiv> ( X; {[c]} \<subseteq> Y)"
 
 types t_equa_rhs = "(string set \<times> rexp) set"
 
@@ -345,7 +345,7 @@
   equation_rhs :: "(string set) set \<Rightarrow> string set \<Rightarrow> t_equa_rhs"
 where
   "equation_rhs CS X \<equiv> if (X = {[]}) then {({[]}, EMPTY)}
-                         else {(S, folds ALT NULL {CHAR c| c. S-c\<rightarrow>X} )| S. S \<in> CS} \<union> empty_rhs X"
+    else {(S, folds ALT NULL {CHAR c| c. S-c\<rightarrow>X} )| S. S \<in> CS} \<union> empty_rhs X"
 
 definition 
   equations :: "(string set) set \<Rightarrow> t_equas"
@@ -505,7 +505,7 @@
 where
   "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>
                                  (\<exists> r1. (X, r1) \<in> rhs \<and> (\<not> (\<exists> r2. (X, r2) \<in> rhs')) \<and> r = r1) \<or>
-                                 (\<exists> r2. (X, r2) \<in> rhs' \<and> (\<not> (\<exists> r1. (X, r1) \<in> rhs)) \<and> r = r2)    }"                                  
+                                 (\<exists> r2. (X, r2) \<in> rhs' \<and> (\<not> (\<exists> r1. (X, r1) \<in> rhs)) \<and> r = r2)    }"   
 
 
 text {* rhs_subst rhs X=xrhs r: substitude all occurence of X in rhs((X,r) \<in> rhs) with xrhs *}
@@ -631,7 +631,8 @@
 definition Inv :: "string set \<Rightarrow> t_equas \<Rightarrow> bool"
 where
   "Inv X ES \<equiv> finite ES \<and> (\<exists> rhs. (X, rhs) \<in> ES) \<and> distinct_equas ES \<and> 
-            (\<forall> X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs) \<and> X \<noteq> {} \<and> rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls ES))"
+         (\<forall> X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs) \<and> X \<noteq> {} \<and> rhs_eq_cls xrhs 
+              \<subseteq> insert {[]} (left_eq_cls ES))"
 
 text {*
   TCon: Termination Condition of the equation-system decreasion.
@@ -643,11 +644,14 @@
 
 text {* 
   The following is a iteration principle, and is the main framework for the proof:
-   1: We can form the initial equation-system using "equations" defined above, and prove it has invariance Inv by lemma "init_ES_satisfy_Inv";
-   2: We can decrease the number of the equation-system using ardens_lemma_revised and substitution ("equas_subst", defined above), 
-        and prove it holds the property "step" in "wf_iter" by lemma "iteration_step"
-   and finally using property Inv and TCon to prove the myhill-nerode theorem
   
+   1: We can form the initial equation-system using "equations" defined above, 
+      and prove it has invariance Inv by lemma "init_ES_satisfy_Inv";
+   
+   2: We can decrease the number of the equation-system using ardens_lemma_revised 
+      and substitution ("equas_subst", defined above), 
+      and prove it holds the property "step" in "wf_iter" by lemma "iteration_step"
+      and finally using property Inv and TCon to prove the myhill-nerode theorem
 *}
 lemma wf_iter [rule_format]: 
   fixes f
@@ -802,7 +806,8 @@
   "(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_charset_rS)+
+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:
@@ -889,7 +894,8 @@
 lemma ardenable_prop:
   assumes not_lambda: "Y \<noteq> {[]}"
   and ardable: "ardenable (Y, yrhs)"
-  shows "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" (is "\<exists> yrhs'. ?P yrhs'")
+  shows "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" 
+    (is "\<exists> yrhs'. ?P yrhs'")
 proof (cases "(\<exists> reg. (Y, reg) \<in> yrhs)")
   case True
   thus ?thesis 
@@ -1306,12 +1312,58 @@
 
 text {* tests by Christian *}
 
-(* Alternative definition for Quo *)
+lemma temp_set_ext[no_atp]: "(\<And>x. (x:A) = (x:B)) \<Longrightarrow> (A = B)"
+by(auto intro:set_eqI)
+
+fun
+  MNRel
+where
+  "MNRel Lang (x, y) = (x \<equiv>Lang\<equiv> y)"
+
+lemma
+  "equiv UNIV (MNRel Lang)"
+unfolding equiv_def
+unfolding refl_on_def sym_def trans_def
+apply(auto simp add: mem_def equiv_str_def)
+done
+
+lemma
+  "(MNRel Lang)``{x} = \<lbrakk>x\<rbrakk>Lang"
+unfolding equiv_class_def Image_def mem_def
+by (simp)
+
+lemma tt: "\<lbrakk>A = B; C \<subseteq> B\<rbrakk> \<Longrightarrow> C \<subseteq> A" by simp 
+
+lemma
+  "UNIV//(MNRel (L1 \<union> L2)) \<subseteq> (UNIV//(MNRel L1)) \<union> (UNIV//(MNRel L2))"
+unfolding quotient_def
+unfolding UNION_eq_Union_image
+apply(rule tt)
+apply(rule Un_Union_image[symmetric])
+apply(simp)
+apply(rule UN_mono)
+apply(simp)
+apply(simp)
+unfolding Image_def
+unfolding mem_def
+unfolding MNRel.simps
+apply(simp)
+oops
+
+
+
+text {* Alternative definition for Quo *}
 definition 
   QUOT :: "string set \<Rightarrow> (string set) set"  
 where
   "QUOT Lang \<equiv> (\<Union>x. {\<lbrakk>x\<rbrakk>Lang})"
 
+lemma test_01:
+  "Lang \<subseteq> (\<Union> QUOT Lang)"
+unfolding QUOT_def equiv_class_def equiv_str_def
+by (blast)
+
+
 (* by chunhan *)
 lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}"
 proof 
@@ -1394,7 +1446,7 @@
             proof -
               have "xa = [c] \<Longrightarrow> {y. xa \<equiv>{[c]}\<equiv> y} = {[c]}" using in_eqiv
                 apply (simp add:equiv_str_def)
-                apply (rule set_ext, rule iffI, simp)
+                apply (rule temp_set_ext, rule iffI, simp)
                 apply (drule_tac x = "[]" in spec, auto)
                 done   
               thus "xa = [c] \<Longrightarrow> x = {[c]}" using in_eqiv by simp 
@@ -1403,7 +1455,7 @@
             proof -
               have "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> {y. xa \<equiv>{[c]}\<equiv> y} = UNIV - {[],[c]}" 
                 apply (clarsimp simp add:equiv_str_def)
-                apply (rule set_ext, rule iffI, simp)
+                apply (rule temp_set_ext, rule iffI, simp)
                 apply (rule conjI)
                 apply (drule_tac x = "[c]" in spec, simp)
                 apply (drule_tac x = "[]" in spec, simp)
@@ -1429,13 +1481,13 @@
         moreover have "x = {[c]} \<Longrightarrow> x \<in> QUOT {[c]}"
           apply (simp add:QUOT_def equiv_class_def equiv_str_def)
           apply (rule_tac x = "[c]" in exI, simp)
-          apply (rule set_ext, rule iffI, simp+)
+          apply (rule temp_set_ext, rule iffI, simp+)
           by (drule_tac x = "[]" in spec, simp)
         moreover have "x = UNIV - {[],[c]} \<Longrightarrow> x \<in> QUOT {[c]}"
           using exist_another
           apply (clarsimp simp add:QUOT_def equiv_class_def equiv_str_def)        
           apply (rule_tac x = "[a]" in exI, simp)
-          apply (rule set_ext, rule iffI, simp)
+          apply (rule temp_set_ext, rule iffI, simp)
           apply (clarsimp simp:quot_single_aux, simp)
           apply (rule conjI)
           apply (drule_tac x = "[c]" in spec, simp)
@@ -1453,11 +1505,26 @@
 apply (simp add:QUOT_def equiv_class_def equiv_str_def)
 sorry
  
+
+lemma a:
+  "\<lbrakk>x \<equiv>L1\<equiv> y \<and> x \<equiv>L2\<equiv> y\<rbrakk> \<Longrightarrow> x \<equiv>(L1 \<union> L2)\<equiv> y"
+apply(simp add: equiv_str_def)
+done
+
+
+lemma QUOT_union:
+  "(QUOT (L1 \<union> L2)) \<subseteq> ((QUOT L1) \<union> (QUOT L2))"
+sorry
+
+
 lemma quot_alt:
   assumes finite1: "finite (QUOT L\<^isub>1)"
   and finite2: "finite (QUOT L\<^isub>2)"
   shows "finite (QUOT (L\<^isub>1 \<union> L\<^isub>2))"
-sorry
+apply(rule finite_subset)
+apply(rule QUOT_union)
+apply(simp add: finite1 finite2)
+done
 
 lemma quot_star:  
   assumes finite1: "finite (QUOT L\<^isub>1)"
@@ -1470,67 +1537,10 @@
 apply (simp add:QUOT_def equiv_class_def equiv_str_def)
 by (simp_all add:quot_lambda quot_single quot_seq quot_alt quot_star)  
 
-
-
-
-
-
 lemma test: 
   "UNIV Quo Lang = QUOT Lang"
 by (auto simp add: quot_def QUOT_def)
 
-lemma test1:
-  assumes finite_CS: "finite (QUOT Lang)"
-  shows "reg Lang"
-using finite_CS
-unfolding test[symmetric]
-by (auto dest: myhill_nerode)
-
-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)
-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