theory MyhillNerode

  imports "Main" "List_Prefix"

begin

text {* sequential composition of languages *}

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 seq_union_distrib:

  "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)"

by (auto simp:Seq_def)

lemma seq_assoc:

  "(A ;; B) ;; C = A ;; (B ;; C)"

by (metis append_assoc)

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

  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

qed

datatype rexp =

  NULL

| EMPTY

| CHAR char

| SEQ rexp rexp

| ALT rexp rexp

| STAR rexp

consts L:: "'a \<Rightarrow> string set"

overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> string set"

begin

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

end

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_alt_simp [simp]:

  "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)"

apply (rule set_ext, simp add:folds_def)

apply (rule someI2_ex, erule finite_imp_fold_graph)

by (erule fold_graph.induct, auto)

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 

  show "Lang \<subseteq> \<Union> {X. final X Lang}"

  proof

    fix x

    assume "x \<in> Lang"   

    thus "x \<in> \<Union> {X. final X Lang}"

      apply (simp, rule_tac x = "(\<approx>Lang) `` {x}" in exI)      

      apply (auto simp:final_def quotient_def Image_def str_eq_rel_def str_eq_def)

      by (drule_tac x = "[]" in spec, simp)

  qed

next

  show "\<Union>{X. final X Lang} \<subseteq> Lang"

    by (auto simp:final_def)

qed

section {* finite \<Rightarrow> regular *}

datatype rhs_item = 

   Lam "rexp"                           (* Lambda *)

 | Trn "string set" "rexp"              (* Transition *)

fun the_Trn:: "rhs_item \<Rightarrow> (string set \<times> rexp)"

where "the_Trn (Trn Y r) = (Y, r)"

fun the_r :: "rhs_item \<Rightarrow> rexp"

where "the_r (Lam r) = r"

overloading L_rhs_e \<equiv> "L:: rhs_item \<Rightarrow> string set"

begin

fun L_rhs_e:: "rhs_item \<Rightarrow> string set"

where

  "L_rhs_e (Lam r) = L r" |

  "L_rhs_e (Trn X r) = X ;; L r"

end

overloading L_rhs \<equiv> "L:: rhs_item set \<Rightarrow> string set"

begin

fun L_rhs:: "rhs_item set \<Rightarrow> string set"

where

  "L_rhs rhs = \<Union> (L ` rhs)"

end

definition

  "init_rhs CS X \<equiv>  if ([] \<in> X)

                    then {Lam EMPTY} \<union> {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}

                    else {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}"

definition

  "eqs CS \<equiv> {(X, init_rhs CS X)|X.  X \<in> CS}"

(************ arden's lemma variation ********************)

definition

  "items_of rhs X \<equiv> {Trn X r | r. (Trn X r) \<in> rhs}"

definition

  "lam_of rhs \<equiv> {Lam r | r. Lam r \<in> rhs}"

definition 

  "rexp_of rhs X \<equiv> folds ALT NULL ((snd o the_Trn) ` items_of rhs X)"

definition

  "rexp_of_lam rhs \<equiv> folds ALT NULL (the_r ` lam_of rhs)"

fun attach_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"

where

  "attach_rexp r' (Lam r)   = Lam (SEQ r r')"

| "attach_rexp r' (Trn X r) = Trn X (SEQ r r')"

definition

  "append_rhs_rexp rhs r \<equiv> (attach_rexp r) ` rhs"

definition 

  "arden_variate X rhs \<equiv> append_rhs_rexp (rhs - items_of rhs X) (STAR (rexp_of rhs X))"

(*********** substitution of ES *************)

text {* rhs_subst rhs X xrhs: substitude all occurence of X in rhs with xrhs *}

definition 

  "rhs_subst rhs X xrhs \<equiv> (rhs - (items_of rhs X)) \<union> (append_rhs_rexp xrhs (rexp_of rhs X))"

definition

  "eqs_subst ES X xrhs \<equiv> {(Y, rhs_subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"

text {*

  Inv: Invairance of the equation-system, during the decrease of the equation-system, Inv holds.

*}

definition 

  "distinct_equas ES \<equiv> \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"

definition 

  "valid_eqns ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> (X = L rhs)"

definition 

  "rhs_nonempty rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"

definition 

  "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> rhs_nonempty rhs"

definition 

  "non_empty ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> X \<noteq> {}"

definition

  "finite_rhs ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs"

definition 

  "classes_of rhs \<equiv> {X. \<exists> r. Trn X r \<in> rhs}"

definition

  "lefts_of ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"

definition 

  "self_contained ES \<equiv> \<forall> (X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lefts_of ES"

definition 

  "Inv ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> 

            non_empty ES \<and> finite_rhs ES \<and> self_contained ES"

lemma wf_iter [rule_format]: 

  fixes f

  assumes step: "\<And> e. \<lbrakk>P e; \<not> Q e\<rbrakk> \<Longrightarrow> (\<exists> e'. P e' \<and>  (f(e'), f(e)) \<in> less_than)"

  shows pe:     "P e \<longrightarrow> (\<exists> e'. P e' \<and>  Q e')"

proof(induct e rule: wf_induct 

           [OF wf_inv_image[OF wf_less_than, where f = "f"]], clarify)

  fix x 

  assume h [rule_format]: 

    "\<forall>y. (y, x) \<in> inv_image less_than f \<longrightarrow> P y \<longrightarrow> (\<exists>e'. P e' \<and> Q e')"

    and px: "P x"

  show "\<exists>e'. P e' \<and> Q e'"

  proof(cases "Q x")

    assume "Q x" with px show ?thesis by blast

  next

    assume nq: "\<not> Q x"

    from step [OF px nq]

    obtain e' where pe': "P e'" and ltf: "(f e', f x) \<in> less_than" by auto

    show ?thesis

    proof(rule h)

      from ltf show "(e', x) \<in> inv_image less_than f" 

	by (simp add:inv_image_def)

    next

      from pe' show "P e'" .

    qed

  qed

qed

text {* ************* basic properties of definitions above ************************ *}

lemma L_rhs_union_distrib:

  " L (A::rhs_item set) \<union> L B = L (A \<union> B)"

by simp

lemma finite_snd_Trn:

  assumes finite:"finite rhs"

  shows "finite {r\<^isub>2. Trn Y r\<^isub>2 \<in> rhs}" (is "finite ?B")

proof-

  def rhs' \<equiv> "{e \<in> rhs. \<exists> r. e = Trn Y r}"

  have "?B = (snd o the_Trn) ` rhs'" using rhs'_def by (auto simp:image_def)

  moreover have "finite rhs'" using finite rhs'_def by auto

  ultimately show ?thesis by simp

qed

lemma rexp_of_empty:

  assumes finite:"finite rhs"

  and nonempty:"rhs_nonempty rhs"

  shows "[] \<notin> L (rexp_of rhs X)"

using finite nonempty rhs_nonempty_def

by (drule_tac finite_snd_Trn[where Y = X], auto simp:rexp_of_def items_of_def)

lemma [intro!]:

  "P (Trn X r) \<Longrightarrow> (\<exists>a. (\<exists>r. a = Trn X r \<and> P a))" by auto

lemma finite_items_of:

  "finite rhs \<Longrightarrow> finite (items_of rhs X)"

by (auto simp:items_of_def intro:finite_subset)

lemma lang_of_rexp_of:

  assumes finite:"finite rhs"

  shows "L (items_of rhs X) = X ;; (L (rexp_of rhs X))"

proof -

  have "finite ((snd \<circ> the_Trn) ` items_of rhs X)" using finite_items_of[OF finite] by auto

  thus ?thesis

    apply (auto simp:rexp_of_def Seq_def items_of_def)

    apply (rule_tac x = s1 in exI, rule_tac x = s2 in exI, auto)

    by (rule_tac x= "Trn X r" in exI, auto simp:Seq_def)

qed

lemma rexp_of_lam_eq_lam_set:

  assumes finite: "finite rhs"

  shows "L (rexp_of_lam rhs) = L (lam_of rhs)"

proof -

  have "finite (the_r ` {Lam r |r. Lam r \<in> rhs})" using finite

    by (rule_tac finite_imageI, auto intro:finite_subset)

  thus ?thesis by (auto simp:rexp_of_lam_def lam_of_def)

qed

lemma [simp]:

  " L (attach_rexp r xb) = L xb ;; L r"

apply (cases xb, auto simp:Seq_def)

by (rule_tac x = "s1 @ s1a" in exI, rule_tac x = s2a in exI,auto simp:Seq_def)

lemma lang_of_append_rhs:

  "L (append_rhs_rexp rhs r) = L rhs ;; L r"

apply (auto simp:append_rhs_rexp_def image_def)

apply (auto simp:Seq_def)

apply (rule_tac x = "L xb ;; L r" in exI, auto simp add:Seq_def)

by (rule_tac x = "attach_rexp r xb" in exI, auto simp:Seq_def)

lemma classes_of_union_distrib:

  "classes_of A \<union> classes_of B = classes_of (A \<union> B)"

by (auto simp add:classes_of_def)

lemma lefts_of_union_distrib:

  "lefts_of A \<union> lefts_of B = lefts_of (A \<union> B)"

by (auto simp:lefts_of_def)

text {* ******BEGIN: proving the initial equation-system satisfies Inv ****** *}

lemma defined_by_str:

  "\<lbrakk>s \<in> X; X \<in> UNIV // (\<approx>Lang)\<rbrakk> \<Longrightarrow> X = (\<approx>Lang) `` {s}"

by (auto simp:quotient_def Image_def str_eq_rel_def str_eq_def)

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

  ultimately show thesis by (blast intro: that)

qed

lemma l_eq_r_in_eqs:

  assumes X_in_eqs: "(X, xrhs) \<in> (eqs (UNIV // (\<approx>Lang)))"

  shows "X = L xrhs"

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 = []"

      thus ?thesis using X_in_eqs "(1)"

        by (auto simp:eqs_def init_rhs_def)

    next

      assume not_empty: "x \<noteq> []"

      then obtain clist c where decom: "x = clist @ [c]"

        by (case_tac x rule:rev_cases, auto)

      have "X \<in> UNIV // (\<approx>Lang)" using X_in_eqs by (auto simp:eqs_def)

      then obtain Y 

        where "Y \<in> UNIV // (\<approx>Lang)" 

        and "Y ;; {[c]} \<subseteq> X"

        and "clist \<in> Y"

        using decom "(1)" every_eqclass_has_transition by blast

      hence "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y ;; {[c]} \<subseteq> X}"

        using "(1)" decom

        by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)

      thus ?thesis using X_in_eqs "(1)"

        by (simp add:eqs_def init_rhs_def)

    qed

  qed

next

  show "L xrhs \<subseteq> X" using X_in_eqs

    by (auto simp:eqs_def init_rhs_def) 

qed

lemma finite_init_rhs: 

  assumes finite: "finite CS"

  shows "finite (init_rhs CS X)"

proof-

  have "finite {Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" (is "finite ?A")

  proof -

    def S \<equiv> "{(Y, c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" 

    def h \<equiv> "\<lambda> (Y, c). Trn Y (CHAR c)"

    have "finite (CS \<times> (UNIV::char set))" using finite by auto

    hence "finite S" using S_def 

      by (rule_tac B = "CS \<times> UNIV" in finite_subset, auto)

    moreover have "?A = h ` S" by (auto simp: S_def h_def image_def)

    ultimately show ?thesis 

      by auto

  qed

  thus ?thesis by (simp add:init_rhs_def)

qed

lemma init_ES_satisfy_Inv:

  assumes finite_CS: "finite (UNIV // (\<approx>Lang))"

  shows "Inv (eqs (UNIV // (\<approx>Lang)))"

proof -

  have "finite (eqs (UNIV // (\<approx>Lang)))" using finite_CS

    by (simp add:eqs_def)

  moreover have "distinct_equas (eqs (UNIV // (\<approx>Lang)))"     

    by (simp add:distinct_equas_def eqs_def)

  moreover have "ardenable (eqs (UNIV // (\<approx>Lang)))"

    by (auto simp add:ardenable_def eqs_def init_rhs_def rhs_nonempty_def del:L_rhs.simps)

  moreover have "valid_eqns (eqs (UNIV // (\<approx>Lang)))"

    using l_eq_r_in_eqs by (simp add:valid_eqns_def)

  moreover have "non_empty (eqs (UNIV // (\<approx>Lang)))"

    by (auto simp:non_empty_def eqs_def quotient_def Image_def str_eq_rel_def str_eq_def)

  moreover have "finite_rhs (eqs (UNIV // (\<approx>Lang)))"

    using finite_init_rhs[OF finite_CS] 

    by (auto simp:finite_rhs_def eqs_def)

  moreover have "self_contained (eqs (UNIV // (\<approx>Lang)))"

    by (auto simp:self_contained_def eqs_def init_rhs_def classes_of_def lefts_of_def)

  ultimately show ?thesis by (simp add:Inv_def)

qed

text {* ****** BEGIN: proving every equation-system's iteration step satisfies Inv ***** *}

lemma arden_variate_keeps_eq:

  assumes l_eq_r: "X = L rhs"

  and not_empty: "[] \<notin> L (rexp_of rhs X)"

  and finite: "finite rhs"

  shows "X = L (arden_variate X rhs)"

proof -

  def A \<equiv> "L (rexp_of rhs X)"

  def b \<equiv> "rhs - items_of rhs X"

  def B \<equiv> "L b" 

  have "X = B ;; A\<star>"

  proof-

    have "rhs = items_of rhs X \<union> b" by (auto simp:b_def items_of_def)

    hence "L rhs = L(items_of rhs X \<union> b)" by simp

    hence "L rhs = L(items_of rhs X) \<union> B" by (simp only:L_rhs_union_distrib B_def)

    with lang_of_rexp_of

    have "L rhs = X ;; A \<union> B " using finite by (simp only:B_def b_def A_def)

    thus ?thesis

      using l_eq_r not_empty

      apply (drule_tac B = B and X = X in ardens_revised)

      by (auto simp:A_def simp del:L_rhs.simps)

  qed

  moreover have "L (arden_variate X rhs) = (B ;; A\<star>)" (is "?L = ?R")

    by (simp only:arden_variate_def L_rhs_union_distrib lang_of_append_rhs 

                  B_def A_def b_def L_rexp.simps seq_union_distrib)

   ultimately show ?thesis by simp

qed 

lemma append_keeps_finite:

  "finite rhs \<Longrightarrow> finite (append_rhs_rexp rhs r)"

by (auto simp:append_rhs_rexp_def)

lemma arden_variate_keeps_finite:

  "finite rhs \<Longrightarrow> finite (arden_variate X rhs)"

by (auto simp:arden_variate_def append_keeps_finite)

lemma append_keeps_nonempty:

  "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (append_rhs_rexp rhs r)"

apply (auto simp:rhs_nonempty_def append_rhs_rexp_def)

by (case_tac x, auto simp:Seq_def)

lemma nonempty_set_sub:

  "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (rhs - A)"

by (auto simp:rhs_nonempty_def)

lemma nonempty_set_union:

  "\<lbrakk>rhs_nonempty rhs; rhs_nonempty rhs'\<rbrakk> \<Longrightarrow> rhs_nonempty (rhs \<union> rhs')"

by (auto simp:rhs_nonempty_def)

lemma arden_variate_keeps_nonempty:

  "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (arden_variate X rhs)"

by (simp only:arden_variate_def append_keeps_nonempty nonempty_set_sub)

lemma rhs_subst_keeps_nonempty:

  "\<lbrakk>rhs_nonempty rhs; rhs_nonempty xrhs\<rbrakk> \<Longrightarrow> rhs_nonempty (rhs_subst rhs X xrhs)"

by (simp only:rhs_subst_def append_keeps_nonempty  nonempty_set_union nonempty_set_sub)

lemma rhs_subst_keeps_eq:

  assumes substor: "X = L xrhs"

  and finite: "finite rhs"

  shows "L (rhs_subst rhs X xrhs) = L rhs" (is "?Left = ?Right")

proof-

  def A \<equiv> "L (rhs - items_of rhs X)"

  have "?Left = A \<union> L (append_rhs_rexp xrhs (rexp_of rhs X))"

    by (simp only:rhs_subst_def L_rhs_union_distrib A_def)

  moreover have "?Right = A \<union> L (items_of rhs X)"

  proof-

    have "rhs = (rhs - items_of rhs X) \<union> (items_of rhs X)" by (auto simp:items_of_def)

    thus ?thesis by (simp only:L_rhs_union_distrib A_def)

  qed

  moreover have "L (append_rhs_rexp xrhs (rexp_of rhs X)) = L (items_of rhs X)" 

    using finite substor  by (simp only:lang_of_append_rhs lang_of_rexp_of)

  ultimately show ?thesis by simp

qed

lemma rhs_subst_keeps_finite_rhs: