--- 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"