# HG changeset patch
# User urbanc
# Date 1297426415 0
# Node ID 70485955c9347edc415ae2acdf2a6a9434c04bef
# Parent 3b9deda4f45960f65a94f3fa0836758aa2054b99
slightly streamlined the proof
diff -r 3b9deda4f459 -r 70485955c934 Myhill_1.thy
--- a/Myhill_1.thy Thu Feb 10 21:00:40 2011 +0000
+++ b/Myhill_1.thy Fri Feb 11 12:13:35 2011 +0000
@@ -249,33 +249,6 @@
show "X = B ;; A\<star>" by simp
qed
-(*
-corollary arden_eq:
- assumes nemp: "[] \<notin> A"
- shows "(X ;; A \<union> B) = (B ;; A\<star>)"
-proof -
- { assume "X = X ;; A \<union> B"
- then have "X = B ;; A\<star>"
- then have ?thesis
- thm arden[THEN iffD1]
-apply(rule set_eqI)
-thm arden[THEN iffD1]
-apply(rule iffI)
-apply(rule trans)
-apply(rule arden[THEN iffD2, symmetric])
-apply(rule arden[OF iffD1, symmetric])
-thm trans
-proof -
- { assume "X = X ;; A \<union> B"
- then have "X = B ;; A\<star>" using arden[OF nemp] by blast
- moreover
-
-
-using arden[of "A" "X" "B", OF nemp]
-apply(erule_tac iffE)
-apply(blast)
-*)
-
section {* Regular Expressions *}
@@ -468,7 +441,11 @@
equation of the equational system @{text ES}.
*}
+types esystem = "(lang \<times> rhs_item set) set"
+
definition
+ Subst_all :: "esystem \<Rightarrow> lang \<Rightarrow> rhs_item set \<Rightarrow> esystem"
+where
"Subst_all ES X xrhs \<equiv> {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
text {*
@@ -495,36 +472,57 @@
"Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y
in Remove ES Y yrhs)"
+lemma IterI2:
+ assumes "(Y, yrhs) \<in> ES"
+ and "X \<noteq> Y"
+ and "\<And>Y yrhs. \<lbrakk>(Y, yrhs) \<in> ES; X \<noteq> Y\<rbrakk> \<Longrightarrow> Q (Remove ES Y yrhs)"
+ shows "Q (Iter X ES)"
+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
+ "Test ES \<equiv> card ES \<noteq> 1"
+
definition
- "Reduce X ES \<equiv> while (\<lambda> ES. card ES \<noteq> 1) (Iter X) ES"
+ "Solve X ES \<equiv> while Test (Iter X) ES"
+
+
+(* test *)
+partial_function (tailrec)
+ solve
+where
+ "solve X ES = (if (card ES = 1) then ES else solve X (Iter X ES))"
+
text {*
- Since the @{text "while"} combinator from HOL library is used to implement @{text "Reduce X ES"},
+ 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 "Reduce X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
+ 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 onece in @{text ES}. *}
+text {* Every variable is defined at most once in @{text ES}. *}
definition
"distinct_equas 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)"}.
+ is valid, i.e. @{text "X = L rhs"}.
*}
definition
- "valid_eqns ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> (X = L rhs)"
+ "valid_eqns ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
text {*
@{text "rhs_nonempty rhs"} requires regular expressions occuring in
@@ -541,7 +539,7 @@
*}
definition
- "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> rhs_nonempty rhs"
+ "ardenable ES \<equiv> \<forall>(X, rhs) \<in> ES. rhs_nonempty rhs"
text {*
@{text "finite_rhs ES"} requires every equation in @{text "rhs"}
@@ -556,7 +554,7 @@
*}
definition
- "classes_of rhs \<equiv> {X. \<exists> r. Trn X r \<in> rhs}"
+ "classes_of rhs \<equiv> {X | X r. Trn X r \<in> rhs}"
text {*
@{text "lefts_of ES"} returns all variables defined by an
@@ -570,7 +568,7 @@
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> lefts_of ES"
text {*
@@ -629,7 +627,7 @@
shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
using finite nonempty rhs_nonempty_def
using finite_Trn[OF finite]
-by (auto)
+by auto
lemma lang_of_rexp_of:
assumes finite:"finite rhs"
@@ -758,7 +756,7 @@
proof (rule invariantI)
show "valid_eqns (Init (UNIV // \<approx>A))"
unfolding valid_eqns_def
- using l_eq_r_in_eqs by simp
+ 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))"
@@ -873,8 +871,8 @@
have "finite {(Ya, Subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \<in> ES}"
(is "finite ?A")
proof-
- def eqns' \<equiv> "{((Ya::string set), yrhsa)| Ya yrhsa. (Ya, yrhsa) \<in> ES}"
- def h \<equiv> "\<lambda> ((Ya::string set), yrhsa). (Ya, Subst yrhsa Y yrhs)"
+ 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
@@ -958,7 +956,7 @@
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 (clarsimp simp add:valid_eqns_def
+ by (auto simp add:valid_eqns_def
Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def
simp del:L_rhs.simps)
qed
@@ -972,7 +970,7 @@
{ fix X rhs
assume "(X, rhs) \<in> ES"
hence "rhs_nonempty rhs" using prems invariant_ES
- by (simp add:invariant_def ardenable_def)
+ by (auto simp add:invariant_def ardenable_def)
with nonempty_yrhs
have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))"
by (simp add:nonempty_yrhs
@@ -996,98 +994,112 @@
using invariant_ES Subst_all_keeps_self_contained by (simp add:invariant_def)
qed
-lemma Subst_all_card_le:
- assumes finite: "finite (ES::(string set \<times> rhs_item set) set)"
- shows "card (Subst_all ES Y yrhs) <= card ES"
-proof-
- def f \<equiv> "\<lambda> x. ((fst x)::string set, Subst (snd x) Y yrhs)"
- have "Subst_all ES Y yrhs = f ` ES"
- apply (auto simp:Subst_all_def f_def image_def)
- by (rule_tac x = "(Ya, yrhsa)" in bexI, simp+)
- thus ?thesis using finite by (auto intro:card_image_le)
+lemma Remove_in_card_measure:
+ assumes finite: "finite ES"
+ and in_ES: "(X, rhs) \<in> ES"
+ shows "(Remove ES X rhs, ES) \<in> measure card"
+proof -
+ def f \<equiv> "\<lambda> x. ((fst x)::lang, Subst (snd x) X (Arden X rhs))"
+ def ES' \<equiv> "ES - {(X, rhs)}"
+ have "Subst_all ES' X (Arden X rhs) = f ` ES'"
+ apply (auto simp: Subst_all_def f_def image_def)
+ by (rule_tac x = "(Y, yrhs)" in bexI, simp+)
+ then have "card (Subst_all ES' X (Arden X rhs)) \<le> card ES'"
+ unfolding ES'_def using finite by (auto intro: card_image_le)
+ also have "\<dots> < card ES" unfolding ES'_def
+ using in_ES finite by (rule_tac card_Diff1_less)
+ finally show "(Remove ES X rhs, ES) \<in> measure card"
+ unfolding Remove_def ES'_def by simp
qed
+
lemma Subst_all_cls_remains:
"(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (Subst_all ES Y yrhs)"
-by (auto simp:Subst_all_def)
+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'"
+ obtains e' where "e' \<in> S \<and> e \<noteq> e'"
proof-
have "card (S - {e}) > 0"
proof -
- have "card S > 1" using card e_in finite
- by (case_tac "card S", auto)
+ 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
qed
-lemma iteration_step:
+
+
+lemma iteration_step_measure:
assumes Inv_ES: "invariant ES"
and X_in_ES: "(X, xrhs) \<in> ES"
and not_T: "card ES \<noteq> 1"
- shows "(invariant (Iter X ES) \<and> (\<exists> xrhs'.(X, xrhs') \<in> (Iter X ES)) \<and>
- (Iter X ES, ES) \<in> measure card)"
+ shows "(Iter X ES, ES) \<in> measure card"
+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 show "(Iter X ES, ES) \<in> measure card"
+ apply(rule IterI2)
+ apply(rule Remove_in_card_measure)
+ apply(simp_all add: finite_ES)
+ done
+qed
+
+lemma iteration_step_invariant:
+ assumes Inv_ES: "invariant ES"
+ and X_in_ES: "(X, xrhs) \<in> ES"
+ and not_T: "card ES \<noteq> 1"
+ 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)
- let ?ES' = "Iter X ES"
- show ?thesis
- proof(unfold Iter_def Remove_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_all (ES - {(Y, yrhs)}) Y (Arden 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_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<and>
- (\<exists>xrhs'. (X, xrhs') \<in> Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<and>
- card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES"
- proof -
- have "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))"
- proof(rule Subst_all_satisfies_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_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))"
- proof(rule Subst_all_cls_remains)
- from X_in_ES and h
- show "(X, xrhs) \<in> ES - {(Y, yrhs)}" by auto
- qed
- moreover have
- "card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES"
- proof(rule le_less_trans)
- show
- "card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<le>
- card (ES - {(Y, yrhs)})"
- proof(rule Subst_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_all_card_le elim:le_less_trans)
- qed
- qed
+ 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 show "invariant (Iter X ES)"
+ proof(rule IterI2)
+ fix Y yrhs
+ 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)
qed
qed
+lemma iteration_step_ex:
+ assumes Inv_ES: "invariant ES"
+ and X_in_ES: "(X, xrhs) \<in> ES"
+ and not_T: "card ES \<noteq> 1"
+ shows "\<exists>xrhs'. (X, xrhs') \<in> (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 show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)"
+ apply(rule IterI2)
+ unfolding Remove_def
+ apply(rule Subst_all_cls_remains)
+ using X_in_ES
+ apply(auto)
+ done
+qed
+
subsubsection {* Conclusion of the proof *}
@@ -1096,38 +1108,37 @@
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'. Reduce X ES = {(X, xrhs')} \<and> invariant(Reduce X ES)"
+ shows "\<exists> xrhs'. Solve X ES = {(X, xrhs')} \<and> invariant(Solve 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"])
+ 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"
- 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
+ then show "(Iter X ES, ES) \<in> measure card"
+ apply(clarify)
+ apply(rule iteration_step_measure)
+ apply(auto)
+ done
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
+ then show "?Inv (Iter X ES)"
+ apply -
+ apply(auto)
+ apply(rule iteration_step_invariant)
+ apply(auto)
+ apply(rule iteration_step_ex)
+ apply(auto)
+ done
next
fix ES
assume "?Inv ES" and "\<not> card ES \<noteq> 1"
@@ -1189,7 +1200,7 @@
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 "Reduce X ES = {(X, xrhs')}" "invariant (Reduce X ES)"
+ obtain xrhs' where "Solve X ES = {(X, xrhs')}" "invariant (Solve X ES)"
using reduce_x by blast
then show "\<exists>r::rexp. L r = X"
using last_cl_exists_rexp by auto