# HG changeset patch
# User urbanc
# Date 1297859153 0
# Node ID 79b37ef9505fc325227aa954684ec7e55dbc8f7e
# Parent  212bfa431fa50c7a956f90082863edb4caefed8c
minor updated

diff -r 212bfa431fa5 -r 79b37ef9505f Myhill_1.thy
--- a/Myhill_1.thy	Wed Feb 16 06:51:58 2011 +0000
+++ b/Myhill_1.thy	Wed Feb 16 12:25:53 2011 +0000
@@ -793,7 +793,7 @@
   def b \<equiv> "rhs - {Trn X r | r. Trn X r \<in> rhs}"
   def B \<equiv> "L b" 
   have "X = B ;; A\<star>"
-  proof-
+  proof -
     have "L rhs = L({Trn X r | r. Trn X r \<in> rhs} \<union> b)" by (auto simp: b_def)
     also have "\<dots> = X ;; A \<union> B"
       unfolding L_rhs_union_distrib[symmetric]
diff -r 212bfa431fa5 -r 79b37ef9505f Myhill_2.thy
--- a/Myhill_2.thy	Wed Feb 16 06:51:58 2011 +0000
+++ b/Myhill_2.thy	Wed Feb 16 12:25:53 2011 +0000
@@ -18,15 +18,18 @@
   "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)"
 
 text {*
-  The main lemma (@{text "rexp_imp_finite"}) is proved by a structural induction over regular expressions.
-  where base cases (cases for @{const "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straightforward to
-  proof. Real difficulty lies in inductive cases.  By inductive hypothesis, languages defined by
-  sub-expressions induce finite partitiions. Under such hypothsis, we need to prove that the language 
-  defined by the composite regular expression gives rise to finite partion.  
-  The basic idea is to attach a tag @{text "tag(x)"} to every string 
-  @{text "x"}. The tagging fuction @{text "tag"} is carefully devised, which returns tags 
-  made of equivalent classes of the partitions induced by subexpressoins, and therefore has a finite
-  range. Let @{text "Lang"} be the composite language, it is proved that:
+  The main lemma (@{text "rexp_imp_finite"}) is proved by a structural
+  induction over regular expressions.  where base cases (cases for @{const
+  "NULL"}, @{const "EMPTY"}, @{const "CHAR"}) are quite straightforward to
+  proof. Real difficulty lies in inductive cases.  By inductive hypothesis,
+  languages defined by sub-expressions induce finite partitiions. Under such
+  hypothsis, we need to prove that the language defined by the composite
+  regular expression gives rise to finite partion.  The basic idea is to
+  attach a tag @{text "tag(x)"} to every string @{text "x"}. The tagging
+  fuction @{text "tag"} is carefully devised, which returns tags made of
+  equivalent classes of the partitions induced by subexpressoins, and
+  therefore has a finite range. Let @{text "Lang"} be the composite language,
+  it is proved that:
   \begin{quote}
   If strings with the same tag are equivalent with respect to @{text "Lang"}, expressed as:
   \[
@@ -57,19 +60,22 @@
 definition 
    f_eq_rel ("=_=")
 where
-   "(=f=) = {(x, y) | x y. f x = f y}"
+   "=f= \<equiv> {(x, y) | x y. f x = f y}"
 
 lemma equiv_f_eq_rel:"equiv UNIV (=f=)"
   by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def)
 
-lemma finite_range_image: "finite (range f) \<Longrightarrow> finite (f ` A)"
-  by (rule_tac B = "{y. \<exists>x. y = f x}" in finite_subset, auto simp:image_def)
+lemma finite_range_image: 
+  assumes "finite (range f)"
+  shows "finite (f ` A)"
+  using assms unfolding image_def
+  by (rule_tac finite_subset) (auto)
 
 lemma finite_eq_f_rel:
   assumes rng_fnt: "finite (range tag)"
-  shows "finite (UNIV // (=tag=))"
+  shows "finite (UNIV // =tag=)"
 proof -
-  let "?f" =  "op ` tag" and ?A = "(UNIV // (=tag=))"
+  let "?f" =  "op ` tag" and ?A = "(UNIV // =tag=)"
   show ?thesis
   proof (rule_tac f = "?f" and A = ?A in finite_imageD) 
     -- {* 
@@ -109,7 +115,8 @@
   qed
 qed
 
-lemma finite_image_finite: "\<lbrakk>\<forall> x \<in> A. f x \<in> B; finite B\<rbrakk> \<Longrightarrow> finite (f ` A)"
+lemma finite_image_finite: 
+  "\<lbrakk>\<forall> x \<in> A. f x \<in> B; finite B\<rbrakk> \<Longrightarrow> finite (f ` A)"
   by (rule finite_subset [of _ B], auto)
 
 lemma refined_partition_finite:
@@ -357,7 +364,7 @@
 definition 
   tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)"
 where
-  "tag_str_ALT L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))"
+  "tag_str_ALT L1 L2 \<equiv> (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))"
 
 lemma quot_union_finiteI [intro]:
   fixes L1 L2::"lang"
@@ -401,7 +408,7 @@
 definition 
   tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
 where
-  "tag_str_SEQ L1 L2 = 
+  "tag_str_SEQ L1 L2 \<equiv>
      (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa.  xa \<le> x \<and> xa \<in> L1}))"
 
 text {* The following is a techical lemma which helps to split the @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"} mentioned above.*}
@@ -581,7 +588,7 @@
 definition 
   tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set"
 where
-  "tag_str_STAR L1 = (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
+  "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
 
 text {* A technical lemma. *}
 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> 
diff -r 212bfa431fa5 -r 79b37ef9505f Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Feb 16 06:51:58 2011 +0000
+++ b/Paper/Paper.thy	Wed Feb 16 12:25:53 2011 +0000
@@ -749,7 +749,7 @@
   that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"},
   and that the invariant holds for this equation. That means we 
   know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
-  this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties in the 
+  this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the 
   invariant and Lem.~???. Using the validity property for the equation @{text "X = rhs"},
   we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the arden operation
   removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
@@ -804,16 +804,23 @@
   \end{center}
 
   \end{proof}
+
+
+  @{thm tag_str_ALT_def[where ?L1.0="A" and ?L2.0="B"]}
+
+  @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B"]}
+ 
+  @{thm tag_str_STAR_def[where ?L1.0="A"]}
 *}
 
 
 section {* Conclusion and Related Work *}
 
 text {*
-  In this paper we took the view that a regular language as one where there exists 
+  In this paper we took the view that a regular language is one where there exists 
   a regular expression that matches all its strings. For us it was important to find 
   out how far we can push this point of view. Having formalised the Myhill-Nerode
-  theorem means pushed very far. Having the Myhill-Nerode theorem means we can 
+  theorem means pushed quite far. Having the Myhill-Nerode theorem means we can 
   formalise much of the textbook results in this subject. 
 
 
diff -r 212bfa431fa5 -r 79b37ef9505f tphols-2011/myhill.pdf
Binary file tphols-2011/myhill.pdf has changed