--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/More_Regular_Set.thy Mon Aug 22 12:49:27 2011 +0000
@@ -0,0 +1,151 @@
+(* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *)
+theory More_Regular_Set
+imports "Regular_Exp" "Folds"
+begin
+
+text {* Some properties of operator @{text "@@"}. *}
+
+notation
+ conc (infixr "\<cdot>" 100) and
+ star ("_\<star>" [101] 102)
+
+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 conc_pow_comm:
+ shows "A \<cdot> (A ^^ n) = (A ^^ n) \<cdot> A"
+by (induct n) (simp_all add: conc_assoc[symmetric])
+
+lemma conc_star_comm:
+ shows "A \<cdot> A\<star> = A\<star> \<cdot> A"
+unfolding star_def conc_pow_comm conc_UNION_distrib
+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 ^^ Suc n"
+ shows "n < length s"
+using b
+proof (induct n arbitrary: s)
+ case 0
+ have "s \<in> A ^^ 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 ^^ Suc n \<Longrightarrow> n < length s" by fact
+ have "s \<in> A ^^ Suc (Suc n)" by fact
+ then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A ^^ Suc n"
+ by (auto simp add: conc_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 conc_pow_length:
+ assumes a: "[] \<notin> A"
+ and b: "s \<in> B \<cdot> (A ^^ Suc n)"
+ shows "n < length s"
+proof -
+ from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A ^^ Suc n"
+ 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 \<cdot> A \<union> B"
+ shows "X = X \<cdot> (A ^^ Suc n) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))"
+proof (induct n)
+ case 0
+ show "X = X \<cdot> (A ^^ Suc 0) \<union> (\<Union>(m::nat)\<in>{0..0}. B \<cdot> (A ^^ m))"
+ using eq by simp
+next
+ case (Suc n)
+ have ih: "X = X \<cdot> (A ^^ Suc n) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))" by fact
+ also have "\<dots> = (X \<cdot> A \<union> B) \<cdot> (A ^^ Suc n) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))" using eq by simp
+ also have "\<dots> = X \<cdot> (A ^^ Suc (Suc n)) \<union> (B \<cdot> (A ^^ Suc n)) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))"
+ by (simp add: conc_Un_distrib conc_assoc)
+ also have "\<dots> = X \<cdot> (A ^^ Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B \<cdot> (A ^^ m))"
+ by (auto simp add: le_Suc_eq)
+ finally show "X = X \<cdot> (A ^^ Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B \<cdot> (A ^^ m))" .
+qed
+
+theorem arden:
+ assumes nemp: "[] \<notin> A"
+ shows "X = X \<cdot> A \<union> B \<longleftrightarrow> X = B \<cdot> A\<star>"
+proof
+ assume eq: "X = B \<cdot> A\<star>"
+ have "A\<star> = {[]} \<union> A\<star> \<cdot> A"
+ unfolding conc_star_comm[symmetric]
+ by(metis Un_commute star_unfold_left)
+ then have "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"
+ by metis
+ also have "\<dots> = B \<union> B \<cdot> (A\<star> \<cdot> A)"
+ unfolding conc_Un_distrib by simp
+ also have "\<dots> = B \<union> (B \<cdot> A\<star>) \<cdot> A"
+ by (simp only: conc_assoc)
+ finally show "X = X \<cdot> A \<union> B"
+ using eq by blast
+next
+ assume eq: "X = X \<cdot> A \<union> B"
+ { fix n::nat
+ have "B \<cdot> (A ^^ n) \<subseteq> X" using arden_helper[OF eq, of "n"] by auto }
+ then have "B \<cdot> A\<star> \<subseteq> X"
+ unfolding conc_def star_def UNION_def by auto
+ moreover
+ { fix s::"'a list"
+ obtain k where "k = length s" by auto
+ then have not_in: "s \<notin> X \<cdot> (A ^^ Suc k)"
+ using conc_pow_length[OF nemp] by blast
+ assume "s \<in> X"
+ then have "s \<in> X \<cdot> (A ^^ Suc k) \<union> (\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m))"
+ using arden_helper[OF eq, of "k"] by auto
+ then have "s \<in> (\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m))" using not_in by auto
+ moreover
+ have "(\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m)) \<subseteq> (\<Union>n. B \<cdot> (A ^^ n))" by auto
+ ultimately
+ have "s \<in> B \<cdot> A\<star>"
+ unfolding conc_Un_distrib star_def by auto }
+ then have "X \<subseteq> B \<cdot> A\<star>" by auto
+ ultimately
+ show "X = B \<cdot> A\<star>" by simp
+qed
+
+
+text {* Plus-combination for a set of regular expressions *}
+
+abbreviation
+ Setalt ("\<Uplus>_" [1000] 999)
+where
+ "\<Uplus>A \<equiv> folds Plus Zero A"
+
+text {*
+ For finite sets, @{term Setalt} is preserved under @{term lang}.
+*}
+
+lemma folds_alt_simp [simp]:
+ fixes rs::"('a rexp) set"
+ assumes a: "finite rs"
+ shows "lang (\<Uplus>rs) = \<Union> (lang ` 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
--- a/Closures.thy Fri Aug 19 20:39:07 2011 +0000
+++ b/Closures.thy Mon Aug 22 12:49:27 2011 +0000
@@ -1,6 +1,6 @@
(* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *)
theory Closures
-imports Derivatives "~~/src/HOL/Library/Infinite_Set"
+imports Myhill "~~/src/HOL/Library/Infinite_Set"
begin
section {* Closure properties of regular languages *}
@@ -10,7 +10,7 @@
where
"regular A \<equiv> \<exists>r. A = lang r"
-subsection {* Closure under set operations *}
+subsection {* Closure under @{text "\<union>"}, @{text "\<cdot>"} and @{text "\<star>"} *}
lemma closure_union [intro]:
assumes "regular A" "regular B"
@@ -39,6 +39,8 @@
then show "regular (A\<star>)" by blast
qed
+subsection {* Closure under complementation *}
+
text {* Closure under complementation is proved via the
Myhill-Nerode theorem *}
@@ -52,6 +54,8 @@
then show "regular (- A)" by (simp add: Myhill_Nerode)
qed
+subsection {* Closure under @{text "-"} and @{text "\<inter>"} *}
+
lemma closure_difference [intro]:
fixes A::"('a::finite) lang"
assumes "regular A" "regular B"
@@ -143,24 +147,24 @@
subsection {* Closure under left-quotients *}
abbreviation
- "Ders_lang A B \<equiv> \<Union>x \<in> A. Ders x B"
+ "Deriv_lang A B \<equiv> \<Union>x \<in> A. Derivs x B"
lemma closure_left_quotient:
assumes "regular A"
- shows "regular (Ders_lang B A)"
+ shows "regular (Deriv_lang B A)"
proof -
from assms obtain r::"'a rexp" where eq: "lang r = A" by auto
- have fin: "finite (pders_lang B r)" by (rule finite_pders_lang)
+ have fin: "finite (pderivs_lang B r)" by (rule finite_pderivs_lang)
- have "Ders_lang B (lang r) = (\<Union> lang ` (pders_lang B r))"
- by (simp add: Ders_pders pders_lang_def)
- also have "\<dots> = lang (\<Uplus>(pders_lang B r))" using fin by simp
- finally have "Ders_lang B A = lang (\<Uplus>(pders_lang B r))" using eq
+ have "Deriv_lang B (lang r) = (\<Union> lang ` (pderivs_lang B r))"
+ by (simp add: Derivs_pderivs pderivs_lang_def)
+ also have "\<dots> = lang (\<Uplus>(pderivs_lang B r))" using fin by simp
+ finally have "Deriv_lang B A = lang (\<Uplus>(pderivs_lang B r))" using eq
by simp
- then show "regular (Ders_lang B A)" by auto
+ then show "regular (Deriv_lang B A)" by auto
qed
-subsection {* Finite and co-finite set are regular *}
+subsection {* Finite and co-finite sets are regular *}
lemma singleton_regular:
shows "regular {s}"
@@ -205,7 +209,7 @@
qed
-subsection {* non-regularity of particular languages *}
+subsection {* Non-regularity for languages *}
lemma continuation_lemma:
fixes A B::"('a::finite list) set"
@@ -238,51 +242,5 @@
by blast
qed
-definition
- "ex1 a b \<equiv> {replicate n a @ replicate n b | n. True}"
-
-(*
-lemma
- fixes a b::"'a::finite"
- assumes "a \<noteq> b"
- shows "\<not> regular (ex1 a b)"
-proof -
- { assume a: "regular (ex1 a b)"
- def fool \<equiv> "{replicate i a | i. True}"
- have b: "infinite fool"
- unfolding fool_def
- unfolding infinite_iff_countable_subset
- apply(rule_tac x="\<lambda>i. replicate i a" in exI)
- apply(auto simp add: inj_on_def)
- done
- from a b have "\<exists>x \<in> fool. \<exists>y \<in> fool. x \<noteq> y \<and> x \<approx>(ex1 a b) y"
- using continuation_lemma by blast
- moreover
- have c: "\<forall>x \<in> fool. \<forall>y \<in> fool. x \<noteq> y \<longrightarrow> \<not>(x \<approx>(ex1 a b) y)"
- apply(rule ballI)
- apply(rule ballI)
- apply(rule impI)
- unfolding fool_def
- apply(simp)
- apply(erule exE)+
- unfolding str_eq_def
- apply(simp)
- apply(rule_tac x="replicate i b" in exI)
- apply(simp add: ex1_def)
- apply(rule iffI)
- prefer 2
- apply(rule_tac x="i" in exI)
- apply(simp)
- apply(rule allI)
- apply(rotate_tac 3)
- apply(thin_tac "?X")
- apply(auto)
- sorry
- ultimately have "False" by auto
- }
- then show "\<not> regular (ex1 a b)" by auto
-qed
-*)
-
end
\ No newline at end of file
--- a/Derivatives.thy Fri Aug 19 20:39:07 2011 +0000
+++ b/Derivatives.thy Mon Aug 22 12:49:27 2011 +0000
@@ -1,67 +1,81 @@
theory Derivatives
-imports Myhill_2
+imports Regular_Exp
begin
-section {* Left-Quotients and Derivatives *}
-
-subsection {* Left-Quotients *}
+section {* Leftquotients, Derivatives and Partial Derivatives *}
-definition
- Delta :: "'a lang \<Rightarrow> 'a lang"
-where
- "Delta A = (if [] \<in> A then {[]} else {})"
+text{* This theory is based on work by Brozowski \cite{Brzozowski64} and Antimirov \cite{Antimirov95}. *}
+
+subsection {* Left-Quotients of languages *}
-definition
- Der :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
-where
- "Der c A \<equiv> {s'. [c] @ s' \<in> A}"
+definition Deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where "Deriv x A = { xs. x#xs \<in> A }"
-definition
- Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
-where
- "Ders s A \<equiv> {s'. s @ s' \<in> A}"
+definition Derivs :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where "Derivs xs A = { ys. xs @ ys \<in> A }"
abbreviation
- "Derss s A \<equiv> \<Union> (Ders s) ` A"
+ Derivss :: "'a list \<Rightarrow> 'a lang set \<Rightarrow> 'a lang"
+where
+ "Derivss s As \<equiv> \<Union> (Derivs s) ` As"
+
+
+lemma Deriv_empty[simp]: "Deriv a {} = {}"
+ and Deriv_epsilon[simp]: "Deriv a {[]} = {}"
+ and Deriv_char[simp]: "Deriv a {[b]} = (if a = b then {[]} else {})"
+ and Deriv_union[simp]: "Deriv a (A \<union> B) = Deriv a A \<union> Deriv a B"
+by (auto simp: Deriv_def)
-lemma Der_simps [simp]:
- shows "Der c {} = {}"
- and "Der c {[]} = {}"
- and "Der c {[d]} = (if c = d then {[]} else {})"
- and "Der c (A \<union> B) = Der c A \<union> Der c B"
-unfolding Der_def by auto
+lemma Deriv_conc_subset:
+"Deriv a A @@ B \<subseteq> Deriv a (A @@ B)" (is "?L \<subseteq> ?R")
+proof
+ fix w assume "w \<in> ?L"
+ then obtain u v where "w = u @ v" "a # u \<in> A" "v \<in> B"
+ by (auto simp: Deriv_def)
+ then have "a # w \<in> A @@ B"
+ by (auto intro: concI[of "a # u", simplified])
+ thus "w \<in> ?R" by (auto simp: Deriv_def)
+qed
lemma Der_conc [simp]:
- shows "Der c (A \<cdot> B) = (Der c A) \<cdot> B \<union> (Delta A \<cdot> Der c B)"
-unfolding Der_def Delta_def conc_def
+ shows "Deriv c (A @@ B) = (Deriv c A) @@ B \<union> (if [] \<in> A then Deriv c B else {})"
+unfolding Deriv_def conc_def
by (auto simp add: Cons_eq_append_conv)
-lemma Der_star [simp]:
- shows "Der c (A\<star>) = (Der c A) \<cdot> A\<star>"
+lemma Deriv_star [simp]:
+ shows "Deriv c (star A) = (Deriv c A) @@ star A"
proof -
- have incl: "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>"
- unfolding Der_def Delta_def conc_def
- apply(auto)
+ have incl: "[] \<in> A \<Longrightarrow> Deriv c (star A) \<subseteq> (Deriv c A) @@ star A"
+ unfolding Deriv_def conc_def
+ apply(auto simp add: Cons_eq_append_conv)
apply(drule star_decom)
apply(auto simp add: Cons_eq_append_conv)
done
-
- have "Der c (A\<star>) = Der c (A \<cdot> A\<star> \<union> {[]})"
+
+ have "Deriv c (star A) = Deriv c (A @@ star A \<union> {[]})"
by (simp only: star_unfold_left[symmetric])
- also have "... = Der c (A \<cdot> A\<star>)"
- by (simp only: Der_simps) (simp)
- also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))"
+ also have "... = Deriv c (A @@ star A)"
+ by (simp only: Deriv_union) (simp)
+ also have "... = (Deriv c A) @@ (star A) \<union> (if [] \<in> A then Deriv c (star A) else {})"
by simp
- also have "... = (Der c A) \<cdot> A\<star>"
+ also have "... = (Deriv c A) @@ star A"
using incl by auto
- finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" .
+ finally show "Deriv c (star A) = (Deriv c A) @@ star A" .
qed
-lemma Ders_simps [simp]:
- shows "Ders [] A = A"
- and "Ders (c # s) A = Ders s (Der c A)"
- and "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"
-unfolding Ders_def Der_def by auto
+lemma Derivs_simps [simp]:
+ shows "Derivs [] A = A"
+ and "Derivs (c # s) A = Derivs s (Deriv c A)"
+ and "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)"
+unfolding Derivs_def Deriv_def by auto
+
+(*
+lemma Deriv_insert_eps[simp]:
+"Deriv a (insert [] A) = Deriv a A"
+by (auto simp: Deriv_def)
+*)
+
+
subsection {* Brozowsky's derivatives of regular expressions *}
@@ -76,247 +90,254 @@
| "nullable (Star r) = True"
fun
- der :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
+ deriv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
where
- "der c (Zero) = Zero"
-| "der c (One) = Zero"
-| "der c (Atom c') = (if c = c' then One else Zero)"
-| "der c (Plus r1 r2) = Plus (der c r1) (der c r2)"
-| "der c (Times r1 r2) =
- (if nullable r1 then Plus (Times (der c r1) r2) (der c r2) else Times (der c r1) r2)"
-| "der c (Star r) = Times (der c r) (Star r)"
+ "deriv c (Zero) = Zero"
+| "deriv c (One) = Zero"
+| "deriv c (Atom c') = (if c = c' then One else Zero)"
+| "deriv c (Plus r1 r2) = Plus (deriv c r1) (deriv c r2)"
+| "deriv c (Times r1 r2) =
+ (if nullable r1 then Plus (Times (deriv c r1) r2) (deriv c r2) else Times (deriv c r1) r2)"
+| "deriv c (Star r) = Times (deriv c r) (Star r)"
fun
- ders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
+ derivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
where
- "ders [] r = r"
-| "ders (c # s) r = ders s (der c r)"
+ "derivs [] r = r"
+| "derivs (c # s) r = derivs s (deriv c r)"
-lemma Delta_nullable:
- shows "Delta (lang r) = (if nullable r then {[]} else {})"
-unfolding Delta_def
+lemma nullable_iff:
+ shows "nullable r \<longleftrightarrow> [] \<in> lang r"
by (induct r) (auto simp add: conc_def split: if_splits)
-lemma Der_der:
- shows "Der c (lang r) = lang (der c r)"
-by (induct r) (simp_all add: Delta_nullable)
+lemma Deriv_deriv:
+ shows "Deriv c (lang r) = lang (deriv c r)"
+by (induct r) (simp_all add: nullable_iff)
-lemma Ders_ders:
- shows "Ders s (lang r) = lang (ders s r)"
-by (induct s arbitrary: r) (simp_all add: Der_der)
+lemma Derivs_derivs:
+ shows "Derivs s (lang r) = lang (derivs s r)"
+by (induct s arbitrary: r) (simp_all add: Deriv_deriv)
-subsection {* Antimirov's Partial Derivatives *}
+subsection {* Antimirov's partial derivivatives *}
abbreviation
"Timess rs r \<equiv> {Times r' r | r'. r' \<in> rs}"
fun
- pder :: "'a \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
+ pderiv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set"
where
- "pder c Zero = {}"
-| "pder c One = {}"
-| "pder c (Atom c') = (if c = c' then {One} else {})"
-| "pder c (Plus r1 r2) = (pder c r1) \<union> (pder c r2)"
-| "pder c (Times r1 r2) =
- (if nullable r1 then Timess (pder c r1) r2 \<union> pder c r2 else Timess (pder c r1) r2)"
-| "pder c (Star r) = Timess (pder c r) (Star r)"
-
-abbreviation
- "pder_set c rs \<equiv> \<Union> pder c ` rs"
+ "pderiv c Zero = {}"
+| "pderiv c One = {}"
+| "pderiv c (Atom c') = (if c = c' then {One} else {})"
+| "pderiv c (Plus r1 r2) = (pderiv c r1) \<union> (pderiv c r2)"
+| "pderiv c (Times r1 r2) =
+ (if nullable r1 then Timess (pderiv c r1) r2 \<union> pderiv c r2 else Timess (pderiv c r1) r2)"
+| "pderiv c (Star r) = Timess (pderiv c r) (Star r)"
fun
- pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
+ pderivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
where
- "pders [] r = {r}"
-| "pders (c # s) r = \<Union> (pders s) ` (pder c r)"
+ "pderivs [] r = {r}"
+| "pderivs (c # s) r = \<Union> (pderivs s) ` (pderiv c r)"
abbreviation
- "pderss s A \<equiv> \<Union> (pders s) ` A"
+ pderiv_set :: "'a \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set"
+where
+ "pderiv_set c rs \<equiv> \<Union> pderiv c ` rs"
-lemma pders_append:
- "pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)"
+abbreviation
+ pderivs_set :: "'a list \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set"
+where
+ "pderivs_set s rs \<equiv> \<Union> (pderivs s) ` rs"
+
+lemma pderivs_append:
+ "pderivs (s1 @ s2) r = \<Union> (pderivs s2) ` (pderivs s1 r)"
by (induct s1 arbitrary: r) (simp_all)
-lemma pders_snoc:
- shows "pders (s @ [c]) r = pder_set c (pders s r)"
-by (simp add: pders_append)
+lemma pderivs_snoc:
+ shows "pderivs (s @ [c]) r = pderiv_set c (pderivs s r)"
+by (simp add: pderivs_append)
-lemma pders_simps [simp]:
- shows "pders s Zero = (if s= [] then {Zero} else {})"
- and "pders s One = (if s = [] then {One} else {})"
- and "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))"
+lemma pderivs_simps [simp]:
+ shows "pderivs s Zero = (if s = [] then {Zero} else {})"
+ and "pderivs s One = (if s = [] then {One} else {})"
+ and "pderivs s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pderivs s r1) \<union> (pderivs s r2))"
by (induct s) (simp_all)
-lemma pders_Atom [intro]:
- shows "pders s (Atom c) \<subseteq> {Atom c, One}"
+lemma pderivs_Atom:
+ shows "pderivs s (Atom c) \<subseteq> {Atom c, One}"
by (induct s) (simp_all)
-subsection {* Relating left-quotients and partial derivatives *}
+subsection {* Relating left-quotients and partial derivivatives *}
-lemma Der_pder:
- shows "Der c (lang r) = \<Union> lang ` (pder c r)"
-by (induct r) (auto simp add: Delta_nullable conc_UNION_distrib)
+lemma Deriv_pderiv:
+ shows "Deriv c (lang r) = \<Union> lang ` (pderiv c r)"
+by (induct r) (auto simp add: nullable_iff conc_UNION_distrib)
-lemma Ders_pders:
- shows "Ders s (lang r) = \<Union> lang ` (pders s r)"
+lemma Derivs_pderivs:
+ shows "Derivs s (lang r) = \<Union> lang ` (pderivs s r)"
proof (induct s arbitrary: r)
case (Cons c s)
- have ih: "\<And>r. Ders s (lang r) = \<Union> lang ` (pders s r)" by fact
- have "Ders (c # s) (lang r) = Ders s (Der c (lang r))" by simp
- also have "\<dots> = Ders s (\<Union> lang ` (pder c r))" by (simp add: Der_pder)
- also have "\<dots> = Derss s (lang ` (pder c r))"
- by (auto simp add: Ders_def)
- also have "\<dots> = \<Union> lang ` (pderss s (pder c r))"
+ have ih: "\<And>r. Derivs s (lang r) = \<Union> lang ` (pderivs s r)" by fact
+ have "Derivs (c # s) (lang r) = Derivs s (Deriv c (lang r))" by simp
+ also have "\<dots> = Derivs s (\<Union> lang ` (pderiv c r))" by (simp add: Deriv_pderiv)
+ also have "\<dots> = Derivss s (lang ` (pderiv c r))"
+ by (auto simp add: Derivs_def)
+ also have "\<dots> = \<Union> lang ` (pderivs_set s (pderiv c r))"
using ih by auto
- also have "\<dots> = \<Union> lang ` (pders (c # s) r)" by simp
- finally show "Ders (c # s) (lang r) = \<Union> lang ` pders (c # s) r" .
-qed (simp add: Ders_def)
+ also have "\<dots> = \<Union> lang ` (pderivs (c # s) r)" by simp
+ finally show "Derivs (c # s) (lang r) = \<Union> lang ` pderivs (c # s) r" .
+qed (simp add: Derivs_def)
-subsection {* Relating derivatives and partial derivatives *}
+subsection {* Relating derivivatives and partial derivivatives *}
-lemma der_pder:
- shows "(\<Union> lang ` (pder c r)) = lang (der c r)"
-unfolding Der_der[symmetric] Der_pder by simp
+lemma deriv_pderiv:
+ shows "(\<Union> lang ` (pderiv c r)) = lang (deriv c r)"
+unfolding Deriv_deriv[symmetric] Deriv_pderiv by simp
-lemma ders_pders:
- shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"
-unfolding Ders_ders[symmetric] Ders_pders by simp
+lemma derivs_pderivs:
+ shows "(\<Union> lang ` (pderivs s r)) = lang (derivs s r)"
+unfolding Derivs_derivs[symmetric] Derivs_pderivs by simp
-subsection {* There are only finitely many partial derivatives for a language *}
+subsection {* Finiteness property of partial derivivatives *}
definition
- "pders_lang A r \<equiv> \<Union>x \<in> A. pders x r"
-
-lemma pders_lang_subsetI [intro]:
- assumes "\<And>s. s \<in> A \<Longrightarrow> pders s r \<subseteq> C"
- shows "pders_lang A r \<subseteq> C"
-using assms unfolding pders_lang_def by (rule UN_least)
+ pderivs_lang :: "'a lang \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set"
+where
+ "pderivs_lang A r \<equiv> \<Union>x \<in> A. pderivs x r"
-lemma pders_lang_union:
- shows "pders_lang (A \<union> B) r = (pders_lang A r \<union> pders_lang B r)"
-by (simp add: pders_lang_def)
+lemma pderivs_lang_subsetI:
+ assumes "\<And>s. s \<in> A \<Longrightarrow> pderivs s r \<subseteq> C"
+ shows "pderivs_lang A r \<subseteq> C"
+using assms unfolding pderivs_lang_def by (rule UN_least)
-lemma pders_lang_subset:
- shows "A \<subseteq> B \<Longrightarrow> pders_lang A r \<subseteq> pders_lang B r"
-by (auto simp add: pders_lang_def)
+lemma pderivs_lang_union:
+ shows "pderivs_lang (A \<union> B) r = (pderivs_lang A r \<union> pderivs_lang B r)"
+by (simp add: pderivs_lang_def)
+
+lemma pderivs_lang_subset:
+ shows "A \<subseteq> B \<Longrightarrow> pderivs_lang A r \<subseteq> pderivs_lang B r"
+by (auto simp add: pderivs_lang_def)
definition
"UNIV1 \<equiv> UNIV - {[]}"
-lemma pders_lang_Zero [simp]:
- shows "pders_lang UNIV1 Zero = {}"
-unfolding UNIV1_def pders_lang_def by auto
+lemma pderivs_lang_Zero [simp]:
+ shows "pderivs_lang UNIV1 Zero = {}"
+unfolding UNIV1_def pderivs_lang_def by auto
-lemma pders_lang_One [simp]:
- shows "pders_lang UNIV1 One = {}"
-unfolding UNIV1_def pders_lang_def by (auto split: if_splits)
+lemma pderivs_lang_One [simp]:
+ shows "pderivs_lang UNIV1 One = {}"
+unfolding UNIV1_def pderivs_lang_def by (auto split: if_splits)
-lemma pders_lang_Atom [simp]:
- shows "pders_lang UNIV1 (Atom c) = {One}"
-unfolding UNIV1_def pders_lang_def
+lemma pderivs_lang_Atom [simp]:
+ shows "pderivs_lang UNIV1 (Atom c) = {One}"
+unfolding UNIV1_def pderivs_lang_def
apply(auto)
apply(frule rev_subsetD)
-apply(rule pders_Atom)
+apply(rule pderivs_Atom)
apply(simp)
apply(case_tac xa)
apply(auto split: if_splits)
done
-lemma pders_lang_Plus [simp]:
- shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \<union> pders_lang UNIV1 r2"
-unfolding UNIV1_def pders_lang_def by auto
+lemma pderivs_lang_Plus [simp]:
+ shows "pderivs_lang UNIV1 (Plus r1 r2) = pderivs_lang UNIV1 r1 \<union> pderivs_lang UNIV1 r2"
+unfolding UNIV1_def pderivs_lang_def by auto
text {* Non-empty suffixes of a string (needed for teh cases of @{const Times} and @{const Star} *}
definition
- "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
+ "PSuf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
-lemma Suf_snoc:
- shows "Suf (s @ [c]) = (Suf s) \<cdot> {[c]} \<union> {[c]}"
-unfolding Suf_def conc_def
+lemma PSuf_snoc:
+ shows "PSuf (s @ [c]) = (PSuf s) @@ {[c]} \<union> {[c]}"
+unfolding PSuf_def conc_def
by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv)
-lemma Suf_Union:
- shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. f v) = (\<Union>v \<in> Suf s. f (v @ [c]))"
+lemma PSuf_Union:
+ shows "(\<Union>v \<in> PSuf s @@ {[c]}. f v) = (\<Union>v \<in> PSuf s. f (v @ [c]))"
by (auto simp add: conc_def)
-lemma pders_lang_snoc:
- shows "pders_lang (Suf s \<cdot> {[c]}) r = (pder_set c (pders_lang (Suf s) r))"
-unfolding pders_lang_def
-by (simp add: Suf_Union pders_snoc)
+lemma pderivs_lang_snoc:
+ shows "pderivs_lang (PSuf s @@ {[c]}) r = (pderiv_set c (pderivs_lang (PSuf s) r))"
+unfolding pderivs_lang_def
+by (simp add: PSuf_Union pderivs_snoc)
-lemma pders_Times:
- shows "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2)"
+lemma pderivs_Times:
+ shows "pderivs s (Times r1 r2) \<subseteq> Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2)"
proof (induct s rule: rev_induct)
case (snoc c s)
- have ih: "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2)"
+ have ih: "pderivs s (Times r1 r2) \<subseteq> Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2)"
by fact
- have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))"
- by (simp add: pders_snoc)
- also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2))"
+ have "pderivs (s @ [c]) (Times r1 r2) = pderiv_set c (pderivs s (Times r1 r2))"
+ by (simp add: pderivs_snoc)
+ also have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2))"
using ih by (auto) (blast)
- also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pder_set c (pders_lang (Suf s) r2)"
+ also have "\<dots> = pderiv_set c (Timess (pderivs s r1) r2) \<union> pderiv_set c (pderivs_lang (PSuf s) r2)"
by (simp)
- also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
- by (simp add: pders_lang_snoc)
- also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2) \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
+ also have "\<dots> = pderiv_set c (Timess (pderivs s r1) r2) \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
+ by (simp add: pderivs_lang_snoc)
+ also
+ have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs s r1) r2) \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
by auto
- also have "\<dots> \<subseteq> Timess (pder_set c (pders s r1)) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
+ also
+ have "\<dots> \<subseteq> Timess (pderiv_set c (pderivs s r1)) r2 \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
by (auto simp add: if_splits) (blast)
- also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
- by (simp add: pders_snoc)
- also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pders_lang (Suf (s @ [c])) r2"
- unfolding pders_lang_def by (auto simp add: Suf_snoc)
+ also have "\<dots> = Timess (pderivs (s @ [c]) r1) r2 \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
+ by (simp add: pderivs_snoc)
+ also have "\<dots> \<subseteq> Timess (pderivs (s @ [c]) r1) r2 \<union> pderivs_lang (PSuf (s @ [c])) r2"
+ unfolding pderivs_lang_def by (auto simp add: PSuf_snoc)
finally show ?case .
qed (simp)
-lemma pders_lang_Times_aux1:
+lemma pderivs_lang_Times_aux1:
assumes a: "s \<in> UNIV1"
- shows "pders_lang (Suf s) r \<subseteq> pders_lang UNIV1 r"
-using a unfolding UNIV1_def Suf_def pders_lang_def by auto
+ shows "pderivs_lang (PSuf s) r \<subseteq> pderivs_lang UNIV1 r"
+using a unfolding UNIV1_def PSuf_def pderivs_lang_def by auto
-lemma pders_lang_Times_aux2:
+lemma pderivs_lang_Times_aux2:
assumes a: "s \<in> UNIV1"
- shows "Timess (pders s r1) r2 \<subseteq> Timess (pders_lang UNIV1 r1) r2"
-using a unfolding pders_lang_def by auto
+ shows "Timess (pderivs s r1) r2 \<subseteq> Timess (pderivs_lang UNIV1 r1) r2"
+using a unfolding pderivs_lang_def by auto
-lemma pders_lang_Times [intro]:
- shows "pders_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pders_lang UNIV1 r1) r2 \<union> pders_lang UNIV1 r2"
-apply(rule pders_lang_subsetI)
+lemma pderivs_lang_Times:
+ shows "pderivs_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pderivs_lang UNIV1 r1) r2 \<union> pderivs_lang UNIV1 r2"
+apply(rule pderivs_lang_subsetI)
apply(rule subset_trans)
-apply(rule pders_Times)
-using pders_lang_Times_aux1 pders_lang_Times_aux2
+apply(rule pderivs_Times)
+using pderivs_lang_Times_aux1 pderivs_lang_Times_aux2
apply(blast)
done
-lemma pders_Star:
+lemma pderivs_Star:
assumes a: "s \<noteq> []"
- shows "pders s (Star r) \<subseteq> Timess (pders_lang (Suf s) r) (Star r)"
+ shows "pderivs s (Star r) \<subseteq> Timess (pderivs_lang (PSuf s) r) (Star r)"
using a
proof (induct s rule: rev_induct)
case (snoc c s)
- have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> Timess (pders_lang (Suf s) r) (Star r)" by fact
+ have ih: "s \<noteq> [] \<Longrightarrow> pderivs s (Star r) \<subseteq> Timess (pderivs_lang (PSuf s) r) (Star r)" by fact
{ assume asm: "s \<noteq> []"
- have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc)
- also have "\<dots> \<subseteq> pder_set c (Timess (pders_lang (Suf s) r) (Star r))"
+ have "pderivs (s @ [c]) (Star r) = pderiv_set c (pderivs s (Star r))" by (simp add: pderivs_snoc)
+ also have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs_lang (PSuf s) r) (Star r))"
using ih[OF asm] by (auto) (blast)
- also have "\<dots> \<subseteq> Timess (pder_set c (pders_lang (Suf s) r)) (Star r) \<union> pder c (Star r)"
+ also have "\<dots> \<subseteq> Timess (pderiv_set c (pderivs_lang (PSuf s) r)) (Star r) \<union> pderiv c (Star r)"
by (auto split: if_splits) (blast)+
- also have "\<dots> \<subseteq> Timess (pders_lang (Suf (s @ [c])) r) (Star r) \<union> (Timess (pder c r) (Star r))"
- by (simp only: Suf_snoc pders_lang_snoc pders_lang_union)
- (auto simp add: pders_lang_def)
- also have "\<dots> = Timess (pders_lang (Suf (s @ [c])) r) (Star r)"
- by (auto simp add: Suf_snoc Suf_Union pders_snoc pders_lang_def)
+ also have "\<dots> \<subseteq> Timess (pderivs_lang (PSuf (s @ [c])) r) (Star r) \<union> (Timess (pderiv c r) (Star r))"
+ by (simp only: PSuf_snoc pderivs_lang_snoc pderivs_lang_union)
+ (auto simp add: pderivs_lang_def)
+ also have "\<dots> = Timess (pderivs_lang (PSuf (s @ [c])) r) (Star r)"
+ by (auto simp add: PSuf_snoc PSuf_Union pderivs_snoc pderivs_lang_def)
finally have ?case .
}
moreover
{ assume asm: "s = []"
then have ?case
- apply (auto simp add: pders_lang_def pders_snoc Suf_def)
+ apply (auto simp add: pderivs_lang_def pderivs_snoc PSuf_def)
apply(rule_tac x = "[c]" in exI)
apply(auto)
done
@@ -324,14 +345,14 @@
ultimately show ?case by blast
qed (simp)
-lemma pders_lang_Star [intro]:
- shows "pders_lang UNIV1 (Star r) \<subseteq> Timess (pders_lang UNIV1 r) (Star r)"
-apply(rule pders_lang_subsetI)
+lemma pderivs_lang_Star:
+ shows "pderivs_lang UNIV1 (Star r) \<subseteq> Timess (pderivs_lang UNIV1 r) (Star r)"
+apply(rule pderivs_lang_subsetI)
apply(rule subset_trans)
-apply(rule pders_Star)
+apply(rule pderivs_Star)
apply(simp add: UNIV1_def)
-apply(simp add: UNIV1_def Suf_def)
-apply(auto simp add: pders_lang_def)
+apply(simp add: UNIV1_def PSuf_def)
+apply(auto simp add: pderivs_lang_def)
done
lemma finite_Timess [simp]:
@@ -339,72 +360,27 @@
shows "finite (Timess A r)"
using a by auto
-lemma finite_pders_lang_UNIV1:
- shows "finite (pders_lang UNIV1 r)"
+lemma finite_pderivs_lang_UNIV1:
+ shows "finite (pderivs_lang UNIV1 r)"
apply(induct r)
apply(simp_all add:
- finite_subset[OF pders_lang_Times]
- finite_subset[OF pders_lang_Star])
+ finite_subset[OF pderivs_lang_Times]
+ finite_subset[OF pderivs_lang_Star])
done
-lemma pders_lang_UNIV:
- shows "pders_lang UNIV r = pders [] r \<union> pders_lang UNIV1 r"
-unfolding UNIV1_def pders_lang_def
+lemma pderivs_lang_UNIV:
+ shows "pderivs_lang UNIV r = pderivs [] r \<union> pderivs_lang UNIV1 r"
+unfolding UNIV1_def pderivs_lang_def
by blast
-lemma finite_pders_lang_UNIV:
- shows "finite (pders_lang UNIV r)"
-unfolding pders_lang_UNIV
-by (simp add: finite_pders_lang_UNIV1)
-
-lemma finite_pders_lang:
- shows "finite (pders_lang A r)"
-apply(rule rev_finite_subset[OF finite_pders_lang_UNIV])
-apply(rule pders_lang_subset)
-apply(simp)
-done
-
-text {* Relating the Myhill-Nerode relation with left-quotients. *}
-
-lemma MN_Rel_Ders:
- shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A"
-unfolding Ders_def str_eq_def
-by auto
-
-subsection {*
- The second direction of the Myhill-Nerode theorem using
- partial derivatives.
-*}
+lemma finite_pderivs_lang_UNIV:
+ shows "finite (pderivs_lang UNIV r)"
+unfolding pderivs_lang_UNIV
+by (simp add: finite_pderivs_lang_UNIV1)
-lemma Myhill_Nerode3:
- fixes r::"'a rexp"
- shows "finite (UNIV // \<approx>(lang r))"
-proof -
- have "finite (UNIV // =(\<lambda>x. pders x r)=)"
- proof -
- have "range (\<lambda>x. pders x r) \<subseteq> Pow (pders_lang UNIV r)"
- unfolding pders_lang_def by auto
- moreover
- have "finite (Pow (pders_lang UNIV r))" by (simp add: finite_pders_lang)
- ultimately
- have "finite (range (\<lambda>x. pders x r))"
- by (simp add: finite_subset)
- then show "finite (UNIV // =(\<lambda>x. pders x r)=)"
- by (rule finite_eq_tag_rel)
- qed
- moreover
- have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(lang r)"
- unfolding tag_eq_def
- by (auto simp add: MN_Rel_Ders Ders_pders)
- moreover
- have "equiv UNIV =(\<lambda>x. pders x r)="
- and "equiv UNIV (\<approx>(lang r))"
- unfolding equiv_def refl_on_def sym_def trans_def
- unfolding tag_eq_def str_eq_def
- by auto
- ultimately show "finite (UNIV // \<approx>(lang r))"
- by (rule refined_partition_finite)
-qed
+lemma finite_pderivs_lang:
+ shows "finite (pderivs_lang A r)"
+by (metis finite_pderivs_lang_UNIV pderivs_lang_subset rev_finite_subset subset_UNIV)
end
\ No newline at end of file
--- a/Folds.thy Fri Aug 19 20:39:07 2011 +0000
+++ b/Folds.thy Mon Aug 22 12:49:27 2011 +0000
@@ -1,8 +1,8 @@
theory Folds
-imports Main
+imports "Regular_Exp"
begin
-section {* Folds for Sets *}
+section {* ``Summation'' for regular expressions *}
text {*
To obtain equational system out of finite set of equivalence classes, a fold operation
@@ -18,5 +18,27 @@
where
"folds f z S \<equiv> SOME x. fold_graph f z S x"
+text {* Plus-combination for a set of regular expressions *}
+
+abbreviation
+ Setalt :: "'a rexp set \<Rightarrow> 'a rexp" ("\<Uplus>_" [1000] 999)
+where
+ "\<Uplus>A \<equiv> folds Plus Zero A"
+
+text {*
+ For finite sets, @{term Setalt} is preserved under @{term lang}.
+*}
+
+lemma folds_plus_simp [simp]:
+ fixes rs::"('a rexp) set"
+ assumes a: "finite rs"
+ shows "lang (\<Uplus>rs) = \<Union> (lang ` 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
--- a/IsaMakefile Fri Aug 19 20:39:07 2011 +0000
+++ b/IsaMakefile Mon Aug 22 12:49:27 2011 +0000
@@ -19,13 +19,25 @@
session1: Slides/ROOT.ML \
Slides/document/root* \
Slides/Slides.thy
- @$(USEDIR) -D generated -f ROOT.ML ListP tphols-2011
+ @$(USEDIR) -D generated -f ROOT.ML HOL Slides
slides: session1
rm -f Slides/generated/*.aux # otherwise latex will fall over
cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
cp Slides/generated/root.beamer.pdf Slides/slides.pdf
+## Slides
+
+session11: Slides/ROOT.ML \
+ Slides/document/root* \
+ Slides/Slides1.thy
+ @$(USEDIR) -D generated -f ROOT1.ML HOL Slides
+
+slides1: session11
+ rm -f Slides/generated/*.aux # otherwise latex will fall over
+ cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+ cp Slides/generated/root.beamer.pdf Slides/slides1.pdf
+
## long paper
--- a/Journal/Paper.thy Fri Aug 19 20:39:07 2011 +0000
+++ b/Journal/Paper.thy Mon Aug 22 12:49:27 2011 +0000
@@ -37,6 +37,10 @@
abbreviation "TIMESS \<equiv> Timess"
abbreviation "STAR \<equiv> Star"
+definition
+ Delta :: "'a lang \<Rightarrow> 'a lang"
+where
+ "Delta A = (if [] \<in> A then {[]} else {})"
notation (latex output)
str_eq ("\<approx>\<^bsub>_\<^esub>") and
@@ -71,12 +75,32 @@
nullable ("\<delta>'(_')") and
Cons ("_ :: _" [100, 100] 100) and
Rev ("Rev _" [1000] 100) and
- Der ("Der _ _" [1000, 1000] 100) and
+ Deriv ("Der _ _" [1000, 1000] 100) and
+ Derivs ("Ders") and
ONE ("ONE" 999) and
ZERO ("ZERO" 999) and
- pders_lang ("pdersl") and
+ pderivs_lang ("pdersl") and
UNIV1 ("UNIV\<^isup>+") and
- Ders_lang ("Dersl")
+ Deriv_lang ("Dersl") and
+ deriv ("der") and
+ derivs ("ders") and
+ pderiv ("pder") and
+ pderivs ("pders") and
+ pderivs_set ("pderss")
+
+
+lemmas Deriv_simps = Deriv_empty Deriv_epsilon Deriv_char Deriv_union
+
+definition
+ Der :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where
+ "Der c A \<equiv> {s. [c] @ s \<in> A}"
+
+definition
+ Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where
+ "Ders s A \<equiv> {s'. s @ s' \<in> A}"
+
lemma meta_eq_app:
shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
@@ -133,6 +157,27 @@
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
"_asm" :: "prop \<Rightarrow> asms" ("_")
+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
(*>*)
@@ -445,25 +490,25 @@
\mbox{@{term "X \<cdot> A"}}).
\begin{lmm}[Reversed Arden's Lemma]\label{arden}\mbox{}\\
- If @{thm (prem 1) arden} then
- @{thm (lhs) arden} if and only if
- @{thm (rhs) arden}.
+ If @{thm (prem 1) reversed_Arden} then
+ @{thm (lhs) reversed_Arden} if and only if
+ @{thm (rhs) reversed_Arden}.
\end{lmm}
\begin{proof}
- For the right-to-left direction we assume @{thm (rhs) arden} and show
- that @{thm (lhs) arden} holds. From Property~\ref{langprops}@{text "(i)"}
+ For the right-to-left direction we assume @{thm (rhs) reversed_Arden} and show
+ that @{thm (lhs) reversed_Arden} holds. From Property~\ref{langprops}@{text "(i)"}
we have @{term "A\<star> = A \<cdot> A\<star> \<union> {[]}"},
which is equal to @{term "A\<star> = A\<star> \<cdot> A \<union> {[]}"}. Adding @{text B} to both
sides gives @{term "B \<cdot> A\<star> = B \<cdot> (A\<star> \<cdot> A \<union> {[]})"}, whose right-hand side
is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. Applying the assumed equation
completes this direction.
- For the other direction we assume @{thm (lhs) arden}. By a simple induction
+ For the other direction we assume @{thm (lhs) reversed_Arden}. By a simple induction
on @{text n}, we can establish the property
\begin{center}
- @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper}
+ @{text "(*)"}\hspace{5mm} @{thm (concl) reversed_arden_helper}
\end{center}
\noindent
@@ -471,12 +516,12 @@
all @{text n}. From this we can infer @{term "B \<cdot> A\<star> \<subseteq> X"} using the definition
of @{text "\<star>"}.
For the inclusion in the other direction we assume a string @{text s}
- with length @{text k} is an element in @{text X}. Since @{thm (prem 1) arden}
+ with length @{text k} is an element in @{text X}. Since @{thm (prem 1) reversed_Arden}
we know by Property~\ref{langprops}@{text "(ii)"} that
@{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}
(the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer).
From @{text "(*)"} it follows then that
- @{term s} must be an element in @{term "(\<Union>m\<in>{0..k}. B \<cdot> (A \<up> m))"}. This in turn
+ @{term s} must be an element in @{term "(\<Union>m\<le>k. B \<cdot> (A \<up> m))"}. This in turn
implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Property~\ref{langprops}@{text "(iii)"}
this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.
\end{proof}
@@ -520,7 +565,7 @@
set @{text rs} with @{const ZERO} for the empty set. We can prove that for a finite set @{text rs}
%
\begin{equation}\label{uplus}
- \mbox{@{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}}
+ \mbox{@{thm (lhs) folds_plus_simp} @{text "= \<Union> (\<calL> ` rs)"}}
\end{equation}
\noindent
@@ -1574,7 +1619,7 @@
relation by using derivatives of regular expressions~\cite{Brzozowski64}.
Assume the following two definitions for the \emph{left-quotient} of a language,
- which we write as @{term "Der c A"} and @{term "Ders s A"} where @{text c}
+ which we write as @{term "Deriv c A"} and @{term "Derivs s A"} where @{text c}
is a character and @{text s} a string, respectively:
\begin{center}
@@ -1588,7 +1633,7 @@
In order to aid readability, we shall make use of the following abbreviation
\begin{center}
- @{abbrev "Derss s As"}
+ @{abbrev "Derivss s As"}
\end{center}
\noindent
@@ -1597,7 +1642,7 @@
(Definition~\ref{myhillneroderel}) and left-quotients
\begin{equation}\label{mhders}
- @{term "x \<approx>A y"} \hspace{4mm}\text{if and only if}\hspace{4mm} @{term "Ders x A = Ders y A"}
+ @{term "x \<approx>A y"} \hspace{4mm}\text{if and only if}\hspace{4mm} @{term "Derivs x A = Derivs y A"}
\end{equation}
\noindent
@@ -1605,16 +1650,16 @@
\begin{equation}
\mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{2mm}}l}
- @{thm (lhs) Der_simps(1)} & $=$ & @{thm (rhs) Der_simps(1)}\\
- @{thm (lhs) Der_simps(2)} & $=$ & @{thm (rhs) Der_simps(2)}\\
- @{thm (lhs) Der_simps(3)} & $=$ & @{thm (rhs) Der_simps(3)}\\
- @{thm (lhs) Der_simps(4)} & $=$ & @{thm (rhs) Der_simps(4)}\\
+ @{thm (lhs) Deriv_simps(1)} & $=$ & @{thm (rhs) Deriv_simps(1)}\\
+ @{thm (lhs) Deriv_simps(2)} & $=$ & @{thm (rhs) Deriv_simps(2)}\\
+ @{thm (lhs) Deriv_simps(3)} & $=$ & @{thm (rhs) Deriv_simps(3)}\\
+ @{thm (lhs) Deriv_simps(4)} & $=$ & @{thm (rhs) Deriv_simps(4)}\\
@{thm (lhs) Der_conc} & $=$ & @{thm (rhs) Der_conc}\\
- @{thm (lhs) Der_star} & $=$ & @{thm (rhs) Der_star}\\
- @{thm (lhs) Ders_simps(1)} & $=$ & @{thm (rhs) Ders_simps(1)}\\
- @{thm (lhs) Ders_simps(2)} & $=$ & @{thm (rhs) Ders_simps(2)}\\
- %@{thm (lhs) Ders_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]} & $=$
- % & @{thm (rhs) Ders_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}\\
+ @{thm (lhs) Deriv_star} & $=$ & @{thm (rhs) Deriv_star}\\
+ @{thm (lhs) Derivs_simps(1)} & $=$ & @{thm (rhs) Derivs_simps(1)}\\
+ @{thm (lhs) Derivs_simps(2)} & $=$ & @{thm (rhs) Derivs_simps(2)}\\
+ %@{thm (lhs) Derivs_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]} & $=$
+ % & @{thm (rhs) Derivs_simps(3)[where ?s1.0="s\<^isub>1" and ?s2.0="s\<^isub>2"]}\\
\end{tabular}}
\end{equation}
@@ -1624,8 +1669,8 @@
accordingly. Note also that in the last equation we use the list-cons operator written
\mbox{@{text "_ :: _"}}. The only interesting case is the case of @{term "A\<star>"}
where we use Property~\ref{langprops}@{text "(i)"} in order to infer that
- @{term "Der c (A\<star>) = Der c (A \<cdot> A\<star>)"}. We can then complete the proof by
- using the fifth equation and noting that @{term "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der
+ @{term "Deriv c (A\<star>) = Deriv c (A \<cdot> A\<star>)"}. We can then complete the proof by
+ using the fifth equation and noting that @{term "Delta A \<cdot> Deriv c (A\<star>) \<subseteq> (Deriv
c A) \<cdot> A\<star>"}.
Brzozowski observed that the left-quotients for languages of
@@ -1635,19 +1680,19 @@
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
- @{thm (lhs) der.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) der.simps(1)}\\
- @{thm (lhs) der.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) der.simps(2)}\\
- @{thm (lhs) der.simps(3)[where c'="d"]} & @{text "\<equiv>"} & @{thm (rhs) der.simps(3)[where c'="d"]}\\
- @{thm (lhs) der.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
- & @{text "\<equiv>"} & @{thm (rhs) der.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
- @{thm (lhs) der.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+ @{thm (lhs) deriv.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(1)}\\
+ @{thm (lhs) deriv.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(2)}\\
+ @{thm (lhs) deriv.simps(3)[where c'="d"]} & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(3)[where c'="d"]}\\
+ @{thm (lhs) deriv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+ & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ @{thm (lhs) deriv.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
& @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%
- @{term "Plus (Times (der c r\<^isub>1) r\<^isub>2) (der c r\<^isub>2)"}\\
+ @{term "Plus (Times (deriv c r\<^isub>1) r\<^isub>2) (deriv c r\<^isub>2)"}\\
& & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%
- @{term "Times (der c r\<^isub>1) r\<^isub>2"}\\
- @{thm (lhs) der.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) der.simps(6)}\smallskip\\
- @{thm (lhs) ders.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) ders.simps(1)}\\
- @{thm (lhs) ders.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) ders.simps(2)}\\
+ @{term "Times (deriv c r\<^isub>1) r\<^isub>2"}\\
+ @{thm (lhs) deriv.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) deriv.simps(6)}\smallskip\\
+ @{thm (lhs) derivs.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) derivs.simps(1)}\\
+ @{thm (lhs) derivs.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) derivs.simps(2)}\\
\end{tabular}
\end{center}
@@ -1679,8 +1724,8 @@
\begin{equation}\label{Dersders}
\mbox{\begin{tabular}{c}
- @{thm Der_der}\\
- @{thm Ders_ders}
+ @{thm Deriv_deriv}\\
+ @{thm Derivs_derivs}
\end{tabular}}
\end{equation}
@@ -1691,14 +1736,14 @@
\begin{center}
@{term "x \<approx>(lang r) y"} \hspace{4mm}if and only if\hspace{4mm}
- @{term "lang (ders x r) = lang (ders y r)"}.
+ @{term "lang (derivs x r) = lang (derivs y r)"}.
\end{center}
\noindent
holds and hence
\begin{equation}
- @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "ders x r = ders y r"}
+ @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "derivs x r = derivs y r"}
\end{equation}
@@ -1743,19 +1788,19 @@
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
- @{thm (lhs) pder.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) pder.simps(1)}\\
- @{thm (lhs) pder.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) pder.simps(2)}\\
- @{thm (lhs) pder.simps(3)[where c'="d"]} & @{text "\<equiv>"} & @{thm (rhs) pder.simps(3)[where c'="d"]}\\
- @{thm (lhs) pder.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
- & @{text "\<equiv>"} & @{thm (rhs) pder.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
- @{thm (lhs) pder.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+ @{thm (lhs) pderiv.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(1)}\\
+ @{thm (lhs) pderiv.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(2)}\\
+ @{thm (lhs) pderiv.simps(3)[where c'="d"]} & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(3)[where c'="d"]}\\
+ @{thm (lhs) pderiv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
+ & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ @{thm (lhs) pderiv.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}
& @{text "\<equiv>"} & @{text "if"}~@{term "nullable r\<^isub>1"}~@{text "then"}~%
- @{term "(Timess (pder c r\<^isub>1) r\<^isub>2) \<union> (pder c r\<^isub>2)"}\\
+ @{term "(Timess (pderiv c r\<^isub>1) r\<^isub>2) \<union> (pderiv c r\<^isub>2)"}\\
& & \phantom{@{text "if"}~@{term "nullable r\<^isub>1"}~}@{text "else"}~%
- @{term "Timess (pder c r\<^isub>1) r\<^isub>2"}\\
- @{thm (lhs) pder.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) pder.simps(6)}\smallskip\\
- @{thm (lhs) pders.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) pders.simps(1)}\\
- @{thm (lhs) pders.simps(2)} & @{text "\<equiv>"} & @{text "\<Union> (pders s) ` (pder c r)"}\\
+ @{term "Timess (pderiv c r\<^isub>1) r\<^isub>2"}\\
+ @{thm (lhs) pderiv.simps(6)} & @{text "\<equiv>"} & @{thm (rhs) pderiv.simps(6)}\smallskip\\
+ @{thm (lhs) pderivs.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) pderivs.simps(1)}\\
+ @{thm (lhs) pderivs.simps(2)} & @{text "\<equiv>"} & @{text "\<Union> (pders s) ` (pder c r)"}\\
\end{tabular}
\end{center}
@@ -1773,19 +1818,19 @@
in order to `sequence' a regular expression with a set of regular
expressions. Note that in the last clause we first build the set of partial
derivatives w.r.t~the character @{text c}, then build the image of this set under the
- function @{term "pders s"} and finally `union up' all resulting sets. It will be
+ function @{term "pderivs s"} and finally `union up' all resulting sets. It will be
convenient to introduce for this the following abbreviation
\begin{center}
- @{abbrev "pderss s rs"}
+ @{abbrev "pderivs_set s rs"}
\end{center}
\noindent
- which simplifies the last clause of @{const "pders"} to
+ which simplifies the last clause of @{const "pderivs"} to
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1.5mm}}l@ {}}
- @{thm (lhs) pders.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) pders.simps(2)}\\
+ @{thm (lhs) pderivs.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) pderivs.simps(2)}\\
\end{tabular}
\end{center}
@@ -1797,8 +1842,8 @@
\begin{equation}\label{Derspders}
\mbox{\begin{tabular}{lc}
- @{text "(i)"} & @{thm Der_pder}\\
- @{text "(ii)"} & @{thm Ders_pders}
+ @{text "(i)"} & @{thm Deriv_pderiv}\\
+ @{text "(ii)"} & @{thm Derivs_pderivs}
\end{tabular}}
\end{equation}
@@ -1809,7 +1854,7 @@
induction hypothesis is
\begin{center}
- @{text "(IH)"}\hspace{3mm}@{term "\<forall>r. Ders s (lang r) = \<Union> lang ` (pders s r)"}
+ @{text "(IH)"}\hspace{3mm}@{term "\<forall>r. Derivs s (lang r) = \<Union> lang ` (pderivs s r)"}
\end{center}
\noindent
@@ -1817,12 +1862,12 @@
\begin{center}
\begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}ll}
- @{term "Ders (c # s) (lang r)"}
- & @{text "="} & @{term "Ders s (Der c (lang r))"} & by def.\\
- & @{text "="} & @{term "Ders s (\<Union> lang ` (pder c r))"} & by @{text "("}\ref{Derspders}@{text ".i)"}\\
- & @{text "="} & @{term "\<Union> (Ders s) ` (lang ` (pder c r))"} & by def.~of @{text "Ders"}\\
- & @{text "="} & @{term "\<Union> lang ` (\<Union> pders s ` (pder c r))"} & by IH\\
- & @{text "="} & @{term "\<Union> lang ` (pders (c # s) r)"} & by def.\\
+ @{term "Derivs (c # s) (lang r)"}
+ & @{text "="} & @{term "Derivs s (Deriv c (lang r))"} & by def.\\
+ & @{text "="} & @{term "Derivs s (\<Union> lang ` (pderiv c r))"} & by @{text "("}\ref{Derspders}@{text ".i)"}\\
+ & @{text "="} & @{term "\<Union> (Derivs s) ` (lang ` (pderiv c r))"} & by def.~of @{text "Ders"}\\
+ & @{text "="} & @{term "\<Union> lang ` (\<Union> pderivs s ` (pderiv c r))"} & by IH\\
+ & @{text "="} & @{term "\<Union> lang ` (pderivs (c # s) r)"} & by def.\\
\end{tabular}
\end{center}
@@ -1838,8 +1883,8 @@
\begin{equation}
\mbox{\begin{tabular}{lc}
- @{text "(i)"} & @{thm der_pder[symmetric]}\\
- @{text "(ii)"} & @{thm ders_pders[symmetric]}
+ @{text "(i)"} & @{thm deriv_pderiv[symmetric]}\\
+ @{text "(ii)"} & @{thm derivs_pderivs[symmetric]}
\end{tabular}}
\end{equation}
@@ -1853,12 +1898,12 @@
derivatives of @{text r} w.r.t.~a language @{text A} is defined as
\begin{equation}\label{Pdersdef}
- @{thm pders_lang_def}
+ @{thm pderivs_lang_def}
\end{equation}
\begin{thrm}[Antimirov \cite{Antimirov95}]\label{antimirov}
For every language @{text A} and every regular expression @{text r},
- \mbox{@{thm finite_pders_lang}}.
+ \mbox{@{thm finite_pderivs_lang}}.
\end{thrm}
\noindent
@@ -1867,12 +1912,12 @@
\begin{equation}\label{pdersunivone}
\mbox{\begin{tabular}{l}
- @{thm pders_lang_Zero}\\
- @{thm pders_lang_One}\\
- @{thm pders_lang_Atom}\\
- @{thm pders_lang_Plus[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
- @{thm pders_lang_Times[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
- @{thm pders_lang_Star}\\
+ @{thm pderivs_lang_Zero}\\
+ @{thm pderivs_lang_One}\\
+ @{thm pderivs_lang_Atom}\\
+ @{thm pderivs_lang_Plus[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ @{thm pderivs_lang_Times[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ @{thm pderivs_lang_Star}\\
\end{tabular}}
\end{equation}
@@ -1880,19 +1925,19 @@
from which one can deduce by induction on @{text r} that
\begin{center}
- @{thm finite_pders_lang_UNIV1}
+ @{thm finite_pderivs_lang_UNIV1}
\end{center}
\noindent
holds. Now Antimirov's theorem follows because
\begin{center}
- @{thm pders_lang_UNIV}\\
+ @{thm pderivs_lang_UNIV}\\
\end{center}
\noindent
- and for all languages @{text "A"}, @{term "pders_lang A r"} is a subset of
- @{term "pders_lang UNIV r"}. Since we follow Antimirov's proof quite
+ and for all languages @{text "A"}, @{term "pderivs_lang A r"} is a subset of
+ @{term "pderivs_lang UNIV r"}. Since we follow Antimirov's proof quite
closely in our formalisation (only the last two cases of
\eqref{pdersunivone} involve some non-routine induction arguments), we omit
the details.
@@ -1907,23 +1952,23 @@
and \eqref{Derspders} we can easily infer that
\begin{center}
- @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "pders x r = pders y r"}
+ @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "pderivs x r = pderivs y r"}
\end{center}
\noindent
which means the tagging-relation @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"} refines @{term "\<approx>(lang r)"}.
So we know by Lemma~\ref{fintwo}, \mbox{@{term "finite (UNIV // (\<approx>(lang r)))"}}
- holds if @{term "finite (UNIV // (=(\<lambda>x. pders x r)=))"}. In order to establish
+ holds if @{term "finite (UNIV // (=(\<lambda>x. pderivs x r)=))"}. In order to establish
the latter, we can use Lemma~\ref{finone} and show that the range of the
- tagging-function \mbox{@{term "\<lambda>x. pders x r"}} is finite. For this recall Definition
+ tagging-function \mbox{@{term "\<lambda>x. pderivs x r"}} is finite. For this recall Definition
\ref{Pdersdef}, which gives us that
\begin{center}
- @{thm pders_lang_def[where A="UNIV", simplified]}
+ @{thm pderivs_lang_def[where A="UNIV", simplified]}
\end{center}
\noindent
- Now the range of @{term "\<lambda>x. pders x r"} is a subset of @{term "Pow (pders_lang UNIV r)"},
+ Now the range of @{term "\<lambda>x. pderivs x r"} is a subset of @{term "Pow (pderivs_lang UNIV r)"},
which we know is finite by Theorem~\ref{antimirov}. Consequently there
are only finitely many equivalence classes of @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. pders x r)\<^esub>"},
which refines @{term "\<approx>(lang r)"}, and therefore we can again conclude the
@@ -2007,29 +2052,29 @@
left-quotient. Define
\begin{center}
- @{abbrev "Ders_lang B A"}
+ @{abbrev "Deriv_lang B A"}
\end{center}
\noindent
and assume @{text B} is any language and @{text A} is regular, then @{term
- "Ders_lang B A"} is regular. To see this consider the following argument
+ "Deriv_lang B A"} is regular. To see this consider the following argument
using partial derivatives: From @{text A} being regular we know there exists
a regular expression @{text r} such that @{term "A = lang r"}. We also know
- that @{term "pders_lang B r"} is finite for every language @{text B} and
+ that @{term "pderivs_lang B r"} is finite for every language @{text B} and
regular expression @{text r} (recall Theorem~\ref{antimirov}). By definition
and \eqref{Derspders} therefore
\begin{equation}\label{eqq}
- @{term "Ders_lang B (lang r) = (\<Union> lang ` (pders_lang B r))"}
+ @{term "Deriv_lang B (lang r) = (\<Union> lang ` (pderivs_lang B r))"}
\end{equation}
\noindent
- Since there are only finitely many regular expressions in @{term "pders_lang
+ Since there are only finitely many regular expressions in @{term "pderivs_lang
B r"}, we know by \eqref{uplus} that there exists a regular expression so that
- the right-hand side of \eqref{eqq} is equal to the language \mbox{@{term "lang (\<Uplus>(pders_lang B
- r))"}}. Thus the regular expression @{term "\<Uplus>(pders_lang B r)"} verifies that
- @{term "Ders_lang B A"} is regular.
+ the right-hand side of \eqref{eqq} is equal to the language \mbox{@{term "lang (\<Uplus>(pderivs_lang B
+ r))"}}. Thus the regular expression @{term "\<Uplus>(pderivs_lang B r)"} verifies that
+ @{term "Deriv_lang B A"} is regular.
*}
--- a/More_Regular_Set.thy Fri Aug 19 20:39:07 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,151 +0,0 @@
-(* Author: Christian Urban, Xingyuan Zhang, Chunhan Wu *)
-theory More_Regular_Set
-imports "Regular_Exp" "Folds"
-begin
-
-text {* Some properties of operator @{text "@@"}. *}
-
-notation
- conc (infixr "\<cdot>" 100) and
- star ("_\<star>" [101] 102)
-
-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 conc_pow_comm:
- shows "A \<cdot> (A ^^ n) = (A ^^ n) \<cdot> A"
-by (induct n) (simp_all add: conc_assoc[symmetric])
-
-lemma conc_star_comm:
- shows "A \<cdot> A\<star> = A\<star> \<cdot> A"
-unfolding star_def conc_pow_comm conc_UNION_distrib
-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 ^^ Suc n"
- shows "n < length s"
-using b
-proof (induct n arbitrary: s)
- case 0
- have "s \<in> A ^^ 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 ^^ Suc n \<Longrightarrow> n < length s" by fact
- have "s \<in> A ^^ Suc (Suc n)" by fact
- then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A ^^ Suc n"
- by (auto simp add: conc_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 conc_pow_length:
- assumes a: "[] \<notin> A"
- and b: "s \<in> B \<cdot> (A ^^ Suc n)"
- shows "n < length s"
-proof -
- from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A ^^ Suc n"
- 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 \<cdot> A \<union> B"
- shows "X = X \<cdot> (A ^^ Suc n) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))"
-proof (induct n)
- case 0
- show "X = X \<cdot> (A ^^ Suc 0) \<union> (\<Union>(m::nat)\<in>{0..0}. B \<cdot> (A ^^ m))"
- using eq by simp
-next
- case (Suc n)
- have ih: "X = X \<cdot> (A ^^ Suc n) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))" by fact
- also have "\<dots> = (X \<cdot> A \<union> B) \<cdot> (A ^^ Suc n) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))" using eq by simp
- also have "\<dots> = X \<cdot> (A ^^ Suc (Suc n)) \<union> (B \<cdot> (A ^^ Suc n)) \<union> (\<Union>m\<in>{0..n}. B \<cdot> (A ^^ m))"
- by (simp add: conc_Un_distrib conc_assoc)
- also have "\<dots> = X \<cdot> (A ^^ Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B \<cdot> (A ^^ m))"
- by (auto simp add: le_Suc_eq)
- finally show "X = X \<cdot> (A ^^ Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B \<cdot> (A ^^ m))" .
-qed
-
-theorem arden:
- assumes nemp: "[] \<notin> A"
- shows "X = X \<cdot> A \<union> B \<longleftrightarrow> X = B \<cdot> A\<star>"
-proof
- assume eq: "X = B \<cdot> A\<star>"
- have "A\<star> = {[]} \<union> A\<star> \<cdot> A"
- unfolding conc_star_comm[symmetric]
- by(metis Un_commute star_unfold_left)
- then have "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"
- by metis
- also have "\<dots> = B \<union> B \<cdot> (A\<star> \<cdot> A)"
- unfolding conc_Un_distrib by simp
- also have "\<dots> = B \<union> (B \<cdot> A\<star>) \<cdot> A"
- by (simp only: conc_assoc)
- finally show "X = X \<cdot> A \<union> B"
- using eq by blast
-next
- assume eq: "X = X \<cdot> A \<union> B"
- { fix n::nat
- have "B \<cdot> (A ^^ n) \<subseteq> X" using arden_helper[OF eq, of "n"] by auto }
- then have "B \<cdot> A\<star> \<subseteq> X"
- unfolding conc_def star_def UNION_def by auto
- moreover
- { fix s::"'a list"
- obtain k where "k = length s" by auto
- then have not_in: "s \<notin> X \<cdot> (A ^^ Suc k)"
- using conc_pow_length[OF nemp] by blast
- assume "s \<in> X"
- then have "s \<in> X \<cdot> (A ^^ Suc k) \<union> (\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m))"
- using arden_helper[OF eq, of "k"] by auto
- then have "s \<in> (\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m))" using not_in by auto
- moreover
- have "(\<Union>m\<in>{0..k}. B \<cdot> (A ^^ m)) \<subseteq> (\<Union>n. B \<cdot> (A ^^ n))" by auto
- ultimately
- have "s \<in> B \<cdot> A\<star>"
- unfolding conc_Un_distrib star_def by auto }
- then have "X \<subseteq> B \<cdot> A\<star>" by auto
- ultimately
- show "X = B \<cdot> A\<star>" by simp
-qed
-
-
-text {* Plus-combination for a set of regular expressions *}
-
-abbreviation
- Setalt ("\<Uplus>_" [1000] 999)
-where
- "\<Uplus>A \<equiv> folds Plus Zero A"
-
-text {*
- For finite sets, @{term Setalt} is preserved under @{term lang}.
-*}
-
-lemma folds_alt_simp [simp]:
- fixes rs::"('a rexp) set"
- assumes a: "finite rs"
- shows "lang (\<Uplus>rs) = \<Union> (lang ` 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Myhill.thy Mon Aug 22 12:49:27 2011 +0000
@@ -0,0 +1,55 @@
+theory Myhill
+ imports Myhill_2 "Derivatives"
+begin
+
+section {* The theorem *}
+
+theorem Myhill_Nerode:
+ fixes A::"('a::finite) lang"
+ shows "(\<exists>r. A = lang r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
+using Myhill_Nerode1 Myhill_Nerode2 by auto
+
+
+subsection {* Second direction proved using partial derivatives *}
+
+text {*
+ An alternaive proof using the notion of partial derivatives for regular
+ expressions due to Antimirov \cite{Antimirov95}.
+*}
+
+lemma MN_Rel_Derivs:
+ shows "x \<approx>A y \<longleftrightarrow> Derivs x A = Derivs y A"
+unfolding Derivs_def str_eq_def
+by auto
+
+lemma Myhill_Nerode3:
+ fixes r::"'a rexp"
+ shows "finite (UNIV // \<approx>(lang r))"
+proof -
+ have "finite (UNIV // =(\<lambda>x. pderivs x r)=)"
+ proof -
+ have "range (\<lambda>x. pderivs x r) \<subseteq> Pow (pderivs_lang UNIV r)"
+ unfolding pderivs_lang_def by auto
+ moreover
+ have "finite (Pow (pderivs_lang UNIV r))" by (simp add: finite_pderivs_lang)
+ ultimately
+ have "finite (range (\<lambda>x. pderivs x r))"
+ by (simp add: finite_subset)
+ then show "finite (UNIV // =(\<lambda>x. pderivs x r)=)"
+ by (rule finite_eq_tag_rel)
+ qed
+ moreover
+ have "=(\<lambda>x. pderivs x r)= \<subseteq> \<approx>(lang r)"
+ unfolding tag_eq_def
+ by (auto simp add: MN_Rel_Derivs Derivs_pderivs)
+ moreover
+ have "equiv UNIV =(\<lambda>x. pderivs x r)="
+ and "equiv UNIV (\<approx>(lang r))"
+ unfolding equiv_def refl_on_def sym_def trans_def
+ unfolding tag_eq_def str_eq_def
+ by auto
+ ultimately show "finite (UNIV // \<approx>(lang r))"
+ by (rule refined_partition_finite)
+qed
+
+end
\ No newline at end of file
--- a/Myhill_1.thy Fri Aug 19 20:39:07 2011 +0000
+++ b/Myhill_1.thy Mon Aug 22 12:49:27 2011 +0000
@@ -1,9 +1,13 @@
theory Myhill_1
-imports More_Regular_Set
+imports "Folds"
"~~/src/HOL/Library/While_Combinator"
begin
-section {* Direction @{text "finite partition \<Rightarrow> regular language"} *}
+section {* First direction of MN: @{text "finite partition \<Rightarrow> regular language"} *}
+
+notation
+ conc (infixr "\<cdot>" 100) and
+ star ("_\<star>" [101] 102)
lemma Pair_Collect [simp]:
shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
@@ -11,7 +15,6 @@
text {* Myhill-Nerode relation *}
-
definition
str_eq :: "'a lang \<Rightarrow> ('a list \<times> 'a list) set" ("\<approx>_" [100] 100)
where
@@ -39,7 +42,7 @@
unfolding finals_def quotient_def
by auto
-section {* Equational systems *}
+subsection {* Equational systems *}
text {* The two kinds of terms in the rhs of equations. *}
@@ -87,7 +90,7 @@
"Init CS \<equiv> {(X, Init_rhs CS X) | X. X \<in> CS}"
-section {* Arden Operation on equations *}
+subsection {* Arden Operation on equations *}
fun
Append_rexp :: "'a rexp \<Rightarrow> 'a trm \<Rightarrow> 'a trm"
@@ -104,7 +107,7 @@
Append_rexp_rhs (rhs - {Trn X r | r. Trn X r \<in> rhs}) (Star (\<Uplus> {r. Trn X r \<in> rhs}))"
-section {* Substitution Operation on equations *}
+subsection {* Substitution Operation on equations *}
definition
"Subst rhs X xrhs \<equiv>
@@ -120,7 +123,7 @@
Subst_all (ES - {(X, xrhs)}) X (Arden X xrhs)"
-section {* While-combinator *}
+subsection {* While-combinator and invariants *}
definition
"Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y
@@ -141,8 +144,6 @@
"Solve X ES \<equiv> while Cond (Iter X) ES"
-section {* Invariants *}
-
definition
"distinctness ES \<equiv>
\<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
@@ -197,8 +198,6 @@
using assms by (simp add: invariant_def)
-subsection {* The proof of this direction *}
-
lemma finite_Trn:
assumes fin: "finite rhs"
shows "finite {r. Trn Y r \<in> rhs}"
@@ -247,7 +246,7 @@
by (auto simp add: conc_def lang_of_append_rexp)
-subsubsection {* Intial Equational System *}
+subsection {* Intial Equational Systems *}
lemma defined_by_str:
assumes "s \<in> X" "X \<in> UNIV // \<approx>A"
@@ -353,7 +352,7 @@
by auto
qed
-subsubsection {* Interation step *}
+subsection {* Interations *}
lemma Arden_preserves_soundness:
assumes l_eq_r: "X = lang_rhs rhs"
@@ -377,7 +376,7 @@
by blast
finally have "X = X \<cdot> A \<union> B" .
then have "X = B \<cdot> A\<star>"
- by (simp add: arden[OF not_empty2])
+ by (simp add: reversed_Arden[OF not_empty2])
also have "\<dots> = lang_rhs (Arden X rhs)"
unfolding Arden_def A_def B_def b_def
by (simp only: lang_of_append_rexp_rhs lang.simps)
@@ -676,7 +675,7 @@
qed
-subsubsection {* Conclusion of the proof *}
+subsection {* The conclusion of the first direction *}
lemma Solve:
fixes A::"('a::finite) lang"
--- a/Myhill_2.thy Fri Aug 19 20:39:07 2011 +0000
+++ b/Myhill_2.thy Mon Aug 22 12:49:27 2011 +0000
@@ -1,9 +1,10 @@
theory Myhill_2
- imports Myhill_1
- "~~/src/HOL/Library/List_Prefix"
+ imports Myhill_1 "~~/src/HOL/Library/List_Prefix"
begin
-section {* Direction @{text "regular language \<Rightarrow> finite partition"} *}
+section {* Second direction of MN: @{text "regular language \<Rightarrow> finite partition"} *}
+
+subsection {* Tagging functions *}
definition
tag_eq :: "('a list \<Rightarrow> 'b) \<Rightarrow> ('a list \<times> 'a list) set" ("=_=")
@@ -115,9 +116,7 @@
qed
-subsection {* The proof *}
-
-subsubsection {* The base case for @{const "Zero"} *}
+subsection {* Base cases: @{const Zero}, @{const One} and @{const Atom} *}
lemma quot_zero_eq:
shows "UNIV // \<approx>{} = {UNIV}"
@@ -128,8 +127,6 @@
unfolding quot_zero_eq by simp
-subsubsection {* The base case for @{const "One"} *}
-
lemma quot_one_subset:
shows "UNIV // \<approx>{[]} \<subseteq> {{[]}, UNIV - {[]}}"
proof
@@ -152,8 +149,6 @@
by (rule finite_subset[OF quot_one_subset]) (simp)
-subsubsection {* The base case for @{const "Atom"} *}
-
lemma quot_atom_subset:
"UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
proof
@@ -185,7 +180,7 @@
by (rule finite_subset[OF quot_atom_subset]) (simp)
-subsubsection {* The inductive case for @{const Plus} *}
+subsection {* Case for @{const Plus} *}
definition
tag_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)"
@@ -208,7 +203,7 @@
qed
-subsubsection {* The inductive case for @{text "Times"} *}
+subsection {* Case for @{text "Times"} *}
definition
"Partitions x \<equiv> {(x\<^isub>p, x\<^isub>s). x\<^isub>p @ x\<^isub>s = x}"
@@ -313,7 +308,7 @@
qed
-subsubsection {* The inductive case for @{const "Star"} *}
+subsection {* Case for @{const "Star"} *}
lemma star_partitions_elim:
assumes "x @ z \<in> A\<star>" "x \<noteq> []"
@@ -463,16 +458,11 @@
(auto simp add: quotient_def)
qed
-subsubsection{* The conclusion *}
+subsection {* The conclusion of the second direction *}
lemma Myhill_Nerode2:
fixes r::"'a rexp"
shows "finite (UNIV // \<approx>(lang r))"
by (induct r) (auto)
-theorem Myhill_Nerode:
- fixes A::"('a::finite) lang"
- shows "(\<exists>r. A = lang r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
-using Myhill_Nerode1 Myhill_Nerode2 by auto
-
end
\ No newline at end of file
--- a/Regular_Exp.thy Fri Aug 19 20:39:07 2011 +0000
+++ b/Regular_Exp.thy Mon Aug 22 12:49:27 2011 +0000
@@ -16,7 +16,7 @@
Times "('a rexp)" "('a rexp)" |
Star "('a rexp)"
-primrec lang :: "'a rexp => 'a list set" where
+primrec lang :: "'a rexp => 'a lang" where
"lang Zero = {}" |
"lang One = {[]}" |
"lang (Atom a) = {[a]}" |
--- a/Regular_Set.thy Fri Aug 19 20:39:07 2011 +0000
+++ b/Regular_Set.thy Mon Aug 22 12:49:27 2011 +0000
@@ -22,17 +22,6 @@
"star A = (\<Union>n. A ^^ n)"
-
-definition deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
-where "deriv x L = { xs. x#xs \<in> L }"
-
-
-coinductive bisimilar :: "'a list set \<Rightarrow> 'a list set \<Rightarrow> bool" where
-"([] \<in> K \<longleftrightarrow> [] \<in> L)
- \<Longrightarrow> (\<And>x. bisimilar (deriv x K) (deriv x L))
- \<Longrightarrow> bisimilar K L"
-
-
subsection{* @{term "op @@"} *}
lemma concI[simp,intro]: "u : A \<Longrightarrow> v : B \<Longrightarrow> u@v : A @@ B"
@@ -77,6 +66,9 @@
lemma lang_pow_empty_Suc[simp]: "({}::'a lang) ^^ Suc n = {}"
by (simp add: lang_pow_empty)
+lemma conc_pow_comm:
+ shows "A @@ (A ^^ n) = (A ^^ n) @@ A"
+by (induct n) (simp_all add: conc_assoc[symmetric])
lemma length_lang_pow_ub:
"ALL w : A. length w \<le> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<le> k*n"
@@ -115,6 +107,11 @@
lemma conc_star_star: "star A @@ star A = star A"
by (auto simp: conc_def)
+lemma conc_star_comm:
+ shows "A @@ star A = star A @@ A"
+unfolding star_def conc_pow_comm conc_UNION_distrib
+by simp
+
lemma star_induct[consumes 1, case_names Nil append, induct set: star]:
assumes "w : star A"
and "P []"
@@ -178,29 +175,36 @@
} thus ?thesis by (auto simp: star_conv_concat)
qed
+lemma star_decom:
+ assumes a: "x \<in> star A" "x \<noteq> []"
+ shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> star A"
+using a by (induct rule: star_induct) (blast)+
+
+subsection {* Arden's Lemma *}
+
+lemma arden_helper:
+ assumes eq: "X = A @@ X \<union> B"
+ shows "X = (A ^^ Suc n) @@ X \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)"
+proof (induct n)
+ case 0
+ show "X = (A ^^ Suc 0) @@ X \<union> (\<Union>m\<le>0. (A ^^ m) @@ B)"
+ using eq by simp
+next
+ case (Suc n)
+ have ih: "X = (A ^^ Suc n) @@ X \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" by fact
+ also have "\<dots> = (A ^^ Suc n) @@ (A @@ X \<union> B) \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" using eq by simp
+ also have "\<dots> = (A ^^ Suc (Suc n)) @@ X \<union> ((A ^^ Suc n) @@ B) \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)"
+ by (simp add: conc_Un_distrib conc_assoc[symmetric] conc_pow_comm)
+ also have "\<dots> = (A ^^ Suc (Suc n)) @@ X \<union> (\<Union>m\<le>Suc n. (A ^^ m) @@ B)"
+ by (auto simp add: le_Suc_eq)
+ finally show "X = (A ^^ Suc (Suc n)) @@ X \<union> (\<Union>m\<le>Suc n. (A ^^ m) @@ B)" .
+qed
+
lemma Arden:
-assumes "[] \<notin> A" and "X = A @@ X \<union> B"
-shows "X = star A @@ B"
-proof -
- { fix n have "X = A^^(n+1)@@X \<union> (\<Union>i\<le>n. A^^i@@B)"
- proof(induct n)
- case 0 show ?case using `X = A @@ X \<union> B` by simp
- next
- case (Suc n)
- have "X = A@@X Un B" by(rule assms(2))
- also have "\<dots> = A@@(A^^(n+1)@@X \<union> (\<Union>i\<le>n. A^^i@@B)) Un B"
- by(subst Suc)(rule refl)
- also have "\<dots> = A^^(n+2)@@X \<union> (\<Union>i\<le>n. A^^(i+1)@@B) Un B"
- by(simp add:conc_UNION_distrib conc_assoc conc_Un_distrib)
- also have "\<dots> = A^^(n+2)@@X \<union> (UN i : {1..n+1}. A^^i@@B) \<union> B"
- by(subst UN_le_add_shift)(rule refl)
- also have "\<dots> = A^^(n+2)@@X \<union> (UN i : {1..n+1}. A^^i@@B) \<union> A^^0@@B"
- by(simp)
- also have "\<dots> = A^^(n+2)@@X \<union> (\<Union>i\<le>n+1. A^^i@@B)"
- by(auto simp: UN_le_eq_Un0)
- finally show ?case by simp
- qed
- } note 1 = this
+ assumes "[] \<notin> A"
+ shows "X = A @@ X \<union> B \<longleftrightarrow> X = star A @@ B"
+proof
+ assume eq: "X = A @@ X \<union> B"
{ fix w assume "w : X"
let ?n = "size w"
from `[] \<notin> A` have "ALL u : A. length u \<ge> 1"
@@ -210,139 +214,81 @@
hence "ALL u : A^^(?n+1)@@X. length u \<ge> ?n+1"
by(auto simp only: conc_def length_append)
hence "w \<notin> A^^(?n+1)@@X" by auto
- hence "w : star A @@ B" using `w : X` 1[of ?n]
- by(auto simp add: star_def conc_UNION_distrib)
+ hence "w : star A @@ B" using `w : X` using arden_helper[OF eq, where n="?n"]
+ by (auto simp add: star_def conc_UNION_distrib)
} moreover
{ fix w assume "w : star A @@ B"
hence "EX n. w : A^^n @@ B" by(auto simp: conc_def star_def)
- hence "w : X" using 1 by blast
- } ultimately show ?thesis by blast
+ hence "w : X" using arden_helper[OF eq] by blast
+ } ultimately show "X = star A @@ B" by blast
+next
+ assume eq: "X = star A @@ B"
+ have "star A = A @@ star A \<union> {[]}"
+ by (rule star_unfold_left)
+ then have "star A @@ B = (A @@ star A \<union> {[]}) @@ B"
+ by metis
+ also have "\<dots> = (A @@ star A) @@ B \<union> B"
+ unfolding conc_Un_distrib by simp
+ also have "\<dots> = A @@ (star A @@ B) \<union> B"
+ by (simp only: conc_assoc)
+ finally show "X = A @@ X \<union> B"
+ using eq by blast
qed
-subsection{* @{const deriv} *}
-lemma deriv_empty[simp]: "deriv a {} = {}"
-and deriv_epsilon[simp]: "deriv a {[]} = {}"
-and deriv_char[simp]: "deriv a {[b]} = (if a = b then {[]} else {})"
-and deriv_union[simp]: "deriv a (A \<union> B) = deriv a A \<union> deriv a B"
-by (auto simp: deriv_def)
-
-lemma deriv_conc_subset:
-"deriv a A @@ B \<subseteq> deriv a (A @@ B)" (is "?L \<subseteq> ?R")
-proof
- fix w assume "w \<in> ?L"
- then obtain u v where "w = u @ v" "a # u \<in> A" "v \<in> B"
- by (auto simp: deriv_def)
- then have "a # w \<in> A @@ B"
- by (auto intro: concI[of "a # u", simplified])
- thus "w \<in> ?R" by (auto simp: deriv_def)
-qed
-
-lemma deriv_conc1:
-assumes "[] \<notin> A"
-shows "deriv a (A @@ B) = deriv a A @@ B" (is "?L = ?R")
-proof
- show "?L \<subseteq> ?R"
- proof
- fix w assume "w \<in> ?L"
- then have "a # w \<in> A @@ B" by (simp add: deriv_def)
- then obtain x y
- where aw: "a # w = x @ y" "x \<in> A" "y \<in> B" by auto
- with `[] \<notin> A` obtain x' where "x = a # x'"
- by (cases x) auto
- with aw have "w = x' @ y" "x' \<in> deriv a A"
- by (auto simp: deriv_def)
- with `y \<in> B` show "w \<in> ?R" by simp
- qed
- show "?R \<subseteq> ?L" by (fact deriv_conc_subset)
+lemma reversed_arden_helper:
+ assumes eq: "X = X @@ A \<union> B"
+ shows "X = X @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))"
+proof (induct n)
+ case 0
+ show "X = X @@ (A ^^ Suc 0) \<union> (\<Union>m\<le>0. B @@ (A ^^ m))"
+ using eq by simp
+next
+ case (Suc n)
+ have ih: "X = X @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" by fact
+ also have "\<dots> = (X @@ A \<union> B) @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" using eq by simp
+ also have "\<dots> = X @@ (A ^^ Suc (Suc n)) \<union> (B @@ (A ^^ Suc n)) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))"
+ by (simp add: conc_Un_distrib conc_assoc)
+ also have "\<dots> = X @@ (A ^^ Suc (Suc n)) \<union> (\<Union>m\<le>Suc n. B @@ (A ^^ m))"
+ by (auto simp add: le_Suc_eq)
+ finally show "X = X @@ (A ^^ Suc (Suc n)) \<union> (\<Union>m\<le>Suc n. B @@ (A ^^ m))" .
qed
-lemma deriv_conc2:
-assumes "[] \<in> A"
-shows "deriv a (A @@ B) = deriv a A @@ B \<union> deriv a B"
-(is "?L = ?R")
+theorem reversed_Arden:
+ assumes nemp: "[] \<notin> A"
+ shows "X = X @@ A \<union> B \<longleftrightarrow> X = B @@ star A"
proof
- show "?L \<subseteq> ?R"
- proof
- fix w assume "w \<in> ?L"
- then have "a # w \<in> A @@ B" by (simp add: deriv_def)
- then obtain x y
- where aw: "a # w = x @ y" "x \<in> A" "y \<in> B" by auto
- show "w \<in> ?R"
- proof (cases x)
- case Nil
- with aw have "w \<in> deriv a B" by (auto simp: deriv_def)
- thus ?thesis ..
- next
- case (Cons b x')
- with aw have "w = x' @ y" "x' \<in> deriv a A"
- by (auto simp: deriv_def)
- with `y \<in> B` show "w \<in> ?R" by simp
- qed
- qed
-
- from concI[OF `[] \<in> A`, simplified]
- have "B \<subseteq> A @@ B" ..
- then have "deriv a B \<subseteq> deriv a (A @@ B)" by (auto simp: deriv_def)
- with deriv_conc_subset[of a A B]
- show "?R \<subseteq> ?L" by auto
+ assume eq: "X = X @@ A \<union> B"
+ { fix w assume "w : X"
+ let ?n = "size w"
+ from `[] \<notin> A` have "ALL u : A. length u \<ge> 1"
+ by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)
+ hence "ALL u : A^^(?n+1). length u \<ge> ?n+1"
+ by (metis length_lang_pow_lb nat_mult_1)
+ hence "ALL u : X @@ A^^(?n+1). length u \<ge> ?n+1"
+ by(auto simp only: conc_def length_append)
+ hence "w \<notin> X @@ A^^(?n+1)" by auto
+ hence "w : B @@ star A" using `w : X` using reversed_arden_helper[OF eq, where n="?n"]
+ by (auto simp add: star_def conc_UNION_distrib)
+ } moreover
+ { fix w assume "w : B @@ star A"
+ hence "EX n. w : B @@ A^^n" by (auto simp: conc_def star_def)
+ hence "w : X" using reversed_arden_helper[OF eq] by blast
+ } ultimately show "X = B @@ star A" by blast
+next
+ assume eq: "X = B @@ star A"
+ have "star A = {[]} \<union> star A @@ A"
+ unfolding conc_star_comm[symmetric]
+ by(metis Un_commute star_unfold_left)
+ then have "B @@ star A = B @@ ({[]} \<union> star A @@ A)"
+ by metis
+ also have "\<dots> = B \<union> B @@ (star A @@ A)"
+ unfolding conc_Un_distrib by simp
+ also have "\<dots> = B \<union> (B @@ star A) @@ A"
+ by (simp only: conc_assoc)
+ finally show "X = X @@ A \<union> B"
+ using eq by blast
qed
-lemma wlog_no_eps:
-assumes PB: "\<And>B. [] \<notin> B \<Longrightarrow> P B"
-assumes preserved: "\<And>A. P A \<Longrightarrow> P (insert [] A)"
-shows "P A"
-proof -
- let ?B = "A - {[]}"
- have "P ?B" by (rule PB) auto
- thus "P A"
- proof cases
- assume "[] \<in> A"
- then have "(insert [] ?B) = A" by auto
- with preserved[OF `P ?B`]
- show ?thesis by simp
- qed auto
-qed
-
-lemma deriv_insert_eps[simp]:
-"deriv a (insert [] A) = deriv a A"
-by (auto simp: deriv_def)
-
-lemma deriv_star[simp]: "deriv a (star A) = deriv a A @@ star A"
-proof (induct A rule: wlog_no_eps)
- fix B :: "'a list set" assume "[] \<notin> B"
- thus "deriv a (star B) = deriv a B @@ star B"
- by (subst star_unfold_left) (simp add: deriv_conc1)
-qed auto
-
-
-subsection{* @{const bisimilar} *}
-
-lemma equal_if_bisimilar:
-assumes "bisimilar K L" shows "K = L"
-proof (rule set_eqI)
- fix w
- from `bisimilar K L` show "w \<in> K \<longleftrightarrow> w \<in> L"
- proof (induct w arbitrary: K L)
- case Nil thus ?case by (auto elim: bisimilar.cases)
- next
- case (Cons a w K L)
- from `bisimilar K L` have "bisimilar (deriv a K) (deriv a L)"
- by (auto elim: bisimilar.cases)
- then have "w \<in> deriv a K \<longleftrightarrow> w \<in> deriv a L" by (rule Cons(1))
- thus ?case by (auto simp: deriv_def)
- qed
-qed
-
-lemma language_coinduct:
-fixes R (infixl "\<sim>" 50)
-assumes "K \<sim> L"
-assumes "\<And>K L. K \<sim> L \<Longrightarrow> ([] \<in> K \<longleftrightarrow> [] \<in> L)"
-assumes "\<And>K L x. K \<sim> L \<Longrightarrow> deriv x K \<sim> deriv x L"
-shows "K = L"
-apply (rule equal_if_bisimilar)
-apply (rule bisimilar.coinduct[of R, OF `K \<sim> L`])
-apply (auto simp: assms)
-done
end
--- a/Slides/ROOT.ML Fri Aug 19 20:39:07 2011 +0000
+++ b/Slides/ROOT.ML Mon Aug 22 12:49:27 2011 +0000
@@ -1,5 +1,5 @@
(*show_question_marks := false;*)
-no_document use_thy "LaTeXsugar";
+no_document use_thy "~~/src/HOL/Library/LaTeXsugar";
quick_and_dirty := true;
use_thy "Slides"
\ No newline at end of file
--- a/Slides/Slides.thy Fri Aug 19 20:39:07 2011 +0000
+++ b/Slides/Slides.thy Mon Aug 22 12:49:27 2011 +0000
@@ -1,6 +1,6 @@
(*<*)
theory Slides
-imports "LaTeXsugar"
+imports "~~/src/HOL/Library/LaTeXsugar"
begin
notation (latex output)