
diff -r 5fed809d0fc1 -r f460d5f75cb5 Myhill_1.thy
--- a/Myhill_1.thy	Mon Feb 14 11:12:01 2011 +0000
+++ b/Myhill_1.thy	Mon Feb 14 23:10:44 2011 +0000
@@ -528,12 +528,17 @@
 definition 
   "ardenable ES \<equiv> \<forall>(X, rhs) \<in> ES. rhs_nonempty rhs"
 
+
 text {* 
   @{text "finite_rhs ES"} requires every equation in @{text "rhs"} 
   be finite.
 *}
 definition
-  "finite_rhs ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs"
+  "finite_rhs ES \<equiv> \<forall>(X, rhs) \<in> ES. finite rhs"
+
+lemma finite_rhs_def2:
+  "finite_rhs ES = (\<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> finite rhs)"
+unfolding finite_rhs_def by auto
 
 text {*
   @{text "classes_of rhs"} returns all variables (or equivalent classes)
@@ -548,22 +553,26 @@
   equational system @{text "ES"}.
 *}
 definition
-  "lefts_of ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"
+  "lhss ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}"
 
 text {*
   The following @{text "self_contained 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> lefts_of ES"
+  "self_contained ES \<equiv> \<forall>(X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lhss ES"
 
 
 text {*
   The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints.
   *}
 definition 
-  "invariant ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> 
-                  finite_rhs ES \<and> self_contained ES"
+  "invariant ES \<equiv> finite ES
+                \<and> finite_rhs ES
+                \<and> valid_eqns ES 
+                \<and> distinct_equas ES 
+                \<and> ardenable ES 
+                \<and> self_contained ES"
 
 
 lemma invariantI:
@@ -645,9 +654,9 @@
   shows "classes_of (A \<union> B) = classes_of A \<union> classes_of B"
 by (auto simp add: classes_of_def)
 
-lemma lefts_of_union_distrib:
-  shows "lefts_of (A \<union> B) = lefts_of A \<union> lefts_of B"
-by (auto simp add: lefts_of_def)
+lemma lhss_union_distrib:
+  shows "lhss (A \<union> B) = lhss A \<union> lhss B"
+by (auto simp add: lhss_def)
 
 
 subsubsection {* Intialization *}
@@ -760,12 +769,12 @@
     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
-    by auto
+   by auto 
   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 lefts_of_def
+    unfolding self_contained_def Init_def Init_rhs_def classes_of_def lhss_def
     by auto
 qed
 
@@ -892,9 +901,9 @@
 apply (simp add:Arden_def append_rhs_keeps_cls)
 by (auto simp:classes_of_def)
 
-lemma lefts_of_keeps_cls:
-  "lefts_of (Subst_all ES Y yrhs) = lefts_of ES"
-by (auto simp:lefts_of_def Subst_all_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> 
@@ -912,10 +921,10 @@
     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> lefts_of ?B"
+    have "classes_of xrhs' \<subseteq> lhss ?B"
     proof-
-      have "lefts_of ?B = lefts_of ES" by (auto simp add:lefts_of_def Subst_all_def)
-      moreover have "classes_of xrhs' \<subseteq> lefts_of ES"
+      have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def)
+      moreover have "classes_of xrhs' \<subseteq> lhss ES"
       proof-
         have "classes_of xrhs' \<subseteq> 
                         classes_of xrhs \<union> classes_of (Arden Y yrhs) - {Y}"
@@ -924,12 +933,12 @@
             using Arden_removes_cl by simp
           thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls)
         qed
-        moreover have "classes_of xrhs \<subseteq> lefts_of ES \<union> {Y}" using X_in sc
-          apply (simp only:self_contained_def lefts_of_union_distrib)
-          by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def)
-        moreover have "classes_of (Arden Y yrhs) \<subseteq> lefts_of ES \<union> {Y}" 
+        moreover have "classes_of xrhs \<subseteq> lhss ES \<union> {Y}" using X_in sc
+          apply (simp only:self_contained_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}" 
           using sc 
-          by (auto simp add:Arden_removes_cl self_contained_def lefts_of_def)
+          by (auto simp add:Arden_removes_cl self_contained_def lhss_def)
         ultimately show ?thesis by auto
       qed
       ultimately show ?thesis by simp
@@ -950,12 +959,16 @@
   show "valid_eqns (Subst_all ES Y (Arden Y yrhs))"
   proof-
     have "Y = L (Arden Y yrhs)" 
-      using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs
-      by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+)
-    thus ?thesis using invariant_ES 
-      by (auto simp add:valid_eqns_def 
-        Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def
-        simp del:L_rhs.simps)
+      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
+      apply(auto)
+      done
+    thus ?thesis using invariant_ES
+      unfolding  invariant_def finite_rhs_def2 valid_eqns_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)
@@ -1015,27 +1028,24 @@
 by (auto simp: Subst_all_def)
 
 lemma card_noteq_1_has_more:
-  assumes card:"card S \<noteq> 1"
-  and e_in: "e \<in> S"
-  and finite: "finite S"
-  obtains e' where "e' \<in> S \<and> e \<noteq> e'"
+  assumes card:"Cond ES"
+  and e_in: "(X, xrhs) \<in> ES"
+  and finite: "finite ES"
+  shows "\<exists>(Y, yrhs) \<in> ES. (X, xrhs) \<noteq> (Y, yrhs)"
 proof-
-  have "card (S - {e}) > 0"
-  proof -
-    have "card S > 1" using card e_in finite 
-      by (cases "card S") (auto) 
-    thus ?thesis using finite e_in by auto
-  qed
-  hence "S - {e} \<noteq> {}" using finite by (rule_tac notI, simp)
-  thus "(\<And>e'. e' \<in> S \<and> e \<noteq> e' \<Longrightarrow> thesis) \<Longrightarrow> thesis" by auto
+  have "card ES > 1" using card e_in finite 
+    by (cases "card ES") (auto) 
+  then have "card (ES - {(X, xrhs)}) > 0"
+    using finite e_in by auto
+  then have "(ES - {(X, xrhs)}) \<noteq> {}" using finite by (rule_tac notI, simp)
+  then show "\<exists>(Y, yrhs) \<in> ES. (X, xrhs) \<noteq> (Y, yrhs)"
+    by auto
 qed
 
-
-
 lemma iteration_step_measure:
   assumes Inv_ES: "invariant ES"
   and    X_in_ES: "(X, xrhs) \<in> ES"
-  and    not_T: "card ES \<noteq> 1"
+  and    not_T: "Cond ES "
   shows "(Iter X ES, ES) \<in> measure card"
 proof -
   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
@@ -1043,8 +1053,8 @@
     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
     using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
   then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"  
-    using X_in_ES Inv_ES 
-    by (auto simp: invariant_def distinct_equas_def)
+    using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
+    by auto
   then show "(Iter X ES, ES) \<in> measure card" 
   apply(rule IterI2)
   apply(rule Remove_in_card_measure)
@@ -1055,16 +1065,16 @@
 lemma iteration_step_invariant:
   assumes Inv_ES: "invariant ES"
   and    X_in_ES: "(X, xrhs) \<in> ES"
-  and    not_T: "card ES \<noteq> 1"
+  and    not_T: "Cond ES"
   shows "invariant (Iter X ES)"
 proof -
   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
   then obtain Y yrhs 
     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
     using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
-  then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"  
-    using X_in_ES Inv_ES 
-    by (auto simp: invariant_def distinct_equas_def)
+  then have "(Y, yrhs) \<in> ES" "X \<noteq> Y" 
+    using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
+    by auto
   then show "invariant (Iter X ES)" 
   proof(rule IterI2)
     fix Y yrhs
@@ -1078,7 +1088,7 @@
 lemma iteration_step_ex:
   assumes Inv_ES: "invariant ES"
   and    X_in_ES: "(X, xrhs) \<in> ES"
-  and    not_T: "card ES \<noteq> 1"
+  and    not_T: "Cond ES"
   shows "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)"
 proof -
   have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def)
@@ -1086,8 +1096,8 @@
     where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" 
     using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto)
   then have "(Y, yrhs) \<in> ES " "X \<noteq> Y"  
-    using X_in_ES Inv_ES 
-    by (auto simp: invariant_def distinct_equas_def)
+    using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def
+    by auto
   then show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" 
   apply(rule IterI2)
   unfolding Remove_def
@@ -1100,49 +1110,44 @@
 
 subsubsection {* Conclusion of the proof *}
 
-text {*
-  From this point until @{text "hard_direction"}, the hard direction is proved
-  through a simple application of the iteration principle.
-*}
-
-
-lemma reduce_x:
-  assumes inv: "invariant ES"
-  and contain_x: "(X, xrhs) \<in> ES" 
-  shows "\<exists> xrhs'. Solve X ES = {(X, xrhs')} \<and> invariant(Solve X ES)"
+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)}"
 proof -
-  let ?Inv = "\<lambda> ES. (invariant ES \<and> (\<exists> xrhs. (X, xrhs) \<in> ES))"
-  show ?thesis unfolding Solve_def
-  proof (rule while_rule [where P = ?Inv and r = "measure card"])
-    from inv and contain_x show "?Inv ES" by auto
-  next
-    show "wf (measure card)" by simp
-  next
-    fix ES
-    assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
-    then show "(Iter X ES, ES) \<in> measure card"
+  def Inv \<equiv> "\<lambda>ES. invariant ES \<and> (\<exists>xrhs. (X, xrhs) \<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
+  { fix ES
+    assume inv: "Inv ES" and crd: "Cond ES"
+    then have "Inv (Iter X ES)"
+      unfolding Inv_def
+      by (auto simp add: iteration_step_invariant iteration_step_ex) }
+  moreover
+  { fix ES
+    assume "Inv ES" and "\<not> Cond ES"
+    then have "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant ES"
+      unfolding Inv_def invariant_def
+      apply (auto, rule_tac x = xrhs 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')}"
+      by auto }
+  moreover
+    have "wf (measure card)" by simp
+  moreover
+  { fix ES
+    assume inv: "Inv ES" and crd: "Cond ES"
+    then have "(Iter X ES, ES) \<in> measure card"
+      unfolding Inv_def
       apply(clarify)
-      apply(rule iteration_step_measure)
-      apply(auto)
-      done
-  next
-    fix ES
-    assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
-    then show "?Inv (Iter X ES)"
-      apply -
-      apply(auto)
-      apply(rule iteration_step_invariant)
+      apply(rule_tac iteration_step_measure)
       apply(auto)
-      apply(rule iteration_step_ex)
-      apply(auto)
-      done
-  next
-    fix ES
-    assume "?Inv ES" and "\<not> card ES \<noteq> 1"
-    thus "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant ES"
-      apply (auto, rule_tac x = xrhs in exI)
-      by (auto simp: invariant_def dest!:card_Suc_Diff1 simp:card_eq_0_iff) 
-  qed
+      done }
+  ultimately 
+  show "\<exists>xrhs. Solve X (Init (UNIV // \<approx>A)) = {(X, xrhs)} \<and> invariant {(X, xrhs)}" 
+    unfolding Solve_def by (rule while_rule)
 qed
 
 lemma last_cl_exists_rexp:
@@ -1153,7 +1158,7 @@
   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 lefts_of_def
+      unfolding A_def self_contained_def invariant_def lhss_def
       by (simp add: Arden_removes_cl) 
     thus ?thesis unfolding A_def classes_of_def
       apply(auto simp only:)
@@ -1190,20 +1195,13 @@
   and X_in_CS: "X \<in> (UNIV // \<approx>A)"
   shows "\<exists>r::rexp. L r = X"
 proof -
-  def ES \<equiv> "Init (UNIV // \<approx>A)"
-  have "invariant ES" using finite_CS unfolding ES_def
-    by (rule Init_ES_satisfies_invariant)
-  moreover
-  from X_in_CS obtain xrhs where "(X, xrhs) \<in> ES" unfolding ES_def
-    unfolding Init_def Init_rhs_def by auto
-  ultimately
-  obtain xrhs' where "Solve X ES = {(X, xrhs')}" "invariant (Solve X ES)"
-    using reduce_x by blast
+  from finite_CS X_in_CS 
+  obtain xrhs where "invariant {(X, xrhs)}"
+    using Solve by metis
   then show "\<exists>r::rexp. L r = X"
-  using last_cl_exists_rexp by auto
+    using last_cl_exists_rexp by auto
 qed
 
-
 lemma bchoice_finite_set:
   assumes a: "\<forall>x \<in> S. \<exists>y. x = f y" 
   and     b: "finite S"




