theory Myhill_1

imports Main Folds

begin

section {* Preliminary definitions *}

types lang = "string set"

text {*  Sequential composition of two languages *}

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

text {* Some properties of operator @{text ";;"}. *}

lemma seq_add_left:

  assumes a: "A = B"

  shows "C ;; A = C ;; B"

using a by simp

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:

  assumes a: "x \<in> A" "y \<in> B"

  shows "x @ y \<in> A ;; B "

using a 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)

text {* Power and Star of a language *}

fun 

  pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100)

where

  "A \<up> 0 = {[]}"

| "A \<up> (Suc n) =  A ;; (A \<up> n)" 

definition

  Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102)

where

  "A\<star> \<equiv> (\<Union>n. A \<up> n)"

lemma star_start[intro]:

  shows "[] \<in> A\<star>"

proof -

  have "[] \<in> A \<up> 0" by auto

  then show "[] \<in> A\<star>" unfolding Star_def by blast

qed

lemma star_step [intro]:

  assumes a: "s1 \<in> A" 

  and     b: "s2 \<in> A\<star>"

  shows "s1 @ s2 \<in> A\<star>"

proof -

  from b obtain n where "s2 \<in> A \<up> n" unfolding Star_def by auto

  then have "s1 @ s2 \<in> A \<up> (Suc n)" using a by (auto simp add: Seq_def)

  then show "s1 @ s2 \<in> A\<star>" unfolding Star_def by blast

qed

lemma star_induct[consumes 1, case_names start step]:

  assumes a: "x \<in> A\<star>" 

  and     b: "P []"

  and     c: "\<And>s1 s2. \<lbrakk>s1 \<in> A; s2 \<in> A\<star>; P s2\<rbrakk> \<Longrightarrow> P (s1 @ s2)"

  shows "P x"

proof -

  from a obtain n where "x \<in> A \<up> n" unfolding Star_def by auto

  then show "P x"

    by (induct n arbitrary: x)

       (auto intro!: b c simp add: Seq_def Star_def)

qed

lemma star_intro1:

  assumes a: "x \<in> A\<star>"

  and     b: "y \<in> A\<star>"

  shows "x @ y \<in> A\<star>"

using a b

by (induct rule: star_induct) (auto)

lemma star_intro2: 

  assumes a: "y \<in> A"

  shows "y \<in> A\<star>"

proof -

  from a have "y @ [] \<in> A\<star>" by blast

  then show "y \<in> A\<star>" by simp

qed

lemma star_intro3:

  assumes a: "x \<in> A\<star>"

  and     b: "y \<in> A"

  shows "x @ y \<in> A\<star>"

using a b by (blast intro: star_intro1 star_intro2)

lemma star_cases:

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

proof

  { fix x

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

      unfolding Seq_def

    by (induct rule: star_induct) (auto)

  }

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

next

  show "{[]} \<union> A ;; A\<star> \<subseteq> A\<star>"

    unfolding Seq_def by auto

qed

lemma star_decom: 

  assumes a: "x \<in> A\<star>" "x \<noteq> []"

  shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>"

using a

by (induct rule: star_induct) (blast)+

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 Star_def seq_Union_left

unfolding seq_pow_comm 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 modified version of Arden's lemma *}

text {*  A helper lemma for Arden *}

lemma arden_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 arden:

  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 star_cases)

  then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"

    by (rule seq_add_left)

  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 arden_helper[OF eq, of "n"] by auto }

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

    unfolding Seq_def Star_def UNION_def 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 arden_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 

    have "s \<in> B ;; A\<star>" 

      unfolding seq_Union_left Star_def by auto }

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

  ultimately 

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

qed

section {* Regular Expressions *}

datatype rexp =

  NULL

| EMPTY

| CHAR char

| SEQ rexp rexp

| ALT rexp rexp

| STAR rexp

text {* 

  The function @{text L} is overloaded, with the idea that @{text "L x"} 

  evaluates to the language represented by the object @{text x}.

*}

consts L:: "'a \<Rightarrow> lang"

overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> lang"

begin

fun

  L_rexp :: "rexp \<Rightarrow> lang"

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 {* ALT-combination of a set or regulare expressions *}

abbreviation

  Setalt  ("\<Uplus>_" [1000] 999) 

where

  "\<Uplus>A == folds ALT NULL A"

text {* 

  For finite sets, @{term Setalt} is preserved under @{term L}.

*}

lemma folds_alt_simp [simp]:

  fixes rs::"rexp set"

  assumes a: "finite rs"

  shows "L (\<Uplus>rs) = \<Union> (L ` rs)"

apply(rule set_eqI)

apply(simp add: folds_def)

apply(rule someI2_ex)

apply(rule_tac finite_imp_fold_graph[OF a])

apply(erule fold_graph.induct)

apply(auto)

done

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

text {* Just a technical lemma for collections and pairs *}

lemma Pair_Collect[simp]:

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

by simp

text {* Myhill-Nerode relation *}

definition

  str_eq_rel :: "lang \<Rightarrow> (string \<times> string) set" ("\<approx>_" [100] 100)

where

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

text {* 

  Among the equivalence clases of @{text "\<approx>A"}, the set @{text "finals A"} 

  singles out those which contains the strings from @{text A}.

*}

definition 

  finals :: "lang \<Rightarrow> lang set"

where

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

lemma lang_is_union_of_finals: 

  shows "A = \<Union> finals A"

unfolding finals_def

unfolding Image_def

unfolding str_eq_rel_def

apply(auto)

apply(drule_tac x = "[]" in spec)

apply(auto)

done

lemma finals_in_partitions:

  shows "finals A \<subseteq> (UNIV // \<approx>A)"

unfolding finals_def

unfolding quotient_def

by auto

section {* Equational systems *}

datatype rhs_item = 

   Lam "rexp"            (* Lambda-marker *)

 | Trn "lang" "rexp"     (* Transition *)

overloading L_rhs_item \<equiv> "L:: rhs_item \<Rightarrow> lang"

begin

  fun L_rhs_item:: "rhs_item \<Rightarrow> lang"

  where

    "L_rhs_item (Lam r) = L r" 

  | "L_rhs_item (Trn X r) = X ;; L r"

end

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

begin

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

   where 

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

end

definition

  "trns_of rhs X \<equiv> {Trn X r | r. Trn X r \<in> rhs}"

text {* Transitions between equivalence classes *}

definition 

  transition :: "lang \<Rightarrow> rexp \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)

where

  "Y \<Turnstile>r\<Rightarrow> X \<equiv> Y ;; (L r) \<subseteq> X"

text {* Initial equational system *}

definition

  "init_rhs CS X \<equiv>  

      if ([] \<in> X) then 

          {Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}

      else 

          {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}"

definition 

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

section {* Arden Operation on equations *}

text {*

  The function @{text "attach_rexp r item"} SEQ-composes @{text r} to the

  right of every rhs-item.

*}

fun 

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

where

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

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

definition

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

definition 

  "arden_op X rhs \<equiv> 

     append_rhs_rexp (rhs - trns_of rhs X) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))"

section {* Substitution Operation on equations *}

text {* 

  Suppose and equation @{text "X = xrhs"}, @{text "subst_op"} substitutes 

  all occurences of @{text "X"} in @{text "rhs"} by @{text "xrhs"}.

*}

definition 

  "subst_op rhs X xrhs \<equiv> 

        (rhs - (trns_of rhs X)) \<union> (append_rhs_rexp xrhs (\<Uplus> {r. Trn X r \<in> rhs}))"

text {*

  @{text "eqs_subst ES X xrhs"} substitutes @{text xrhs} into every 

  equation of the equational system @{text ES}.

*}

definition

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

section {* Well-founded iteration *}

text {*

  The computation of regular expressions for equivalence classes is accomplished

  using a iteration principle given by the following lemma.

*}

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 {*

  The @{text "P"} in lemma @{text "wf_iter"} is an invariant kept throughout the iteration procedure.

  The particular invariant used to solve our problem is defined by function @{text "Inv(ES)"},

  an invariant over equal system @{text "ES"}.

  Every definition starting next till @{text "Inv"} stipulates a property to be satisfied by @{text "ES"}.

*}

section {* Invariants *}

text {* Every variable is defined at most onece in @{text ES}. *}