--- a/Myhill_1.thy Mon Feb 14 11:12:01 2011 +0000
+++ b/Myhill_1.thy Mon Feb 14 23:10:44 2011 +0000
@@ -528,12 +528,17 @@
definition
"ardenable ES \<equiv> \<forall>(X, rhs) \<in> ES. rhs_nonempty rhs"
+
text {*
@{text "finite_rhs ES"} requires every equation in @{text "rhs"}
be finite.
*}
definition
- "finite_rhs ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs"
+ "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)
@@ -548,22 +553,26 @@
equational system @{text "ES"}.
*}
definition
- "lefts_of ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"
+ "lhss ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"
text {*
The following @{text "self_contained 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> lefts_of ES"
+ "self_contained ES \<equiv> \<forall>(X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lhss ES"
text {*
The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints.
*}
definition
- "invariant ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and>
- finite_rhs ES \<and> self_contained ES"
+ "invariant ES \<equiv> finite ES
+ \<and> finite_rhs ES
+ \<and> valid_eqns ES
+ \<and> distinct_equas ES
+ \<and> ardenable ES
+ \<and> self_contained ES"
lemma invariantI:
@@ -645,9 +654,9 @@
shows "classes_of (A \<union> B) = classes_of A \<union> classes_of B"
by (auto simp add: classes_of_def)
-lemma lefts_of_union_distrib:
- shows "lefts_of (A \<union> B) = lefts_of A \<union> lefts_of B"
-by (auto simp add: lefts_of_def)
+lemma lhss_union_distrib:
+ shows "lhss (A \<union> B) = lhss A \<union> lhss B"
+by (auto simp add: lhss_def)
subsubsection {* Intialization *}
@@ -760,12 +769,12 @@
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
- by auto
+ 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 "self_contained (Init (UNIV // \<approx>A))"
- unfolding self_contained_def Init_def Init_rhs_def classes_of_def lefts_of_def
+ unfolding self_contained_def Init_def Init_rhs_def classes_of_def lhss_def
by auto
qed
@@ -892,9 +901,9 @@
apply (simp add:Arden_def append_rhs_keeps_cls)
by (auto simp:classes_of_def)
-lemma lefts_of_keeps_cls:
- "lefts_of (Subst_all ES Y yrhs) = lefts_of ES"
-by (auto simp:lefts_of_def Subst_all_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>
@@ -912,10 +921,10 @@
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> lefts_of ?B"
+ have "classes_of xrhs' \<subseteq> lhss ?B"
proof-
- have "lefts_of ?B = lefts_of ES" by (auto simp add:lefts_of_def Subst_all_def)
- moreover have "classes_of xrhs' \<subseteq> lefts_of ES"
+ have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def)
+ moreover have "classes_of xrhs' \<subseteq> lhss ES"
proof-
have "classes_of xrhs' \<subseteq>
classes_of xrhs \<union> classes_of (Arden Y yrhs) - {Y}"
@@ -924,12 +933,12 @@
using Arden_removes_cl by simp
thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls)
qed
- moreover have "classes_of xrhs \<subseteq> lefts_of ES \<union> {Y}" using X_in sc
- apply (simp only:self_contained_def lefts_of_union_distrib)
- by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def)
- moreover have "classes_of (Arden Y yrhs) \<subseteq> lefts_of ES \<union> {Y}"
+ moreover have "classes_of xrhs \<subseteq> lhss ES \<union> {Y}" using X_in sc
+ apply (simp only:self_contained_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}"
using sc
- by (auto simp add:Arden_removes_cl self_contained_def lefts_of_def)
+ by (auto simp add:Arden_removes_cl self_contained_def lhss_def)
ultimately show ?thesis by auto
qed
ultimately show ?thesis by simp
@@ -950,12 +959,16 @@
show "valid_eqns (Subst_all ES Y (Arden Y yrhs))"
proof-
have "Y = L (Arden Y yrhs)"
- using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs
- by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+)
- thus ?thesis using invariant_ES
- by (auto simp add:valid_eqns_def
- Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def
- simp del:L_rhs.simps)
+ 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
+ apply(auto)
+ done
+ thus ?thesis using invariant_ES
+ unfolding invariant_def finite_rhs_def2 valid_eqns_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)
@@ -1015,27 +1028,24 @@
by (auto simp: Subst_all_def)
lemma card_noteq_1_has_more:
- assumes card:"card S \<noteq> 1"
- and e_in: "e \<in> S"
- and finite: "finite S"
- obtains e' where "e' \<in> S \<and> e \<noteq> e'"
+ assumes card:"Cond ES"
+ and e_in: "(X, xrhs) \<in> ES"
+ and finite: "finite ES"
+ shows "\<exists>(Y, yrhs) \<in> ES. (X, xrhs) \<noteq> (Y, yrhs)"
proof-
- have "card (S - {e}) > 0"
- proof -
- have "card S > 1" using card e_in finite
- by (cases "card S") (auto)
- thus ?thesis using finite e_in by auto
- qed
- hence "S - {e} \<noteq> {}" using finite by (rule_tac notI, simp)
- thus "(\<And>e'. e' \<in> S \<and> e \<noteq> e' \<Longrightarrow> thesis) \<Longrightarrow> thesis" by auto
+ have "card ES > 1" using card e_in finite
+ by (cases "card ES") (auto)
+ then have "card (ES - {(X, xrhs)}) > 0"
+ using finite e_in by auto
+ then have "(ES - {(X, xrhs)}) \<noteq> {}" using finite by (rule_tac notI, simp)
+ then show "\<exists>(Y, yrhs) \<in> ES. (X, xrhs) \<noteq> (Y, yrhs)"
+ by auto
qed
-
-
lemma iteration_step_measure:
assumes Inv_ES: "invariant ES"
and X_in_ES: "(X, xrhs) \<in> ES"
- and not_T: "card ES \<noteq> 1"
+ and not_T: "Cond ES "
shows "(Iter X ES, ES) \<in> measure card"
proof -
have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
@@ -1043,8 +1053,8 @@
where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)"
using not_T 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
- by (auto simp: invariant_def distinct_equas_def)
+ using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
+ by auto
then show "(Iter X ES, ES) \<in> measure card"
apply(rule IterI2)
apply(rule Remove_in_card_measure)
@@ -1055,16 +1065,16 @@
lemma iteration_step_invariant:
assumes Inv_ES: "invariant ES"
and X_in_ES: "(X, xrhs) \<in> ES"
- and not_T: "card ES \<noteq> 1"
+ and not_T: "Cond ES"
shows "invariant (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)"
using not_T 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
- by (auto simp: invariant_def distinct_equas_def)
+ then have "(Y, yrhs) \<in> ES" "X \<noteq> Y"
+ using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
+ by auto
then show "invariant (Iter X ES)"
proof(rule IterI2)
fix Y yrhs
@@ -1078,7 +1088,7 @@
lemma iteration_step_ex:
assumes Inv_ES: "invariant ES"
and X_in_ES: "(X, xrhs) \<in> ES"
- and not_T: "card ES \<noteq> 1"
+ and not_T: "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)
@@ -1086,8 +1096,8 @@
where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)"
using not_T 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
- by (auto simp: invariant_def distinct_equas_def)
+ using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
+ by auto
then show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)"
apply(rule IterI2)
unfolding Remove_def
@@ -1100,49 +1110,44 @@
subsubsection {* Conclusion of the proof *}
-text {*
- From this point until @{text "hard_direction"}, the hard direction is proved
- through a simple application of the iteration principle.
-*}
-
-
-lemma reduce_x:
- assumes inv: "invariant ES"
- and contain_x: "(X, xrhs) \<in> ES"
- shows "\<exists> xrhs'. Solve X ES = {(X, xrhs')} \<and> invariant(Solve X ES)"
+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)}"
proof -
- let ?Inv = "\<lambda> ES. (invariant ES \<and> (\<exists> xrhs. (X, xrhs) \<in> ES))"
- show ?thesis unfolding Solve_def
- proof (rule while_rule [where P = ?Inv and r = "measure card"])
- from inv and contain_x show "?Inv ES" by auto
- next
- show "wf (measure card)" by simp
- next
- fix ES
- assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
- then show "(Iter X ES, ES) \<in> measure card"
+ def Inv \<equiv> "\<lambda>ES. invariant ES \<and> (\<exists>xrhs. (X, xrhs) \<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
+ { fix ES
+ assume inv: "Inv ES" and crd: "Cond ES"
+ then have "Inv (Iter X ES)"
+ unfolding Inv_def
+ by (auto simp add: iteration_step_invariant iteration_step_ex) }
+ moreover
+ { fix ES
+ assume "Inv ES" and "\<not> Cond ES"
+ then have "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant ES"
+ unfolding Inv_def invariant_def
+ apply (auto, rule_tac x = xrhs 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')}"
+ by auto }
+ moreover
+ have "wf (measure card)" by simp
+ moreover
+ { fix ES
+ assume inv: "Inv ES" and crd: "Cond ES"
+ then have "(Iter X ES, ES) \<in> measure card"
+ unfolding Inv_def
apply(clarify)
- apply(rule iteration_step_measure)
- apply(auto)
- done
- next
- fix ES
- assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
- then show "?Inv (Iter X ES)"
- apply -
- apply(auto)
- apply(rule iteration_step_invariant)
+ apply(rule_tac iteration_step_measure)
apply(auto)
- apply(rule iteration_step_ex)
- apply(auto)
- done
- next
- fix ES
- assume "?Inv ES" and "\<not> card ES \<noteq> 1"
- thus "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant ES"
- apply (auto, rule_tac x = xrhs in exI)
- by (auto simp: invariant_def dest!:card_Suc_Diff1 simp:card_eq_0_iff)
- qed
+ done }
+ ultimately
+ show "\<exists>xrhs. Solve X (Init (UNIV // \<approx>A)) = {(X, xrhs)} \<and> invariant {(X, xrhs)}"
+ unfolding Solve_def by (rule while_rule)
qed
lemma last_cl_exists_rexp:
@@ -1153,7 +1158,7 @@
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 lefts_of_def
+ unfolding A_def self_contained_def invariant_def lhss_def
by (simp add: Arden_removes_cl)
thus ?thesis unfolding A_def classes_of_def
apply(auto simp only:)
@@ -1190,20 +1195,13 @@
and X_in_CS: "X \<in> (UNIV // \<approx>A)"
shows "\<exists>r::rexp. L r = X"
proof -
- def ES \<equiv> "Init (UNIV // \<approx>A)"
- have "invariant ES" using finite_CS unfolding ES_def
- by (rule Init_ES_satisfies_invariant)
- moreover
- from X_in_CS obtain xrhs where "(X, xrhs) \<in> ES" unfolding ES_def
- unfolding Init_def Init_rhs_def by auto
- ultimately
- obtain xrhs' where "Solve X ES = {(X, xrhs')}" "invariant (Solve X ES)"
- using reduce_x by blast
+ from finite_CS X_in_CS
+ obtain xrhs where "invariant {(X, xrhs)}"
+ using Solve by metis
then show "\<exists>r::rexp. L r = X"
- using last_cl_exists_rexp by auto
+ using last_cl_exists_rexp by auto
qed
-
lemma bchoice_finite_set:
assumes a: "\<forall>x \<in> S. \<exists>y. x = f y"
and b: "finite S"
--- a/Paper/Paper.thy Mon Feb 14 11:12:01 2011 +0000
+++ b/Paper/Paper.thy Mon Feb 14 23:10:44 2011 +0000
@@ -149,7 +149,7 @@
requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98}
dismisses for this the option of using identities, because it leads according to
him to ``messy proofs''. He
- opts for a variant of \eqref{disjointunion} using bitlists, but writes
+ opts for a variant of \eqref{disjointunion} using bit lists, but writes
\begin{quote}
\it%
@@ -482,7 +482,7 @@
\noindent
The reason for adding the @{text \<lambda>}-marker to our initial equational system is
- to obtain this equation: it only holds with the marker since none of
+ to obtain this equation: it only holds with the marker, since none of
the other terms contain the empty string.
Our representation for the equations in Isabelle/HOL are pairs,
@@ -592,7 +592,7 @@
expression. Therefore we define the iteration step so that it chooses an
equation with an equivalence class that is not @{text X}. This allows us to
control, which equation will be the last. We use Hilbert's choice operator,
- written @{text SOME}, to chose an equation to be eliminated in @{text ES}.
+ written @{text SOME}, to choose an equation to be eliminated in @{text ES}.
\begin{center}
\begin{tabular}{rc@ {\hspace{4mm}}r@ {\hspace{1mm}}l}
@@ -603,22 +603,62 @@
\end{center}
\noindent
- The last definition applies @{term Iter} over and over again a condition
+ 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 in the equational system @{text ES}. The
- iteration is defined in terms of HOL's @{text while}-operator as follows:
+ are more than one equation left in the equational system @{text ES}. For this
+ we use Isabelle/HOL's @{text while}-operator as follows:
\begin{center}
@{thm Solve_def}
\end{center}
\noindent
- We are not concerned here with the definition of this operator in this paper
- (see \cite{BerghoferNipkow00}).
+ We are not concerned here with the definition of this operator
+ (see \cite{BerghoferNipkow00}), but note that we eliminate
+ 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:
+
\begin{center}
- @{thm while_rule}
+ \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}
+
+ \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
+ initial equational system satisfies the invariant; second that the iteration
+ step @{text "Iter"} preserves the the invariant as long as the condition @{term Cond};
+ 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.
+
+ The property @{term P} we will show states 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
+
+ \begin{center}
+ \begin{tabular}{rcl@ {\hspace{10mm}}l}
+ @{text "invariant X 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>"} & @{thm (rhs) ardenable_def} & @{text "(ardenable)"}\\
+ \end{tabular}
+ \end{center}
+
*}