# HG changeset patch
# User zhang
# Date 1296301277 0
# Node ID 61d9684a557a8bd676b894d63661d5551fc9928b
# Parent  bea2466a6084245d7e24041d6a772994d01c605f
Myhill.thy and Myhill_1.thy changed.

diff -r bea2466a6084 -r 61d9684a557a Myhill.thy
--- a/Myhill.thy	Fri Jan 28 19:17:40 2011 +0000
+++ b/Myhill.thy	Sat Jan 29 11:41:17 2011 +0000
@@ -2,9 +2,9 @@
   imports Myhill_1
 begin
 
-section {* Direction: @{text "regular language \<Rightarrow>finite partition"} *}
+section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
 
-subsection {* The scheme for this direction *}
+subsection {* The scheme*}
 
 text {* 
   The following convenient notation @{text "x \<approx>Lang y"} means:
@@ -243,9 +243,9 @@
   qed
 qed
 
-subsection {* Lemmas for basic cases *}
+subsection {* The proof*}
 
-subsection {* The case for @{const "NULL"} *}
+subsubsection {* The case for @{const "NULL"} *}
 
 lemma quot_null_eq:
   shows "(UNIV // \<approx>{}) = ({UNIV}::lang set)"
@@ -256,7 +256,7 @@
 unfolding quot_null_eq by simp
 
 
-subsection {* The case for @{const "EMPTY"} *}
+subsubsection {* The case for @{const "EMPTY"} *}
 
 
 lemma quot_empty_subset:
@@ -283,7 +283,7 @@
 by (rule finite_subset[OF quot_empty_subset]) (simp)
 
 
-subsection {* The case for @{const "CHAR"} *}
+subsubsection {* The case for @{const "CHAR"} *}
 
 lemma quot_char_subset:
   "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
@@ -316,12 +316,13 @@
 
 
 
-subsection {* The case for @{text "SEQ"}*}
+subsubsection {* The case for @{text "SEQ"}*}
 
 definition 
   tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
 where
-  "tag_str_SEQ L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa.  xa \<le> x \<and> xa \<in> L1}))"
+  "tag_str_SEQ L1 L2 = 
+     (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa.  xa \<le> x \<and> xa \<in> L1}))"
 
 
 lemma append_seq_elim:
@@ -410,7 +411,7 @@
     by auto
 qed
 
-subsection {* The case for @{const ALT} *}
+subsubsection {* The case for @{const ALT} *}
 
 definition 
   tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)"
@@ -440,14 +441,14 @@
     by auto
 qed
 
-subsection {* The case for @{const "STAR"} *}
+subsubsection {* The case for @{const "STAR"} *}
 
 text {* 
   This turned out to be the trickiest case. 
   Any string @{text "x"} in language @{text "L\<^isub>1\<star>"}, 
   can be splited into a prefix @{text "xa \<in> L\<^isub>1\<star>"} and a suffix @{text "x - xa \<in> L\<^isub>1"}.
   For one such @{text "x"}, there can be many such splits. The tagging of @{text "x"} is then 
-  defined by collecting the @{text "L\<^isub>1"}-state of the suffixes from every possible split.
+  defined by collecting the @{text "L\<^isub>1"}-state of the suffixe from every possible split.
 *} 
 
 definition 
@@ -496,6 +497,7 @@
   the tagging function for case @{text "STAR"}.
   *}
 
+
 lemma tag_str_STAR_injI:
   fixes v w
   assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"
@@ -531,6 +533,173 @@
         \end{minipage}
         *}
       case False
+      -- {* 
+        \begin{minipage}{0.9\textwidth}
+        Since @{text "x @ z \<in> L\<^isub>1\<star>"}, @{text "x"} can always be splited
+        by a prefix @{text "xa"} together with its suffix @{text "x - xa"}, such
+        that both @{text "xa"} and @{text "(x - xa) @ z"} are in @{text "L\<^isub>1\<star>"},
+        and there could be many such splittings.Therefore, the following set @{text "?S"} 
+        is nonempty, and finite as well:
+        \end{minipage}
+        *}
+      let ?S = "{xa. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}"
+      have "finite ?S"
+        by (rule_tac B = "{xa. xa < x}" in finite_subset, 
+          auto simp:finite_strict_prefix_set)
+      moreover have "?S \<noteq> {}" using False xz_in_star
+        by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def)
+      -- {* Since @{text "?S"} is finite, we can always single out the longest
+          and name it @{text "xa_max"}:
+          *}
+      ultimately have "\<exists> xa_max \<in> ?S. \<forall> xa \<in> ?S. length xa \<le> length xa_max" 
+        using finite_set_has_max by blast
+      then obtain xa_max 
+        where h1: "xa_max < x" 
+        and h2: "xa_max \<in> L\<^isub>1\<star>" 
+        and h3: "(x - xa_max) @ z \<in> L\<^isub>1\<star>" 
+        and h4:"\<forall> xa < x. xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>  
+                                     \<longrightarrow> length xa \<le> length xa_max"
+        by blast
+      -- {*
+          \begin{minipage}{0.9\textwidth}
+          By the equality of tags, the counterpart of @{text "xa_max"} among 
+          @{text "y"}-prefixes, named @{text "ya"}, can be found:
+          \end{minipage}
+          *}
+      obtain ya 
+        where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>" 
+        and eq_xya: "(x - xa_max) \<approx>L\<^isub>1 (y - ya)"
+      proof-
+        from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} = 
+          {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right")
+          by (auto simp:tag_str_STAR_def)
+        moreover have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?left" using h1 h2 by auto
+        ultimately have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?right" by simp
+        with prems show ?thesis apply 
+          (simp add:Image_def str_eq_rel_def str_eq_def) by blast
+      qed 
+      -- {*
+          \begin{minipage}{0.9\textwidth}
+          If the following proposition can be proved, then the @{text "?thesis"}:
+          @{text "y @ z \<in> L\<^isub>1\<star>"} is just a simple consequence.
+          \end{minipage}
+          *}
+      have "(y - ya) @ z \<in> L\<^isub>1\<star>" 
+      proof-
+        -- {* The idea is to split the suffix @{text "z"} into @{text "za"} and @{text "zb"}, 
+          such that: *}
+        obtain za zb where eq_zab: "z = za @ zb" 
+          and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>"
+        proof -
+          -- {* 
+            \begin{minipage}{0.9\textwidth}
+            Since @{text  "(x - xa_max) @ z"} is in @{text "L\<^isub>1\<star>"}, it can be split into
+            @{text "a"} and @{text "b"} such that:
+            \end{minipage}
+            *}
+          from h1 have "(x - xa_max) @ z \<noteq> []" 
+            by (auto simp:strict_prefix_def elim:prefixE)
+          from star_decom [OF h3 this]
+          obtain a b where a_in: "a \<in> L\<^isub>1" 
+            and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" 
+            and ab_max: "(x - xa_max) @ z = a @ b" by blast
+          -- {* Now the candiates for @{text "za"} and @{text "zb"} are found:*}
+          let ?za = "a - (x - xa_max)" and ?zb = "b"
+          have pfx: "(x - xa_max) \<le> a" (is "?P1") 
+            and eq_z: "z = ?za @ ?zb" (is "?P2")
+          proof -
+            -- {* 
+              \begin{minipage}{0.9\textwidth}
+              Since @{text "(x - xa_max) @ z = a @ b"}, the string @{text "(x - xa_max) @ z"}
+              could be splited in two ways:
+              \end{minipage}
+              *}
+            have "((x - xa_max) \<le> a \<and> (a - (x - xa_max)) @ b = z) \<or> 
+              (a < (x - xa_max) \<and> ((x - xa_max) - a) @ z = b)" 
+              using app_eq_dest[OF ab_max] by (auto simp:strict_prefix_def)
+            moreover {
+              -- {* However, the undsired way can be refuted by absurdity: *}
+              assume np: "a < (x - xa_max)" 
+                and b_eqs: "((x - xa_max) - a) @ z = b"
+              have "False"
+              proof -
+                let ?xa_max' = "xa_max @ a"
+                have "?xa_max' < x" 
+                  using np h1 by (clarsimp simp:strict_prefix_def diff_prefix) 
+                moreover have "?xa_max' \<in> L\<^isub>1\<star>" 
+                  using a_in h2 by (simp add:star_intro3) 
+                moreover have "(x - ?xa_max') @ z \<in> L\<^isub>1\<star>" 
+                  using b_eqs b_in np h1 by (simp add:diff_diff_appd)
+                moreover have "\<not> (length ?xa_max' \<le> length xa_max)" 
+                  using a_neq by simp
+                ultimately show ?thesis using h4 by blast
+              qed }
+            -- {* Now it can be shown that the splitting goes the way we desired. *}
+            ultimately show ?P1 and ?P2 by auto
+          qed
+          hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in by (auto elim:prefixE)
+          -- {* Now candidates @{text "?za"} and @{text "?zb"} have all the requred properteis. *}
+          with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1" 
+            by (auto simp:str_eq_def str_eq_rel_def)
+           with eq_z and b_in prems
+          show ?thesis by blast
+        qed
+        -- {* 
+            \begin{minipage}{0.9\textwidth}
+            From the properties of @{text "za"} and @{text "zb"} such obtained,
+              @{text "?thesis"} can be shown easily. 
+            \end{minipage}
+            *}
+        from step [OF l_za ls_zb]
+        have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" .
+        with eq_zab show ?thesis by simp
+      qed
+      with h5 h6 show ?thesis 
+        by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE)
+    qed
+  } 
+  -- {* By instantiating the reasoning pattern just derived for both directions:*} 
+  from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
+  -- {* The thesis is proved as a trival consequence: *} 
+    show  ?thesis by (unfold str_eq_def str_eq_rel_def, blast)
+qed
+
+
+lemma -- {* The oringal version with a poor readability*}
+  fixes v w
+  assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"
+  shows "(v::string) \<approx>(L\<^isub>1\<star>) w"
+proof-
+    -- {* 
+    \begin{minipage}{0.9\textwidth}
+    According to the definition of @{text "\<approx>Lang"}, 
+    proving @{text "v \<approx>(L\<^isub>1\<star>) w"} amounts to
+    showing: for any string @{text "u"},
+    if @{text "v @ u \<in> (L\<^isub>1\<star>)"} then @{text "w @ u \<in> (L\<^isub>1\<star>)"} and vice versa.
+    The reasoning pattern for both directions are the same, as derived
+    in the following:
+    \end{minipage}
+    *}
+  { fix x y z
+    assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>" 
+      and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y"
+    have "y @ z \<in> L\<^isub>1\<star>"
+    proof(cases "x = []")
+      -- {* 
+        The degenerated case when @{text "x"} is a null string is easy to prove:
+        *}
+      case True
+      with tag_xy have "y = []" 
+        by (auto simp:tag_str_STAR_def strict_prefix_def)
+      thus ?thesis using xz_in_star True by simp
+    next
+        -- {*
+        \begin{minipage}{0.9\textwidth}
+        The case when @{text "x"} is not null, and
+        @{text "x @ z"} is in @{text "L\<^isub>1\<star>"}, 
+        \end{minipage}
+        *}
+      case False
       obtain x_max 
         where h1: "x_max < x" 
         and h2: "x_max \<in> L\<^isub>1\<star>" 
@@ -621,6 +790,7 @@
     by auto
 qed
 
+subsubsection{* The conclusion *}
 
 lemma rexp_imp_finite:
   fixes r::"rexp"
diff -r bea2466a6084 -r 61d9684a557a Myhill_1.thy
--- a/Myhill_1.thy	Fri Jan 28 19:17:40 2011 +0000
+++ b/Myhill_1.thy	Sat Jan 29 11:41:17 2011 +0000
@@ -82,6 +82,87 @@
 apply (simp, (erule exE| erule conjE)+)
 by (rule_tac x = "s1 @ a" in exI, rule_tac x = b in exI, simp add:step)
 
+
+text {* The syntax of regular expressions is defined by the datatype @{text "rexp"}. *}
+datatype rexp =
+  NULL
+| EMPTY
+| CHAR char
+| SEQ rexp rexp
+| ALT rexp rexp
+| STAR rexp
+
+
+text {* 
+  The following @{text "L"} is an overloaded operator, where @{text "L(x)"} evaluates to 
+  the language represented by the syntactic object @{text "x"}.
+*}
+consts L:: "'a \<Rightarrow> string set"
+
+
+text {* 
+  The @{text "L(rexp)"} for regular expression @{text "rexp"} is defined by the 
+  following overloading function @{text "L_rexp"}.
+*}
+overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> string set"
+begin
+fun
+  L_rexp :: "rexp \<Rightarrow> string set"
+where
+    "L_rexp (NULL) = {}"
+  | "L_rexp (EMPTY) = {[]}"
+  | "L_rexp (CHAR c) = {[c]}"
+  | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)"
+  | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"
+  | "L_rexp (STAR r) = (L_rexp r)\<star>"
+end
+
+(* Just a technical lemma. *)
+lemma [simp]:
+  shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
+by simp
+
+text {*
+  @{text "\<approx>L"} is an equivalent class defined by language @{text "Lang"}.
+*}
+definition
+  str_eq_rel ("\<approx>_" [100] 100)
+where
+  "\<approx>Lang \<equiv> {(x, y).  (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)}"
+
+text {* 
+  Among equivlant clases of @{text "\<approx>Lang"}, the set @{text "finals(Lang)"} singles out 
+  those which contains strings from @{text "Lang"}.
+*}
+
+definition 
+   "finals Lang \<equiv> {\<approx>Lang `` {x} | x . x \<in> Lang}"
+
+text {* 
+  The following lemma show the relationshipt between @{text "finals(Lang)"} and @{text "Lang"}.
+*}
+lemma lang_is_union_of_finals: 
+  "Lang = \<Union> finals(Lang)"
+proof 
+  show "Lang \<subseteq> \<Union> (finals Lang)"
+  proof
+    fix x
+    assume "x \<in> Lang"   
+    thus "x \<in> \<Union> (finals Lang)"
+      apply (simp add:finals_def, rule_tac x = "(\<approx>Lang) `` {x}" in exI)
+      by (auto simp:Image_def str_eq_rel_def)    
+  qed
+next
+  show "\<Union> (finals Lang) \<subseteq> Lang"
+    apply (clarsimp simp:finals_def str_eq_rel_def)
+    by (drule_tac x = "[]" in spec, auto)
+qed
+
+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:
@@ -144,40 +225,9 @@
   qed
 qed
 
-
-text {* The syntax of regular expressions is defined by the datatype @{text "rexp"}. *}
-datatype rexp =
-  NULL
-| EMPTY
-| CHAR char
-| SEQ rexp rexp
-| ALT rexp rexp
-| STAR rexp
-
-
-text {* 
-  The following @{text "L"} is an overloaded operator, where @{text "L(x)"} evaluates to 
-  the language represented by the syntactic object @{text "x"}.
-*}
-consts L:: "'a \<Rightarrow> string set"
-
-
-text {* 
-  The @{text "L(rexp)"} for regular expression @{text "rexp"} is defined by the 
-  following overloading function @{text "L_rexp"}.
-*}
-overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> string set"
-begin
-fun
-  L_rexp :: "rexp \<Rightarrow> string set"
-where
-    "L_rexp (NULL) = {}"
-  | "L_rexp (EMPTY) = {[]}"
-  | "L_rexp (CHAR c) = {[c]}"
-  | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)"
-  | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"
-  | "L_rexp (STAR r) = (L_rexp r)\<star>"
-end
+subsection {*
+  Defintions peculiar to this direction
+  *}
 
 text {*
   To obtain equational system out of finite set of equivalent classes, a fold operation
@@ -202,49 +252,6 @@
 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"
-by simp
-
-text {*
-  @{text "\<approx>L"} is an equivalent class defined by language @{text "Lang"}.
-*}
-definition
-  str_eq_rel ("\<approx>_" [100] 100)
-where
-  "\<approx>Lang \<equiv> {(x, y).  (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)}"
-
-text {* 
-  Among equivlant clases of @{text "\<approx>Lang"}, the set @{text "finals(Lang)"} singles out 
-  those which contains strings from @{text "Lang"}.
-*}
-
-definition 
-   "finals Lang \<equiv> {\<approx>Lang `` {x} | x . x \<in> Lang}"
-
-text {* 
-  The following lemma show the relationshipt between @{text "finals(Lang)"} and @{text "Lang"}.
-*}
-lemma lang_is_union_of_finals: 
-  "Lang = \<Union> finals(Lang)"
-proof 
-  show "Lang \<subseteq> \<Union> (finals Lang)"
-  proof
-    fix x
-    assume "x \<in> Lang"   
-    thus "x \<in> \<Union> (finals Lang)"
-      apply (simp add:finals_def, rule_tac x = "(\<approx>Lang) `` {x}" in exI)
-      by (auto simp:Image_def str_eq_rel_def)    
-  qed
-next
-  show "\<Union> (finals Lang) \<subseteq> Lang"
-    apply (clarsimp simp:finals_def str_eq_rel_def)
-    by (drule_tac x = "[]" in spec, auto)
-qed
-
-section {* Direction @{text "finite partition \<Rightarrow> regular language"}*}
-
 text {* 
   The relationship between equivalent classes can be described by an
   equational system.
diff -r bea2466a6084 -r 61d9684a557a tphols-2011/myhill.pdf
Binary file tphols-2011/myhill.pdf has changed