# HG changeset patch
# User urbanc
# Date 1287673590 0
# Node ID 1f8fe5bfd38102578f1463ae9bfde3e0cab4d382
# Parent  86167563a1edbe4c9e4f8f48f15261798d95dc06
tried at the end to prove the other direction (failed at the moment)

diff -r 86167563a1ed -r 1f8fe5bfd381 Literature/Tom Henzinger.pdf
Binary file Literature/Tom Henzinger.pdf has changed
diff -r 86167563a1ed -r 1f8fe5bfd381 MyhillNerode.thy
--- a/MyhillNerode.thy	Thu Oct 21 13:42:08 2010 +0000
+++ b/MyhillNerode.thy	Thu Oct 21 15:06:30 2010 +0000
@@ -184,42 +184,6 @@
   shows "L\<star> \<subseteq> L\<star>\<star>"
 by (rule lang_star_simple)
 
-section {* tricky section  *}
-
-lemma k1:
-  assumes b: "s \<in> L\<star>"
-  and a: "s \<noteq> []"
-  shows "s \<in> (L - {[]}); L\<star>"
-using b a
-apply(induct rule: Star.induct)
-apply(simp)
-apply(case_tac "s1=[]")
-apply(simp)
-apply(simp add: lang_seq_def)
-apply(blast)
-done
-
-section {* (relies on lemma k1) *}
-
-lemma zzz:
-  shows "{s. c#s \<in> L1\<star>} = {s. c#s \<in> L1} ; (L1\<star>)"
-apply(auto simp add: lang_seq_def Cons_eq_append_conv)
-apply(drule k1)
-apply(auto)[1]
-apply(auto simp add: lang_seq_def)[1]
-apply(rule_tac x="tl s1" in exI)
-apply(rule_tac x="s2" in exI)
-apply(auto)[1]
-apply(auto simp add: Cons_eq_append_conv)[2]
-apply(drule lang_seq_append)
-apply(assumption)
-apply(rotate_tac 1)
-apply(drule rev_subsetD)
-apply(rule lang_star_seq_subseteq)
-apply(simp)
-done
-
-
 
 section {* regular expressions *}
 
@@ -248,7 +212,7 @@
 end
 
 
-(* ************ now is the codes writen by chunhan ************************************* *)
+text{* ************ now is the codes writen by chunhan ************************************* *}
 
 section {* Arden's Lemma revised *}
 
@@ -311,18 +275,23 @@
 definition 
   equiv_str :: "string \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> bool" ("_ \<equiv>_\<equiv> _" [100, 100, 100] 100)
 where
-  "x \<equiv>L'\<equiv> y \<longleftrightarrow> (\<forall>z. x@z \<in> L' \<longleftrightarrow> y@z \<in> L')"
+  "x \<equiv>Lang\<equiv> y \<longleftrightarrow> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)"
 
 definition
   equiv_class :: "string \<Rightarrow> (string set) \<Rightarrow> string set" ("\<lbrakk>_\<rbrakk>_" [100, 100] 100)
 where
-  "\<lbrakk>x\<rbrakk>L' \<equiv> {y. x \<equiv>L'\<equiv> y}"
+  "\<lbrakk>x\<rbrakk>Lang \<equiv> {y. x \<equiv>Lang\<equiv> y}"
 
 text {* Chunhan modifies Q to Quo *}
+
 definition  
-  quot :: "string set \<Rightarrow> (string set) \<Rightarrow> (string set) set" ("_ Quo _" [100, 100] 100)
+  quot :: "string set \<Rightarrow> string set \<Rightarrow> (string set) set" ("_ Quo _" [100, 100] 100)
 where
-  "L' Quo R \<equiv> { \<lbrakk>x\<rbrakk>R | x. x \<in> L'}" 
+  "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)}"
@@ -367,8 +336,12 @@
 
 types t_equas = "t_equa set"
 
-text {* "empty_rhs" generates "\<lambda>" for init-state, just like "\<lambda>" for final states in Brzozowski method. 
-        But if the init-state is "{[]}" ("\<lambda>" itself) then empty set is returned, see definition of "equation_rhs" *} 
+text {* 
+  "empty_rhs" generates "\<lambda>" for init-state, just like "\<lambda>" for final states 
+  in Brzozowski method. But if the init-state is "{[]}" ("\<lambda>" itself) then 
+  empty set is returned, see definition of "equation_rhs" 
+*} 
+
 definition 
   empty_rhs :: "string set \<Rightarrow> t_equa_rhs"
 where
@@ -1324,5 +1297,33 @@
   qed
   thus ?thesis by blast
 qed 
-  
+
+
+text {* tests by Christian *}
+
+abbreviation
+  reg :: "string set => bool"
+where
+  "reg L1 \<equiv> (\<exists>r::rexp. L r = L1)"
+
+lemma test1:
+  assumes finite_CS: "finite (UNIV Quo Lang)"
+  shows "reg Lang"
+using finite_CS
+by (auto dest: myhill_nerode)
+
+lemma t1: "(UNIV Quo {}) = {UNIV}"
+apply(simp only: quot_def equiv_class_def equiv_str_def)
+apply(simp)
+done
+
+lemma 
+  fixes r :: "rexp"
+  shows "finite (UNIV Quo (L r))"
+apply(induct r)
+apply(simp add: t1)
+oops
+
+
+
 end
\ No newline at end of file