
diff -r c6ebfe052109 -r edacc141060f Myhill_1.thy
--- 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




