1 theory Closure2

     2 imports Closures

     3 begin

     4 

     5 inductive emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _")

     6 where

     7    emb0 [Pure.intro]: "emb [] bs"

     8  | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)"

     9  | emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)"

    10 

    11 lemma emb_refl:

    12   shows "x \<preceq> x"

    13 apply(induct x)

    14 apply(auto intro: emb.intros)

    15 done

    16 

    17 lemma emb_right:

    18   assumes a: "x \<preceq> y"

    19   shows "x \<preceq> y @ y'"

    20 using a

    21 apply(induct arbitrary: y')

    22 apply(auto intro: emb.intros)

    23 done

    24 

    25 lemma emb_left:

    26   assumes a: "x \<preceq> y"

    27   shows "x \<preceq> y' @ y"

    28 using a

    29 apply(induct y')

    30 apply(auto intro: emb.intros)

    31 done

    32 

    33 lemma emb_appendI:

    34   assumes a: "x \<preceq> x'"

    35   and     b: "y \<preceq> y'"

    36   shows "x @ y \<preceq> x' @ y'"

    37 using a b

    38 apply(induct)

    39 apply(auto intro: emb.intros emb_left)

    40 done

    41 

    42 lemma emb_append:

    43   assumes a: "x \<preceq> y1 @ y2"

    44   shows "\<exists>x1 x2. x = x1 @ x2 \<and> x1 \<preceq> y1 \<and> x2 \<preceq> y2"

    45 using a

    46 apply(induct x y\<equiv>"y1 @ y2" arbitrary: y1 y2)

    47 apply(auto intro: emb0)[1]

    48 apply(simp add: Cons_eq_append_conv)

    49 apply(auto)[1]

    50 apply(rule_tac x="[]" in exI)

    51 apply(rule_tac x="as" in exI)

    52 apply(auto intro: emb.intros)[1]

    53 apply(simp add: append_eq_append_conv2)

    54 apply(drule_tac x="ys'" in meta_spec)

    55 apply(drule_tac x="y2" in meta_spec)

    56 apply(auto)[1]

    57 apply(rule_tac x="x1" in exI)

    58 apply(rule_tac x="x2" in exI)

    59 apply(auto intro: emb.intros)[1]

    60 apply(subst (asm) Cons_eq_append_conv)

    61 apply(auto)[1]

    62 apply(rule_tac x="[]" in exI)

    63 apply(rule_tac x="a # as" in exI)

    64 apply(auto intro: emb.intros)[1]

    65 apply(simp add: append_eq_append_conv2)

    66 apply(drule_tac x="ys'" in meta_spec)

    67 apply(drule_tac x="y2" in meta_spec)

    68 apply(auto)[1]

    69 apply(rule_tac x="a # x1" in exI)

    70 apply(rule_tac x="x2" in exI)

    71 apply(auto intro: emb.intros)[1]

    72 done

    73 

    74 

    75 definition

    76  "SUBSEQ A \<equiv> {x. \<exists>y \<in> A. x \<preceq> y}"

    77 

    78 definition

    79  "SUPSEQ A \<equiv> (- SUBSEQ A) \<union> A"

    80 

    81 lemma [simp]:

    82   "SUBSEQ {} = {}"

    83 unfolding SUBSEQ_def

    84 by auto

    85 

    86 lemma [simp]:

    87   "SUBSEQ {[]} = {[]}"

    88 unfolding SUBSEQ_def

    89 apply(auto)

    90 apply(erule emb.cases)

    91 apply(auto)[3]

    92 apply(rule emb0)

    93 done

    94 

    95 lemma SUBSEQ_atom [simp]:

    96   "SUBSEQ {[a]} = {[], [a]}"

    97 apply(auto simp add: SUBSEQ_def)

    98 apply(erule emb.cases)

    99 apply(auto)[3]

   100 apply(erule emb.cases)

   101 apply(auto)[3]

   102 apply(erule emb.cases)

   103 apply(auto)[3]

   104 apply(rule emb0)

   105 apply(rule emb2)

   106 apply(rule emb0)

   107 done

   108 

   109 lemma SUBSEQ_union [simp]:

   110   "SUBSEQ (A \<union> B) = SUBSEQ A \<union> SUBSEQ B"

   111 unfolding SUBSEQ_def by auto

   112 

   113 lemma SUBSEQ_Union [simp]:

   114   fixes A :: "nat \<Rightarrow> 'a lang"

   115   shows "SUBSEQ (\<Union>n. (A n)) = (\<Union>n. (SUBSEQ  (A n)))"

   116 unfolding SUBSEQ_def image_def by auto

   117 

   118 lemma SUBSEQ_conc1:

   119   "\<lbrakk>x \<in> SUBSEQ A; y \<in> SUBSEQ B\<rbrakk> \<Longrightarrow> x @ y \<in> SUBSEQ (A \<cdot> B)"

   120 unfolding SUBSEQ_def 

   121 apply(auto)

   122 apply(rule_tac x="xa @ xaa" in bexI)

   123 apply(rule emb_appendI)

   124 apply(simp_all)

   125 done

   126 

   127 lemma SUBSEQ_conc2:

   128   "x \<in> SUBSEQ (A \<cdot> B) \<Longrightarrow> x \<in> (SUBSEQ A) \<cdot> (SUBSEQ B)"

   129 unfolding SUBSEQ_def conc_def 

   130 apply(auto)

   131 apply(drule emb_append)

   132 apply(auto)

   133 done

   134 

   135 lemma SUBSEQ_conc [simp]:

   136   "SUBSEQ (A \<cdot> B) = SUBSEQ A \<cdot> SUBSEQ B"

   137 apply(auto)

   138 apply(simp add: SUBSEQ_conc2)

   139 apply(subst (asm) conc_def)

   140 apply(auto simp add: SUBSEQ_conc1)

   141 done

   142 

   143 lemma SUBSEQ_star1:

   144   assumes a: "x \<in> (SUBSEQ A)\<star>" 

   145   shows "x \<in> SUBSEQ (A\<star>)"

   146 using a

   147 apply(induct rule: star_induct)

   148 apply(simp add: SUBSEQ_def)

   149 apply(rule_tac x="[]" in bexI)

   150 apply(rule emb0)

   151 apply(auto)[1]

   152 apply(drule SUBSEQ_conc1)

   153 apply(assumption)

   154 apply(subst star_unfold_left)

   155 apply(simp only: SUBSEQ_union)

   156 apply(simp)

   157 done

   158 

   159 lemma SUBSEQ_star2_aux:

   160   assumes a: "x \<in> SUBSEQ (A ^^ n)" 

   161   shows "x \<in> (SUBSEQ A)\<star>"

   162 using a

   163 apply(induct n arbitrary: x)

   164 apply(simp)

   165 apply(simp)

   166 apply(simp add: conc_def)

   167 apply(auto)

   168 done

   169 

   170 lemma SUBSEQ_star2:

   171   assumes a: "x \<in> SUBSEQ (A\<star>)" 

   172   shows "x \<in> (SUBSEQ A)\<star>"

   173 using a

   174 apply(subst (asm) star_def)

   175 apply(auto simp add: SUBSEQ_star2_aux)

   176 done

   177 

   178 lemma SUBSEQ_star [simp]:

   179   shows "SUBSEQ (A\<star>) = (SUBSEQ A)\<star>"

   180 using SUBSEQ_star1 SUBSEQ_star2 by auto

   181 

   182 lemma SUBSEQ_fold:

   183   shows "SUBSEQ A \<union> A = SUBSEQ A"

   184 apply(auto simp add: SUBSEQ_def)

   185 apply(rule_tac x="x" in bexI)

   186 apply(auto simp add: emb_refl)

   187 done

   188 

   189 

   190 lemma SUPSEQ_union [simp]:

   191   "SUPSEQ (A \<union> B) = (SUPSEQ A \<union> B) \<inter> (SUPSEQ B \<union> A)"

   192 unfolding SUPSEQ_def 

   193 by auto

   194 

   195 

   196 definition

   197   Notreg :: "'a::finite rexp \<Rightarrow> 'a rexp"

   198 where

   199   "Notreg r \<equiv> SOME r'. lang r' = - (lang r)"

   200 

   201 lemma [simp]:

   202   "lang (Notreg r) = - lang r"

   203 apply(simp add: Notreg_def)

   204 apply(rule someI2_ex)

   205 apply(auto)

   206 apply(subgoal_tac "regular (lang r)")

   207 apply(drule closure_complement)

   208 apply(auto) 

   209 done

   210 

   211 definition

   212   Interreg :: "'a::finite rexp \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"

   213 where

   214   "Interreg r1 r2 = Notreg (Plus (Notreg r1) (Notreg r2))"

   215 

   216 lemma [simp]:

   217   "lang (Interreg r1 r2) = (lang r1) \<inter> (lang r2)"

   218 by (simp add: Interreg_def)

   219 

   220 definition

   221   Diffreg :: "'a::finite rexp \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"

   222 where

   223   "Diffreg r1 r2 = Notreg (Plus (Notreg r1) r2)"

   224 

   225 lemma [simp]:

   226   "lang (Diffreg r1 r2) = (lang r1) - (lang r2)"

   227 by (auto simp add: Diffreg_def)

   228 

   229 definition

   230   Allreg :: "'a::finite rexp"

   231 where

   232   "Allreg \<equiv> \<Uplus>(Atom ` UNIV)"

   233 

   234 lemma Allreg_lang [simp]:

   235   "lang Allreg = (\<Union>a. {[a]})"

   236 unfolding Allreg_def

   237 by auto

   238 

   239 lemma [simp]:

   240   "(\<Union>a. {[a]})\<star> = UNIV"

   241 apply(auto)

   242 apply(induct_tac x rule: list.induct)

   243 apply(auto)

   244 apply(subgoal_tac "[a] @ list \<in> (\<Union>a. {[a]})\<star>")

   245 apply(simp)

   246 apply(rule append_in_starI)

   247 apply(auto)

   248 done

   249 

   250 lemma Star_Allreg_lang [simp]:

   251   "lang (Star Allreg) = UNIV"

   252 by (simp)

   253 

   254 fun UP :: "'a::finite rexp \<Rightarrow> 'a rexp"

   255 where

   256   "UP (Zero) = Star Allreg"

   257 | "UP (One) = Star Allreg"

   258 | "UP (Atom c) = Times Allreg (Star Allreg)"   

   259 | "UP (Plus r1 r2) = Interreg (Plus (UP r1) (r2)) (Plus (UP r2) r1)"

   260 | "UP (Times r1 r2) = 

   261      Plus (Notreg (Times (Plus (Notreg (UP r1)) r1) (Plus (Notreg (UP r2)) r2))) (Times r1 r2)"

   262 | "UP (Star r) = Plus (Notreg (Star (Plus (Notreg (UP r)) r))) (Star r)"

   263 

   264 lemma UP:

   265   "lang (UP r) = SUPSEQ (lang r)"

   266 apply(induct r)

   267 apply(simp add: SUPSEQ_def)

   268 apply(simp add: SUPSEQ_def)

   269 apply(simp add: Compl_eq_Diff_UNIV)

   270 apply(auto)[1]

   271 apply(simp add: SUPSEQ_def)

   272 apply(simp add: Compl_eq_Diff_UNIV)

   273 apply(rule sym)

   274 apply(rule_tac s="UNIV - {[]}" in trans)

   275 apply(auto)[1]

   276 apply(auto simp add: conc_def)[1]

   277 apply(case_tac x)

   278 apply(simp)

   279 apply(simp)

   280 apply(rule_tac x="[a]" in exI)

   281 apply(simp)

   282 apply(simp)

   283 apply(simp)

   284 apply(simp add: SUPSEQ_def)

   285 apply(simp add: Un_Int_distrib2)

   286 apply(simp add: Compl_partition2)

   287 apply(simp add: SUBSEQ_fold)

   288 apply(simp add: Un_Diff)

   289 apply(simp add: SUPSEQ_def)

   290 apply(simp add: Un_Int_distrib2)

   291 apply(simp add: Compl_partition2)

   292 apply(simp add: SUBSEQ_fold)

   293 done

   294 

   295 lemma SUPSEQ_reg:

   296   fixes A :: "'a::finite lang"

   297   assumes "regular A"

   298   shows "regular (SUPSEQ A)"

   299 proof -

   300   from assms obtain r::"'a::finite rexp" where eq: "lang r = A" by auto

   301   moreover 

   302   have "lang (UP r) = SUPSEQ (lang r)" by (rule UP)

   303   ultimately show "regular (SUPSEQ A)" by auto

   304 qed

   305    

   306 

   307  

   308 

   309 

   310 end