diff -r e31b733ace44 -r f72c82bf59e5 My.thy
--- a/My.thy	Thu Nov 18 11:39:17 2010 +0000
+++ b/My.thy	Thu Nov 25 18:54:45 2010 +0000
@@ -1,12 +1,12 @@
 theory My
-imports Main
+imports Main Infinite_Set
 begin
 
 
 definition
-  lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ; _" [100,100] 100)
+  Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
 where 
-  "L1 ; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
+  "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
 
 inductive_set
   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
@@ -15,6 +15,32 @@
   start[intro]: "[] \<in> L\<star>"
 | step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>"
 
+lemma lang_star_cases:
+  shows "L\<star> =  {[]} \<union> L ;; L\<star>"
+unfolding Seq_def
+by (auto) (metis Star.simps)
+
+lemma lang_star_cases2:
+  shows "L ;; L\<star>  = L\<star> ;; L"
+sorry
+
+
+theorem ardens_revised:
+  assumes nemp: "[] \<notin> A"
+  shows "(X = X ;; A \<union> B) \<longleftrightarrow> (X = B ;; A\<star>)"
+proof
+  assume eq: "X = B ;; A\<star>"
+  have "A\<star> =  {[]} \<union> A\<star> ;; A" sorry
+  then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)" unfolding Seq_def by simp
+  also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"  unfolding Seq_def by auto
+  also have "\<dots> = B \<union> (B ;; A\<star>) ;; A"  unfolding Seq_def
+    by (auto) (metis append_assoc)+
+  finally show "X = X ;; A \<union> B" using eq by auto
+next
+  assume "X = X ;; A \<union> B"
+  then have "B \<subseteq> X" "X ;; A \<subseteq> X" by auto
+  show "X = B ;; A\<star>" sorry
+qed
 
 datatype rexp =
   NULL
@@ -25,14 +51,14 @@
 | STAR rexp
 
 fun
-  L_rexp :: "rexp \<Rightarrow> string set"
+  Sem :: "rexp \<Rightarrow> string set" ("\<lparr>_\<rparr>" [0] 1000)
 where
-    "L_rexp (NULL) = {}"
-  | "L_rexp (EMPTY) = {[]}"
-  | "L_rexp (CHAR c) = {[c]}"
-  | "L_rexp (SEQ r1 r2) = (L_rexp r1) ; (L_rexp r2)"
-  | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"
-  | "L_rexp (STAR r) = (L_rexp r)\<star>"
+    "\<lparr>NULL\<rparr> = {}"
+  | "\<lparr>EMPTY\<rparr> = {[]}"
+  | "\<lparr>CHAR c\<rparr> = {[c]}"
+  | "\<lparr>SEQ r1 r2\<rparr> = \<lparr>r1\<rparr> ;; \<lparr>r2\<rparr>"
+  | "\<lparr>ALT r1 r2\<rparr> = \<lparr>r1\<rparr> \<union> \<lparr>r2\<rparr>"
+  | "\<lparr>STAR r\<rparr> = \<lparr>r\<rparr>\<star>"
 
 definition 
   folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
@@ -40,7 +66,7 @@
   "folds f z S \<equiv> SOME x. fold_graph f z S x"
 
 lemma folds_simp_null [simp]:
-  "finite rs \<Longrightarrow> x \<in> L_rexp (folds ALT NULL rs) = (\<exists>r \<in> rs. x \<in> L_rexp r)"
+  "finite rs \<Longrightarrow> x \<in> \<lparr>folds ALT NULL rs\<rparr> \<longleftrightarrow> (\<exists>r \<in> rs. x \<in> \<lparr>r\<rparr>)"
 apply (simp add: folds_def)
 apply (rule someI2_ex)
 apply (erule finite_imp_fold_graph)
@@ -49,7 +75,7 @@
 done
 
 lemma folds_simp_empty [simp]:
-  "finite rs \<Longrightarrow> x \<in> L_rexp (folds ALT EMPTY rs) = ((\<exists>r \<in> rs. x \<in> L_rexp r) \<or> x = [])"
+  "finite rs \<Longrightarrow> x \<in> \<lparr>folds ALT EMPTY rs\<rparr> \<longleftrightarrow> (\<exists>r \<in> rs. x \<in> \<lparr>r\<rparr>) \<or> x = []"
 apply (simp add: folds_def)
 apply (rule someI2_ex)
 apply (erule finite_imp_fold_graph)
@@ -58,7 +84,7 @@
 done
 
 lemma [simp]:
-  "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
+  shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
 by simp
 
 definition
@@ -103,11 +129,11 @@
 qed
 
 lemma all_rexp:
-  "\<lbrakk>finite (UNIV // \<approx>Lang); X \<in> (UNIV // \<approx>Lang)\<rbrakk> \<Longrightarrow> \<exists>r. X = L_rexp r"
+  "\<lbrakk>finite (UNIV // \<approx>Lang); X \<in> (UNIV // \<approx>Lang)\<rbrakk> \<Longrightarrow> \<exists>r. X = \<lparr>r\<rparr>"
 sorry
 
 lemma final_rexp:
-  "\<lbrakk>finite (UNIV // (\<approx>Lang)); final X Lang\<rbrakk> \<Longrightarrow> \<exists>r. X = L_rexp r"
+  "\<lbrakk>finite (UNIV // (\<approx>Lang)); final X Lang\<rbrakk> \<Longrightarrow> \<exists>r. X = \<lparr>r\<rparr>"
 unfolding final_def
 using all_rexp by blast
 
@@ -132,12 +158,12 @@
 lemma finite_regular_aux:
   fixes Lang :: "string set"
   assumes "finite (UNIV // (\<approx>Lang))"
-  shows "\<exists>rs. Lang =  L_rexp (folds ALT NULL rs)"
+  shows "\<exists>rs. Lang = \<lparr>folds ALT NULL rs\<rparr>"
 apply(subst lang_is_union_of_finals)
 using assms
 apply -
 apply(drule finite_final)
-apply(drule_tac f="L_rexp" in finite_f_one_to_one)
+apply(drule_tac f="Sem" in finite_f_one_to_one)
 apply(clarify)
 apply(drule final_rexp[OF assms])
 apply(auto)[1]
@@ -151,7 +177,7 @@
 lemma finite_regular:
   fixes Lang :: "string set"
   assumes "finite (UNIV // (\<approx>Lang))"
-  shows "\<exists>r. Lang =  L_rexp r"
+  shows "\<exists>r. Lang =  \<lparr>r\<rparr>"
 using assms finite_regular_aux
 by auto
 
@@ -239,7 +265,7 @@
 definition
   transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_")
 where
-  "Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ; {[c]} \<subseteq> X}"
+  "Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ;; {[c]} \<subseteq> X}"
 
 definition
   transitions_rexp ("_ \<turnstile>\<rightarrow> _")
@@ -250,7 +276,7 @@
   "rhs CS X \<equiv> if X = {[]} then {({[]}, EMPTY)} else {(Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS}"
 
 definition
-  "rhs_sem CS X \<equiv> \<Union> {(Y; L_rexp r) | Y r . (Y, r) \<in> rhs CS X}"
+  "rhs_sem CS X \<equiv> \<Union> {(Y;; \<lparr>r\<rparr>) | Y r . (Y, r) \<in> rhs CS X}"
 
 definition
   "eqs CS \<equiv> (\<Union>X \<in> CS. {(X, rhs CS X)})"
@@ -276,7 +302,7 @@
 lemma every_eqclass_has_transition:
   assumes has_str: "s @ [c] \<in> X"
   and     in_CS:   "X \<in> UNIV // (\<approx>Lang)"
-  obtains Y where "Y \<in> UNIV // (\<approx>Lang)" and "Y ; {[c]} \<subseteq> X" and "s \<in> Y"
+  obtains Y where "Y \<in> UNIV // (\<approx>Lang)" and "Y ;; {[c]} \<subseteq> X" and "s \<in> Y"
 proof -
   def Y \<equiv> "(\<approx>Lang) `` {s}"
   have "Y \<in> UNIV // (\<approx>Lang)" 
@@ -284,22 +310,21 @@
   moreover
   have "X = (\<approx>Lang) `` {s @ [c]}" 
     using has_str in_CS defined_by_str by blast
-  then have "Y ; {[c]} \<subseteq> X" 
-    unfolding Y_def Image_def lang_seq_def
+  then have "Y ;; {[c]} \<subseteq> X" 
+    unfolding Y_def Image_def Seq_def
     unfolding str_eq_rel_def
     by (auto) (simp add: str_eq_def)
   moreover
   have "s \<in> Y" unfolding Y_def 
     unfolding Image_def str_eq_rel_def str_eq_def by simp
-  moreover 
-  have "True" by simp (* FIXME *)
-  note that 
-  ultimately show thesis by blast
+  (*moreover 
+  have "True" by simp FIXME *) 
+  ultimately show thesis by (blast intro: that)
 qed
 
 lemma test:
   assumes "[] \<in> X"
-  shows "[] \<in> L_rexp (Y \<turnstile>\<rightarrow> X)"
+  shows "[] \<in> \<lparr>Y \<turnstile>\<rightarrow> X\<rparr>"
 using assms
 by (simp add: transitions_rexp_def)
 
@@ -308,7 +333,7 @@
   shows "X \<subseteq> rhs_sem (UNIV // (\<approx>Lang)) X"
 apply(case_tac "X = {[]}")
 apply(simp)
-apply(simp add: rhs_sem_def rhs_def lang_seq_def)
+apply(simp add: rhs_sem_def rhs_def Seq_def)
 apply(rule subsetI)
 apply(case_tac "x = []")
 apply(simp add: rhs_sem_def rhs_def)
@@ -317,4 +342,48 @@
 apply(rule_tac x = "X" in exI)
 apply(simp add: assms)
 apply(simp add: transitions_rexp_def)
-oops
\ No newline at end of file
+oops
+
+
+(*
+fun
+  power :: "string \<Rightarrow> nat \<Rightarrow> string" (infixr "\<Up>" 100)
+where
+  "s \<Up> 0 = s"
+| "s \<Up> (Suc n) = s @ (s \<Up> n)"
+
+definition 
+ "Lone = {(''0'' \<Up> n) @ (''1'' \<Up> n) | n. True }"
+
+lemma
+  "infinite (UNIV // (\<approx>Lone))"
+unfolding infinite_iff_countable_subset
+apply(rule_tac x="\<lambda>n. {(''0'' \<Up> n) @ (''1'' \<Up> i) | i. i \<in> {..n} }" in exI)
+apply(auto)
+prefer 2
+unfolding Lone_def
+unfolding quotient_def
+unfolding Image_def
+apply(simp)
+unfolding str_eq_rel_def
+unfolding str_eq_def
+apply(auto)
+apply(rule_tac x="''0'' \<Up> n" in exI)
+apply(auto)
+unfolding infinite_nat_iff_unbounded
+unfolding Lone_def
+*)
+
+
+
+text {* Derivatives *}
+
+definition
+  DERS :: "string \<Rightarrow> string set \<Rightarrow> string set"
+where
+  "DERS s L \<equiv> {s'. s @ s' \<in> L}"
+
+lemma
+  shows "x \<approx>L y \<longleftrightarrow> DERS x L = DERS y L"
+unfolding DERS_def str_eq_def
+by auto
\ No newline at end of file