diff -r 663816814e3e -r 85fa86398d39 MyhillNerode.thy
--- a/MyhillNerode.thy	Wed Nov 03 21:42:44 2010 +0000
+++ b/MyhillNerode.thy	Wed Nov 03 22:08:50 2010 +0000
@@ -740,8 +740,12 @@
   shows "X = L xrhs"    
 proof (cases "X = {[]}")
   case True
-  thus ?thesis using X_in_equas 
-    by (simp add:equations_def equation_rhs_def lang_seq_def)
+  thus ?thesis using X_in_equas
+    unfolding equations_def 
+    unfolding equation_rhs_def 
+    apply(simp del: L_rhs.simps)
+    apply(simp add: lang_seq_def)
+    done
 next
   case False 
   show ?thesis
@@ -754,33 +758,32 @@
       proof (cases "x = []")
         assume empty: "x = []"
         hence "x \<in> L (empty_rhs X)" using "(1)"
-          by (auto simp:empty_rhs_def lang_seq_def)
+	  unfolding empty_rhs_def
+          by (simp add: lang_seq_def)
         thus ?thesis using X_in_equas False empty "(1)" 
           unfolding equations_def equation_rhs_def by auto
       next
         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})"
+        then obtain clist c where decom: "x = clist @ [c]" 
+	  using rev_cases by blast
+        moreover have "\<And> Y. Y-c\<rightarrow>X \<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"
-            and Y_CT_X: "Y-c\<rightarrow>X"
-            and clist_in_Y: "clist \<in> Y"
+          assume Y_CT_X: "Y-c\<rightarrow>X"
           with finite_charset_rS 
           show "[c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})"
-            by (auto simp :fold_alt_null_eqs)
+            by (auto simp: fold_alt_null_eqs)
         qed
         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)
+          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
+          "Xa \<in> UNIV Quo Lang" "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
+        thus "x \<in> L xrhs" using X_in_equas False not_empty 
+	  unfolding equations_def equation_rhs_def
           by auto
       qed
     qed
@@ -791,11 +794,14 @@
       assume "(2)": "x \<in> L xrhs"
       have "(2_1)": "\<And> s1 s2 r Xa. \<lbrakk>s1 \<in> Xa; s2 \<in> L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X"
         using finite_charset_rS
-        by (auto simp:CT_def lang_seq_def fold_alt_null_eqs)
+	unfolding CT_def
+        by (simp add: lang_seq_def fold_alt_null_eqs) (auto)
       have "(2_2)": "\<And> s1 s2 Xa r.\<lbrakk>s1 \<in> Xa; s2 \<in> L r; (Xa, r) \<in> empty_rhs X\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X"
-        by (simp add:empty_rhs_def split:if_splits)
-      show "x \<in> X" using X_in_equas False "(2)"         
-        by (auto intro:"(2_1)" "(2_2)" simp:equations_def equation_rhs_def lang_seq_def)
+        by (simp add: empty_rhs_def split: if_splits)
+      show "x \<in> X" using X_in_equas False "(2)"
+        unfolding equations_def
+	unfolding equation_rhs_def
+	by (auto intro:"(2_1)" "(2_2)" simp: lang_seq_def)
     qed
   qed
 qed
@@ -1316,6 +1322,24 @@
 lemma temp_set_ext[no_atp]: "(\<And>x. (x:A) = (x:B)) \<Longrightarrow> (A = B)"
   by(auto intro:set_eqI)
 
+lemma folds_simp_null [simp]:
+  "finite rs \<Longrightarrow> x \<in> L (folds ALT NULL rs) = (\<exists>r \<in> rs. x \<in> L r)"
+apply (simp add: folds_def)
+apply (rule someI2_ex)
+apply (erule finite_imp_fold_graph)
+apply (erule fold_graph.induct)
+apply (auto)
+done
+
+lemma folds_simp_empty [simp]:
+  "finite rs \<Longrightarrow> x \<in> L (folds ALT EMPTY rs) = ((\<exists>r \<in> rs. x \<in> L r) \<or> x = [])"
+apply (simp add: folds_def)
+apply (rule someI2_ex)
+apply (erule finite_imp_fold_graph)
+apply (erule fold_graph.induct)
+apply (auto)
+done
+
 abbreviation
   str_eq ("_ \<approx>_ _")
 where
@@ -1335,7 +1359,7 @@
 text {*
   equivalence classes of x can be written
 
-    (\<approx>Lang)``{x}
+    UNIV // (\<approx>Lang)``{x}
 
   the language quotient can be written
 
@@ -1367,17 +1391,79 @@
 definition
   transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_")
 where
-  "X \<Turnstile>\<Rightarrow> Y \<equiv> {CHAR c | c. X ; {[c]} \<subseteq> Y}"
+  "Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ; {[c]} \<subseteq> X}"
 
 definition
-  "rhs CS X \<equiv> { (Y, X \<Turnstile>\<Rightarrow>Y) | Y. Y \<in> CS }"
+  transitions_rexp ("_ \<turnstile>\<rightarrow> _")
+where
+  "Y \<turnstile>\<rightarrow> X \<equiv> if [] \<in> X then folds ALT EMPTY (Y \<Turnstile>\<Rightarrow>X) else folds ALT NULL (Y \<Turnstile>\<Rightarrow>X)"
 
 definition
-  "rhs_sem CS X \<equiv> { (Y; L (folds ALT NULL (X \<Turnstile>\<Rightarrow>Y))) | Y. Y \<in> CS }"
+  "rhs CS X \<equiv> { (Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS }"
+
+definition
+  "rhs_sem CS X \<equiv> { (Y; L (Y \<turnstile>\<rightarrow> X)) | Y. Y \<in> CS }"
 
 definition
   "eqs CS \<equiv> (\<Union>X \<in> CS. {(X, rhs CS X)})"
 
+definition
+  "eqs_sem CS \<equiv> (\<Union>X \<in> CS. {(X, rhs_sem CS X)})"
+
+(*
+lemma 
+  assumes X_in_equas: "(X, rhss) \<in> (eqs_sem (UNIV // (\<approx>Lang)))"
+  shows "X = \<Union>rhss"
+using assms
+proof (cases "X = {[]}")
+  case True
+  thus ?thesis using X_in_equas 
+    by (simp add:equations_def equation_rhs_def lang_seq_def)
+next
+  case False 
+  show ?thesis
+  proof 
+    show "X \<subseteq> L xrhs"
+    proof
+      fix x
+      assume "(1)": "x \<in> X"
+      show "x \<in> L xrhs"          
+      proof (cases "x = []")
+        assume empty: "x = []"
+        hence "x \<in> L (empty_rhs X)" using "(1)"
+          by (auto simp:empty_rhs_def lang_seq_def)
+        thus ?thesis using X_in_equas False empty "(1)" 
+          unfolding equations_def equation_rhs_def by auto
+      next
+        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})"
+        proof -
+          fix Y
+          assume Y_is_eq_cl: "Y \<in> UNIV Quo Lang"
+            and Y_CT_X: "Y-c\<rightarrow>X"
+            and clist_in_Y: "clist \<in> Y"
+          with finite_charset_rS 
+          show "[c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})"
+            by (auto simp :fold_alt_null_eqs)
+        qed
+        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
+          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
+      qed
+    qed
+  next
+*)
+
 lemma finite_rhs:
   assumes fin: "finite CS"
   shows "finite (rhs CS X)"
@@ -1393,8 +1479,25 @@
 done
 
 lemma
-  shows "X ; L (folds ALT NULL X \<Turnstile>\<Rightarrow> Y) \<subseteq> Y" 
-by (auto simp add: transitions_def lang_seq_def fold_alt_null_eqs)
+  shows "X ; L (folds ALT NULL (X \<Turnstile>\<Rightarrow> Y)) \<subseteq> Y" 
+by (auto simp add: transitions_def lang_seq_def)
+
+lemma
+  shows "X ; L (X \<turnstile>\<rightarrow> Y) \<subseteq> Y" 
+apply (auto simp add: transitions_rexp_def transitions_def lang_seq_def)
+oops
+
+lemma 
+  "equation_rhs CS X = rhs CS X"
+apply(simp only: rhs_def empty_rhs_def CT_def transitions_rexp_def transitions_def equation_rhs_def)
+oops
+
+
+
+lemma
+  shows "X ; L (X \<turnstile>\<rightarrow> Y) \<subseteq> Y" 
+apply (auto simp add: transitions_rexp_def transitions_def lang_seq_def)
+oops
 
 lemma
   assumes a: "X \<in> (UNIV // (\<approx>Lang))"
@@ -1405,27 +1508,62 @@
 apply(simp)
 apply(simp add: quotient_def Image_def)
 apply(subst (4) mem_def)
-apply(simp)
-using a
-apply(simp add: quotient_def Image_def)
-apply(subst (asm) (2) mem_def)
-apply(simp)
-apply(rule_tac x="X" in exI)
-apply(simp)
-apply(erule exE)
-apply(simp)
-apply(rule temp_set_ext)
-apply(simp)
-apply(rule iffI)
-apply(rule_tac x="x" in exI)
-apply(simp)
 oops
 
-lemma tt: "\<lbrakk>A = B; C \<subseteq> B\<rbrakk> \<Longrightarrow> C \<subseteq> A" by simp 
+
+lemma UNIV_eq_complement:
+  "UNIV // (\<approx>Lang) = UNIV // (\<approx>(- Lang))"
+by auto
+
+lemma eq_inter:
+  fixes x y::"string"
+  shows "\<lbrakk>x \<approx>L1 y; x \<approx>L2 y\<rbrakk> \<Longrightarrow> (x \<approx>(L1 \<inter> L2) y)"
+by auto
+
+lemma equ_union:
+  fixes x y::"string"
+  shows "\<lbrakk>x \<approx>L1 y; x \<approx>L2 y\<rbrakk> \<Longrightarrow> (x \<approx>(L1 \<union> L2) y)"
+by auto
+
+(* HERE *)
+
+lemma tt:
+  "R1 \<subseteq> R2 \<Longrightarrow> R1 `` {x} \<subseteq> R2 `` {x}"
+unfolding Image_def
+by auto
+
+lemma tt_aux:
+  "(\<approx>Lang) `` {x} = \<lbrakk>x\<rbrakk>Lang"
+unfolding Image_def
+unfolding equiv_class_def
+unfolding equiv_str_def
+unfolding mem_def
+apply(simp)
+done
+
+lemma tt_old:
+  "(\<approx>L1) \<subseteq> (\<approx>L2) \<Longrightarrow> \<lbrakk>x\<rbrakk>L1 \<subseteq> \<lbrakk>x\<rbrakk>L2"
+unfolding tt_aux[symmetric]
+apply(simp add: tt)
+done
+
+
+
 
 lemma
-  "UNIV//(\<approx>(L1 \<union> L2)) \<subseteq> (UNIV//(\<approx>L1)) \<union> (UNIV//(\<approx>L2))"
-unfolding quotient_def Image_def
+  assumes a: "finite (A // R1)" "R1 \<subseteq> R2"
+  shows "card (A // R2) <= card (A // R1)"
+using assms
+apply(induct )
+unfolding quotient_def
+apply(drule_tac tt)
+sorry 
+
+lemma other_direction_cu:
+  fixes r::"rexp"
+  shows "finite (UNIV // (\<approx>(L r)))"
+apply(induct r)
+apply(simp_all)
 oops