--- a/Myhill_1.thy Wed Feb 16 12:25:53 2011 +0000
+++ b/Myhill_1.thy Thu Feb 17 11:42:16 2011 +0000
@@ -512,21 +512,21 @@
"sound_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
text {*
- @{text "rhs_nonempty rhs"} requires regular expressions occuring in
+ @{text "ardenable rhs"} requires regular expressions occuring in
transitional items of @{text "rhs"} do not contain empty string. This is
necessary for the application of Arden's transformation to @{text "rhs"}.
*}
definition
- "rhs_nonempty rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"
+ "ardenable rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"
text {*
- The following @{text "ardenable ES"} requires that Arden's transformation
+ The following @{text "ardenable_all ES"} requires that Arden's transformation
is applicable to every equation of equational system @{text "ES"}.
*}
definition
- "ardenable ES \<equiv> \<forall>(X, rhs) \<in> ES. rhs_nonempty rhs"
+ "ardenable_all ES \<equiv> \<forall>(X, rhs) \<in> ES. ardenable rhs"
text {*
@@ -571,12 +571,12 @@
\<and> finite_rhs ES
\<and> sound_eqs ES
\<and> distinct_equas ES
- \<and> ardenable ES
+ \<and> ardenable_all ES
\<and> valid_eqs ES"
lemma invariantI:
- assumes "sound_eqs ES" "finite ES" "distinct_equas ES" "ardenable ES"
+ assumes "sound_eqs ES" "finite ES" "distinct_equas ES" "ardenable_all ES"
"finite_rhs ES" "valid_eqs ES"
shows "invariant ES"
using assms by (simp add: invariant_def)
@@ -619,9 +619,9 @@
lemma rexp_of_empty:
assumes finite: "finite rhs"
- and nonempty: "rhs_nonempty rhs"
+ and nonempty: "ardenable rhs"
shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
-using finite nonempty rhs_nonempty_def
+using finite nonempty ardenable_def
using finite_Trn[OF finite]
by auto
@@ -765,8 +765,8 @@
unfolding Init_def by simp
show "distinct_equas (Init (UNIV // \<approx>A))"
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
+ show "ardenable_all (Init (UNIV // \<approx>A))"
+ unfolding ardenable_all_def Init_def Init_rhs_def ardenable_def
by auto
show "finite_rhs (Init (UNIV // \<approx>A))"
using finite_Init_rhs[OF finite_CS]
@@ -785,7 +785,7 @@
lemma Arden_keeps_eq:
assumes l_eq_r: "X = L rhs"
- and not_empty: "[] \<notin> L (\<Uplus>{r. Trn X r \<in> rhs})"
+ and not_empty: "ardenable rhs"
and finite: "finite rhs"
shows "X = L (Arden X rhs)"
proof -
@@ -799,9 +799,11 @@
unfolding L_rhs_union_distrib[symmetric]
by (simp only: lang_of_rexp_of finite B_def A_def)
finally show ?thesis
- using l_eq_r not_empty
apply(rule_tac arden[THEN iffD1])
- apply(simp add: A_def)
+ apply(simp (no_asm) add: A_def)
+ using finite_Trn[OF finite] not_empty
+ apply(simp add: ardenable_def)
+ using l_eq_r
apply(simp)
done
qed
@@ -820,25 +822,25 @@
by (auto simp:Arden_def append_keeps_finite)
lemma append_keeps_nonempty:
- "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (append_rhs_rexp rhs r)"
-apply (auto simp:rhs_nonempty_def append_rhs_rexp_def)
+ "ardenable rhs \<Longrightarrow> ardenable (append_rhs_rexp rhs r)"
+apply (auto simp:ardenable_def append_rhs_rexp_def)
by (case_tac x, auto simp:Seq_def)
lemma nonempty_set_sub:
- "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (rhs - A)"
-by (auto simp:rhs_nonempty_def)
+ "ardenable rhs \<Longrightarrow> ardenable (rhs - A)"
+by (auto simp:ardenable_def)
lemma nonempty_set_union:
- "\<lbrakk>rhs_nonempty rhs; rhs_nonempty rhs'\<rbrakk> \<Longrightarrow> rhs_nonempty (rhs \<union> rhs')"
-by (auto simp:rhs_nonempty_def)
+ "\<lbrakk>ardenable rhs; ardenable rhs'\<rbrakk> \<Longrightarrow> ardenable (rhs \<union> rhs')"
+by (auto simp:ardenable_def)
lemma Arden_keeps_nonempty:
- "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (Arden X rhs)"
+ "ardenable rhs \<Longrightarrow> ardenable (Arden X rhs)"
by (simp only:Arden_def append_keeps_nonempty nonempty_set_sub)
lemma Subst_keeps_nonempty:
- "\<lbrakk>rhs_nonempty rhs; rhs_nonempty xrhs\<rbrakk> \<Longrightarrow> rhs_nonempty (Subst rhs X xrhs)"
+ "\<lbrakk>ardenable rhs; ardenable xrhs\<rbrakk> \<Longrightarrow> ardenable (Subst rhs X xrhs)"
by (simp only:Subst_def append_keeps_nonempty nonempty_set_union nonempty_set_sub)
lemma Subst_keeps_eq:
@@ -869,19 +871,16 @@
by (auto simp:Subst_def append_keeps_finite)
lemma Subst_all_keeps_finite:
- assumes finite:"finite (ES:: (string set \<times> rhs_item set) set)"
+ assumes finite: "finite ES"
shows "finite (Subst_all ES Y yrhs)"
proof -
- have "finite {(Ya, Subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \<in> ES}"
- (is "finite ?A")
- proof-
- 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
- qed
- thus ?thesis by (simp add:Subst_all_def)
+ def eqns \<equiv> "{(X::lang, rhs) |X rhs. (X, rhs) \<in> ES}"
+ def h \<equiv> "\<lambda>(X::lang, rhs). (X, Subst rhs Y yrhs)"
+ have "finite (h ` eqns)" using finite h_def eqns_def by auto
+ moreover
+ have "Subst_all ES Y yrhs = h ` eqns" unfolding h_def eqns_def Subst_all_def by auto
+ ultimately
+ show "finite (Subst_all ES Y yrhs)" by simp
qed
lemma Subst_all_keeps_finite_rhs:
@@ -910,10 +909,9 @@
by (auto simp:rhss_def)
lemma Subst_all_keeps_valid_eqs:
- assumes sc: "valid_eqs (ES \<union> {(Y, yrhs)})" (is "valid_eqs ?A")
- shows "valid_eqs (Subst_all ES Y (Arden Y yrhs))"
- (is "valid_eqs ?B")
-proof-
+ assumes sc: "valid_eqs (ES \<union> {(Y, yrhs)})" (is "valid_eqs ?A")
+ shows "valid_eqs (Subst_all ES Y (Arden Y yrhs))" (is "valid_eqs ?B")
+proof -
{ fix X xrhs'
assume "(X, xrhs') \<in> ?B"
then obtain xrhs
@@ -924,8 +922,7 @@
have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def)
moreover have "rhss xrhs' \<subseteq> lhss ES"
proof-
- have "rhss xrhs' \<subseteq>
- rhss xrhs \<union> rhss (Arden Y yrhs) - {Y}"
+ have "rhss xrhs' \<subseteq> rhss xrhs \<union> rhss (Arden Y yrhs) - {Y}"
proof-
have "Y \<notin> rhss (Arden Y yrhs)"
using Arden_removes_cl by simp
@@ -952,38 +949,38 @@
using invariant_ES by (simp only:invariant_def sound_eqs_def, blast)
have finite_yrhs: "finite yrhs"
using invariant_ES by (auto simp:invariant_def finite_rhs_def)
- have nonempty_yrhs: "rhs_nonempty yrhs"
- using invariant_ES by (auto simp:invariant_def ardenable_def)
+ have nonempty_yrhs: "ardenable yrhs"
+ using invariant_ES by (auto simp:invariant_def ardenable_all_def)
show "sound_eqs (Subst_all ES Y (Arden Y yrhs))"
- proof-
+ proof -
have "Y = L (Arden Y yrhs)"
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
+ unfolding invariant_def ardenable_all_def ardenable_def
apply(auto)
done
thus ?thesis using invariant_ES
- unfolding invariant_def finite_rhs_def2 sound_eqs_def Subst_all_def
+ unfolding invariant_def finite_rhs_def2 sound_eqs_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)
show "distinct_equas (Subst_all ES Y (Arden Y yrhs))"
- using invariant_ES
- by (auto simp:distinct_equas_def Subst_all_def invariant_def)
- show "ardenable (Subst_all ES Y (Arden Y yrhs))"
+ using invariant_ES
+ unfolding distinct_equas_def Subst_all_def invariant_def by auto
+ show "ardenable_all (Subst_all ES Y (Arden Y yrhs))"
proof -
{ fix X rhs
assume "(X, rhs) \<in> ES"
- hence "rhs_nonempty rhs" using prems invariant_ES
- by (auto simp add:invariant_def ardenable_def)
+ hence "ardenable rhs" using prems invariant_ES
+ by (auto simp add:invariant_def ardenable_all_def)
with nonempty_yrhs
- have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))"
+ have "ardenable (Subst rhs Y (Arden Y yrhs))"
by (simp add:nonempty_yrhs
Subst_keeps_nonempty Arden_keeps_nonempty)
- } thus ?thesis by (auto simp add:ardenable_def Subst_all_def)
+ } thus ?thesis by (auto simp add:ardenable_all_def Subst_all_def)
qed
show "finite_rhs (Subst_all ES Y (Arden Y yrhs))"
proof-
@@ -1079,7 +1076,9 @@
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)
+ using Inv_ES
+ thm Subst_all_satisfies_invariant
+ by (rule_tac Subst_all_satisfies_invariant) (simp)
qed
qed
@@ -1124,14 +1123,14 @@
by (auto simp add: iteration_step_invariant iteration_step_ex) }
moreover
{ fix ES
- assume "Inv ES" and "\<not> Cond ES"
- then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant ES"
- unfolding Inv_def invariant_def
- apply (auto, rule_tac x = rhs in exI)
- apply (auto dest!: card_Suc_Diff1 simp: card_eq_0_iff)
- done
- then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant {(X, rhs')}"
- by auto }
+ assume inv: "Inv ES" and not_crd: "\<not>Cond ES"
+ from inv obtain rhs where "(X, rhs) \<in> ES" unfolding Inv_def by auto
+ moreover
+ from not_crd have "card ES = 1" by simp
+ ultimately
+ have "ES = {(X, rhs)}" by (auto simp add: card_Suc_eq)
+ then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant {(X, rhs')}" using inv
+ unfolding Inv_def by auto }
moreover
have "wf (measure card)" by simp
moreover
@@ -1173,7 +1172,7 @@
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
+ unfolding A_def invariant_def ardenable_all_def finite_rhs_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