diff -r b794db0b79db -r b1258b7d2789 Closure.thy --- a/Closure.thy Fri Jun 03 13:59:21 2011 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,158 +0,0 @@ -(* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *) -theory Closure -imports Derivs -begin - -section {* Closure properties of regular languages *} - -abbreviation - regular :: "lang \ bool" -where - "regular A \ \r. A = L_rexp r" - -subsection {* Closure under set operations *} - -lemma closure_union[intro]: - assumes "regular A" "regular B" - shows "regular (A \ B)" -proof - - from assms obtain r1 r2::rexp where "L_rexp r1 = A" "L_rexp r2 = B" by auto - then have "A \ B = L_rexp (ALT r1 r2)" by simp - then show "regular (A \ B)" by blast -qed - -lemma closure_seq[intro]: - assumes "regular A" "regular B" - shows "regular (A \ B)" -proof - - from assms obtain r1 r2::rexp where "L_rexp r1 = A" "L_rexp r2 = B" by auto - then have "A \ B = L_rexp (SEQ r1 r2)" by simp - then show "regular (A \ B)" by blast -qed - -lemma closure_star[intro]: - assumes "regular A" - shows "regular (A\)" -proof - - from assms obtain r::rexp where "L_rexp r = A" by auto - then have "A\ = L_rexp (STAR r)" by simp - then show "regular (A\)" by blast -qed - -text {* Closure under complementation is proved via the - Myhill-Nerode theorem *} - -lemma closure_complement[intro]: - assumes "regular A" - shows "regular (- A)" -proof - - from assms have "finite (UNIV // \A)" by (simp add: Myhill_Nerode) - then have "finite (UNIV // \(-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 \ B)" by blast - moreover - have "regular (- (- A \ 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 \ B)" -proof - - have "A \ B = - (- A \ - B)" by blast - moreover - have "regular (- (- A \ - B))" - using assms by blast - ultimately show "regular (A \ B)" by simp -qed - -subsection {* Closure under string reversal *} - -fun - Rev :: "rexp \ rexp" -where - "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 rev_seq[simp]: - shows "rev ` (B \ A) = (rev ` A) \ (rev ` B)" -unfolding Seq_def image_def -by (auto) (metis rev_append)+ - -lemma rev_star1: - assumes a: "s \ (rev ` A)\" - shows "s \ rev ` (A\)" -using a -proof(induct rule: star_induct) - case (step s1 s2) - have inj: "inj (rev::string \ string)" unfolding inj_on_def by auto - have "s1 \ rev ` A" "s2 \ rev ` (A\)" by fact+ - then obtain x1 x2 where "x1 \ A" "x2 \ A\" and eqs: "s1 = rev x1" "s2 = rev x2" by auto - then have "x1 \ A\" "x2 \ A\" by (auto intro: star_intro2) - then have "x2 @ x1 \ A\" by (auto intro: star_intro1) - then have "rev (x2 @ x1) \ rev ` A\" using inj by (simp only: inj_image_mem_iff) - then show "s1 @ s2 \ rev ` A\" using eqs by simp -qed (auto) - -lemma rev_star2: - assumes a: "s \ A\" - shows "rev s \ (rev ` A)\" -using a -proof(induct rule: star_induct) - case (step s1 s2) - have inj: "inj (rev::string \ string)" unfolding inj_on_def by auto - have "s1 \ A"by fact - then have "rev s1 \ rev ` A" using inj by (simp only: inj_image_mem_iff) - then have "rev s1 \ (rev ` A)\" by (auto intro: star_intro2) - moreover - have "rev s2 \ (rev ` A)\" by fact - ultimately show "rev (s1 @ s2) \ (rev ` A)\" by (auto intro: star_intro1) -qed (auto) - -lemma rev_star[simp]: - shows " rev ` (A\) = (rev ` A)\" -using rev_star1 rev_star2 by auto - -lemma rev_lang: - shows "rev ` (L_rexp r) = L_rexp (Rev r)" -by (induct r) (simp_all add: image_Un) - -lemma closure_reversal[intro]: - assumes "regular A" - shows "regular (rev ` A)" -proof - - from assms obtain r::rexp where "A = L_rexp r" by auto - then have "L_rexp (Rev r) = rev ` A" by (simp add: rev_lang) - then show "regular (rev` A)" by blast -qed - -subsection {* Closure under left-quotients *} - -lemma closure_left_quotient: - assumes "regular A" - shows "regular (Ders_set B A)" -proof - - from assms obtain r::rexp where eq: "L_rexp r = A" by auto - have fin: "finite (pders_set B r)" by (rule finite_pders_set) - - have "Ders_set B (L_rexp r) = (\ L_rexp ` (pders_set B r))" - by (simp add: Ders_set_pders_set) - also have "\ = L_rexp (\(pders_set B r))" using fin by simp - finally have "Ders_set B A = L_rexp (\(pders_set B r))" using eq - by simp - then show "regular (Ders_set B A)" by auto -qed - - -end \ No newline at end of file