theory Myhill_1

  imports Main List_Prefix Prefix_subtract Prelude

begin

(*

text {*

     \begin{figure}

    \centering

    \scalebox{0.95}{

    \begin{tikzpicture}[->,>=latex,shorten >=1pt,auto,node distance=1.2cm, semithick]

        \node[state,initial] (n1)                   {$1$};

        \node[state,accepting] (n2) [right = 10em of n1]   {$2$};

        \path (n1) edge [bend left] node {$0$} (n2)

            (n1) edge [loop above] node{$1$} (n1)

            (n2) edge [loop above] node{$0$} (n2)

            (n2) edge [bend left]  node {$1$} (n1)

            ;

    \end{tikzpicture}}

    \caption{An example automaton (or partition)}\label{fig:example_automata}

    \end{figure}

*}

*)

section {* Preliminary definitions *}

types lang = "string set"

text {* 

  Sequential composition of two languages @{text "L1"} and @{text "L2"} 

*}

definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100)

where 

  "A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"

lemma seq_union_distrib_right:

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

unfolding Seq_def by auto

lemma seq_union_distrib_left:

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

unfolding Seq_def by  auto

lemma seq_intro:

  "\<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x @ y \<in> A ;; B "

by (auto simp:Seq_def)

lemma seq_assoc:

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

unfolding Seq_def

apply(auto)

apply(blast)

by (metis append_assoc)

lemma seq_empty [simp]:

  shows "A ;; {[]} = A"

  and   "{[]} ;; A = A"

by (simp_all add: Seq_def)

lemma star_decom: 

lemma lang_star_cases:

  shows "L\<star> =  {[]} \<union> L ;; L\<star>"

proof

  { fix x

    have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ;; L\<star>"

      unfolding Seq_def

  }

  then show "L\<star> \<subseteq> {[]} \<union> L ;; L\<star>" by auto

next

    unfolding Seq_def by auto

qed

lemma

  shows seq_Union_left:  "B ;; (\<Union>n. A \<up> n) = (\<Union>n. B ;; (A \<up> n))"

  and   seq_Union_right: "(\<Union>n. A \<up> n) ;; B = (\<Union>n. (A \<up> n) ;; B)"

unfolding Seq_def by auto

lemma seq_pow_comm:

  shows "A ;; (A \<up> n) = (A \<up> n) ;; A"

by (induct n) (simp_all add: seq_assoc[symmetric])

lemma seq_star_comm:

  shows "A ;; A\<star> = A\<star> ;; A"

unfolding seq_Union_left

unfolding seq_pow_comm

unfolding seq_Union_right 

by simp

text {* Two lemmas about the length of strings in @{text "A \<up> n"} *}

lemma pow_length:

  assumes a: "[] \<notin> A"

  and     b: "s \<in> A \<up> Suc n"

  shows "n < length s"

using b

proof (induct n arbitrary: s)

  case 0

  have "s \<in> A \<up> Suc 0" by fact

  with a have "s \<noteq> []" by auto

  then show "0 < length s" by auto

next

  case (Suc n)

  have ih: "\<And>s. s \<in> A \<up> Suc n \<Longrightarrow> n < length s" by fact

  have "s \<in> A \<up> Suc (Suc n)" by fact

  then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A \<up> Suc n"

    by (auto simp add: Seq_def)

  from ih ** have "n < length s2" by simp

  moreover have "0 < length s1" using * a by auto

  ultimately show "Suc n < length s" unfolding eq 

    by (simp only: length_append)

qed

lemma seq_pow_length:

  assumes a: "[] \<notin> A"

  and     b: "s \<in> B ;; (A \<up> Suc n)"

  shows "n < length s"

proof -

  from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A \<up> Suc n"

    unfolding Seq_def by auto

  from * have " n < length s2" by (rule pow_length[OF a])

  then show "n < length s" using eq by simp

qed

section {* A slightly modified version of Arden's lemma *}

text {* 

  Arden's lemma expressed at the level of languages, rather 

  than the level of regular expression. 

*}

lemma ardens_helper:

  assumes eq: "X = X ;; A \<union> B"

  shows "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"

proof (induct n)

  case 0 

  show "X = X ;; (A \<up> Suc 0) \<union> (\<Union>(m::nat)\<in>{0..0}. B ;; (A \<up> m))"

    using eq by simp

next

  case (Suc n)

  have ih: "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" by fact

  also have "\<dots> = (X ;; A \<union> B) ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" using eq by simp

  also have "\<dots> = X ;; (A \<up> Suc (Suc n)) \<union> (B ;; (A \<up> Suc n)) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"

    by (simp add: seq_union_distrib_right seq_assoc)

  also have "\<dots> = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))"

    by (auto simp add: le_Suc_eq)

  finally show "X = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))" .

qed

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" 

    unfolding seq_star_comm[symmetric]

    by (rule lang_star_cases)

  also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"

    unfolding seq_union_distrib_left by simp

  also have "\<dots> = B \<union> (B ;; A\<star>) ;; A" 

    by (simp only: seq_assoc)

  finally show "X = X ;; A \<union> B" 

    using eq by blast 

next

  assume eq: "X = X ;; A \<union> B"

  { fix n::nat

    have "B ;; (A \<up> n) \<subseteq> X" using ardens_helper[OF eq, of "n"] by auto }

  moreover

  { fix s::string

    obtain k where "k = length s" by auto

    then have not_in: "s \<notin> X ;; (A \<up> Suc k)" 

      using seq_pow_length[OF nemp] by blast

    assume "s \<in> X"

    then have "s \<in> X ;; (A \<up> Suc k) \<union> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))"

      using ardens_helper[OF eq, of "k"] by auto

    then have "s \<in> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))" using not_in by auto

    moreover

    have "(\<Union>m\<in>{0..k}. B ;; (A \<up> m)) \<subseteq> (\<Union>n. B ;; (A \<up> n))" by auto

    ultimately 

      by auto }

  then have "X \<subseteq> B ;; A\<star>" by auto

  ultimately 

  show "X = B ;; A\<star>" by simp

qed

text {* The syntax of regular expressions is defined by the datatype @{text "rexp"}. *}

datatype rexp =

  NULL

| EMPTY

| CHAR char

| SEQ rexp rexp

| ALT rexp rexp

| STAR rexp

text {* 

  The following @{text "L"} is an overloaded operator, where @{text "L(x)"} evaluates to 

  the language represented by the syntactic object @{text "x"}.

*}

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

text {* 

  The @{text "L(rexp)"} for regular expression @{text "rexp"} is defined by the 

  following overloading function @{text "L_rexp"}.

*}

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

text {*

  To obtain equational system out of finite set of equivalent classes, a fold operation

  on finite set @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "fold"}

  more robust than the @{text "fold"} in Isabelle library. The expression @{text "folds f"}

  makes sense when @{text "f"} is not @{text "associative"} and @{text "commutitive"},

  while @{text "fold f"} does not.  

*}

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"

text {* 

  The following lemma assures that the arbitrary choice made by the @{text "SOME"} in @{text "folds"}

  does not affect the @{text "L"}-value of the resultant regular expression. 

  *}

lemma folds_alt_simp [simp]:

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

apply (rule set_eq_intro, simp add:folds_def)

apply (rule someI2_ex, erule finite_imp_fold_graph)

by (erule fold_graph.induct, auto)

(* Just a technical lemma. *)

lemma [simp]:

  shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"

by simp

text {*

  @{text "\<approx>L"} is an equivalent class defined by language @{text "Lang"}.

*}

definition

  str_eq_rel ("\<approx>_" [100] 100)

where

  "\<approx>Lang \<equiv> {(x, y).  (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)}"

text {* 

  Among equivlant clases of @{text "\<approx>Lang"}, the set @{text "finals(Lang)"} singles out 

  those which contains strings from @{text "Lang"}.

*}

definition 

   "finals Lang \<equiv> {\<approx>Lang `` {x} | x . x \<in> Lang}"

text {* 

  The following lemma show the relationshipt between @{text "finals(Lang)"} and @{text "Lang"}.

*}

lemma lang_is_union_of_finals: 

  "Lang = \<Union> finals(Lang)"

proof 

  show "Lang \<subseteq> \<Union> (finals Lang)"

  proof

    fix x

    assume "x \<in> Lang"   

    thus "x \<in> \<Union> (finals Lang)"

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

      by (auto simp:Image_def str_eq_rel_def)    

  qed

next

  show "\<Union> (finals Lang) \<subseteq> Lang"

    apply (clarsimp simp:finals_def str_eq_rel_def)

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

qed

section {* Direction @{text "finite partition \<Rightarrow> regular language"}*}

text {* 

  The relationship between equivalent classes can be described by an

  equational system.

  For example, in equational system \eqref{example_eqns},  $X_0, X_1$ are equivalent 

  classes. The first equation says every string in $X_0$ is obtained either by

  appending one $b$ to a string in $X_0$ or by appending one $a$ to a string in

  $X_1$ or just be an empty string (represented by the regular expression $\lambda$). Similary,

  the second equation tells how the strings inside $X_1$ are composed.

  \begin{equation}\label{example_eqns}

    \begin{aligned}

      X_0 & = X_0 b + X_1 a + \lambda \\

      X_1 & = X_0 a + X_1 b

    \end{aligned}

  \end{equation}

  The summands on the right hand side is represented by the following data type

  @{text "rhs_item"}, mnemonic for 'right hand side item'.

  Generally, there are two kinds of right hand side items, one kind corresponds to

  pure regular expressions, like the $\lambda$ in \eqref{example_eqns}, the other kind corresponds to

  transitions from one one equivalent class to another, like the $X_0 b, X_1 a$ etc.

  *}

datatype rhs_item = 

   Lam "rexp"                           (* Lambda *)

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

text {*

  In this formalization, pure regular expressions like $\lambda$ is 

  repsented by @{text "Lam(EMPTY)"}, while transitions like $X_0 a$ is represented by $Trn~X_0~(CHAR~a)$.

  *}

text {*

  The functions @{text "the_r"} and @{text "the_Trn"} are used to extract

  subcomponents from right hand side items.

  *}

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

where "the_r (Lam r) = r"

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

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

text {*

  Every right hand side item @{text "itm"} defines a string set given 

  @{text "L(itm)"}, defined as:

*}

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

text {*

  The right hand side of every equation is represented by a set of

  items. The string set defined by such a set @{text "itms"} is given

  by @{text "L(itms)"}, defined as:

*}

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

text {* 

  Given a set of equivalent classses @{text "CS"} and one equivalent class @{text "X"} among

  @{text "CS"}, the term @{text "init_rhs CS X"} is used to extract the right hand side of

  the equation describing the formation of @{text "X"}. The definition of @{text "init_rhs"}

  is:

  *}

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

text {*

  In the definition of @{text "init_rhs"}, the term 

  @{text "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}"} appearing on both branches

  describes the formation of strings in @{text "X"} out of transitions, while 

  the term @{text "{Lam(EMPTY)}"} describes the empty string which is intrinsically contained in

  @{text "X"} rather than by transition. This @{text "{Lam(EMPTY)}"} corresponds to 

  the $\lambda$ in \eqref{example_eqns}.

  With the help of @{text "init_rhs"}, the equitional system descrbing the formation of every

  equivalent class inside @{text "CS"} is given by the following @{text "eqs(CS)"}.

  *}

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

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

text {* 

  The following @{text "items_of rhs X"} returns all @{text "X"}-items in @{text "rhs"}.

  *}

definition

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

text {* 

  The following @{text "rexp_of rhs X"} combines all regular expressions in @{text "X"}-items

  using @{text "ALT"} to form a single regular expression. 

  It will be used later to implement @{text "arden_variate"} and @{text "rhs_subst"}.

  *}

definition 

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

text {* 

  The following @{text "lam_of rhs"} returns all pure regular expression items in @{text "rhs"}.

  *}

definition

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

text {*

  The following @{text "rexp_of_lam rhs"} combines pure regular expression items in @{text "rhs"}

  using @{text "ALT"} to form a single regular expression. 

  When all variables inside @{text "rhs"} are eliminated, @{text "rexp_of_lam rhs"}

  is used to compute compute the regular expression corresponds to @{text "rhs"}.

  *}

definition

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

text {*

  The following @{text "attach_rexp rexp' itm"} attach