--- a/Myhill_1.thy Tue Feb 15 08:08:04 2011 +0000
+++ b/Myhill_1.thy Tue Feb 15 10:37:56 2011 +0000
@@ -742,18 +742,16 @@
assumes finite: "finite CS"
shows "finite (Init_rhs CS X)"
proof-
- have "finite {Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" (is "finite ?A")
- proof -
- def S \<equiv> "{(Y, c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}"
- def h \<equiv> "\<lambda> (Y, c). Trn Y (CHAR c)"
- have "finite (CS \<times> (UNIV::char set))" using finite by auto
- hence "finite S" using S_def
- by (rule_tac B = "CS \<times> UNIV" in finite_subset, auto)
- moreover have "?A = h ` S" by (auto simp: S_def h_def image_def)
- ultimately show ?thesis
- by auto
- qed
- thus ?thesis by (simp add:Init_rhs_def transition_def)
+ def S \<equiv> "{(Y, c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}"
+ def h \<equiv> "\<lambda> (Y, c). Trn Y (CHAR c)"
+ have "finite (CS \<times> (UNIV::char set))" using finite by auto
+ then have "finite S" using S_def
+ by (rule_tac B = "CS \<times> UNIV" in finite_subset) (auto)
+ moreover have "{Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X} = h ` S"
+ unfolding S_def h_def image_def by auto
+ ultimately
+ have "finite {Trn Y (CHAR c) |Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}" by auto
+ then show "finite (Init_rhs CS X)" unfolding Init_rhs_def transition_def by simp
qed
lemma Init_ES_satisfies_invariant:
@@ -1045,33 +1043,33 @@
lemma iteration_step_measure:
assumes Inv_ES: "invariant ES"
and X_in_ES: "(X, xrhs) \<in> ES"
- and not_T: "Cond ES "
+ and Cnd: "Cond ES "
shows "(Iter X ES, ES) \<in> measure card"
proof -
- have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
+ have fin: "finite ES" using Inv_ES unfolding invariant_def by simp
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)
+ using Cnd 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 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)
- apply(simp_all add: finite_ES)
+ apply(simp_all add: fin)
done
qed
lemma iteration_step_invariant:
assumes Inv_ES: "invariant ES"
and X_in_ES: "(X, xrhs) \<in> ES"
- and not_T: "Cond ES"
+ and Cnd: "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)
+ using Cnd 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 unfolding invariant_def distinct_equas_def
by auto
@@ -1088,13 +1086,13 @@
lemma iteration_step_ex:
assumes Inv_ES: "invariant ES"
and X_in_ES: "(X, xrhs) \<in> ES"
- and not_T: "Cond ES"
+ and Cnd: "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)
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)
+ using Cnd 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 unfolding invariant_def distinct_equas_def
by auto
@@ -1155,38 +1153,25 @@
shows "\<exists>r::rexp. L r = X"
proof-
def A \<equiv> "Arden X xrhs"
- have eq: "{Lam r | r. Lam r \<in> A} = A"
- proof -
- 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 rhss_def
- apply(auto simp only:)
- apply(case_tac x)
- apply(auto)
- done
- qed
+ have "rhss xrhs \<subseteq> {X}" using Inv_ES
+ unfolding valid_eqs_def invariant_def rhss_def lhss_def
+ by auto
+ then have "rhss A = {}" unfolding A_def
+ by (simp add: Arden_removes_cl)
+ then have eq: "{Lam r | r. Lam r \<in> A} = A" unfolding rhss_def
+ by (auto, case_tac x, auto)
+
have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def
using Arden_keeps_finite by auto
- then have "finite {r. Lam r \<in> A}" by (rule finite_Lam)
- then have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in> A})"
- by auto
- also have "\<dots> = L A" by (simp add: eq)
- also have "\<dots> = X"
- proof -
- 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})"
- unfolding invariant_def ardenable_def finite_rhs_def
- by(simp add: rexp_of_empty)
- moreover
- from Inv_ES have "finite xrhs" unfolding invariant_def finite_rhs_def
- by simp
- ultimately show "L A = X" unfolding A_def
- by (rule Arden_keeps_eq[symmetric])
- qed
- finally have "L (\<Uplus>{r. Lam r \<in> A}) = X" .
+ then have fin: "finite {r. Lam r \<in> A}" by (rule finite_Lam)
+
+ have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def
+ by simp
+ then have "X = L A" using Inv_ES
+ unfolding A_def invariant_def ardenable_def finite_rhs_def rhs_nonempty_def
+ by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn)
+ then have "X = L {Lam r | r. Lam r \<in> A}" using eq by simp
+ then have "X = L (\<Uplus>{r. Lam r \<in> A})" using fin by auto
then show "\<exists>r::rexp. L r = X" by blast
qed
@@ -1216,14 +1201,14 @@
assumes finite_CS: "finite (UNIV // \<approx>A)"
shows "\<exists>r::rexp. A = L r"
proof -
- have f: "finite (finals A)"
+ have fin: "finite (finals A)"
using finals_in_partitions finite_CS by (rule finite_subset)
have "\<forall>X \<in> (UNIV // \<approx>A). \<exists>r::rexp. X = L r"
using finite_CS every_eqcl_has_reg by blast
then have a: "\<forall>X \<in> finals A. \<exists>r::rexp. X = L r"
using finals_in_partitions by auto
then obtain rs::"rexp set" where "\<Union> (finals A) = \<Union>(L ` rs)" "finite rs"
- using f by (auto dest: bchoice_finite_set)
+ using fin by (auto dest: bchoice_finite_set)
then have "A = L (\<Uplus>rs)"
unfolding lang_is_union_of_finals[symmetric] by simp
then show "\<exists>r::rexp. A = L r" by blast