--- a/Myhill_1.thy Thu Jul 28 11:56:25 2011 +0000
+++ b/Myhill_1.thy Thu Jul 28 14:22:10 2011 +0000
@@ -5,7 +5,7 @@
section {* Direction @{text "finite partition \<Rightarrow> regular language"} *}
-lemma Pair_Collect[simp]:
+lemma Pair_Collect [simp]:
shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
by simp
@@ -57,7 +57,6 @@
by (auto)
lemma lang_rhs_union_distrib:
- fixes A B::"('a trm) set"
shows "lang_rhs A \<union> lang_rhs B = lang_rhs (A \<union> B)"
by simp
@@ -350,7 +349,7 @@
subsubsection {* Interation step *}
-lemma Arden_keeps_eq:
+lemma Arden_preserves_soundness:
assumes l_eq_r: "X = lang_rhs rhs"
and not_empty: "ardenable rhs"
and finite: "finite rhs"
@@ -379,37 +378,37 @@
finally show "X = lang_rhs (Arden X rhs)" by simp
qed
-lemma Append_keeps_finite:
+lemma Append_preserves_finite:
"finite rhs \<Longrightarrow> finite (Append_rexp_rhs rhs r)"
by (auto simp: Append_rexp_rhs_def)
-lemma Arden_keeps_finite:
+lemma Arden_preserves_finite:
"finite rhs \<Longrightarrow> finite (Arden X rhs)"
-by (auto simp: Arden_def Append_keeps_finite)
+by (auto simp: Arden_def Append_preserves_finite)
-lemma Append_keeps_nonempty:
+lemma Append_preserves_ardenable:
"ardenable rhs \<Longrightarrow> ardenable (Append_rexp_rhs rhs r)"
apply (auto simp: ardenable_def Append_rexp_rhs_def)
by (case_tac x, auto simp: conc_def)
-lemma nonempty_set_sub:
+lemma ardenable_set_sub:
"ardenable rhs \<Longrightarrow> ardenable (rhs - A)"
by (auto simp:ardenable_def)
-lemma nonempty_set_union:
+lemma ardenable_set_union:
"\<lbrakk>ardenable rhs; ardenable rhs'\<rbrakk> \<Longrightarrow> ardenable (rhs \<union> rhs')"
by (auto simp:ardenable_def)
-lemma Arden_keeps_nonempty:
+lemma Arden_preserves_ardenable:
"ardenable rhs \<Longrightarrow> ardenable (Arden X rhs)"
-by (simp only:Arden_def Append_keeps_nonempty nonempty_set_sub)
+by (simp only:Arden_def Append_preserves_ardenable ardenable_set_sub)
-lemma Subst_keeps_nonempty:
+lemma Subst_preserves_ardenable:
"\<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)
+by (simp only: Subst_def Append_preserves_ardenable ardenable_set_union ardenable_set_sub)
-lemma Subst_keeps_eq:
+lemma Subst_preserves_soundness:
assumes substor: "X = lang_rhs xrhs"
and finite: "finite rhs"
shows "lang_rhs (Subst rhs X xrhs) = lang_rhs rhs" (is "?Left = ?Right")
@@ -433,11 +432,11 @@
ultimately show ?thesis by simp
qed
-lemma Subst_keeps_finite_rhs:
+lemma Subst_preserves_finite_rhs:
"\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (Subst rhs Y yrhs)"
-by (auto simp: Subst_def Append_keeps_finite)
+by (auto simp: Subst_def Append_preserves_finite)
-lemma Subst_all_keeps_finite:
+lemma Subst_all_preserves_finite:
assumes finite: "finite ES"
shows "finite (Subst_all ES Y yrhs)"
proof -
@@ -450,11 +449,11 @@
show "finite (Subst_all ES Y yrhs)" by simp
qed
-lemma Subst_all_keeps_finite_rhs:
+lemma Subst_all_preserves_finite_rhs:
"\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)"
-by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def)
+by (auto intro:Subst_preserves_finite_rhs simp add:Subst_all_def finite_rhs_def)
-lemma append_rhs_keeps_cls:
+lemma append_rhs_preserves_cls:
"rhss (Append_rexp_rhs rhs r) = rhss rhs"
apply (auto simp: rhss_def Append_rexp_rhs_def)
apply (case_tac xa, auto simp: image_def)
@@ -462,20 +461,20 @@
lemma Arden_removes_cl:
"rhss (Arden Y yrhs) = rhss yrhs - {Y}"
-apply (simp add:Arden_def append_rhs_keeps_cls)
+apply (simp add:Arden_def append_rhs_preserves_cls)
by (auto simp: rhss_def)
-lemma lhss_keeps_cls:
+lemma lhss_preserves_cls:
"lhss (Subst_all ES Y yrhs) = lhss ES"
by (auto simp: lhss_def Subst_all_def)
lemma Subst_updates_cls:
"X \<notin> rhss xrhs \<Longrightarrow>
rhss (Subst rhs X xrhs) = rhss rhs \<union> rhss xrhs - {X}"
-apply (simp only:Subst_def append_rhs_keeps_cls rhss_union_distrib)
+apply (simp only:Subst_def append_rhs_preserves_cls rhss_union_distrib)
by (auto simp: rhss_def)
-lemma Subst_all_keeps_validity:
+lemma Subst_all_preserves_validity:
assumes sc: "validity (ES \<union> {(Y, yrhs)})" (is "validity ?A")
shows "validity (Subst_all ES Y (Arden Y yrhs))" (is "validity ?B")
proof -
@@ -516,24 +515,24 @@
using invariant_ES by (simp only:invariant_def soundness_def, blast)
have finite_yrhs: "finite yrhs"
using invariant_ES by (auto simp:invariant_def finite_rhs_def)
- have nonempty_yrhs: "ardenable yrhs"
+ have ardenable_yrhs: "ardenable yrhs"
using invariant_ES by (auto simp:invariant_def ardenable_all_def)
show "soundness (Subst_all ES Y (Arden Y yrhs))"
proof -
have "Y = lang_rhs (Arden Y yrhs)"
using Y_eq_yrhs invariant_ES finite_yrhs
using finite_Trn[OF finite_yrhs]
- apply(rule_tac Arden_keeps_eq)
+ apply(rule_tac Arden_preserves_soundness)
apply(simp_all)
unfolding invariant_def ardenable_all_def ardenable_def
apply(auto)
done
thus ?thesis using invariant_ES
unfolding invariant_def finite_rhs_def2 soundness_def Subst_all_def
- by (auto simp add: Subst_keeps_eq simp del: lang_rhs.simps)
+ by (auto simp add: Subst_preserves_soundness simp del: lang_rhs.simps)
qed
show "finite (Subst_all ES Y (Arden Y yrhs))"
- using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
+ using invariant_ES by (simp add:invariant_def Subst_all_preserves_finite)
show "distinctness (Subst_all ES Y (Arden Y yrhs))"
using invariant_ES
unfolding distinctness_def Subst_all_def invariant_def by auto
@@ -543,10 +542,10 @@
assume "(X, rhs) \<in> ES"
hence "ardenable rhs" using invariant_ES
by (auto simp add:invariant_def ardenable_all_def)
- with nonempty_yrhs
+ with ardenable_yrhs
have "ardenable (Subst rhs Y (Arden Y yrhs))"
- by (simp add:nonempty_yrhs
- Subst_keeps_nonempty Arden_keeps_nonempty)
+ by (simp add:ardenable_yrhs
+ Subst_preserves_ardenable Arden_preserves_ardenable)
} thus ?thesis by (auto simp add:ardenable_all_def Subst_all_def)
qed
show "finite_rhs (Subst_all ES Y (Arden Y yrhs))"
@@ -557,13 +556,13 @@
proof -
have "finite yrhs" using invariant_ES
by (auto simp:invariant_def finite_rhs_def)
- thus ?thesis using Arden_keeps_finite by auto
+ thus ?thesis using Arden_preserves_finite by auto
qed
ultimately show ?thesis
- by (simp add:Subst_all_keeps_finite_rhs)
+ by (simp add:Subst_all_preserves_finite_rhs)
qed
show "validity (Subst_all ES Y (Arden Y yrhs))"
- using invariant_ES Subst_all_keeps_validity by (auto simp add: invariant_def)
+ using invariant_ES Subst_all_preserves_validity by (auto simp add: invariant_def)
qed
lemma Remove_in_card_measure:
@@ -734,14 +733,14 @@
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
+ using Arden_preserves_finite by auto
then have fin: "finite {r. Lam r \<in> A}" by (rule finite_Lam)
have "X = lang_rhs xrhs" using Inv_ES unfolding invariant_def soundness_def
by simp
then have "X = lang_rhs A" using Inv_ES
unfolding A_def invariant_def ardenable_all_def finite_rhs_def
- by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn)
+ by (rule_tac Arden_preserves_soundness) (simp_all add: finite_Trn)
then have "X = lang_rhs {Lam r | r. Lam r \<in> A}" using eq by simp
then have "X = lang (\<Uplus>{r. Lam r \<in> A})" using fin by auto
then show "\<exists>r. X = lang r" by blast