1 theory MyhillNerode

     2   imports "Main" "List_Prefix"

     3 begin

     4 

     5 text {* sequential composition of languages *}

     6 

     7 definition

     8   lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ; _" [100,100] 100)

     9 where 

    10   "L1 ; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"

    11 

    12 lemma lang_seq_empty:

    13   shows "{[]} ; L = L"

    14   and   "L ; {[]} = L"

    15 unfolding lang_seq_def by auto

    16 

    17 lemma lang_seq_null:

    18   shows "{} ; L = {}"

    19   and   "L ; {} = {}"

    20 unfolding lang_seq_def by auto

    21 

    22 lemma lang_seq_append:

    23   assumes a: "s1 \<in> L1"

    24   and     b: "s2 \<in> L2"

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

    26 unfolding lang_seq_def

    27 using a b by auto 

    28 

    29 lemma lang_seq_union:

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

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

    32 unfolding lang_seq_def by auto

    33 

    34 lemma lang_seq_assoc:

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

    36 unfolding lang_seq_def

    37 apply(auto)

    38 apply(metis)

    39 by (metis append_assoc)

    40 

    41 

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

    43 

    44 inductive_set

    45   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)

    46   for L :: "string set"

    47 where

    48   start[intro]: "[] \<in> L\<star>"

    49 | step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>"

    50 

    51 lemma lang_star_empty:

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

    53 by (auto elim: Star.cases)

    54 

    55 lemma lang_star_cases:

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

    57 proof

    58   { fix x

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

    60       unfolding lang_seq_def

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

    62   }

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

    64 next

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

    66     unfolding lang_seq_def by auto

    67 qed

    68 

    69 lemma lang_star_cases':

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

    71 proof

    72   { fix x

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

    74       unfolding lang_seq_def

    75     apply (induct rule: Star.induct)

    76     apply simp

    77     apply simp

    78     apply (erule disjE)

    79     apply (auto)[1]

    80     apply (erule exE | erule conjE)+

    81     apply (rule disjI2)

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

    83     by auto

    84   }

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

    86 next

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

    88     unfolding lang_seq_def

    89     apply auto

    90     apply (erule Star.induct)

    91     apply auto

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

    93     by (auto intro:start)

    94 qed

    95 

    96 lemma lang_star_simple:

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

    98 by (subst lang_star_cases)

    99    (auto simp only: lang_seq_def)

   100 

   101 lemma lang_star_prop0_aux:

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

   103 apply (erule Star.induct)

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

   105 apply (clarify, drule_tac x = s1 in spec)

   106 apply (drule mp, simp, clarify)

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

   108 by auto

   109 

   110 lemma lang_star_prop0:

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

   112 by (auto dest:lang_star_prop0_aux)

   113 

   114 lemma lang_star_prop1:

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

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

   117 proof -

   118   { fix s1 s2

   119     assume minor: "s2 \<in> L2"

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

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

   122     proof(induct rule: Star.induct)

   123       case start

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

   125     next

   126       case (step s1 s1')

   127       have "s1 \<in> L1" by fact

   128       moreover

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

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

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

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

   133     qed

   134   } 

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

   136 qed

   137 

   138 lemma lang_star_prop2_aux:

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

   140 apply (erule Star.induct, simp)

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

   142 by (auto simp:lang_seq_def)

   143 

   144 lemma lang_star_prop2:

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

   146 by (auto dest!:lang_star_prop2_aux simp:lang_seq_def)

   147 

   148 lemma lang_star_seq_subseteq: 

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

   150 using lang_star_cases by blast

   151 

   152 lemma lang_star_double:

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

   154 proof

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

   156     using lang_star_prop1 lang_star_seq_subseteq by blast

   157 next

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

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

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

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

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

   163 qed

   164 

   165 lemma lang_star_seq_subseteq': 

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

   167 proof -

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

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

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

   171 qed

   172 

   173 lemma

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

   175 by (rule lang_star_simple)

   176 

   177 

   178 section {* regular expressions *}

   179 

   180 datatype rexp =

   181   NULL

   182 | EMPTY

   183 | CHAR char

   184 | SEQ rexp rexp

   185 | ALT rexp rexp

   186 | STAR rexp

   187 

   188 

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

   190 

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

   192 begin

   193 fun

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

   195 where

   196     "L_rexp (NULL) = {}"

   197   | "L_rexp (EMPTY) = {[]}"

   198   | "L_rexp (CHAR c) = {[c]}"

   199   | "L_rexp (SEQ r1 r2) = (L_rexp r1) ; (L_rexp r2)"

   200   | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"

   201   | "L_rexp (STAR r) = (L_rexp r)\<star>"

   202 end

   203 

   204 

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

   206 

   207 section {* Arden's Lemma revised *}

   208 

   209 lemma arden_aux1:

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

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

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

   213 apply (induct x taking:length rule:measure_induct)

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

   215 defer

   216 using a

   217 apply (auto)[1]

   218 apply simp

   219 apply (erule disjE)

   220 defer

   221 apply (auto simp add:lang_seq_def) [1]

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

   223 defer

   224 apply (auto simp add:lang_seq_def) [1]

   225 apply (erule exE | erule conjE)+

   226 apply simp

   227 apply (drule_tac x = x1 in spec)

   228 apply (simp)

   229 using b

   230 apply -

   231 apply (auto)[1]

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

   233 defer

   234 apply (auto simp add:lang_seq_def)[1]

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

   236 

   237 theorem ardens_revised:

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

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

   240 apply(rule iffI)

   241 defer

   242 apply(simp)

   243 apply(subst lang_star_cases')

   244 apply(subst lang_seq_union)

   245 apply(simp add: lang_seq_empty)

   246 apply(simp add: lang_seq_assoc)

   247 apply(auto)[1]

   248 proof -

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

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

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

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

   253   moreover

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

   255 

   256 by (rule lang_star_prop2)

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

   258   from as2 nemp

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

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

   261 qed

   262 

   263 

   264 

   265 section {* equiv class' definition *}

   266 

   267 definition 

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

   269 where

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

   271 

   272 definition

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

   274 where

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

   276 

   277 text {* Chunhan modifies Q to Quo *}

   278 

   279 definition  

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

   281 where

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

   283 

   284 

   285 lemma lang_eqs_union_of_eqcls: 

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

   287 proof

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

   289   proof

   290     fix x

   291     assume "x \<in> Lang"

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

   293     proof (simp add:quot_def)

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

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

   296       proof -

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

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

   299         thus ?thesis by blast

   300       qed

   301     qed

   302   qed   

   303 next

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

   305     by auto

   306 qed

   307 

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

   309 apply (clarsimp simp:quot_def equiv_class_def)

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

   311 

   312 lemma no_two_cls_inters:

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

   314 by (auto simp:quot_def equiv_class_def equiv_str_def)

   315 

   316 text {* equiv_class transition *}

   317 definition 

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

   319 where

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

   321 

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

   323 

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

   325 

   326 types t_equas = "t_equa set"

   327 

   328 text {* 

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

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

   331   empty set is returned, see definition of "equation_rhs" 

   332 *} 

   333 

   334 definition 

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

   336 where

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

   338 

   339 definition 

   340   folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"

   341 where

   342   "folds f z S \<equiv> SOME x. fold_graph f z S x"

   343 

   344 definition 

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

   346 where

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

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

   349 

   350 definition 

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

   352 where

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

   354 

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

   356 begin

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

   358 where

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

   360 end

   361 

   362 definition 

   363   distinct_rhs :: "t_equa_rhs \<Rightarrow> bool"

   364 where

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

   366 

   367 definition

   368   distinct_equas_rhs :: "t_equas \<Rightarrow> bool"

   369 where

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

   371 

   372 definition 

   373   distinct_equas :: "t_equas \<Rightarrow> bool"

   374 where

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

   376 

   377 definition 

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

   379 where

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

   381 

   382 definition 

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

   384 where

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

   386 

   387 definition

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

   389 where

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

   391 

   392 definition

   393   no_EMPTY_rhs :: "t_equa_rhs \<Rightarrow> bool"

   394 where

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

   396 

   397 definition 

   398   no_EMPTY_equas :: "t_equas \<Rightarrow> bool"

   399 where

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

   401 

   402 lemma fold_alt_null_eqs:

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

   404 apply (simp add:folds_def)

   405 apply (rule someI2_ex)

   406 apply (erule finite_imp_fold_graph)

   407 apply (erule fold_graph.induct)

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

   409 

   410 lemma seq_rhs_r_prop1:

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

   412 apply (auto simp:seq_rhs_r_def image_def lang_seq_def)

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

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

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

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

   417 apply (rule conjI)

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

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

   420 apply (simp add:lang_seq_def)

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

   422 

   423 lemma del_x_paired_prop1:  

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

   425   apply (simp add:del_x_paired_def)

   426   apply (simp add: distinct_rhs_def)

   427   apply(auto simp add: lang_seq_def)

   428   apply(metis)

   429   done

   430 

   431 lemma arden_variate_prop:

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

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

   434 proof (rule allI, rule impI)

   435   fix Y

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

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

   438   proof

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

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

   441     proof -

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

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

   444       proof (simp add:arden_variate_def image_def)

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

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

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

   448           by (auto simp:seq_rhs_r_def)

   449       qed

   450       thus ?thesis by blast

   451     qed

   452   next

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

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

   455       by (auto simp:arden_variate_def del_x_paired_def seq_rhs_r_def image_def)

   456   qed

   457 qed

   458 

   459 text {*

   460   arden_variate_valid:  proves variation from 

   461   

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

   463 

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

   465 *}

   466 lemma arden_variate_valid:

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

   468   and     l_eq_r:   "X = L rhs"

   469   and     dist: "distinct_rhs rhs"

   470   and     no_empty: "no_EMPTY_rhs rhs"

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

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

   473 proof -

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

   475     by (auto simp:no_EMPTY_rhs_def)

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

   477     by (rule ardens_revised)

   478   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

   479     by (auto dest!:del_x_paired_prop1)

   480   show ?thesis

   481   proof

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

   483     proof

   484       fix x

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

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

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

   488     qed

   489   next

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

   491     proof

   492       fix x

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

   494       show "x \<in> X" 

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

   496     qed

   497   qed

   498 qed

   499 

   500 text {* 

   501   merge_rhs {(x1, r1), (x2, r2}, (x4, r4), \<dots>} {(x1, r1'), (x3, r3'), \<dots>} = 

   502      {(x1, ALT r1 r1'}, (x2, r2), (x3, r3'), (x4, r4), \<dots>} *}  

   503 definition 

   504   merge_rhs :: "t_equa_rhs \<Rightarrow> t_equa_rhs \<Rightarrow> t_equa_rhs"

   505 where

   506   "merge_rhs rhs rhs' \<equiv> {(X, r). (\<exists> r1 r2. ((X,r1) \<in> rhs \<and> (X, r2) \<in> rhs') \<and> r = ALT r1 r2)  \<or>

   507                                  (\<exists> r1. (X, r1) \<in> rhs \<and> (\<not> (\<exists> r2. (X, r2) \<in> rhs')) \<and> r = r1) \<or>

   508                                  (\<exists> r2. (X, r2) \<in> rhs' \<and> (\<not> (\<exists> r1. (X, r1) \<in> rhs)) \<and> r = r2)    }"                                  

   509 

   510 

   511 text {* rhs_subst rhs X=xrhs r: substitude all occurence of X in rhs((X,r) \<in> rhs) with xrhs *}

   512 definition 

   513   rhs_subst :: "t_equa_rhs \<Rightarrow> string set \<Rightarrow> t_equa_rhs \<Rightarrow> rexp \<Rightarrow> t_equa_rhs"

   514 where

   515   "rhs_subst rhs X xrhs r \<equiv> merge_rhs (del_x_paired rhs X) (seq_rhs_r xrhs r)"

   516 

   517 definition 

   518   equas_subst_f :: "string set \<Rightarrow> t_equa_rhs \<Rightarrow> t_equa \<Rightarrow> t_equa"

   519 where

   520   "equas_subst_f X xrhs equa \<equiv> let (Y, rhs) = equa in

   521                                  if (\<exists> r. (X, r) \<in> rhs)

   522                                  then (Y, rhs_subst rhs X xrhs (SOME r. (X, r) \<in> rhs))

   523                                  else equa"

   524 

   525 definition

   526   equas_subst :: "t_equas \<Rightarrow> string set \<Rightarrow> t_equa_rhs \<Rightarrow> t_equas"

   527 where

   528   "equas_subst ES X xrhs \<equiv> del_x_paired (equas_subst_f X xrhs ` ES) X"

   529 

   530 lemma lang_seq_prop1:

   531  "x \<in> X ; L r \<Longrightarrow> x \<in> X ; (L r \<union> L r')"

   532 by (auto simp:lang_seq_def)

   533 

   534 lemma lang_seq_prop1':

   535   "x \<in> X; L r \<Longrightarrow> x \<in> X ; (L r' \<union> L r)"

   536 by (auto simp:lang_seq_def)

   537 

   538 lemma lang_seq_prop2:

   539   "x \<in> X; (L r \<union> L r') \<Longrightarrow> x \<in> X;L r \<or> x \<in> X;L r'"

   540 by (auto simp:lang_seq_def)

   541 

   542 lemma merge_rhs_prop1:

   543   shows "L (merge_rhs rhs rhs') = L rhs \<union> L rhs' "

   544 apply (auto simp add:merge_rhs_def dest!:lang_seq_prop2 intro:lang_seq_prop1)

   545 apply (rule_tac x = X in exI, rule_tac x = r1 in exI, simp)

   546 apply (case_tac "\<exists> r2. (X, r2) \<in> rhs'")

   547 apply (clarify, rule_tac x = X in exI, rule_tac x = "ALT r r2" in exI, simp add:lang_seq_prop1)

   548 apply (rule_tac x = X in exI, rule_tac x = r in exI, simp)

   549 apply (case_tac "\<exists> r1. (X, r1) \<in> rhs")

   550 apply (clarify, rule_tac x = X in exI, rule_tac x = "ALT r1 r" in exI, simp add:lang_seq_prop1')

   551 apply (rule_tac x = X in exI, rule_tac x = r in exI, simp)

   552 done

   553 

   554 lemma no_EMPTY_rhss_imp_merge_no_EMPTY:

   555   "\<lbrakk>no_EMPTY_rhs rhs; no_EMPTY_rhs rhs'\<rbrakk> \<Longrightarrow> no_EMPTY_rhs (merge_rhs rhs rhs')"

   556 apply (simp add:no_EMPTY_rhs_def merge_rhs_def)

   557 apply (clarify, (erule conjE | erule exE | erule disjE)+)

   558 by auto

   559 

   560 lemma distinct_rhs_prop:

   561   "\<lbrakk>distinct_rhs rhs; (X, r1) \<in> rhs; (X, r2) \<in> rhs\<rbrakk> \<Longrightarrow> r1 = r2"

   562 by (auto simp:distinct_rhs_def)

   563 

   564 lemma merge_rhs_prop2:

   565   assumes dist_rhs: "distinct_rhs rhs"

   566   and     dist_rhs':"distinct_rhs rhs'"

   567   shows "distinct_rhs (merge_rhs rhs rhs')"

   568 apply (auto simp:merge_rhs_def distinct_rhs_def)

   569 using dist_rhs

   570 apply (drule distinct_rhs_prop, simp+)

   571 using dist_rhs'

   572 apply (drule distinct_rhs_prop, simp+)

   573 using dist_rhs

   574 apply (drule distinct_rhs_prop, simp+)

   575 using dist_rhs'

   576 apply (drule distinct_rhs_prop, simp+)

   577 done

   578 

   579 lemma seq_rhs_r_holds_distinct: 

   580   "distinct_rhs rhs \<Longrightarrow> distinct_rhs (seq_rhs_r rhs r)"

   581 by (auto simp:distinct_rhs_def seq_rhs_r_def)

   582 

   583 lemma seq_rhs_r_prop0:

   584   assumes l_eq_r: "X = L xrhs"

   585   shows "L (seq_rhs_r xrhs r) = X ; L r "

   586 using l_eq_r

   587 by (auto simp only:seq_rhs_r_prop1)

   588 

   589 lemma rhs_subst_prop1:

   590   assumes l_eq_r: "X = L xrhs"

   591   and     dist:  "distinct_rhs rhs"

   592   shows "(X, r) \<in> rhs \<Longrightarrow> L rhs = L (rhs_subst rhs X xrhs r)"

   593 apply (simp add:rhs_subst_def merge_rhs_prop1 del:L_rhs.simps)

   594 using l_eq_r 

   595 apply (drule_tac r = r in seq_rhs_r_prop0, simp del:L_rhs.simps)

   596 using dist

   597 by (auto dest!:del_x_paired_prop1 simp del:L_rhs.simps)

   598 

   599 lemma del_x_paired_holds_distinct_rhs:

   600   "distinct_rhs rhs \<Longrightarrow> distinct_rhs (del_x_paired rhs x)"

   601 by (auto simp:distinct_rhs_def del_x_paired_def)

   602 

   603 lemma rhs_subst_holds_distinct_rhs:

   604   "\<lbrakk>distinct_rhs rhs; distinct_rhs xrhs\<rbrakk> \<Longrightarrow> distinct_rhs (rhs_subst rhs X xrhs r)"

   605 apply (drule_tac r = r and rhs = xrhs in seq_rhs_r_holds_distinct)

   606 apply (drule_tac x = X in del_x_paired_holds_distinct_rhs)

   607 by (auto dest:merge_rhs_prop2[where rhs = "del_x_paired rhs X"] simp:rhs_subst_def)

   608 

   609 section {* myhill-nerode theorem *}

   610 

   611 definition left_eq_cls :: "t_equas \<Rightarrow> (string set) set"

   612 where

   613   "left_eq_cls ES \<equiv> {X. \<exists> rhs. (X, rhs) \<in> ES} "

   614 

   615 definition right_eq_cls :: "t_equas \<Rightarrow> (string set) set"

   616 where

   617   "right_eq_cls ES \<equiv> {Y. \<exists> X rhs r. (X, rhs) \<in> ES \<and> (Y, r) \<in> rhs }"

   618 

   619 definition rhs_eq_cls :: "t_equa_rhs \<Rightarrow> (string set) set"

   620 where

   621   "rhs_eq_cls rhs \<equiv> {Y. \<exists> r. (Y, r) \<in> rhs}"

   622 

   623 definition ardenable :: "t_equa \<Rightarrow> bool"

   624 where

   625   "ardenable equa \<equiv> let (X, rhs) = equa in 

   626                       distinct_rhs rhs \<and> no_EMPTY_rhs rhs \<and> X = L rhs"

   627 

   628 text {*

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

   630 *}

   631 definition Inv :: "string set \<Rightarrow> t_equas \<Rightarrow> bool"

   632 where

   633   "Inv X ES \<equiv> finite ES \<and> (\<exists> rhs. (X, rhs) \<in> ES) \<and> distinct_equas ES \<and> 

   634             (\<forall> X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs) \<and> X \<noteq> {} \<and> rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls ES))"

   635 

   636 text {*

   637   TCon: Termination Condition of the equation-system decreasion.

   638 *}

   639 definition TCon:: "'a set \<Rightarrow> bool"

   640 where

   641   "TCon ES \<equiv> card ES = 1"

   642 

   643 

   644 text {* 

   645   The following is a iteration principle, and is the main framework for the proof:

   646    1: We can form the initial equation-system using "equations" defined above, and prove it has invariance Inv by lemma "init_ES_satisfy_Inv";

   647    2: We can decrease the number of the equation-system using ardens_lemma_revised and substitution ("equas_subst", defined above), 

   648         and prove it holds the property "step" in "wf_iter" by lemma "iteration_step"

   649    and finally using property Inv and TCon to prove the myhill-nerode theorem

   650   

   651 *}

   652 lemma wf_iter [rule_format]: 

   653   fixes f

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

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

   656 proof(induct e rule: wf_induct 

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

   658   fix x 

   659   assume h [rule_format]: 

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

   661     and px: "P x"

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

   663   proof(cases "Q x")

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

   665   next

   666     assume nq: "\<not> Q x"

   667     from step [OF px nq]

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

   669     show ?thesis

   670     proof(rule h)

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

   672 	by (simp add:inv_image_def)

   673     next

   674       from pe' show "P e'" .

   675     qed

   676   qed

   677 qed

   678 

   679 

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

   681 

   682 lemma distinct_rhs_equations:

   683   "(X, xrhs) \<in> equations (UNIV Quo Lang) \<Longrightarrow> distinct_rhs xrhs"

   684 by (auto simp: equations_def equation_rhs_def distinct_rhs_def empty_rhs_def dest:no_two_cls_inters)

   685 

   686 lemma every_nonempty_eqclass_has_strings:

   687   "\<lbrakk>X \<in> (UNIV Quo Lang); X \<noteq> {[]}\<rbrakk> \<Longrightarrow> \<exists> clist. clist \<in> X \<and> clist \<noteq> []"

   688 by (auto simp:quot_def equiv_class_def equiv_str_def)

   689 

   690 lemma every_eqclass_is_derived_from_empty:

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

   692   shows "X \<in> (UNIV Quo Lang) \<Longrightarrow> \<exists> clist. {[]};{clist} \<subseteq> X \<and> clist \<noteq> []"

   693 using not_empty

   694 apply (drule_tac every_nonempty_eqclass_has_strings, simp)

   695 by (auto intro:exI[where x = clist] simp:lang_seq_def)

   696 

   697 lemma equiv_str_in_CS:

   698   "\<lbrakk>clist\<rbrakk>Lang \<in> (UNIV Quo Lang)"

   699 by (auto simp:quot_def)

   700 

   701 lemma has_str_imp_defined_by_str:

   702   "\<lbrakk>str \<in> X; X \<in> UNIV Quo Lang\<rbrakk> \<Longrightarrow> X = \<lbrakk>str\<rbrakk>Lang"

   703 by (auto simp:quot_def equiv_class_def equiv_str_def)

   704 

   705 lemma every_eqclass_has_ascendent:

   706   assumes has_str: "clist @ [c] \<in> X"

   707   and     in_CS:   "X \<in> UNIV Quo Lang"

   708   shows "\<exists> Y. Y \<in> UNIV Quo Lang \<and> Y-c\<rightarrow>X \<and> clist \<in> Y" (is "\<exists> Y. ?P Y")

   709 proof -

   710   have "?P (\<lbrakk>clist\<rbrakk>Lang)" 

   711   proof -

   712     have "\<lbrakk>clist\<rbrakk>Lang \<in> UNIV Quo Lang"       

   713       by (simp add:quot_def, rule_tac x = clist in exI, simp)

   714     moreover have "\<lbrakk>clist\<rbrakk>Lang-c\<rightarrow>X" 

   715     proof -

   716       have "X = \<lbrakk>(clist @ [c])\<rbrakk>Lang" using has_str in_CS

   717         by (auto intro!:has_str_imp_defined_by_str)

   718       moreover have "\<forall> sl. sl \<in> \<lbrakk>clist\<rbrakk>Lang \<longrightarrow> sl @ [c] \<in> \<lbrakk>(clist @ [c])\<rbrakk>Lang"

   719         by (auto simp:equiv_class_def equiv_str_def)

   720       ultimately show ?thesis unfolding CT_def lang_seq_def

   721         by auto

   722     qed

   723     moreover have "clist \<in> \<lbrakk>clist\<rbrakk>Lang" 

   724       by (auto simp:equiv_str_def equiv_class_def)

   725     ultimately show "?P (\<lbrakk>clist\<rbrakk>Lang)" by simp

   726   qed

   727   thus ?thesis by blast

   728 qed

   729 

   730 lemma finite_charset_rS:

   731   "finite {CHAR c |c. Y-c\<rightarrow>X}"

   732 by (rule_tac A = UNIV and f = CHAR in finite_surj, auto)

   733 

   734 lemma l_eq_r_in_equations:

   735   assumes X_in_equas: "(X, xrhs) \<in> equations (UNIV Quo Lang)"

   736   shows "X = L xrhs"    

   737 proof (cases "X = {[]}")

   738   case True

   739   thus ?thesis using X_in_equas 

   740     by (simp add:equations_def equation_rhs_def lang_seq_def)

   741 next

   742   case False 

   743   show ?thesis

   744   proof 

   745     show "X \<subseteq> L xrhs"

   746     proof

   747       fix x

   748       assume "(1)": "x \<in> X"

   749       show "x \<in> L xrhs"          

   750       proof (cases "x = []")

   751         assume empty: "x = []"

   752         hence "x \<in> L (empty_rhs X)" using "(1)"

   753           by (auto simp:empty_rhs_def lang_seq_def)

   754         thus ?thesis using X_in_equas False empty "(1)" 

   755           unfolding equations_def equation_rhs_def by auto

   756       next

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

   758         hence "\<exists> clist c. x = clist @ [c]" by (case_tac x rule:rev_cases, auto)

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

   760         moreover have "\<And> Y. \<lbrakk>Y \<in> UNIV Quo Lang; Y-c\<rightarrow>X; clist \<in> Y\<rbrakk>

   761           \<Longrightarrow> [c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})"

   762         proof -

   763           fix Y

   764           assume Y_is_eq_cl: "Y \<in> UNIV Quo Lang"

   765             and Y_CT_X: "Y-c\<rightarrow>X"

   766             and clist_in_Y: "clist \<in> Y"

   767           with finite_charset_rS 

   768           show "[c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})"

   769             by (auto simp :fold_alt_null_eqs)

   770         qed

   771         hence "\<exists>Xa. Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" 

   772           using X_in_equas False not_empty "(1)" decom

   773           by (auto dest!:every_eqclass_has_ascendent simp:equations_def equation_rhs_def lang_seq_def)

   774         then obtain Xa where 

   775           "Xa \<in> UNIV Quo Lang \<and> clist @ [c] \<in> Xa ; L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})" by blast

   776         hence "x \<in> L {(S, folds ALT NULL {CHAR c |c. S-c\<rightarrow>X}) |S. S \<in> UNIV Quo Lang}" 

   777           using X_in_equas "(1)" decom

   778           by (auto simp add:equations_def equation_rhs_def intro!:exI[where x = Xa])

   779         thus "x \<in> L xrhs" using X_in_equas False not_empty unfolding equations_def equation_rhs_def

   780           by auto

   781       qed

   782     qed

   783   next

   784     show "L xrhs \<subseteq> X"

   785     proof

   786       fix x 

   787       assume "(2)": "x \<in> L xrhs"

   788       have "(2_1)": "\<And> s1 s2 r Xa. \<lbrakk>s1 \<in> Xa; s2 \<in> L (folds ALT NULL {CHAR c |c. Xa-c\<rightarrow>X})\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X"

   789         using finite_charset_rS

   790         by (auto simp:CT_def lang_seq_def fold_alt_null_eqs)

   791       have "(2_2)": "\<And> s1 s2 Xa r.\<lbrakk>s1 \<in> Xa; s2 \<in> L r; (Xa, r) \<in> empty_rhs X\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> X"

   792         by (simp add:empty_rhs_def split:if_splits)

   793       show "x \<in> X" using X_in_equas False "(2)"         

   794         by (auto intro:"(2_1)" "(2_2)" simp:equations_def equation_rhs_def lang_seq_def)

   795     qed

   796   qed

   797 qed

   798 

   799 

   800 

   801 lemma no_EMPTY_equations:

   802   "(X, xrhs) \<in> equations CS \<Longrightarrow> no_EMPTY_rhs xrhs"

   803 apply (clarsimp simp add:equations_def equation_rhs_def)

   804 apply (simp add:no_EMPTY_rhs_def empty_rhs_def, auto)

   805 apply (subgoal_tac "finite {CHAR c |c. Xa-c\<rightarrow>X}", drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_charset_rS)+

   806 done

   807 

   808 lemma init_ES_satisfy_ardenable:

   809   "(X, xrhs) \<in> equations (UNIV Quo Lang)  \<Longrightarrow> ardenable (X, xrhs)"  

   810   unfolding ardenable_def

   811   by (auto intro:distinct_rhs_equations no_EMPTY_equations simp:l_eq_r_in_equations simp del:L_rhs.simps)

   812 

   813 lemma init_ES_satisfy_Inv:

   814   assumes finite_CS: "finite (UNIV Quo Lang)"

   815   and X_in_eq_cls: "X \<in> UNIV Quo Lang"

   816   shows "Inv X (equations (UNIV Quo Lang))"

   817 proof -

   818   have "finite (equations (UNIV Quo Lang))" using finite_CS

   819     by (auto simp:equations_def)    

   820   moreover have "\<exists>rhs. (X, rhs) \<in> equations (UNIV Quo Lang)" using X_in_eq_cls 

   821     by (simp add:equations_def)

   822   moreover have "distinct_equas (equations (UNIV Quo Lang))" 

   823     by (auto simp:distinct_equas_def equations_def)

   824   moreover have "\<forall>X xrhs. (X, xrhs) \<in> equations (UNIV Quo Lang) \<longrightarrow>

   825                  rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (equations (UNIV Quo Lang)))" 

   826     apply (simp add:left_eq_cls_def equations_def rhs_eq_cls_def equation_rhs_def)

   827     by (auto simp:empty_rhs_def split:if_splits)

   828   moreover have "\<forall>X xrhs. (X, xrhs) \<in> equations (UNIV Quo Lang) \<longrightarrow> X \<noteq> {}"

   829     by (clarsimp simp:equations_def empty_notin_CS intro:classical)

   830   moreover have "\<forall>X xrhs. (X, xrhs) \<in> equations (UNIV Quo Lang) \<longrightarrow> ardenable (X, xrhs)"

   831     by (auto intro!:init_ES_satisfy_ardenable)

   832   ultimately show ?thesis by (simp add:Inv_def)

   833 qed

   834 

   835 

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

   837 

   838 

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

   840 

   841 lemma not_T_aux: "\<lbrakk>\<not> TCon (insert a A); x = a\<rbrakk>

   842        \<Longrightarrow> \<exists>y. x \<noteq> y \<and> y \<in> insert a A "

   843 apply (case_tac "insert a A = {a}")

   844 by (auto simp:TCon_def)

   845 

   846 lemma not_T_atleast_2[rule_format]:

   847   "finite S \<Longrightarrow> \<forall> x. x \<in> S \<and> (\<not> TCon S)\<longrightarrow> (\<exists> y. x \<noteq> y \<and> y \<in> S)"

   848 apply (erule finite.induct, simp)

   849 apply (clarify, case_tac "x = a")

   850 by (erule not_T_aux, auto)

   851 

   852 lemma exist_another_equa: 

   853   "\<lbrakk>\<not> TCon ES; finite ES; distinct_equas ES; (X, rhl) \<in> ES\<rbrakk> \<Longrightarrow> \<exists> Y yrhl. (Y, yrhl) \<in> ES \<and> X \<noteq> Y"

   854 apply (drule not_T_atleast_2, simp)

   855 apply (clarsimp simp:distinct_equas_def)

   856 apply (drule_tac x= X in spec, drule_tac x = rhl in spec, drule_tac x = b in spec)

   857 by auto

   858 

   859 lemma Inv_mono_with_lambda:

   860   assumes Inv_ES: "Inv X ES"

   861   and X_noteq_Y:  "X \<noteq> {[]}"

   862   shows "Inv X (ES - {({[]}, yrhs)})"

   863 proof -

   864   have "finite (ES - {({[]}, yrhs)})" using Inv_ES

   865     by (simp add:Inv_def)

   866   moreover have "\<exists>rhs. (X, rhs) \<in> ES - {({[]}, yrhs)}" using Inv_ES X_noteq_Y

   867     by (simp add:Inv_def)

   868   moreover have "distinct_equas (ES - {({[]}, yrhs)})" using Inv_ES X_noteq_Y

   869     apply (clarsimp simp:Inv_def distinct_equas_def)

   870     by (drule_tac x = Xa in spec, simp)    

   871   moreover have "\<forall>X xrhs.(X, xrhs) \<in> ES - {({[]}, yrhs)} \<longrightarrow>

   872                           ardenable (X, xrhs) \<and> X \<noteq> {}" using Inv_ES

   873     by (clarify, simp add:Inv_def)

   874   moreover 

   875   have "insert {[]} (left_eq_cls (ES - {({[]}, yrhs)})) = insert {[]} (left_eq_cls ES)"

   876     by (auto simp:left_eq_cls_def)

   877   hence "\<forall>X xrhs.(X, xrhs) \<in> ES - {({[]}, yrhs)} \<longrightarrow>

   878                           rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (ES - {({[]}, yrhs)}))"

   879     using Inv_ES by (auto simp:Inv_def)

   880   ultimately show ?thesis by (simp add:Inv_def)

   881 qed

   882 

   883 lemma non_empty_card_prop:

   884   "finite ES \<Longrightarrow> \<forall>e. e \<in> ES \<longrightarrow> card ES - Suc 0 < card ES"

   885 apply (erule finite.induct, simp)

   886 apply (case_tac[!] "a \<in> A")

   887 by (auto simp:insert_absorb)

   888 

   889 lemma ardenable_prop:

   890   assumes not_lambda: "Y \<noteq> {[]}"

   891   and ardable: "ardenable (Y, yrhs)"

   892   shows "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" (is "\<exists> yrhs'. ?P yrhs'")

   893 proof (cases "(\<exists> reg. (Y, reg) \<in> yrhs)")

   894   case True

   895   thus ?thesis 

   896   proof 

   897     fix reg

   898     assume self_contained: "(Y, reg) \<in> yrhs"

   899     show ?thesis 

   900     proof -

   901       have "?P (arden_variate Y reg yrhs)"

   902       proof -

   903         have "Y = L (arden_variate Y reg yrhs)" 

   904           using self_contained not_lambda ardable

   905           by (rule_tac arden_variate_valid, simp_all add:ardenable_def)

   906         moreover have "distinct_rhs (arden_variate Y reg yrhs)" 

   907           using ardable 

   908           by (auto simp:distinct_rhs_def arden_variate_def seq_rhs_r_def del_x_paired_def ardenable_def)

   909         moreover have "rhs_eq_cls (arden_variate Y reg yrhs) = rhs_eq_cls yrhs - {Y}"

   910         proof -

   911           have "\<And> rhs r. rhs_eq_cls (seq_rhs_r rhs r) = rhs_eq_cls rhs"

   912             apply (auto simp:rhs_eq_cls_def seq_rhs_r_def image_def)

   913             by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "(x, ra)" in bexI, simp+)

   914           moreover have "\<And> rhs X. rhs_eq_cls (del_x_paired rhs X) = rhs_eq_cls rhs - {X}"

   915             by (auto simp:rhs_eq_cls_def del_x_paired_def)

   916           ultimately show ?thesis by (simp add:arden_variate_def)

   917         qed

   918         ultimately show ?thesis by simp

   919       qed

   920       thus ?thesis by (rule_tac x= "arden_variate Y reg yrhs" in exI, simp)

   921     qed

   922   qed

   923 next

   924   case False

   925   hence "(2)": "rhs_eq_cls yrhs - {Y} = rhs_eq_cls yrhs"

   926     by (auto simp:rhs_eq_cls_def)

   927   show ?thesis 

   928   proof -

   929     have "?P yrhs" using False ardable "(2)" 

   930       by (simp add:ardenable_def)      

   931     thus ?thesis by blast

   932   qed

   933 qed

   934 

   935 lemma equas_subst_f_del_no_other:

   936   assumes self_contained: "(Y, rhs) \<in> ES"

   937   shows "\<exists> rhs'. (Y, rhs') \<in> (equas_subst_f X xrhs ` ES)" (is "\<exists> rhs'. ?P rhs'")

   938 proof -

   939   have "\<exists> rhs'. equas_subst_f X xrhs (Y, rhs) = (Y, rhs')"

   940     by (auto simp:equas_subst_f_def)

   941   then obtain rhs' where "equas_subst_f X xrhs (Y, rhs) = (Y, rhs')" by blast

   942   hence "?P rhs'" unfolding image_def using self_contained

   943     by (auto intro:bexI[where x = "(Y, rhs)"])

   944   thus ?thesis by blast

   945 qed

   946 

   947 lemma del_x_paired_del_only_x: 

   948   "\<lbrakk>X \<noteq> Y; (X, rhs) \<in> ES\<rbrakk> \<Longrightarrow> (X, rhs) \<in> del_x_paired ES Y"

   949 by (auto simp:del_x_paired_def)

   950 

   951 lemma equas_subst_del_no_other:

   952  "\<lbrakk>(X, rhs) \<in> ES; X \<noteq> Y\<rbrakk> \<Longrightarrow> (\<exists>rhs. (X, rhs) \<in> equas_subst ES Y rhs')"

   953 unfolding equas_subst_def

   954 apply (drule_tac X = Y and xrhs = rhs' in equas_subst_f_del_no_other)

   955 by (erule exE, drule del_x_paired_del_only_x, auto)

   956 

   957 lemma equas_subst_holds_distinct:

   958   "distinct_equas ES \<Longrightarrow> distinct_equas (equas_subst ES Y rhs')"

   959 apply (clarsimp simp add:equas_subst_def distinct_equas_def del_x_paired_def equas_subst_f_def)

   960 by (auto split:if_splits)

   961 

   962 lemma del_x_paired_dels: 

   963   "(X, rhs) \<in> ES \<Longrightarrow> {Y. Y \<in> ES \<and> fst Y = X} \<inter> ES \<noteq> {}"

   964 by (auto)

   965 

   966 lemma del_x_paired_subset:

   967   "(X, rhs) \<in> ES \<Longrightarrow> ES - {Y. Y \<in> ES \<and> fst Y = X} \<subset> ES"

   968 apply (drule del_x_paired_dels)

   969 by auto

   970 

   971 lemma del_x_paired_card_less: 

   972   "\<lbrakk>finite ES; (X, rhs) \<in> ES\<rbrakk> \<Longrightarrow> card (del_x_paired ES X) < card ES"

   973 apply (simp add:del_x_paired_def)

   974 apply (drule del_x_paired_subset)

   975 by (auto intro:psubset_card_mono)

   976 

   977 lemma equas_subst_card_less:

   978   "\<lbrakk>finite ES; (Y, yrhs) \<in> ES\<rbrakk> \<Longrightarrow> card (equas_subst ES Y rhs') < card ES"

   979 apply (simp add:equas_subst_def)

   980 apply (frule_tac h = "equas_subst_f Y rhs'" in finite_imageI)

   981 apply (drule_tac f = "equas_subst_f Y rhs'" in Finite_Set.card_image_le)

   982 apply (drule_tac X = Y and xrhs = rhs' in equas_subst_f_del_no_other,erule exE)

   983 by (drule del_x_paired_card_less, auto)

   984 

   985 lemma equas_subst_holds_distinct_rhs:

   986   assumes   dist': "distinct_rhs yrhs'"

   987   and     history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"

   988   and     X_in :  "(X, xrhs) \<in> equas_subst ES Y yrhs'"

   989   shows "distinct_rhs xrhs"

   990 using X_in history

   991 apply (clarsimp simp:equas_subst_def del_x_paired_def)

   992 apply (drule_tac x = a in spec, drule_tac x = b in spec)

   993 apply (simp add:ardenable_def equas_subst_f_def)

   994 by (auto intro:rhs_subst_holds_distinct_rhs simp:dist' split:if_splits)

   995 

   996 lemma r_no_EMPTY_imp_seq_rhs_r_no_EMPTY:

   997   "[] \<notin> L r \<Longrightarrow> no_EMPTY_rhs (seq_rhs_r rhs r)"

   998 by (auto simp:no_EMPTY_rhs_def seq_rhs_r_def lang_seq_def)

   999 

  1000 lemma del_x_paired_holds_no_EMPTY:

  1001   "no_EMPTY_rhs yrhs \<Longrightarrow> no_EMPTY_rhs (del_x_paired yrhs Y)"

  1002 by (auto simp:no_EMPTY_rhs_def del_x_paired_def)

  1003 

  1004 lemma rhs_subst_holds_no_EMPTY:

  1005   "\<lbrakk>no_EMPTY_rhs yrhs; (Y, r) \<in> yrhs; Y \<noteq> {[]}\<rbrakk> \<Longrightarrow> no_EMPTY_rhs (rhs_subst yrhs Y rhs' r)"

  1006 apply (auto simp:rhs_subst_def intro!:no_EMPTY_rhss_imp_merge_no_EMPTY r_no_EMPTY_imp_seq_rhs_r_no_EMPTY del_x_paired_holds_no_EMPTY)

  1007 by (auto simp:no_EMPTY_rhs_def)

  1008 

  1009 lemma equas_subst_holds_no_EMPTY:

  1010   assumes substor: "Y \<noteq> {[]}"

  1011   and history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"

  1012   and X_in:"(X, xrhs) \<in> equas_subst ES Y yrhs'"

  1013   shows "no_EMPTY_rhs xrhs"

  1014 proof-

  1015   from X_in have "\<exists> (Z, zrhs) \<in> ES. (X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)"

  1016     by (auto simp add:equas_subst_def del_x_paired_def)

  1017   then obtain Z zrhs where Z_in: "(Z, zrhs) \<in> ES"

  1018                        and X_Z: "(X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)" by blast

  1019   hence dist_zrhs: "distinct_rhs zrhs" using history

  1020     by (auto simp:ardenable_def)

  1021   show ?thesis

  1022   proof (cases "\<exists> r. (Y, r) \<in> zrhs")

  1023     case True

  1024     then obtain r where Y_in_zrhs: "(Y, r) \<in> zrhs" ..

  1025     hence some: "(SOME r. (Y, r) \<in> zrhs) = r" using Z_in dist_zrhs

  1026       by (auto simp:distinct_rhs_def)

  1027     hence "no_EMPTY_rhs (rhs_subst zrhs Y yrhs' r)"

  1028       using substor Y_in_zrhs history Z_in

  1029       by (rule_tac rhs_subst_holds_no_EMPTY, auto simp:ardenable_def)

  1030     thus ?thesis using X_Z True some

  1031       by (simp add:equas_subst_def equas_subst_f_def)

  1032   next

  1033     case False

  1034     hence "(X, xrhs) = (Z, zrhs)" using Z_in X_Z

  1035       by (simp add:equas_subst_f_def)

  1036     thus ?thesis using history Z_in

  1037       by (auto simp:ardenable_def)

  1038   qed

  1039 qed

  1040 

  1041 lemma equas_subst_f_holds_left_eq_right:

  1042   assumes substor: "Y = L rhs'"

  1043   and     history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> distinct_rhs xrhs \<and> X = L xrhs"

  1044   and       subst: "(X, xrhs) = equas_subst_f Y rhs' (Z, zrhs)"

  1045   and     self_contained: "(Z, zrhs) \<in> ES"

  1046   shows "X = L xrhs"

  1047 proof (cases "\<exists> r. (Y, r) \<in> zrhs")

  1048   case True

  1049   from True obtain r where "(1)":"(Y, r) \<in> zrhs" ..

  1050   show ?thesis

  1051   proof -

  1052     from history self_contained

  1053     have dist: "distinct_rhs zrhs" by auto

  1054     hence "(SOME r. (Y, r) \<in> zrhs) = r" using self_contained "(1)"

  1055       using distinct_rhs_def by (auto intro:some_equality)

  1056     moreover have "L zrhs = L (rhs_subst zrhs Y rhs' r)" using substor dist "(1)" self_contained

  1057       by (rule_tac rhs_subst_prop1, auto simp:distinct_equas_rhs_def)

  1058     ultimately show ?thesis using subst history self_contained

  1059       by (auto simp:equas_subst_f_def split:if_splits)

  1060   qed

  1061 next

  1062   case False

  1063   thus ?thesis using history subst self_contained

  1064     by (auto simp:equas_subst_f_def)

  1065 qed

  1066 

  1067 lemma equas_subst_holds_left_eq_right:

  1068   assumes history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"

  1069   and     substor: "Y = L rhs'"

  1070   and     X_in :  "(X, xrhs) \<in> equas_subst ES Y yrhs'"

  1071   shows "\<forall>X xrhs. (X, xrhs) \<in> equas_subst ES Y rhs' \<longrightarrow> X = L xrhs"

  1072 apply (clarsimp simp add:equas_subst_def del_x_paired_def)

  1073 using substor

  1074 apply (drule_tac equas_subst_f_holds_left_eq_right)

  1075 using history

  1076 by (auto simp:ardenable_def)

  1077 

  1078 lemma equas_subst_holds_ardenable:

  1079   assumes substor: "Y = L yrhs'"

  1080   and history: "\<forall>X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs)"

  1081   and X_in:"(X, xrhs) \<in> equas_subst ES Y yrhs'"

  1082   and dist': "distinct_rhs yrhs'"

  1083   and not_lambda: "Y \<noteq> {[]}"

  1084   shows "ardenable (X, xrhs)"

  1085 proof -

  1086   have "distinct_rhs xrhs" using history X_in dist' 

  1087     by (auto dest:equas_subst_holds_distinct_rhs)

  1088   moreover have "no_EMPTY_rhs xrhs" using history X_in not_lambda

  1089     by (auto intro:equas_subst_holds_no_EMPTY)

  1090   moreover have "X = L xrhs" using history substor X_in

  1091   by (auto dest: equas_subst_holds_left_eq_right simp del:L_rhs.simps)

  1092   ultimately show ?thesis using ardenable_def by simp

  1093 qed

  1094 

  1095 lemma equas_subst_holds_cls_defined:

  1096   assumes         X_in: "(X, xrhs) \<in> equas_subst ES Y yrhs'"

  1097   and           Inv_ES: "Inv X' ES"

  1098   and            subst: "(Y, yrhs) \<in> ES"

  1099   and  cls_holds_but_Y: "rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}"

  1100   shows "rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls (equas_subst ES Y yrhs'))"

  1101 proof-

  1102   have tac: "\<lbrakk> A \<subseteq> B; C \<subseteq> D; E \<subseteq> A \<union> B\<rbrakk> \<Longrightarrow> E \<subseteq> B \<union> D" by auto

  1103   from X_in have "\<exists> (Z, zrhs) \<in> ES. (X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)"

  1104     by (auto simp add:equas_subst_def del_x_paired_def)

  1105   then obtain Z zrhs where Z_in: "(Z, zrhs) \<in> ES"

  1106                        and X_Z: "(X, xrhs) = equas_subst_f Y yrhs' (Z, zrhs)" by blast

  1107   hence "rhs_eq_cls zrhs \<subseteq> insert {[]} (left_eq_cls ES)" using Inv_ES

  1108     by (auto simp:Inv_def)

  1109   moreover have "rhs_eq_cls yrhs' \<subseteq> insert {[]} (left_eq_cls ES) - {Y}" 

  1110     using Inv_ES subst cls_holds_but_Y

  1111     by (auto simp:Inv_def)

  1112   moreover have "rhs_eq_cls xrhs \<subseteq> rhs_eq_cls zrhs \<union> rhs_eq_cls yrhs' - {Y}"

  1113     using X_Z cls_holds_but_Y

  1114     apply (clarsimp simp add:equas_subst_f_def rhs_subst_def split:if_splits)

  1115     by (auto simp:rhs_eq_cls_def merge_rhs_def del_x_paired_def seq_rhs_r_def)

  1116   moreover have "left_eq_cls (equas_subst ES Y yrhs') = left_eq_cls ES - {Y}" using subst

  1117     by (auto simp: left_eq_cls_def equas_subst_def del_x_paired_def equas_subst_f_def

  1118              dest: equas_subst_f_del_no_other

  1119              split: if_splits)

  1120   ultimately show ?thesis by blast

  1121 qed

  1122 

  1123 lemma iteration_step: 

  1124   assumes Inv_ES: "Inv X ES"

  1125   and    not_T: "\<not> TCon ES"

  1126   shows "(\<exists> ES'. Inv X ES' \<and> (card ES', card ES) \<in> less_than)" 

  1127 proof -

  1128   from Inv_ES not_T have another: "\<exists>Y yrhs. (Y, yrhs) \<in> ES \<and> X \<noteq> Y" unfolding Inv_def

  1129     by (clarify, rule_tac exist_another_equa[where X = X], auto)

  1130   then obtain Y yrhs where subst: "(Y, yrhs) \<in> ES" and not_X: " X \<noteq> Y" by blast

  1131   show ?thesis (is "\<exists> ES'. ?P ES'")

  1132   proof (cases "Y = {[]}") 

  1133     case True

  1134       --"in this situation, we pick a \"\<lambda>\" equation, thus directly remove it from the equation-system"

  1135     have "?P (ES - {(Y, yrhs)})"