
diff -r f460d5f75cb5 -r 5bd73aa805a7 Myhill_1.thy
--- a/Myhill_1.thy	Mon Feb 14 23:10:44 2011 +0000
+++ b/Myhill_1.thy	Tue Feb 15 08:08:04 2011 +0000
@@ -509,7 +509,7 @@
 *}
 
 definition 
-  "valid_eqns ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
+  "sound_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
 
 text {*
   @{text "rhs_nonempty rhs"} requires regular expressions occuring in 
@@ -546,7 +546,7 @@
   *}
 
 definition 
-  "classes_of rhs \<equiv> {X | X r. Trn X r \<in> rhs}"
+  "rhss rhs \<equiv> {X | X r. Trn X r \<in> rhs}"
 
 text {*
   @{text "lefts_of ES"} returns all variables defined by an 
@@ -556,11 +556,11 @@
   "lhss ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"
 
 text {*
-  The following @{text "self_contained ES"} requires that every variable occuring 
+  The following @{text "valid_eqs ES"} requires that every variable occuring 
   on the right hand side of equations is already defined by some equation in @{text "ES"}.
 *}
 definition 
-  "self_contained ES \<equiv> \<forall>(X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lhss ES"
+  "valid_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. rhss rhs \<subseteq> lhss ES"
 
 
 text {*
@@ -569,15 +569,15 @@
 definition 
   "invariant ES \<equiv> finite ES
                 \<and> finite_rhs ES
-                \<and> valid_eqns ES 
+                \<and> sound_eqs ES 
                 \<and> distinct_equas ES 
                 \<and> ardenable ES 
-                \<and> self_contained ES"
+                \<and> valid_eqs ES"
 
 
 lemma invariantI:
-  assumes "valid_eqns ES" "finite ES" "distinct_equas ES" "ardenable ES" 
-          "finite_rhs ES" "self_contained ES"
+  assumes "sound_eqs ES" "finite ES" "distinct_equas ES" "ardenable ES" 
+          "finite_rhs ES" "valid_eqs ES"
   shows "invariant ES"
 using assms by (simp add: invariant_def)
 
@@ -650,9 +650,9 @@
 unfolding append_rhs_rexp_def
 by (auto simp add: Seq_def lang_of_append)
 
-lemma classes_of_union_distrib:
-  shows "classes_of (A \<union> B) = classes_of A \<union> classes_of B"
-by (auto simp add: classes_of_def)
+lemma rhss_union_distrib:
+  shows "rhss (A \<union> B) = rhss A \<union> rhss B"
+by (auto simp add: rhss_def)
 
 lemma lhss_union_distrib:
   shows "lhss (A \<union> B) = lhss A \<union> lhss B"
@@ -760,8 +760,8 @@
   assumes finite_CS: "finite (UNIV // \<approx>A)"
   shows "invariant (Init (UNIV // \<approx>A))"
 proof (rule invariantI)
-  show "valid_eqns (Init (UNIV // \<approx>A))"
-    unfolding valid_eqns_def 
+  show "sound_eqs (Init (UNIV // \<approx>A))"
+    unfolding sound_eqs_def 
     using l_eq_r_in_eqs by auto
   show "finite (Init (UNIV // \<approx>A))" using finite_CS
     unfolding Init_def by simp
@@ -773,8 +773,8 @@
   show "finite_rhs (Init (UNIV // \<approx>A))"
     using finite_Init_rhs[OF finite_CS]
     unfolding finite_rhs_def Init_def by auto
-  show "self_contained (Init (UNIV // \<approx>A))"
-    unfolding self_contained_def Init_def Init_rhs_def classes_of_def lhss_def
+  show "valid_eqs (Init (UNIV // \<approx>A))"
+    unfolding valid_eqs_def Init_def Init_rhs_def rhss_def lhss_def
     by auto
 qed
 
@@ -891,59 +891,59 @@
 by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def)
 
 lemma append_rhs_keeps_cls:
-  "classes_of (append_rhs_rexp rhs r) = classes_of rhs"
-apply (auto simp:classes_of_def append_rhs_rexp_def)
+  "rhss (append_rhs_rexp rhs r) = rhss rhs"
+apply (auto simp:rhss_def append_rhs_rexp_def)
 apply (case_tac xa, auto simp:image_def)
 by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+)
 
 lemma Arden_removes_cl:
-  "classes_of (Arden Y yrhs) = classes_of yrhs - {Y}"
+  "rhss (Arden Y yrhs) = rhss yrhs - {Y}"
 apply (simp add:Arden_def append_rhs_keeps_cls)
-by (auto simp:classes_of_def)
+by (auto simp:rhss_def)
 
 lemma lhss_keeps_cls:
   "lhss (Subst_all ES Y yrhs) = lhss ES"
 by (auto simp:lhss_def Subst_all_def)
 
 lemma Subst_updates_cls:
-  "X \<notin> classes_of xrhs \<Longrightarrow> 
-      classes_of (Subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
-apply (simp only:Subst_def append_rhs_keeps_cls classes_of_union_distrib)
-by (auto simp:classes_of_def)
+  "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)
+by (auto simp:rhss_def)
 
-lemma Subst_all_keeps_self_contained:
-  assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A")
-  shows "self_contained (Subst_all ES Y (Arden Y yrhs))" 
-                                                   (is "self_contained ?B")
+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-
   { fix X xrhs'
     assume "(X, xrhs') \<in> ?B"
     then obtain xrhs 
       where xrhs_xrhs': "xrhs' = Subst xrhs Y (Arden Y yrhs)"
       and X_in: "(X, xrhs) \<in> ES" by (simp add:Subst_all_def, blast)    
-    have "classes_of xrhs' \<subseteq> lhss ?B"
+    have "rhss xrhs' \<subseteq> lhss ?B"
     proof-
       have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def)
-      moreover have "classes_of xrhs' \<subseteq> lhss ES"
+      moreover have "rhss xrhs' \<subseteq> lhss ES"
       proof-
-        have "classes_of xrhs' \<subseteq> 
-                        classes_of xrhs \<union> classes_of (Arden Y yrhs) - {Y}"
+        have "rhss xrhs' \<subseteq> 
+                        rhss xrhs \<union> rhss (Arden Y yrhs) - {Y}"
         proof-
-          have "Y \<notin> classes_of (Arden Y yrhs)" 
+          have "Y \<notin> rhss (Arden Y yrhs)" 
             using Arden_removes_cl by simp
           thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls)
         qed
-        moreover have "classes_of xrhs \<subseteq> lhss ES \<union> {Y}" using X_in sc
-          apply (simp only:self_contained_def lhss_union_distrib)
+        moreover have "rhss xrhs \<subseteq> lhss ES \<union> {Y}" using X_in sc
+          apply (simp only:valid_eqs_def lhss_union_distrib)
           by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lhss_def)
-        moreover have "classes_of (Arden Y yrhs) \<subseteq> lhss ES \<union> {Y}" 
+        moreover have "rhss (Arden Y yrhs) \<subseteq> lhss ES \<union> {Y}" 
           using sc 
-          by (auto simp add:Arden_removes_cl self_contained_def lhss_def)
+          by (auto simp add:Arden_removes_cl valid_eqs_def lhss_def)
         ultimately show ?thesis by auto
       qed
       ultimately show ?thesis by simp
     qed
-  } thus ?thesis by (auto simp only:Subst_all_def self_contained_def)
+  } thus ?thesis by (auto simp only:Subst_all_def valid_eqs_def)
 qed
 
 lemma Subst_all_satisfies_invariant:
@@ -951,12 +951,12 @@
   shows "invariant (Subst_all ES Y (Arden Y yrhs))"
 proof (rule invariantI)
   have Y_eq_yrhs: "Y = L yrhs" 
-    using invariant_ES by (simp only:invariant_def valid_eqns_def, blast)
+    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)
-  show "valid_eqns (Subst_all ES Y (Arden Y yrhs))"
+  show "sound_eqs (Subst_all ES Y (Arden Y yrhs))"
   proof-
     have "Y = L (Arden Y yrhs)" 
       using Y_eq_yrhs invariant_ES finite_yrhs
@@ -967,7 +967,7 @@
       apply(auto)
       done
     thus ?thesis using invariant_ES
-      unfolding  invariant_def finite_rhs_def2 valid_eqns_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))" 
@@ -1000,8 +1000,8 @@
     ultimately show ?thesis 
       by (simp add:Subst_all_keeps_finite_rhs)
   qed
-  show "self_contained (Subst_all ES Y (Arden Y yrhs))"
-    using invariant_ES Subst_all_keeps_self_contained by (simp add:invariant_def)
+  show "valid_eqs (Subst_all ES Y (Arden Y yrhs))"
+    using invariant_ES Subst_all_keeps_valid_eqs by (simp add:invariant_def)
 qed
 
 lemma Remove_in_card_measure:
@@ -1113,9 +1113,9 @@
 lemma Solve:
   assumes fin: "finite (UNIV // \<approx>A)"
   and     X_in: "X \<in> (UNIV // \<approx>A)"
-  shows "\<exists>xrhs. Solve X (Init (UNIV // \<approx>A)) = {(X, xrhs)} \<and> invariant {(X, xrhs)}"
+  shows "\<exists>rhs. Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)} \<and> invariant {(X, rhs)}"
 proof -
-  def Inv \<equiv> "\<lambda>ES. invariant ES \<and> (\<exists>xrhs. (X, xrhs) \<in> ES)"
+  def Inv \<equiv> "\<lambda>ES. invariant ES \<and> (\<exists>rhs. (X, rhs) \<in> ES)"
   have "Inv (Init (UNIV // \<approx>A))" unfolding Inv_def
       using fin X_in by (simp add: Init_ES_satisfies_invariant, simp add: Init_def)
   moreover
@@ -1127,12 +1127,12 @@
   moreover
   { fix ES
     assume "Inv ES" and "\<not> Cond ES"
-    then have "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant ES"
+    then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant ES"
       unfolding Inv_def invariant_def
-      apply (auto, rule_tac x = xrhs in exI)
+      apply (auto, rule_tac x = rhs in exI)
       apply (auto dest!: card_Suc_Diff1 simp: card_eq_0_iff) 
       done
-    then have "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant {(X, xrhs')}"
+    then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant {(X, rhs')}"
       by auto }
   moreover
     have "wf (measure card)" by simp
@@ -1146,7 +1146,7 @@
       apply(auto)
       done }
   ultimately 
-  show "\<exists>xrhs. Solve X (Init (UNIV // \<approx>A)) = {(X, xrhs)} \<and> invariant {(X, xrhs)}" 
+  show "\<exists>rhs. Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)} \<and> invariant {(X, rhs)}" 
     unfolding Solve_def by (rule while_rule)
 qed
 
@@ -1157,10 +1157,10 @@
   def A \<equiv> "Arden X xrhs"
   have eq: "{Lam r | r. Lam r \<in> A} = A"
   proof -
-    have "classes_of A = {}" using Inv_ES 
-      unfolding A_def self_contained_def invariant_def lhss_def
+    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 classes_of_def
+    thus ?thesis unfolding A_def rhss_def
       apply(auto simp only:)
       apply(case_tac x)
       apply(auto)
@@ -1174,7 +1174,7 @@
   also have "\<dots> = L A" by (simp add: eq)
   also have "\<dots> = X" 
   proof -
-    have "X = L xrhs" using Inv_ES unfolding invariant_def valid_eqns_def
+    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})"




