--- a/Myhill_1.thy Wed Feb 16 12:25:53 2011 +0000
+++ b/Myhill_1.thy Thu Feb 17 11:42:16 2011 +0000
@@ -512,21 +512,21 @@
"sound_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
text {*
- @{text "rhs_nonempty rhs"} requires regular expressions occuring in
+ @{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
- "rhs_nonempty rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"
+ "ardenable rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"
text {*
- The following @{text "ardenable ES"} requires that Arden's transformation
+ The following @{text "ardenable_all ES"} requires that Arden's transformation
is applicable to every equation of equational system @{text "ES"}.
*}
definition
- "ardenable ES \<equiv> \<forall>(X, rhs) \<in> ES. rhs_nonempty rhs"
+ "ardenable_all ES \<equiv> \<forall>(X, rhs) \<in> ES. ardenable rhs"
text {*
@@ -571,12 +571,12 @@
\<and> finite_rhs ES
\<and> sound_eqs ES
\<and> distinct_equas ES
- \<and> ardenable ES
+ \<and> ardenable_all ES
\<and> valid_eqs ES"
lemma invariantI:
- assumes "sound_eqs ES" "finite ES" "distinct_equas ES" "ardenable ES"
+ assumes "sound_eqs ES" "finite ES" "distinct_equas ES" "ardenable_all ES"
"finite_rhs ES" "valid_eqs ES"
shows "invariant ES"
using assms by (simp add: invariant_def)
@@ -619,9 +619,9 @@
lemma rexp_of_empty:
assumes finite: "finite rhs"
- and nonempty: "rhs_nonempty rhs"
+ and nonempty: "ardenable rhs"
shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
-using finite nonempty rhs_nonempty_def
+using finite nonempty ardenable_def
using finite_Trn[OF finite]
by auto
@@ -765,8 +765,8 @@
unfolding Init_def by simp
show "distinct_equas (Init (UNIV // \<approx>A))"
unfolding distinct_equas_def Init_def by simp
- show "ardenable (Init (UNIV // \<approx>A))"
- unfolding ardenable_def Init_def Init_rhs_def rhs_nonempty_def
+ 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]
@@ -785,7 +785,7 @@
lemma Arden_keeps_eq:
assumes l_eq_r: "X = L rhs"
- and not_empty: "[] \<notin> L (\<Uplus>{r. Trn X r \<in> rhs})"
+ and not_empty: "ardenable rhs"
and finite: "finite rhs"
shows "X = L (Arden X rhs)"
proof -
@@ -799,9 +799,11 @@
unfolding L_rhs_union_distrib[symmetric]
by (simp only: lang_of_rexp_of finite B_def A_def)
finally show ?thesis
- using l_eq_r not_empty
apply(rule_tac arden[THEN iffD1])
- apply(simp add: A_def)
+ 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
@@ -820,25 +822,25 @@
by (auto simp:Arden_def append_keeps_finite)
lemma append_keeps_nonempty:
- "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (append_rhs_rexp rhs r)"
-apply (auto simp:rhs_nonempty_def append_rhs_rexp_def)
+ "ardenable rhs \<Longrightarrow> ardenable (append_rhs_rexp rhs r)"
+apply (auto simp:ardenable_def append_rhs_rexp_def)
by (case_tac x, auto simp:Seq_def)
lemma nonempty_set_sub:
- "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (rhs - A)"
-by (auto simp:rhs_nonempty_def)
+ "ardenable rhs \<Longrightarrow> ardenable (rhs - A)"
+by (auto simp:ardenable_def)
lemma nonempty_set_union:
- "\<lbrakk>rhs_nonempty rhs; rhs_nonempty rhs'\<rbrakk> \<Longrightarrow> rhs_nonempty (rhs \<union> rhs')"
-by (auto simp:rhs_nonempty_def)
+ "\<lbrakk>ardenable rhs; ardenable rhs'\<rbrakk> \<Longrightarrow> ardenable (rhs \<union> rhs')"
+by (auto simp:ardenable_def)
lemma Arden_keeps_nonempty:
- "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (Arden X rhs)"
+ "ardenable rhs \<Longrightarrow> ardenable (Arden X rhs)"
by (simp only:Arden_def append_keeps_nonempty nonempty_set_sub)
lemma Subst_keeps_nonempty:
- "\<lbrakk>rhs_nonempty rhs; rhs_nonempty xrhs\<rbrakk> \<Longrightarrow> rhs_nonempty (Subst rhs X xrhs)"
+ "\<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)
lemma Subst_keeps_eq:
@@ -869,19 +871,16 @@
by (auto simp:Subst_def append_keeps_finite)
lemma Subst_all_keeps_finite:
- assumes finite:"finite (ES:: (string set \<times> rhs_item set) set)"
+ assumes finite: "finite ES"
shows "finite (Subst_all ES Y yrhs)"
proof -
- have "finite {(Ya, Subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \<in> ES}"
- (is "finite ?A")
- proof-
- def eqns' \<equiv> "{(Ya::lang, yrhsa) | Ya yrhsa. (Ya, yrhsa) \<in> ES}"
- def h \<equiv> "\<lambda>(Ya::lang, yrhsa). (Ya, Subst yrhsa Y yrhs)"
- have "finite (h ` eqns')" using finite h_def eqns'_def by auto
- moreover have "?A = h ` eqns'" by (auto simp:h_def eqns'_def)
- ultimately show ?thesis by auto
- qed
- thus ?thesis by (simp add:Subst_all_def)
+ def eqns \<equiv> "{(X::lang, rhs) |X rhs. (X, rhs) \<in> ES}"
+ def h \<equiv> "\<lambda>(X::lang, rhs). (X, Subst rhs Y yrhs)"
+ have "finite (h ` eqns)" using finite h_def eqns_def by auto
+ moreover
+ have "Subst_all ES Y yrhs = h ` eqns" unfolding h_def eqns_def Subst_all_def by auto
+ ultimately
+ show "finite (Subst_all ES Y yrhs)" by simp
qed
lemma Subst_all_keeps_finite_rhs:
@@ -910,10 +909,9 @@
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")
-proof-
+ 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")
+proof -
{ fix X xrhs'
assume "(X, xrhs') \<in> ?B"
then obtain xrhs
@@ -924,8 +922,7 @@
have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def)
moreover have "rhss xrhs' \<subseteq> lhss ES"
proof-
- have "rhss xrhs' \<subseteq>
- rhss xrhs \<union> rhss (Arden Y yrhs) - {Y}"
+ have "rhss xrhs' \<subseteq> rhss xrhs \<union> rhss (Arden Y yrhs) - {Y}"
proof-
have "Y \<notin> rhss (Arden Y yrhs)"
using Arden_removes_cl by simp
@@ -952,38 +949,38 @@
using invariant_ES by (simp only:invariant_def sound_eqs_def, blast)
have finite_yrhs: "finite yrhs"
using invariant_ES by (auto simp:invariant_def finite_rhs_def)
- have nonempty_yrhs: "rhs_nonempty yrhs"
- using invariant_ES by (auto simp:invariant_def ardenable_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))"
- proof-
+ 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_def rhs_nonempty_def
+ 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 sound_eqs_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))"
- using invariant_ES
- by (auto simp:distinct_equas_def Subst_all_def invariant_def)
- show "ardenable (Subst_all ES Y (Arden Y yrhs))"
+ using invariant_ES
+ unfolding distinct_equas_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 "rhs_nonempty rhs" using prems invariant_ES
- by (auto simp add:invariant_def ardenable_def)
+ hence "ardenable rhs" using prems invariant_ES
+ by (auto simp add:invariant_def ardenable_all_def)
with nonempty_yrhs
- have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))"
+ have "ardenable (Subst rhs Y (Arden Y yrhs))"
by (simp add:nonempty_yrhs
Subst_keeps_nonempty Arden_keeps_nonempty)
- } thus ?thesis by (auto simp add:ardenable_def Subst_all_def)
+ } thus ?thesis by (auto simp add:ardenable_all_def Subst_all_def)
qed
show "finite_rhs (Subst_all ES Y (Arden Y yrhs))"
proof-
@@ -1079,7 +1076,9 @@
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 by (rule_tac Subst_all_satisfies_invariant) (simp)
+ using Inv_ES
+ thm Subst_all_satisfies_invariant
+ by (rule_tac Subst_all_satisfies_invariant) (simp)
qed
qed
@@ -1124,14 +1123,14 @@
by (auto simp add: iteration_step_invariant iteration_step_ex) }
moreover
{ fix ES
- assume "Inv ES" and "\<not> Cond ES"
- then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant ES"
- unfolding Inv_def invariant_def
- apply (auto, rule_tac x = rhs in exI)
- apply (auto dest!: card_Suc_Diff1 simp: card_eq_0_iff)
- done
- then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant {(X, rhs')}"
- by auto }
+ assume inv: "Inv ES" and not_crd: "\<not>Cond ES"
+ from inv obtain rhs where "(X, rhs) \<in> ES" unfolding Inv_def by auto
+ moreover
+ from not_crd have "card ES = 1" by simp
+ ultimately
+ have "ES = {(X, rhs)}" by (auto simp add: card_Suc_eq)
+ then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant {(X, rhs')}" using inv
+ unfolding Inv_def by auto }
moreover
have "wf (measure card)" by simp
moreover
@@ -1173,7 +1172,7 @@
have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def
by simp
then have "X = L A" using Inv_ES
- unfolding A_def invariant_def ardenable_def finite_rhs_def rhs_nonempty_def
+ 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
then have "X = L (\<Uplus>{r. Lam r \<in> A})" using fin by auto
--- a/Paper/Paper.thy Wed Feb 16 12:25:53 2011 +0000
+++ b/Paper/Paper.thy Thu Feb 17 11:42:16 2011 +0000
@@ -176,7 +176,7 @@
upon functions in order to represent \emph{finite} automata. The best is
probably to resort to more advanced reasoning frameworks, such as \emph{locales}
or \emph{type classes},
- which are not avaiable in \emph{all} HOL-based theorem provers.
+ which are \emph{not} avaiable in all HOL-based theorem provers.
Because of these problems to do with representing automata, there seems
to be no substantial formalisation of automata theory and regular languages
@@ -198,7 +198,7 @@
\end{definition}
\noindent
- The reason is that regular expressions, unlike graphs, matrices and functons, can
+ The reason is that regular expressions, unlike graphs, matrices and functions, can
be easily defined as inductive datatype. Consequently a corresponding reasoning
infrastructure comes for free. This has recently been exploited in HOL4 with a formalisation
of regular expression matching based on derivatives \cite{OwensSlind08} and
@@ -346,10 +346,10 @@
of such a regular expression and therefore we use Isabelle/HOL's @{const "fold_graph"} and Hilbert's
@{text "\<epsilon>"} to define @{term "\<Uplus>rs"}. This operation, roughly speaking, folds @{const ALT} over the
set @{text rs} with @{const NULL} for the empty set. We can prove that for a finite set @{text rs}
-
- \begin{center}
- @{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}
- \end{center}
+ %
+ \begin{equation}\label{uplus}
+ \mbox{@{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}}
+ \end{equation}
\noindent
holds, whereby @{text "\<calL> ` rs"} stands for the
@@ -423,11 +423,11 @@
which means that if we concatenate the character @{text c} to the end of all
strings in the equivalence class @{text Y}, we obtain a subset of
@{text X}. Note that we do not define an automaton here, we merely relate two sets
- (with respect to a character). In our concrete example we have
+ (with the help of a character). In our concrete example we have
@{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<Rightarrow> X\<^isub>3"} with @{text d} being any
other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>d\<Rightarrow> X\<^isub>3"} for any @{text d}.
- Next we build an \emph{initial} equational system that
+ Next we build an \emph{initial equational system} that
contains an equation for each equivalence class. Suppose we have
the equivalence classes @{text "X\<^isub>1,\<dots>,X\<^isub>n"}, there must be one and only one that
contains the empty string @{text "[]"} (since equivalence classes are disjoint).
@@ -446,7 +446,7 @@
where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"}
stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow>
X\<^isub>i"}. There can only be
- finitely many such terms in a right-hand side since there are only finitely many
+ finitely many such terms in a right-hand side since by assumption there are only finitely many
equivalence classes and only finitely many characters. The term @{text
"\<lambda>(EMPTY)"} in the first equation acts as a marker for the equivalence class
containing @{text "[]"}.\footnote{Note that we mark, roughly speaking, the
@@ -522,10 +522,10 @@
In order to transform an equational system into solved form, we have two
operations: one that takes an equation of the form @{text "X = rhs"} and removes
- any recursive occurences of @{text X} in the @{text rhs} using our variant of Arden's
+ any recursive occurrences of @{text X} in the @{text rhs} using our variant of Arden's
Lemma. The other operation takes an equation @{text "X = rhs"}
and substitutes @{text X} throughout the rest of the equational system
- adjusting the remaining regular expressions approriately. To define this adjustment
+ adjusting the remaining regular expressions appropriately. To define this adjustment
we define the \emph{append-operation} taking a term and a regular expression as argument
\begin{center}
@@ -537,22 +537,40 @@
We lift this operation to entire right-hand sides of equations, written as
@{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. With this we can define
the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as:
-
- \begin{center}
- \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
+ %
+ \begin{equation}\label{arden_def}
+ \mbox{\begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}
@{thm (lhs) Arden_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\
& & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\
& & @{text "r' ="} & @{term "STAR (\<Uplus> {r. Trn X r \<in> rhs})"}\\
& & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "append_rhs_rexp rhs' r'"}}\\
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \end{equation}
\noindent
In this definition, we first delete all terms of the form @{text "(X, r)"} from @{text rhs};
- then we calculate the combinded regular expressions for all @{text r} coming
+ then we calculate the combined regular expressions for all @{text r} coming
from the deleted @{text "(X, r)"}, and take the @{const STAR} of it;
finally we append this regular expression to @{text rhs'}. It can be easily seen
- that this operation mimics Arden's lemma on the level of equations.
+ that this operation mimics Arden's lemma on the level of equations. To ensure
+ the non-emptiness condition of Arden's lemma we say that a right-hand side is
+ \emph{ardenable} provided
+
+ \begin{center}
+ @{thm ardenable_def}
+ \end{center}
+
+ \noindent
+ This allows us to prove
+
+ \begin{lemma}\label{ardenable}
+ If @{text "X = \<Union>\<calL> ` rhs"},
+ @{thm (prem 2) Arden_keeps_eq} and
+ @{thm (prem 3) Arden_keeps_eq}, then
+ @{text "X = \<Union>\<calL> ` (Arden X rhs)"}
+ \end{lemma}
+
+ \noindent
The \emph{substituion-operation} takes an equation
of the form @{text "X = xrhs"} and substitutes it into the right-hand side @{text rhs}.
@@ -566,17 +584,17 @@
\end{center}
\noindent
- We again delete first all occurence of @{text "(X, r)"} in @{text rhs}; we then calculate
+ We again delete first all occurrence of @{text "(X, r)"} in @{text rhs}; we then calculate
the regular expression corresponding to the deleted terms; finally we append this
regular expression to @{text "xrhs"} and union it up with @{text rhs'}. When we use
the substitution operation we will arrange it so that @{text "xrhs"} does not contain
- any occurence of @{text X}.
+ any occurrence of @{text X}.
With these two operation in place, we can define the operation that removes one equation
from an equational systems @{text ES}. The operation @{const Subst_all}
substitutes an equation @{text "X = xrhs"} throughout an equational system @{text ES};
@{const Remove} then completely removes such an equation from @{text ES} by substituting
- it to the rest of the equational system, but first eliminating all recursive occurences
+ it to the rest of the equational system, but first eliminating all recursive occurrences
of @{text X} by applying @{const Arden} to @{text "xrhs"}.
\begin{center}
@@ -587,7 +605,7 @@
\end{center}
\noindent
- Finially, we can define how an equational system should be solved. For this
+ Finally, we can define how an equational system should be solved. For this
we will need to iterate the process of eliminating equations until only one equation
will be left in the system. However, we not just want to have any equation
as being the last one, but the one involving the equivalence class for
@@ -607,10 +625,10 @@
\end{center}
\noindent
- The last definition we need applies @{term Iter} over and over again until a condition
- @{text COND} is \emph{not} satisfied anymore. The condition states that there
- are more than one equation left in the equational system @{text ES}. For this
- we use Isabelle/HOL's @{text while}-operator as follows:
+ The last definition we need applies @{term Iter} over and over until a condition
+ @{text Cond} is \emph{not} satisfied anymore. The condition states that there
+ are more than one equation left in the equational system @{text ES}. To solve
+ an equational system we use Isabelle/HOL's @{text while}-operator as follows:
\begin{center}
@{thm Solve_def}
@@ -626,18 +644,17 @@
the equivalence class @{text X} and the initial equational system
@{term "Init (UNIV // \<approx>A)"} from
\eqref{initcs} using the principle:
-
-
- \begin{center}
- \begin{tabular}{l}
+ %
+ \begin{equation}\label{whileprinciple}
+ \mbox{\begin{tabular}{l}
@{term "invariant (Init (UNIV // \<approx>A))"} \\
@{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> invariant (Iter X ES)"}\\
@{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> card (Iter X ES) < card ES"}\\
@{term "\<forall>ES. invariant ES \<and> \<not> Cond ES \<longrightarrow> P ES"}\\
\hline
\multicolumn{1}{c}{@{term "P (Solve X (Init (UNIV // \<approx>A)))"}}
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \end{equation}
\noindent
This principle states that given an invariant (which we will specify below)
@@ -662,7 +679,7 @@
& @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\
& @{text "\<and>"} & @{thm (rhs) distinct_equas_def}\\
& & & @{text "(distinctness)"}\\
- & @{text "\<and>"} & @{thm (rhs) ardenable_def} & @{text "(ardenable)"}\\
+ & @{text "\<and>"} & @{thm (rhs) ardenable_all_def} & @{text "(ardenable)"}\\
& @{text "\<and>"} & @{thm (rhs) valid_eqs_def} & @{text "(validity)"}\\
\end{tabular}
\end{center}
@@ -672,28 +689,20 @@
and number of terms in each equation); the second makes sure the ``meaning'' of the
equations is preserved under our transformations. The other properties are a bit more
technical, but are needed to get our proof through. Distinctness states that every
- equation in the system is distinct; @{text "ardenable"} ensures that we can always
- apply the arden operation. For this we have to make sure that in every @{text rhs},
- terms of the form @{term "Trn Y r"} cannot have a regular expresion that matches the
- empty string. Therefore @{text "rhs_nonempty"} is defined as
-
- \begin{center}
- @{thm rhs_nonempty_def}
- \end{center}
-
- \noindent
+ equation in the system is distinct. Ardenable ensures that we can always
+ apply the arden operation.
The last property states that every @{text rhs} can only contain equivalence classes
for which there is an equation. Therefore @{text lhss} is just the set containing
the first components of an equational system,
while @{text "rhss"} collects all equivalence classes @{text X} in the terms of the
- form @{term "Trn X r"} (that means @{thm (lhs) lhss_def}~@{text "\<equiv> {X | (X, rhs) \<in> ES}"}
- and @{thm (lhs) rhss_def}~@{text "\<equiv> {X | (X, r) \<in> rhs}"}).
+ form @{term "Trn X r"}. That means @{thm (lhs) lhss_def}~@{text "\<equiv> {X | (X, rhs) \<in> ES}"}
+ and @{thm (lhs) rhss_def}~@{text "\<equiv> {X | (X, r) \<in> rhs}"}.
- It is straightforward to prove that the inital equational system satisfies the
+ It is straightforward to prove that the initial equational system satisfies the
invariant.
- \begin{lemma}
+ \begin{lemma}\label{invzero}
@{thm[mode=IfThen] Init_ES_satisfies_invariant}
\end{lemma}
@@ -701,26 +710,47 @@
Finiteness is given by the assumption and the way how we set up the
initial equational system. Soundness is proved in Lem.~\ref{inv}. Distinctness
follows from the fact that the equivalence classes are disjoint. The ardenable
- property also follows from the setup of the equational system as does
+ property also follows from the setup of the equational system, as does
validity.\qed
\end{proof}
- \begin{lemma}
+ \begin{lemma}\label{iterone}
@{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
\end{lemma}
\begin{proof}
- ???
+ This boils down to choosing an equation @{text "Y = yrhs"} to be eliminated
+ and to show that @{term "Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"}
+ preserves the invariant.
+ We prove this as follows:
+
+ \begin{center}
+ @{text "\<forall> ES."} @{thm (prem 1) Subst_all_satisfies_invariant} implies
+ @{thm (concl) Subst_all_satisfies_invariant}
+ \end{center}
+
+ \noindent
+ Finiteness is straightforward, as @{const Subst} and @{const Arden} operations
+ keep the equational system finite. These operation also preserve soundness
+ distinctness (we proved soundness for @{const Arden} in Lem.~\ref{ardenable}).
+ The property Ardenable is clearly preserved because the append-operation
+ cannot make a regular expression to match the empty string. Validity is
+ given because @{const Arden} removes an equivalence class from @{text yrhs}
+ and then @{const Subst_all} removes @{text Y} from the equational system.
+ Having proved the implication above, we can replace @{text "ES"} with @{text "ES - {(Y, yrhs)}"}
+ which matches with our proof-obligation of @{const "Subst_all"}. Since
+ \mbox{@{term "ES = ES - {(Y, yrhs)} \<union> {(Y, yrhs)}"}}, we can use our assumption
+ to complete the proof.\qed
\end{proof}
- \begin{lemma}
+ \begin{lemma}\label{itertwo}
@{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
\end{lemma}
\begin{proof}
By assumption we know that @{text "ES"} is finite and has more than one element.
Therefore there must be an element @{term "(Y, yrhs) \<in> ES"} with
- @{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distictness property we can infer
+ @{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distinctness property we can infer
that @{term "Y \<noteq> X"}. We further know that @{text "Remove ES Y yrhs"}
removes the equation @{text "Y = yrhs"} from the system, and therefore
the cardinality of @{const Iter} strictly decreases.\qed
@@ -733,7 +763,24 @@
\end{lemma}
\begin{proof}
- ???
+ In order to prove this lemma using \eqref{whileprinciple}, we have to use a slightly
+ stronger invariant since Lem.~\ref{iterone} and \ref{itertwo} have the precondition
+ that @{term "(X, rhs) \<in> ES"} for some @{text rhs}. This precondition is needed
+ in order to choose in the @{const Iter}-step an equation that is not \mbox{@{term "X = rhs"}}.
+ Therefore our invariant is cannot be just @{term "invariant ES"}, but must be
+ @{term "invariant ES \<and> (\<exists>rhs. (X, rhs) \<in> ES)"}. By assumption
+ @{thm (prem 2) Solve} and Lem.~\ref{invzero}, the more general invariant holds for
+ the initial equational system. This is premise 1 of~\eqref{whileprinciple}.
+ Premise 2 is given by Lem.~\ref{iterone} and the fact that @{const Iter} might
+ modify the @{text rhs} in the equation @{term "X = rhs"}, but does not remove it.
+ Premise 3 of~\eqref{whileprinciple} is by Lem.~\ref{itertwo}. Now in premise 4
+ we like to show that there exists a @{text rhs} such that @{term "ES = {(X, rhs)}"}
+ and that @{text "invariant {(X, rhs)}"} holds, provided the condition @{text "Cond"}
+ does not hols. By the stronger invariant we know there exists such a @{text "rhs"}
+ with @{term "(X, rhs) \<in> ES"}. Because @{text Cond} is not true, we know the cardinality
+ of @{text ES} is @{text 1}. This means @{text "ES"} must actually be the equation @{text "X = rhs"},
+ for which the invariant holds. This allows us to conclude that
+ @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"} and @{term "invariant {(X, rhs)}"} hold.\qed
\end{proof}
\noindent
@@ -750,7 +797,7 @@
and that the invariant holds for this equation. That means we
know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the
- invariant and Lem.~???. Using the validity property for the equation @{text "X = rhs"},
+ invariant and Lem.\ref{ardenable}. Using the validity property for the equation @{text "X = rhs"},
we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the arden operation
removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
That means @{term "Arden X rhs"} can only consist of terms of the form @{term "Lam r"}.
@@ -765,7 +812,7 @@
\begin{proof}[of Thm.~\ref{myhillnerodeone}]
By Lem.~\ref{every_eqcl_has_reg} we know that there exists a regular language for
every equivalence class in @{term "UNIV // \<approx>A"}. Since @{text "finals A"} is
- a subset of @{term "UNIV // \<approx>A"}, we also know that for every equvalence class
+ a subset of @{term "UNIV // \<approx>A"}, we also know that for every equivalence class
in @{term "finals A"} there exists a regular language. Moreover by assumption
we know that @{term "finals A"} must be finite, and therefore there must be a finite
set of regular expressions @{text "rs"} such that