--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Mirkin.thy	Thu Aug 11 23:11:39 2011 +0000
@@ -0,0 +1,56 @@
+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
\ No newline at end of file