--- a/My.thy	Fri Jun 03 13:59:21 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,389 +0,0 @@
-theory My
-imports Main Infinite_Set
-begin
-
-
-definition
-  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}"
-
-inductive_set
-  Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
-  for L :: "string set"
-where
-  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
-| EMPTY
-| CHAR char
-| SEQ rexp rexp
-| ALT rexp rexp
-| STAR rexp
-
-fun
-  Sem :: "rexp \<Rightarrow> string set" ("\<lparr>_\<rparr>" [0] 1000)
-where
-    "\<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"
-where
-  "folds f z S \<equiv> SOME x. fold_graph f z S x"
-
-lemma folds_simp_null [simp]:
-  "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)
-apply (erule fold_graph.induct)
-apply (auto)
-done
-
-lemma folds_simp_empty [simp]:
-  "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)
-apply (erule fold_graph.induct)
-apply (auto)
-done
-
-lemma [simp]:
-  shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
-by simp
-
-definition
-  str_eq ("_ \<approx>_ _")
-where
-  "x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)"
-
-definition
-  str_eq_rel ("\<approx>_")
-where
-  "\<approx>Lang \<equiv> {(x, y). x \<approx>Lang y}"
-
-definition
-  final :: "string set \<Rightarrow> string set \<Rightarrow> bool"
-where
-  "final X Lang \<equiv> (X \<in> UNIV // \<approx>Lang) \<and> (\<forall>s \<in> X. s \<in> Lang)"
-
-lemma lang_is_union_of_finals: 
-  "Lang = \<Union> {X. final X Lang}"
-proof -
-  have  "Lang \<subseteq> \<Union> {X. final X Lang}"
-    unfolding final_def
-    unfolding quotient_def Image_def
-    unfolding str_eq_rel_def
-    apply(simp)
-    apply(auto)
-    apply(rule_tac x="(\<approx>Lang) `` {x}" in exI)
-    unfolding Image_def
-    unfolding str_eq_rel_def
-    apply(auto)
-    unfolding str_eq_def
-    apply(auto)
-    apply(drule_tac x="[]" in spec)
-    apply(simp)
-    done
-  moreover
-  have "\<Union>{X. final X Lang} \<subseteq> Lang" 
-    unfolding final_def by auto
-  ultimately 
-  show "Lang = \<Union> {X. final X Lang}"
-    by blast
-qed
-
-lemma all_rexp:
-  "\<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 = \<lparr>r\<rparr>"
-unfolding final_def
-using all_rexp by blast
-
-lemma finite_f_one_to_one:
-  assumes "finite B"
-  and "\<forall>x \<in> B. \<exists>y. f y = x"
-  shows "\<exists>rs. finite rs \<and> (B = {f y | y . y \<in> rs})"
-using assms
-by (induct) (auto)
-
-lemma finite_final:
-  assumes "finite (UNIV // (\<approx>Lang))"
-  shows "finite {X. final X Lang}"
-using assms
-proof -
-  have "{X. final X Lang} \<subseteq> (UNIV // (\<approx>Lang))"
-    unfolding final_def by auto
-  with assms show "finite {X. final X Lang}" 
-    using finite_subset by auto
-qed
-
-lemma finite_regular_aux:
-  fixes Lang :: "string set"
-  assumes "finite (UNIV // (\<approx>Lang))"
-  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="Sem" in finite_f_one_to_one)
-apply(clarify)
-apply(drule final_rexp[OF assms])
-apply(auto)[1]
-apply(clarify)
-apply(rule_tac x="rs" in exI)
-apply(simp)
-apply(rule set_eqI)
-apply(auto)
-done
-
-lemma finite_regular:
-  fixes Lang :: "string set"
-  assumes "finite (UNIV // (\<approx>Lang))"
-  shows "\<exists>r. Lang =  \<lparr>r\<rparr>"
-using assms finite_regular_aux
-by auto
-
-
-
-section {* other direction *}
-
-
-lemma inj_image_lang:
-  fixes f::"string \<Rightarrow> 'a"
-  assumes str_inj: "\<And>x y. f x = f y \<Longrightarrow> x \<approx>Lang y"
-  shows "inj_on (image f) (UNIV // (\<approx>Lang))"
-proof - 
-  { fix x y::string
-    assume eq_tag: "f ` {z. x \<approx>Lang z} = f ` {z. y \<approx>Lang z}"
-    moreover
-    have "{z. x \<approx>Lang z} \<noteq> {}" unfolding str_eq_def by auto
-    ultimately obtain a b where "x \<approx>Lang a" "y \<approx>Lang b" "f a = f b" by blast
-    then have "x \<approx>Lang a" "y \<approx>Lang b" "a \<approx>Lang b" using str_inj by auto
-    then have "x \<approx>Lang y" unfolding str_eq_def by simp 
-    then have "{z. x \<approx>Lang z} = {z. y \<approx>Lang z}" unfolding str_eq_def by simp
-  }
-  then have "\<forall>x\<in>UNIV // \<approx>Lang. \<forall>y\<in>UNIV // \<approx>Lang. f ` x = f ` y \<longrightarrow> x = y"
-    unfolding quotient_def Image_def str_eq_rel_def by simp
-  then show "inj_on (image f) (UNIV // (\<approx>Lang))"
-    unfolding inj_on_def by simp
-qed
-
-
-lemma finite_range_image: 
-  assumes fin: "finite (range f)"
-  shows "finite ((image f) ` X)"
-proof -
-  from fin have "finite (Pow (f ` UNIV))" by auto
-  moreover
-  have "(image f) ` X \<subseteq> Pow (f ` UNIV)" by auto
-  ultimately show "finite ((image f) ` X)" using finite_subset by auto
-qed
-
-definition 
-  tag1 :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)"
-where
-  "tag1 L\<^isub>1 L\<^isub>2 \<equiv> \<lambda>x. ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})"
-
-lemma tag1_range_finite:
-  assumes finite1: "finite (UNIV // \<approx>L\<^isub>1)"
-  and finite2: "finite (UNIV // \<approx>L\<^isub>2)"
-  shows "finite (range (tag1 L\<^isub>1 L\<^isub>2))"
-proof -
-  have "finite (UNIV // \<approx>L\<^isub>1 \<times> UNIV // \<approx>L\<^isub>2)" using finite1 finite2 by auto
-  moreover
-  have "range (tag1 L\<^isub>1 L\<^isub>2) \<subseteq> (UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)"
-    unfolding tag1_def quotient_def by auto
-  ultimately show "finite (range (tag1 L\<^isub>1 L\<^isub>2))" 
-    using finite_subset by blast
-qed
-
-lemma tag1_inj:
-  "tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y"
-unfolding tag1_def Image_def str_eq_rel_def str_eq_def
-by auto
-
-lemma quot_alt_cu:
-  fixes L\<^isub>1 L\<^isub>2::"string set"
-  assumes fin1: "finite (UNIV // \<approx>L\<^isub>1)"
-  and fin2: "finite (UNIV // \<approx>L\<^isub>2)"
-  shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"
-proof -
-  have "finite (range (tag1 L\<^isub>1 L\<^isub>2))" 
-    using fin1 fin2 tag1_range_finite by simp
-  then have "finite (image (tag1 L\<^isub>1 L\<^isub>2) ` (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2)))" 
-    using finite_range_image by blast
-  moreover 
-  have "\<And>x y. tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y" 
-    using tag1_inj by simp
-  then have "inj_on (image (tag1 L\<^isub>1 L\<^isub>2)) (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" 
-    using inj_image_lang by blast
-  ultimately 
-  show "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" by (rule finite_imageD)
-qed
-
-
-section {* finite \<Rightarrow> regular *}
-
-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}"
-
-definition
-  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 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;; \<lparr>r\<rparr>) | Y r . (Y, r) \<in> rhs CS X}"
-
-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 [simp]:
-  shows "finite (Y \<Turnstile>\<Rightarrow> X)"
-unfolding transitions_def
-by auto
-
-
-lemma defined_by_str:
-  assumes "s \<in> X" 
-  and "X \<in> UNIV // (\<approx>Lang)"
-  shows "X = (\<approx>Lang) `` {s}"
-using assms
-unfolding quotient_def Image_def
-unfolding str_eq_rel_def str_eq_def
-by auto
-
-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"
-proof -
-  def Y \<equiv> "(\<approx>Lang) `` {s}"
-  have "Y \<in> UNIV // (\<approx>Lang)" 
-    unfolding Y_def quotient_def by auto
-  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 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 *) 
-  ultimately show thesis by (blast intro: that)
-qed
-
-lemma test:
-  assumes "[] \<in> X"
-  shows "[] \<in> \<lparr>Y \<turnstile>\<rightarrow> X\<rparr>"
-using assms
-by (simp add: transitions_rexp_def)
-
-lemma rhs_sem:
-  assumes "X \<in> (UNIV // (\<approx>Lang))"
-  shows "X \<subseteq> rhs_sem (UNIV // (\<approx>Lang)) X"
-apply(case_tac "X = {[]}")
-apply(simp)
-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)
-apply(rule_tac x = "X" in exI)
-apply(simp)
-apply(rule_tac x = "X" in exI)
-apply(simp add: assms)
-apply(simp add: transitions_rexp_def)
-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