# HG changeset patch
# User urbanc
# Date 1296406797 0
# Node ID 32bff8310071469ffbc758045526b3bd0cde9279
# Parent  59936c012addbc9c838bcdf55363662f9eac618d
revised proof of Ardens lemma

diff -r 59936c012add -r 32bff8310071 Myhill_1.thy
--- a/Myhill_1.thy	Sun Jan 30 12:22:07 2011 +0000
+++ b/Myhill_1.thy	Sun Jan 30 16:59:57 2011 +0000
@@ -32,11 +32,14 @@
   Sequential composition of two languages @{text "L1"} and @{text "L2"} 
 *}
 
-definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" ("_ ;; _" [100,100] 100)
+definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100)
 where 
   "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
 
-text {* Transitive closure of language @{text "L"}. *}
+text {* 
+  Transitive closure of language @{text "L"}. 
+*}
+
 inductive_set
   Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102)
   for L 
@@ -44,23 +47,35 @@
   start[intro]: "[] \<in> L\<star>"
 | step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>" 
 
-text {* Some properties of operator @{text ";;"}.*}
+text {* Some properties of operator @{text ";;"}. *}
 
-lemma seq_union_distrib:
-  "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)"
-by (auto simp:Seq_def)
+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:
   "\<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x @ y \<in> A ;; B "
 by (auto simp:Seq_def)
 
 lemma seq_assoc:
-  "(A ;; B) ;; C = A ;; (B ;; C)"
-apply(auto simp:Seq_def)
-apply blast
+  shows "(A ;; B) ;; C = A ;; (B ;; C)"
+unfolding Seq_def
+apply(auto)
+apply(blast)
 by (metis append_assoc)
 
-lemma star_intro1[rule_format]: "x \<in> lang\<star> \<Longrightarrow> \<forall> y. y \<in> lang\<star> \<longrightarrow> x @ y \<in> lang\<star>"
+lemma seq_empty [simp]:
+  shows "A ;; {[]} = A"
+  and   "{[]} ;; A = A"
+by (simp_all add: Seq_def)
+
+
+lemma star_intro1[rule_format]: 
+  "x \<in> lang\<star> \<Longrightarrow> \<forall> y. y \<in> lang\<star> \<longrightarrow> x @ y \<in> lang\<star>"
 by (erule Star.induct, auto)
 
 lemma star_intro2: "y \<in> lang \<Longrightarrow> y \<in> lang\<star>"
@@ -74,13 +89,176 @@
   "\<lbrakk>x \<in> lang\<star>; x \<noteq> []\<rbrakk> \<Longrightarrow>(\<exists> a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> lang \<and> b \<in> lang\<star>)"
 by (induct x rule: Star.induct, simp, blast)
 
-lemma star_decom': 
-  "\<lbrakk>x \<in> lang\<star>; x \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>a b. x = a @ b \<and> a \<in> lang\<star> \<and> b \<in> lang"
-apply (induct x rule:Star.induct, simp)
-apply (case_tac "s2 = []")
-apply (rule_tac x = "[]" in exI, rule_tac x = s1 in exI, simp add:start)
-apply (simp, (erule exE| erule conjE)+)
-by (rule_tac x = "s1 @ a" in exI, rule_tac x = b in exI, simp add:step)
+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 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 Seq_def by auto
+qed
+
+fun 
+  pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100)
+where
+  "A \<up> 0 = {[]}"
+| "A \<up> (Suc n) =  A ;; (A \<up> n)" 
+
+lemma star_pow_eq:
+  shows "A\<star> = (\<Union>n. A \<up> n)"
+proof -
+  { fix n x
+    assume "x \<in> (A \<up> n)"
+    then have "x \<in> A\<star>"
+      by (induct n arbitrary: x) (auto simp add: Seq_def)
+  }
+  moreover
+  { fix x
+    assume "x \<in> A\<star>"
+    then have "\<exists>n. x \<in> A \<up> n"
+    proof (induct rule: Star.induct)
+      case start
+      have "[] \<in> A \<up> 0" by auto
+      then show "\<exists>n. [] \<in> A \<up> n" by blast
+    next
+      case (step s1 s2)
+      have "s1 \<in> A" by fact
+      moreover
+      have "\<exists>n. s2 \<in> A \<up> n" by fact
+      then obtain n where "s2 \<in> A \<up> n" by blast
+      ultimately
+      have "s1 @ s2 \<in> A \<up> (Suc n)" by (auto simp add: Seq_def)
+      then show "\<exists>n. s1 @ s2 \<in> A \<up> n" by blast
+    qed
+  }
+  ultimately show "A\<star> = (\<Union>n. A \<up> n)" by auto
+qed
+
+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_pow_eq
+unfolding seq_Union_left
+unfolding seq_pow_comm
+unfolding 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 slightly modified version of Arden's lemma *}
+
+text {* 
+  Arden's lemma expressed at the level of languages, rather 
+  than the level of regular expression. 
+*}
+
+
+lemma ardens_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 ardens_revised:
+  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 lang_star_cases)
+  then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)" 
+    unfolding Seq_def by simp
+  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 ardens_helper[OF eq, of "n"] by auto }
+  then have "B ;; A\<star> \<subseteq> X" unfolding star_pow_eq Seq_def
+    by (auto simp add: UNION_def)
+  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 ardens_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 star_pow_eq seq_Union_left
+      by auto }
+  then have "X \<subseteq> B ;; A\<star>" by auto
+  ultimately 
+  show "X = B ;; A\<star>" by simp
+qed
+
 
 
 text {* The syntax of regular expressions is defined by the datatype @{text "rexp"}. *}
@@ -117,6 +295,29 @@
   | "L_rexp (STAR r) = (L_rexp r)\<star>"
 end
 
+text {*
+  To obtain equational system out of finite set of equivalent classes, a fold operation
+  on finite set @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "fold"}
+  more robust than the @{text "fold"} in Isabelle library. The expression @{text "folds f"}
+  makes sense when @{text "f"} is not @{text "associative"} and @{text "commutitive"},
+  while @{text "fold f"} does not.  
+*}
+
+definition 
+  folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
+where
+  "folds f z S \<equiv> SOME x. fold_graph f z S x"
+
+text {* 
+  The following lemma assures that the arbitrary choice made by the @{text "SOME"} in @{text "folds"}
+  does not affect the @{text "L"}-value of the resultant regular expression. 
+  *}
+lemma folds_alt_simp [simp]:
+  "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)"
+apply (rule set_eq_intro, simp add:folds_def)
+apply (rule someI2_ex, erule finite_imp_fold_graph)
+by (erule fold_graph.induct, auto)
+
 (* Just a technical lemma. *)
 lemma [simp]:
   shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
@@ -160,98 +361,6 @@
 
 section {* Direction @{text "finite partition \<Rightarrow> regular language"}*}
 
-subsection {*
-  Ardens lemma
-  *}
-text {* Ardens lemma expressed at the level of language, rather than the level of regular expression. *}
-
-theorem ardens_revised:
-  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" 
-    by (auto simp:Seq_def star_intro3 star_decom')  
-  then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)" 
-    unfolding Seq_def by simp
-  also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"  
-    unfolding Seq_def by auto
-  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"
-  hence c1': "\<And> x. x \<in> B \<Longrightarrow> x \<in> X" 
-    and c2': "\<And> x y. \<lbrakk>x \<in> X; y \<in> A\<rbrakk> \<Longrightarrow> x @ y \<in> X" 
-    using Seq_def by auto
-  show "X = B ;; A\<star>" 
-  proof
-    show "B ;; A\<star> \<subseteq> X"
-    proof-
-      { fix x y
-        have "\<lbrakk>y \<in> A\<star>; x \<in> X\<rbrakk> \<Longrightarrow> x @ y \<in> X "
-          apply (induct arbitrary:x rule:Star.induct, simp)
-          by (auto simp only:append_assoc[THEN sym] dest:c2')
-      } thus ?thesis using c1' by (auto simp:Seq_def) 
-    qed
-  next
-    show "X \<subseteq> B ;; A\<star>"
-    proof-
-      { fix x 
-        have "x \<in> X \<Longrightarrow> x \<in> B ;; A\<star>"
-        proof (induct x taking:length rule:measure_induct)
-          fix z
-          assume hyps: 
-            "\<forall>y. length y < length z \<longrightarrow> y \<in> X \<longrightarrow> y \<in> B ;; A\<star>" 
-            and z_in: "z \<in> X"
-          show "z \<in> B ;; A\<star>"
-          proof (cases "z \<in> B")
-            case True thus ?thesis by (auto simp:Seq_def start)
-          next
-            case False hence "z \<in> X ;; A" using eq' z_in by auto
-            then obtain za zb where za_in: "za \<in> X" 
-              and zab: "z = za @ zb \<and> zb \<in> A" and zbne: "zb \<noteq> []" 
-              using nemp unfolding Seq_def by blast
-            from zbne zab have "length za < length z" by auto
-            with za_in hyps have "za \<in> B ;; A\<star>" by blast
-            hence "za @ zb \<in> B ;; A\<star>" using zab 
-              by (clarsimp simp:Seq_def, blast dest:star_intro3)
-            thus ?thesis using zab by simp       
-          qed
-        qed 
-      } thus ?thesis by blast
-    qed
-  qed
-qed
-
-subsection {*
-  Defintions peculiar to this direction
-  *}
-
-text {*
-  To obtain equational system out of finite set of equivalent classes, a fold operation
-  on finite set @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "fold"}
-  more robust than the @{text "fold"} in Isabelle library. The expression @{text "folds f"}
-  makes sense when @{text "f"} is not @{text "associative"} and @{text "commutitive"},
-  while @{text "fold f"} does not.  
-*}
-
-definition 
-  folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
-where
-  "folds f z S \<equiv> SOME x. fold_graph f z S x"
-
-text {* 
-  The following lemma assures that the arbitrary choice made by the @{text "SOME"} in @{text "folds"}
-  does not affect the @{text "L"}-value of the resultant regular expression. 
-  *}
-lemma folds_alt_simp [simp]:
-  "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)"
-apply (rule set_eq_intro, simp add:folds_def)
-apply (rule someI2_ex, erule finite_imp_fold_graph)
-by (erule fold_graph.induct, auto)
-
 text {* 
   The relationship between equivalent classes can be described by an
   equational system.
@@ -756,7 +865,7 @@
   qed
   moreover have "L (arden_variate X rhs) = (B ;; A\<star>)" (is "?L = ?R")
     by (simp only:arden_variate_def L_rhs_union_distrib lang_of_append_rhs 
-                  B_def A_def b_def L_rexp.simps seq_union_distrib)
+                  B_def A_def b_def L_rexp.simps seq_union_distrib_left)
    ultimately show ?thesis by simp
 qed 
 
diff -r 59936c012add -r 32bff8310071 Paper/Paper.thy
--- a/Paper/Paper.thy	Sun Jan 30 12:22:07 2011 +0000
+++ b/Paper/Paper.thy	Sun Jan 30 16:59:57 2011 +0000
@@ -6,7 +6,11 @@
 declare [[show_question_marks = false]]
 
 notation (latex output)
-  str_eq_rel ("\<approx>\<^bsub>_\<^esub>")
+  str_eq_rel ("\<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)
 
 (*>*)
 
@@ -16,6 +20,45 @@
   
 *}
 
+section {* Preliminaries *}
+
+text {*
+  A central technique in our proof is the solution of equational systems
+  involving regular expressions. For this we will use the following ``reverse'' 
+  version of Arden's lemma.
+
+  \begin{lemma}[Reverse Arden's Lemma]\mbox{}\\
+  If @{thm (prem 1) ardens_revised} then
+  @{thm (lhs) ardens_revised} has the unique solution
+  @{thm (rhs) ardens_revised}.
+  \end{lemma}
+
+  \begin{proof}
+  For right-to-left direction we assume @{thm (rhs) ardens_revised} and show
+  @{thm (lhs) ardens_revised}. From Lemma ??? 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 @{term "B \<union> (B ;; A\<star>) ;; A"}. This completes this direction. 
+
+  For the other direction we assume @{thm (lhs) ardens_revised}. By a simple induction
+  on @{text n}, we can show the property
+
+  \begin{center}
+  @{text "(*)"}\hspace{5mm} @{thm (concl) ardens_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 Lemma ???.
+  The inclusion in the other direction we establishing by assuming a string @{text s}
+  with length @{text k} is element in @{text X}. Since @{thm (prem 1) ardens_revised}
+  we know that @{term "s \<notin> X ;; (A \<up> Suc k)"} as its length is only @{text k}. 
+  From @{text "(*)"} it follows that
+  @{term s} must be 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 Lemma ??? this
+  is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed
+  \end{proof}
+*}
 
 section {* Regular expressions have finitely many partitions *}
 
@@ -27,7 +70,7 @@
 
   \begin{proof}
   By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY}
-  and @{const CHAR} are starightforward, because we can easily establish
+  and @{const CHAR} are straightforward, because we can easily establish
 
   \begin{center}
   \begin{tabular}{l}
diff -r 59936c012add -r 32bff8310071 tphols-2011/myhill.pdf
Binary file tphols-2011/myhill.pdf has changed