--- a/Myhill_1.thy Wed Feb 09 09:46:59 2011 +0000
+++ b/Myhill_1.thy Wed Feb 09 12:34:30 2011 +0000
@@ -1,5 +1,5 @@
theory Myhill_1
-imports Main Folds
+imports Main Folds While_Combinator
begin
section {* Preliminary definitions *}
@@ -442,47 +442,43 @@
"subst_op_all ES X xrhs \<equiv> {(Y, subst_op yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
-section {* Well-founded iteration *}
+section {* While-combinator *}
text {*
- The computation of regular expressions for equivalence classes is accomplished
- using a iteration principle given by the following lemma.
+ 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_op ES Y yrhs \<equiv>
+ subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)"
+
+text {*
+ The following term @{text "iterm X ES"} represents one iteration in the while loop.
+ It arbitrarily chooses a @{text "Y"} different from @{text "X"} to remove.
*}
-lemma wf_iter [rule_format]:
- fixes f
- assumes step: "\<And> e. \<lbrakk>P e; \<not> Q e\<rbrakk> \<Longrightarrow> (\<exists> e'. P e' \<and> (f(e'), f(e)) \<in> less_than)"
- shows pe: "P e \<longrightarrow> (\<exists> e'. P e' \<and> Q e')"
-proof(induct e rule: wf_induct
- [OF wf_inv_image[OF wf_less_than, where f = "f"]], clarify)
- fix x
- assume h [rule_format]:
- "\<forall>y. (y, x) \<in> inv_image less_than f \<longrightarrow> P y \<longrightarrow> (\<exists>e'. P e' \<and> Q e')"
- and px: "P x"
- show "\<exists>e'. P e' \<and> Q e'"
- proof(cases "Q x")
- assume "Q x" with px show ?thesis by blast
- next
- assume nq: "\<not> Q x"
- from step [OF px nq]
- obtain e' where pe': "P e'" and ltf: "(f e', f x) \<in> less_than" by auto
- show ?thesis
- proof(rule h)
- from ltf show "(e', x) \<in> inv_image less_than f"
- by (simp add:inv_image_def)
- next
- from pe' show "P e'" .
- qed
- qed
-qed
+definition
+ "iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> (X \<noteq> Y)
+ in remove_op ES Y yrhs)"
text {*
- The @{text "P"} in lemma @{text "wf_iter"} is an invariant kept throughout the iteration procedure.
- The particular invariant used to solve our problem is defined by function @{text "Inv(ES)"},
- an invariant over equal system @{text "ES"}.
- Every definition starting next till @{text "Inv"} stipulates a property to be satisfied by @{text "ES"}.
+ The following term @{text "reduce X ES"} repeatedly removes characteriztion equations
+ for unknowns other than @{text "X"} until one is left.
*}
+definition
+ "reduce X ES \<equiv> while (\<lambda> ES. card ES \<noteq> 1) (iter X) ES"
+
+text {*
+ Since the @{text "while"} combinator from HOL library is used to implement @{text "reduce X ES"},
+ the induction principle @{thm [source] while_rule} is used to proved the desired properties
+ of @{text "reduce X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
+ in terms of a series of auxilliary predicates:
+*}
section {* Invariants *}
@@ -757,14 +753,11 @@
ultimately show ?thesis by (simp add:invariant_def)
qed
-subsubsection {*
- Interation step
- *}
+subsubsection {* Interation step *}
text {*
- From this point until @{text "iteration_step"}, it is proved
- that there exists iteration steps which keep @{text "invariant(ES)"} while
- decreasing the size of @{text "ES"}.
+ From this point until @{text "iteration_step"},
+ the correctness of the iteration step @{text "iter X ES"} is proved.
*}
lemma arden_op_keeps_eq:
@@ -1019,66 +1012,118 @@
thus "(\<And>e'. e' \<in> S \<and> e \<noteq> e' \<Longrightarrow> thesis) \<Longrightarrow> thesis" by auto
qed
-lemma iteration_step:
- assumes invariant_ES: "invariant ES"
+lemma iteration_step:
+ assumes Inv_ES: "invariant ES"
and X_in_ES: "(X, xrhs) \<in> ES"
and not_T: "card ES \<noteq> 1"
- shows "\<exists> ES'. (invariant ES' \<and> (\<exists> xrhs'.(X, xrhs') \<in> ES')) \<and>
- (card ES', card ES) \<in> less_than" (is "\<exists> ES'. ?P ES'")
+ shows "(invariant (iter X ES) \<and> (\<exists> xrhs'.(X, xrhs') \<in> (iter X ES)) \<and>
+ (iter X ES, ES) \<in> measure card)"
proof -
- have finite_ES: "finite ES" using invariant_ES by (simp add:invariant_def)
+ 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)
- def ES' == "ES - {(Y, yrhs)}"
- let ?ES'' = "subst_op_all ES' Y (arden_op Y yrhs)"
- have "?P ?ES''"
- proof -
- have "invariant ?ES''" using Y_in_ES invariant_ES
- by (rule_tac subst_op_all_satisfy_invariant, simp add:ES'_def insert_absorb)
- moreover have "\<exists>xrhs'. (X, xrhs') \<in> ?ES''" using not_eq X_in_ES
- by (rule_tac ES = ES' in subst_op_all_cls_remains, auto simp add:ES'_def)
- moreover have "(card ?ES'', card ES) \<in> less_than"
- proof -
- have "finite ES'" using finite_ES ES'_def by auto
- moreover have "card ES' < card ES" using finite_ES Y_in_ES
- by (auto simp:ES'_def card_gt_0_iff intro:diff_Suc_less)
- ultimately show ?thesis
- by (auto dest:subst_op_all_card_le elim:le_less_trans)
+ let ?ES' = "iter X ES"
+ show ?thesis
+ proof(unfold iter_def remove_op_def, rule someI2 [where a = "(Y, yrhs)"], clarsimp)
+ from X_in_ES Y_in_ES and not_eq and Inv_ES
+ show "(Y, yrhs) \<in> ES \<and> X \<noteq> Y"
+ by (auto simp: invariant_def distinct_equas_def)
+ next
+ fix x
+ let ?ES' = "let (Y, yrhs) = x in subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)"
+ assume prem: "case x of (Y, yrhs) \<Rightarrow> (Y, yrhs) \<in> ES \<and> (X \<noteq> Y)"
+ thus "invariant (?ES') \<and> (\<exists>xrhs'. (X, xrhs') \<in> ?ES') \<and> (?ES', ES) \<in> measure card"
+ proof(cases "x", simp)
+ fix Y yrhs
+ assume h: "(Y, yrhs) \<in> ES \<and> X \<noteq> Y"
+ show "invariant (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \<and>
+ (\<exists>xrhs'. (X, xrhs') \<in> subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \<and>
+ card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) < card ES"
+ proof -
+ have "invariant (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs))"
+ proof(rule subst_op_all_satisfy_invariant)
+ from h have "(Y, yrhs) \<in> ES" by simp
+ hence "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto
+ with Inv_ES show "invariant (ES - {(Y, yrhs)} \<union> {(Y, yrhs)})" by auto
+ qed
+ moreover have
+ "(\<exists>xrhs'. (X, xrhs') \<in> subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs))"
+ proof(rule subst_op_all_cls_remains)
+ from X_in_ES and h
+ show "(X, xrhs) \<in> ES - {(Y, yrhs)}" by auto
+ qed
+ moreover have
+ "card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) < card ES"
+ proof(rule le_less_trans)
+ show
+ "card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \<le>
+ card (ES - {(Y, yrhs)})"
+ proof(rule subst_op_all_card_le)
+ show "finite (ES - {(Y, yrhs)})" using finite_ES by auto
+ qed
+ next
+ show "card (ES - {(Y, yrhs)}) < card ES" using finite_ES h
+ by (auto simp:card_gt_0_iff intro:diff_Suc_less)
+ qed
+ ultimately show ?thesis
+ by (auto dest: subst_op_all_card_le elim:le_less_trans)
+ qed
qed
- ultimately show ?thesis by simp
qed
- thus ?thesis by blast
qed
-subsubsection {*
- Conclusion of the proof
- *}
+
+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 iteration_conc:
- assumes history: "invariant ES"
- and X_in_ES: "\<exists> xrhs. (X, xrhs) \<in> ES"
- shows
- "\<exists> ES'. (invariant ES' \<and> (\<exists> xrhs'. (X, xrhs') \<in> ES')) \<and> card ES' = 1"
- (is "\<exists> ES'. ?P ES'")
-proof (cases "card ES = 1")
- case True
- thus ?thesis using history X_in_ES
- by blast
-next
- case False
- thus ?thesis using history iteration_step X_in_ES
- by (rule_tac f = card in wf_iter, auto)
+lemma reduce_x:
+ assumes inv: "invariant ES"
+ and contain_x: "(X, xrhs) \<in> ES"
+ shows "\<exists> xrhs'. reduce X ES = {(X, xrhs')} \<and> invariant(reduce X ES)"
+proof -
+ let ?Inv = "\<lambda> ES. (invariant ES \<and> (\<exists> xrhs. (X, xrhs) \<in> ES))"
+ show ?thesis
+ proof (unfold reduce_def,
+ 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"
+ show "(iter X ES, ES) \<in> measure card"
+ proof -
+ from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto
+ from inv have "invariant ES" by simp
+ from iteration_step [OF this x_in crd]
+ show ?thesis by auto
+ qed
+ next
+ fix ES
+ assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
+ thus "?Inv (iter X ES)"
+ proof -
+ from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto
+ from inv have "invariant ES" by simp
+ from iteration_step [OF this x_in crd]
+ show ?thesis by auto
+ qed
+ 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
qed
-
+
lemma last_cl_exists_rexp:
- assumes ES_single: "ES = {(X, xrhs)}"
- and invariant_ES: "invariant ES"
+ assumes Inv_ES: "invariant {(X, xrhs)}"
shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r")
proof-
def A \<equiv> "arden_op X xrhs"
@@ -1088,7 +1133,7 @@
proof(rule rexp_of_lam_eq_lam_set)
show "finite A"
unfolding A_def
- using invariant_ES ES_single
+ using Inv_ES
by (rule_tac arden_op_keeps_finite)
(auto simp add: invariant_def finite_rhs_def)
qed
@@ -1096,7 +1141,7 @@
proof-
have "{Lam r | r. Lam r \<in> A} = A"
proof-
- have "classes_of A = {}" using invariant_ES ES_single
+ have "classes_of A = {}" using Inv_ES
unfolding A_def
by (simp add:arden_op_removes_cl
self_contained_def invariant_def lefts_of_def)
@@ -1109,38 +1154,37 @@
also have "\<dots> = X"
unfolding A_def
proof(rule arden_op_keeps_eq [THEN sym])
- show "X = L xrhs" using invariant_ES ES_single
- by (auto simp only:invariant_def valid_eqns_def)
+ show "X = L xrhs" using Inv_ES
+ by (auto simp only: invariant_def valid_eqns_def)
next
- from invariant_ES ES_single show "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})"
- by(simp add:invariant_def ardenable_def rexp_of_empty finite_rhs_def)
+ from Inv_ES show "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})"
+ by(simp add: invariant_def ardenable_def rexp_of_empty finite_rhs_def)
next
- from invariant_ES ES_single show "finite xrhs"
- by (simp add:invariant_def finite_rhs_def)
+ from Inv_ES show "finite xrhs"
+ by (simp add: invariant_def finite_rhs_def)
qed
finally show ?thesis by simp
qed
thus ?thesis by auto
qed
-
+
lemma every_eqcl_has_reg:
assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
and X_in_CS: "X \<in> (UNIV // (\<approx>Lang))"
shows "\<exists> (reg::rexp). L reg = X" (is "\<exists> r. ?E r")
proof -
- from X_in_CS have "\<exists> xrhs. (X, xrhs) \<in> (eqs (UNIV // (\<approx>Lang)))"
+ let ?ES = " eqs (UNIV // \<approx>Lang)"
+ from X_in_CS
+ obtain xrhs where "(X, xrhs) \<in> ?ES"
by (auto simp:eqs_def init_rhs_def)
- then obtain ES xrhs where invariant_ES: "invariant ES"
- and X_in_ES: "(X, xrhs) \<in> ES"
- and card_ES: "card ES = 1"
- using finite_CS X_in_CS init_ES_satisfy_invariant iteration_conc
- by blast
- hence ES_single_equa: "ES = {(X, xrhs)}"
- by (auto simp:invariant_def dest!:card_Suc_Diff1 simp:card_eq_0_iff)
- thus ?thesis using invariant_ES
- by (rule last_cl_exists_rexp)
+ from reduce_x [OF init_ES_satisfy_invariant [OF finite_CS] this]
+ have "\<exists>xrhs'. reduce X ?ES = {(X, xrhs')} \<and> invariant (reduce X ?ES)" .
+ then obtain xrhs' where "invariant {(X, xrhs')}" by auto
+ from last_cl_exists_rexp [OF this]
+ show ?thesis .
qed
+
theorem hard_direction:
assumes finite_CS: "finite (UNIV // \<approx>A)"
shows "\<exists>r::rexp. A = L r"