--- a/Closure.thy Thu May 12 05:55:05 2011 +0000
+++ b/Closure.thy Wed May 18 19:54:43 2011 +0000
@@ -1,223 +1,140 @@
-theory "RegSet"
- imports "Main"
+theory Closure
+imports Myhill_2
begin
-
-text {* Sequential composition of sets *}
+section {* Closure properties of regular languages *}
-definition
- lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ; _" [100,100] 100)
-where
- "L1 ; L2 = {s1@s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
+abbreviation
+ regular :: "lang \<Rightarrow> bool"
+where
+ "regular A \<equiv> \<exists>r::rexp. A = L r"
-section {* Kleene star for sets *}
+lemma closure_union[intro]:
+ assumes "regular A" "regular B"
+ shows "regular (A \<union> B)"
+proof -
+ from assms obtain r1 r2::rexp where "L r1 = A" "L r2 = B" by auto
+ then have "A \<union> B = L (ALT r1 r2)" by simp
+ then show "regular (A \<union> B)" by blast
+qed
-inductive_set
- Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
- for L :: "string set"
-where
- start[intro]: "[] \<in> L\<star>"
-| step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> L\<star>"
+lemma closure_seq[intro]:
+ assumes "regular A" "regular B"
+ shows "regular (A ;; B)"
+proof -
+ from assms obtain r1 r2::rexp where "L r1 = A" "L r2 = B" by auto
+ then have "A ;; B = L (SEQ r1 r2)" by simp
+ then show "regular (A ;; B)" by blast
+qed
-
-text {* A standard property of star *}
+lemma closure_star[intro]:
+ assumes "regular A"
+ shows "regular (A\<star>)"
+proof -
+ from assms obtain r::rexp where "L r = A" by auto
+ then have "A\<star> = L (STAR r)" by simp
+ then show "regular (A\<star>)" by blast
+qed
-lemma lang_star_cases:
- shows "L\<star> = {[]} \<union> L ; L\<star>"
-proof
- { fix x
- have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ; L\<star>"
- unfolding lang_seq_def
- by (induct rule: Star.induct) (auto)
- }
- then show "L\<star> \<subseteq> {[]} \<union> L ; L\<star>" by auto
-next
- show "{[]} \<union> L ; L\<star> \<subseteq> L\<star>"
- unfolding lang_seq_def by auto
+lemma closure_complement[intro]:
+ assumes "regular A"
+ shows "regular (- A)"
+proof -
+ from assms have "finite (UNIV // \<approx>A)" by (simp add: Myhill_Nerode)
+ then have "finite (UNIV // \<approx>(-A))" by (simp add: str_eq_rel_def)
+ then show "regular (- A)" by (simp add: Myhill_Nerode)
+qed
+
+lemma closure_difference[intro]:
+ assumes "regular A" "regular B"
+ shows "regular (A - B)"
+proof -
+ have "A - B = - (- A \<union> B)" by blast
+ moreover
+ have "regular (- (- A \<union> B))"
+ using assms by blast
+ ultimately show "regular (A - B)" by simp
+qed
+
+lemma closure_intersection[intro]:
+ assumes "regular A" "regular B"
+ shows "regular (A \<inter> B)"
+proof -
+ have "A \<inter> B = - (- A \<union> - B)" by blast
+ moreover
+ have "regular (- (- A \<union> - B))"
+ using assms by blast
+ ultimately show "regular (A \<inter> B)" by simp
qed
-lemma lang_star_cases2:
- shows "[] \<notin> L \<Longrightarrow> L\<star> - {[]} = L ; L\<star>"
-by (subst lang_star_cases)
- (simp add: lang_seq_def)
-
-
-section {* Regular Expressions *}
-
-datatype rexp =
- NULL
-| EMPTY
-| CHAR char
-| SEQ rexp rexp
-| ALT rexp rexp
-| STAR rexp
-
-
-section {* Semantics of Regular Expressions *}
+text {* closure under string reversal *}
fun
- L :: "rexp \<Rightarrow> string set"
+ Rev :: "rexp \<Rightarrow> rexp"
where
- "L (NULL) = {}"
-| "L (EMPTY) = {[]}"
-| "L (CHAR c) = {[c]}"
-| "L (SEQ r1 r2) = (L r1) ; (L r2)"
-| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
-| "L (STAR r) = (L r)\<star>"
-
-abbreviation
- CUNIV :: "string set"
-where
- "CUNIV \<equiv> (\<lambda>x. [x]) ` (UNIV::char set)"
-
-lemma CUNIV_star_minus:
- "(CUNIV\<star> - {[c]}) = {[]} \<union> (CUNIV - {[c]}; (CUNIV\<star>))"
-apply(subst lang_star_cases)
-apply(simp add: lang_seq_def)
-oops
-
+ "Rev NULL = NULL"
+| "Rev EMPTY = EMPTY"
+| "Rev (CHAR c) = CHAR c"
+| "Rev (ALT r1 r2) = ALT (Rev r1) (Rev r2)"
+| "Rev (SEQ r1 r2) = SEQ (Rev r2) (Rev r1)"
+| "Rev (STAR r) = STAR (Rev r)"
-lemma string_in_CUNIV:
- shows "s \<in> CUNIV\<star>"
-proof (induct s)
- case Nil
- show "[] \<in> CUNIV\<star>" by (rule start)
-next
- case (Cons c s)
- have "[c] \<in> CUNIV" by simp
- moreover
- have "s \<in> CUNIV\<star>" by fact
- ultimately have "[c] @ s \<in> CUNIV\<star>" by (rule step)
- then show "c # s \<in> CUNIV\<star>" by simp
-qed
-
-lemma UNIV_CUNIV_star:
- shows "UNIV = CUNIV\<star>"
-using string_in_CUNIV
-by (auto)
-
-abbreviation
- reg :: "string set => bool"
-where
- "reg L1 \<equiv> (\<exists>r. L r = L1)"
-
-lemma reg_null [intro]:
- shows "reg {}"
-by (metis L.simps(1))
+lemma rev_Seq:
+ "(rev ` A) ;; (rev ` B) = rev ` (B ;; A)"
+unfolding Seq_def image_def
+apply(auto)
+apply(rule_tac x="xb @ xa" in exI)
+apply(auto)
+done
-lemma reg_empty [intro]:
- shows "reg {[]}"
-by (metis L.simps(2))
-
-lemma reg_star [intro]:
- shows "reg L1 \<Longrightarrow> reg (L1\<star>)"
-by (metis L.simps(6))
-
-lemma reg_seq [intro]:
- assumes a: "reg L1" "reg L2"
- shows "reg (L1 ; L2)"
+lemma rev_Star1:
+ assumes a: "s \<in> (rev ` A)\<star>"
+ shows "s \<in> rev ` (A\<star>)"
using a
-by (metis L.simps(4))
-
-lemma reg_union [intro]:
- assumes a: "reg L1" "reg L2"
- shows "reg (L1 \<union> L2)"
-using a
-by (metis L.simps(5))
+proof(induct rule: star_induct)
+ case (step s1 s2)
+ have inj: "inj (rev::string \<Rightarrow> string)" unfolding inj_on_def by auto
+ have "s1 \<in> rev ` A" "s2 \<in> rev ` (A\<star>)" by fact+
+ then obtain x1 x2 where "x1 \<in> A" "x2 \<in> A\<star>" and eqs: "s1 = rev x1" "s2 = rev x2" by auto
+ then have "x1 \<in> A\<star>" "x2 \<in> A\<star>" by (auto intro: star_intro2)
+ then have "x2 @ x1 \<in> A\<star>" by (auto intro: star_intro1)
+ then have "rev (x2 @ x1) \<in> rev ` A\<star>" using inj by (simp only: inj_image_mem_iff)
+ then show "s1 @ s2 \<in> rev ` A\<star>" using eqs by simp
+qed (auto)
-lemma reg_string [intro]:
- fixes s::string
- shows "reg {s}"
-proof (induct s)
- case Nil
- show "reg {[]}" by (rule reg_empty)
-next
- case (Cons c s)
- have "reg {s}" by fact
- then obtain r where "L r = {s}" by auto
- then have "L (SEQ (CHAR c) r) = {[c]} ; {s}" by simp
- also have "\<dots> = {c # s}" by (simp add: lang_seq_def)
- finally show "reg {c # s}" by blast
-qed
+lemma rev_Star2:
+ assumes a: "s \<in> A\<star>"
+ shows "rev s \<in> (rev ` A)\<star>"
+using a
+proof(induct rule: star_induct)
+ case (step s1 s2)
+ have inj: "inj (rev::string \<Rightarrow> string)" unfolding inj_on_def by auto
+ have "s1 \<in> A"by fact
+ then have "rev s1 \<in> rev ` A" using inj by (simp only: inj_image_mem_iff)
+ then have "rev s1 \<in> (rev ` A)\<star>" by (auto intro: star_intro2)
+ moreover
+ have "rev s2 \<in> (rev ` A)\<star>" by fact
+ ultimately show "rev (s1 @ s2) \<in> (rev ` A)\<star>" by (auto intro: star_intro1)
+qed (auto)
-lemma reg_finite [intro]:
- assumes a: "finite L1"
- shows "reg L1"
-using a
-proof(induct)
- case empty
- show "reg {}" by (rule reg_null)
-next
- case (insert s S)
- have "reg {s}" by (rule reg_string)
- moreover
- have "reg S" by fact
- ultimately have "reg ({s} \<union> S)" by (rule reg_union)
- then show "reg (insert s S)" by simp
+lemma rev_Star:
+ "(rev ` A)\<star> = rev ` (A\<star>)"
+using rev_Star1 rev_Star2 by auto
+
+lemma rev_lang:
+ "L (Rev r) = rev ` (L r)"
+by (induct r) (simp_all add: rev_Star rev_Seq image_Un)
+
+lemma closure_reversal[intro]:
+ assumes "regular A"
+ shows "regular (rev ` A)"
+proof -
+ from assms obtain r::rexp where "L r = A" by auto
+ then have "L (Rev r) = rev ` A" by (simp add: rev_lang)
+ then show "regular (rev` A)" by blast
qed
-lemma reg_cuniv [intro]:
- shows "reg (CUNIV)"
-by (rule reg_finite) (auto)
-lemma reg_univ:
- shows "reg (UNIV::string set)"
-proof -
- have "reg CUNIV" by (rule reg_cuniv)
- then have "reg (CUNIV\<star>)" by (rule reg_star)
- then show "reg UNIV" by (simp add: UNIV_CUNIV_star)
-qed
-
-lemma reg_finite_subset:
- assumes a: "finite L1"
- and b: "reg L1" "L2 \<subseteq> L1"
- shows "reg L2"
-using a b
-apply(induct arbitrary: L2)
-apply(simp add: reg_empty)
-oops
-
-
-lemma reg_not:
- shows "reg (UNIV - L r)"
-proof (induct r)
- case NULL
- have "reg UNIV" by (rule reg_univ)
- then show "reg (UNIV - L NULL)" by simp
-next
- case EMPTY
- have "[] \<notin> CUNIV" by auto
- moreover
- have "reg (CUNIV; CUNIV\<star>)" by auto
- ultimately have "reg (CUNIV\<star> - {[]})"
- using lang_star_cases2 by simp
- then show "reg (UNIV - L EMPTY)" by (simp add: UNIV_CUNIV_star)
-next
- case (CHAR c)
- then show "?case"
- apply(simp)
-
-using reg_UNIV
-apply(simp)
-apply(simp add: char_star2[symmetric])
-apply(rule reg_seq)
-apply(rule reg_cuniv)
-apply(rule reg_star)
-apply(rule reg_cuniv)
-oops
-
-
-
-end
-
-
-
-
-
-
-
-
-
-
+end
\ No newline at end of file