--- a/Closure.thy Thu May 12 05:55:05 2011 +0000
+++ b/Closure.thy Wed May 18 19:54:43 2011 +0000
@@ -1,223 +1,140 @@
-theory "RegSet"
- imports "Main"
+theory Closure
+imports Myhill_2
begin
-
-text {* Sequential composition of sets *}
+section {* Closure properties of regular languages *}
-definition
- lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ; _" [100,100] 100)
-where
- "L1 ; L2 = {s1@s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
+abbreviation
+ regular :: "lang \<Rightarrow> bool"
+where
+ "regular A \<equiv> \<exists>r::rexp. A = L r"
-section {* Kleene star for sets *}
+lemma closure_union[intro]:
+ assumes "regular A" "regular B"
+ shows "regular (A \<union> B)"
+proof -
+ from assms obtain r1 r2::rexp where "L r1 = A" "L r2 = B" by auto
+ then have "A \<union> B = L (ALT r1 r2)" by simp
+ then show "regular (A \<union> B)" by blast
+qed
-inductive_set
- Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
- for L :: "string set"
-where
- start[intro]: "[] \<in> L\<star>"
-| step[intro]: "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> L\<star>"
+lemma closure_seq[intro]:
+ assumes "regular A" "regular B"
+ shows "regular (A ;; B)"
+proof -
+ from assms obtain r1 r2::rexp where "L r1 = A" "L r2 = B" by auto
+ then have "A ;; B = L (SEQ r1 r2)" by simp
+ then show "regular (A ;; B)" by blast
+qed
-
-text {* A standard property of star *}
+lemma closure_star[intro]:
+ assumes "regular A"
+ shows "regular (A\<star>)"
+proof -
+ from assms obtain r::rexp where "L r = A" by auto
+ then have "A\<star> = L (STAR r)" by simp
+ then show "regular (A\<star>)" by blast
+qed
-lemma lang_star_cases:
- shows "L\<star> = {[]} \<union> L ; L\<star>"
-proof
- { fix x
- have "x \<in> L\<star> \<Longrightarrow> x \<in> {[]} \<union> L ; L\<star>"
- unfolding lang_seq_def
- by (induct rule: Star.induct) (auto)
- }
- then show "L\<star> \<subseteq> {[]} \<union> L ; L\<star>" by auto
-next
- show "{[]} \<union> L ; L\<star> \<subseteq> L\<star>"
- unfolding lang_seq_def by auto
+lemma closure_complement[intro]:
+ assumes "regular A"
+ shows "regular (- A)"
+proof -
+ from assms have "finite (UNIV // \<approx>A)" by (simp add: Myhill_Nerode)
+ then have "finite (UNIV // \<approx>(-A))" by (simp add: str_eq_rel_def)
+ then show "regular (- A)" by (simp add: Myhill_Nerode)
+qed
+
+lemma closure_difference[intro]:
+ assumes "regular A" "regular B"
+ shows "regular (A - B)"
+proof -
+ have "A - B = - (- A \<union> B)" by blast
+ moreover
+ have "regular (- (- A \<union> B))"
+ using assms by blast
+ ultimately show "regular (A - B)" by simp
+qed
+
+lemma closure_intersection[intro]:
+ assumes "regular A" "regular B"
+ shows "regular (A \<inter> B)"
+proof -
+ have "A \<inter> B = - (- A \<union> - B)" by blast
+ moreover
+ have "regular (- (- A \<union> - B))"
+ using assms by blast
+ ultimately show "regular (A \<inter> B)" by simp
qed
-lemma lang_star_cases2:
- shows "[] \<notin> L \<Longrightarrow> L\<star> - {[]} = L ; L\<star>"
-by (subst lang_star_cases)
- (simp add: lang_seq_def)
-
-
-section {* Regular Expressions *}
-
-datatype rexp =
- NULL
-| EMPTY
-| CHAR char
-| SEQ rexp rexp
-| ALT rexp rexp
-| STAR rexp
-
-
-section {* Semantics of Regular Expressions *}
+text {* closure under string reversal *}
fun
- L :: "rexp \<Rightarrow> string set"
+ Rev :: "rexp \<Rightarrow> rexp"
where
- "L (NULL) = {}"
-| "L (EMPTY) = {[]}"
-| "L (CHAR c) = {[c]}"
-| "L (SEQ r1 r2) = (L r1) ; (L r2)"
-| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
-| "L (STAR r) = (L r)\<star>"
-
-abbreviation
- CUNIV :: "string set"
-where
- "CUNIV \<equiv> (\<lambda>x. [x]) ` (UNIV::char set)"
-
-lemma CUNIV_star_minus:
- "(CUNIV\<star> - {[c]}) = {[]} \<union> (CUNIV - {[c]}; (CUNIV\<star>))"
-apply(subst lang_star_cases)
-apply(simp add: lang_seq_def)
-oops
-
+ "Rev NULL = NULL"
+| "Rev EMPTY = EMPTY"
+| "Rev (CHAR c) = CHAR c"
+| "Rev (ALT r1 r2) = ALT (Rev r1) (Rev r2)"
+| "Rev (SEQ r1 r2) = SEQ (Rev r2) (Rev r1)"
+| "Rev (STAR r) = STAR (Rev r)"
-lemma string_in_CUNIV:
- shows "s \<in> CUNIV\<star>"
-proof (induct s)
- case Nil
- show "[] \<in> CUNIV\<star>" by (rule start)
-next
- case (Cons c s)
- have "[c] \<in> CUNIV" by simp
- moreover
- have "s \<in> CUNIV\<star>" by fact
- ultimately have "[c] @ s \<in> CUNIV\<star>" by (rule step)
- then show "c # s \<in> CUNIV\<star>" by simp
-qed
-
-lemma UNIV_CUNIV_star:
- shows "UNIV = CUNIV\<star>"
-using string_in_CUNIV
-by (auto)
-
-abbreviation
- reg :: "string set => bool"
-where
- "reg L1 \<equiv> (\<exists>r. L r = L1)"
-
-lemma reg_null [intro]:
- shows "reg {}"
-by (metis L.simps(1))
+lemma rev_Seq:
+ "(rev ` A) ;; (rev ` B) = rev ` (B ;; A)"
+unfolding Seq_def image_def
+apply(auto)
+apply(rule_tac x="xb @ xa" in exI)
+apply(auto)
+done
-lemma reg_empty [intro]:
- shows "reg {[]}"
-by (metis L.simps(2))
-
-lemma reg_star [intro]:
- shows "reg L1 \<Longrightarrow> reg (L1\<star>)"
-by (metis L.simps(6))
-
-lemma reg_seq [intro]:
- assumes a: "reg L1" "reg L2"
- shows "reg (L1 ; L2)"
+lemma rev_Star1:
+ assumes a: "s \<in> (rev ` A)\<star>"
+ shows "s \<in> rev ` (A\<star>)"
using a
-by (metis L.simps(4))
-
-lemma reg_union [intro]:
- assumes a: "reg L1" "reg L2"
- shows "reg (L1 \<union> L2)"
-using a
-by (metis L.simps(5))
+proof(induct rule: star_induct)
+ case (step s1 s2)
+ have inj: "inj (rev::string \<Rightarrow> string)" unfolding inj_on_def by auto
+ have "s1 \<in> rev ` A" "s2 \<in> rev ` (A\<star>)" by fact+
+ then obtain x1 x2 where "x1 \<in> A" "x2 \<in> A\<star>" and eqs: "s1 = rev x1" "s2 = rev x2" by auto
+ then have "x1 \<in> A\<star>" "x2 \<in> A\<star>" by (auto intro: star_intro2)
+ then have "x2 @ x1 \<in> A\<star>" by (auto intro: star_intro1)
+ then have "rev (x2 @ x1) \<in> rev ` A\<star>" using inj by (simp only: inj_image_mem_iff)
+ then show "s1 @ s2 \<in> rev ` A\<star>" using eqs by simp
+qed (auto)
-lemma reg_string [intro]:
- fixes s::string
- shows "reg {s}"
-proof (induct s)
- case Nil
- show "reg {[]}" by (rule reg_empty)
-next
- case (Cons c s)
- have "reg {s}" by fact
- then obtain r where "L r = {s}" by auto
- then have "L (SEQ (CHAR c) r) = {[c]} ; {s}" by simp
- also have "\<dots> = {c # s}" by (simp add: lang_seq_def)
- finally show "reg {c # s}" by blast
-qed
+lemma rev_Star2:
+ assumes a: "s \<in> A\<star>"
+ shows "rev s \<in> (rev ` A)\<star>"
+using a
+proof(induct rule: star_induct)
+ case (step s1 s2)
+ have inj: "inj (rev::string \<Rightarrow> string)" unfolding inj_on_def by auto
+ have "s1 \<in> A"by fact
+ then have "rev s1 \<in> rev ` A" using inj by (simp only: inj_image_mem_iff)
+ then have "rev s1 \<in> (rev ` A)\<star>" by (auto intro: star_intro2)
+ moreover
+ have "rev s2 \<in> (rev ` A)\<star>" by fact
+ ultimately show "rev (s1 @ s2) \<in> (rev ` A)\<star>" by (auto intro: star_intro1)
+qed (auto)
-lemma reg_finite [intro]:
- assumes a: "finite L1"
- shows "reg L1"
-using a
-proof(induct)
- case empty
- show "reg {}" by (rule reg_null)
-next
- case (insert s S)
- have "reg {s}" by (rule reg_string)
- moreover
- have "reg S" by fact
- ultimately have "reg ({s} \<union> S)" by (rule reg_union)
- then show "reg (insert s S)" by simp
+lemma rev_Star:
+ "(rev ` A)\<star> = rev ` (A\<star>)"
+using rev_Star1 rev_Star2 by auto
+
+lemma rev_lang:
+ "L (Rev r) = rev ` (L r)"
+by (induct r) (simp_all add: rev_Star rev_Seq image_Un)
+
+lemma closure_reversal[intro]:
+ assumes "regular A"
+ shows "regular (rev ` A)"
+proof -
+ from assms obtain r::rexp where "L r = A" by auto
+ then have "L (Rev r) = rev ` A" by (simp add: rev_lang)
+ then show "regular (rev` A)" by blast
qed
-lemma reg_cuniv [intro]:
- shows "reg (CUNIV)"
-by (rule reg_finite) (auto)
-lemma reg_univ:
- shows "reg (UNIV::string set)"
-proof -
- have "reg CUNIV" by (rule reg_cuniv)
- then have "reg (CUNIV\<star>)" by (rule reg_star)
- then show "reg UNIV" by (simp add: UNIV_CUNIV_star)
-qed
-
-lemma reg_finite_subset:
- assumes a: "finite L1"
- and b: "reg L1" "L2 \<subseteq> L1"
- shows "reg L2"
-using a b
-apply(induct arbitrary: L2)
-apply(simp add: reg_empty)
-oops
-
-
-lemma reg_not:
- shows "reg (UNIV - L r)"
-proof (induct r)
- case NULL
- have "reg UNIV" by (rule reg_univ)
- then show "reg (UNIV - L NULL)" by simp
-next
- case EMPTY
- have "[] \<notin> CUNIV" by auto
- moreover
- have "reg (CUNIV; CUNIV\<star>)" by auto
- ultimately have "reg (CUNIV\<star> - {[]})"
- using lang_star_cases2 by simp
- then show "reg (UNIV - L EMPTY)" by (simp add: UNIV_CUNIV_star)
-next
- case (CHAR c)
- then show "?case"
- apply(simp)
-
-using reg_UNIV
-apply(simp)
-apply(simp add: char_star2[symmetric])
-apply(rule reg_seq)
-apply(rule reg_cuniv)
-apply(rule reg_star)
-apply(rule reg_cuniv)
-oops
-
-
-
-end
-
-
-
-
-
-
-
-
-
-
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Derivs.thy Wed May 18 19:54:43 2011 +0000
@@ -0,0 +1,521 @@
+theory Derivs
+imports Closure
+begin
+
+section {* Experiments with Derivatives -- independent of Myhill-Nerode *}
+
+subsection {* Left-Quotients *}
+
+definition
+ Delta :: "lang \<Rightarrow> lang"
+where
+ "Delta A = (if [] \<in> A then {[]} else {})"
+
+definition
+ Der :: "char \<Rightarrow> lang \<Rightarrow> lang"
+where
+ "Der c A \<equiv> {s. [c] @ s \<in> A}"
+
+definition
+ Ders :: "string \<Rightarrow> lang \<Rightarrow> lang"
+where
+ "Ders s A \<equiv> {s'. s @ s' \<in> A}"
+
+definition
+ Ders_set :: "lang \<Rightarrow> lang \<Rightarrow> lang"
+where
+ "Ders_set A B \<equiv> {s' | s s'. s @ s' \<in> B \<and> s \<in> A}"
+
+lemma Ders_set_Ders:
+ shows "Ders_set A B = (\<Union>s \<in> A. Ders s B)"
+unfolding Ders_set_def Ders_def
+by auto
+
+lemma Der_null [simp]:
+ shows "Der c {} = {}"
+unfolding Der_def
+by auto
+
+lemma Der_empty [simp]:
+ shows "Der c {[]} = {}"
+unfolding Der_def
+by auto
+
+lemma Der_char [simp]:
+ shows "Der c {[d]} = (if c = d then {[]} else {})"
+unfolding Der_def
+by auto
+
+lemma Der_union [simp]:
+ shows "Der c (A \<union> B) = Der c A \<union> Der c B"
+unfolding Der_def
+by auto
+
+lemma Der_seq [simp]:
+ shows "Der c (A ;; B) = (Der c A) ;; B \<union> (Delta A ;; Der c B)"
+unfolding Der_def Delta_def
+unfolding Seq_def
+by (auto simp add: Cons_eq_append_conv)
+
+lemma Der_star [simp]:
+ shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
+proof -
+ have incl: "Delta A ;; Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>"
+ unfolding Der_def Delta_def Seq_def
+ apply(auto)
+ apply(drule star_decom)
+ apply(auto simp add: Cons_eq_append_conv)
+ done
+
+ have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"
+ by (simp only: star_cases[symmetric])
+ also have "... = Der c (A ;; A\<star>)"
+ by (simp only: Der_union Der_empty) (simp)
+ also have "... = (Der c A) ;; A\<star> \<union> (Delta A ;; Der c (A\<star>))"
+ by simp
+ also have "... = (Der c A) ;; A\<star>"
+ using incl by auto
+ finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
+qed
+
+
+lemma Ders_singleton:
+ shows "Ders [c] A = Der c A"
+unfolding Der_def Ders_def
+by simp
+
+lemma Ders_append:
+ shows "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"
+unfolding Ders_def by simp
+
+lemma MN_Rel_Ders:
+ shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A"
+unfolding Ders_def str_eq_def str_eq_rel_def
+by auto
+
+subsection {* Brozowsky's derivatives of regular expressions *}
+
+fun
+ nullable :: "rexp \<Rightarrow> bool"
+where
+ "nullable (NULL) = False"
+| "nullable (EMPTY) = True"
+| "nullable (CHAR c) = False"
+| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
+| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
+| "nullable (STAR r) = True"
+
+fun
+ der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
+where
+ "der c (NULL) = NULL"
+| "der c (EMPTY) = NULL"
+| "der c (CHAR c') = (if c = c' then EMPTY else NULL)"
+| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
+| "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)"
+| "der c (STAR r) = SEQ (der c r) (STAR r)"
+
+function
+ ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
+where
+ "ders [] r = r"
+| "ders (s @ [c]) r = der c (ders s r)"
+by (auto) (metis rev_cases)
+
+termination
+ by (relation "measure (length o fst)") (auto)
+
+lemma Delta_nullable:
+ shows "Delta (L r) = (if nullable r then {[]} else {})"
+unfolding Delta_def
+by (induct r) (auto simp add: Seq_def split: if_splits)
+
+lemma Der_der:
+ fixes r::rexp
+ shows "Der c (L r) = L (der c r)"
+by (induct r) (simp_all add: Delta_nullable)
+
+lemma Ders_ders:
+ fixes r::rexp
+ shows "Ders s (L r) = L (ders s r)"
+apply(induct s rule: rev_induct)
+apply(simp add: Ders_def)
+apply(simp only: ders.simps)
+apply(simp only: Ders_append)
+apply(simp only: Ders_singleton)
+apply(simp only: Der_der)
+done
+
+
+subsection {* Antimirov's Partial Derivatives *}
+
+abbreviation
+ "SEQS R r \<equiv> {SEQ r' r | r'. r' \<in> R}"
+
+fun
+ pder :: "char \<Rightarrow> rexp \<Rightarrow> rexp set"
+where
+ "pder c NULL = {NULL}"
+| "pder c EMPTY = {NULL}"
+| "pder c (CHAR c') = (if c = c' then {EMPTY} else {NULL})"
+| "pder c (ALT r1 r2) = (pder c r1) \<union> (pder c r2)"
+| "pder c (SEQ r1 r2) = SEQS (pder c r1) r2 \<union> (if nullable r1 then pder c r2 else {})"
+| "pder c (STAR r) = SEQS (pder c r) (STAR r)"
+
+abbreviation
+ "pder_set c R \<equiv> \<Union>r \<in> R. pder c r"
+
+function
+ pders :: "string \<Rightarrow> rexp \<Rightarrow> rexp set"
+where
+ "pders [] r = {r}"
+| "pders (s @ [c]) r = pder_set c (pders s r)"
+by (auto) (metis rev_cases)
+
+termination
+ by (relation "measure (length o fst)") (auto)
+
+abbreviation
+ "pders_set A r \<equiv> \<Union>s \<in> A. pders s r"
+
+lemma pders_append:
+ "pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)"
+apply(induct s2 arbitrary: s1 r rule: rev_induct)
+apply(simp)
+apply(subst append_assoc[symmetric])
+apply(simp only: pders.simps)
+apply(auto)
+done
+
+lemma pders_singleton:
+ "pders [c] r = pder c r"
+apply(subst append_Nil[symmetric])
+apply(simp only: pders.simps)
+apply(simp)
+done
+
+lemma pder_set_lang:
+ shows "(\<Union> (L ` pder_set c R)) = (\<Union>r \<in> R. (\<Union>L ` (pder c r)))"
+unfolding image_def
+by auto
+
+lemma
+ shows seq_UNION_left: "B ;; (\<Union>n\<in>C. A n) = (\<Union>n\<in>C. B ;; A n)"
+ and seq_UNION_right: "(\<Union>n\<in>C. A n) ;; B = (\<Union>n\<in>C. A n ;; B)"
+unfolding Seq_def by auto
+
+lemma Der_pder:
+ fixes r::rexp
+ shows "Der c (L r) = \<Union> L ` (pder c r)"
+by (induct r) (auto simp add: Delta_nullable seq_UNION_right)
+
+lemma Ders_pders:
+ fixes r::rexp
+ shows "Ders s (L r) = \<Union> L ` (pders s r)"
+proof (induct s rule: rev_induct)
+ case (snoc c s)
+ have ih: "Ders s (L r) = \<Union> L ` (pders s r)" by fact
+ have "Ders (s @ [c]) (L r) = Ders [c] (Ders s (L r))"
+ by (simp add: Ders_append)
+ also have "\<dots> = Der c (\<Union> L ` (pders s r))" using ih
+ by (simp add: Ders_singleton)
+ also have "\<dots> = (\<Union>r\<in>pders s r. Der c (L r))"
+ unfolding Der_def image_def by auto
+ also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> L ` (pder c r)))"
+ by (simp add: Der_pder)
+ also have "\<dots> = (\<Union>L ` (pder_set c (pders s r)))"
+ by (simp add: pder_set_lang)
+ also have "\<dots> = (\<Union>L ` (pders (s @ [c]) r))"
+ by simp
+ finally show "Ders (s @ [c]) (L r) = \<Union>L ` pders (s @ [c]) r" .
+qed (simp add: Ders_def)
+
+lemma Ders_set_pders_set:
+ fixes r::rexp
+ shows "Ders_set A (L r) = (\<Union> L ` (pders_set A r))"
+by (simp add: Ders_set_Ders Ders_pders)
+
+lemma pders_NULL [simp]:
+ shows "pders s NULL = {NULL}"
+by (induct s rule: rev_induct) (simp_all)
+
+lemma pders_EMPTY [simp]:
+ shows "pders s EMPTY = (if s = [] then {EMPTY} else {NULL})"
+by (induct s rule: rev_induct) (auto)
+
+lemma pders_CHAR [simp]:
+ shows "pders s (CHAR c) = (if s = [] then {CHAR c} else (if s = [c] then {EMPTY} else {NULL}))"
+by (induct s rule: rev_induct) (auto)
+
+lemma pders_ALT [simp]:
+ shows "pders s (ALT r1 r2) = (if s = [] then {ALT r1 r2} else (pders s r1) \<union> (pders s r2))"
+by (induct s rule: rev_induct) (auto)
+
+definition
+ "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
+
+lemma Suf:
+ shows "Suf (s @ [c]) = (Suf s) ;; {[c]} \<union> {[c]}"
+unfolding Suf_def Seq_def
+by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv)
+
+lemma Suf_Union:
+ shows "(\<Union>v \<in> Suf s ;; {[c]}. P v) = (\<Union>v \<in> Suf s. P (v @ [c]))"
+by (auto simp add: Seq_def)
+
+lemma inclusion1:
+ shows "pder_set c (SEQS R r2) \<subseteq> SEQS (pder_set c R) r2 \<union> (pder c r2)"
+apply(auto simp add: if_splits)
+apply(blast)
+done
+
+lemma pders_SEQ:
+ shows "pders s (SEQ r1 r2) \<subseteq> SEQS (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)"
+proof (induct s rule: rev_induct)
+ case (snoc c s)
+ have ih: "pders s (SEQ r1 r2) \<subseteq> SEQS (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)"
+ by fact
+ have "pders (s @ [c]) (SEQ r1 r2) = pder_set c (pders s (SEQ r1 r2))" by simp
+ also have "\<dots> \<subseteq> pder_set c (SEQS (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2))"
+ using ih by auto
+ also have "\<dots> = pder_set c (SEQS (pders s r1) r2) \<union> pder_set c (\<Union>v \<in> Suf s. pders v r2)"
+ by (simp)
+ also have "\<dots> = pder_set c (SEQS (pders s r1) r2) \<union> (\<Union>v \<in> Suf s. pder_set c (pders v r2))"
+ by (simp)
+ also have "\<dots> \<subseteq> pder_set c (SEQS (pders s r1) r2) \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
+ by (auto)
+ also have "\<dots> \<subseteq> SEQS (pder_set c (pders s r1)) r2 \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
+ using inclusion1 by blast
+ also have "\<dots> = SEQS (pders (s @ [c]) r1) r2 \<union> (\<Union>v \<in> Suf (s @ [c]). pders v r2)"
+ apply(subst (2) pders.simps)
+ apply(simp only: Suf)
+ apply(simp add: Suf_Union pders_singleton)
+ apply(auto)
+ done
+ finally show ?case .
+qed (simp)
+
+lemma pders_STAR:
+ assumes a: "s \<noteq> []"
+ shows "pders s (STAR r) \<subseteq> (\<Union>v \<in> Suf s. SEQS (pders v 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> (\<Union>v\<in>Suf s. SEQS (pders v r) (STAR r))" by fact
+ { assume asm: "s \<noteq> []"
+ have "pders (s @ [c]) (STAR r) = pder_set c (pders s (STAR r))" by simp
+ also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. SEQS (pders v r) (STAR r)))"
+ using ih[OF asm] by blast
+ also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (SEQS (pders v r) (STAR r)))"
+ by simp
+ also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (SEQS (pder_set c (pders v r)) (STAR r) \<union> pder c (STAR r)))"
+ using inclusion1 by blast
+ also have "\<dots> = (\<Union>v\<in>Suf s. (SEQS (pder_set c (pders v r)) (STAR r))) \<union> pder c (STAR r)"
+ using asm by (auto simp add: Suf_def)
+ also have "\<dots> = (\<Union>v\<in>Suf s. (SEQS (pders (v @ [c]) r) (STAR r))) \<union> (SEQS (pder c r) (STAR r))"
+ by simp
+ also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (SEQS (pders v r) (STAR r)))"
+ apply(simp only: Suf)
+ apply(simp add: Suf_Union pders_singleton)
+ apply(auto)
+ done
+ finally have ?case .
+ }
+ moreover
+ { assume asm: "s = []"
+ then have ?case
+ apply(simp add: pders_singleton Suf_def)
+ apply(auto)
+ apply(rule_tac x="[c]" in exI)
+ apply(simp add: pders_singleton)
+ done
+ }
+ ultimately show ?case by blast
+qed (simp)
+
+abbreviation
+ "UNIV1 \<equiv> UNIV - {[]}"
+
+lemma pders_set_NULL:
+ shows "pders_set UNIV1 NULL = {NULL}"
+by auto
+
+lemma pders_set_EMPTY:
+ shows "pders_set UNIV1 EMPTY = {NULL}"
+by (auto split: if_splits)
+
+lemma pders_set_CHAR:
+ shows "pders_set UNIV1 (CHAR c) \<subseteq> {EMPTY, NULL}"
+by (auto split: if_splits)
+
+lemma pders_set_ALT:
+ shows "pders_set UNIV1 (ALT r1 r2) = pders_set UNIV1 r1 \<union> pders_set UNIV1 r2"
+by auto
+
+lemma pders_set_SEQ_aux:
+ assumes a: "s \<in> UNIV1"
+ shows "pders_set (Suf s) r2 \<subseteq> pders_set UNIV1 r2"
+using a by (auto simp add: Suf_def)
+
+lemma pders_set_SEQ:
+ shows "pders_set UNIV1 (SEQ r1 r2) \<subseteq> SEQS (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"
+apply(rule UN_least)
+apply(rule subset_trans)
+apply(rule pders_SEQ)
+apply(simp)
+apply(rule conjI)
+apply(auto)[1]
+apply(rule subset_trans)
+apply(rule pders_set_SEQ_aux)
+apply(auto)
+done
+
+lemma pders_set_STAR:
+ shows "pders_set UNIV1 (STAR r) \<subseteq> SEQS (pders_set UNIV1 r) (STAR r)"
+apply(rule UN_least)
+apply(rule subset_trans)
+apply(rule pders_STAR)
+apply(simp)
+apply(simp add: Suf_def)
+apply(auto)
+done
+
+lemma finite_SEQS:
+ assumes a: "finite A"
+ shows "finite (SEQS A r)"
+using a by (auto)
+
+lemma finite_pders_set_UNIV1:
+ shows "finite (pders_set UNIV1 r)"
+apply(induct r)
+apply(simp)
+apply(simp only: pders_set_EMPTY)
+apply(simp)
+apply(rule finite_subset)
+apply(rule pders_set_CHAR)
+apply(simp)
+apply(rule finite_subset)
+apply(rule pders_set_SEQ)
+apply(simp only: finite_SEQS finite_Un)
+apply(simp)
+apply(simp only: pders_set_ALT)
+apply(simp)
+apply(rule finite_subset)
+apply(rule pders_set_STAR)
+apply(simp only: finite_SEQS)
+done
+
+lemma pders_set_UNIV_UNIV1:
+ shows "pders_set UNIV r = pders [] r \<union> pders_set UNIV1 r"
+apply(auto)
+apply(rule_tac x="[]" in exI)
+apply(simp)
+done
+
+lemma finite_pders_set_UNIV:
+ shows "finite (pders_set UNIV r)"
+unfolding pders_set_UNIV_UNIV1
+by (simp add: finite_pders_set_UNIV1)
+
+lemma finite_pders_set:
+ shows "finite (pders_set A r)"
+apply(rule rev_finite_subset)
+apply(rule_tac r="r" in finite_pders_set_UNIV)
+apply(auto)
+done
+
+lemma finite_pders:
+ shows "finite (pders s r)"
+using finite_pders_set[where A="{s}" and r="r"]
+by simp
+
+lemma finite_pders2:
+ shows "finite {pders s r | s. s \<in> A}"
+proof -
+ have "{pders s r | s. s \<in> A} \<subseteq> Pow (pders_set A r)" by auto
+ moreover
+ have "finite (Pow (pders_set A r))"
+ using finite_pders_set by simp
+ ultimately
+ show "finite {pders s r | s. s \<in> A}"
+ by(rule finite_subset)
+qed
+
+
+lemma Myhill_Nerode3:
+ fixes r::"rexp"
+ shows "finite (UNIV // \<approx>(L r))"
+proof -
+ have "finite (UNIV // =(\<lambda>x. pders x r)=)"
+ proof -
+ have "range (\<lambda>x. pders x r) \<subseteq> {pders s r | s. s \<in> UNIV}" by auto
+ moreover
+ have "finite {pders s r | s. s \<in> UNIV}" by (rule finite_pders2)
+ ultimately
+ have "finite (range (\<lambda>x. pders x r))"
+ by (rule 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>(L r)"
+ unfolding tag_eq_rel_def
+ by (auto simp add: str_eq_def[symmetric] MN_Rel_Ders Ders_pders)
+ moreover
+ have "equiv UNIV =(\<lambda>x. pders x r)="
+ unfolding equiv_def refl_on_def sym_def trans_def
+ unfolding tag_eq_rel_def
+ by auto
+ moreover
+ have "equiv UNIV (\<approx>(L r))"
+ unfolding equiv_def refl_on_def sym_def trans_def
+ unfolding str_eq_rel_def
+ by auto
+ ultimately show "finite (UNIV // \<approx>(L r))"
+ by (rule refined_partition_finite)
+qed
+
+
+section {* 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 r = A" by auto
+ have fin: "finite (pders_set B r)" by (rule finite_pders_set)
+
+ have "Ders_set B (L r) = (\<Union> L ` (pders_set B r))"
+ by (simp add: Ders_set_pders_set)
+ also have "\<dots> = L (\<Uplus>(pders_set B r))" using fin by simp
+ finally have "Ders_set B A = L (\<Uplus>(pders_set B r))" using eq
+ by simp
+ then show "regular (Ders_set B A)" by auto
+qed
+
+
+section {* Relating standard and partial derivations *}
+
+lemma
+ shows "(\<Union> L ` (pder c r)) = L (der c r)"
+unfolding Der_der[symmetric] Der_pder by simp
+
+lemma
+ shows "(\<Union> L ` (pders s r)) = L (ders s r)"
+unfolding Ders_ders[symmetric] Ders_pders by simp
+
+
+
+fun
+ width :: "rexp \<Rightarrow> nat"
+where
+ "width (NULL) = 0"
+| "width (EMPTY) = 0"
+| "width (CHAR c) = 1"
+| "width (ALT r1 r2) = width r1 + width r2"
+| "width (SEQ r1 r2) = width r1 + width r2"
+| "width (STAR r) = width r"
+
+
+
+end
\ No newline at end of file
--- a/IsaMakefile Thu May 12 05:55:05 2011 +0000
+++ b/IsaMakefile Wed May 18 19:54:43 2011 +0000
@@ -69,6 +69,20 @@
cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
cp Paper/generated/root.pdf paper.pdf
+## Journal Version
+
+session4: Journal/ROOT.ML \
+ Journal/document/root* \
+ Journal/*.thy
+ @$(USEDIR) -D generated -f ROOT.ML HOL Journal
+
+journal: session4
+ rm -f Journal/generated/*.aux # otherwise latex will fall over
+ cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+ cd Journal/generated ; bibtex root
+ cd Journal/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+ cp Journal/generated/root.pdf journal.pdf
+
## clean
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/Paper.thy Wed May 18 19:54:43 2011 +0000
@@ -0,0 +1,1403 @@
+(*<*)
+theory Paper
+imports "../Derivs" "~~/src/HOL/Library/LaTeXsugar"
+begin
+
+declare [[show_question_marks = false]]
+
+consts
+ REL :: "(string \<times> string) \<Rightarrow> bool"
+ UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"
+
+abbreviation
+ "EClass x R \<equiv> R `` {x}"
+
+abbreviation
+ "Append_rexp2 r_itm r \<equiv> Append_rexp r r_itm"
+
+
+notation (latex output)
+ str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
+ str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and
+ Seq (infixr "\<cdot>" 100) and
+ Star ("_\<^bsup>\<star>\<^esup>") and
+ pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
+ Suc ("_+1" [100] 100) and
+ quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
+ REL ("\<approx>") and
+ UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
+ L ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
+ Lam ("\<lambda>'(_')" [100] 100) and
+ Trn ("'(_, _')" [100, 100] 100) and
+ EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
+ transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
+ Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
+ Append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
+ Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
+ uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
+ tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
+ tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and
+ tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
+ tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and
+ tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and
+ tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100)
+lemma meta_eq_app:
+ shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
+ by auto
+
+(*>*)
+
+
+section {* Introduction *}
+
+text {*
+ Regular languages are an important and well-understood subject in Computer
+ Science, with many beautiful theorems and many useful algorithms. There is a
+ wide range of textbooks on this subject, many of which are aimed at students
+ and contain very detailed `pencil-and-paper' proofs
+ (e.g.~\cite{Kozen97}). It seems natural to exercise theorem provers by
+ formalising the theorems and by verifying formally the algorithms.
+
+ There is however a problem: the typical approach to regular languages is to
+ introduce finite automata and then define everything in terms of them. For
+ example, a regular language is normally defined as one whose strings are
+ recognised by a finite deterministic automaton. This approach has many
+ benefits. Among them is the fact that it is easy to convince oneself that
+ regular languages are closed under complementation: one just has to exchange
+ the accepting and non-accepting states in the corresponding automaton to
+ obtain an automaton for the complement language. The problem, however, lies with
+ formalising such reasoning in a HOL-based theorem prover, in our case
+ Isabelle/HOL. Automata are built up from states and transitions that
+ need to be represented as graphs, matrices or functions, none
+ of which can be defined as an inductive datatype.
+
+ In case of graphs and matrices, this means we have to build our own
+ reasoning infrastructure for them, as neither Isabelle/HOL nor HOL4 nor
+ HOLlight support them with libraries. Even worse, reasoning about graphs and
+ matrices can be a real hassle in HOL-based theorem provers. Consider for
+ example the operation of sequencing two automata, say $A_1$ and $A_2$, by
+ connecting the accepting states of $A_1$ to the initial state of $A_2$:\\[-5.5mm]
+ %
+ \begin{center}
+ \begin{tabular}{ccc}
+ \begin{tikzpicture}[scale=0.8]
+ %\draw[step=2mm] (-1,-1) grid (1,1);
+
+ \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+ \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+
+ \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+
+ \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+
+ \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+
+ \draw (-0.6,0.0) node {\footnotesize$A_1$};
+ \draw ( 0.6,0.0) node {\footnotesize$A_2$};
+ \end{tikzpicture}
+
+ &
+
+ \raisebox{1.1mm}{\bf\Large$\;\;\;\Rightarrow\,\;\;$}
+
+ &
+
+ \begin{tikzpicture}[scale=0.8]
+ %\draw[step=2mm] (-1,-1) grid (1,1);
+
+ \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+ \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+
+ \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+
+ \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+
+ \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+ \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+
+ \draw (C) to [very thick, bend left=45] (B);
+ \draw (D) to [very thick, bend right=45] (B);
+
+ \draw (-0.6,0.0) node {\footnotesize$A_1$};
+ \draw ( 0.6,0.0) node {\footnotesize$A_2$};
+ \end{tikzpicture}
+
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ On `paper' we can define the corresponding graph in terms of the disjoint
+ union of the state nodes. Unfortunately in HOL, the standard definition for disjoint
+ union, namely
+ %
+ \begin{equation}\label{disjointunion}
+ @{term "UPLUS A\<^isub>1 A\<^isub>2 \<equiv> {(1, x) | x. x \<in> A\<^isub>1} \<union> {(2, y) | y. y \<in> A\<^isub>2}"}
+ \end{equation}
+
+ \noindent
+ changes the type---the disjoint union is not a set, but a set of pairs.
+ Using this definition for disjoint union means we do not have a single type for automata
+ and hence will not be able to state certain properties about \emph{all}
+ automata, since there is no type quantification available in HOL (unlike in Coq, for example). An
+ alternative, which provides us with a single type for automata, is to give every
+ state node an identity, for example a natural
+ number, and then be careful to rename these identities apart whenever
+ connecting two automata. This results in clunky proofs
+ establishing that properties are invariant under renaming. Similarly,
+ connecting two automata represented as matrices results in very adhoc
+ constructions, which are not pleasant to reason about.
+
+ Functions are much better supported in Isabelle/HOL, but they still lead to similar
+ problems as with graphs. Composing, for example, two non-deterministic automata in parallel
+ requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98}
+ dismisses for this the option of using identities, because it leads according to
+ him to ``messy proofs''. He
+ opts for a variant of \eqref{disjointunion} using bit lists, but writes
+
+ \begin{quote}
+ \it%
+ \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
+ `` & All lemmas appear obvious given a picture of the composition of automata\ldots
+ Yet their proofs require a painful amount of detail.''
+ \end{tabular}
+ \end{quote}
+
+ \noindent
+ and
+
+ \begin{quote}
+ \it%
+ \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
+ `` & If the reader finds the above treatment in terms of bit lists revoltingly
+ concrete, I cannot disagree. A more abstract approach is clearly desirable.''
+ \end{tabular}
+ \end{quote}
+
+
+ \noindent
+ Moreover, it is not so clear how to conveniently impose a finiteness condition
+ upon functions in order to represent \emph{finite} automata. The best is
+ probably to resort to more advanced reasoning frameworks, such as \emph{locales}
+ or \emph{type classes},
+ which are \emph{not} available in all HOL-based theorem provers.
+
+ {\bf add commnets from Brozowski}
+
+ Because of these problems to do with representing automata, there seems
+ to be no substantial formalisation of automata theory and regular languages
+ carried out in HOL-based theorem provers. Nipkow \cite{Nipkow98} establishes
+ the link between regular expressions and automata in
+ the context of lexing. Berghofer and Reiter \cite{BerghoferReiter09}
+ formalise automata working over
+ bit strings in the context of Presburger arithmetic.
+ The only larger formalisations of automata theory
+ are carried out in Nuprl \cite{Constable00} and in Coq \cite{Filliatre97}.
+
+ In this paper, we will not attempt to formalise automata theory in
+ Isabelle/HOL, but take a different approach to regular
+ languages. Instead of defining a regular language as one where there exists
+ an automaton that recognises all strings of the language, we define a
+ regular language as:
+
+ \begin{definition}
+ A language @{text A} is \emph{regular}, provided there is a regular expression that matches all
+ strings of @{text "A"}.
+ \end{definition}
+
+ \noindent
+ The reason is that regular expressions, unlike graphs, matrices and functions, can
+ be easily defined as inductive datatype. Consequently a corresponding reasoning
+ infrastructure comes for free. This has recently been exploited in HOL4 with a formalisation
+ of regular expression matching based on derivatives \cite{OwensSlind08} and
+ with an equivalence checker for regular expressions in Isabelle/HOL \cite{KraussNipkow11}.
+ The purpose of this paper is to
+ show that a central result about regular languages---the Myhill-Nerode theorem---can
+ be recreated by only using regular expressions. This theorem gives necessary
+ and sufficient conditions for when a language is regular. As a corollary of this
+ theorem we can easily establish the usual closure properties, including
+ complementation, for regular languages.\smallskip
+
+ \noindent
+ {\bf Contributions:}
+ There is an extensive literature on regular languages.
+ To our best knowledge, our proof of the Myhill-Nerode theorem is the
+ first that is based on regular expressions, only. We prove the part of this theorem
+ stating that a regular expression has only finitely many partitions using certain
+ tagging-functions. Again to our best knowledge, these tagging-functions have
+ not been used before to establish the Myhill-Nerode theorem.
+*}
+
+section {* Preliminaries *}
+
+text {*
+ Strings in Isabelle/HOL are lists of characters with the \emph{empty string}
+ being represented by the empty list, written @{term "[]"}. \emph{Languages}
+ are sets of strings. The language containing all strings is written in
+ Isabelle/HOL as @{term "UNIV::string set"}. The concatenation of two languages
+ is written @{term "A ;; B"} and a language raised to the power @{text n} is written
+ @{term "A \<up> n"}. They are defined as usual
+
+ \begin{center}
+ @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]}
+ \hspace{7mm}
+ @{thm pow.simps(1)[THEN eq_reflection, where A1="A"]}
+ \hspace{7mm}
+ @{thm pow.simps(2)[THEN eq_reflection, where A1="A" and n1="n"]}
+ \end{center}
+
+ \noindent
+ where @{text "@"} is the list-append operation. The Kleene-star of a language @{text A}
+ is defined as the union over all powers, namely @{thm Star_def}. In the paper
+ we will make use of the following properties of these constructions.
+
+ \begin{proposition}\label{langprops}\mbox{}\\
+ \begin{tabular}{@ {}ll}
+ (i) & @{thm star_cases} \\
+ (ii) & @{thm[mode=IfThen] pow_length}\\
+ (iii) & @{thm seq_Union_left} \\
+ \end{tabular}
+ \end{proposition}
+
+ \noindent
+ In @{text "(ii)"} we use the notation @{term "length s"} for the length of a
+ string; this property states that if \mbox{@{term "[] \<notin> A"}} then the lengths of
+ the strings in @{term "A \<up> (Suc n)"} must be longer than @{text n}. We omit
+ the proofs for these properties, but invite the reader to consult our
+ formalisation.\footnote{Available at \url{http://www4.in.tum.de/~urbanc/regexp.html}}
+
+ The notation in Isabelle/HOL for the quotient of a language @{text A} according to an
+ equivalence relation @{term REL} is @{term "A // REL"}. We will write
+ @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined
+ as \mbox{@{text "{y | y \<approx> x}"}}.
+
+
+ Central to our proof will be the solution of equational systems
+ involving equivalence classes of languages. For this we will use Arden's Lemma \cite{Brzozowski64},
+ which solves equations of the form @{term "X = A ;; X \<union> B"} provided
+ @{term "[] \<notin> A"}. However we will need the following `reverse'
+ version of Arden's Lemma (`reverse' in the sense of changing the order of @{term "A ;; X"} to
+ \mbox{@{term "X ;; A"}}).
+
+ \begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
+ If @{thm (prem 1) arden} then
+ @{thm (lhs) arden} if and only if
+ @{thm (rhs) arden}.
+ \end{lemma}
+
+ \begin{proof}
+ For the right-to-left direction we assume @{thm (rhs) arden} and show
+ that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"}
+ we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"},
+ which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both
+ sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side
+ is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction.
+
+ For the other direction we assume @{thm (lhs) arden}. By a simple induction
+ on @{text n}, we can establish the property
+
+ \begin{center}
+ @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper}
+ \end{center}
+
+ \noindent
+ Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for
+ all @{text n}. From this we can infer @{term "B ;; 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}
+ we know by Prop.~\ref{langprops}@{text "(ii)"} that
+ @{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}
+ (the strings in @{term "X ;; (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 ;; (A \<up> m))"}. This in turn
+ implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"}
+ this is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed
+ \end{proof}
+
+ \noindent
+ Regular expressions are defined as the inductive datatype
+
+ \begin{center}
+ @{text r} @{text "::="}
+ @{term NULL}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ @{term EMPTY}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ @{term "CHAR c"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ @{term "SEQ r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ @{term "ALT r r"}\hspace{1.5mm}@{text"|"}\hspace{1.5mm}
+ @{term "STAR r"}
+ \end{center}
+
+ \noindent
+ and the language matched by a regular expression is defined as
+
+ \begin{center}
+ \begin{tabular}{c@ {\hspace{10mm}}c}
+ \begin{tabular}{rcl}
+ @{thm (lhs) L_rexp.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(1)}\\
+ @{thm (lhs) L_rexp.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(2)}\\
+ @{thm (lhs) L_rexp.simps(3)[where c="c"]} & @{text "\<equiv>"} & @{thm (rhs) L_rexp.simps(3)[where c="c"]}\\
+ \end{tabular}
+ &
+ \begin{tabular}{rcl}
+ @{thm (lhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+ @{thm (rhs) L_rexp.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ @{thm (lhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & @{text "\<equiv>"} &
+ @{thm (rhs) L_rexp.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
+ @{thm (lhs) L_rexp.simps(6)[where r="r"]} & @{text "\<equiv>"} &
+ @{thm (rhs) L_rexp.simps(6)[where r="r"]}\\
+ \end{tabular}
+ \end{tabular}
+ \end{center}
+
+ Given a finite set of regular expressions @{text rs}, we will make use of the operation of generating
+ a regular expression that matches the union of all languages of @{text rs}. We only need to know the
+ existence
+ of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's
+ @{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const ALT} over the
+ set @{text rs} with @{const NULL} 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)"}}
+ \end{equation}
+
+ \noindent
+ holds, whereby @{text "\<calL> ` rs"} stands for the
+ image of the set @{text rs} under function @{text "\<calL>"}.
+*}
+
+
+section {* The Myhill-Nerode Theorem, First Part *}
+
+text {*
+ The key definition in the Myhill-Nerode theorem is the
+ \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two
+ strings are related, provided there is no distinguishing extension in this
+ language. This can be defined as a tertiary relation.
+
+ \begin{definition}[Myhill-Nerode Relation] Given a language @{text A}, two strings @{text x} and
+ @{text y} are Myhill-Nerode related provided
+ \begin{center}
+ @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}
+ \end{center}
+ \end{definition}
+
+ \noindent
+ It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
+ partitions the set of all strings, @{text "UNIV"}, into a set of disjoint
+ equivalence classes. To illustrate this quotient construction, let us give a simple
+ example: consider the regular language containing just
+ the string @{text "[c]"}. The relation @{term "\<approx>({[c]})"} partitions @{text UNIV}
+ into three equivalence classes @{text "X\<^isub>1"}, @{text "X\<^isub>2"} and @{text "X\<^isub>3"}
+ as follows
+
+ \begin{center}
+ @{text "X\<^isub>1 = {[]}"}\hspace{5mm}
+ @{text "X\<^isub>2 = {[c]}"}\hspace{5mm}
+ @{text "X\<^isub>3 = UNIV - {[], [c]}"}
+ \end{center}
+
+ One direction of the Myhill-Nerode theorem establishes
+ that if there are finitely many equivalence classes, like in the example above, then
+ the language is regular. In our setting we therefore have to show:
+
+ \begin{theorem}\label{myhillnerodeone}
+ @{thm[mode=IfThen] Myhill_Nerode1}
+ \end{theorem}
+
+ \noindent
+ To prove this theorem, we first define the set @{term "finals A"} as those equivalence
+ classes from @{term "UNIV // \<approx>A"} that contain strings of @{text A}, namely
+ %
+ \begin{equation}
+ @{thm finals_def}
+ \end{equation}
+
+ \noindent
+ In our running example, @{text "X\<^isub>2"} is the only
+ equivalence class in @{term "finals {[c]}"}.
+ It is straightforward to show that in general @{thm lang_is_union_of_finals} and
+ @{thm finals_in_partitions} hold.
+ Therefore if we know that there exists a regular expression for every
+ equivalence class in \mbox{@{term "finals A"}} (which by assumption must be
+ a finite set), then we can use @{text "\<bigplus>"} to obtain a regular expression
+ that matches every string in @{text A}.
+
+
+ Our proof of Thm.~\ref{myhillnerodeone} relies on a method that can calculate a
+ regular expression for \emph{every} equivalence class, not just the ones
+ in @{term "finals A"}. We
+ first define the notion of \emph{one-character-transition} between
+ two equivalence classes
+ %
+ \begin{equation}
+ @{thm transition_def}
+ \end{equation}
+
+ \noindent
+ which means that if we concatenate the character @{text c} to the end of all
+ strings in the equivalence class @{text Y}, we obtain a subset of
+ @{text X}. Note that we do not define an automaton here, we merely relate two sets
+ (with the help of a character). In our concrete example we have
+ @{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<Rightarrow> X\<^isub>3"} with @{text d} being any
+ other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>d\<Rightarrow> X\<^isub>3"} for any @{text d}.
+
+ Next we construct an \emph{initial equational system} that
+ contains an equation for each equivalence class. We first give
+ an informal description of this construction. Suppose we have
+ the equivalence classes @{text "X\<^isub>1,\<dots>,X\<^isub>n"}, there must be one and only one that
+ contains the empty string @{text "[]"} (since equivalence classes are disjoint).
+ Let us assume @{text "[] \<in> X\<^isub>1"}. We build the following equational system
+
+ \begin{center}
+ \begin{tabular}{rcl}
+ @{text "X\<^isub>1"} & @{text "="} & @{text "(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) + \<dots> + (Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) + \<lambda>(EMPTY)"} \\
+ @{text "X\<^isub>2"} & @{text "="} & @{text "(Y\<^isub>2\<^isub>1, CHAR c\<^isub>2\<^isub>1) + \<dots> + (Y\<^isub>2\<^isub>o, CHAR c\<^isub>2\<^isub>o)"} \\
+ & $\vdots$ \\
+ @{text "X\<^isub>n"} & @{text "="} & @{text "(Y\<^isub>n\<^isub>1, CHAR c\<^isub>n\<^isub>1) + \<dots> + (Y\<^isub>n\<^isub>q, CHAR c\<^isub>n\<^isub>q)"}\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"}
+ stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
+ X\<^isub>i"}.
+ %The intuition behind the equational system is that every
+ %equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
+ %corresponds roughly to a state of an automaton whose name is @{text X\<^isub>i} and its predecessor states
+ %are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these
+ %predecessor states to @{text X\<^isub>i}.
+ There can only be
+ finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side
+ since by assumption there are only finitely many
+ equivalence classes and only finitely many characters.
+ The term @{text "\<lambda>(EMPTY)"} in the first equation acts as a marker for the initial state, that
+ is the equivalence class
+ containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
+ single `initial' state in the equational system, which is different from
+ the method by Brzozowski \cite{Brzozowski64}, where he marks the
+ `terminal' states. We are forced to set up the equational system in our
+ way, because the Myhill-Nerode relation determines the `direction' of the
+ transitions---the successor `state' of an equivalence class @{text Y} can
+ be reached by adding a character to the end of @{text Y}. This is also the
+ reason why we have to use our reverse version of Arden's Lemma.}
+ %In our initial equation system there can only be
+ %finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side
+ %since by assumption there are only finitely many
+ %equivalence classes and only finitely many characters.
+ Overloading the function @{text \<calL>} for the two kinds of terms in the
+ equational system, we have
+
+ \begin{center}
+ @{text "\<calL>(Y, r) \<equiv>"} %
+ @{thm (rhs) L_rhs_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
+ @{thm L_rhs_trm.simps(1)[where r="r", THEN eq_reflection]}
+ \end{center}
+
+ \noindent
+ and we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
+ %
+ \begin{equation}\label{inv1}
+ @{text "X\<^isub>i = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}.
+ \end{equation}
+
+ \noindent
+ hold. Similarly for @{text "X\<^isub>1"} we can show the following equation
+ %
+ \begin{equation}\label{inv2}
+ @{text "X\<^isub>1 = \<calL>(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}.
+ \end{equation}
+
+ \noindent
+ holds. The reason for adding the @{text \<lambda>}-marker to our initial equational system is
+ to obtain this equation: it only holds with the marker, since none of
+ the other terms contain the empty string. The point of the initial equational system is
+ that solving it means we will be able to extract a regular expression for every equivalence class.
+
+ Our representation for the equations in Isabelle/HOL are pairs,
+ where the first component is an equivalence class (a set of strings)
+ and the second component
+ is a set of terms. Given a set of equivalence
+ classes @{text CS}, our initial equational system @{term "Init CS"} is thus
+ formally defined as
+ %
+ \begin{equation}\label{initcs}
+ \mbox{\begin{tabular}{rcl}
+ @{thm (lhs) Init_rhs_def} & @{text "\<equiv>"} &
+ @{text "if"}~@{term "[] \<in> X"}\\
+ & & @{text "then"}~@{term "{Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} \<union> {Lam EMPTY}"}\\
+ & & @{text "else"}~@{term "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"}\\
+ @{thm (lhs) Init_def} & @{text "\<equiv>"} & @{thm (rhs) Init_def}
+ \end{tabular}}
+ \end{equation}
+
+
+
+ \noindent
+ Because we use sets of terms
+ for representing the right-hand sides of equations, we can
+ prove \eqref{inv1} and \eqref{inv2} more concisely as
+ %
+ \begin{lemma}\label{inv}
+ If @{thm (prem 1) test} then @{text "X = \<Union> \<calL> ` rhs"}.
+ \end{lemma}
+
+ \noindent
+ Our proof of Thm.~\ref{myhillnerodeone} will proceed by transforming the
+ initial equational system into one in \emph{solved form} maintaining the invariant
+ in Lem.~\ref{inv}. From the solved form we will be able to read
+ off the regular expressions.
+
+ In order to transform an equational system into solved form, we have two
+ operations: one that takes an equation of the form @{text "X = rhs"} and removes
+ any recursive occurrences of @{text X} in the @{text rhs} using our variant of Arden's
+ Lemma. The other operation takes an equation @{text "X = rhs"}
+ and substitutes @{text X} throughout the rest of the equational system
+ adjusting the remaining regular expressions appropriately. To define this adjustment
+ we define the \emph{append-operation} taking a term and a regular expression as argument
+
+ \begin{center}
+ @{thm Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
+ @{thm Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+ \end{center}
+
+ \noindent
+ We lift this operation to entire right-hand sides of equations, written as
+ @{thm (lhs) Append_rexp_rhs_def[where rexp="r"]}. With this we can define
+ the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as:
+ %
+ \begin{equation}\label{arden_def}
+ \mbox{\begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
+ @{thm (lhs) Arden_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
+ & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
+ & & @{text "r' ="} & @{term "STAR (\<Uplus> {r. Trn X r \<in> rhs})"}\\
+ & & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "append_rhs_rexp rhs' r'"}}\\
+ \end{tabular}}
+ \end{equation}
+
+ \noindent
+ In this definition, we first delete all terms of the form @{text "(X, r)"} from @{text rhs};
+ then we calculate the combined regular expressions for all @{text r} coming
+ from the deleted @{text "(X, r)"}, and take the @{const STAR} of it;
+ finally we append this regular expression to @{text rhs'}. It can be easily seen
+ that this operation mimics Arden's Lemma on the level of equations. To ensure
+ the non-emptiness condition of Arden's Lemma we say that a right-hand side is
+ @{text ardenable} provided
+
+ \begin{center}
+ @{thm ardenable_def}
+ \end{center}
+
+ \noindent
+ This allows us to prove a version of Arden's Lemma on the level of equations.
+
+ \begin{lemma}\label{ardenable}
+ Given an equation @{text "X = rhs"}.
+ If @{text "X = \<Union>\<calL> ` rhs"},
+ @{thm (prem 2) Arden_keeps_eq}, and
+ @{thm (prem 3) Arden_keeps_eq}, then
+ @{text "X = \<Union>\<calL> ` (Arden X rhs)"}.
+ \end{lemma}
+
+ \noindent
+ Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma,
+ but we can still ensure that it holds troughout our algorithm of transforming equations
+ into solved form. The \emph{substitution-operation} takes an equation
+ of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
+
+ \begin{center}
+ \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
+ @{thm (lhs) Subst_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
+ & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
+ & & @{text "r' ="} & @{term "\<Uplus> {r. Trn X r \<in> rhs}"}\\
+ & & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "rhs' \<union> append_rhs_rexp xrhs r'"}}\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ We again delete first all occurrences of @{text "(X, r)"} in @{text rhs}; we then calculate
+ the regular expression corresponding to the deleted terms; finally we append this
+ regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use
+ the substitution operation we will arrange it so that @{text "xrhs"} does not contain
+ any occurrence of @{text X}.
+
+ With these two operations in place, we can define the operation that removes one equation
+ from an equational systems @{text ES}. The operation @{const Subst_all}
+ substitutes an equation @{text "X = xrhs"} throughout an equational system @{text ES};
+ @{const Remove} then completely removes such an equation from @{text ES} by substituting
+ it to the rest of the equational system, but first eliminating all recursive occurrences
+ of @{text X} by applying @{const Arden} to @{text "xrhs"}.
+
+ \begin{center}
+ \begin{tabular}{rcl}
+ @{thm (lhs) Subst_all_def} & @{text "\<equiv>"} & @{thm (rhs) Subst_all_def}\\
+ @{thm (lhs) Remove_def} & @{text "\<equiv>"} & @{thm (rhs) Remove_def}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ Finally, we can define how an equational system should be solved. For this
+ we will need to iterate the process of eliminating equations until only one equation
+ will be left in the system. However, we do not just want to have any equation
+ as being the last one, but the one involving the equivalence class for
+ which we want to calculate the regular
+ expression. Let us suppose this equivalence class is @{text X}.
+ Since @{text X} is the one to be solved, in every iteration step we have to pick an
+ equation to be eliminated that is different from @{text X}. In this way
+ @{text X} is kept to the final step. The choice is implemented using Hilbert's choice
+ operator, written @{text SOME} in the definition below.
+
+ \begin{center}
+ \begin{tabular}{rc@ {\hspace{4mm}}r@ {\hspace{1mm}}l}
+ @{thm (lhs) Iter_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "let"}}\\
+ & & @{text "(Y, yrhs) ="} & @{term "SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y"} \\
+ & & \multicolumn{2}{@ {\hspace{-4mm}}l}{@{text "in"}~~@{term "Remove ES Y yrhs"}}\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ The last definition we need applies @{term Iter} over and over until a condition
+ @{text Cond} is \emph{not} satisfied anymore. This condition states that there
+ are more than one equation left in the equational system @{text ES}. To solve
+ an equational system we use Isabelle/HOL's @{text while}-operator as follows:
+
+ \begin{center}
+ @{thm Solve_def}
+ \end{center}
+
+ \noindent
+ We are not concerned here with the definition of this operator
+ (see Berghofer and Nipkow \cite{BerghoferNipkow00}), but note that we eliminate
+ in each @{const Iter}-step a single equation, and therefore
+ have a well-founded termination order by taking the cardinality
+ of the equational system @{text ES}. This enables us to prove
+ properties about our definition of @{const Solve} when we `call' it with
+ the equivalence class @{text X} and the initial equational system
+ @{term "Init (UNIV // \<approx>A)"} from
+ \eqref{initcs} using the principle:
+ %
+ \begin{equation}\label{whileprinciple}
+ \mbox{\begin{tabular}{l}
+ @{term "invariant (Init (UNIV // \<approx>A))"} \\
+ @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> invariant (Iter X ES)"}\\
+ @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> card (Iter X ES) < card ES"}\\
+ @{term "\<forall>ES. invariant ES \<and> \<not> Cond ES \<longrightarrow> P ES"}\\
+ \hline
+ \multicolumn{1}{c}{@{term "P (Solve X (Init (UNIV // \<approx>A)))"}}
+ \end{tabular}}
+ \end{equation}
+
+ \noindent
+ This principle states that given an invariant (which we will specify below)
+ we can prove a property
+ @{text "P"} involving @{const Solve}. For this we have to discharge the following
+ proof obligations: first the
+ initial equational system satisfies the invariant; second the iteration
+ step @{text "Iter"} preserves the invariant as long as the condition @{term Cond} holds;
+ third @{text "Iter"} decreases the termination order, and fourth that
+ once the condition does not hold anymore then the property @{text P} must hold.
+
+ The property @{term P} in our proof will state that @{term "Solve X (Init (UNIV // \<approx>A))"}
+ returns with a single equation @{text "X = xrhs"} for some @{text "xrhs"}, and
+ that this equational system still satisfies the invariant. In order to get
+ the proof through, the invariant is composed of the following six properties:
+
+ \begin{center}
+ \begin{tabular}{@ {}rcl@ {\hspace{-13mm}}l @ {}}
+ @{text "invariant ES"} & @{text "\<equiv>"} &
+ @{term "finite ES"} & @{text "(finiteness)"}\\
+ & @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\
+ & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\
+ & @{text "\<and>"} & @{thm (rhs) distinctness_def}\\
+ & & & @{text "(distinctness)"}\\
+ & @{text "\<and>"} & @{thm (rhs) ardenable_all_def} & @{text "(ardenable)"}\\
+ & @{text "\<and>"} & @{thm (rhs) validity_def} & @{text "(validity)"}\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ The first two ensure that the equational system is always finite (number of equations
+ and number of terms in each equation); the third makes sure the `meaning' of the
+ equations is preserved under our transformations. The other properties are a bit more
+ technical, but are needed to get our proof through. Distinctness states that every
+ equation in the system is distinct. @{text Ardenable} ensures that we can always
+ apply the @{text Arden} operation.
+ The last property states that every @{text rhs} can only contain equivalence classes
+ for which there is an equation. Therefore @{text lhss} is just the set containing
+ the first components of an equational system,
+ while @{text "rhss"} collects all equivalence classes @{text X} in the terms of the
+ form @{term "Trn X r"}. That means formally @{thm (lhs) lhss_def}~@{text "\<equiv> {X | (X, rhs) \<in> ES}"}
+ and @{thm (lhs) rhss_def}~@{text "\<equiv> {X | (X, r) \<in> rhs}"}.
+
+
+ It is straightforward to prove that the initial equational system satisfies the
+ invariant.
+
+ \begin{lemma}\label{invzero}
+ @{thm[mode=IfThen] Init_ES_satisfies_invariant}
+ \end{lemma}
+
+ \begin{proof}
+ Finiteness is given by the assumption and the way how we set up the
+ initial equational system. Soundness is proved in Lem.~\ref{inv}. Distinctness
+ follows from the fact that the equivalence classes are disjoint. The @{text ardenable}
+ property also follows from the setup of the initial equational system, as does
+ validity.\qed
+ \end{proof}
+
+ \noindent
+ Next we show that @{text Iter} preserves the invariant.
+
+ \begin{lemma}\label{iterone}
+ @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
+ \end{lemma}
+
+ \begin{proof}
+ The argument boils down to choosing an equation @{text "Y = yrhs"} to be eliminated
+ and to show that @{term "Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"}
+ preserves the invariant.
+ We prove this as follows:
+
+ \begin{center}
+ @{text "\<forall> ES."} @{thm (prem 1) Subst_all_satisfies_invariant} implies
+ @{thm (concl) Subst_all_satisfies_invariant}
+ \end{center}
+
+ \noindent
+ Finiteness is straightforward, as the @{const Subst} and @{const Arden} operations
+ keep the equational system finite. These operations also preserve soundness
+ and distinctness (we proved soundness for @{const Arden} in Lem.~\ref{ardenable}).
+ The property @{text ardenable} is clearly preserved because the append-operation
+ cannot make a regular expression to match the empty string. Validity is
+ given because @{const Arden} removes an equivalence class from @{text yrhs}
+ and then @{const Subst_all} removes @{text Y} from the equational system.
+ Having proved the implication above, we can instantiate @{text "ES"} with @{text "ES - {(Y, yrhs)}"}
+ which matches with our proof-obligation of @{const "Subst_all"}. Since
+ \mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use the assumption
+ to complete the proof.\qed
+ \end{proof}
+
+ \noindent
+ We also need the fact that @{text Iter} decreases the termination measure.
+
+ \begin{lemma}\label{itertwo}
+ @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
+ \end{lemma}
+
+ \begin{proof}
+ By assumption we know that @{text "ES"} is finite and has more than one element.
+ Therefore there must be an element @{term "(Y, yrhs) \<in> ES"} with
+ @{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distinctness property we can infer
+ that @{term "Y \<noteq> X"}. We further know that @{text "Remove ES Y yrhs"}
+ removes the equation @{text "Y = yrhs"} from the system, and therefore
+ the cardinality of @{const Iter} strictly decreases.\qed
+ \end{proof}
+
+ \noindent
+ This brings us to our property we want to establish for @{text Solve}.
+
+
+ \begin{lemma}
+ If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists
+ a @{text rhs} such that @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"}
+ and @{term "invariant {(X, rhs)}"}.
+ \end{lemma}
+
+ \begin{proof}
+ In order to prove this lemma using \eqref{whileprinciple}, we have to use a slightly
+ stronger invariant since Lem.~\ref{iterone} and \ref{itertwo} have the precondition
+ that @{term "(X, rhs) \<in> ES"} for some @{text rhs}. This precondition is needed
+ in order to choose in the @{const Iter}-step an equation that is not \mbox{@{term "X = rhs"}}.
+ Therefore our invariant cannot be just @{term "invariant ES"}, but must be
+ @{term "invariant ES \<and> (\<exists>rhs. (X, rhs) \<in> ES)"}. By assumption
+ @{thm (prem 2) Solve} and Lem.~\ref{invzero}, the more general invariant holds for
+ the initial equational system. This is premise 1 of~\eqref{whileprinciple}.
+ Premise 2 is given by Lem.~\ref{iterone} and the fact that @{const Iter} might
+ modify the @{text rhs} in the equation @{term "X = rhs"}, but does not remove it.
+ Premise 3 of~\eqref{whileprinciple} is by Lem.~\ref{itertwo}. Now in premise 4
+ we like to show that there exists a @{text rhs} such that @{term "ES = {(X, rhs)}"}
+ and that @{text "invariant {(X, rhs)}"} holds, provided the condition @{text "Cond"}
+ does not holds. By the stronger invariant we know there exists such a @{text "rhs"}
+ with @{term "(X, rhs) \<in> ES"}. Because @{text Cond} is not true, we know the cardinality
+ of @{text ES} is @{text 1}. This means @{text "ES"} must actually be the set @{text "{(X, rhs)}"},
+ for which the invariant holds. This allows us to conclude that
+ @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"} and @{term "invariant {(X, rhs)}"} hold,
+ as needed.\qed
+ \end{proof}
+
+ \noindent
+ With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"}
+ there exists a regular expression.
+
+ \begin{lemma}\label{every_eqcl_has_reg}
+ @{thm[mode=IfThen] every_eqcl_has_reg}
+ \end{lemma}
+
+ \begin{proof}
+ By the preceding lemma, we know that there exists a @{text "rhs"} such
+ that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"},
+ and that the invariant holds for this equation. That means we
+ know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
+ this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the
+ invariant and Lem.~\ref{ardenable}. Using the validity property for the equation @{text "X = rhs"},
+ we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the @{text Arden} operation
+ removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
+ This means the right-hand side @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}.
+ So we can collect those (finitely many) regular expressions @{text rs} and have @{term "X = L (\<Uplus>rs)"}.
+ With this we can conclude the proof.\qed
+ \end{proof}
+
+ \noindent
+ Lem.~\ref{every_eqcl_has_reg} allows us to finally give a proof for the first direction
+ of the Myhill-Nerode theorem.
+
+ \begin{proof}[of Thm.~\ref{myhillnerodeone}]
+ By Lem.~\ref{every_eqcl_has_reg} we know that there exists a regular expression for
+ every equivalence class in @{term "UNIV // \<approx>A"}. Since @{text "finals A"} is
+ a subset of @{term "UNIV // \<approx>A"}, we also know that for every equivalence class
+ in @{term "finals A"} there exists a regular expression. Moreover by assumption
+ we know that @{term "finals A"} must be finite, and therefore there must be a finite
+ set of regular expressions @{text "rs"} such that
+ @{term "\<Union>(finals A) = L (\<Uplus>rs)"}.
+ Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"}
+ as the regular expression that is needed in the theorem.\qed
+ \end{proof}
+*}
+
+
+
+
+section {* Myhill-Nerode, Second Part *}
+
+text {*
+ We will prove in this section the second part of the Myhill-Nerode
+ theorem. It can be formulated in our setting as follows:
+
+ \begin{theorem}
+ Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}.
+ \end{theorem}
+
+ \noindent
+ The proof will be by induction on the structure of @{text r}. It turns out
+ the base cases are straightforward.
+
+
+ \begin{proof}[Base Cases]
+ The cases for @{const NULL}, @{const EMPTY} and @{const CHAR} are routine, because
+ we can easily establish that
+
+ \begin{center}
+ \begin{tabular}{l}
+ @{thm quot_null_eq}\\
+ @{thm quot_empty_subset}\\
+ @{thm quot_char_subset}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ hold, which shows that @{term "UNIV // \<approx>(L r)"} must be finite.\qed
+ \end{proof}
+
+ \noindent
+ Much more interesting, however, are the inductive cases. They seem hard to solve
+ directly. The reader is invited to try.
+
+ Our proof will rely on some
+ \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will
+ be easy to prove that the \emph{range} of these tagging-functions is finite
+ (the range of a function @{text f} is defined as @{text "range f \<equiv> f ` UNIV"}).
+ With this we will be able to infer that the tagging-functions, seen as relations,
+ give rise to finitely many equivalence classes of @{const UNIV}. Finally we
+ will show that the tagging-relations are more refined than @{term "\<approx>(L r)"}, which
+ implies that @{term "UNIV // \<approx>(L r)"} must also be finite (a relation @{text "R\<^isub>1"}
+ is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}).
+ We formally define the notion of a \emph{tagging-relation} as follows.
+
+ \begin{definition}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
+ and @{text y} are \emph{tag-related} provided
+ \begin{center}
+ @{text "x =tag= y \<equiv> tag x = tag y"}\;.
+ \end{center}
+ \end{definition}
+
+
+ In order to establish finiteness of a set @{text A}, we shall use the following powerful
+ principle from Isabelle/HOL's library.
+ %
+ \begin{equation}\label{finiteimageD}
+ @{thm[mode=IfThen] finite_imageD}
+ \end{equation}
+
+ \noindent
+ It states that if an image of a set under an injective function @{text f} (injective over this set)
+ is finite, then the set @{text A} itself must be finite. We can use it to establish the following
+ two lemmas.
+
+ \begin{lemma}\label{finone}
+ @{thm[mode=IfThen] finite_eq_tag_rel}
+ \end{lemma}
+
+ \begin{proof}
+ We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have
+ @{text "range f"} to be a subset of @{term "Pow (range tag)"}, which we know must be
+ finite by assumption. Now @{term "f (UNIV // =tag=)"} is a subset of @{text "range f"},
+ and so also finite. Injectivity amounts to showing that @{text "X = Y"} under the
+ assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}.
+ From the assumptions we can obtain @{text "x \<in> X"} and @{text "y \<in> Y"} with
+ @{text "tag x = tag y"}. Since @{text x} and @{text y} are tag-related, this in
+ turn means that the equivalence classes @{text X}
+ and @{text Y} must be equal.\qed
+ \end{proof}
+
+ \begin{lemma}\label{fintwo}
+ Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, whereby
+ @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
+ If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
+ then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
+ \end{lemma}
+
+ \begin{proof}
+ We prove this lemma again using \eqref{finiteimageD}. This time we set @{text f} to
+ be @{text "X \<mapsto>"}~@{term "{R\<^isub>1 `` {x} | x. x \<in> X}"}. It is easy to see that
+ @{term "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{term "Pow (UNIV // R\<^isub>1)"},
+ which is finite by assumption. What remains to be shown is that @{text f} is injective
+ on @{term "UNIV // R\<^isub>2"}. This is equivalent to showing that two equivalence
+ classes, say @{text "X"} and @{text Y}, in @{term "UNIV // R\<^isub>2"} are equal, provided
+ @{text "f X = f Y"}. For @{text "X = Y"} to be equal, we have to find two elements
+ @{text "x \<in> X"} and @{text "y \<in> Y"} such that they are @{text R\<^isub>2} related.
+ We know there exists a @{text "x \<in> X"} with \mbox{@{term "X = R\<^isub>2 `` {x}"}}.
+ From the latter fact we can infer that @{term "R\<^isub>1 ``{x} \<in> f X"}
+ and further @{term "R\<^isub>1 ``{x} \<in> f Y"}. This means we can obtain a @{text y}
+ such that @{term "R\<^isub>1 `` {x} = R\<^isub>1 `` {y}"} holds. Consequently @{text x} and @{text y}
+ are @{text "R\<^isub>1"}-related. Since by assumption @{text "R\<^isub>1"} refines @{text "R\<^isub>2"},
+ they must also be @{text "R\<^isub>2"}-related, as we need to show.\qed
+ \end{proof}
+
+ \noindent
+ Chaining Lem.~\ref{finone} and \ref{fintwo} together, means in order to show
+ that @{term "UNIV // \<approx>(L r)"} is finite, we have to find a tagging-function whose
+ range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(L r)"}.
+ Let us attempt the @{const ALT}-case first.
+
+ \begin{proof}[@{const "ALT"}-Case]
+ We take as tagging-function
+ %
+ \begin{center}
+ @{thm tag_str_ALT_def[where A="A" and B="B", THEN meta_eq_app]}
+ \end{center}
+
+ \noindent
+ where @{text "A"} and @{text "B"} are some arbitrary languages.
+ We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
+ then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of
+ @{term "tag_str_ALT A B"} is a subset of this product set---so finite. It remains to be shown
+ that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to
+ showing
+ %
+ \begin{center}
+ @{term "tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<longrightarrow> x \<approx>(A \<union> B) y"}
+ \end{center}
+ %
+ \noindent
+ which by unfolding the Myhill-Nerode relation is identical to
+ %
+ \begin{equation}\label{pattern}
+ @{text "\<forall>z. tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<and> x @ z \<in> A \<union> B \<longrightarrow> y @ z \<in> A \<union> B"}
+ \end{equation}
+ %
+ \noindent
+ since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve
+ \eqref{pattern} we just have to unfold the definition of the tagging-function and analyse
+ in which set, @{text A} or @{text B}, the string @{term "x @ z"} is.
+ The definition of the tagging-function will give us in each case the
+ information to infer that @{text "y @ z \<in> A \<union> B"}.
+ Finally we
+ can discharge this case by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed
+ \end{proof}
+
+
+ \noindent
+ The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,
+ they are slightly more complicated. In the @{const SEQ}-case we essentially have
+ to be able to infer that
+ %
+ \begin{center}
+ @{text "\<dots>"}@{term "x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
+ \end{center}
+ %
+ \noindent
+ using the information given by the appropriate tagging-function. The complication
+ is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A ;; B"}
+ (this was easy in case of @{term "A \<union> B"}). To deal with this complication we define the
+ notions of \emph{string prefixes}
+ %
+ \begin{center}
+ @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\hspace{10mm}
+ @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}
+ \end{center}
+ %
+ \noindent
+ and \emph{string subtraction}:
+ %
+ \begin{center}
+ @{text "[] - y \<equiv> []"}\hspace{10mm}
+ @{text "x - [] \<equiv> x"}\hspace{10mm}
+ @{text "cx - dy \<equiv> if c = d then x - y else cx"}
+ \end{center}
+ %
+ \noindent
+ where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.
+
+ Now assuming @{term "x @ z \<in> A ;; B"} there are only two possible ways of how to `split'
+ this string to be in @{term "A ;; B"}:
+ %
+ \begin{center}
+ \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+ \scalebox{0.7}{
+ \begin{tikzpicture}
+ \node[draw,minimum height=3.8ex] (xa) { $\hspace{3em}@{text "x'"}\hspace{3em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.2em}@{text "x - x'"}\hspace{0.2em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (z) { $\hspace{5em}@{text z}\hspace{5em}$ };
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{@{text x}};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (z.north west) -- ($(z.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{@{text z}};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
+ node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{@{term "(x - x') @ z \<in> B"}};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{@{term "x' \<in> A"}};
+ \end{tikzpicture}}
+ &
+ \scalebox{0.7}{
+ \begin{tikzpicture}
+ \node[draw,minimum height=3.8ex] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{0.6em}@{text "z'"}\hspace{0.6em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{2.6em}@{text "z - z'"}\hspace{2.6em}$ };
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (x.north west) -- ($(za.north west)+(0em,0em)$)
+ node[midway, above=0.5em]{@{text x}};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
+ node[midway, above=0.5em]{@{text z}};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
+ node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{@{text "x @ z' \<in> A"}};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)
+ node[midway, below=0.5em]{@{text "(z - z') \<in> B"}};
+ \end{tikzpicture}}
+ \end{tabular}
+ \end{center}
+ %
+ \noindent
+ Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B} (first picture),
+ or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} (second picture).
+ In both cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the
+ following tagging-function
+ %
+ \begin{center}
+ @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
+ \end{center}
+
+ \noindent
+ with the idea that in the first split we have to make sure that @{text "(x - x') @ z"}
+ is in the language @{text B}.
+
+ \begin{proof}[@{const SEQ}-Case]
+ If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
+ then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
+ @{term "tag_str_SEQ A B"} is a subset of this product set, and therefore finite.
+ We have to show injectivity of this tagging-function as
+ %
+ \begin{center}
+ @{term "\<forall>z. tag_str_SEQ A B x = tag_str_SEQ A B y \<and> x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
+ \end{center}
+ %
+ \noindent
+ There are two cases to be considered (see pictures above). First, there exists
+ a @{text "x'"} such that
+ @{text "x' \<in> A"}, @{text "x' \<le> x"} and @{text "(x - x') @ z \<in> B"} hold. We therefore have
+ %
+ \begin{center}
+ @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A})"}
+ \end{center}
+ %
+ \noindent
+ and by the assumption about @{term "tag_str_SEQ A B"} also
+ %
+ \begin{center}
+ @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A})"}
+ \end{center}
+ %
+ \noindent
+ That means there must be a @{text "y'"} such that @{text "y' \<in> A"} and
+ @{term "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"}. This equality means that
+ @{term "(x - x') \<approx>B (y - y')"} holds. Unfolding the Myhill-Nerode
+ relation and together with the fact that @{text "(x - x') @ z \<in> B"}, we
+ have @{text "(y - y') @ z \<in> B"}. We already know @{text "y' \<in> A"}, therefore
+ @{term "y @ z \<in> A ;; B"}, as needed in this case.
+
+ Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}.
+ By the assumption about @{term "tag_str_SEQ A B"} we have
+ @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode
+ relation that @{term "y @ z' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude also in this case
+ with @{term "y @ z \<in> A ;; B"}. We again can complete the @{const SEQ}-case
+ by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed
+ \end{proof}
+
+ \noindent
+ The case for @{const STAR} is similar to @{const SEQ}, but poses a few extra challenges. When
+ we analyse the case that @{text "x @ z"} is an element in @{term "A\<star>"} and @{text x} is not the
+ empty string, we
+ have the following picture:
+ %
+ \begin{center}
+ \scalebox{0.7}{
+ \begin{tikzpicture}
+ \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{4em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{0.5em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of xxa] (za) { $\hspace{2em}@{text "z\<^isub>a"}\hspace{2em}$ };
+ \node[draw,minimum height=3.8ex, right=-0.03em of za] (zb) { $\hspace{7em}@{text "z\<^isub>b"}\hspace{7em}$ };
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (xa.north west) -- ($(xxa.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{@{text x}};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ (za.north west) -- ($(zb.north east)+(0em,0em)$)
+ node[midway, above=0.5em]{@{text z}};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$)
+ node[midway, above=0.8em]{@{term "x @ z \<in> A\<star>"}};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"}};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{@{term "x'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"}};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
+ node[midway, below=0.5em]{@{term "z\<^isub>b \<in> A\<star>"}};
+
+ \draw[decoration={brace,transform={yscale=3}},decorate]
+ ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
+ node[midway, below=0.5em]{@{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}};
+ \end{tikzpicture}}
+ \end{center}
+ %
+ \noindent
+ We can find a strict prefix @{text "x'"} of @{text x} such that @{term "x' \<in> A\<star>"},
+ @{text "x' < x"} and the rest @{term "(x - x') @ z \<in> A\<star>"}. For example the empty string
+ @{text "[]"} would do.
+ There are potentially many such prefixes, but there can only be finitely many of them (the
+ string @{text x} is finite). Let us therefore choose the longest one and call it
+ @{text "x'\<^isub>m\<^isub>a\<^isub>x"}. Now for the rest of the string @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z"} we
+ know it is in @{term "A\<star>"}. By definition of @{term "A\<star>"}, we can separate
+ this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<in> A"}
+ and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x - x'\<^isub>m\<^isub>a\<^isub>x"},
+ otherwise @{text "x'\<^isub>m\<^isub>a\<^isub>x"} is not the longest prefix. That means @{text a}
+ `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and
+ @{text "z\<^isub>b"}. For this we know that @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"} and
+ @{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"}
+ such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the
+ `border' of @{text x} and @{text z}. This string is @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a"}.
+
+ In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use
+ the following tagging-function:
+ %
+ \begin{center}
+ @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}\smallskip
+ \end{center}
+
+ \begin{proof}[@{const STAR}-Case]
+ If @{term "finite (UNIV // \<approx>A)"}
+ then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of
+ @{term "tag_str_STAR A"} is a subset of this set, and therefore finite.
+ Again we have to show injectivity of this tagging-function as
+ %
+ \begin{center}
+ @{term "\<forall>z. tag_str_STAR A x = tag_str_STAR A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"}
+ \end{center}
+ %
+ \noindent
+ We first need to consider the case that @{text x} is the empty string.
+ From the assumption we can infer @{text y} is the empty string and
+ clearly have @{term "y @ z \<in> A\<star>"}. In case @{text x} is not the empty
+ string, we can divide the string @{text "x @ z"} as shown in the picture
+ above. By the tagging-function we have
+ %
+ \begin{center}
+ @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {x - x'} |x'. x' < x \<and> x' \<in> A\<star>})"}
+ \end{center}
+ %
+ \noindent
+ which by assumption is equal to
+ %
+ \begin{center}
+ @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {y - y'} |y'. y' < y \<and> y' \<in> A\<star>})"}
+ \end{center}
+ %
+ \noindent
+ and we know that we have a @{term "y' \<in> A\<star>"} and @{text "y' < y"}
+ and also know @{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) \<approx>A (y - y')"}. Unfolding the Myhill-Nerode
+ relation we know @{term "(y - y') @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}.
+ Therefore @{term "y' @ ((y - y') @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means
+ @{term "y @ z \<in> A\<star>"}. As the last step we have to set @{text "A"} to @{term "L r"} and
+ complete the proof.\qed
+ \end{proof}
+*}
+
+section {* Second Part based on Partial Derivatives *}
+
+text {*
+ We briefly considered using the method Brzozowski presented in the
+ Appendix of~\cite{Brzozowski64} in order to prove the second
+ direction of the Myhill-Nerode theorem. There he calculates the
+ derivatives for regular expressions and shows that for every
+ language there can be only finitely many of them %derivations (if
+ regarded equal modulo ACI). We could have used as tagging-function
+ the set of derivatives of a regular expression with respect to a
+ language. Using the fact that two strings are Myhill-Nerode related
+ whenever their derivative is the same, together with the fact that
+ there are only finitely such derivatives would give us a similar
+ argument as ours. However it seems not so easy to calculate the set
+ of derivatives modulo ACI. Therefore we preferred our direct method
+ of using tagging-functions.
+
+*}
+
+section {* Closure Properties *}
+
+
+section {* Conclusion and Related Work *}
+
+text {*
+ In this paper we took the view that a regular language is one where there
+ exists a regular expression that matches all of its strings. Regular
+ expressions can conveniently be defined as a datatype in HOL-based theorem
+ provers. For us it was therefore interesting to find out how far we can push
+ this point of view. We have established in Isabelle/HOL both directions
+ of the Myhill-Nerode theorem.
+ %
+ \begin{theorem}[The Myhill-Nerode Theorem]\mbox{}\\
+ A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}.
+ \end{theorem}
+ %
+ \noindent
+ Having formalised this theorem means we
+ pushed our point of view quite far. Using this theorem we can obviously prove when a language
+ is \emph{not} regular---by establishing that it has infinitely many
+ equivalence classes generated by the Myhill-Nerode relation (this is usually
+ the purpose of the pumping lemma \cite{Kozen97}). We can also use it to
+ establish the standard textbook results about closure properties of regular
+ languages. Interesting is the case of closure under complement, because
+ it seems difficult to construct a regular expression for the complement
+ language by direct means. However the existence of such a regular expression
+ can be easily proved using the Myhill-Nerode theorem since
+ %
+ \begin{center}
+ @{term "s\<^isub>1 \<approx>A s\<^isub>2"} if and only if @{term "s\<^isub>1 \<approx>(-A) s\<^isub>2"}
+ \end{center}
+ %
+ \noindent
+ holds for any strings @{text "s\<^isub>1"} and @{text
+ "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} give rise to the same
+ partitions. Proving the existence of such a regular expression via automata
+ using the standard method would
+ be quite involved. It includes the
+ steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text
+ "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"}
+ regular expression.
+
+ While regular expressions are convenient in formalisations, they have some
+ limitations. One is that there seems to be no method of calculating a
+ minimal regular expression (for example in terms of length) for a regular
+ language, like there is
+ for automata. On the other hand, efficient regular expression matching,
+ without using automata, poses no problem \cite{OwensReppyTuron09}.
+ For an implementation of a simple regular expression matcher,
+ whose correctness has been formally established, we refer the reader to
+ Owens and Slind \cite{OwensSlind08}.
+
+
+ Our formalisation consists of 780 lines of Isabelle/Isar code for the first
+ direction and 460 for the second, plus around 300 lines of standard material about
+ regular languages. While this might be seen as too large to count as a
+ concise proof pearl, this should be seen in the context of the work done by
+ Constable at al \cite{Constable00} who formalised the Myhill-Nerode theorem
+ in Nuprl using automata. They write that their four-member team needed
+ something on the magnitude of 18 months for their formalisation. The
+ estimate for our formalisation is that we needed approximately 3 months and
+ this included the time to find our proof arguments. Unlike Constable et al,
+ who were able to follow the proofs from \cite{HopcroftUllman69}, we had to
+ find our own arguments. So for us the formalisation was not the
+ bottleneck. It is hard to gauge the size of a formalisation in Nurpl, but
+ from what is shown in the Nuprl Math Library about their development it
+ seems substantially larger than ours. The code of ours can be found in the
+ Mercurial Repository at
+ \mbox{\url{http://www4.in.tum.de/~urbanc/regexp.html}}.
+
+
+ Our proof of the first direction is very much inspired by \emph{Brzozowski's
+ algebraic method} used to convert a finite automaton to a regular
+ expression \cite{Brzozowski64}. The close connection can be seen by considering the equivalence
+ classes as the states of the minimal automaton for the regular language.
+ However there are some subtle differences. Since we identify equivalence
+ classes with the states of the automaton, then the most natural choice is to
+ characterise each state with the set of strings starting from the initial
+ state leading up to that state. Usually, however, the states are characterised as the
+ strings starting from that state leading to the terminal states. The first
+ choice has consequences about how the initial equational system is set up. We have
+ the $\lambda$-term on our `initial state', while Brzozowski has it on the
+ terminal states. This means we also need to reverse the direction of Arden's
+ Lemma.
+
+ This is also where our method shines, because we can completely
+ side-step the standard argument \cite{Kozen97} where automata need
+ to be composed, which as stated in the Introduction is not so easy
+ to formalise in a HOL-based theorem prover. However, it is also the
+ direction where we had to spend most of the `conceptual' time, as
+ our proof-argument based on tagging-functions is new for
+ establishing the Myhill-Nerode theorem. All standard proofs of this
+ direction proceed by arguments over automata.\medskip
+
+ \noindent
+ {\bf Acknowledgements:} We are grateful for the comments we received from Larry
+ Paulson.
+
+*}
+
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/ROOT.ML Wed May 18 19:54:43 2011 +0000
@@ -0,0 +1,6 @@
+no_document use_thy "../Myhill";
+no_document use_thy "~~/src/HOL/Library/LaTeXsugar";
+no_document use_thy "../Derivs";
+no_document use_thy "../Closure";
+
+use_thy "Paper"
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/document/llncs.cls Wed May 18 19:54:43 2011 +0000
@@ -0,0 +1,1189 @@
+% LLNCS DOCUMENT CLASS -- version 2.13 (28-Jan-2002)
+% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science
+%
+%%
+%% \CharacterTable
+%% {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%% Lower-case \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%% Digits \0\1\2\3\4\5\6\7\8\9
+%% Exclamation \! Double quote \" Hash (number) \#
+%% Dollar \$ Percent \% Ampersand \&
+%% Acute accent \' Left paren \( Right paren \)
+%% Asterisk \* Plus \+ Comma \,
+%% Minus \- Point \. Solidus \/
+%% Colon \: Semicolon \; Less than \<
+%% Equals \= Greater than \> Question mark \?
+%% Commercial at \@ Left bracket \[ Backslash \\
+%% Right bracket \] Circumflex \^ Underscore \_
+%% Grave accent \` Left brace \{ Vertical bar \|
+%% Right brace \} Tilde \~}
+%%
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesClass{llncs}[2002/01/28 v2.13
+^^J LaTeX document class for Lecture Notes in Computer Science]
+% Options
+\let\if@envcntreset\iffalse
+\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue}
+\DeclareOption{citeauthoryear}{\let\citeauthoryear=Y}
+\DeclareOption{oribibl}{\let\oribibl=Y}
+\let\if@custvec\iftrue
+\DeclareOption{orivec}{\let\if@custvec\iffalse}
+\let\if@envcntsame\iffalse
+\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue}
+\let\if@envcntsect\iffalse
+\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue}
+\let\if@runhead\iffalse
+\DeclareOption{runningheads}{\let\if@runhead\iftrue}
+
+\let\if@openbib\iffalse
+\DeclareOption{openbib}{\let\if@openbib\iftrue}
+
+% languages
+\let\switcht@@therlang\relax
+\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}}
+\def\ds@francais{\def\switcht@@therlang{\switcht@francais}}
+
+\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}}
+
+\ProcessOptions
+
+\LoadClass[twoside]{article}
+\RequirePackage{multicol} % needed for the list of participants, index
+
+\setlength{\textwidth}{12.2cm}
+\setlength{\textheight}{19.3cm}
+\renewcommand\@pnumwidth{2em}
+\renewcommand\@tocrmarg{3.5em}
+%
+\def\@dottedtocline#1#2#3#4#5{%
+ \ifnum #1>\c@tocdepth \else
+ \vskip \z@ \@plus.2\p@
+ {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \parindent #2\relax\@afterindenttrue
+ \interlinepenalty\@M
+ \leavevmode
+ \@tempdima #3\relax
+ \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip
+ {#4}\nobreak
+ \leaders\hbox{$\m@th
+ \mkern \@dotsep mu\hbox{.}\mkern \@dotsep
+ mu$}\hfill
+ \nobreak
+ \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}%
+ \par}%
+ \fi}
+%
+\def\switcht@albion{%
+\def\abstractname{Abstract.}
+\def\ackname{Acknowledgement.}
+\def\andname{and}
+\def\lastandname{\unskip, and}
+\def\appendixname{Appendix}
+\def\chaptername{Chapter}
+\def\claimname{Claim}
+\def\conjecturename{Conjecture}
+\def\contentsname{Table of Contents}
+\def\corollaryname{Corollary}
+\def\definitionname{Definition}
+\def\examplename{Example}
+\def\exercisename{Exercise}
+\def\figurename{Fig.}
+\def\keywordname{{\bf Key words:}}
+\def\indexname{Index}
+\def\lemmaname{Lemma}
+\def\contriblistname{List of Contributors}
+\def\listfigurename{List of Figures}
+\def\listtablename{List of Tables}
+\def\mailname{{\it Correspondence to\/}:}
+\def\noteaddname{Note added in proof}
+\def\notename{Note}
+\def\partname{Part}
+\def\problemname{Problem}
+\def\proofname{Proof}
+\def\propertyname{Property}
+\def\propositionname{Proposition}
+\def\questionname{Question}
+\def\remarkname{Remark}
+\def\seename{see}
+\def\solutionname{Solution}
+\def\subclassname{{\it Subject Classifications\/}:}
+\def\tablename{Table}
+\def\theoremname{Theorem}}
+\switcht@albion
+% Names of theorem like environments are already defined
+% but must be translated if another language is chosen
+%
+% French section
+\def\switcht@francais{%\typeout{On parle francais.}%
+ \def\abstractname{R\'esum\'e.}%
+ \def\ackname{Remerciements.}%
+ \def\andname{et}%
+ \def\lastandname{ et}%
+ \def\appendixname{Appendice}
+ \def\chaptername{Chapitre}%
+ \def\claimname{Pr\'etention}%
+ \def\conjecturename{Hypoth\`ese}%
+ \def\contentsname{Table des mati\`eres}%
+ \def\corollaryname{Corollaire}%
+ \def\definitionname{D\'efinition}%
+ \def\examplename{Exemple}%
+ \def\exercisename{Exercice}%
+ \def\figurename{Fig.}%
+ \def\keywordname{{\bf Mots-cl\'e:}}
+ \def\indexname{Index}
+ \def\lemmaname{Lemme}%
+ \def\contriblistname{Liste des contributeurs}
+ \def\listfigurename{Liste des figures}%
+ \def\listtablename{Liste des tables}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
+ \def\notename{Remarque}%
+ \def\partname{Partie}%
+ \def\problemname{Probl\`eme}%
+ \def\proofname{Preuve}%
+ \def\propertyname{Caract\'eristique}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Question}%
+ \def\remarkname{Remarque}%
+ \def\seename{voir}
+ \def\solutionname{Solution}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tableau}%
+ \def\theoremname{Th\'eor\`eme}%
+}
+%
+% German section
+\def\switcht@deutsch{%\typeout{Man spricht deutsch.}%
+ \def\abstractname{Zusammenfassung.}%
+ \def\ackname{Danksagung.}%
+ \def\andname{und}%
+ \def\lastandname{ und}%
+ \def\appendixname{Anhang}%
+ \def\chaptername{Kapitel}%
+ \def\claimname{Behauptung}%
+ \def\conjecturename{Hypothese}%
+ \def\contentsname{Inhaltsverzeichnis}%
+ \def\corollaryname{Korollar}%
+%\def\definitionname{Definition}%
+ \def\examplename{Beispiel}%
+ \def\exercisename{\"Ubung}%
+ \def\figurename{Abb.}%
+ \def\keywordname{{\bf Schl\"usselw\"orter:}}
+ \def\indexname{Index}
+%\def\lemmaname{Lemma}%
+ \def\contriblistname{Mitarbeiter}
+ \def\listfigurename{Abbildungsverzeichnis}%
+ \def\listtablename{Tabellenverzeichnis}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Nachtrag}%
+ \def\notename{Anmerkung}%
+ \def\partname{Teil}%
+%\def\problemname{Problem}%
+ \def\proofname{Beweis}%
+ \def\propertyname{Eigenschaft}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Frage}%
+ \def\remarkname{Anmerkung}%
+ \def\seename{siehe}
+ \def\solutionname{L\"osung}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tabelle}%
+%\def\theoremname{Theorem}%
+}
+
+% Ragged bottom for the actual page
+\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil
+\global\let\@textbottom\relax}}
+
+\renewcommand\small{%
+ \@setfontsize\small\@ixpt{11}%
+ \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@
+ \abovedisplayshortskip \z@ \@plus2\p@
+ \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
+ \def\@listi{\leftmargin\leftmargini
+ \parsep 0\p@ \@plus1\p@ \@minus\p@
+ \topsep 8\p@ \@plus2\p@ \@minus4\p@
+ \itemsep0\p@}%
+ \belowdisplayskip \abovedisplayskip
+}
+
+\frenchspacing
+\widowpenalty=10000
+\clubpenalty=10000
+
+\setlength\oddsidemargin {63\p@}
+\setlength\evensidemargin {63\p@}
+\setlength\marginparwidth {90\p@}
+
+\setlength\headsep {16\p@}
+
+\setlength\footnotesep{7.7\p@}
+\setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@}
+\setlength\intextsep {8mm\@plus 2\p@ \@minus 2\p@}
+
+\setcounter{secnumdepth}{2}
+
+\newcounter {chapter}
+\renewcommand\thechapter {\@arabic\c@chapter}
+
+\newif\if@mainmatter \@mainmattertrue
+\newcommand\frontmatter{\cleardoublepage
+ \@mainmatterfalse\pagenumbering{Roman}}
+\newcommand\mainmatter{\cleardoublepage
+ \@mainmattertrue\pagenumbering{arabic}}
+\newcommand\backmatter{\if@openright\cleardoublepage\else\clearpage\fi
+ \@mainmatterfalse}
+
+\renewcommand\part{\cleardoublepage
+ \thispagestyle{empty}%
+ \if@twocolumn
+ \onecolumn
+ \@tempswatrue
+ \else
+ \@tempswafalse
+ \fi
+ \null\vfil
+ \secdef\@part\@spart}
+
+\def\@part[#1]#2{%
+ \ifnum \c@secnumdepth >-2\relax
+ \refstepcounter{part}%
+ \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}%
+ \else
+ \addcontentsline{toc}{part}{#1}%
+ \fi
+ \markboth{}{}%
+ {\centering
+ \interlinepenalty \@M
+ \normalfont
+ \ifnum \c@secnumdepth >-2\relax
+ \huge\bfseries \partname~\thepart
+ \par
+ \vskip 20\p@
+ \fi
+ \Huge \bfseries #2\par}%
+ \@endpart}
+\def\@spart#1{%
+ {\centering
+ \interlinepenalty \@M
+ \normalfont
+ \Huge \bfseries #1\par}%
+ \@endpart}
+\def\@endpart{\vfil\newpage
+ \if@twoside
+ \null
+ \thispagestyle{empty}%
+ \newpage
+ \fi
+ \if@tempswa
+ \twocolumn
+ \fi}
+
+\newcommand\chapter{\clearpage
+ \thispagestyle{empty}%
+ \global\@topnum\z@
+ \@afterindentfalse
+ \secdef\@chapter\@schapter}
+\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne
+ \if@mainmatter
+ \refstepcounter{chapter}%
+ \typeout{\@chapapp\space\thechapter.}%
+ \addcontentsline{toc}{chapter}%
+ {\protect\numberline{\thechapter}#1}%
+ \else
+ \addcontentsline{toc}{chapter}{#1}%
+ \fi
+ \else
+ \addcontentsline{toc}{chapter}{#1}%
+ \fi
+ \chaptermark{#1}%
+ \addtocontents{lof}{\protect\addvspace{10\p@}}%
+ \addtocontents{lot}{\protect\addvspace{10\p@}}%
+ \if@twocolumn
+ \@topnewpage[\@makechapterhead{#2}]%
+ \else
+ \@makechapterhead{#2}%
+ \@afterheading
+ \fi}
+\def\@makechapterhead#1{%
+% \vspace*{50\p@}%
+ {\centering
+ \ifnum \c@secnumdepth >\m@ne
+ \if@mainmatter
+ \large\bfseries \@chapapp{} \thechapter
+ \par\nobreak
+ \vskip 20\p@
+ \fi
+ \fi
+ \interlinepenalty\@M
+ \Large \bfseries #1\par\nobreak
+ \vskip 40\p@
+ }}
+\def\@schapter#1{\if@twocolumn
+ \@topnewpage[\@makeschapterhead{#1}]%
+ \else
+ \@makeschapterhead{#1}%
+ \@afterheading
+ \fi}
+\def\@makeschapterhead#1{%
+% \vspace*{50\p@}%
+ {\centering
+ \normalfont
+ \interlinepenalty\@M
+ \Large \bfseries #1\par\nobreak
+ \vskip 40\p@
+ }}
+
+\renewcommand\section{\@startsection{section}{1}{\z@}%
+ {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+ {12\p@ \@plus 4\p@ \@minus 4\p@}%
+ {\normalfont\large\bfseries\boldmath
+ \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
+ {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+ {8\p@ \@plus 4\p@ \@minus 4\p@}%
+ {\normalfont\normalsize\bfseries\boldmath
+ \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
+ {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+ {-0.5em \@plus -0.22em \@minus -0.1em}%
+ {\normalfont\normalsize\bfseries\boldmath}}
+\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
+ {-12\p@ \@plus -4\p@ \@minus -4\p@}%
+ {-0.5em \@plus -0.22em \@minus -0.1em}%
+ {\normalfont\normalsize\itshape}}
+\renewcommand\subparagraph[1]{\typeout{LLNCS warning: You should not use
+ \string\subparagraph\space with this class}\vskip0.5cm
+You should not use \verb|\subparagraph| with this class.\vskip0.5cm}
+
+\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00}
+\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01}
+\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02}
+\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03}
+\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04}
+\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05}
+\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06}
+\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07}
+\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08}
+\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09}
+\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A}
+
+\let\footnotesize\small
+
+\if@custvec
+\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle#1$}}
+{\mbox{\boldmath$\textstyle#1$}}
+{\mbox{\boldmath$\scriptstyle#1$}}
+{\mbox{\boldmath$\scriptscriptstyle#1$}}}
+\fi
+
+\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
+\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
+\penalty50\hskip1em\null\nobreak\hfil\squareforqed
+\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}
+
+\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr\gets\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+\gets\cr\to\cr}}}}}
+\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+<\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr
+>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.8pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.3pt}<\cr}}}}}
+\def\bbbr{{\rm I\!R}} %reelle Zahlen
+\def\bbbm{{\rm I\!M}}
+\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
+\def\bbbf{{\rm I\!F}}
+\def\bbbh{{\rm I\!H}}
+\def\bbbk{{\rm I\!K}}
+\def\bbbp{{\rm I\!P}}
+\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
+{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
+\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}
+\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbs{{\mathchoice
+{\setbox0=\hbox{$\displaystyle \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}}
+\def\bbbz{{\mathchoice {\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\scriptstyle Z\kern-0.3em Z$}}
+{\hbox{$\mathsf\scriptscriptstyle Z\kern-0.2em Z$}}}}
+
+\let\ts\,
+
+\setlength\leftmargini {17\p@}
+\setlength\leftmargin {\leftmargini}
+\setlength\leftmarginii {\leftmargini}
+\setlength\leftmarginiii {\leftmargini}
+\setlength\leftmarginiv {\leftmargini}
+\setlength \labelsep {.5em}
+\setlength \labelwidth{\leftmargini}
+\addtolength\labelwidth{-\labelsep}
+
+\def\@listI{\leftmargin\leftmargini
+ \parsep 0\p@ \@plus1\p@ \@minus\p@
+ \topsep 8\p@ \@plus2\p@ \@minus4\p@
+ \itemsep0\p@}
+\let\@listi\@listI
+\@listi
+\def\@listii {\leftmargin\leftmarginii
+ \labelwidth\leftmarginii
+ \advance\labelwidth-\labelsep
+ \topsep 0\p@ \@plus2\p@ \@minus\p@}
+\def\@listiii{\leftmargin\leftmarginiii
+ \labelwidth\leftmarginiii
+ \advance\labelwidth-\labelsep
+ \topsep 0\p@ \@plus\p@\@minus\p@
+ \parsep \z@
+ \partopsep \p@ \@plus\z@ \@minus\p@}
+
+\renewcommand\labelitemi{\normalfont\bfseries --}
+\renewcommand\labelitemii{$\m@th\bullet$}
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\def\tableofcontents{\chapter*{\contentsname\@mkboth{{\contentsname}}%
+ {{\contentsname}}}
+ \def\authcount##1{\setcounter{auco}{##1}\setcounter{@auth}{1}}
+ \def\lastand{\ifnum\value{auco}=2\relax
+ \unskip{} \andname\
+ \else
+ \unskip \lastandname\
+ \fi}%
+ \def\and{\stepcounter{@auth}\relax
+ \ifnum\value{@auth}=\value{auco}%
+ \lastand
+ \else
+ \unskip,
+ \fi}%
+ \@starttoc{toc}\if@restonecol\twocolumn\fi}
+
+\def\l@part#1#2{\addpenalty{\@secpenalty}%
+ \addvspace{2em plus\p@}% % space above part line
+ \begingroup
+ \parindent \z@
+ \rightskip \z@ plus 5em
+ \hrule\vskip5pt
+ \large % same size as for a contribution heading
+ \bfseries\boldmath % set line in boldface
+ \leavevmode % TeX command to enter horizontal mode.
+ #1\par
+ \vskip5pt
+ \hrule
+ \vskip1pt
+ \nobreak % Never break after part entry
+ \endgroup}
+
+\def\@dotsep{2}
+
+\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else
+{chapter.\thechapter}\fi}
+
+\def\addnumcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline
+ {\thechapter}#3}{\thepage}\hyperhrefextend}}
+\def\addcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}
+\def\addcontentsmarkwop#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}
+
+\def\@adcmk[#1]{\ifcase #1 \or
+\def\@gtempa{\addnumcontentsmark}%
+ \or \def\@gtempa{\addcontentsmark}%
+ \or \def\@gtempa{\addcontentsmarkwop}%
+ \fi\@gtempa{toc}{chapter}}
+\def\addtocmark{\@ifnextchar[{\@adcmk}{\@adcmk[3]}}
+
+\def\l@chapter#1#2{\addpenalty{-\@highpenalty}
+ \vskip 1.0em plus 1pt \@tempdima 1.5em \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ {\large\bfseries\boldmath#1}\ifx0#2\hfil\null
+ \else
+ \nobreak
+ \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+ \@dotsep mu$}\hfill
+ \nobreak\hbox to\@pnumwidth{\hss #2}%
+ \fi\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@title#1#2{\addpenalty{-\@highpenalty}
+ \addvspace{8pt plus 1pt}
+ \@tempdima \z@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ #1\nobreak
+ \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+ \@dotsep mu$}\hfill
+ \nobreak\hbox to\@pnumwidth{\hss #2}\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@author#1#2{\addpenalty{\@highpenalty}
+ \@tempdima=\z@ %15\p@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima %\hskip -\leftskip
+ \textit{#1}\par
+ \penalty\@highpenalty \endgroup}
+
+%\setcounter{tocdepth}{0}
+\newdimen\tocchpnum
+\newdimen\tocsecnum
+\newdimen\tocsectotal
+\newdimen\tocsubsecnum
+\newdimen\tocsubsectotal
+\newdimen\tocsubsubsecnum
+\newdimen\tocsubsubsectotal
+\newdimen\tocparanum
+\newdimen\tocparatotal
+\newdimen\tocsubparanum
+\tocchpnum=\z@ % no chapter numbers
+\tocsecnum=15\p@ % section 88. plus 2.222pt
+\tocsubsecnum=23\p@ % subsection 88.8 plus 2.222pt
+\tocsubsubsecnum=27\p@ % subsubsection 88.8.8 plus 1.444pt
+\tocparanum=35\p@ % paragraph 88.8.8.8 plus 1.666pt
+\tocsubparanum=43\p@ % subparagraph 88.8.8.8.8 plus 1.888pt
+\def\calctocindent{%
+\tocsectotal=\tocchpnum
+\advance\tocsectotal by\tocsecnum
+\tocsubsectotal=\tocsectotal
+\advance\tocsubsectotal by\tocsubsecnum
+\tocsubsubsectotal=\tocsubsectotal
+\advance\tocsubsubsectotal by\tocsubsubsecnum
+\tocparatotal=\tocsubsubsectotal
+\advance\tocparatotal by\tocparanum}
+\calctocindent
+
+\def\l@section{\@dottedtocline{1}{\tocchpnum}{\tocsecnum}}
+\def\l@subsection{\@dottedtocline{2}{\tocsectotal}{\tocsubsecnum}}
+\def\l@subsubsection{\@dottedtocline{3}{\tocsubsectotal}{\tocsubsubsecnum}}
+\def\l@paragraph{\@dottedtocline{4}{\tocsubsubsectotal}{\tocparanum}}
+\def\l@subparagraph{\@dottedtocline{5}{\tocparatotal}{\tocsubparanum}}
+
+\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listfigurename\@mkboth{{\listfigurename}}{{\listfigurename}}}
+ \@starttoc{lof}\if@restonecol\twocolumn\fi}
+\def\l@figure{\@dottedtocline{1}{0em}{1.5em}}
+
+\def\listoftables{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listtablename\@mkboth{{\listtablename}}{{\listtablename}}}
+ \@starttoc{lot}\if@restonecol\twocolumn\fi}
+\let\l@table\l@figure
+
+\renewcommand\listoffigures{%
+ \section*{\listfigurename
+ \@mkboth{\listfigurename}{\listfigurename}}%
+ \@starttoc{lof}%
+ }
+
+\renewcommand\listoftables{%
+ \section*{\listtablename
+ \@mkboth{\listtablename}{\listtablename}}%
+ \@starttoc{lot}%
+ }
+
+\ifx\oribibl\undefined
+\ifx\citeauthoryear\undefined
+\renewenvironment{thebibliography}[1]
+ {\section*{\refname}
+ \def\@biblabel##1{##1.}
+ \small
+ \list{\@biblabel{\@arabic\c@enumiv}}%
+ {\settowidth\labelwidth{\@biblabel{#1}}%
+ \leftmargin\labelwidth
+ \advance\leftmargin\labelsep
+ \if@openbib
+ \advance\leftmargin\bibindent
+ \itemindent -\bibindent
+ \listparindent \itemindent
+ \parsep \z@
+ \fi
+ \usecounter{enumiv}%
+ \let\p@enumiv\@empty
+ \renewcommand\theenumiv{\@arabic\c@enumiv}}%
+ \if@openbib
+ \renewcommand\newblock{\par}%
+ \else
+ \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+ \fi
+ \sloppy\clubpenalty4000\widowpenalty4000%
+ \sfcode`\.=\@m}
+ {\def\@noitemerr
+ {\@latex@warning{Empty `thebibliography' environment}}%
+ \endlist}
+\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw
+ {\let\protect\noexpand\immediate
+ \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+\newcount\@tempcntc
+\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi
+ \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do
+ {\@ifundefined
+ {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries
+ ?}\@warning
+ {Citation `\@citeb' on page \thepage \space undefined}}%
+ {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}%
+ \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne
+ \@citea\def\@citea{,}\hbox{\csname b@\@citeb\endcsname}%
+ \else
+ \advance\@tempcntb\@ne
+ \ifnum\@tempcntb=\@tempcntc
+ \else\advance\@tempcntb\m@ne\@citeo
+ \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}}
+\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else
+ \@citea\def\@citea{,\,\hskip\z@skip}%
+ \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else
+ {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else
+ \def\@citea{--}\fi
+ \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi}
+\else
+\renewenvironment{thebibliography}[1]
+ {\section*{\refname}
+ \small
+ \list{}%
+ {\settowidth\labelwidth{}%
+ \leftmargin\parindent
+ \itemindent=-\parindent
+ \labelsep=\z@
+ \if@openbib
+ \advance\leftmargin\bibindent
+ \itemindent -\bibindent
+ \listparindent \itemindent
+ \parsep \z@
+ \fi
+ \usecounter{enumiv}%
+ \let\p@enumiv\@empty
+ \renewcommand\theenumiv{}}%
+ \if@openbib
+ \renewcommand\newblock{\par}%
+ \else
+ \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+ \fi
+ \sloppy\clubpenalty4000\widowpenalty4000%
+ \sfcode`\.=\@m}
+ {\def\@noitemerr
+ {\@latex@warning{Empty `thebibliography' environment}}%
+ \endlist}
+ \def\@cite#1{#1}%
+ \def\@lbibitem[#1]#2{\item[]\if@filesw
+ {\def\protect##1{\string ##1\space}\immediate
+ \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+ \fi
+\else
+\@cons\@openbib@code{\noexpand\small}
+\fi
+
+\def\idxquad{\hskip 10\p@}% space that divides entry from number
+
+\def\@idxitem{\par\hangindent 10\p@}
+
+\def\subitem{\par\setbox0=\hbox{--\enspace}% second order
+ \noindent\hangindent\wd0\box0}% index entry
+
+\def\subsubitem{\par\setbox0=\hbox{--\,--\enspace}% third
+ \noindent\hangindent\wd0\box0}% order index entry
+
+\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax}
+
+\renewenvironment{theindex}
+ {\@mkboth{\indexname}{\indexname}%
+ \thispagestyle{empty}\parindent\z@
+ \parskip\z@ \@plus .3\p@\relax
+ \let\item\par
+ \def\,{\relax\ifmmode\mskip\thinmuskip
+ \else\hskip0.2em\ignorespaces\fi}%
+ \normalfont\small
+ \begin{multicols}{2}[\@makeschapterhead{\indexname}]%
+ }
+ {\end{multicols}}
+
+\renewcommand\footnoterule{%
+ \kern-3\p@
+ \hrule\@width 2truecm
+ \kern2.6\p@}
+ \newdimen\fnindent
+ \fnindent1em
+\long\def\@makefntext#1{%
+ \parindent \fnindent%
+ \leftskip \fnindent%
+ \noindent
+ \llap{\hb@xt@1em{\hss\@makefnmark\ }}\ignorespaces#1}
+
+\long\def\@makecaption#1#2{%
+ \vskip\abovecaptionskip
+ \sbox\@tempboxa{{\bfseries #1.} #2}%
+ \ifdim \wd\@tempboxa >\hsize
+ {\bfseries #1.} #2\par
+ \else
+ \global \@minipagefalse
+ \hb@xt@\hsize{\hfil\box\@tempboxa\hfil}%
+ \fi
+ \vskip\belowcaptionskip}
+
+\def\fps@figure{htbp}
+\def\fnum@figure{\figurename\thinspace\thefigure}
+\def \@floatboxreset {%
+ \reset@font
+ \small
+ \@setnobreak
+ \@setminipage
+}
+\def\fps@table{htbp}
+\def\fnum@table{\tablename~\thetable}
+\renewenvironment{table}
+ {\setlength\abovecaptionskip{0\p@}%
+ \setlength\belowcaptionskip{10\p@}%
+ \@float{table}}
+ {\end@float}
+\renewenvironment{table*}
+ {\setlength\abovecaptionskip{0\p@}%
+ \setlength\belowcaptionskip{10\p@}%
+ \@dblfloat{table}}
+ {\end@dblfloat}
+
+\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname
+ ext@#1\endcsname}{#1}{\protect\numberline{\csname
+ the#1\endcsname}{\ignorespaces #2}}\begingroup
+ \@parboxrestore
+ \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
+ \endgroup}
+
+% LaTeX does not provide a command to enter the authors institute
+% addresses. The \institute command is defined here.
+
+\newcounter{@inst}
+\newcounter{@auth}
+\newcounter{auco}
+\newdimen\instindent
+\newbox\authrun
+\newtoks\authorrunning
+\newtoks\tocauthor
+\newbox\titrun
+\newtoks\titlerunning
+\newtoks\toctitle
+
+\def\clearheadinfo{\gdef\@author{No Author Given}%
+ \gdef\@title{No Title Given}%
+ \gdef\@subtitle{}%
+ \gdef\@institute{No Institute Given}%
+ \gdef\@thanks{}%
+ \global\titlerunning={}\global\authorrunning={}%
+ \global\toctitle={}\global\tocauthor={}}
+
+\def\institute#1{\gdef\@institute{#1}}
+
+\def\institutename{\par
+ \begingroup
+ \parskip=\z@
+ \parindent=\z@
+ \setcounter{@inst}{1}%
+ \def\and{\par\stepcounter{@inst}%
+ \noindent$^{\the@inst}$\enspace\ignorespaces}%
+ \setbox0=\vbox{\def\thanks##1{}\@institute}%
+ \ifnum\c@@inst=1\relax
+ \gdef\fnnstart{0}%
+ \else
+ \xdef\fnnstart{\c@@inst}%
+ \setcounter{@inst}{1}%
+ \noindent$^{\the@inst}$\enspace
+ \fi
+ \ignorespaces
+ \@institute\par
+ \endgroup}
+
+\def\@fnsymbol#1{\ensuremath{\ifcase#1\or\star\or{\star\star}\or
+ {\star\star\star}\or \dagger\or \ddagger\or
+ \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger
+ \or \ddagger\ddagger \else\@ctrerr\fi}}
+
+\def\inst#1{\unskip$^{#1}$}
+\def\fnmsep{\unskip$^,$}
+\def\email#1{{\tt#1}}
+\AtBeginDocument{\@ifundefined{url}{\def\url#1{#1}}{}%
+\@ifpackageloaded{babel}{%
+\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}%
+\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}%
+\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}%
+}{\switcht@@therlang}%
+}
+\def\homedir{\~{ }}
+
+\def\subtitle#1{\gdef\@subtitle{#1}}
+\clearheadinfo
+
+\renewcommand\maketitle{\newpage
+ \refstepcounter{chapter}%
+ \stepcounter{section}%
+ \setcounter{section}{0}%
+ \setcounter{subsection}{0}%
+ \setcounter{figure}{0}
+ \setcounter{table}{0}
+ \setcounter{equation}{0}
+ \setcounter{footnote}{0}%
+ \begingroup
+ \parindent=\z@
+ \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
+ \if@twocolumn
+ \ifnum \col@number=\@ne
+ \@maketitle
+ \else
+ \twocolumn[\@maketitle]%
+ \fi
+ \else
+ \newpage
+ \global\@topnum\z@ % Prevents figures from going at top of page.
+ \@maketitle
+ \fi
+ \thispagestyle{empty}\@thanks
+%
+ \def\\{\unskip\ \ignorespaces}\def\inst##1{\unskip{}}%
+ \def\thanks##1{\unskip{}}\def\fnmsep{\unskip}%
+ \instindent=\hsize
+ \advance\instindent by-\headlineindent
+% \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else
+% \addcontentsline{toc}{title}{\the\toctitle}\fi
+ \if@runhead
+ \if!\the\titlerunning!\else
+ \edef\@title{\the\titlerunning}%
+ \fi
+ \global\setbox\titrun=\hbox{\small\rm\unboldmath\ignorespaces\@title}%
+ \ifdim\wd\titrun>\instindent
+ \typeout{Title too long for running head. Please supply}%
+ \typeout{a shorter form with \string\titlerunning\space prior to
+ \string\maketitle}%
+ \global\setbox\titrun=\hbox{\small\rm
+ Title Suppressed Due to Excessive Length}%
+ \fi
+ \xdef\@title{\copy\titrun}%
+ \fi
+%
+ \if!\the\tocauthor!\relax
+ {\def\and{\noexpand\protect\noexpand\and}%
+ \protected@xdef\toc@uthor{\@author}}%
+ \else
+ \def\\{\noexpand\protect\noexpand\newline}%
+ \protected@xdef\scratch{\the\tocauthor}%
+ \protected@xdef\toc@uthor{\scratch}%
+ \fi
+% \addcontentsline{toc}{author}{\toc@uthor}%
+ \if@runhead
+ \if!\the\authorrunning!
+ \value{@inst}=\value{@auth}%
+ \setcounter{@auth}{1}%
+ \else
+ \edef\@author{\the\authorrunning}%
+ \fi
+ \global\setbox\authrun=\hbox{\small\unboldmath\@author\unskip}%
+ \ifdim\wd\authrun>\instindent
+ \typeout{Names of authors too long for running head. Please supply}%
+ \typeout{a shorter form with \string\authorrunning\space prior to
+ \string\maketitle}%
+ \global\setbox\authrun=\hbox{\small\rm
+ Authors Suppressed Due to Excessive Length}%
+ \fi
+ \xdef\@author{\copy\authrun}%
+ \markboth{\@author}{\@title}%
+ \fi
+ \endgroup
+ \setcounter{footnote}{\fnnstart}%
+ \clearheadinfo}
+%
+\def\@maketitle{\newpage
+ \markboth{}{}%
+ \def\lastand{\ifnum\value{@inst}=2\relax
+ \unskip{} \andname\
+ \else
+ \unskip \lastandname\
+ \fi}%
+ \def\and{\stepcounter{@auth}\relax
+ \ifnum\value{@auth}=\value{@inst}%
+ \lastand
+ \else
+ \unskip,
+ \fi}%
+ \begin{center}%
+ \let\newline\\
+ {\Large \bfseries\boldmath
+ \pretolerance=10000
+ \@title \par}\vskip .8cm
+\if!\@subtitle!\else {\large \bfseries\boldmath
+ \vskip -.65cm
+ \pretolerance=10000
+ \@subtitle \par}\vskip .8cm\fi
+ \setbox0=\vbox{\setcounter{@auth}{1}\def\and{\stepcounter{@auth}}%
+ \def\thanks##1{}\@author}%
+ \global\value{@inst}=\value{@auth}%
+ \global\value{auco}=\value{@auth}%
+ \setcounter{@auth}{1}%
+{\lineskip .5em
+\noindent\ignorespaces
+\@author\vskip.35cm}
+ {\small\institutename}
+ \end{center}%
+ }
+
+% definition of the "\spnewtheorem" command.
+%
+% Usage:
+%
+% \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font}
+% or \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font}
+% or \spnewtheorem*{env_nam}{caption}{cap_font}{body_font}
+%
+% New is "cap_font" and "body_font". It stands for
+% fontdefinition of the caption and the text itself.
+%
+% "\spnewtheorem*" gives a theorem without number.
+%
+% A defined spnewthoerem environment is used as described
+% by Lamport.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\@thmcountersep{}
+\def\@thmcounterend{.}
+
+\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}}
+
+% definition of \spnewtheorem with number
+
+\def\@spnthm#1#2{%
+ \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}}
+\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}}
+
+\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname
+ {\@definecounter{#1}\@addtoreset{#1}{#3}%
+ \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand
+ \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}%
+ \expandafter\xdef\csname #1name\endcsname{#2}%
+ \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
+ \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+ {\@definecounter{#1}%
+ \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
+ \expandafter\xdef\csname #1name\endcsname{#2}%
+ \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}%
+ \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spothm#1[#2]#3#4#5{%
+ \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}%
+ {\expandafter\@ifdefinable\csname #1\endcsname
+ {\global\@namedef{the#1}{\@nameuse{the#2}}%
+ \expandafter\xdef\csname #1name\endcsname{#3}%
+ \global\@namedef{#1}{\@spthm{#2}{\csname #1name\endcsname}{#4}{#5}}%
+ \global\@namedef{end#1}{\@endtheorem}}}}
+
+\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\refstepcounter{#1}%
+\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}}
+
+\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}%
+ \ignorespaces}
+
+\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname
+ the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
+
+\def\@spbegintheorem#1#2#3#4{\trivlist
+ \item[\hskip\labelsep{#3#1\ #2\@thmcounterend}]#4}
+
+\def\@spopargbegintheorem#1#2#3#4#5{\trivlist
+ \item[\hskip\labelsep{#4#1\ #2}]{#4(#3)\@thmcounterend\ }#5}
+
+% definition of \spnewtheorem* without number
+
+\def\@sthm#1#2{\@Ynthm{#1}{#2}}
+
+\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+ {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}%
+ \expandafter\xdef\csname #1name\endcsname{#2}%
+ \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}}
+
+\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces}
+
+\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1}
+ {#4}{#2}{#3}\ignorespaces}
+
+\def\@Begintheorem#1#2#3{#3\trivlist
+ \item[\hskip\labelsep{#2#1\@thmcounterend}]}
+
+\def\@Opargbegintheorem#1#2#3#4{#4\trivlist
+ \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }}
+
+\if@envcntsect
+ \def\@thmcountersep{.}
+ \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape}
+\else
+ \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape}
+ \if@envcntreset
+ \@addtoreset{theorem}{section}
+ \else
+ \@addtoreset{theorem}{chapter}
+ \fi
+\fi
+
+%definition of divers theorem environments
+\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily}
+\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily}
+\if@envcntsame % alle Umgebungen wie Theorem.
+ \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}}
+\else % alle Umgebungen mit eigenem Zaehler
+ \if@envcntsect % mit section numeriert
+ \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}}
+ \else % nicht mit section numeriert
+ \if@envcntreset
+ \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+ \@addtoreset{#1}{section}}
+ \else
+ \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+ \@addtoreset{#1}{chapter}}%
+ \fi
+ \fi
+\fi
+\spn@wtheorem{case}{Case}{\itshape}{\rmfamily}
+\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily}
+\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape}
+\spn@wtheorem{definition}{Definition}{\bfseries}{\itshape}
+\spn@wtheorem{example}{Example}{\itshape}{\rmfamily}
+\spn@wtheorem{exercise}{Exercise}{\itshape}{\rmfamily}
+\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape}
+\spn@wtheorem{note}{Note}{\itshape}{\rmfamily}
+\spn@wtheorem{problem}{Problem}{\itshape}{\rmfamily}
+\spn@wtheorem{property}{Property}{\itshape}{\rmfamily}
+\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape}
+\spn@wtheorem{question}{Question}{\itshape}{\rmfamily}
+\spn@wtheorem{solution}{Solution}{\itshape}{\rmfamily}
+\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily}
+
+\def\@takefromreset#1#2{%
+ \def\@tempa{#1}%
+ \let\@tempd\@elt
+ \def\@elt##1{%
+ \def\@tempb{##1}%
+ \ifx\@tempa\@tempb\else
+ \@addtoreset{##1}{#2}%
+ \fi}%
+ \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname
+ \expandafter\def\csname cl@#2\endcsname{}%
+ \@tempc
+ \let\@elt\@tempd}
+
+\def\theopargself{\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
+ \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5}
+ \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
+ \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }}
+ }
+
+\renewenvironment{abstract}{%
+ \list{}{\advance\topsep by0.35cm\relax\small
+ \leftmargin=1cm
+ \labelwidth=\z@
+ \listparindent=\z@
+ \itemindent\listparindent
+ \rightmargin\leftmargin}\item[\hskip\labelsep
+ \bfseries\abstractname]}
+ {\endlist}
+
+\newdimen\headlineindent % dimension for space between
+\headlineindent=1.166cm % number and text of headings.
+
+\def\ps@headings{\let\@mkboth\@gobbletwo
+ \let\@oddfoot\@empty\let\@evenfoot\@empty
+ \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+ \leftmark\hfil}
+ \def\@oddhead{\normalfont\small\hfil\rightmark\hspace{\headlineindent}%
+ \llap{\thepage}}
+ \def\chaptermark##1{}%
+ \def\sectionmark##1{}%
+ \def\subsectionmark##1{}}
+
+\def\ps@titlepage{\let\@mkboth\@gobbletwo
+ \let\@oddfoot\@empty\let\@evenfoot\@empty
+ \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+ \hfil}
+ \def\@oddhead{\normalfont\small\hfil\hspace{\headlineindent}%
+ \llap{\thepage}}
+ \def\chaptermark##1{}%
+ \def\sectionmark##1{}%
+ \def\subsectionmark##1{}}
+
+\if@runhead\ps@headings\else
+\ps@empty\fi
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\endinput
+%end of file llncs.cls
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/document/root.bib Wed May 18 19:54:43 2011 +0000
@@ -0,0 +1,111 @@
+@article{OwensReppyTuron09,
+ author = {S.~Owens and J.~Reppy and A.~Turon},
+ title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined},
+ journal = {Journal of Functional Programming},
+ volume = 19,
+ number = {2},
+ year = 2009,
+ pages = {173--190}
+}
+
+
+
+@Unpublished{KraussNipkow11,
+ author = {A.~Kraus and T.~Nipkow},
+ title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},
+ note = {To appear in Journal of Automated Reasoning},
+ year = {2011}
+}
+
+@Book{Kozen97,
+ author = {D.~Kozen},
+ title = {{A}utomata and {C}omputability},
+ publisher = {Springer Verlag},
+ year = {1997}
+}
+
+
+@incollection{Constable00,
+ author = {R.~L.~Constable and
+ P.~B.~Jackson and
+ P.~Naumov and
+ J.~C.~Uribe},
+ title = {{C}onstructively {F}ormalizing {A}utomata {T}heory},
+ booktitle = {Proof, Language, and Interaction},
+ year = {2000},
+ publisher = {MIT Press},
+ pages = {213-238}
+}
+
+
+@techreport{Filliatre97,
+ author = {J.-C. Filli\^atre},
+ institution = {LIP - ENS Lyon},
+ number = {97--04},
+ title = {{F}inite {A}utomata {T}heory in {C}oq:
+ {A} {C}onstructive {P}roof of {K}leene's {T}heorem},
+ type = {Research Report},
+ year = {1997}
+}
+
+@article{OwensSlind08,
+ author = {S.~Owens and K.~Slind},
+ title = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic},
+ journal = {Higher-Order and Symbolic Computation},
+ volume = {21},
+ number = {4},
+ year = {2008},
+ pages = {377--409}
+}
+
+@article{Brzozowski64,
+ author = {J.~A.~Brzozowski},
+ title = {{D}erivatives of {R}egular {E}xpressions},
+ journal = {J.~ACM},
+ volume = {11},
+ issue = {4},
+ year = {1964},
+ pages = {481--494},
+ publisher = {ACM}
+}
+
+@inproceedings{Nipkow98,
+ author={T.~Nipkow},
+ title={{V}erified {L}exical {A}nalysis},
+ booktitle={Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics},
+ series={LNCS},
+ volume=1479,
+ pages={1--15},
+ year=1998
+}
+
+@inproceedings{BerghoferNipkow00,
+ author={S.~Berghofer and T.~Nipkow},
+ title={{E}xecuting {H}igher {O}rder {L}ogic},
+ booktitle={Proc.~of the International Workshop on Types for Proofs and Programs},
+ year=2002,
+ series={LNCS},
+ volume=2277,
+ pages="24--40"
+}
+
+@book{HopcroftUllman69,
+ author = {J.~E.~Hopcroft and
+ J.~D.~Ullman},
+ title = {{F}ormal {L}anguages and {T}heir {R}elation to {A}utomata},
+ publisher = {Addison-Wesley},
+ year = {1969}
+}
+
+
+@inproceedings{BerghoferReiter09,
+ author = {S.~Berghofer and
+ M.~Reiter},
+ title = {{F}ormalizing the {L}ogic-{A}utomaton {C}onnection},
+ booktitle = {Proc.~of the 22nd International
+ Conference on Theorem Proving in Higher Order Logics},
+ year = {2009},
+ pages = {147-163},
+ series = {LNCS},
+ volume = {5674}
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/document/root.tex Wed May 18 19:54:43 2011 +0000
@@ -0,0 +1,73 @@
+\documentclass[runningheads]{llncs}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{tikz}
+\usepackage{pgf}
+\usetikzlibrary{arrows,automata,decorations,fit,calc}
+\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
+\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
+\usetikzlibrary{matrix}
+\usepackage{pdfsetup}
+\usepackage{ot1patch}
+\usepackage{times}
+%%\usepackage{proof}
+%%\usepackage{mathabx}
+\usepackage{stmaryrd}
+
+\titlerunning{Myhill-Nerode using Regular Expressions}
+
+
+\urlstyle{rm}
+\isabellestyle{it}
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastyle}{\normalsize\it}%
+
+
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+
+\newcommand{\isasymcalL}{\ensuremath{\cal{L}}}
+\newcommand{\isasymbigplus}{\ensuremath{\bigplus}}
+
+\newcommand{\bigplus}{\mbox{\Large\bf$+$}}
+\begin{document}
+
+\title{A Formalisation of the Myhill-Nerode Theorem\\ based on Regular
+ Expressions (Proof Pearl)}
+\author{Chunhan Wu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}
+\institute{PLA University of Science and Technology, China \and TU Munich, Germany}
+\maketitle
+
+%\mbox{}\\[-10mm]
+\begin{abstract}
+There are numerous textbooks on regular languages. Nearly all of them
+introduce the subject by describing finite automata and only mentioning on the
+side a connection with regular expressions. Unfortunately, automata are difficult
+to formalise in HOL-based theorem provers. The reason is that
+they need to be represented as graphs, matrices or functions, none of which
+are inductive datatypes. Also convenient operations for disjoint unions of
+graphs and functions are not easily formalisiable in HOL. In contrast, regular
+expressions can be defined conveniently as a datatype and a corresponding
+reasoning infrastructure comes for free. We show in this paper that a central
+result from formal language theory---the Myhill-Nerode theorem---can be
+recreated using only regular expressions.
+
+\end{abstract}
+
+
+\input{session}
+
+%%\mbox{}\\[-10mm]
+\bibliographystyle{plain}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
--- a/Myhill_1.thy Thu May 12 05:55:05 2011 +0000
+++ b/Myhill_1.thy Wed May 18 19:54:43 2011 +0000
@@ -1,315 +1,10 @@
theory Myhill_1
-imports Main Folds
- "~~/src/HOL/Library/While_Combinator"
+imports Main Folds Regular
+ "~~/src/HOL/Library/While_Combinator"
begin
-section {* Preliminary definitions *}
-
-types 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)
-
-
-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 of a set or regulare 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
-
-
section {* Direction @{text "finite partition \<Rightarrow> regular language"} *}
-
-text {* Just a technical lemma for collections and pairs *}
-
lemma Pair_Collect[simp]:
shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
by simp
@@ -321,26 +16,17 @@
where
"\<approx>A \<equiv> {(x, y). (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)}"
-text {*
- Among the equivalence clases of @{text "\<approx>A"}, the set @{text "finals A"}
- singles out those which contains the strings from @{text A}.
-*}
-
definition
finals :: "lang \<Rightarrow> lang set"
where
"finals A \<equiv> {\<approx>A `` {s} | s . s \<in> A}"
-
lemma lang_is_union_of_finals:
shows "A = \<Union> finals A"
unfolding finals_def
unfolding Image_def
unfolding str_eq_rel_def
-apply(auto)
-apply(drule_tac x = "[]" in spec)
-apply(auto)
-done
+by (auto) (metis append_Nil2)
lemma finals_in_partitions:
shows "finals A \<subseteq> (UNIV // \<approx>A)"
@@ -351,28 +37,32 @@
text {* The two kinds of terms in the rhs of equations. *}
-datatype rhs_item =
+datatype rhs_trm =
Lam "rexp" (* Lambda-marker *)
| Trn "lang" "rexp" (* Transition *)
-overloading L_rhs_item \<equiv> "L:: rhs_item \<Rightarrow> lang"
+overloading L_rhs_trm \<equiv> "L:: rhs_trm \<Rightarrow> lang"
begin
- fun L_rhs_item:: "rhs_item \<Rightarrow> lang"
+ fun L_rhs_trm:: "rhs_trm \<Rightarrow> lang"
where
- "L_rhs_item (Lam r) = L r"
- | "L_rhs_item (Trn X r) = X ;; L r"
+ "L_rhs_trm (Lam r) = L r"
+ | "L_rhs_trm (Trn X r) = X ;; L r"
end
-overloading L_rhs \<equiv> "L:: rhs_item set \<Rightarrow> lang"
+overloading L_rhs \<equiv> "L:: rhs_trm set \<Rightarrow> lang"
begin
- fun L_rhs:: "rhs_item set \<Rightarrow> lang"
+ fun L_rhs:: "rhs_trm set \<Rightarrow> lang"
where
"L_rhs rhs = \<Union> (L ` rhs)"
end
+lemma L_rhs_set:
+ shows "L {Trn X r | r. P r} = \<Union>{L (Trn X r) | r. P r}"
+by (auto simp del: L_rhs_trm.simps)
+
lemma L_rhs_union_distrib:
- fixes A B::"rhs_item set"
+ fixes A B::"rhs_trm set"
shows "L A \<union> L B = L (A \<union> B)"
by simp
@@ -398,60 +88,34 @@
"Init CS \<equiv> {(X, Init_rhs CS X) | X. X \<in> CS}"
-
section {* Arden Operation on equations *}
-text {*
- The function @{text "attach_rexp r item"} SEQ-composes @{text r} to the
- right of every rhs-item.
-*}
-
fun
- append_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"
+ Append_rexp :: "rexp \<Rightarrow> rhs_trm \<Rightarrow> rhs_trm"
where
- "append_rexp r (Lam rexp) = Lam (SEQ rexp r)"
-| "append_rexp r (Trn X rexp) = Trn X (SEQ rexp r)"
+ "Append_rexp r (Lam rexp) = Lam (SEQ rexp r)"
+| "Append_rexp r (Trn X rexp) = Trn X (SEQ rexp r)"
definition
- "append_rhs_rexp rhs rexp \<equiv> (append_rexp rexp) ` rhs"
+ "Append_rexp_rhs rhs rexp \<equiv> (Append_rexp rexp) ` rhs"
definition
"Arden X rhs \<equiv>
- append_rhs_rexp (rhs - {Trn X r | r. Trn X r \<in> rhs}) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))"
+ 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 *}
-text {*
- Suppose and equation @{text "X = xrhs"}, @{text "Subst"} substitutes
- all occurences of @{text "X"} in @{text "rhs"} by @{text "xrhs"}.
-*}
-
definition
"Subst rhs X xrhs \<equiv>
- (rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> (append_rhs_rexp xrhs (\<Uplus> {r. Trn X r \<in> rhs}))"
-
-text {*
- @{text "eqs_subst ES X xrhs"} substitutes @{text xrhs} into every
- equation of the equational system @{text ES}.
-*}
-
-types esystem = "(lang \<times> rhs_item set) set"
+ (rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> (Append_rexp_rhs xrhs (\<Uplus> {r. Trn X r \<in> rhs}))"
definition
- Subst_all :: "esystem \<Rightarrow> lang \<Rightarrow> rhs_item set \<Rightarrow> esystem"
+ Subst_all :: "(lang \<times> rhs_trm set) set \<Rightarrow> lang \<Rightarrow> rhs_trm set \<Rightarrow> (lang \<times> rhs_trm set) set"
where
"Subst_all ES X xrhs \<equiv> {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
-text {*
- The following term @{text "remove ES Y yrhs"} removes the equation
- @{text "Y = yrhs"} from equational system @{text "ES"} by replacing
- all occurences of @{text "Y"} by its definition (using @{text "eqs_subst"}).
- The @{text "Y"}-definition is made non-recursive using Arden's transformation
- @{text "arden_variate Y yrhs"}.
- *}
-
definition
"Remove ES X xrhs \<equiv>
Subst_all (ES - {(X, xrhs)}) X (Arden X xrhs)"
@@ -459,11 +123,6 @@
section {* While-combinator *}
-text {*
- The following term @{text "Iter X ES"} represents one iteration in the while loop.
- It arbitrarily chooses a @{text "Y"} different from @{text "X"} to remove.
-*}
-
definition
"Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y
in Remove ES Y yrhs)"
@@ -476,64 +135,28 @@
unfolding Iter_def using assms
by (rule_tac a="(Y, yrhs)" in someI2) (auto)
-
-text {*
- The following term @{text "Reduce X ES"} repeatedly removes characteriztion equations
- for unknowns other than @{text "X"} until one is left.
-*}
-
abbreviation
"Cond ES \<equiv> card ES \<noteq> 1"
definition
"Solve X ES \<equiv> while Cond (Iter X) ES"
-text {*
- Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"},
- the induction principle @{thm [source] while_rule} is used to proved the desired properties
- of @{text "Solve X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
- in terms of a series of auxilliary predicates:
-*}
section {* Invariants *}
-text {* Every variable is defined at most once in @{text ES}. *}
-
definition
- "distinct_equas ES \<equiv>
+ "distinctness ES \<equiv>
\<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
-
-text {*
- Every equation in @{text ES} (represented by @{text "(X, rhs)"})
- is valid, i.e. @{text "X = L rhs"}.
-*}
-
definition
- "sound_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
-
-text {*
- @{text "ardenable rhs"} requires regular expressions occuring in
- transitional items of @{text "rhs"} do not contain empty string. This is
- necessary for the application of Arden's transformation to @{text "rhs"}.
-*}
+ "soundness ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
definition
"ardenable rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"
-text {*
- The following @{text "ardenable_all ES"} requires that Arden's transformation
- is applicable to every equation of equational system @{text "ES"}.
-*}
-
definition
"ardenable_all ES \<equiv> \<forall>(X, rhs) \<in> ES. ardenable rhs"
-
-text {*
- @{text "finite_rhs ES"} requires every equation in @{text "rhs"}
- be finite.
-*}
definition
"finite_rhs ES \<equiv> \<forall>(X, rhs) \<in> ES. finite rhs"
@@ -541,56 +164,42 @@
"finite_rhs ES = (\<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs)"
unfolding finite_rhs_def by auto
-text {*
- @{text "classes_of rhs"} returns all variables (or equivalent classes)
- occuring in @{text "rhs"}.
- *}
-
definition
"rhss rhs \<equiv> {X | X r. Trn X r \<in> rhs}"
-text {*
- @{text "lefts_of ES"} returns all variables defined by an
- equational system @{text "ES"}.
-*}
definition
"lhss ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"
-text {*
- The following @{text "valid_eqs ES"} requires that every variable occuring
- on the right hand side of equations is already defined by some equation in @{text "ES"}.
-*}
definition
- "valid_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. rhss rhs \<subseteq> lhss ES"
+ "validity ES \<equiv> \<forall>(X, rhs) \<in> ES. rhss rhs \<subseteq> lhss ES"
+
+lemma rhss_union_distrib:
+ shows "rhss (A \<union> B) = rhss A \<union> rhss B"
+by (auto simp add: rhss_def)
+
+lemma lhss_union_distrib:
+ shows "lhss (A \<union> B) = lhss A \<union> lhss B"
+by (auto simp add: lhss_def)
-text {*
- The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints.
- *}
definition
"invariant ES \<equiv> finite ES
\<and> finite_rhs ES
- \<and> sound_eqs ES
- \<and> distinct_equas ES
+ \<and> soundness ES
+ \<and> distinctness ES
\<and> ardenable_all ES
- \<and> valid_eqs ES"
+ \<and> validity ES"
lemma invariantI:
- assumes "sound_eqs ES" "finite ES" "distinct_equas ES" "ardenable_all ES"
- "finite_rhs ES" "valid_eqs ES"
+ assumes "soundness ES" "finite ES" "distinctness ES" "ardenable_all ES"
+ "finite_rhs ES" "validity ES"
shows "invariant ES"
using assms by (simp add: invariant_def)
+
subsection {* The proof of this direction *}
-subsubsection {* Basic properties *}
-
-text {*
- The following are some basic properties of the above definitions.
-*}
-
-
lemma finite_Trn:
assumes fin: "finite rhs"
shows "finite {r. Trn Y r \<in> rhs}"
@@ -618,55 +227,30 @@
done
qed
-lemma rexp_of_empty:
- assumes finite: "finite rhs"
- and nonempty: "ardenable rhs"
- shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
-using finite nonempty ardenable_def
-using finite_Trn[OF finite]
-by auto
-
-lemma lang_of_rexp_of:
+lemma rhs_trm_soundness:
assumes finite:"finite rhs"
shows "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
proof -
have "finite {r. Trn X r \<in> rhs}"
by (rule finite_Trn[OF finite])
- then show ?thesis
- apply(auto simp add: Seq_def)
- apply(rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI)
- apply(auto)
- apply(rule_tac x= "Trn X xa" in exI)
- apply(auto simp add: Seq_def)
- done
+ then show "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
+ by (simp only: L_rhs_set L_rhs_trm.simps) (auto simp add: Seq_def)
qed
-lemma lang_of_append:
- "L (append_rexp r rhs_item) = L rhs_item ;; L r"
-by (induct rule: append_rexp.induct)
+lemma lang_of_append_rexp:
+ "L (Append_rexp r rhs_trm) = L rhs_trm ;; L r"
+by (induct rule: Append_rexp.induct)
(auto simp add: seq_assoc)
-lemma lang_of_append_rhs:
- "L (append_rhs_rexp rhs r) = L rhs ;; L r"
-unfolding append_rhs_rexp_def
-by (auto simp add: Seq_def lang_of_append)
+lemma lang_of_append_rexp_rhs:
+ "L (Append_rexp_rhs rhs r) = L rhs ;; L r"
+unfolding Append_rexp_rhs_def
+by (auto simp add: Seq_def lang_of_append_rexp)
-lemma rhss_union_distrib:
- shows "rhss (A \<union> B) = rhss A \<union> rhss B"
-by (auto simp add: rhss_def)
-
-lemma lhss_union_distrib:
- shows "lhss (A \<union> B) = lhss A \<union> lhss B"
-by (auto simp add: lhss_def)
subsubsection {* Intialization *}
-text {*
- The following several lemmas until @{text "init_ES_satisfy_invariant"} shows that
- the initial equational system satisfies invariant @{text "invariant"}.
-*}
-
lemma defined_by_str:
assumes "s \<in> X" "X \<in> UNIV // \<approx>A"
shows "X = \<approx>A `` {s}"
@@ -702,42 +286,37 @@
show "X \<subseteq> L rhs"
proof
fix x
- assume "(1)": "x \<in> X"
- show "x \<in> L rhs"
- proof (cases "x = []")
- assume empty: "x = []"
- thus ?thesis using X_in_eqs "(1)"
- by (auto simp: Init_def Init_rhs_def)
- next
- assume not_empty: "x \<noteq> []"
- then obtain clist c where decom: "x = clist @ [c]"
- by (case_tac x rule:rev_cases, auto)
- have "X \<in> UNIV // \<approx>A" using X_in_eqs by (auto simp:Init_def)
- then obtain Y
- where "Y \<in> UNIV // \<approx>A"
- and "Y ;; {[c]} \<subseteq> X"
- and "clist \<in> Y"
- using decom "(1)" every_eqclass_has_transition by blast
- hence
- "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // \<approx>A \<and> Y \<Turnstile>c\<Rightarrow> X}"
+ assume in_X: "x \<in> X"
+ { assume empty: "x = []"
+ then have "x \<in> L rhs" using X_in_eqs in_X
+ unfolding Init_def Init_rhs_def
+ by auto
+ }
+ moreover
+ { assume not_empty: "x \<noteq> []"
+ then obtain s c where decom: "x = s @ [c]"
+ using rev_cases by blast
+ have "X \<in> UNIV // \<approx>A" using X_in_eqs unfolding Init_def by auto
+ then obtain Y where "Y \<in> UNIV // \<approx>A" "Y ;; {[c]} \<subseteq> X" "s \<in> Y"
+ using decom in_X every_eqclass_has_transition by blast
+ then have "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // \<approx>A \<and> Y \<Turnstile>c\<Rightarrow> X}"
unfolding transition_def
- using "(1)" decom
- by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)
- thus ?thesis using X_in_eqs "(1)"
- by (simp add: Init_def Init_rhs_def)
- qed
+ using decom by (force simp add: Seq_def)
+ then have "x \<in> L rhs" using X_in_eqs in_X
+ unfolding Init_def Init_rhs_def by simp
+ }
+ ultimately show "x \<in> L rhs" by blast
qed
next
show "L rhs \<subseteq> X" using X_in_eqs
- by (auto simp:Init_def Init_rhs_def transition_def)
+ unfolding Init_def Init_rhs_def transition_def
+ by auto
qed
lemma test:
assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)"
shows "X = \<Union> (L ` rhs)"
-using assms
-by (drule_tac l_eq_r_in_eqs) (simp)
-
+using assms l_eq_r_in_eqs by (simp)
lemma finite_Init_rhs:
assumes finite: "finite CS"
@@ -759,31 +338,26 @@
assumes finite_CS: "finite (UNIV // \<approx>A)"
shows "invariant (Init (UNIV // \<approx>A))"
proof (rule invariantI)
- show "sound_eqs (Init (UNIV // \<approx>A))"
- unfolding sound_eqs_def
+ show "soundness (Init (UNIV // \<approx>A))"
+ unfolding soundness_def
using l_eq_r_in_eqs by auto
show "finite (Init (UNIV // \<approx>A))" using finite_CS
unfolding Init_def by simp
- show "distinct_equas (Init (UNIV // \<approx>A))"
- unfolding distinct_equas_def Init_def by simp
+ show "distinctness (Init (UNIV // \<approx>A))"
+ unfolding distinctness_def Init_def by simp
show "ardenable_all (Init (UNIV // \<approx>A))"
unfolding ardenable_all_def Init_def Init_rhs_def ardenable_def
by auto
show "finite_rhs (Init (UNIV // \<approx>A))"
using finite_Init_rhs[OF finite_CS]
unfolding finite_rhs_def Init_def by auto
- show "valid_eqs (Init (UNIV // \<approx>A))"
- unfolding valid_eqs_def Init_def Init_rhs_def rhss_def lhss_def
+ show "validity (Init (UNIV // \<approx>A))"
+ unfolding validity_def Init_def Init_rhs_def rhss_def lhss_def
by auto
qed
subsubsection {* Interation step *}
-text {*
- From this point until @{text "iteration_step"},
- the correctness of the iteration step @{text "Iter X ES"} is proved.
-*}
-
lemma Arden_keeps_eq:
assumes l_eq_r: "X = L rhs"
and not_empty: "ardenable rhs"
@@ -791,40 +365,39 @@
shows "X = L (Arden X rhs)"
proof -
def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})"
- def b \<equiv> "rhs - {Trn X r | r. Trn X r \<in> rhs}"
- def B \<equiv> "L b"
- have "X = B ;; A\<star>"
- proof -
- have "L rhs = L({Trn X r | r. Trn X r \<in> rhs} \<union> b)" by (auto simp: b_def)
- also have "\<dots> = X ;; A \<union> B"
- unfolding L_rhs_union_distrib[symmetric]
- by (simp only: lang_of_rexp_of finite B_def A_def)
- finally show ?thesis
- apply(rule_tac arden[THEN iffD1])
- apply(simp (no_asm) add: A_def)
- using finite_Trn[OF finite] not_empty
- apply(simp add: ardenable_def)
- using l_eq_r
- apply(simp)
- done
- qed
- moreover have "L (Arden X rhs) = B ;; A\<star>"
- by (simp only:Arden_def L_rhs_union_distrib lang_of_append_rhs
- B_def A_def b_def L_rexp.simps seq_union_distrib_left)
- ultimately show ?thesis by simp
+ def b \<equiv> "{Trn X r | r. Trn X r \<in> rhs}"
+ def B \<equiv> "L (rhs - b)"
+ have not_empty2: "[] \<notin> A"
+ using finite_Trn[OF finite] not_empty
+ unfolding A_def ardenable_def by simp
+ have "X = L rhs" using l_eq_r by simp
+ also have "\<dots> = L (b \<union> (rhs - b))" unfolding b_def by auto
+ also have "\<dots> = L b \<union> B" unfolding B_def by (simp only: L_rhs_union_distrib)
+ also have "\<dots> = X ;; A \<union> B"
+ unfolding b_def
+ unfolding rhs_trm_soundness[OF finite]
+ unfolding A_def
+ by blast
+ finally have "X = X ;; A \<union> B" .
+ then have "X = B ;; A\<star>"
+ by (simp add: arden[OF not_empty2])
+ also have "\<dots> = L (Arden X rhs)"
+ unfolding Arden_def A_def B_def b_def
+ by (simp only: lang_of_append_rexp_rhs L_rexp.simps)
+ finally show "X = L (Arden X rhs)" by simp
qed
-lemma append_keeps_finite:
- "finite rhs \<Longrightarrow> finite (append_rhs_rexp rhs r)"
-by (auto simp:append_rhs_rexp_def)
+lemma Append_keeps_finite:
+ "finite rhs \<Longrightarrow> finite (Append_rexp_rhs rhs r)"
+by (auto simp:Append_rexp_rhs_def)
lemma Arden_keeps_finite:
"finite rhs \<Longrightarrow> finite (Arden X rhs)"
-by (auto simp:Arden_def append_keeps_finite)
+by (auto simp:Arden_def Append_keeps_finite)
-lemma append_keeps_nonempty:
- "ardenable rhs \<Longrightarrow> ardenable (append_rhs_rexp rhs r)"
-apply (auto simp:ardenable_def append_rhs_rexp_def)
+lemma Append_keeps_nonempty:
+ "ardenable rhs \<Longrightarrow> ardenable (Append_rexp_rhs rhs r)"
+apply (auto simp:ardenable_def Append_rexp_rhs_def)
by (case_tac x, auto simp:Seq_def)
lemma nonempty_set_sub:
@@ -837,12 +410,12 @@
lemma Arden_keeps_nonempty:
"ardenable rhs \<Longrightarrow> ardenable (Arden X rhs)"
-by (simp only:Arden_def append_keeps_nonempty nonempty_set_sub)
+by (simp only:Arden_def Append_keeps_nonempty nonempty_set_sub)
lemma Subst_keeps_nonempty:
"\<lbrakk>ardenable rhs; ardenable xrhs\<rbrakk> \<Longrightarrow> ardenable (Subst rhs X xrhs)"
-by (simp only:Subst_def append_keeps_nonempty nonempty_set_union nonempty_set_sub)
+by (simp only: Subst_def Append_keeps_nonempty nonempty_set_union nonempty_set_sub)
lemma Subst_keeps_eq:
assumes substor: "X = L xrhs"
@@ -850,7 +423,7 @@
shows "L (Subst rhs X xrhs) = L rhs" (is "?Left = ?Right")
proof-
def A \<equiv> "L (rhs - {Trn X r | r. Trn X r \<in> rhs})"
- have "?Left = A \<union> L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs}))"
+ have "?Left = A \<union> L (Append_rexp_rhs xrhs (\<Uplus>{r. Trn X r \<in> rhs}))"
unfolding Subst_def
unfolding L_rhs_union_distrib[symmetric]
by (simp add: A_def)
@@ -862,14 +435,14 @@
unfolding L_rhs_union_distrib
by simp
qed
- moreover have "L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs})) = L ({Trn X r | r. Trn X r \<in> rhs})"
- using finite substor by (simp only:lang_of_append_rhs lang_of_rexp_of)
+ moreover have "L (Append_rexp_rhs xrhs (\<Uplus>{r. Trn X r \<in> rhs})) = L ({Trn X r | r. Trn X r \<in> rhs})"
+ using finite substor by (simp only: lang_of_append_rexp_rhs rhs_trm_soundness)
ultimately show ?thesis by simp
qed
lemma Subst_keeps_finite_rhs:
"\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (Subst rhs Y yrhs)"
-by (auto simp:Subst_def append_keeps_finite)
+by (auto simp: Subst_def Append_keeps_finite)
lemma Subst_all_keeps_finite:
assumes finite: "finite ES"
@@ -889,8 +462,8 @@
by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def)
lemma append_rhs_keeps_cls:
- "rhss (append_rhs_rexp rhs r) = rhss rhs"
-apply (auto simp:rhss_def append_rhs_rexp_def)
+ "rhss (Append_rexp_rhs rhs r) = rhss rhs"
+apply (auto simp:rhss_def Append_rexp_rhs_def)
apply (case_tac xa, auto simp:image_def)
by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+)
@@ -909,9 +482,9 @@
apply (simp only:Subst_def append_rhs_keeps_cls rhss_union_distrib)
by (auto simp:rhss_def)
-lemma Subst_all_keeps_valid_eqs:
- assumes sc: "valid_eqs (ES \<union> {(Y, yrhs)})" (is "valid_eqs ?A")
- shows "valid_eqs (Subst_all ES Y (Arden Y yrhs))" (is "valid_eqs ?B")
+lemma Subst_all_keeps_validity:
+ assumes sc: "validity (ES \<union> {(Y, yrhs)})" (is "validity ?A")
+ shows "validity (Subst_all ES Y (Arden Y yrhs))" (is "validity ?B")
proof -
{ fix X xrhs'
assume "(X, xrhs') \<in> ?B"
@@ -930,16 +503,16 @@
thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls)
qed
moreover have "rhss xrhs \<subseteq> lhss ES \<union> {Y}" using X_in sc
- apply (simp only:valid_eqs_def lhss_union_distrib)
+ apply (simp only:validity_def lhss_union_distrib)
by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lhss_def)
moreover have "rhss (Arden Y yrhs) \<subseteq> lhss ES \<union> {Y}"
using sc
- by (auto simp add:Arden_removes_cl valid_eqs_def lhss_def)
+ by (auto simp add:Arden_removes_cl validity_def lhss_def)
ultimately show ?thesis by auto
qed
ultimately show ?thesis by simp
qed
- } thus ?thesis by (auto simp only:Subst_all_def valid_eqs_def)
+ } thus ?thesis by (auto simp only:Subst_all_def validity_def)
qed
lemma Subst_all_satisfies_invariant:
@@ -947,12 +520,12 @@
shows "invariant (Subst_all ES Y (Arden Y yrhs))"
proof (rule invariantI)
have Y_eq_yrhs: "Y = L yrhs"
- using invariant_ES by (simp only:invariant_def sound_eqs_def, blast)
+ using invariant_ES by (simp only:invariant_def soundness_def, blast)
have finite_yrhs: "finite yrhs"
using invariant_ES by (auto simp:invariant_def finite_rhs_def)
have nonempty_yrhs: "ardenable yrhs"
using invariant_ES by (auto simp:invariant_def ardenable_all_def)
- show "sound_eqs (Subst_all ES Y (Arden Y yrhs))"
+ show "soundness (Subst_all ES Y (Arden Y yrhs))"
proof -
have "Y = L (Arden Y yrhs)"
using Y_eq_yrhs invariant_ES finite_yrhs
@@ -963,19 +536,19 @@
apply(auto)
done
thus ?thesis using invariant_ES
- unfolding invariant_def finite_rhs_def2 sound_eqs_def Subst_all_def
+ unfolding invariant_def finite_rhs_def2 soundness_def Subst_all_def
by (auto simp add: Subst_keeps_eq simp del: L_rhs.simps)
qed
show "finite (Subst_all ES Y (Arden Y yrhs))"
using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
- show "distinct_equas (Subst_all ES Y (Arden Y yrhs))"
+ show "distinctness (Subst_all ES Y (Arden Y yrhs))"
using invariant_ES
- unfolding distinct_equas_def Subst_all_def invariant_def by auto
+ unfolding distinctness_def Subst_all_def invariant_def by auto
show "ardenable_all (Subst_all ES Y (Arden Y yrhs))"
proof -
{ fix X rhs
assume "(X, rhs) \<in> ES"
- hence "ardenable rhs" using prems invariant_ES
+ hence "ardenable rhs" using invariant_ES
by (auto simp add:invariant_def ardenable_all_def)
with nonempty_yrhs
have "ardenable (Subst rhs Y (Arden Y yrhs))"
@@ -996,8 +569,8 @@
ultimately show ?thesis
by (simp add:Subst_all_keeps_finite_rhs)
qed
- show "valid_eqs (Subst_all ES Y (Arden Y yrhs))"
- using invariant_ES Subst_all_keeps_valid_eqs by (simp add:invariant_def)
+ show "validity (Subst_all ES Y (Arden Y yrhs))"
+ using invariant_ES Subst_all_keeps_validity by (simp add:invariant_def)
qed
lemma Remove_in_card_measure:
@@ -1049,7 +622,7 @@
where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)"
using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"
- using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
+ using X_in_ES Inv_ES unfolding invariant_def distinctness_def
by auto
then show "(Iter X ES, ES) \<in> measure card"
apply(rule IterI2)
@@ -1069,7 +642,7 @@
where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)"
using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
then have "(Y, yrhs) \<in> ES" "X \<noteq> Y"
- using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
+ using X_in_ES Inv_ES unfolding invariant_def distinctness_def
by auto
then show "invariant (Iter X ES)"
proof(rule IterI2)
@@ -1078,7 +651,6 @@
then have "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto
then show "invariant (Remove ES Y yrhs)" unfolding Remove_def
using Inv_ES
- thm Subst_all_satisfies_invariant
by (rule_tac Subst_all_satisfies_invariant) (simp)
qed
qed
@@ -1091,10 +663,10 @@
proof -
have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
then obtain Y yrhs
- where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)"
+ where "(Y, yrhs) \<in> ES" "(X, xrhs) \<noteq> (Y, yrhs)"
using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"
- using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
+ using X_in_ES Inv_ES unfolding invariant_def distinctness_def
by auto
then show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)"
apply(rule IterI2)
@@ -1159,7 +731,7 @@
def A \<equiv> "Arden X xrhs"
have "rhss xrhs \<subseteq> {X}" using Inv_ES
- unfolding valid_eqs_def invariant_def rhss_def lhss_def
+ unfolding validity_def invariant_def rhss_def lhss_def
by auto
then have "rhss A = {}" unfolding A_def
by (simp add: Arden_removes_cl)
@@ -1170,7 +742,7 @@
using Arden_keeps_finite by auto
then have fin: "finite {r. Lam r \<in> A}" by (rule finite_Lam)
- have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def
+ have "X = L xrhs" using Inv_ES unfolding invariant_def soundness_def
by simp
then have "X = L A" using Inv_ES
unfolding A_def invariant_def ardenable_all_def finite_rhs_def
--- a/Myhill_2.thy Thu May 12 05:55:05 2011 +0000
+++ b/Myhill_2.thy Wed May 18 19:54:43 2011 +0000
@@ -1,64 +1,15 @@
theory Myhill_2
- imports Myhill_1
- Prefix_subtract
+ imports Myhill_1 Prefix_subtract
"~~/src/HOL/Library/List_Prefix"
begin
section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
-subsection {* The scheme*}
-
-text {*
- The following convenient notation @{text "x \<approx>A y"} means:
- string @{text "x"} and @{text "y"} are equivalent with respect to
- language @{text "A"}.
- *}
-
definition
str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _")
where
"x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)"
-text {*
- The main lemma (@{text "rexp_imp_finite"}) is proved by a structural
- induction over regular expressions. where base cases (cases for @{const
- "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straightforward to
- proof. Real difficulty lies in inductive cases. By inductive hypothesis,
- languages defined by sub-expressions induce finite partitiions. Under such
- hypothsis, we need to prove that the language defined by the composite
- regular expression gives rise to finite partion. The basic idea is to
- attach a tag @{text "tag(x)"} to every string @{text "x"}. The tagging
- fuction @{text "tag"} is carefully devised, which returns tags made of
- equivalent classes of the partitions induced by subexpressoins, and
- therefore has a finite range. Let @{text "Lang"} be the composite language,
- it is proved that:
- \begin{quote}
- If strings with the same tag are equivalent with respect to @{text "Lang"}, expressed as:
- \[
- @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"}
- \]
- then the partition induced by @{text "Lang"} must be finite.
- \end{quote}
- There are two arguments for this. The first goes as the following:
- \begin{enumerate}
- \item First, the tagging function @{text "tag"} induces an equivalent relation @{text "(=tag=)"}
- (defiintion of @{text "f_eq_rel"} and lemma @{text "equiv_f_eq_rel"}).
- \item It is shown that: if the range of @{text "tag"} (denoted @{text "range(tag)"}) is finite,
- the partition given rise by @{text "(=tag=)"} is finite (lemma @{text "finite_eq_f_rel"}).
- Since tags are made from equivalent classes from component partitions, and the inductive
- hypothesis ensures the finiteness of these partitions, it is not difficult to prove
- the finiteness of @{text "range(tag)"}.
- \item It is proved that if equivalent relation @{text "R1"} is more refined than @{text "R2"}
- (expressed as @{text "R1 \<subseteq> R2"}),
- and the partition induced by @{text "R1"} is finite, then the partition induced by @{text "R2"}
- is finite as well (lemma @{text "refined_partition_finite"}).
- \item The injectivity assumption @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} implies that
- @{text "(=tag=)"} is more refined than @{text "(\<approx>Lang)"}.
- \item Combining the points above, we have: the partition induced by language @{text "Lang"}
- is finite (lemma @{text "tag_finite_imageD"}).
- \end{enumerate}
-*}
-
definition
tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=")
where
@@ -69,7 +20,6 @@
shows "finite (UNIV // =tag=)"
proof -
let "?f" = "\<lambda>X. tag ` X" and ?A = "(UNIV // =tag=)"
- -- {* The finiteness of @{text "f"}-image is a consequence of @{text "rng_fnt"} *}
have "finite (?f ` ?A)"
proof -
have "range ?f \<subseteq> (Pow (range tag))" unfolding Pow_def by auto
@@ -82,25 +32,23 @@
ultimately show "finite (?f ` ?A)" by (rule rev_finite_subset)
qed
moreover
- -- {* The injectivity of @{text "f"}-image follows from the definition of @{text "(=tag=)"} *}
have "inj_on ?f ?A"
proof -
{ fix X Y
assume X_in: "X \<in> ?A"
and Y_in: "Y \<in> ?A"
and tag_eq: "?f X = ?f Y"
- then
- obtain x y
+ then obtain x y
where "x \<in> X" "y \<in> Y" "tag x = tag y"
unfolding quotient_def Image_def image_def tag_eq_rel_def
by (simp) (blast)
with X_in Y_in
have "X = Y"
unfolding quotient_def tag_eq_rel_def by auto
- } then show "inj_on ?f ?A" unfolding inj_on_def by auto
+ }
+ then show "inj_on ?f ?A" unfolding inj_on_def by auto
qed
- ultimately
- show "finite (UNIV // =tag=)" by (rule finite_imageD)
+ ultimately show "finite (UNIV // =tag=)" by (rule finite_imageD)
qed
lemma refined_partition_finite:
@@ -142,7 +90,7 @@
lemma tag_finite_imageD:
assumes rng_fnt: "finite (range tag)"
- and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>A n"
+ and same_tag_eqvt: "\<And>m n. tag m = tag n \<Longrightarrow> m \<approx>A n"
shows "finite (UNIV // \<approx>A)"
proof (rule_tac refined_partition_finite [of "=tag="])
show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt])
@@ -161,48 +109,23 @@
qed
-subsection {* The proof*}
-
-text {*
- Each case is given in a separate section, as well as the final main lemma. Detailed explainations accompanied by
- illustrations are given for non-trivial cases.
-
- For ever inductive case, there are two tasks, the easier one is to show the range finiteness of
- of the tagging function based on the finiteness of component partitions, the
- difficult one is to show that strings with the same tag are equivalent with respect to the
- composite language. Suppose the composite language be @{text "Lang"}, tagging function be
- @{text "tag"}, it amounts to show:
- \[
- @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"}
- \]
- expanding the definition of @{text "\<approx>Lang"}, it amounts to show:
- \[
- @{text "tag(x) = tag(y) \<Longrightarrow> (\<forall> z. x@z \<in> Lang \<longleftrightarrow> y@z \<in> Lang)"}
- \]
- Because the assumed tag equlity @{text "tag(x) = tag(y)"} is symmetric,
- it is suffcient to show just one direction:
- \[
- @{text "\<And> x y z. \<lbrakk>tag(x) = tag(y); x@z \<in> Lang\<rbrakk> \<Longrightarrow> y@z \<in> Lang"}
- \]
- This is the pattern followed by every inductive case.
- *}
+subsection {* The proof *}
subsubsection {* The base case for @{const "NULL"} *}
lemma quot_null_eq:
- shows "(UNIV // \<approx>{}) = ({UNIV}::lang set)"
- unfolding quotient_def Image_def str_eq_rel_def by auto
+ shows "UNIV // \<approx>{} = {UNIV}"
+unfolding quotient_def Image_def str_eq_rel_def by auto
lemma quot_null_finiteI [intro]:
- shows "finite ((UNIV // \<approx>{})::lang set)"
+ shows "finite (UNIV // \<approx>{})"
unfolding quot_null_eq by simp
subsubsection {* The base case for @{const "EMPTY"} *}
-
lemma quot_empty_subset:
- "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}"
+ shows "UNIV // \<approx>{[]} \<subseteq> {{[]}, UNIV - {[]}}"
proof
fix x
assume "x \<in> UNIV // \<approx>{[]}"
@@ -221,7 +144,7 @@
qed
lemma quot_empty_finiteI [intro]:
- shows "finite (UNIV // (\<approx>{[]}))"
+ shows "finite (UNIV // \<approx>{[]})"
by (rule finite_subset[OF quot_empty_subset]) (simp)
@@ -237,23 +160,24 @@
show "x \<in> {{[]},{[c]}, UNIV - {[], [c]}}"
proof -
{ assume "y = []" hence "x = {[]}" using h
- by (auto simp:str_eq_rel_def)
- } moreover {
- assume "y = [c]" hence "x = {[c]}" using h
- by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_def)
- } moreover {
- assume "y \<noteq> []" and "y \<noteq> [c]"
+ by (auto simp:str_eq_rel_def) }
+ moreover
+ { assume "y = [c]" hence "x = {[c]}" using h
+ by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_def) }
+ moreover
+ { assume "y \<noteq> []" and "y \<noteq> [c]"
hence "\<forall> z. (y @ z) \<noteq> [c]" by (case_tac y, auto)
moreover have "\<And> p. (p \<noteq> [] \<and> p \<noteq> [c]) = (\<forall> q. p @ q \<noteq> [c])"
by (case_tac p, auto)
ultimately have "x = UNIV - {[],[c]}" using h
by (auto simp add:str_eq_rel_def)
- } ultimately show ?thesis by blast
+ }
+ ultimately show ?thesis by blast
qed
qed
lemma quot_char_finiteI [intro]:
- shows "finite (UNIV // (\<approx>{[c]}))"
+ shows "finite (UNIV // \<approx>{[c]})"
by (rule finite_subset[OF quot_char_subset]) (simp)
@@ -265,7 +189,6 @@
"tag_str_ALT A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"
lemma quot_union_finiteI [intro]:
- fixes L1 L2::"lang"
assumes finite1: "finite (UNIV // \<approx>A)"
and finite2: "finite (UNIV // \<approx>B)"
shows "finite (UNIV // \<approx>(A \<union> B))"
@@ -283,140 +206,79 @@
by auto
qed
+
subsubsection {* The inductive case for @{text "SEQ"}*}
-text {*
- For case @{const "SEQ"}, the language @{text "L"} is @{text "L\<^isub>1 ;; L\<^isub>2"}.
- Given @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"}, according to the defintion of @{text " L\<^isub>1 ;; L\<^isub>2"},
- string @{text "x @ z"} can be splitted with the prefix in @{text "L\<^isub>1"} and suffix in @{text "L\<^isub>2"}.
- The split point can either be in @{text "x"} (as shown in Fig. \ref{seq_first_split}),
- or in @{text "z"} (as shown in Fig. \ref{seq_snd_split}). Whichever way it goes, the structure
- on @{text "x @ z"} cn be transfered faithfully onto @{text "y @ z"}
- (as shown in Fig. \ref{seq_trans_first_split} and \ref{seq_trans_snd_split}) with the the help of the assumed
- tag equality. The following tag function @{text "tag_str_SEQ"} is such designed to facilitate
- such transfers and lemma @{text "tag_str_SEQ_injI"} formalizes the informal argument above. The details
- of structure transfer will be given their.
-\input{fig_seq}
-
- *}
-
definition
tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
where
"tag_str_SEQ L1 L2 \<equiv>
- (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - x'}) | x'. x' \<le> x \<and> x' \<in> L1}))"
-
-text {* The following is a techical lemma which helps to split the @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"} mentioned above.*}
+ (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))"
-lemma append_seq_elim:
- assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2"
- shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or>
- (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)"
-proof-
- from assms obtain s\<^isub>1 s\<^isub>2
- where eq_xys: "x @ y = s\<^isub>1 @ s\<^isub>2"
- and in_seq: "s\<^isub>1 \<in> L\<^isub>1 \<and> s\<^isub>2 \<in> L\<^isub>2"
- by (auto simp:Seq_def)
- from app_eq_dest [OF eq_xys]
- have
- "(x \<le> s\<^isub>1 \<and> (s\<^isub>1 - x) @ s\<^isub>2 = y) \<or> (s\<^isub>1 \<le> x \<and> (x - s\<^isub>1) @ y = s\<^isub>2)"
- (is "?Split1 \<or> ?Split2") .
- moreover have "?Split1 \<Longrightarrow> \<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2"
- using in_seq by (rule_tac x = "s\<^isub>1 - x" in exI, auto elim:prefixE)
- moreover have "?Split2 \<Longrightarrow> \<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2"
- using in_seq by (rule_tac x = s\<^isub>1 in exI, auto)
- ultimately show ?thesis by blast
-qed
-
+lemma Seq_in_cases:
+ assumes "x @ z \<in> A ;; B"
+ shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or>
+ (\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)"
+using assms
+unfolding Seq_def prefix_def
+by (auto simp add: append_eq_append_conv2)
lemma tag_str_SEQ_injI:
- fixes v w
- assumes eq_tag: "tag_str_SEQ L\<^isub>1 L\<^isub>2 v = tag_str_SEQ L\<^isub>1 L\<^isub>2 w"
- shows "v \<approx>(L\<^isub>1 ;; L\<^isub>2) w"
-proof-
- -- {* As explained before, a pattern for just one direction needs to be dealt with:*}
+ assumes eq_tag: "tag_str_SEQ A B x = tag_str_SEQ A B y"
+ shows "x \<approx>(A ;; B) y"
+proof -
{ fix x y z
- assume xz_in_seq: "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"
- and tag_xy: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y"
- have"y @ z \<in> L\<^isub>1 ;; L\<^isub>2"
- proof-
- -- {* There are two ways to split @{text "x@z"}: *}
- from append_seq_elim [OF xz_in_seq]
- have "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ z \<in> L\<^isub>2) \<or>
- (\<exists> za \<le> z. (x @ za) \<in> L\<^isub>1 \<and> (z - za) \<in> L\<^isub>2)" .
- -- {* It can be shown that @{text "?thesis"} holds in either case: *}
- moreover {
- -- {* The case for the first split:*}
- fix xa
- assume h1: "xa \<le> x" and h2: "xa \<in> L\<^isub>1" and h3: "(x - xa) @ z \<in> L\<^isub>2"
- -- {* The following subgoal implements the structure transfer:*}
- obtain ya
- where "ya \<le> y"
- and "ya \<in> L\<^isub>1"
- and "(y - ya) @ z \<in> L\<^isub>2"
+ assume xz_in_seq: "x @ z \<in> A ;; B"
+ and tag_xy: "tag_str_SEQ A B x = tag_str_SEQ A B y"
+ have"y @ z \<in> A ;; B"
+ proof -
+ { (* first case with x' in A and (x - x') @ z in B *)
+ fix x'
+ assume h1: "x' \<le> x" and h2: "x' \<in> A" and h3: "(x - x') @ z \<in> B"
+ obtain y'
+ where "y' \<le> y"
+ and "y' \<in> A"
+ and "(y - y') @ z \<in> B"
proof -
- -- {*
- \begin{minipage}{0.8\textwidth}
- By expanding the definition of
- @{thm [display] "tag_xy"}
- and extracting the second compoent, we get:
- \end{minipage}
- *}
- have "{\<approx>L\<^isub>2 `` {x - xa} |xa. xa \<le> x \<and> xa \<in> L\<^isub>1} =
- {\<approx>L\<^isub>2 `` {y - ya} |ya. ya \<le> y \<and> ya \<in> L\<^isub>1}" (is "?Left = ?Right")
+ have "{\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A} =
+ {\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A}" (is "?Left = ?Right")
using tag_xy unfolding tag_str_SEQ_def by simp
- -- {* Since @{thm "h1"} and @{thm "h2"} hold, it is not difficult to show: *}
- moreover have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Left" using h1 h2 by auto
- -- {*
- \begin{minipage}{0.7\textwidth}
- Through tag equality, equivalent class @{term "\<approx>L\<^isub>2 `` {x - xa}"} also
- belongs to the @{text "?Right"}:
- \end{minipage}
- *}
- ultimately have "\<approx>L\<^isub>2 `` {x - xa} \<in> ?Right" by simp
- -- {* From this, the counterpart of @{text "xa"} in @{text "y"} is obtained:*}
- then obtain ya
- where eq_xya: "\<approx>L\<^isub>2 `` {x - xa} = \<approx>L\<^isub>2 `` {y - ya}"
- and pref_ya: "ya \<le> y" and ya_in: "ya \<in> L\<^isub>1"
+ moreover
+ have "\<approx>B `` {x - x'} \<in> ?Left" using h1 h2 by auto
+ ultimately
+ have "\<approx>B `` {x - x'} \<in> ?Right" by simp
+ then obtain y'
+ where eq_xy': "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"
+ and pref_y': "y' \<le> y" and y'_in: "y' \<in> A"
by simp blast
- -- {* It can be proved that @{text "ya"} has the desired property:*}
- have "(y - ya)@z \<in> L\<^isub>2"
- proof -
- from eq_xya have "(x - xa) \<approx>L\<^isub>2 (y - ya)"
- unfolding Image_def str_eq_rel_def str_eq_def by auto
- with h3 show ?thesis unfolding str_eq_rel_def str_eq_def by simp
- qed
- -- {* Now, @{text "ya"} has all properties to be a qualified candidate:*}
- with pref_ya ya_in
+
+ have "(x - x') \<approx>B (y - y')" using eq_xy'
+ unfolding Image_def str_eq_rel_def str_eq_def by auto
+ with h3 have "(y - y') @ z \<in> B"
+ unfolding str_eq_rel_def str_eq_def by simp
+ with pref_y' y'_in
show ?thesis using that by blast
qed
- -- {* From the properties of @{text "ya"}, @{text "y @ z \<in> L\<^isub>1 ;; L\<^isub>2"} is derived easily.*}
- hence "y @ z \<in> L\<^isub>1 ;; L\<^isub>2" by (erule_tac prefixE, auto simp:Seq_def)
- } moreover {
- -- {* The other case is even more simpler: *}
- fix za
- assume h1: "za \<le> z" and h2: "(x @ za) \<in> L\<^isub>1" and h3: "z - za \<in> L\<^isub>2"
- have "y @ za \<in> L\<^isub>1"
- proof-
- have "\<approx>L\<^isub>1 `` {x} = \<approx>L\<^isub>1 `` {y}"
- using tag_xy unfolding tag_str_SEQ_def by simp
- with h2 show ?thesis
+ then have "y @ z \<in> A ;; B" by (erule_tac prefixE) (auto simp: Seq_def)
+ }
+ moreover
+ { (* second case with x @ z' in A and z - z' in B *)
+ fix z'
+ assume h1: "z' \<le> z" and h2: "(x @ z') \<in> A" and h3: "z - z' \<in> B"
+ have "\<approx>A `` {x} = \<approx>A `` {y}"
+ using tag_xy unfolding tag_str_SEQ_def by simp
+ with h2 have "y @ z' \<in> A"
unfolding Image_def str_eq_rel_def str_eq_def by auto
- qed
- with h1 h3 have "y @ z \<in> L\<^isub>1 ;; L\<^isub>2"
- by (drule_tac A = L\<^isub>1 in seq_intro, auto elim:prefixE)
+ with h1 h3 have "y @ z \<in> A ;; B"
+ unfolding prefix_def Seq_def
+ by (auto) (metis append_assoc)
}
- ultimately show ?thesis by blast
+ ultimately show "y @ z \<in> A ;; B"
+ using Seq_in_cases [OF xz_in_seq] by blast
qed
- }
- -- {*
- \begin{minipage}{0.8\textwidth}
- @{text "?thesis"} is proved by exploiting the symmetry of
- @{thm [source] "eq_tag"}:
- \end{minipage}
- *}
+ }
from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
- show ?thesis unfolding str_eq_def str_eq_rel_def by blast
+ show "x \<approx>(A ;; B) y" unfolding str_eq_def str_eq_rel_def by blast
qed
lemma quot_seq_finiteI [intro]:
@@ -437,53 +299,13 @@
by auto
qed
+
subsubsection {* The inductive case for @{const "STAR"} *}
-text {*
- This turned out to be the trickiest case. The essential goal is
- to proved @{text "y @ z \<in> L\<^isub>1*"} under the assumptions that @{text "x @ z \<in> L\<^isub>1*"}
- and that @{text "x"} and @{text "y"} have the same tag. The reasoning goes as the following:
- \begin{enumerate}
- \item Since @{text "x @ z \<in> L\<^isub>1*"} holds, a prefix @{text "xa"} of @{text "x"} can be found
- such that @{text "xa \<in> L\<^isub>1*"} and @{text "(x - xa)@z \<in> L\<^isub>1*"}, as shown in Fig. \ref{first_split}.
- Such a prefix always exists, @{text "xa = []"}, for example, is one.
- \item There could be many but fintie many of such @{text "xa"}, from which we can find the longest
- and name it @{text "xa_max"}, as shown in Fig. \ref{max_split}.
- \item The next step is to split @{text "z"} into @{text "za"} and @{text "zb"} such that
- @{text "(x - xa_max) @ za \<in> L\<^isub>1"} and @{text "zb \<in> L\<^isub>1*"} as shown in Fig. \ref{last_split}.
- Such a split always exists because:
- \begin{enumerate}
- \item Because @{text "(x - x_max) @ z \<in> L\<^isub>1*"}, it can always be splitted into prefix @{text "a"}
- and suffix @{text "b"}, such that @{text "a \<in> L\<^isub>1"} and @{text "b \<in> L\<^isub>1*"},
- as shown in Fig. \ref{ab_split}.
- \item But the prefix @{text "a"} CANNOT be shorter than @{text "x - xa_max"}
- (as shown in Fig. \ref{ab_split_wrong}), becasue otherwise,
- @{text "ma_max@a"} would be in the same kind as @{text "xa_max"} but with
- a larger size, conflicting with the fact that @{text "xa_max"} is the longest.
- \end{enumerate}
- \item \label{tansfer_step}
- By the assumption that @{text "x"} and @{text "y"} have the same tag, the structure on @{text "x @ z"}
- can be transferred to @{text "y @ z"} as shown in Fig. \ref{trans_split}. The detailed steps are:
- \begin{enumerate}
- \item A @{text "y"}-prefix @{text "ya"} corresponding to @{text "xa"} can be found,
- which satisfies conditions: @{text "ya \<in> L\<^isub>1*"} and @{text "(y - ya)@za \<in> L\<^isub>1"}.
- \item Since we already know @{text "zb \<in> L\<^isub>1*"}, we get @{text "(y - ya)@za@zb \<in> L\<^isub>1*"},
- and this is just @{text "(y - ya)@z \<in> L\<^isub>1*"}.
- \item With fact @{text "ya \<in> L\<^isub>1*"}, we finally get @{text "y@z \<in> L\<^isub>1*"}.
- \end{enumerate}
- \end{enumerate}
-
- The formal proof of lemma @{text "tag_str_STAR_injI"} faithfully follows this informal argument
- while the tagging function @{text "tag_str_STAR"} is defined to make the transfer in step
- \ref{ansfer_step} feasible.
-
- \input{fig_star}
-*}
-
definition
tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set"
where
- "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - x'} | x'. x' < x \<and> x' \<in> L1\<star>})"
+ "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
text {* A technical lemma. *}
lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow>
@@ -513,7 +335,8 @@
qed
-text {* The following is a technical lemma.which helps to show the range finiteness of tag function. *}
+text {* The following is a technical lemma, which helps to show the range finiteness of tag function. *}
+
lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}"
apply (induct x rule:rev_induct, simp)
apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}")
@@ -521,46 +344,26 @@
lemma tag_str_STAR_injI:
- fixes v w
assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"
- shows "(v::string) \<approx>(L\<^isub>1\<star>) w"
+ shows "v \<approx>(L\<^isub>1\<star>) w"
proof-
- -- {* As explained before, a pattern for just one direction needs to be dealt with:*}
{ fix x y z
assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>"
and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y"
have "y @ z \<in> L\<^isub>1\<star>"
proof(cases "x = []")
- -- {*
- The degenerated case when @{text "x"} is a null string is easy to prove:
- *}
case True
with tag_xy have "y = []"
by (auto simp add: tag_str_STAR_def strict_prefix_def)
thus ?thesis using xz_in_star True by simp
next
- -- {* The nontrival case:
- *}
case False
- -- {*
- \begin{minipage}{0.8\textwidth}
- Since @{text "x @ z \<in> L\<^isub>1\<star>"}, @{text "x"} can always be splitted
- by a prefix @{text "xa"} together with its suffix @{text "x - xa"}, such
- that both @{text "xa"} and @{text "(x - xa) @ z"} are in @{text "L\<^isub>1\<star>"},
- and there could be many such splittings.Therefore, the following set @{text "?S"}
- is nonempty, and finite as well:
- \end{minipage}
- *}
let ?S = "{xa. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}"
have "finite ?S"
by (rule_tac B = "{xa. xa < x}" in finite_subset,
auto simp:finite_strict_prefix_set)
moreover have "?S \<noteq> {}" using False xz_in_star
by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def)
- -- {* \begin{minipage}{0.7\textwidth}
- Since @{text "?S"} is finite, we can always single out the longest and name it @{text "xa_max"}:
- \end{minipage}
- *}
ultimately have "\<exists> xa_max \<in> ?S. \<forall> xa \<in> ?S. length xa \<le> length xa_max"
using finite_set_has_max by blast
then obtain xa_max
@@ -570,12 +373,6 @@
and h4:"\<forall> xa < x. xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>
\<longrightarrow> length xa \<le> length xa_max"
by blast
- -- {*
- \begin{minipage}{0.8\textwidth}
- By the equality of tags, the counterpart of @{text "xa_max"} among
- @{text "y"}-prefixes, named @{text "ya"}, can be found:
- \end{minipage}
- *}
obtain ya
where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>"
and eq_xya: "(x - xa_max) \<approx>L\<^isub>1 (y - ya)"
@@ -588,47 +385,25 @@
thus ?thesis using that
apply (simp add:Image_def str_eq_rel_def str_eq_def) by blast
qed
- -- {*
- \begin{minipage}{0.8\textwidth}
- The @{text "?thesis"}, @{prop "y @ z \<in> L\<^isub>1\<star>"}, is a simple consequence
- of the following proposition:
- \end{minipage}
- *}
have "(y - ya) @ z \<in> L\<^isub>1\<star>"
proof-
- -- {* The idea is to split the suffix @{text "z"} into @{text "za"} and @{text "zb"},
- such that: *}
obtain za zb where eq_zab: "z = za @ zb"
and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>"
proof -
- -- {*
- \begin{minipage}{0.8\textwidth}
- Since @{thm "h1"}, @{text "x"} can be splitted into
- @{text "a"} and @{text "b"} such that:
- \end{minipage}
- *}
from h1 have "(x - xa_max) @ z \<noteq> []"
by (auto simp:strict_prefix_def elim:prefixE)
from star_decom [OF h3 this]
obtain a b where a_in: "a \<in> L\<^isub>1"
and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>"
and ab_max: "(x - xa_max) @ z = a @ b" by blast
- -- {* Now the candiates for @{text "za"} and @{text "zb"} are found:*}
let ?za = "a - (x - xa_max)" and ?zb = "b"
have pfx: "(x - xa_max) \<le> a" (is "?P1")
and eq_z: "z = ?za @ ?zb" (is "?P2")
proof -
- -- {*
- \begin{minipage}{0.8\textwidth}
- Since @{text "(x - xa_max) @ z = a @ b"}, string @{text "(x - xa_max) @ z"}
- can be splitted in two ways:
- \end{minipage}
- *}
have "((x - xa_max) \<le> a \<and> (a - (x - xa_max)) @ b = z) \<or>
(a < (x - xa_max) \<and> ((x - xa_max) - a) @ z = b)"
- using app_eq_dest[OF ab_max] by (auto simp:strict_prefix_def)
+ using append_eq_dest[OF ab_max] by (auto simp:strict_prefix_def)
moreover {
- -- {* However, the undsired way can be refuted by absurdity: *}
assume np: "a < (x - xa_max)"
and b_eqs: "((x - xa_max) - a) @ z = b"
have "False"
@@ -639,24 +414,19 @@
moreover have "?xa_max' \<in> L\<^isub>1\<star>"
using a_in h2 by (simp add:star_intro3)
moreover have "(x - ?xa_max') @ z \<in> L\<^isub>1\<star>"
- using b_eqs b_in np h1 by (simp add:diff_diff_appd)
+ using b_eqs b_in np h1 by (simp add:diff_diff_append)
moreover have "\<not> (length ?xa_max' \<le> length xa_max)"
using a_neq by simp
ultimately show ?thesis using h4 by blast
qed }
- -- {* Now it can be shown that the splitting goes the way we desired. *}
ultimately show ?P1 and ?P2 by auto
qed
hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in by (auto elim:prefixE)
- -- {* Now candidates @{text "?za"} and @{text "?zb"} have all the requred properteis. *}
with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1"
by (auto simp:str_eq_def str_eq_rel_def)
with eq_z and b_in
show ?thesis using that by blast
qed
- -- {*
- @{text "?thesis"} can easily be shown using properties of @{text "za"} and @{text "zb"}:
- *}
have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using l_za ls_zb by blast
with eq_zab show ?thesis by simp
qed
@@ -664,123 +434,11 @@
by (drule_tac star_intro1) (auto simp:strict_prefix_def elim:prefixE)
qed
}
- -- {* By instantiating the reasoning pattern just derived for both directions:*}
from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
- -- {* The thesis is proved as a trival consequence: *}
- show ?thesis unfolding str_eq_def str_eq_rel_def by blast
-qed
-
-lemma -- {* The oringal version with less explicit details. *}
- fixes v w
- assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"
- shows "(v::string) \<approx>(L\<^isub>1\<star>) w"
-proof-
- -- {*
- \begin{minipage}{0.8\textwidth}
- According to the definition of @{text "\<approx>Lang"},
- proving @{text "v \<approx>(L\<^isub>1\<star>) w"} amounts to
- showing: for any string @{text "u"},
- if @{text "v @ u \<in> (L\<^isub>1\<star>)"} then @{text "w @ u \<in> (L\<^isub>1\<star>)"} and vice versa.
- The reasoning pattern for both directions are the same, as derived
- in the following:
- \end{minipage}
- *}
- { fix x y z
- assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>"
- and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y"
- have "y @ z \<in> L\<^isub>1\<star>"
- proof(cases "x = []")
- -- {*
- The degenerated case when @{text "x"} is a null string is easy to prove:
- *}
- case True
- with tag_xy have "y = []"
- by (auto simp:tag_str_STAR_def strict_prefix_def)
- thus ?thesis using xz_in_star True by simp
- next
- -- {*
- \begin{minipage}{0.8\textwidth}
- The case when @{text "x"} is not null, and
- @{text "x @ z"} is in @{text "L\<^isub>1\<star>"},
- \end{minipage}
- *}
- case False
- obtain x_max
- where h1: "x_max < x"
- and h2: "x_max \<in> L\<^isub>1\<star>"
- and h3: "(x - x_max) @ z \<in> L\<^isub>1\<star>"
- and h4:"\<forall> xa < x. xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>
- \<longrightarrow> length xa \<le> length x_max"
- proof-
- let ?S = "{xa. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}"
- have "finite ?S"
- by (rule_tac B = "{xa. xa < x}" in finite_subset,
- auto simp:finite_strict_prefix_set)
- moreover have "?S \<noteq> {}" using False xz_in_star
- by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def)
- ultimately have "\<exists> max \<in> ?S. \<forall> a \<in> ?S. length a \<le> length max"
- using finite_set_has_max by blast
- thus ?thesis using that by blast
- qed
- obtain ya
- where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>" and h7: "(x - x_max) \<approx>L\<^isub>1 (y - ya)"
- proof-
- from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} =
- {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right")
- by (auto simp:tag_str_STAR_def)
- moreover have "\<approx>L\<^isub>1 `` {x - x_max} \<in> ?left" using h1 h2 by auto
- ultimately have "\<approx>L\<^isub>1 `` {x - x_max} \<in> ?right" by simp
- with that show ?thesis apply
- (simp add:Image_def str_eq_rel_def str_eq_def) by blast
- qed
- have "(y - ya) @ z \<in> L\<^isub>1\<star>"
- proof-
- from h3 h1 obtain a b where a_in: "a \<in> L\<^isub>1"
- and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>"
- and ab_max: "(x - x_max) @ z = a @ b"
- by (drule_tac star_decom, auto simp:strict_prefix_def elim:prefixE)
- have "(x - x_max) \<le> a \<and> (a - (x - x_max)) @ b = z"
- proof -
- have "((x - x_max) \<le> a \<and> (a - (x - x_max)) @ b = z) \<or>
- (a < (x - x_max) \<and> ((x - x_max) - a) @ z = b)"
- using app_eq_dest[OF ab_max] by (auto simp:strict_prefix_def)
- moreover {
- assume np: "a < (x - x_max)" and b_eqs: " ((x - x_max) - a) @ z = b"
- have "False"
- proof -
- let ?x_max' = "x_max @ a"
- have "?x_max' < x"
- using np h1 by (clarsimp simp:strict_prefix_def diff_prefix)
- moreover have "?x_max' \<in> L\<^isub>1\<star>"
- using a_in h2 by (simp add:star_intro3)
- moreover have "(x - ?x_max') @ z \<in> L\<^isub>1\<star>"
- using b_eqs b_in np h1 by (simp add:diff_diff_appd)
- moreover have "\<not> (length ?x_max' \<le> length x_max)"
- using a_neq by simp
- ultimately show ?thesis using h4 by blast
- qed
- } ultimately show ?thesis by blast
- qed
- then obtain za where z_decom: "z = za @ b"
- and x_za: "(x - x_max) @ za \<in> L\<^isub>1"
- using a_in by (auto elim:prefixE)
- from x_za h7 have "(y - ya) @ za \<in> L\<^isub>1"
- by (auto simp:str_eq_def str_eq_rel_def)
- with b_in have "((y - ya) @ za) @ b \<in> L\<^isub>1\<star>" by blast
- with z_decom show ?thesis by auto
- qed
- with h5 h6 show ?thesis
- by (drule_tac star_intro1) (auto simp:strict_prefix_def elim:prefixE)
- qed
- }
- -- {* By instantiating the reasoning pattern just derived for both directions:*}
- from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
- -- {* The thesis is proved as a trival consequence: *}
show ?thesis unfolding str_eq_def str_eq_rel_def by blast
qed
lemma quot_star_finiteI [intro]:
- fixes L1::"lang"
assumes finite1: "finite (UNIV // \<approx>L1)"
shows "finite (UNIV // \<approx>(L1\<star>))"
proof (rule_tac tag = "tag_str_STAR L1" in tag_finite_imageD)
@@ -803,76 +461,9 @@
shows "finite (UNIV // \<approx>(L r))"
by (induct r) (auto)
+
theorem Myhill_Nerode:
shows "(\<exists>r::rexp. A = L r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
-using Myhill_Nerode1 Myhill_Nerode2 by metis
-
-(*
-section {* Closure properties *}
-
-abbreviation
- reg :: "lang \<Rightarrow> bool"
-where
- "reg A \<equiv> \<exists>r::rexp. A = L r"
-
-
-
-lemma closure_union[intro]:
- assumes "reg A" "reg B"
- shows "reg (A \<union> B)"
-using assms
-apply(auto)
-apply(rule_tac x="ALT r ra" in exI)
-apply(auto)
-done
-
-lemma closure_seq[intro]:
- assumes "reg A" "reg B"
- shows "reg (A ;; B)"
-using assms
-apply(auto)
-apply(rule_tac x="SEQ r ra" in exI)
-apply(auto)
-done
-
-lemma closure_star[intro]:
- assumes "reg A"
- shows "reg (A\<star>)"
-using assms
-apply(auto)
-apply(rule_tac x="STAR r" in exI)
-apply(auto)
-done
-
-lemma closure_complement[intro]:
- assumes "reg A"
- shows "reg (- A)"
-using assms
-unfolding Myhill_Nerode
-unfolding str_eq_rel_def
-by auto
-
-lemma closure_difference[intro]:
- assumes "reg A" "reg B"
- shows "reg (A - B)"
-proof -
- have "A - B = - ((- A) \<union> B)" by blast
- moreover
- have "reg (- ((- A) \<union> B))"
- using assms by blast
- ultimately show "reg (A - B)" by simp
-qed
-
-lemma closure_intersection[intro]:
- assumes "reg A" "reg B"
- shows "reg (A \<inter> B)"
-proof -
- have "A \<inter> B = - ((- A) \<union> (- B))" by blast
- moreover
- have "reg (- ((- A) \<union> (- B)))"
- using assms by blast
- ultimately show "reg (A \<inter> B)" by simp
-qed
-*)
+using Myhill_Nerode1 Myhill_Nerode2 by auto
end
--- a/Paper/Paper.thy Thu May 12 05:55:05 2011 +0000
+++ b/Paper/Paper.thy Wed May 18 19:54:43 2011 +0000
@@ -12,9 +12,8 @@
abbreviation
"EClass x R \<equiv> R `` {x}"
-abbreviation
- "append_rexp2 r_itm r \<equiv> append_rexp r r_itm"
-
+abbreviation
+ "Append_rexp2 r_itm r == Append_rexp r r_itm"
notation (latex output)
str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
@@ -32,8 +31,9 @@
EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
- append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
- append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
+ Append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
+ Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
+
uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and
@@ -494,8 +494,8 @@
\begin{center}
@{text "\<calL>(Y, r) \<equiv>"} %
- @{thm (rhs) L_rhs_item.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
- @{thm L_rhs_item.simps(1)[where r="r", THEN eq_reflection]}
+ @{thm (rhs) L_rhs_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
+ @{thm L_rhs_trm.simps(1)[where r="r", THEN eq_reflection]}
\end{center}
\noindent
@@ -561,13 +561,13 @@
we define the \emph{append-operation} taking a term and a regular expression as argument
\begin{center}
- @{thm append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
- @{thm append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
+ @{thm Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm}
+ @{thm Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}
\end{center}
\noindent
We lift this operation to entire right-hand sides of equations, written as
- @{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. With this we can define
+ @{thm (lhs) Append_rexp_rhs_def[where rexp="r"]}. With this we can define
the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as:
%
\begin{equation}\label{arden_def}
@@ -712,10 +712,10 @@
@{term "finite ES"} & @{text "(finiteness)"}\\
& @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\
& @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\
- & @{text "\<and>"} & @{thm (rhs) distinct_equas_def}\\
+ & @{text "\<and>"} & @{thm (rhs) distinctness_def}\\
& & & @{text "(distinctness)"}\\
& @{text "\<and>"} & @{thm (rhs) ardenable_all_def} & @{text "(ardenable)"}\\
- & @{text "\<and>"} & @{thm (rhs) valid_eqs_def} & @{text "(validity)"}\\
+ & @{text "\<and>"} & @{thm (rhs) validity_def} & @{text "(validity)"}\\
\end{tabular}
\end{center}
--- a/Prefix_subtract.thy Thu May 12 05:55:05 2011 +0000
+++ b/Prefix_subtract.thy Wed May 18 19:54:43 2011 +0000
@@ -1,59 +1,60 @@
theory Prefix_subtract
- imports Main
- "~~/src/HOL/Library/List_Prefix"
+ imports Main "~~/src/HOL/Library/List_Prefix"
begin
+
section {* A small theory of prefix subtraction *}
text {*
- The notion of @{text "prefix_subtract"} is need to make proofs more readable.
- *}
+ The notion of @{text "prefix_subtract"} makes
+ the second direction of the Myhill-Nerode theorem
+ more readable.
+*}
+
+instantiation list :: (type) minus
+begin
-fun prefix_subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "-" 51)
+fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
- "prefix_subtract [] xs = []"
-| "prefix_subtract (x#xs) [] = x#xs"
-| "prefix_subtract (x#xs) (y#ys) = (if x = y then prefix_subtract xs ys else (x#xs))"
+ "minus_list [] xs = []"
+| "minus_list (x#xs) [] = x#xs"
+| "minus_list (x#xs) (y#ys) = (if x = y then minus_list xs ys else (x#xs))"
+
+instance by default
+
+end
+
+lemma [simp]: "x - [] = x"
+by (induct x) (auto)
lemma [simp]: "(x @ y) - x = y"
-apply (induct x)
-by (case_tac y, simp+)
+by (induct x) (auto)
lemma [simp]: "x - x = []"
-by (induct x, auto)
-
-lemma [simp]: "x = xa @ y \<Longrightarrow> x - xa = y "
-by (induct x, auto)
-
-lemma [simp]: "x - [] = x"
-by (induct x, auto)
+by (induct x) (auto)
-lemma [simp]: "(x - y = []) \<Longrightarrow> (x \<le> y)"
-proof-
- have "\<exists>xa. x = xa @ (x - y) \<and> xa \<le> y"
- apply (rule prefix_subtract.induct[of _ x y], simp+)
- by (clarsimp, rule_tac x = "y # xa" in exI, simp+)
- thus "(x - y = []) \<Longrightarrow> (x \<le> y)" by simp
-qed
+lemma [simp]: "x = z @ y \<Longrightarrow> x - z = y "
+by (induct x) (auto)
lemma diff_prefix:
"\<lbrakk>c \<le> a - b; b \<le> a\<rbrakk> \<Longrightarrow> b @ c \<le> a"
-by (auto elim:prefixE)
+by (auto elim: prefixE)
-lemma diff_diff_appd:
+lemma diff_diff_append:
"\<lbrakk>c < a - b; b < a\<rbrakk> \<Longrightarrow> (a - b) - c = a - (b @ c)"
apply (clarsimp simp:strict_prefix_def)
by (drule diff_prefix, auto elim:prefixE)
-lemma app_eq_cases[rule_format]:
- "\<forall> x . x @ y = m @ n \<longrightarrow> (x \<le> m \<or> m \<le> x)"
-apply (induct y, simp)
-apply (clarify, drule_tac x = "x @ [a]" in spec)
-by (clarsimp, auto simp:prefix_def)
+lemma append_eq_cases:
+ assumes a: "x @ y = m @ n"
+ shows "x \<le> m \<or> m \<le> x"
+unfolding prefix_def using a
+by (auto simp add: append_eq_append_conv2)
-lemma app_eq_dest:
- "x @ y = m @ n \<Longrightarrow>
- (x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"
-by (frule_tac app_eq_cases, auto elim:prefixE)
+lemma append_eq_dest:
+ assumes a: "x @ y = m @ n"
+ shows "(x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"
+using append_eq_cases[OF a] a
+by (auto elim: prefixE)
end