2   imports "Main" 

     2   imports "Main" 

     3 begin

     3 begin

     4 

     4 

     5 text {* sequential composition of languages *}

     5 text {* sequential composition of languages *}

     6 

     6 

   230 | STAR rexp

   230 | STAR rexp

   231 

   231 

   232 

   232 

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

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

   234 

   234 

   235 fun

   237 fun

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

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

   237 where

   239 where

   249 

   247 

   250 definition

   248 definition

   251   Ls :: "rexp set \<Rightarrow> string set"

   249   Ls :: "rexp set \<Rightarrow> string set"

   252 where

   250 where

   253   "Ls R = (\<Union>r\<in>R. (L r))"

   251   "Ls R = (\<Union>r\<in>R. (L r))"

   865 definition 

   863 definition 

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

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

   867 where

   865 where

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

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

   869 

   867 

   879 

   874 

   880 definition 

   875 definition 

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

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

   882 where

   877 where

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

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

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

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

   927 

   922 

   928 lemma seq_rhs_r_prop1:

   923 lemma seq_rhs_r_prop1:

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

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

   930 apply (rule set_ext, rule iffI)

   925 apply (rule set_ext, rule iffI)

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

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

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

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

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

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

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

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

   936 apply (rule conjI)

   931 apply (rule conjI)

   939 apply (simp add:lang_seq_def)

   934 apply (simp add:lang_seq_def)

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

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

   941 

   936 

   942 lemma del_x_paired_prop1:  

   937 lemma del_x_paired_prop1:  

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

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

   945 apply (rule set_ext, rule iffI, simp)

   940 apply (rule set_ext, rule iffI, simp)

   946 apply (erule disjE, rule_tac x = X in exI, rule_tac x = r in exI, simp)

   941 apply (erule disjE, rule_tac x = X in exI, rule_tac x = r in exI, simp)

   947 apply (clarify, rule_tac x = Xa in exI, rule_tac x = ra in exI, simp)

   942 apply (clarify, rule_tac x = Xa in exI, rule_tac x = ra in exI, simp)

   948 apply (clarsimp, drule_tac x = Xa in spec, drule_tac x = ra in spec)

   943 apply (clarsimp, drule_tac x = Xa in spec, drule_tac x = ra in spec)

   949 apply (auto simp:distinct_rhs_def)

   944 apply (auto simp:distinct_rhs_def)

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

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

   992     by (auto simp:no_EMPTY_rhs_def)

   987     by (auto simp:no_EMPTY_rhs_def)

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

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

   994     by (rule ardens_revised)

   989     by (rule ardens_revised)

   995   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

   990   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

   997   show ?thesis

   992   show ?thesis

   998   proof

   993   proof

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

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

  1000     proof

   995     proof

  1001       fix x

   996       fix x

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

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

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

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

  1005     qed

  1000     qed

  1006   next

  1001   next

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

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

  1008     proof

  1003     proof

  1009       fix x

  1004       fix x

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

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

  1011       show "x \<in> X" 

  1006       show "x \<in> X" 

  1013     qed

  1008     qed

  1014   qed

  1009   qed

  1015 qed

  1010 qed

  1016 

  1011 

  1017 text {* merge_rhs {(X1, r1), (x2, r2}, (x4, r4), \<dots>} {(x1, r1'), (x3, r3'), \<dots>} = {(x1, ALT r1 r1'}, (x2, r2), (x3, r3'), (x4, r4), \<dots>} *}  

  1012 text {* merge_rhs {(X1, r1), (x2, r2}, (x4, r4), \<dots>} {(x1, r1'), (x3, r3'), \<dots>} = {(x1, ALT r1 r1'}, (x2, r2), (x3, r3'), (x4, r4), \<dots>} *}  

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

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

  1055 by (auto simp:lang_seq_def)

  1050 by (auto simp:lang_seq_def)

  1056 

  1051 

  1057 lemma merge_rhs_prop1:

  1052 lemma merge_rhs_prop1:

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

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

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

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

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

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

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

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

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

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

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

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

  1097 

  1092 

  1098 lemma seq_rhs_r_prop0:

  1093 lemma seq_rhs_r_prop0:

  1099   assumes l_eq_r: "X = L xrhs"

  1094   assumes l_eq_r: "X = L xrhs"

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

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

  1101 using l_eq_r

  1096 using l_eq_r

  1103 

  1098 

  1104 lemma rhs_subst_prop1:

  1099 lemma rhs_subst_prop1:

  1105   assumes l_eq_r: "X = L xrhs"

  1100   assumes l_eq_r: "X = L xrhs"

  1106   and     dist:  "distinct_rhs rhs"

  1101   and     dist:  "distinct_rhs rhs"

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

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

  1109 using l_eq_r 

  1104 using l_eq_r 

  1111 using dist

  1106 using dist

  1114 

  1108 

  1115 lemma del_x_paired_holds_distinct_rhs:

  1109 lemma del_x_paired_holds_distinct_rhs:

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

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

  1117 by (auto simp:distinct_rhs_def del_x_paired_def)

  1111 by (auto simp:distinct_rhs_def del_x_paired_def)

  1118 

  1112 

  1160 text {* 

  1154 text {* 

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

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

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

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

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

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

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

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

  1166   

  1160   

  1167 *}

  1161 *}

  1168 lemma wf_iter [rule_format]: 

  1162 lemma wf_iter [rule_format]: 

  1169   fixes f

  1163   fixes f

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

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

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

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

  1252   shows "X = L xrhs"    

  1246   shows "X = L xrhs"    

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

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

  1254   case True

  1248   case True

  1255   thus ?thesis using X_in_equas 

  1249   thus ?thesis using X_in_equas 

  1257 next

  1251 next

  1258   case False 

  1252   case False 

  1259   show ?thesis

  1253   show ?thesis

  1260   proof 

  1254   proof 

  1261     show "X \<subseteq> L xrhs"

  1255     show "X \<subseteq> L xrhs"

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

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

  1265       show "x \<in> L xrhs"          

  1259       show "x \<in> L xrhs"          

  1266       proof (cases "x = []")

  1260       proof (cases "x = []")

  1267         assume empty: "x = []"

  1261         assume empty: "x = []"

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

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

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

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

  1272       next

  1266       next

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

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

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

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

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

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

  1276         moreover have "\<And> Y. \<lbrakk>Y \<in> UNIV Quo Lang; Y-c\<rightarrow>X; clist \<in> Y\<rbrakk>\<Longrightarrow> [c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})"

  1270         moreover have "\<And> Y. \<lbrakk>Y \<in> UNIV Quo Lang; Y-c\<rightarrow>X; clist \<in> Y\<rbrakk>\<Longrightarrow> [c] \<in> L (folds ALT NULL {CHAR c |c. Y-c\<rightarrow>X})"

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

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

  1284             by (auto simp :fold_alt_null_eqs)

  1278             by (auto simp :fold_alt_null_eqs)

  1285         qed

  1279         qed

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

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

  1287           using X_in_equas False not_empty "(1)" decom

  1281           using X_in_equas False not_empty "(1)" decom

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

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

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

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

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

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

  1294       qed

  1288       qed

  1295     qed

  1289     qed

  1296   next

  1290   next

  1297     show "L xrhs \<subseteq> X"

  1291     show "L xrhs \<subseteq> X"

  1298     proof

  1292     proof

  1302         using finite_charset_rS

  1296         using finite_charset_rS

  1303         by (auto simp:CT_def lang_seq_def fold_alt_null_eqs)

  1297         by (auto simp:CT_def lang_seq_def fold_alt_null_eqs)

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

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

  1305         by (simp add:empty_rhs_def split:if_splits)

  1299         by (simp add:empty_rhs_def split:if_splits)

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

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

  1308     qed

  1302     qed

  1309   qed

  1303   qed

  1310 qed

  1304 qed

  1311 

  1305 

  1312 lemma finite_CT_chars:

  1306 lemma finite_CT_chars:

  1321 done

  1315 done

  1322 

  1316 

  1323 lemma init_ES_satisfy_ardenable:

  1317 lemma init_ES_satisfy_ardenable:

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

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

  1325   unfolding ardenable_def

  1319   unfolding ardenable_def

  1327 

  1321 

  1328 lemma init_ES_satisfy_Inv:

  1322 lemma init_ES_satisfy_Inv:

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

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

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

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

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

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

  1461 

  1455 

  1462 lemma del_x_paired_del_only_x: 

  1456 lemma del_x_paired_del_only_x: 

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

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

  1464 by (auto simp:del_x_paired_def)

  1458 by (auto simp:del_x_paired_def)

  1465 

  1459 

  1470 lemma equas_subst_del_no_other:

  1460 lemma equas_subst_del_no_other:

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

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

  1472 unfolding equas_subst_def

  1462 unfolding equas_subst_def

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

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

  1474 by (erule exE, drule del_x_paired_del_only_x, auto)

  1464 by (erule exE, drule del_x_paired_del_only_x, auto)

  1605   have "distinct_rhs xrhs" using history X_in dist' 

  1595   have "distinct_rhs xrhs" using history X_in dist' 

  1606     by (auto dest:equas_subst_holds_distinct_rhs)

  1596     by (auto dest:equas_subst_holds_distinct_rhs)

  1607   moreover have "no_EMPTY_rhs xrhs" using history X_in not_lambda

  1597   moreover have "no_EMPTY_rhs xrhs" using history X_in not_lambda

  1608     by (auto intro:equas_subst_holds_no_EMPTY)

  1598     by (auto intro:equas_subst_holds_no_EMPTY)

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

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

  1611   ultimately show ?thesis using ardenable_def by simp

  1601   ultimately show ?thesis using ardenable_def by simp

  1612 qed

  1602 qed

  1613 

  1603 

  1614 lemma equas_subst_holds_cls_defined:

  1604 lemma equas_subst_holds_cls_defined:

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

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

  1662     thus ?thesis by blast

  1652     thus ?thesis by blast

  1663   next

  1653   next

  1664     case False

  1654     case False

  1665       --"in this situation, we pick a equation and using ardenable to get a rhs without itself in it, then use equas_subst to form a new equation-system"

  1655       --"in this situation, we pick a equation and using ardenable to get a rhs without itself in it, then use equas_subst to form a new equation-system"

  1666     hence "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" using subst Inv_ES

  1656     hence "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" using subst Inv_ES

  1668     then obtain yrhs' where Y'_l_eq_r: "Y = L yrhs'"

  1658     then obtain yrhs' where Y'_l_eq_r: "Y = L yrhs'"

  1669       and dist_Y': "distinct_rhs yrhs'"

  1659       and dist_Y': "distinct_rhs yrhs'"

  1670       and cls_holds_but_Y: "rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" by blast

  1660       and cls_holds_but_Y: "rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" by blast

  1671     hence "?P (equas_subst ES Y yrhs')"

  1661     hence "?P (equas_subst ES Y yrhs')"

  1672     proof -

  1662     proof -

  1748     by (simp add:Inv_def)

  1738     by (simp add:Inv_def)

  1749   

  1739   

  1750   from X_ardenable have X_l_eq_r: "X = L rhs"

  1740   from X_ardenable have X_l_eq_r: "X = L rhs"

  1751     by (simp add:ardenable_def)

  1741     by (simp add:ardenable_def)

  1752   hence rhs_not_empty: "rhs \<noteq> {}" using Inv_ES' ES'_single_equa

  1742   hence rhs_not_empty: "rhs \<noteq> {}" using Inv_ES' ES'_single_equa

  1754   have rhs_eq_cls: "rhs_eq_cls rhs \<subseteq> {X, {[]}}"

  1744   have rhs_eq_cls: "rhs_eq_cls rhs \<subseteq> {X, {[]}}"

  1755     using Inv_ES' ES'_single_equa

  1745     using Inv_ES' ES'_single_equa

  1756     by (auto simp:Inv_def ardenable_def left_eq_cls_def)

  1746     by (auto simp:Inv_def ardenable_def left_eq_cls_def)

  1757   have X_not_empty: "X \<noteq> {}" using Inv_ES' ES'_single_equa

  1747   have X_not_empty: "X \<noteq> {}" using Inv_ES' ES'_single_equa

  1758     by (auto simp:Inv_def)    

  1748     by (auto simp:Inv_def)    

  1759   show ?thesis

  1749   show ?thesis

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

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

  1761     case True

  1751     case True

  1763     thus ?thesis by blast

  1753     thus ?thesis by blast

  1764   next

  1754   next

  1765     case False with  X_ardenable

  1755     case False with  X_ardenable

  1766     have "\<exists> rhs'. X = L rhs' \<and> rhs_eq_cls rhs' = rhs_eq_cls rhs - {X} \<and> distinct_rhs rhs'"

  1756     have "\<exists> rhs'. X = L rhs' \<and> rhs_eq_cls rhs' = rhs_eq_cls rhs - {X} \<and> distinct_rhs rhs'"

  1767       by (drule_tac ardenable_prop, auto)

  1757       by (drule_tac ardenable_prop, auto)

  1769       and rhs'_eq_cls: "rhs_eq_cls rhs' = rhs_eq_cls rhs - {X}" 

  1759       and rhs'_eq_cls: "rhs_eq_cls rhs' = rhs_eq_cls rhs - {X}" 

  1770       and rhs'_dist : "distinct_rhs rhs'" by blast

  1760       and rhs'_dist : "distinct_rhs rhs'" by blast

  1771     have "rhs_eq_cls rhs' \<subseteq> {{[]}}" using rhs_eq_cls False rhs'_eq_cls rhs_not_empty 

  1761     have "rhs_eq_cls rhs' \<subseteq> {{[]}}" using rhs_eq_cls False rhs'_eq_cls rhs_not_empty 

  1772       by blast

  1762       by blast

  1773     hence "rhs_eq_cls rhs' = {{[]}}" using X_not_empty X_eq_rhs'

  1763     hence "rhs_eq_cls rhs' = {{[]}}" using X_not_empty X_eq_rhs'

  1775     hence "\<exists> r. rhs' = {({[]}, r)}" using rhs'_dist

  1765     hence "\<exists> r. rhs' = {({[]}, r)}" using rhs'_dist

  1776       by (auto intro:rhs_aux simp:rhs_eq_cls_def)

  1766       by (auto intro:rhs_aux simp:rhs_eq_cls_def)

  1777     then obtain r where "rhs' = {({[]}, r)}" ..

  1767     then obtain r where "rhs' = {({[]}, r)}" ..

  1779     thus ?thesis by blast     

  1769     thus ?thesis by blast     

  1780   qed

  1770   qed

  1781 qed

  1771 qed

  1782 

  1772 

  1783 theorem myhill_nerode: 

  1773 theorem myhill_nerode: 

  1811       by (clarsimp simp:fold_alt_null_eqs)

  1801       by (clarsimp simp:fold_alt_null_eqs)

  1812   qed

  1802   qed

  1813   thus ?thesis by blast

  1803   thus ?thesis by blast

  1814 qed 

  1804 qed 

  1815   

  1805