--- a/Myhill_1.thy Mon Feb 14 23:10:44 2011 +0000
+++ b/Myhill_1.thy Tue Feb 15 08:08:04 2011 +0000
@@ -509,7 +509,7 @@
*}
definition
- "valid_eqns ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
+ "sound_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
text {*
@{text "rhs_nonempty rhs"} requires regular expressions occuring in
@@ -546,7 +546,7 @@
*}
definition
- "classes_of rhs \<equiv> {X | X r. Trn X r \<in> rhs}"
+ "rhss rhs \<equiv> {X | X r. Trn X r \<in> rhs}"
text {*
@{text "lefts_of ES"} returns all variables defined by an
@@ -556,11 +556,11 @@
"lhss ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"
text {*
- The following @{text "self_contained ES"} requires that every variable occuring
+ 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
- "self_contained ES \<equiv> \<forall>(X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lhss ES"
+ "valid_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. rhss rhs \<subseteq> lhss ES"
text {*
@@ -569,15 +569,15 @@
definition
"invariant ES \<equiv> finite ES
\<and> finite_rhs ES
- \<and> valid_eqns ES
+ \<and> sound_eqs ES
\<and> distinct_equas ES
\<and> ardenable ES
- \<and> self_contained ES"
+ \<and> valid_eqs ES"
lemma invariantI:
- assumes "valid_eqns ES" "finite ES" "distinct_equas ES" "ardenable ES"
- "finite_rhs ES" "self_contained ES"
+ assumes "sound_eqs ES" "finite ES" "distinct_equas ES" "ardenable ES"
+ "finite_rhs ES" "valid_eqs ES"
shows "invariant ES"
using assms by (simp add: invariant_def)
@@ -650,9 +650,9 @@
unfolding append_rhs_rexp_def
by (auto simp add: Seq_def lang_of_append)
-lemma classes_of_union_distrib:
- shows "classes_of (A \<union> B) = classes_of A \<union> classes_of B"
-by (auto simp add: classes_of_def)
+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"
@@ -760,8 +760,8 @@
assumes finite_CS: "finite (UNIV // \<approx>A)"
shows "invariant (Init (UNIV // \<approx>A))"
proof (rule invariantI)
- show "valid_eqns (Init (UNIV // \<approx>A))"
- unfolding valid_eqns_def
+ show "sound_eqs (Init (UNIV // \<approx>A))"
+ unfolding sound_eqs_def
using l_eq_r_in_eqs by auto
show "finite (Init (UNIV // \<approx>A))" using finite_CS
unfolding Init_def by simp
@@ -773,8 +773,8 @@
show "finite_rhs (Init (UNIV // \<approx>A))"
using finite_Init_rhs[OF finite_CS]
unfolding finite_rhs_def Init_def by auto
- show "self_contained (Init (UNIV // \<approx>A))"
- unfolding self_contained_def Init_def Init_rhs_def classes_of_def lhss_def
+ show "valid_eqs (Init (UNIV // \<approx>A))"
+ unfolding valid_eqs_def Init_def Init_rhs_def rhss_def lhss_def
by auto
qed
@@ -891,59 +891,59 @@
by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def)
lemma append_rhs_keeps_cls:
- "classes_of (append_rhs_rexp rhs r) = classes_of rhs"
-apply (auto simp:classes_of_def append_rhs_rexp_def)
+ "rhss (append_rhs_rexp rhs r) = rhss rhs"
+apply (auto simp:rhss_def append_rhs_rexp_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:
- "classes_of (Arden Y yrhs) = classes_of yrhs - {Y}"
+ "rhss (Arden Y yrhs) = rhss yrhs - {Y}"
apply (simp add:Arden_def append_rhs_keeps_cls)
-by (auto simp:classes_of_def)
+by (auto simp:rhss_def)
lemma lhss_keeps_cls:
"lhss (Subst_all ES Y yrhs) = lhss ES"
by (auto simp:lhss_def Subst_all_def)
lemma Subst_updates_cls:
- "X \<notin> classes_of xrhs \<Longrightarrow>
- classes_of (Subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
-apply (simp only:Subst_def append_rhs_keeps_cls classes_of_union_distrib)
-by (auto simp:classes_of_def)
+ "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_self_contained:
- assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A")
- shows "self_contained (Subst_all ES Y (Arden Y yrhs))"
- (is "self_contained ?B")
+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-
{ fix X xrhs'
assume "(X, xrhs') \<in> ?B"
then obtain xrhs
where xrhs_xrhs': "xrhs' = Subst xrhs Y (Arden Y yrhs)"
and X_in: "(X, xrhs) \<in> ES" by (simp add:Subst_all_def, blast)
- have "classes_of xrhs' \<subseteq> lhss ?B"
+ have "rhss xrhs' \<subseteq> lhss ?B"
proof-
have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def)
- moreover have "classes_of xrhs' \<subseteq> lhss ES"
+ moreover have "rhss xrhs' \<subseteq> lhss ES"
proof-
- have "classes_of xrhs' \<subseteq>
- classes_of xrhs \<union> classes_of (Arden Y yrhs) - {Y}"
+ have "rhss xrhs' \<subseteq>
+ rhss xrhs \<union> rhss (Arden Y yrhs) - {Y}"
proof-
- have "Y \<notin> classes_of (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 "classes_of xrhs \<subseteq> lhss ES \<union> {Y}" using X_in sc
- apply (simp only:self_contained_def lhss_union_distrib)
+ moreover have "rhss xrhs \<subseteq> lhss ES \<union> {Y}" using X_in sc
+ apply (simp only:valid_eqs_def lhss_union_distrib)
by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lhss_def)
- moreover have "classes_of (Arden Y yrhs) \<subseteq> lhss ES \<union> {Y}"
+ moreover have "rhss (Arden Y yrhs) \<subseteq> lhss ES \<union> {Y}"
using sc
- by (auto simp add:Arden_removes_cl self_contained_def lhss_def)
+ by (auto simp add:Arden_removes_cl valid_eqs_def lhss_def)
ultimately show ?thesis by auto
qed
ultimately show ?thesis by simp
qed
- } thus ?thesis by (auto simp only:Subst_all_def self_contained_def)
+ } thus ?thesis by (auto simp only:Subst_all_def valid_eqs_def)
qed
lemma Subst_all_satisfies_invariant:
@@ -951,12 +951,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 valid_eqns_def, blast)
+ 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)
- show "valid_eqns (Subst_all ES Y (Arden Y yrhs))"
+ show "sound_eqs (Subst_all ES Y (Arden Y yrhs))"
proof-
have "Y = L (Arden Y yrhs)"
using Y_eq_yrhs invariant_ES finite_yrhs
@@ -967,7 +967,7 @@
apply(auto)
done
thus ?thesis using invariant_ES
- unfolding invariant_def finite_rhs_def2 valid_eqns_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))"
@@ -1000,8 +1000,8 @@
ultimately show ?thesis
by (simp add:Subst_all_keeps_finite_rhs)
qed
- show "self_contained (Subst_all ES Y (Arden Y yrhs))"
- using invariant_ES Subst_all_keeps_self_contained by (simp add:invariant_def)
+ show "valid_eqs (Subst_all ES Y (Arden Y yrhs))"
+ using invariant_ES Subst_all_keeps_valid_eqs by (simp add:invariant_def)
qed
lemma Remove_in_card_measure:
@@ -1113,9 +1113,9 @@
lemma Solve:
assumes fin: "finite (UNIV // \<approx>A)"
and X_in: "X \<in> (UNIV // \<approx>A)"
- shows "\<exists>xrhs. Solve X (Init (UNIV // \<approx>A)) = {(X, xrhs)} \<and> invariant {(X, xrhs)}"
+ shows "\<exists>rhs. Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)} \<and> invariant {(X, rhs)}"
proof -
- def Inv \<equiv> "\<lambda>ES. invariant ES \<and> (\<exists>xrhs. (X, xrhs) \<in> ES)"
+ def Inv \<equiv> "\<lambda>ES. invariant ES \<and> (\<exists>rhs. (X, rhs) \<in> ES)"
have "Inv (Init (UNIV // \<approx>A))" unfolding Inv_def
using fin X_in by (simp add: Init_ES_satisfies_invariant, simp add: Init_def)
moreover
@@ -1127,12 +1127,12 @@
moreover
{ fix ES
assume "Inv ES" and "\<not> Cond ES"
- then have "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant ES"
+ then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant ES"
unfolding Inv_def invariant_def
- apply (auto, rule_tac x = xrhs in exI)
+ apply (auto, rule_tac x = rhs in exI)
apply (auto dest!: card_Suc_Diff1 simp: card_eq_0_iff)
done
- then have "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant {(X, xrhs')}"
+ then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant {(X, rhs')}"
by auto }
moreover
have "wf (measure card)" by simp
@@ -1146,7 +1146,7 @@
apply(auto)
done }
ultimately
- show "\<exists>xrhs. Solve X (Init (UNIV // \<approx>A)) = {(X, xrhs)} \<and> invariant {(X, xrhs)}"
+ show "\<exists>rhs. Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)} \<and> invariant {(X, rhs)}"
unfolding Solve_def by (rule while_rule)
qed
@@ -1157,10 +1157,10 @@
def A \<equiv> "Arden X xrhs"
have eq: "{Lam r | r. Lam r \<in> A} = A"
proof -
- have "classes_of A = {}" using Inv_ES
- unfolding A_def self_contained_def invariant_def lhss_def
+ have "rhss A = {}" using Inv_ES
+ unfolding A_def valid_eqs_def invariant_def lhss_def
by (simp add: Arden_removes_cl)
- thus ?thesis unfolding A_def classes_of_def
+ thus ?thesis unfolding A_def rhss_def
apply(auto simp only:)
apply(case_tac x)
apply(auto)
@@ -1174,7 +1174,7 @@
also have "\<dots> = L A" by (simp add: eq)
also have "\<dots> = X"
proof -
- have "X = L xrhs" using Inv_ES unfolding invariant_def valid_eqns_def
+ have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def
by auto
moreover
from Inv_ES have "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})"
--- a/Paper/Paper.thy Mon Feb 14 23:10:44 2011 +0000
+++ b/Paper/Paper.thy Tue Feb 15 08:08:04 2011 +0000
@@ -490,16 +490,16 @@
is a set of terms. Given a set of equivalence
classes @{text CS}, our initial equational system @{term "Init CS"} is thus
formally defined as
-
- \begin{center}
- \begin{tabular}{rcl}
+ %
+ \begin{equation}\label{initcs}
+ \mbox{\begin{tabular}{rcl}
@{thm (lhs) Init_rhs_def} & @{text "\<equiv>"} &
@{text "if"}~@{term "[] \<in> X"}\\
& & @{text "then"}~@{term "{Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} \<union> {Lam EMPTY}"}\\
& & @{text "else"}~@{term "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"}\\
@{thm (lhs) Init_def} & @{text "\<equiv>"} & @{thm (rhs) Init_def}
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \end{equation}
@@ -618,9 +618,10 @@
in each @{const Iter}-step a single equation, and therefore
have a well-founded termination order by taking the cardinality
of the equational system @{text ES}. This enables us to prove
- properties about our definition of @{const Solve} called with
- our initial equational system @{term "Init (UNIV // \<approx>A)"} from ???
- as follows:
+ properties about our definition of @{const Solve} when we ``call'' it with
+ the equivalence class @{text X} and the initial equational system
+ @{term "Init (UNIV // \<approx>A)"} from
+ \eqref{initcs}:
\begin{center}
@@ -635,30 +636,58 @@
\end{center}
\noindent
- This principle states that given an invariant we can prove a property
- @{text "P"} involving @{const Solve}. For this we have to first show that the
+ This principle states that given an invariant (which we will specify below)
+ we can prove a property
+ @{text "P"} involving @{const Solve}. For this we have to discharge the following
+ proof obligations: first the
initial equational system satisfies the invariant; second that the iteration
- step @{text "Iter"} preserves the the invariant as long as the condition @{term Cond};
+ step @{text "Iter"} preserves the the invariant as long as the condition @{term Cond} holds;
third that @{text "Iter"} decreases the termination order, and fourth that
- once the condition does not hold for an invariant equational system @{text ES},
- then the property must hold.
+ once the condition does not hold anymore then the property @{text P} must hold.
- The property @{term P} we will show states that @{term "Solve X (Init (UNIV // \<approx>A))"}
+ The property @{term P} in our proof will state that @{term "Solve X (Init (UNIV // \<approx>A))"}
returns with a single equation @{text "X = xrhs"}, for some @{text "xrhs"} and
- that this equation satisfies also the invariant. The invariant is composed
- of several properties
+ that this equational system still satisfies the invariant. In order to get
+ the proof through, the invariant is composed of the following six properties:
\begin{center}
- \begin{tabular}{rcl@ {\hspace{10mm}}l}
- @{text "invariant X ES"} & @{text "\<equiv>"} &
+ \begin{tabular}{@ {}rcl@ {\hspace{-13mm}}l @ {}}
+ @{text "invariant ES"} & @{text "\<equiv>"} &
@{term "finite ES"} & @{text "(finiteness)"}\\
& @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\
- & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(validity)"}\\
- & @{text "\<and>"} & @{thm (rhs) distinct_equas_def} & @{text "(distinctness)"}\\
+ & @{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) valid_eqs_def} & @{text "(validity)"}\\
\end{tabular}
\end{center}
+ \noindent
+ The first two ensure that the equational system is always finite (number of equations
+ and number of terms in each equation); \ldots
+
+ \begin{lemma}
+ @{thm[mode=IfThen] Init_ES_satisfies_invariant}
+ \end{lemma}
+
+ \begin{lemma}
+ @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
+ \end{lemma}
+
+ \begin{lemma}
+ @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
+ \end{lemma}
+
+ \begin{lemma}
+ If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists
+ a @{text rhs} such that @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"}
+ and @{term "invariant {(X, rhs)}"}.
+ \end{lemma}
+
+ \begin{theorem}
+ @{thm[mode=IfThen] Myhill_Nerode1}
+ \end{theorem}
*}