# HG changeset patch
# User urbanc
# Date 1314017367 0
# Node ID 5d724fe0e096d7289b0da76b9c9c6d5b021e23fb
# Parent  09e6f3719cbcad7cc677be910259f6ff4d962d4f
changes according to afp-submission

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