--- 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