theory Mirkin
imports Derivatives
begin

fun
  pbase :: "'a rexp \<Rightarrow> 'a rexp set"
where
  "pbase (Zero) = {}"
| "pbase (One) = {}"
| "pbase (Atom a) = {One}"
| "pbase (Plus r1 r2) = pbase r1 \<union> pbase r2"
| "pbase (Times r1 r2) = Timess (pbase r1) r2 \<union> pbase r2"
| "pbase (Star r) = Timess (pbase r) (Star r)"


lemma a: "A \<subseteq> B \<Longrightarrow> Timess A r \<subseteq> Timess B r"
apply(auto)
done

lemma b: "pders_lang UNIV1 r \<subseteq> pbase r"
apply(induct r)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
apply(auto)[1]
apply(simp)
apply(rule subset_trans)
apply(rule pders_lang_Times)
apply(simp)
apply(rule conjI)
apply(drule_tac r="r2" in a)
apply(auto)[1]
apply(auto)[1]
apply(rule subset_trans)
apply(rule pders_lang_Star)
apply(simp)
apply(rule a)
apply(simp)
done

lemma c: "pders_lang UNIV r \<subseteq> pbase r \<union> {r}"
using b
apply(auto simp add: pders_lang_UNIV)
done

lemma d: "finite (pbase r)"
apply(induct r)
apply(auto)
done

lemma e: "pder c r \<subseteq> pbase r"
by (induct r) (auto)


end