--- a/Theories/Regular.thy Tue May 31 20:32:49 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,311 +0,0 @@
-theory Regular
-imports Main Folds
-begin
-
-section {* Preliminary definitions *}
-
-type_synonym lang = "string set"
-
-
-text {* Sequential composition of two languages *}
-
-definition
- Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100)
-where
- "A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"
-
-
-text {* Some properties of operator @{text ";;"}. *}
-
-lemma seq_add_left:
- assumes a: "A = B"
- shows "C ;; A = C ;; B"
-using a by simp
-
-lemma seq_union_distrib_right:
- shows "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)"
-unfolding Seq_def by auto
-
-lemma seq_union_distrib_left:
- shows "C ;; (A \<union> B) = (C ;; A) \<union> (C ;; B)"
-unfolding Seq_def by auto
-
-lemma seq_intro:
- assumes a: "x \<in> A" "y \<in> B"
- shows "x @ y \<in> A ;; B "
-using a by (auto simp: Seq_def)
-
-lemma seq_assoc:
- shows "(A ;; B) ;; C = A ;; (B ;; C)"
-unfolding Seq_def
-apply(auto)
-apply(blast)
-by (metis append_assoc)
-
-lemma seq_empty [simp]:
- shows "A ;; {[]} = A"
- and "{[]} ;; A = A"
-by (simp_all add: Seq_def)
-
-lemma seq_null [simp]:
- shows "A ;; {} = {}"
- and "{} ;; A = {}"
-by (simp_all add: Seq_def)
-
-
-text {* Power and Star of a language *}
-
-fun
- pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100)
-where
- "A \<up> 0 = {[]}"
-| "A \<up> (Suc n) = A ;; (A \<up> n)"
-
-definition
- Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102)
-where
- "A\<star> \<equiv> (\<Union>n. A \<up> n)"
-
-
-lemma star_start[intro]:
- shows "[] \<in> A\<star>"
-proof -
- have "[] \<in> A \<up> 0" by auto
- then show "[] \<in> A\<star>" unfolding Star_def by blast
-qed
-
-lemma star_step [intro]:
- assumes a: "s1 \<in> A"
- and b: "s2 \<in> A\<star>"
- shows "s1 @ s2 \<in> A\<star>"
-proof -
- from b obtain n where "s2 \<in> A \<up> n" unfolding Star_def by auto
- then have "s1 @ s2 \<in> A \<up> (Suc n)" using a by (auto simp add: Seq_def)
- then show "s1 @ s2 \<in> A\<star>" unfolding Star_def by blast
-qed
-
-lemma star_induct[consumes 1, case_names start step]:
- assumes a: "x \<in> A\<star>"
- and b: "P []"
- and c: "\<And>s1 s2. \<lbrakk>s1 \<in> A; s2 \<in> A\<star>; P s2\<rbrakk> \<Longrightarrow> P (s1 @ s2)"
- shows "P x"
-proof -
- from a obtain n where "x \<in> A \<up> n" unfolding Star_def by auto
- then show "P x"
- by (induct n arbitrary: x)
- (auto intro!: b c simp add: Seq_def Star_def)
-qed
-
-lemma star_intro1:
- assumes a: "x \<in> A\<star>"
- and b: "y \<in> A\<star>"
- shows "x @ y \<in> A\<star>"
-using a b
-by (induct rule: star_induct) (auto)
-
-lemma star_intro2:
- assumes a: "y \<in> A"
- shows "y \<in> A\<star>"
-proof -
- from a have "y @ [] \<in> A\<star>" by blast
- then show "y \<in> A\<star>" by simp
-qed
-
-lemma star_intro3:
- assumes a: "x \<in> A\<star>"
- and b: "y \<in> A"
- shows "x @ y \<in> A\<star>"
-using a b by (blast intro: star_intro1 star_intro2)
-
-lemma star_cases:
- shows "A\<star> = {[]} \<union> A ;; A\<star>"
-proof
- { fix x
- have "x \<in> A\<star> \<Longrightarrow> x \<in> {[]} \<union> A ;; A\<star>"
- unfolding Seq_def
- by (induct rule: star_induct) (auto)
- }
- then show "A\<star> \<subseteq> {[]} \<union> A ;; A\<star>" by auto
-next
- show "{[]} \<union> A ;; A\<star> \<subseteq> A\<star>"
- unfolding Seq_def by auto
-qed
-
-lemma star_decom:
- assumes a: "x \<in> A\<star>" "x \<noteq> []"
- shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>"
-using a
-by (induct rule: star_induct) (blast)+
-
-lemma
- shows seq_Union_left: "B ;; (\<Union>n. A \<up> n) = (\<Union>n. B ;; (A \<up> n))"
- and seq_Union_right: "(\<Union>n. A \<up> n) ;; B = (\<Union>n. (A \<up> n) ;; B)"
-unfolding Seq_def by auto
-
-lemma seq_pow_comm:
- shows "A ;; (A \<up> n) = (A \<up> n) ;; A"
-by (induct n) (simp_all add: seq_assoc[symmetric])
-
-lemma seq_star_comm:
- shows "A ;; A\<star> = A\<star> ;; A"
-unfolding Star_def seq_Union_left
-unfolding seq_pow_comm seq_Union_right
-by simp
-
-
-text {* Two lemmas about the length of strings in @{text "A \<up> n"} *}
-
-lemma pow_length:
- assumes a: "[] \<notin> A"
- and b: "s \<in> A \<up> Suc n"
- shows "n < length s"
-using b
-proof (induct n arbitrary: s)
- case 0
- have "s \<in> A \<up> Suc 0" by fact
- with a have "s \<noteq> []" by auto
- then show "0 < length s" by auto
-next
- case (Suc n)
- have ih: "\<And>s. s \<in> A \<up> Suc n \<Longrightarrow> n < length s" by fact
- have "s \<in> A \<up> Suc (Suc n)" by fact
- then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A \<up> Suc n"
- by (auto simp add: Seq_def)
- from ih ** have "n < length s2" by simp
- moreover have "0 < length s1" using * a by auto
- ultimately show "Suc n < length s" unfolding eq
- by (simp only: length_append)
-qed
-
-lemma seq_pow_length:
- assumes a: "[] \<notin> A"
- and b: "s \<in> B ;; (A \<up> Suc n)"
- shows "n < length s"
-proof -
- from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A \<up> Suc n"
- unfolding Seq_def by auto
- from * have " n < length s2" by (rule pow_length[OF a])
- then show "n < length s" using eq by simp
-qed
-
-
-section {* A modified version of Arden's lemma *}
-
-text {* A helper lemma for Arden *}
-
-lemma arden_helper:
- assumes eq: "X = X ;; A \<union> B"
- shows "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"
-proof (induct n)
- case 0
- show "X = X ;; (A \<up> Suc 0) \<union> (\<Union>(m::nat)\<in>{0..0}. B ;; (A \<up> m))"
- using eq by simp
-next
- case (Suc n)
- have ih: "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" by fact
- also have "\<dots> = (X ;; A \<union> B) ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" using eq by simp
- also have "\<dots> = X ;; (A \<up> Suc (Suc n)) \<union> (B ;; (A \<up> Suc n)) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"
- by (simp add: seq_union_distrib_right seq_assoc)
- also have "\<dots> = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))"
- by (auto simp add: le_Suc_eq)
- finally show "X = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))" .
-qed
-
-theorem arden:
- assumes nemp: "[] \<notin> A"
- shows "X = X ;; A \<union> B \<longleftrightarrow> X = B ;; A\<star>"
-proof
- assume eq: "X = B ;; A\<star>"
- have "A\<star> = {[]} \<union> A\<star> ;; A"
- unfolding seq_star_comm[symmetric]
- by (rule star_cases)
- then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"
- by (rule seq_add_left)
- also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"
- unfolding seq_union_distrib_left by simp
- also have "\<dots> = B \<union> (B ;; A\<star>) ;; A"
- by (simp only: seq_assoc)
- finally show "X = X ;; A \<union> B"
- using eq by blast
-next
- assume eq: "X = X ;; A \<union> B"
- { fix n::nat
- have "B ;; (A \<up> n) \<subseteq> X" using arden_helper[OF eq, of "n"] by auto }
- then have "B ;; A\<star> \<subseteq> X"
- unfolding Seq_def Star_def UNION_def by auto
- moreover
- { fix s::string
- obtain k where "k = length s" by auto
- then have not_in: "s \<notin> X ;; (A \<up> Suc k)"
- using seq_pow_length[OF nemp] by blast
- assume "s \<in> X"
- then have "s \<in> X ;; (A \<up> Suc k) \<union> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))"
- using arden_helper[OF eq, of "k"] by auto
- then have "s \<in> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))" using not_in by auto
- moreover
- have "(\<Union>m\<in>{0..k}. B ;; (A \<up> m)) \<subseteq> (\<Union>n. B ;; (A \<up> n))" by auto
- ultimately
- have "s \<in> B ;; A\<star>"
- unfolding seq_Union_left Star_def by auto }
- then have "X \<subseteq> B ;; A\<star>" by auto
- ultimately
- show "X = B ;; A\<star>" by simp
-qed
-
-
-section {* Regular Expressions *}
-
-datatype rexp =
- NULL
-| EMPTY
-| CHAR char
-| SEQ rexp rexp
-| ALT rexp rexp
-| STAR rexp
-
-
-text {*
- The function @{text L} is overloaded, with the idea that @{text "L x"}
- evaluates to the language represented by the object @{text x}.
-*}
-
-consts L:: "'a \<Rightarrow> lang"
-
-overloading L_rexp \<equiv> "L:: rexp \<Rightarrow> lang"
-begin
-fun
- L_rexp :: "rexp \<Rightarrow> lang"
-where
- "L_rexp (NULL) = {}"
- | "L_rexp (EMPTY) = {[]}"
- | "L_rexp (CHAR c) = {[c]}"
- | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)"
- | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"
- | "L_rexp (STAR r) = (L_rexp r)\<star>"
-end
-
-
-text {* ALT-combination for a set of regular expressions *}
-
-abbreviation
- Setalt ("\<Uplus>_" [1000] 999)
-where
- "\<Uplus>A \<equiv> folds ALT NULL A"
-
-text {*
- For finite sets, @{term Setalt} is preserved under @{term L}.
-*}
-
-lemma folds_alt_simp [simp]:
- fixes rs::"rexp set"
- assumes a: "finite rs"
- shows "L (\<Uplus>rs) = \<Union> (L ` rs)"
-unfolding folds_def
-apply(rule set_eqI)
-apply(rule someI2_ex)
-apply(rule_tac finite_imp_fold_graph[OF a])
-apply(erule fold_graph.induct)
-apply(auto)
-done
-
-end
\ No newline at end of file