theory MyhillNerode

  imports "Main" "List_Prefix"

begin

text {* sequential composition of languages *}

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

lemma lang_seq_empty:

  shows "{[]} ; L = L"

  and   "L ; {[]} = L"

unfolding lang_seq_def by auto

lemma lang_seq_null:

  shows "{} ; L = {}"

  and   "L ; {} = {}"

unfolding lang_seq_def by auto

lemma lang_seq_append:

  assumes a: "s1 \<in> L1"

  and     b: "s2 \<in> L2"

  shows "s1@s2 \<in> L1 ; L2"

unfolding lang_seq_def

using a b by auto 

lemma lang_seq_union:

  shows "(L1 \<union> L2); L3 = (L1; L3) \<union> (L2; L3)"

  and   "L1; (L2 \<union> L3) = (L1; L2) \<union> (L1; L3)"

unfolding lang_seq_def by auto

lemma lang_seq_assoc:

  shows "(L1 ; L2) ; L3 = L1 ; (L2 ; L3)"

unfolding lang_seq_def

apply(auto)

apply(metis)

by (metis append_assoc)

section {* Kleene star for languages defined as least fixed point *}

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

  shows "{}\<star> = {[]}"

by (auto elim: Star.cases)

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 lang_seq_def

    by (induct rule: Star.induct) (auto)

  }

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

next

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

    unfolding lang_seq_def by auto

qed

lemma lang_star_cases':

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

proof

  { fix x

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

      unfolding lang_seq_def

    apply (induct rule: Star.induct)

    apply simp

    apply simp

    apply (erule disjE)

    apply (auto)[1]

    apply (erule exE | erule conjE)+

    apply (rule disjI2)

    apply (rule_tac x = "s1 @ s1a" in exI)

    by auto

  }

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

next

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

    unfolding lang_seq_def

    apply auto

    apply (erule Star.induct)

    apply auto

    apply (drule step[of _ _ "[]"])

    by (auto intro:start)

qed

lemma lang_star_simple:

  shows "L \<subseteq> L\<star>"

by (subst lang_star_cases)

   (auto simp only: lang_seq_def)

lemma lang_star_prop0_aux:

  "s2 \<in> L\<star> \<Longrightarrow> \<forall> s1. s1 \<in> L \<longrightarrow> (\<exists> s3 s4. s3 \<in> L\<star> \<and> s4 \<in> L \<and> s1 @ s2 = s3 @ s4)" 

apply (erule Star.induct)

apply (clarify, rule_tac x = "[]" in exI, rule_tac x = s1 in exI, simp add:start)

apply (clarify, drule_tac x = s1 in spec)

apply (drule mp, simp, clarify)

apply (rule_tac x = "s1a @ s3" in exI, rule_tac x = s4 in exI)

by auto

lemma lang_star_prop0:

  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> \<exists> s3 s4. s3 \<in> L\<star> \<and> s4 \<in> L \<and> s1 @ s2 = s3 @ s4" 

by (auto dest:lang_star_prop0_aux)

lemma lang_star_prop1:

  assumes asm: "L1; L2 \<subseteq> L2" 

  shows "L1\<star>; L2 \<subseteq> L2"

proof -

  { fix s1 s2

    assume minor: "s2 \<in> L2"

    assume major: "s1 \<in> L1\<star>"

    then have "s1@s2 \<in> L2"

    proof(induct rule: Star.induct)

      case start

      show "[]@s2 \<in> L2" using minor by simp

    next

      case (step s1 s1')

      have "s1 \<in> L1" by fact

      moreover

      have "s1'@s2 \<in> L2" by fact

      ultimately have "s1@(s1'@s2) \<in> L1; L2" by (auto simp add: lang_seq_def)

      with asm have "s1@(s1'@s2) \<in> L2" by auto

      then show "(s1@s1')@s2 \<in> L2" by simp

    qed

  } 

  then show "L1\<star>; L2 \<subseteq> L2" by (auto simp add: lang_seq_def)

qed

lemma lang_star_prop2_aux:

  "s2 \<in> L2\<star> \<Longrightarrow> \<forall> s1. s1 \<in> L1 \<and> L1 ; L2 \<subseteq> L1 \<longrightarrow> s1 @ s2 \<in> L1"

apply (erule Star.induct, simp)

apply (clarify, drule_tac x = "s1a @ s1" in spec)

by (auto simp:lang_seq_def)

lemma lang_star_prop2:

  "L1; L2 \<subseteq> L1 \<Longrightarrow> L1 ; L2\<star> \<subseteq> L1"

by (auto dest!:lang_star_prop2_aux simp:lang_seq_def)

lemma lang_star_seq_subseteq: 

  shows "L ; L\<star> \<subseteq> L\<star>"

using lang_star_cases by blast

lemma lang_star_double:

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

proof

  show "L\<star> ; L\<star> \<subseteq> L\<star>" 

    using lang_star_prop1 lang_star_seq_subseteq by blast

next

  have "L\<star> \<subseteq> L\<star> \<union> L\<star>; (L; L\<star>)" by auto

  also have "\<dots> = L\<star>;{[]} \<union> L\<star>; (L; L\<star>)" by (simp add: lang_seq_empty)

  also have "\<dots> = L\<star>; ({[]} \<union> L; L\<star>)" by (simp only: lang_seq_union)

  also have "\<dots> = L\<star>; L\<star>" using lang_star_cases by simp 

  finally show "L\<star> \<subseteq> L\<star> ; L\<star>" by simp

qed

lemma lang_star_seq_subseteq': 

  shows "L\<star>; L \<subseteq> L\<star>"

proof -

  have "L \<subseteq> L\<star>" by (rule lang_star_simple)

  then have "L\<star>; L \<subseteq> L\<star>; L\<star>" by (auto simp add: lang_seq_def)

  then show "L\<star>; L \<subseteq> L\<star>" using lang_star_double by blast

qed

lemma

  shows "L\<star> \<subseteq> L\<star>\<star>"

by (rule lang_star_simple)

section {* regular expressions *}

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

text{* ************ now is the codes writen by chunhan ************************************* *}

section {* Arden's Lemma revised *}

lemma arden_aux1:

  assumes a: "X \<subseteq> X ; A \<union> B"

  and     b: "[] \<notin> A"

  shows      "x \<in> X \<Longrightarrow> x \<in> B ; A\<star>"

apply (induct x taking:length rule:measure_induct)

apply (subgoal_tac "x \<in> X ; A \<union> B")

defer

using a

apply (auto)[1]

apply simp

apply (erule disjE)

defer

apply (auto simp add:lang_seq_def) [1]

apply (subgoal_tac "\<exists> x1 x2. x = x1 @ x2 \<and> x1 \<in> X \<and> x2 \<in> A")

defer

apply (auto simp add:lang_seq_def) [1]

apply (erule exE | erule conjE)+

apply simp

apply (drule_tac x = x1 in spec)

apply (simp)

using b

apply -

apply (auto)[1]

apply (subgoal_tac "x1 @ x2 \<in> (B ; A\<star>) ; A")

defer

apply (auto simp add:lang_seq_def)[1]

by (metis Un_absorb1 lang_seq_assoc lang_seq_union(2) lang_star_double lang_star_simple mem_def sup1CI)

theorem ardens_revised:

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

  shows "(X = X ; A \<union> B) \<longleftrightarrow> (X = B ; A\<star>)"

apply(rule iffI)

defer

apply(simp)

apply(subst lang_star_cases')

apply(subst lang_seq_union)

apply(simp add: lang_seq_empty)

apply(simp add: lang_seq_assoc)

apply(auto)[1]

proof -

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

  then have as1: "X ; A \<union> B \<subseteq> X" and as2: "X \<subseteq> X ; A \<union> B" by simp_all

  from as1 have a: "X ; A \<subseteq> X" and b: "B \<subseteq> X" by simp_all

  from b have "B; A\<star> \<subseteq> X ; A\<star>" by (auto simp add: lang_seq_def)

  moreover

  from a have "X ; A\<star> \<subseteq> X" 

by (rule lang_star_prop2)

  ultimately have f1: "B ; A\<star> \<subseteq> X" by simp

  from as2 nemp

  have f2: "X \<subseteq> B; A\<star>" using arden_aux1 by auto

  from f1 f2 show "X = B; A\<star>" by auto

qed

section {* equiv class' definition *}

definition 

  equiv_str :: "string \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> bool" ("_ \<equiv>_\<equiv> _" [100, 100, 100] 100)

where

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

definition

  equiv_class :: "string \<Rightarrow> (string set) \<Rightarrow> string set" ("\<lbrakk>_\<rbrakk>_" [100, 100] 100)

where

  "\<lbrakk>x\<rbrakk>Lang \<equiv> {y. x \<equiv>Lang\<equiv> y}"

text {* Chunhan modifies Q to Quo *}

definition  

  quot :: "string set \<Rightarrow> string set \<Rightarrow> (string set) set" ("_ Quo _" [100, 100] 100)

where

  "L1 Quo L2 \<equiv> { \<lbrakk>x\<rbrakk>L2 | x. x \<in> L1}" 

lemma lang_eqs_union_of_eqcls: 

  "Lang = \<Union> {X. X \<in> (UNIV Quo Lang) \<and> (\<forall> x \<in> X. x \<in> Lang)}"

proof

  show "Lang \<subseteq> \<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}"

  proof

    fix x

    assume "x \<in> Lang"

    thus "x \<in> \<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}"

    proof (simp add:quot_def)

      assume "(1)": "x \<in> Lang"

      show "\<exists>xa. (\<exists>x. xa = \<lbrakk>x\<rbrakk>Lang) \<and> (\<forall>x\<in>xa. x \<in> Lang) \<and> x \<in> xa" (is "\<exists>xa.?P xa")

      proof -

        have "?P (\<lbrakk>x\<rbrakk>Lang)" using "(1)"

          by (auto simp:equiv_class_def equiv_str_def dest: spec[where  x = "[]"])

        thus ?thesis by blast

      qed

    qed

  qed   

next

  show "\<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang} \<subseteq> Lang"

    by auto

qed

lemma empty_notin_CS: "{} \<notin> UNIV Quo Lang"

apply (clarsimp simp:quot_def equiv_class_def)

by (rule_tac x = x in exI, auto simp:equiv_str_def)

lemma no_two_cls_inters:

  "\<lbrakk>X \<in> UNIV Quo Lang; Y \<in> UNIV Quo Lang; X \<noteq> Y\<rbrakk> \<Longrightarrow> X \<inter> Y = {}"

by (auto simp:quot_def equiv_class_def equiv_str_def)

text {* equiv_class transition *}

definition 

  CT :: "string set \<Rightarrow> char \<Rightarrow> string set \<Rightarrow> bool" ("_-_\<rightarrow>_" [99,99]99)

where

  "X-c\<rightarrow>Y \<equiv> ((X;{[c]}) \<subseteq> Y)"

types t_equa_rhs = "(string set \<times> rexp) set"

types t_equa = "(string set \<times> t_equa_rhs)"

types t_equas = "t_equa set"

text {* 

  "empty_rhs" generates "\<lambda>" for init-state, just like "\<lambda>" for final states 

  in Brzozowski method. But if the init-state is "{[]}" ("\<lambda>" itself) then 

  empty set is returned, see definition of "equation_rhs" 

*} 

definition 

  empty_rhs :: "string set \<Rightarrow> t_equa_rhs"

where

  "empty_rhs X \<equiv> if ([] \<in> X) then {({[]}, EMPTY)} else {}"

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"

definition 

  equation_rhs :: "(string set) set \<Rightarrow> string set \<Rightarrow> t_equa_rhs"

where

  "equation_rhs CS X \<equiv> if (X = {[]}) then {({[]}, EMPTY)}

                         else {(S, folds ALT NULL {CHAR c| c. S-c\<rightarrow>X} )| S. S \<in> CS} \<union> empty_rhs X"

definition 

  equations :: "(string set) set \<Rightarrow> t_equas"

where

  "equations CS \<equiv> {(X, equation_rhs CS X) | X. X \<in> CS}"

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

begin

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

where

  "L_rhs rhs = {x. \<exists> X r. (X, r) \<in> rhs \<and> x \<in> X;(L r)}"

end

definition 

  distinct_rhs :: "t_equa_rhs \<Rightarrow> bool"

where

  "distinct_rhs rhs \<equiv> \<forall> X reg\<^isub>1 reg\<^isub>2. (X, reg\<^isub>1) \<in> rhs \<and> (X, reg\<^isub>2) \<in> rhs \<longrightarrow> reg\<^isub>1 = reg\<^isub>2"

definition

  distinct_equas_rhs :: "t_equas \<Rightarrow> bool"

where

  "distinct_equas_rhs equas \<equiv> \<forall> X rhs. (X, rhs) \<in> equas \<longrightarrow> distinct_rhs rhs"

definition 

  distinct_equas :: "t_equas \<Rightarrow> bool"

where

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

definition 

  seq_rhs_r :: "t_equa_rhs \<Rightarrow> rexp \<Rightarrow> t_equa_rhs"

where

  "seq_rhs_r rhs r \<equiv> (\<lambda>(X, reg). (X, SEQ reg r)) ` rhs"

definition 

  del_x_paired :: "('a \<times> 'b) set \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'b) set"

where

  "del_x_paired S x \<equiv> S - {X. X \<in> S \<and> fst X = x}"

definition

  arden_variate :: "string set \<Rightarrow> rexp \<Rightarrow> t_equa_rhs \<Rightarrow> t_equa_rhs"

where

  "arden_variate X r rhs \<equiv> seq_rhs_r (del_x_paired rhs X) (STAR r)"

definition

  no_EMPTY_rhs :: "t_equa_rhs \<Rightarrow> bool"

where

  "no_EMPTY_rhs rhs \<equiv> \<forall> X r. (X, r) \<in> rhs \<and> X \<noteq> {[]} \<longrightarrow> [] \<notin> L r"

definition 

  no_EMPTY_equas :: "t_equas \<Rightarrow> bool"

where

  "no_EMPTY_equas equas \<equiv> \<forall> X rhs. (X, rhs) \<in> equas \<longrightarrow> no_EMPTY_rhs rhs"

lemma fold_alt_null_eqs:

  "finite rS \<Longrightarrow> x \<in> L (folds ALT NULL rS) = (\<exists> r \<in> rS. x \<in> L r)"

apply (simp add:folds_def)

apply (rule someI2_ex)

apply (erule finite_imp_fold_graph)

apply (erule fold_graph.induct)

by auto (*??? how do this be in Isar ?? *)

lemma seq_rhs_r_prop1:

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

apply (auto simp:seq_rhs_r_def image_def lang_seq_def)

apply (rule_tac x = "s1 @ s1a" in exI, rule_tac x = "s2a" in exI, simp)

apply (rule_tac x = a in exI, rule_tac x = b in exI, simp)

apply (rule_tac x = s1 in exI, rule_tac x = s1a in exI, simp)

apply (rule_tac x = X in exI, rule_tac x  = "SEQ ra r" in exI, simp)

apply (rule conjI)

apply (rule_tac x = "(X, ra)" in bexI, simp+) 

apply (rule_tac x = s1a in exI, rule_tac x = "s2a @ s2" in exI, simp)

apply (simp add:lang_seq_def)

by (rule_tac x = s2a in exI, rule_tac x = s2 in exI, simp)

lemma del_x_paired_prop1:  

  "\<lbrakk>distinct_rhs rhs; (X, r) \<in> rhs\<rbrakk> \<Longrightarrow> X ; L r \<union> L (del_x_paired rhs X) = L rhs"

  apply (simp add:del_x_paired_def)

  apply (simp add: distinct_rhs_def)

  apply(auto simp add: lang_seq_def)

  apply(metis)

  done

lemma arden_variate_prop:

  assumes "(X, rx) \<in> rhs"

  shows "(\<forall> Y. Y \<noteq> X \<longrightarrow> (\<exists> r. (Y, r) \<in> rhs) = (\<exists> r. (Y, r) \<in> (arden_variate X rx rhs)))"

proof (rule allI, rule impI)

  fix Y

  assume "(1)": "Y \<noteq> X"

  show "(\<exists>r. (Y, r) \<in> rhs) = (\<exists>r. (Y, r) \<in> arden_variate X rx rhs)"

  proof

    assume "(1_1)": "\<exists>r. (Y, r) \<in> rhs"

    show "\<exists>r. (Y, r) \<in> arden_variate X rx rhs" (is "\<exists>r. ?P r")

    proof -

      from "(1_1)" obtain r where "(Y, r) \<in> rhs" ..

      hence "?P (SEQ r (STAR rx))"

      proof (simp add:arden_variate_def image_def)

        have "(Y, r) \<in> rhs \<Longrightarrow> (Y, r) \<in> del_x_paired rhs X"

          by (auto simp:del_x_paired_def "(1)")

        thus "(Y, r) \<in> rhs \<Longrightarrow> (Y, SEQ r (STAR rx)) \<in> seq_rhs_r (del_x_paired rhs X) (STAR rx)"

          by (auto simp:seq_rhs_r_def)

      qed

      thus ?thesis by blast

    qed

  next

    assume "(2_1)": "\<exists>r. (Y, r) \<in> arden_variate X rx rhs"

    thus "\<exists>r. (Y, r) \<in> rhs" (is "\<exists> r. ?P r")

      by (auto simp:arden_variate_def del_x_paired_def seq_rhs_r_def image_def)

  qed

qed

text {*

  arden_variate_valid:  proves variation from 

   "X = X;r + Y;ry + \<dots>" to "X = Y;(SEQ ry (STAR r)) + \<dots>" 

  holds the law of "language of left equiv language of right" 

*}

lemma arden_variate_valid:

  assumes X_not_empty: "X \<noteq> {[]}"

  and     l_eq_r:   "X = L rhs"

  and     dist: "distinct_rhs rhs"

  and     no_empty: "no_EMPTY_rhs rhs"

  and     self_contained: "(X, r) \<in> rhs"

  shows   "X = L (arden_variate X r rhs)" 

proof -

  have "[] \<notin> L r" using no_empty X_not_empty self_contained

    by (auto simp:no_EMPTY_rhs_def)

  hence ardens: "X = X;(L r) \<union> (L (del_x_paired rhs X)) \<longleftrightarrow> X = (L (del_x_paired rhs X)) ; (L r)\<star>" 

    by (rule ardens_revised)

  have del_x: "X = X ; L r \<union> L (del_x_paired rhs X) \<longleftrightarrow> X = L rhs" using dist l_eq_r self_contained

    by (auto dest!:del_x_paired_prop1)

  show ?thesis

  proof

    show "X \<subseteq> L (arden_variate X r rhs)"

    proof

      fix x

      assume "(1_1)": "x \<in> X" with l_eq_r ardens del_x

      show "x \<in> L (arden_variate X r rhs)" 

        by (simp add:arden_variate_def seq_rhs_r_prop1 del:L_rhs.simps)

    qed

  next

    show "L (arden_variate X r rhs) \<subseteq> X"

    proof

      fix x

      assume "(2_1)": "x \<in> L (arden_variate X r rhs)" with ardens del_x l_eq_r

      show "x \<in> X"