diff -r a8a442ba0dbf -r e93760534354 Myhill_1.thy
--- a/Myhill_1.thy	Thu May 12 05:55:05 2011 +0000
+++ b/Myhill_1.thy	Wed May 18 19:54:43 2011 +0000
@@ -1,315 +1,10 @@
 theory Myhill_1
-imports Main Folds 
-        "~~/src/HOL/Library/While_Combinator"
+imports Main Folds Regular
+        "~~/src/HOL/Library/While_Combinator" 
 begin
 
-section {* Preliminary definitions *}
-
-types lang = "string set"
-
-
-text {*  Sequential composition of two languages *}
-
-definition 
-  Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100)
-where 
-  "A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"
-
-
-text {* Some properties of operator @{text ";;"}. *}
-
-lemma seq_add_left:
-  assumes a: "A = B"
-  shows "C ;; A = C ;; B"
-using a by simp
-
-lemma seq_union_distrib_right:
-  shows "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)"
-unfolding Seq_def by auto
-
-lemma seq_union_distrib_left:
-  shows "C ;; (A \<union> B) = (C ;; A) \<union> (C ;; B)"
-unfolding Seq_def by  auto
-
-lemma seq_intro:
-  assumes a: "x \<in> A" "y \<in> B"
-  shows "x @ y \<in> A ;; B "
-using a by (auto simp: Seq_def)
-
-lemma seq_assoc:
-  shows "(A ;; B) ;; C = A ;; (B ;; C)"
-unfolding Seq_def
-apply(auto)
-apply(blast)
-by (metis append_assoc)
-
-lemma seq_empty [simp]:
-  shows "A ;; {[]} = A"
-  and   "{[]} ;; A = A"
-by (simp_all add: Seq_def)
-
-
-text {* Power and Star of a language *}
-
-fun 
-  pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100)
-where
-  "A \<up> 0 = {[]}"
-| "A \<up> (Suc n) =  A ;; (A \<up> n)" 
-
-definition
-  Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102)
-where
-  "A\<star> \<equiv> (\<Union>n. A \<up> n)"
-
-
-lemma star_start[intro]:
-  shows "[] \<in> A\<star>"
-proof -
-  have "[] \<in> A \<up> 0" by auto
-  then show "[] \<in> A\<star>" unfolding Star_def by blast
-qed
-
-lemma star_step [intro]:
-  assumes a: "s1 \<in> A" 
-  and     b: "s2 \<in> A\<star>"
-  shows "s1 @ s2 \<in> A\<star>"
-proof -
-  from b obtain n where "s2 \<in> A \<up> n" unfolding Star_def by auto
-  then have "s1 @ s2 \<in> A \<up> (Suc n)" using a by (auto simp add: Seq_def)
-  then show "s1 @ s2 \<in> A\<star>" unfolding Star_def by blast
-qed
-
-lemma star_induct[consumes 1, case_names start step]:
-  assumes a: "x \<in> A\<star>" 
-  and     b: "P []"
-  and     c: "\<And>s1 s2. \<lbrakk>s1 \<in> A; s2 \<in> A\<star>; P s2\<rbrakk> \<Longrightarrow> P (s1 @ s2)"
-  shows "P x"
-proof -
-  from a obtain n where "x \<in> A \<up> n" unfolding Star_def by auto
-  then show "P x"
-    by (induct n arbitrary: x)
-       (auto intro!: b c simp add: Seq_def Star_def)
-qed
-    
-lemma star_intro1:
-  assumes a: "x \<in> A\<star>"
-  and     b: "y \<in> A\<star>"
-  shows "x @ y \<in> A\<star>"
-using a b
-by (induct rule: star_induct) (auto)
-
-lemma star_intro2: 
-  assumes a: "y \<in> A"
-  shows "y \<in> A\<star>"
-proof -
-  from a have "y @ [] \<in> A\<star>" by blast
-  then show "y \<in> A\<star>" by simp
-qed
-
-lemma star_intro3:
-  assumes a: "x \<in> A\<star>"
-  and     b: "y \<in> A"
-  shows "x @ y \<in> A\<star>"
-using a b by (blast intro: star_intro1 star_intro2)
-
-lemma star_cases:
-  shows "A\<star> =  {[]} \<union> A ;; A\<star>"
-proof
-  { fix x
-    have "x \<in> A\<star> \<Longrightarrow> x \<in> {[]} \<union> A ;; A\<star>"
-      unfolding Seq_def
-    by (induct rule: star_induct) (auto)
-  }
-  then show "A\<star> \<subseteq> {[]} \<union> A ;; A\<star>" by auto
-next
-  show "{[]} \<union> A ;; A\<star> \<subseteq> A\<star>"
-    unfolding Seq_def by auto
-qed
-
-lemma star_decom: 
-  assumes a: "x \<in> A\<star>" "x \<noteq> []"
-  shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>"
-using a
-by (induct rule: star_induct) (blast)+
-
-lemma
-  shows seq_Union_left:  "B ;; (\<Union>n. A \<up> n) = (\<Union>n. B ;; (A \<up> n))"
-  and   seq_Union_right: "(\<Union>n. A \<up> n) ;; B = (\<Union>n. (A \<up> n) ;; B)"
-unfolding Seq_def by auto
-
-lemma seq_pow_comm:
-  shows "A ;; (A \<up> n) = (A \<up> n) ;; A"
-by (induct n) (simp_all add: seq_assoc[symmetric])
-
-lemma seq_star_comm:
-  shows "A ;; A\<star> = A\<star> ;; A"
-unfolding Star_def seq_Union_left
-unfolding seq_pow_comm seq_Union_right 
-by simp
-
-
-text {* Two lemmas about the length of strings in @{text "A \<up> n"} *}
-
-lemma pow_length:
-  assumes a: "[] \<notin> A"
-  and     b: "s \<in> A \<up> Suc n"
-  shows "n < length s"
-using b
-proof (induct n arbitrary: s)
-  case 0
-  have "s \<in> A \<up> Suc 0" by fact
-  with a have "s \<noteq> []" by auto
-  then show "0 < length s" by auto
-next
-  case (Suc n)
-  have ih: "\<And>s. s \<in> A \<up> Suc n \<Longrightarrow> n < length s" by fact
-  have "s \<in> A \<up> Suc (Suc n)" by fact
-  then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A \<up> Suc n"
-    by (auto simp add: Seq_def)
-  from ih ** have "n < length s2" by simp
-  moreover have "0 < length s1" using * a by auto
-  ultimately show "Suc n < length s" unfolding eq 
-    by (simp only: length_append)
-qed
-
-lemma seq_pow_length:
-  assumes a: "[] \<notin> A"
-  and     b: "s \<in> B ;; (A \<up> Suc n)"
-  shows "n < length s"
-proof -
-  from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A \<up> Suc n"
-    unfolding Seq_def by auto
-  from * have " n < length s2" by (rule pow_length[OF a])
-  then show "n < length s" using eq by simp
-qed
-
-
-section {* A modified version of Arden's lemma *}
-
-text {*  A helper lemma for Arden *}
-
-lemma arden_helper:
-  assumes eq: "X = X ;; A \<union> B"
-  shows "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"
-proof (induct n)
-  case 0 
-  show "X = X ;; (A \<up> Suc 0) \<union> (\<Union>(m::nat)\<in>{0..0}. B ;; (A \<up> m))"
-    using eq by simp
-next
-  case (Suc n)
-  have ih: "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" by fact
-  also have "\<dots> = (X ;; A \<union> B) ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" using eq by simp
-  also have "\<dots> = X ;; (A \<up> Suc (Suc n)) \<union> (B ;; (A \<up> Suc n)) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"
-    by (simp add: seq_union_distrib_right seq_assoc)
-  also have "\<dots> = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))"
-    by (auto simp add: le_Suc_eq)
-  finally show "X = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))" .
-qed
-
-theorem arden:
-  assumes nemp: "[] \<notin> A"
-  shows "X = X ;; A \<union> B \<longleftrightarrow> X = B ;; A\<star>"
-proof
-  assume eq: "X = B ;; A\<star>"
-  have "A\<star> = {[]} \<union> A\<star> ;; A" 
-    unfolding seq_star_comm[symmetric]
-    by (rule star_cases)
-  then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"
-    by (rule seq_add_left)
-  also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"
-    unfolding seq_union_distrib_left by simp
-  also have "\<dots> = B \<union> (B ;; A\<star>) ;; A" 
-    by (simp only: seq_assoc)
-  finally show "X = X ;; A \<union> B" 
-    using eq by blast 
-next
-  assume eq: "X = X ;; A \<union> B"
-  { fix n::nat
-    have "B ;; (A \<up> n) \<subseteq> X" using arden_helper[OF eq, of "n"] by auto }
-  then have "B ;; A\<star> \<subseteq> X" 
-    unfolding Seq_def Star_def UNION_def by auto
-  moreover
-  { fix s::string
-    obtain k where "k = length s" by auto
-    then have not_in: "s \<notin> X ;; (A \<up> Suc k)" 
-      using seq_pow_length[OF nemp] by blast
-    assume "s \<in> X"
-    then have "s \<in> X ;; (A \<up> Suc k) \<union> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))"
-      using arden_helper[OF eq, of "k"] by auto
-    then have "s \<in> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))" using not_in by auto
-    moreover
-    have "(\<Union>m\<in>{0..k}. B ;; (A \<up> m)) \<subseteq> (\<Union>n. B ;; (A \<up> n))" by auto
-    ultimately 
-    have "s \<in> B ;; A\<star>" 
-      unfolding seq_Union_left Star_def by auto }
-  then have "X \<subseteq> B ;; A\<star>" by auto
-  ultimately 
-  show "X = B ;; A\<star>" by simp
-qed
-
-
-section {* Regular Expressions *}
-
-datatype rexp =
-  NULL
-| EMPTY
-| CHAR char
-| SEQ rexp rexp
-| ALT rexp rexp
-| STAR rexp
-
-
-text {* 
-  The function @{text L} is overloaded, with the idea that @{text "L x"} 
-  evaluates to the language represented by the object @{text x}.
-*}
-
-consts L:: "'a \<Rightarrow> lang"
-
-overloading L_rexp \<equiv> "L::  rexp \<Rightarrow> lang"
-begin
-fun
-  L_rexp :: "rexp \<Rightarrow> lang"
-where
-    "L_rexp (NULL) = {}"
-  | "L_rexp (EMPTY) = {[]}"
-  | "L_rexp (CHAR c) = {[c]}"
-  | "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)"
-  | "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"
-  | "L_rexp (STAR r) = (L_rexp r)\<star>"
-end
-
-
-text {* ALT-combination of a set or regulare expressions *}
-
-abbreviation
-  Setalt  ("\<Uplus>_" [1000] 999) 
-where
-  "\<Uplus>A \<equiv> folds ALT NULL A"
-
-text {* 
-  For finite sets, @{term Setalt} is preserved under @{term L}.
-*}
-
-lemma folds_alt_simp [simp]:
-  fixes rs::"rexp set"
-  assumes a: "finite rs"
-  shows "L (\<Uplus>rs) = \<Union> (L ` rs)"
-unfolding folds_def
-apply(rule set_eqI)
-apply(rule someI2_ex)
-apply(rule_tac finite_imp_fold_graph[OF a])
-apply(erule fold_graph.induct)
-apply(auto)
-done
-
-
 section {* Direction @{text "finite partition \<Rightarrow> regular language"} *}
 
-
-text {* Just a technical lemma for collections and pairs *}
-
 lemma Pair_Collect[simp]:
   shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
 by simp
@@ -321,26 +16,17 @@
 where
   "\<approx>A \<equiv> {(x, y).  (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)}"
 
-text {* 
-  Among the equivalence clases of @{text "\<approx>A"}, the set @{text "finals A"} 
-  singles out those which contains the strings from @{text A}.
-*}
-
 definition 
   finals :: "lang \<Rightarrow> lang set"
 where
   "finals A \<equiv> {\<approx>A `` {s} | s . s \<in> A}"
 
-
 lemma lang_is_union_of_finals: 
   shows "A = \<Union> finals A"
 unfolding finals_def
 unfolding Image_def
 unfolding str_eq_rel_def
-apply(auto)
-apply(drule_tac x = "[]" in spec)
-apply(auto)
-done
+by (auto) (metis append_Nil2)
 
 lemma finals_in_partitions:
   shows "finals A \<subseteq> (UNIV // \<approx>A)"
@@ -351,28 +37,32 @@
 
 text {* The two kinds of terms in the rhs of equations. *}
 
-datatype rhs_item = 
+datatype rhs_trm = 
    Lam "rexp"            (* Lambda-marker *)
  | Trn "lang" "rexp"     (* Transition *)
 
 
-overloading L_rhs_item \<equiv> "L:: rhs_item \<Rightarrow> lang"
+overloading L_rhs_trm \<equiv> "L:: rhs_trm \<Rightarrow> lang"
 begin
-  fun L_rhs_item:: "rhs_item \<Rightarrow> lang"
+  fun L_rhs_trm:: "rhs_trm \<Rightarrow> lang"
   where
-    "L_rhs_item (Lam r) = L r" 
-  | "L_rhs_item (Trn X r) = X ;; L r"
+    "L_rhs_trm (Lam r) = L r" 
+  | "L_rhs_trm (Trn X r) = X ;; L r"
 end
 
-overloading L_rhs \<equiv> "L:: rhs_item set \<Rightarrow> lang"
+overloading L_rhs \<equiv> "L:: rhs_trm set \<Rightarrow> lang"
 begin
-   fun L_rhs:: "rhs_item set \<Rightarrow> lang"
+   fun L_rhs:: "rhs_trm set \<Rightarrow> lang"
    where 
      "L_rhs rhs = \<Union> (L ` rhs)"
 end
 
+lemma L_rhs_set:
+  shows "L {Trn X r | r. P r} = \<Union>{L (Trn X r) | r. P r}"
+by (auto simp del: L_rhs_trm.simps)
+
 lemma L_rhs_union_distrib:
-  fixes A B::"rhs_item set"
+  fixes A B::"rhs_trm set"
   shows "L A \<union> L B = L (A \<union> B)"
 by simp
 
@@ -398,60 +88,34 @@
   "Init CS \<equiv> {(X, Init_rhs CS X) | X.  X \<in> CS}"
 
 
-
 section {* Arden Operation on equations *}
 
-text {*
-  The function @{text "attach_rexp r item"} SEQ-composes @{text r} to the
-  right of every rhs-item.
-*}
-
 fun 
-  append_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"
+  Append_rexp :: "rexp \<Rightarrow> rhs_trm \<Rightarrow> rhs_trm"
 where
-  "append_rexp r (Lam rexp)   = Lam (SEQ rexp r)"
-| "append_rexp r (Trn X rexp) = Trn X (SEQ rexp r)"
+  "Append_rexp r (Lam rexp)   = Lam (SEQ rexp r)"
+| "Append_rexp r (Trn X rexp) = Trn X (SEQ rexp r)"
 
 
 definition
-  "append_rhs_rexp rhs rexp \<equiv> (append_rexp rexp) ` rhs"
+  "Append_rexp_rhs rhs rexp \<equiv> (Append_rexp rexp) ` rhs"
 
 definition 
   "Arden X rhs \<equiv> 
-     append_rhs_rexp (rhs - {Trn X r | r. Trn X r \<in> rhs}) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))"
+     Append_rexp_rhs (rhs - {Trn X r | r. Trn X r \<in> rhs}) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))"
 
 
 section {* Substitution Operation on equations *}
 
-text {* 
-  Suppose and equation @{text "X = xrhs"}, @{text "Subst"} substitutes 
-  all occurences of @{text "X"} in @{text "rhs"} by @{text "xrhs"}.
-*}
-
 definition 
   "Subst rhs X xrhs \<equiv> 
-        (rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> (append_rhs_rexp xrhs (\<Uplus> {r. Trn X r \<in> rhs}))"
-
-text {*
-  @{text "eqs_subst ES X xrhs"} substitutes @{text xrhs} into every 
-  equation of the equational system @{text ES}.
-*}
-
-types esystem = "(lang \<times> rhs_item set) set"
+        (rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> (Append_rexp_rhs xrhs (\<Uplus> {r. Trn X r \<in> rhs}))"
 
 definition
-  Subst_all :: "esystem \<Rightarrow> lang \<Rightarrow> rhs_item set \<Rightarrow> esystem"
+  Subst_all :: "(lang \<times> rhs_trm set) set \<Rightarrow> lang \<Rightarrow> rhs_trm set \<Rightarrow> (lang \<times> rhs_trm set) set"
 where
   "Subst_all ES X xrhs \<equiv> {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
 
-text {*
-  The following term @{text "remove ES Y yrhs"} removes the equation
-  @{text "Y = yrhs"} from equational system @{text "ES"} by replacing
-  all occurences of @{text "Y"} by its definition (using @{text "eqs_subst"}).
-  The @{text "Y"}-definition is made non-recursive using Arden's transformation
-  @{text "arden_variate Y yrhs"}.
-  *}
-
 definition
   "Remove ES X xrhs \<equiv> 
       Subst_all  (ES - {(X, xrhs)}) X (Arden X xrhs)"
@@ -459,11 +123,6 @@
 
 section {* While-combinator *}
 
-text {*
-  The following term @{text "Iter X ES"} represents one iteration in the while loop.
-  It arbitrarily chooses a @{text "Y"} different from @{text "X"} to remove.
-*}
-
 definition 
   "Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y
                 in Remove ES Y yrhs)"
@@ -476,64 +135,28 @@
 unfolding Iter_def using assms
 by (rule_tac a="(Y, yrhs)" in someI2) (auto)
 
-
-text {*
-  The following term @{text "Reduce X ES"} repeatedly removes characteriztion equations
-  for unknowns other than @{text "X"} until one is left.
-*}
-
 abbreviation
   "Cond ES \<equiv> card ES \<noteq> 1"
 
 definition 
   "Solve X ES \<equiv> while Cond (Iter X) ES"
 
-text {*
-  Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"},
-  the induction principle @{thm [source] while_rule} is used to proved the desired properties
-  of @{text "Solve X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
-  in terms of a series of auxilliary predicates:
-*}
 
 section {* Invariants *}
 
-text {* Every variable is defined at most once in @{text ES}. *}
-
 definition 
-  "distinct_equas ES \<equiv> 
+  "distinctness ES \<equiv> 
      \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
 
-
-text {* 
-  Every equation in @{text ES} (represented by @{text "(X, rhs)"}) 
-  is valid, i.e. @{text "X = L rhs"}.
-*}
-
 definition 
-  "sound_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
-
-text {*
-  @{text "ardenable rhs"} requires regular expressions occuring in 
-  transitional items of @{text "rhs"} do not contain empty string. This is 
-  necessary for the application of Arden's transformation to @{text "rhs"}.
-*}
+  "soundness ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
 
 definition 
   "ardenable rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"
 
-text {*
-  The following @{text "ardenable_all ES"} requires that Arden's transformation 
-  is applicable to every equation of equational system @{text "ES"}.
-*}
-
 definition 
   "ardenable_all ES \<equiv> \<forall>(X, rhs) \<in> ES. ardenable rhs"
 
-
-text {* 
-  @{text "finite_rhs ES"} requires every equation in @{text "rhs"} 
-  be finite.
-*}
 definition
   "finite_rhs ES \<equiv> \<forall>(X, rhs) \<in> ES. finite rhs"
 
@@ -541,56 +164,42 @@
   "finite_rhs ES = (\<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs)"
 unfolding finite_rhs_def by auto
 
-text {*
-  @{text "classes_of rhs"} returns all variables (or equivalent classes)
-  occuring in @{text "rhs"}.
-  *}
-
 definition 
   "rhss rhs \<equiv> {X | X r. Trn X r \<in> rhs}"
 
-text {*
-  @{text "lefts_of ES"} returns all variables defined by an 
-  equational system @{text "ES"}.
-*}
 definition
   "lhss ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"
 
-text {*
-  The following @{text "valid_eqs ES"} requires that every variable occuring 
-  on the right hand side of equations is already defined by some equation in @{text "ES"}.
-*}
 definition 
-  "valid_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. rhss rhs \<subseteq> lhss ES"
+  "validity ES \<equiv> \<forall>(X, rhs) \<in> ES. rhss rhs \<subseteq> lhss ES"
+
+lemma rhss_union_distrib:
+  shows "rhss (A \<union> B) = rhss A \<union> rhss B"
+by (auto simp add: rhss_def)
+
+lemma lhss_union_distrib:
+  shows "lhss (A \<union> B) = lhss A \<union> lhss B"
+by (auto simp add: lhss_def)
 
 
-text {*
-  The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints.
-  *}
 definition 
   "invariant ES \<equiv> finite ES
                 \<and> finite_rhs ES
-                \<and> sound_eqs ES 
-                \<and> distinct_equas ES 
+                \<and> soundness ES 
+                \<and> distinctness ES 
                 \<and> ardenable_all ES 
-                \<and> valid_eqs ES"
+                \<and> validity ES"
 
 
 lemma invariantI:
-  assumes "sound_eqs ES" "finite ES" "distinct_equas ES" "ardenable_all ES" 
-          "finite_rhs ES" "valid_eqs ES"
+  assumes "soundness ES" "finite ES" "distinctness ES" "ardenable_all ES" 
+          "finite_rhs ES" "validity ES"
   shows "invariant ES"
 using assms by (simp add: invariant_def)
 
+
 subsection {* The proof of this direction *}
 
-subsubsection {* Basic properties *}
-
-text {*
-  The following are some basic properties of the above definitions.
-*}
-
-
 lemma finite_Trn:
   assumes fin: "finite rhs"
   shows "finite {r. Trn Y r \<in> rhs}"
@@ -618,55 +227,30 @@
     done
 qed
 
-lemma rexp_of_empty:
-  assumes finite: "finite rhs"
-  and nonempty: "ardenable rhs"
-  shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
-using finite nonempty ardenable_def
-using finite_Trn[OF finite]
-by auto
-
-lemma lang_of_rexp_of:
+lemma rhs_trm_soundness:
   assumes finite:"finite rhs"
   shows "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
 proof -
   have "finite {r. Trn X r \<in> rhs}" 
     by (rule finite_Trn[OF finite]) 
-  then show ?thesis
-    apply(auto simp add: Seq_def)
-    apply(rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI)
-    apply(auto)
-    apply(rule_tac x= "Trn X xa" in exI)
-    apply(auto simp add: Seq_def)
-    done
+  then show "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
+    by (simp only: L_rhs_set L_rhs_trm.simps) (auto simp add: Seq_def)
 qed
 
-lemma lang_of_append:
-  "L (append_rexp r rhs_item) = L rhs_item ;; L r"
-by (induct rule: append_rexp.induct)
+lemma lang_of_append_rexp:
+  "L (Append_rexp r rhs_trm) = L rhs_trm ;; L r"
+by (induct rule: Append_rexp.induct)
    (auto simp add: seq_assoc)
 
-lemma lang_of_append_rhs:
-  "L (append_rhs_rexp rhs r) = L rhs ;; L r"
-unfolding append_rhs_rexp_def
-by (auto simp add: Seq_def lang_of_append)
+lemma lang_of_append_rexp_rhs:
+  "L (Append_rexp_rhs rhs r) = L rhs ;; L r"
+unfolding Append_rexp_rhs_def
+by (auto simp add: Seq_def lang_of_append_rexp)
 
-lemma rhss_union_distrib:
-  shows "rhss (A \<union> B) = rhss A \<union> rhss B"
-by (auto simp add: rhss_def)
-
-lemma lhss_union_distrib:
-  shows "lhss (A \<union> B) = lhss A \<union> lhss B"
-by (auto simp add: lhss_def)
 
 
 subsubsection {* Intialization *}
 
-text {*
-  The following several lemmas until @{text "init_ES_satisfy_invariant"} shows that
-  the initial equational system satisfies invariant @{text "invariant"}.
-*}
-
 lemma defined_by_str:
   assumes "s \<in> X" "X \<in> UNIV // \<approx>A" 
   shows "X = \<approx>A `` {s}"
@@ -702,42 +286,37 @@
   show "X \<subseteq> L rhs"
   proof
     fix x
-    assume "(1)": "x \<in> X"
-    show "x \<in> L rhs"          
-    proof (cases "x = []")
-      assume empty: "x = []"
-      thus ?thesis using X_in_eqs "(1)"
-        by (auto simp: Init_def Init_rhs_def)
-    next
-      assume not_empty: "x \<noteq> []"
-      then obtain clist c where decom: "x = clist @ [c]"
-        by (case_tac x rule:rev_cases, auto)
-      have "X \<in> UNIV // \<approx>A" using X_in_eqs by (auto simp:Init_def)
-      then obtain Y 
-        where "Y \<in> UNIV // \<approx>A" 
-        and "Y ;; {[c]} \<subseteq> X"
-        and "clist \<in> Y"
-        using decom "(1)" every_eqclass_has_transition by blast
-      hence 
-        "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // \<approx>A \<and> Y \<Turnstile>c\<Rightarrow> X}"
+    assume in_X: "x \<in> X"
+    { assume empty: "x = []"
+      then have "x \<in> L rhs" using X_in_eqs in_X
+	unfolding Init_def Init_rhs_def
+        by auto
+    }
+    moreover
+    { assume not_empty: "x \<noteq> []"
+      then obtain s c where decom: "x = s @ [c]"
+	using rev_cases by blast
+      have "X \<in> UNIV // \<approx>A" using X_in_eqs unfolding Init_def by auto
+      then obtain Y where "Y \<in> UNIV // \<approx>A" "Y ;; {[c]} \<subseteq> X" "s \<in> Y"
+        using decom in_X every_eqclass_has_transition by blast
+      then have "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // \<approx>A \<and> Y \<Turnstile>c\<Rightarrow> X}"
         unfolding transition_def
-	using "(1)" decom
-        by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)
-      thus ?thesis using X_in_eqs "(1)"	
-        by (simp add: Init_def Init_rhs_def)
-    qed
+	using decom by (force simp add: Seq_def)
+      then have "x \<in> L rhs" using X_in_eqs in_X
+	unfolding Init_def Init_rhs_def by simp
+    }
+    ultimately show "x \<in> L rhs" by blast
   qed
 next
   show "L rhs \<subseteq> X" using X_in_eqs
-    by (auto simp:Init_def Init_rhs_def transition_def) 
+    unfolding Init_def Init_rhs_def transition_def
+    by auto 
 qed
 
 lemma test:
   assumes X_in_eqs: "(X, rhs) \<in> Init (UNIV // \<approx>A)"
   shows "X = \<Union> (L `  rhs)"
-using assms
-by (drule_tac l_eq_r_in_eqs) (simp)
-
+using assms l_eq_r_in_eqs by (simp)
 
 lemma finite_Init_rhs: 
   assumes finite: "finite CS"
@@ -759,31 +338,26 @@
   assumes finite_CS: "finite (UNIV // \<approx>A)"
   shows "invariant (Init (UNIV // \<approx>A))"
 proof (rule invariantI)
-  show "sound_eqs (Init (UNIV // \<approx>A))"
-    unfolding sound_eqs_def 
+  show "soundness (Init (UNIV // \<approx>A))"
+    unfolding soundness_def 
     using l_eq_r_in_eqs by auto
   show "finite (Init (UNIV // \<approx>A))" using finite_CS
     unfolding Init_def by simp
-  show "distinct_equas (Init (UNIV // \<approx>A))"     
-    unfolding distinct_equas_def Init_def by simp
+  show "distinctness (Init (UNIV // \<approx>A))"     
+    unfolding distinctness_def Init_def by simp
   show "ardenable_all (Init (UNIV // \<approx>A))"
     unfolding ardenable_all_def Init_def Init_rhs_def ardenable_def
    by auto 
   show "finite_rhs (Init (UNIV // \<approx>A))"
     using finite_Init_rhs[OF finite_CS]
     unfolding finite_rhs_def Init_def by auto
-  show "valid_eqs (Init (UNIV // \<approx>A))"
-    unfolding valid_eqs_def Init_def Init_rhs_def rhss_def lhss_def
+  show "validity (Init (UNIV // \<approx>A))"
+    unfolding validity_def Init_def Init_rhs_def rhss_def lhss_def
     by auto
 qed
 
 subsubsection {* Interation step *}
 
-text {*
-  From this point until @{text "iteration_step"}, 
-  the correctness of the iteration step @{text "Iter X ES"} is proved.
-*}
-
 lemma Arden_keeps_eq:
   assumes l_eq_r: "X = L rhs"
   and not_empty: "ardenable rhs"
@@ -791,40 +365,39 @@
   shows "X = L (Arden X rhs)"
 proof -
   def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})"
-  def b \<equiv> "rhs - {Trn X r | r. Trn X r \<in> rhs}"
-  def B \<equiv> "L b" 
-  have "X = B ;; A\<star>"
-  proof -
-    have "L rhs = L({Trn X r | r. Trn X r \<in> rhs} \<union> b)" by (auto simp: b_def)
-    also have "\<dots> = X ;; A \<union> B"
-      unfolding L_rhs_union_distrib[symmetric]
-      by (simp only: lang_of_rexp_of finite B_def A_def)
-    finally show ?thesis
-      apply(rule_tac arden[THEN iffD1])
-      apply(simp (no_asm) add: A_def)
-      using finite_Trn[OF finite] not_empty
-      apply(simp add: ardenable_def)
-      using l_eq_r
-      apply(simp)
-      done
-  qed
-  moreover have "L (Arden X rhs) = B ;; A\<star>"
-    by (simp only:Arden_def L_rhs_union_distrib lang_of_append_rhs 
-                  B_def A_def b_def L_rexp.simps seq_union_distrib_left)
-   ultimately show ?thesis by simp
+  def b \<equiv> "{Trn X r | r. Trn X r \<in> rhs}"
+  def B \<equiv> "L (rhs - b)"
+  have not_empty2: "[] \<notin> A" 
+    using finite_Trn[OF finite] not_empty
+    unfolding A_def ardenable_def by simp
+  have "X = L rhs" using l_eq_r by simp
+  also have "\<dots> = L (b \<union> (rhs - b))" unfolding b_def by auto
+  also have "\<dots> = L b \<union> B" unfolding B_def by (simp only: L_rhs_union_distrib)
+  also have "\<dots> = X ;; A \<union> B"
+    unfolding b_def
+    unfolding rhs_trm_soundness[OF finite]
+    unfolding A_def
+    by blast
+  finally have "X = X ;; A \<union> B" . 
+  then have "X = B ;; A\<star>"
+    by (simp add: arden[OF not_empty2])
+  also have "\<dots> = L (Arden X rhs)"
+    unfolding Arden_def A_def B_def b_def
+    by (simp only: lang_of_append_rexp_rhs L_rexp.simps)
+  finally show "X = L (Arden X rhs)" by simp
 qed 
 
-lemma append_keeps_finite:
-  "finite rhs \<Longrightarrow> finite (append_rhs_rexp rhs r)"
-by (auto simp:append_rhs_rexp_def)
+lemma Append_keeps_finite:
+  "finite rhs \<Longrightarrow> finite (Append_rexp_rhs rhs r)"
+by (auto simp:Append_rexp_rhs_def)
 
 lemma Arden_keeps_finite:
   "finite rhs \<Longrightarrow> finite (Arden X rhs)"
-by (auto simp:Arden_def append_keeps_finite)
+by (auto simp:Arden_def Append_keeps_finite)
 
-lemma append_keeps_nonempty:
-  "ardenable rhs \<Longrightarrow> ardenable (append_rhs_rexp rhs r)"
-apply (auto simp:ardenable_def append_rhs_rexp_def)
+lemma Append_keeps_nonempty:
+  "ardenable rhs \<Longrightarrow> ardenable (Append_rexp_rhs rhs r)"
+apply (auto simp:ardenable_def Append_rexp_rhs_def)
 by (case_tac x, auto simp:Seq_def)
 
 lemma nonempty_set_sub:
@@ -837,12 +410,12 @@
 
 lemma Arden_keeps_nonempty:
   "ardenable rhs \<Longrightarrow> ardenable (Arden X rhs)"
-by (simp only:Arden_def append_keeps_nonempty nonempty_set_sub)
+by (simp only:Arden_def Append_keeps_nonempty nonempty_set_sub)
 
 
 lemma Subst_keeps_nonempty:
   "\<lbrakk>ardenable rhs; ardenable xrhs\<rbrakk> \<Longrightarrow> ardenable (Subst rhs X xrhs)"
-by (simp only:Subst_def append_keeps_nonempty  nonempty_set_union nonempty_set_sub)
+by (simp only: Subst_def Append_keeps_nonempty nonempty_set_union nonempty_set_sub)
 
 lemma Subst_keeps_eq:
   assumes substor: "X = L xrhs"
@@ -850,7 +423,7 @@
   shows "L (Subst rhs X xrhs) = L rhs" (is "?Left = ?Right")
 proof-
   def A \<equiv> "L (rhs - {Trn X r | r. Trn X r \<in> rhs})"
-  have "?Left = A \<union> L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs}))"
+  have "?Left = A \<union> L (Append_rexp_rhs xrhs (\<Uplus>{r. Trn X r \<in> rhs}))"
     unfolding Subst_def
     unfolding L_rhs_union_distrib[symmetric]
     by (simp add: A_def)
@@ -862,14 +435,14 @@
       unfolding L_rhs_union_distrib
       by simp
   qed
-  moreover have "L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs})) = L ({Trn X r | r. Trn X r \<in> rhs})" 
-    using finite substor  by (simp only:lang_of_append_rhs lang_of_rexp_of)
+  moreover have "L (Append_rexp_rhs xrhs (\<Uplus>{r. Trn X r \<in> rhs})) = L ({Trn X r | r. Trn X r \<in> rhs})" 
+    using finite substor by (simp only: lang_of_append_rexp_rhs rhs_trm_soundness)
   ultimately show ?thesis by simp
 qed
 
 lemma Subst_keeps_finite_rhs:
   "\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (Subst rhs Y yrhs)"
-by (auto simp:Subst_def append_keeps_finite)
+by (auto simp: Subst_def Append_keeps_finite)
 
 lemma Subst_all_keeps_finite:
   assumes finite: "finite ES"
@@ -889,8 +462,8 @@
 by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def)
 
 lemma append_rhs_keeps_cls:
-  "rhss (append_rhs_rexp rhs r) = rhss rhs"
-apply (auto simp:rhss_def append_rhs_rexp_def)
+  "rhss (Append_rexp_rhs rhs r) = rhss rhs"
+apply (auto simp:rhss_def Append_rexp_rhs_def)
 apply (case_tac xa, auto simp:image_def)
 by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+)
 
@@ -909,9 +482,9 @@
 apply (simp only:Subst_def append_rhs_keeps_cls rhss_union_distrib)
 by (auto simp:rhss_def)
 
-lemma Subst_all_keeps_valid_eqs:
-  assumes sc: "valid_eqs (ES \<union> {(Y, yrhs)})"        (is "valid_eqs ?A")
-  shows "valid_eqs (Subst_all ES Y (Arden Y yrhs))"  (is "valid_eqs ?B")
+lemma Subst_all_keeps_validity:
+  assumes sc: "validity (ES \<union> {(Y, yrhs)})"        (is "validity ?A")
+  shows "validity (Subst_all ES Y (Arden Y yrhs))"  (is "validity ?B")
 proof -
   { fix X xrhs'
     assume "(X, xrhs') \<in> ?B"
@@ -930,16 +503,16 @@
           thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls)
         qed
         moreover have "rhss xrhs \<subseteq> lhss ES \<union> {Y}" using X_in sc
-          apply (simp only:valid_eqs_def lhss_union_distrib)
+          apply (simp only:validity_def lhss_union_distrib)
           by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lhss_def)
         moreover have "rhss (Arden Y yrhs) \<subseteq> lhss ES \<union> {Y}" 
           using sc 
-          by (auto simp add:Arden_removes_cl valid_eqs_def lhss_def)
+          by (auto simp add:Arden_removes_cl validity_def lhss_def)
         ultimately show ?thesis by auto
       qed
       ultimately show ?thesis by simp
     qed
-  } thus ?thesis by (auto simp only:Subst_all_def valid_eqs_def)
+  } thus ?thesis by (auto simp only:Subst_all_def validity_def)
 qed
 
 lemma Subst_all_satisfies_invariant:
@@ -947,12 +520,12 @@
   shows "invariant (Subst_all ES Y (Arden Y yrhs))"
 proof (rule invariantI)
   have Y_eq_yrhs: "Y = L yrhs" 
-    using invariant_ES by (simp only:invariant_def sound_eqs_def, blast)
+    using invariant_ES by (simp only:invariant_def soundness_def, blast)
    have finite_yrhs: "finite yrhs" 
     using invariant_ES by (auto simp:invariant_def finite_rhs_def)
   have nonempty_yrhs: "ardenable yrhs" 
     using invariant_ES by (auto simp:invariant_def ardenable_all_def)
-  show "sound_eqs (Subst_all ES Y (Arden Y yrhs))"
+  show "soundness (Subst_all ES Y (Arden Y yrhs))"
   proof -
     have "Y = L (Arden Y yrhs)" 
       using Y_eq_yrhs invariant_ES finite_yrhs
@@ -963,19 +536,19 @@
       apply(auto)
       done
     thus ?thesis using invariant_ES
-      unfolding invariant_def finite_rhs_def2 sound_eqs_def Subst_all_def
+      unfolding invariant_def finite_rhs_def2 soundness_def Subst_all_def
       by (auto simp add: Subst_keeps_eq simp del: L_rhs.simps)
   qed
   show "finite (Subst_all ES Y (Arden Y yrhs))" 
     using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
-  show "distinct_equas (Subst_all ES Y (Arden Y yrhs))" 
+  show "distinctness (Subst_all ES Y (Arden Y yrhs))" 
     using invariant_ES 
-    unfolding distinct_equas_def Subst_all_def invariant_def by auto
+    unfolding distinctness_def Subst_all_def invariant_def by auto
   show "ardenable_all (Subst_all ES Y (Arden Y yrhs))"
   proof - 
     { fix X rhs
       assume "(X, rhs) \<in> ES"
-      hence "ardenable rhs"  using prems invariant_ES  
+      hence "ardenable rhs"  using invariant_ES  
         by (auto simp add:invariant_def ardenable_all_def)
       with nonempty_yrhs 
       have "ardenable (Subst rhs Y (Arden Y yrhs))"
@@ -996,8 +569,8 @@
     ultimately show ?thesis 
       by (simp add:Subst_all_keeps_finite_rhs)
   qed
-  show "valid_eqs (Subst_all ES Y (Arden Y yrhs))"
-    using invariant_ES Subst_all_keeps_valid_eqs by (simp add:invariant_def)
+  show "validity (Subst_all ES Y (Arden Y yrhs))"
+    using invariant_ES Subst_all_keeps_validity by (simp add:invariant_def)
 qed
 
 lemma Remove_in_card_measure:
@@ -1049,7 +622,7 @@
     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
     using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
   then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"  
-    using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
+    using X_in_ES Inv_ES unfolding invariant_def distinctness_def
     by auto
   then show "(Iter X ES, ES) \<in> measure card" 
   apply(rule IterI2)
@@ -1069,7 +642,7 @@
     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
     using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
   then have "(Y, yrhs) \<in> ES" "X \<noteq> Y" 
-    using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
+    using X_in_ES Inv_ES unfolding invariant_def distinctness_def
     by auto
   then show "invariant (Iter X ES)" 
   proof(rule IterI2)
@@ -1078,7 +651,6 @@
     then have "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto
     then show "invariant (Remove ES Y yrhs)" unfolding Remove_def
       using Inv_ES
-      thm Subst_all_satisfies_invariant
       by (rule_tac Subst_all_satisfies_invariant) (simp) 
   qed
 qed
@@ -1091,10 +663,10 @@
 proof -
   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
   then obtain Y yrhs 
-    where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
+    where "(Y, yrhs) \<in> ES" "(X, xrhs) \<noteq> (Y, yrhs)" 
     using Cnd X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
   then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"  
-    using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
+    using X_in_ES Inv_ES unfolding invariant_def distinctness_def
     by auto
   then show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" 
   apply(rule IterI2)
@@ -1159,7 +731,7 @@
 
   def A \<equiv> "Arden X xrhs"
   have "rhss xrhs \<subseteq> {X}" using Inv_ES 
-    unfolding valid_eqs_def invariant_def rhss_def lhss_def
+    unfolding validity_def invariant_def rhss_def lhss_def
     by auto
   then have "rhss A = {}" unfolding A_def 
     by (simp add: Arden_removes_cl)
@@ -1170,7 +742,7 @@
     using Arden_keeps_finite by auto
   then have fin: "finite {r. Lam r \<in> A}" by (rule finite_Lam)
 
-  have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def
+  have "X = L xrhs" using Inv_ES unfolding invariant_def soundness_def
     by simp
   then have "X = L A" using Inv_ES 
     unfolding A_def invariant_def ardenable_all_def finite_rhs_def