1 theory Mirkin

     2 imports Derivatives

     3 begin

     4 

     5 fun

     6   pbase :: "'a rexp \<Rightarrow> 'a rexp set"

     7 where

     8   "pbase (Zero) = {}"

     9 | "pbase (One) = {}"

    10 | "pbase (Atom a) = {One}"

    11 | "pbase (Plus r1 r2) = pbase r1 \<union> pbase r2"

    12 | "pbase (Times r1 r2) = Timess (pbase r1) r2 \<union> pbase r2"

    13 | "pbase (Star r) = Timess (pbase r) (Star r)"

    14 

    15 

    16 lemma a: "A \<subseteq> B \<Longrightarrow> Timess A r \<subseteq> Timess B r"

    17 apply(auto)

    18 done

    19 

    20 lemma b: "pders_lang UNIV1 r \<subseteq> pbase r"

    21 apply(induct r)

    22 apply(simp)

    23 apply(simp)

    24 apply(simp)

    25 apply(simp)

    26 apply(auto)[1]

    27 apply(simp)

    28 apply(rule subset_trans)

    29 apply(rule pders_lang_Times)

    30 apply(simp)

    31 apply(rule conjI)

    32 apply(drule_tac r="r2" in a)

    33 apply(auto)[1]

    34 apply(auto)[1]

    35 apply(rule subset_trans)

    36 apply(rule pders_lang_Star)

    37 apply(simp)

    38 apply(rule a)

    39 apply(simp)

    40 done

    41 

    42 lemma c: "pders_lang UNIV r \<subseteq> pbase r \<union> {r}"

    43 using b

    44 apply(auto simp add: pders_lang_UNIV)

    45 done

    46 

    47 lemma d: "finite (pbase r)"

    48 apply(induct r)

    49 apply(auto)

    50 done

    51 

    52 lemma e: "pder c r \<subseteq> pbase r"

    53 by (induct r) (auto)

    54 

    55 

    56 end