1 theory My

     2 imports Main Infinite_Set

     3 begin

     4 

     5 

     6 definition

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

     8 where 

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

    10 

    11 inductive_set

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

    13   for L :: "string set"

    14 where

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

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

    17 

    18 lemma lang_star_cases:

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

    20 unfolding Seq_def

    21 by (auto) (metis Star.simps)

    22 

    23 lemma lang_star_cases2:

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

    25 sorry

    26 

    27 

    28 theorem ardens_revised:

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

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

    31 proof

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

    33   have "A\<star> =  {[]} \<union> A\<star> ;; A" sorry

    34   then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)" unfolding Seq_def by simp

    35   also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"  unfolding Seq_def by auto

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

    37     by (auto) (metis append_assoc)+

    38   finally show "X = X ;; A \<union> B" using eq by auto

    39 next

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

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

    42   show "X = B ;; A\<star>" sorry

    43 qed

    44 

    45 datatype rexp =

    46   NULL

    47 | EMPTY

    48 | CHAR char

    49 | SEQ rexp rexp

    50 | ALT rexp rexp

    51 | STAR rexp

    52 

    53 fun

    54   Sem :: "rexp \<Rightarrow> string set" ("\<lparr>_\<rparr>" [0] 1000)

    55 where

    56     "\<lparr>NULL\<rparr> = {}"

    57   | "\<lparr>EMPTY\<rparr> = {[]}"

    58   | "\<lparr>CHAR c\<rparr> = {[c]}"

    59   | "\<lparr>SEQ r1 r2\<rparr> = \<lparr>r1\<rparr> ;; \<lparr>r2\<rparr>"

    60   | "\<lparr>ALT r1 r2\<rparr> = \<lparr>r1\<rparr> \<union> \<lparr>r2\<rparr>"

    61   | "\<lparr>STAR r\<rparr> = \<lparr>r\<rparr>\<star>"

    62 

    63 definition 

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

    65 where

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

    67 

    68 lemma folds_simp_null [simp]:

    69   "finite rs \<Longrightarrow> x \<in> \<lparr>folds ALT NULL rs\<rparr> \<longleftrightarrow> (\<exists>r \<in> rs. x \<in> \<lparr>r\<rparr>)"

    70 apply (simp add: folds_def)

    71 apply (rule someI2_ex)

    72 apply (erule finite_imp_fold_graph)

    73 apply (erule fold_graph.induct)

    74 apply (auto)

    75 done

    76 

    77 lemma folds_simp_empty [simp]:

    78   "finite rs \<Longrightarrow> x \<in> \<lparr>folds ALT EMPTY rs\<rparr> \<longleftrightarrow> (\<exists>r \<in> rs. x \<in> \<lparr>r\<rparr>) \<or> x = []"

    79 apply (simp add: folds_def)

    80 apply (rule someI2_ex)

    81 apply (erule finite_imp_fold_graph)

    82 apply (erule fold_graph.induct)

    83 apply (auto)

    84 done

    85 

    86 lemma [simp]:

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

    88 by simp

    89 

    90 definition

    91   str_eq ("_ \<approx>_ _")

    92 where

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

    94 

    95 definition

    96   str_eq_rel ("\<approx>_")

    97 where

    98   "\<approx>Lang \<equiv> {(x, y). x \<approx>Lang y}"

    99 

   100 definition

   101   final :: "string set \<Rightarrow> string set \<Rightarrow> bool"

   102 where

   103   "final X Lang \<equiv> (X \<in> UNIV // \<approx>Lang) \<and> (\<forall>s \<in> X. s \<in> Lang)"

   104 

   105 lemma lang_is_union_of_finals: 

   106   "Lang = \<Union> {X. final X Lang}"

   107 proof -

   108   have  "Lang \<subseteq> \<Union> {X. final X Lang}"

   109     unfolding final_def

   110     unfolding quotient_def Image_def

   111     unfolding str_eq_rel_def

   112     apply(simp)

   113     apply(auto)

   114     apply(rule_tac x="(\<approx>Lang) `` {x}" in exI)

   115     unfolding Image_def

   116     unfolding str_eq_rel_def

   117     apply(auto)

   118     unfolding str_eq_def

   119     apply(auto)

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

   121     apply(simp)

   122     done

   123   moreover

   124   have "\<Union>{X. final X Lang} \<subseteq> Lang" 

   125     unfolding final_def by auto

   126   ultimately 

   127   show "Lang = \<Union> {X. final X Lang}"

   128     by blast

   129 qed

   130 

   131 lemma all_rexp:

   132   "\<lbrakk>finite (UNIV // \<approx>Lang); X \<in> (UNIV // \<approx>Lang)\<rbrakk> \<Longrightarrow> \<exists>r. X = \<lparr>r\<rparr>"

   133 sorry

   134 

   135 lemma final_rexp:

   136   "\<lbrakk>finite (UNIV // (\<approx>Lang)); final X Lang\<rbrakk> \<Longrightarrow> \<exists>r. X = \<lparr>r\<rparr>"

   137 unfolding final_def

   138 using all_rexp by blast

   139 

   140 lemma finite_f_one_to_one:

   141   assumes "finite B"

   142   and "\<forall>x \<in> B. \<exists>y. f y = x"

   143   shows "\<exists>rs. finite rs \<and> (B = {f y | y . y \<in> rs})"

   144 using assms

   145 by (induct) (auto)

   146 

   147 lemma finite_final:

   148   assumes "finite (UNIV // (\<approx>Lang))"

   149   shows "finite {X. final X Lang}"

   150 using assms

   151 proof -

   152   have "{X. final X Lang} \<subseteq> (UNIV // (\<approx>Lang))"

   153     unfolding final_def by auto

   154   with assms show "finite {X. final X Lang}" 

   155     using finite_subset by auto

   156 qed

   157 

   158 lemma finite_regular_aux:

   159   fixes Lang :: "string set"

   160   assumes "finite (UNIV // (\<approx>Lang))"

   161   shows "\<exists>rs. Lang = \<lparr>folds ALT NULL rs\<rparr>"

   162 apply(subst lang_is_union_of_finals)

   163 using assms

   164 apply -

   165 apply(drule finite_final)

   166 apply(drule_tac f="Sem" in finite_f_one_to_one)

   167 apply(clarify)

   168 apply(drule final_rexp[OF assms])

   169 apply(auto)[1]

   170 apply(clarify)

   171 apply(rule_tac x="rs" in exI)

   172 apply(simp)

   173 apply(rule set_eqI)

   174 apply(auto)

   175 done

   176 

   177 lemma finite_regular:

   178   fixes Lang :: "string set"

   179   assumes "finite (UNIV // (\<approx>Lang))"

   180   shows "\<exists>r. Lang =  \<lparr>r\<rparr>"

   181 using assms finite_regular_aux

   182 by auto

   183 

   184 

   185 

   186 section {* other direction *}

   187 

   188 

   189 lemma inj_image_lang:

   190   fixes f::"string \<Rightarrow> 'a"

   191   assumes str_inj: "\<And>x y. f x = f y \<Longrightarrow> x \<approx>Lang y"

   192   shows "inj_on (image f) (UNIV // (\<approx>Lang))"

   193 proof - 

   194   { fix x y::string

   195     assume eq_tag: "f ` {z. x \<approx>Lang z} = f ` {z. y \<approx>Lang z}"

   196     moreover

   197     have "{z. x \<approx>Lang z} \<noteq> {}" unfolding str_eq_def by auto

   198     ultimately obtain a b where "x \<approx>Lang a" "y \<approx>Lang b" "f a = f b" by blast

   199     then have "x \<approx>Lang a" "y \<approx>Lang b" "a \<approx>Lang b" using str_inj by auto

   200     then have "x \<approx>Lang y" unfolding str_eq_def by simp 

   201     then have "{z. x \<approx>Lang z} = {z. y \<approx>Lang z}" unfolding str_eq_def by simp

   202   }

   203   then have "\<forall>x\<in>UNIV // \<approx>Lang. \<forall>y\<in>UNIV // \<approx>Lang. f ` x = f ` y \<longrightarrow> x = y"

   204     unfolding quotient_def Image_def str_eq_rel_def by simp

   205   then show "inj_on (image f) (UNIV // (\<approx>Lang))"

   206     unfolding inj_on_def by simp

   207 qed

   208 

   209 

   210 lemma finite_range_image: 

   211   assumes fin: "finite (range f)"

   212   shows "finite ((image f) ` X)"

   213 proof -

   214   from fin have "finite (Pow (f ` UNIV))" by auto

   215   moreover

   216   have "(image f) ` X \<subseteq> Pow (f ` UNIV)" by auto

   217   ultimately show "finite ((image f) ` X)" using finite_subset by auto

   218 qed

   219 

   220 definition 

   221   tag1 :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)"

   222 where

   223   "tag1 L\<^isub>1 L\<^isub>2 \<equiv> \<lambda>x. ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})"

   224 

   225 lemma tag1_range_finite:

   226   assumes finite1: "finite (UNIV // \<approx>L\<^isub>1)"

   227   and finite2: "finite (UNIV // \<approx>L\<^isub>2)"

   228   shows "finite (range (tag1 L\<^isub>1 L\<^isub>2))"

   229 proof -

   230   have "finite (UNIV // \<approx>L\<^isub>1 \<times> UNIV // \<approx>L\<^isub>2)" using finite1 finite2 by auto

   231   moreover

   232   have "range (tag1 L\<^isub>1 L\<^isub>2) \<subseteq> (UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)"

   233     unfolding tag1_def quotient_def by auto

   234   ultimately show "finite (range (tag1 L\<^isub>1 L\<^isub>2))" 

   235     using finite_subset by blast

   236 qed

   237 

   238 lemma tag1_inj:

   239   "tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y"

   240 unfolding tag1_def Image_def str_eq_rel_def str_eq_def

   241 by auto

   242 

   243 lemma quot_alt_cu:

   244   fixes L\<^isub>1 L\<^isub>2::"string set"

   245   assumes fin1: "finite (UNIV // \<approx>L\<^isub>1)"

   246   and fin2: "finite (UNIV // \<approx>L\<^isub>2)"

   247   shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"

   248 proof -

   249   have "finite (range (tag1 L\<^isub>1 L\<^isub>2))" 

   250     using fin1 fin2 tag1_range_finite by simp

   251   then have "finite (image (tag1 L\<^isub>1 L\<^isub>2) ` (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2)))" 

   252     using finite_range_image by blast

   253   moreover 

   254   have "\<And>x y. tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y" 

   255     using tag1_inj by simp

   256   then have "inj_on (image (tag1 L\<^isub>1 L\<^isub>2)) (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" 

   257     using inj_image_lang by blast

   258   ultimately 

   259   show "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" by (rule finite_imageD)

   260 qed

   261 

   262 

   263 section {* finite \<Rightarrow> regular *}

   264 

   265 definition

   266   transitions :: "string set \<Rightarrow> string set \<Rightarrow> rexp set" ("_\<Turnstile>\<Rightarrow>_")

   267 where

   268   "Y \<Turnstile>\<Rightarrow> X \<equiv> {CHAR c | c. Y ;; {[c]} \<subseteq> X}"

   269 

   270 definition

   271   transitions_rexp ("_ \<turnstile>\<rightarrow> _")

   272 where

   273   "Y \<turnstile>\<rightarrow> X \<equiv> if [] \<in> X then folds ALT EMPTY (Y \<Turnstile>\<Rightarrow>X) else folds ALT NULL (Y \<Turnstile>\<Rightarrow>X)"

   274 

   275 definition

   276   "rhs CS X \<equiv> if X = {[]} then {({[]}, EMPTY)} else {(Y, Y \<turnstile>\<rightarrow>X) | Y. Y \<in> CS}"

   277 

   278 definition

   279   "rhs_sem CS X \<equiv> \<Union> {(Y;; \<lparr>r\<rparr>) | Y r . (Y, r) \<in> rhs CS X}"

   280 

   281 definition

   282   "eqs CS \<equiv> (\<Union>X \<in> CS. {(X, rhs CS X)})"

   283 

   284 definition

   285   "eqs_sem CS \<equiv> (\<Union>X \<in> CS. {(X, rhs_sem CS X)})"

   286 

   287 lemma [simp]:

   288   shows "finite (Y \<Turnstile>\<Rightarrow> X)"

   289 unfolding transitions_def

   290 by auto

   291 

   292 

   293 lemma defined_by_str:

   294   assumes "s \<in> X" 

   295   and "X \<in> UNIV // (\<approx>Lang)"

   296   shows "X = (\<approx>Lang) `` {s}"

   297 using assms

   298 unfolding quotient_def Image_def

   299 unfolding str_eq_rel_def str_eq_def

   300 by auto

   301 

   302 lemma every_eqclass_has_transition:

   303   assumes has_str: "s @ [c] \<in> X"

   304   and     in_CS:   "X \<in> UNIV // (\<approx>Lang)"

   305   obtains Y where "Y \<in> UNIV // (\<approx>Lang)" and "Y ;; {[c]} \<subseteq> X" and "s \<in> Y"

   306 proof -

   307   def Y \<equiv> "(\<approx>Lang) `` {s}"

   308   have "Y \<in> UNIV // (\<approx>Lang)" 

   309     unfolding Y_def quotient_def by auto

   310   moreover

   311   have "X = (\<approx>Lang) `` {s @ [c]}" 

   312     using has_str in_CS defined_by_str by blast

   313   then have "Y ;; {[c]} \<subseteq> X" 

   314     unfolding Y_def Image_def Seq_def

   315     unfolding str_eq_rel_def

   316     by (auto) (simp add: str_eq_def)

   317   moreover

   318   have "s \<in> Y" unfolding Y_def 

   319     unfolding Image_def str_eq_rel_def str_eq_def by simp

   320   (*moreover 

   321   have "True" by simp FIXME *) 

   322   ultimately show thesis by (blast intro: that)

   323 qed

   324 

   325 lemma test:

   326   assumes "[] \<in> X"

   327   shows "[] \<in> \<lparr>Y \<turnstile>\<rightarrow> X\<rparr>"

   328 using assms

   329 by (simp add: transitions_rexp_def)

   330 

   331 lemma rhs_sem:

   332   assumes "X \<in> (UNIV // (\<approx>Lang))"

   333   shows "X \<subseteq> rhs_sem (UNIV // (\<approx>Lang)) X"

   334 apply(case_tac "X = {[]}")

   335 apply(simp)

   336 apply(simp add: rhs_sem_def rhs_def Seq_def)

   337 apply(rule subsetI)

   338 apply(case_tac "x = []")

   339 apply(simp add: rhs_sem_def rhs_def)

   340 apply(rule_tac x = "X" in exI)

   341 apply(simp)

   342 apply(rule_tac x = "X" in exI)

   343 apply(simp add: assms)

   344 apply(simp add: transitions_rexp_def)

   345 oops

   346 

   347 

   348 (*

   349 fun

   350   power :: "string \<Rightarrow> nat \<Rightarrow> string" (infixr "\<Up>" 100)

   351 where

   352   "s \<Up> 0 = s"

   353 | "s \<Up> (Suc n) = s @ (s \<Up> n)"

   354 

   355 definition 

   356  "Lone = {(''0'' \<Up> n) @ (''1'' \<Up> n) | n. True }"

   357 

   358 lemma

   359   "infinite (UNIV // (\<approx>Lone))"

   360 unfolding infinite_iff_countable_subset

   361 apply(rule_tac x="\<lambda>n. {(''0'' \<Up> n) @ (''1'' \<Up> i) | i. i \<in> {..n} }" in exI)

   362 apply(auto)

   363 prefer 2

   364 unfolding Lone_def

   365 unfolding quotient_def

   366 unfolding Image_def

   367 apply(simp)

   368 unfolding str_eq_rel_def

   369 unfolding str_eq_def

   370 apply(auto)

   371 apply(rule_tac x="''0'' \<Up> n" in exI)

   372 apply(auto)

   373 unfolding infinite_nat_iff_unbounded

   374 unfolding Lone_def

   375 *)

   376 

   377 

   378 

   379 text {* Derivatives *}

   380 

   381 definition

   382   DERS :: "string \<Rightarrow> string set \<Rightarrow> string set"

   383 where

   384   "DERS s L \<equiv> {s'. s @ s' \<in> L}"

   385 

   386 lemma

   387   shows "x \<approx>L y \<longleftrightarrow> DERS x L = DERS y L"

   388 unfolding DERS_def str_eq_def

   389 by auto