regexp: comparison Myhill

equal deleted inserted replaced

-:a8a442ba0dbf
+:e93760534354
 theory Myhill_1
-imports Main Folds
+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
 definition
 str_eq_rel :: "lang \<Rightarrow> (string \<times> string) set" ("\<approx>_" [100] 100)
 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)
+by (auto) (metis append_Nil2)
-apply(drule_tac x = "[]" in spec)
-apply(auto)
-done
 lemma finals_in_partitions:
 shows "finals A \<subseteq> (UNIV // \<approx>A)"
 unfolding finals_def quotient_def
 by auto
 section {* Equational systems *}
 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_trm (Lam r) = L r"
-| "L_rhs_item (Trn X r) = X ;; 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
 definition
 "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 (Lam rexp)   = Lam (SEQ rexp r)"
-| "append_rexp r (Trn X rexp) = Trn X (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}))"
+(rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> (Append_rexp_rhs 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"
 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)"
 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)"
 and     "\<And>Y yrhs. \<lbrakk>(Y, yrhs) \<in> ES; X \<noteq> Y\<rbrakk> \<Longrightarrow> Q (Remove ES Y yrhs)"
 shows "Q (Iter X ES)"
 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
+"distinctness ES \<equiv>
-definition
-"distinct_equas ES \<equiv>
 \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
+definition
-text {*
+"soundness ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
-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"}.
-*}
 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"
 lemma finite_rhs_def2:
 "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 {*
+definition
-The following @{text "valid_eqs ES"} requires that every variable occuring
+"validity ES \<equiv> \<forall>(X, rhs) \<in> ES. rhss rhs \<subseteq> lhss ES"
-on the right hand side of equations is already defined by some equation in @{text "ES"}.
-*}
+lemma rhss_union_distrib:
-definition
+shows "rhss (A \<union> B) = rhss A \<union> rhss B"
-"valid_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. rhss rhs \<subseteq> lhss ES"
+by (auto simp add: rhss_def)
+lemma lhss_union_distrib:
-text {*
+shows "lhss (A \<union> B) = lhss A \<union> lhss B"
-The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints.
+by (auto simp add: lhss_def)
-*}
 definition
 "invariant ES \<equiv> finite ES
 \<and> finite_rhs ES
-\<and> sound_eqs ES
+\<and> soundness ES
-\<and> distinct_equas 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"
+assumes "soundness ES" "finite ES" "distinctness ES" "ardenable_all ES"
-"finite_rhs ES" "valid_eqs 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}"
 proof -
 apply(erule finite_imageD)
 apply(auto simp add: inj_on_def)
 done
 qed
-lemma rexp_of_empty:
+lemma rhs_trm_soundness:
-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:
 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
+then show "L ({Trn X r| r. Trn X r \<in> rhs}) = X ;; (L (\<Uplus>{r. Trn X r \<in> rhs}))"
-apply(auto simp add: Seq_def)
+by (simp only: L_rhs_set L_rhs_trm.simps) (auto simp add: Seq_def)
-apply(rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI)
+qed
-apply(auto)
-apply(rule_tac x= "Trn X xa" in exI)
+lemma lang_of_append_rexp:
-apply(auto simp add: Seq_def)
+"L (Append_rexp r rhs_trm) = L rhs_trm ;; L r"
-done
+by (induct rule: Append_rexp.induct)
-qed
-lemma lang_of_append:
-"L (append_rexp r rhs_item) = L rhs_item ;; L r"
-by (induct rule: append_rexp.induct)
 (auto simp add: seq_assoc)
-lemma lang_of_append_rhs:
+lemma lang_of_append_rexp_rhs:
-"L (append_rhs_rexp rhs r) = L rhs ;; L r"
+"L (Append_rexp_rhs rhs r) = L rhs ;; L r"
-unfolding append_rhs_rexp_def
+unfolding Append_rexp_rhs_def
-by (auto simp add: Seq_def lang_of_append)
+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}"
 using assms
 shows "X = L rhs"
 proof
 show "X \<subseteq> L rhs"
 proof
 fix x
-assume "(1)": "x \<in> X"
+assume in_X: "x \<in> X"
-show "x \<in> L rhs"
+{ assume empty: "x = []"
-proof (cases "x = []")
+then have "x \<in> L rhs" using X_in_eqs in_X
-assume empty: "x = []"
+	unfolding Init_def Init_rhs_def
-thus ?thesis using X_in_eqs "(1)"
+by auto
-by (auto simp: Init_def Init_rhs_def)
+}
-next
+moreover
-assume not_empty: "x \<noteq> []"
+{ assume not_empty: "x \<noteq> []"
-then obtain clist c where decom: "x = clist @ [c]"
+then obtain s c where decom: "x = s @ [c]"
-by (case_tac x rule:rev_cases, auto)
+	using rev_cases by blast
-have "X \<in> UNIV // \<approx>A" using X_in_eqs by (auto simp:Init_def)
+have "X \<in> UNIV // \<approx>A" using X_in_eqs unfolding Init_def by auto
-then obtain Y
+then obtain Y where "Y \<in> UNIV // \<approx>A" "Y ;; {[c]} \<subseteq> X" "s \<in> Y"
-where "Y \<in> UNIV // \<approx>A"
+using decom in_X every_eqclass_has_transition by blast
-and "Y ;; {[c]} \<subseteq> X"
+then have "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // \<approx>A \<and> Y \<Turnstile>c\<Rightarrow> 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}"
 unfolding transition_def
-	using "(1)" decom
+	using decom by (force simp add: Seq_def)
-by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)
+then have "x \<in> L rhs" using X_in_eqs in_X
-thus ?thesis using X_in_eqs "(1)"
+	unfolding Init_def Init_rhs_def by simp
-by (simp add: Init_def Init_rhs_def)
+}
-qed
+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
+using assms l_eq_r_in_eqs by (simp)
-by (drule_tac l_eq_r_in_eqs) (simp)
 lemma finite_Init_rhs:
 assumes finite: "finite CS"
 shows "finite (Init_rhs CS X)"
 proof-
 lemma Init_ES_satisfies_invariant:
 assumes finite_CS: "finite (UNIV // \<approx>A)"
 shows "invariant (Init (UNIV // \<approx>A))"
 proof (rule invariantI)
-show "sound_eqs (Init (UNIV // \<approx>A))"
+show "soundness (Init (UNIV // \<approx>A))"
-unfolding sound_eqs_def
+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))"
+show "distinctness (Init (UNIV // \<approx>A))"
-unfolding distinct_equas_def Init_def by simp
+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))"
+show "validity (Init (UNIV // \<approx>A))"
-unfolding valid_eqs_def Init_def Init_rhs_def rhss_def lhss_def
+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"
 and finite: "finite rhs"
 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> "{Trn X r | r. Trn X r \<in> rhs}"
-def B \<equiv> "L b"
+def B \<equiv> "L (rhs - b)"
-have "X = B ;; A\<star>"
+have not_empty2: "[] \<notin> A"
-proof -
+using finite_Trn[OF finite] not_empty
-have "L rhs = L({Trn X r | r. Trn X r \<in> rhs} \<union> b)" by (auto simp: b_def)
+unfolding A_def ardenable_def by simp
-also have "\<dots> = X ;; A \<union> B"
+have "X = L rhs" using l_eq_r by simp
-unfolding L_rhs_union_distrib[symmetric]
+also have "\<dots> = L (b \<union> (rhs - b))" unfolding b_def by auto
-by (simp only: lang_of_rexp_of finite B_def A_def)
+also have "\<dots> = L b \<union> B" unfolding B_def by (simp only: L_rhs_union_distrib)
-finally show ?thesis
+also have "\<dots> = X ;; A \<union> B"
-apply(rule_tac arden[THEN iffD1])
+unfolding b_def
-apply(simp (no_asm) add: A_def)
+unfolding rhs_trm_soundness[OF finite]
-using finite_Trn[OF finite] not_empty
+unfolding A_def
-apply(simp add: ardenable_def)
+by blast
-using l_eq_r
+finally have "X = X ;; A \<union> B" .
-apply(simp)
+then have "X = B ;; A\<star>"
-done
+by (simp add: arden[OF not_empty2])
-qed
+also have "\<dots> = L (Arden X rhs)"
-moreover have "L (Arden X rhs) = B ;; A\<star>"
+unfolding Arden_def A_def B_def b_def
-by (simp only:Arden_def L_rhs_union_distrib lang_of_append_rhs
+by (simp only: lang_of_append_rexp_rhs L_rexp.simps)
-B_def A_def b_def L_rexp.simps seq_union_distrib_left)
+finally show "X = L (Arden X rhs)" by simp
-ultimately show ?thesis by simp
 qed
-lemma append_keeps_finite:
+lemma Append_keeps_finite:
-"finite rhs \<Longrightarrow> finite (append_rhs_rexp rhs r)"
+"finite rhs \<Longrightarrow> finite (Append_rexp_rhs rhs r)"
-by (auto simp:append_rhs_rexp_def)
+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:
+lemma Append_keeps_nonempty:
-"ardenable rhs \<Longrightarrow> ardenable (append_rhs_rexp rhs r)"
+"ardenable rhs \<Longrightarrow> ardenable (Append_rexp_rhs rhs r)"
-apply (auto simp:ardenable_def append_rhs_rexp_def)
+apply (auto simp:ardenable_def Append_rexp_rhs_def)
 by (case_tac x, auto simp:Seq_def)
 lemma nonempty_set_sub:
 "ardenable rhs \<Longrightarrow> ardenable (rhs - A)"
 by (auto simp:ardenable_def)
 "\<lbrakk>ardenable rhs; ardenable rhs'\<rbrakk> \<Longrightarrow> ardenable (rhs \<union> rhs')"
 by (auto simp:ardenable_def)
 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"
 and finite: "finite rhs"
 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)
 moreover have "?Right = A \<union> L ({Trn X r | r. Trn X r \<in> rhs})"
 proof-
 thus ?thesis
 unfolding A_def
 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})"
+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_rhs lang_of_rexp_of)
+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"
 shows "finite (Subst_all ES Y yrhs)"
 proof -
 lemma Subst_all_keeps_finite_rhs:
 "\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)"
 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"
+"rhss (Append_rexp_rhs rhs r) = rhss rhs"
-apply (auto simp:rhss_def append_rhs_rexp_def)
+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+)
 lemma Arden_removes_cl:
 "rhss (Arden Y yrhs) = rhss yrhs - {Y}"
 "X \<notin> rhss xrhs \<Longrightarrow>
 rhss (Subst rhs X xrhs) = rhss rhs \<union> rhss xrhs - {X}"
 apply (simp only:Subst_def append_rhs_keeps_cls rhss_union_distrib)
 by (auto simp:rhss_def)
-lemma Subst_all_keeps_valid_eqs:
+lemma Subst_all_keeps_validity:
-assumes sc: "valid_eqs (ES \<union> {(Y, yrhs)})"        (is "valid_eqs ?A")
+assumes sc: "validity (ES \<union> {(Y, yrhs)})"        (is "validity ?A")
-shows "valid_eqs (Subst_all ES Y (Arden Y yrhs))"  (is "valid_eqs ?B")
+shows "validity (Subst_all ES Y (Arden Y yrhs))"  (is "validity ?B")
 proof -
 { fix X xrhs'
 assume "(X, xrhs') \<in> ?B"
 then obtain xrhs
 where xrhs_xrhs': "xrhs' = Subst xrhs Y (Arden Y yrhs)"
 have "Y \<notin> rhss (Arden Y yrhs)"
 using Arden_removes_cl by simp
 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:
 assumes invariant_ES: "invariant (ES \<union> {(Y, yrhs)})"
 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
 using finite_Trn[OF finite_yrhs]
 apply(rule_tac Arden_keeps_eq)
 apply(simp_all)
 unfolding invariant_def ardenable_all_def ardenable_def
 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))"
 by (simp add:nonempty_yrhs
 Subst_keeps_nonempty Arden_keeps_nonempty)
 thus ?thesis using Arden_keeps_finite by simp
 qed
 ultimately show ?thesis
 by (simp add:Subst_all_keeps_finite_rhs)
 qed
-show "valid_eqs (Subst_all ES Y (Arden Y yrhs))"
+show "validity (Subst_all ES Y (Arden Y yrhs))"
-using invariant_ES Subst_all_keeps_valid_eqs by (simp add:invariant_def)
+using invariant_ES Subst_all_keeps_validity by (simp add:invariant_def)
 qed
 lemma Remove_in_card_measure:
 assumes finite: "finite ES"
 and     in_ES: "(X, rhs) \<in> ES"
 have fin: "finite ES" using Inv_ES unfolding invariant_def by simp
 then obtain Y yrhs
 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)
 apply(rule Remove_in_card_measure)
 apply(simp_all add: fin)
 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)"
 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)
 fix Y yrhs
 assume h: "(Y, yrhs) \<in> ES" "X \<noteq> Y"
 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
 lemma iteration_step_ex:
 and    Cnd: "Cond ES"
 shows "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)"
 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)
 unfolding Remove_def
 apply(rule Subst_all_cls_remains)
 obtain xrhs where Inv_ES: "invariant {(X, xrhs)}"
 using Solve by metis
 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)
 then have eq: "{Lam r | r. Lam r \<in> A} = A" unfolding rhss_def
 by (auto, case_tac x, auto)
 have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def
 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
 by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn)
 then have "X = L {Lam r | r. Lam r \<in> A}" using eq by simp

changeset 162	e93760534354
parent 149	e122cb146ecc
child 166	7743d2ad71d1