
diff -r 79b37ef9505f -r e500cab16be4 Myhill_1.thy
--- 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




