theory My

imports Main

begin

definition

  lang_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>"

datatype rexp =

  NULL

| EMPTY

| CHAR char

| SEQ rexp rexp

| ALT rexp rexp

| STAR rexp

fun

  L_rexp :: "rexp \<Rightarrow> string set"

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>"

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> L_rexp (folds ALT NULL rs) = (\<exists>r \<in> rs. x \<in> L_rexp 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_rexp (folds ALT EMPTY rs) = ((\<exists>r \<in> rs. x \<in> L_rexp 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

lemma [simp]:

  "(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 = L_rexp r"

sorry

lemma final_rexp:

  "\<lbrakk>finite (UNIV // (\<approx>Lang)); final X Lang\<rbrakk> \<Longrightarrow> \<exists>r. X = L_rexp r"

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 =  L_rexp (folds ALT NULL rs)"

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(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 =  L_rexp r"

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; L_rexp r) | 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 lang_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

qed

lemma test:

  assumes "[] \<in> X"

  shows "[] \<in> L_rexp (Y \<turnstile>\<rightarrow> X)"

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 lang_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