diff -r 97b783438316 -r 37ab56205097 Myhill_1.thy
--- a/Myhill_1.thy	Wed Feb 09 09:46:59 2011 +0000
+++ b/Myhill_1.thy	Wed Feb 09 12:34:30 2011 +0000
@@ -1,5 +1,5 @@
 theory Myhill_1
-imports Main Folds
+imports Main Folds While_Combinator
 begin
 
 section {* Preliminary definitions *}
@@ -442,47 +442,43 @@
   "subst_op_all ES X xrhs \<equiv> {(Y, subst_op yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
 
 
-section {* Well-founded iteration *}
+section {* While-combinator *}
 
 text {*
-  The computation of regular expressions for equivalence classes is accomplished
-  using a iteration principle given by the following lemma.
+  The following term @{text "remove ES Y yrhs"} removes the equation
+  @{text "Y = yrhs"} from equational system @{text "ES"} by replacing
+  all occurences of @{text "Y"} by its definition (using @{text "eqs_subst"}).
+  The @{text "Y"}-definition is made non-recursive using Arden's transformation
+  @{text "arden_variate Y yrhs"}.
+  *}
+
+definition
+  "remove_op ES Y yrhs \<equiv> 
+      subst_op_all  (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)"
+
+text {*
+  The following term @{text "iterm X ES"} represents one iteration in the while loop.
+  It arbitrarily chooses a @{text "Y"} different from @{text "X"} to remove.
 *}
 
-lemma wf_iter [rule_format]: 
-  fixes f
-  assumes step: "\<And> e. \<lbrakk>P e; \<not> Q e\<rbrakk> \<Longrightarrow> (\<exists> e'. P e' \<and>  (f(e'), f(e)) \<in> less_than)"
-  shows pe:     "P e \<longrightarrow> (\<exists> e'. P e' \<and>  Q e')"
-proof(induct e rule: wf_induct 
-           [OF wf_inv_image[OF wf_less_than, where f = "f"]], clarify)
-  fix x 
-  assume h [rule_format]: 
-    "\<forall>y. (y, x) \<in> inv_image less_than f \<longrightarrow> P y \<longrightarrow> (\<exists>e'. P e' \<and> Q e')"
-    and px: "P x"
-  show "\<exists>e'. P e' \<and> Q e'"
-  proof(cases "Q x")
-    assume "Q x" with px show ?thesis by blast
-  next
-    assume nq: "\<not> Q x"
-    from step [OF px nq]
-    obtain e' where pe': "P e'" and ltf: "(f e', f x) \<in> less_than" by auto
-    show ?thesis
-    proof(rule h)
-      from ltf show "(e', x) \<in> inv_image less_than f" 
-	by (simp add:inv_image_def)
-    next
-      from pe' show "P e'" .
-    qed
-  qed
-qed
+definition 
+  "iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> (X \<noteq> Y)
+                in remove_op ES Y yrhs)"
 
 text {*
-  The @{text "P"} in lemma @{text "wf_iter"} is an invariant kept throughout the iteration procedure.
-  The particular invariant used to solve our problem is defined by function @{text "Inv(ES)"},
-  an invariant over equal system @{text "ES"}.
-  Every definition starting next till @{text "Inv"} stipulates a property to be satisfied by @{text "ES"}.
+  The following term @{text "reduce X ES"} repeatedly removes characteriztion equations
+  for unknowns other than @{text "X"} until one is left.
 *}
 
+definition 
+  "reduce X ES \<equiv> while (\<lambda> ES. card ES \<noteq> 1) (iter X) ES"
+
+text {*
+  Since the @{text "while"} combinator from HOL library is used to implement @{text "reduce X ES"},
+  the induction principle @{thm [source] while_rule} is used to proved the desired properties
+  of @{text "reduce X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
+  in terms of a series of auxilliary predicates:
+*}
 
 section {* Invariants *}
 
@@ -757,14 +753,11 @@
   ultimately show ?thesis by (simp add:invariant_def)
 qed
 
-subsubsection {* 
-  Interation step
-  *}
+subsubsection {* Interation step *}
 
 text {*
-  From this point until @{text "iteration_step"}, it is proved
-  that there exists iteration steps which keep @{text "invariant(ES)"} while
-  decreasing the size of @{text "ES"}.
+  From this point until @{text "iteration_step"}, 
+  the correctness of the iteration step @{text "iter X ES"} is proved.
 *}
 
 lemma arden_op_keeps_eq:
@@ -1019,66 +1012,118 @@
   thus "(\<And>e'. e' \<in> S \<and> e \<noteq> e' \<Longrightarrow> thesis) \<Longrightarrow> thesis" by auto
 qed
 
-lemma iteration_step: 
-  assumes invariant_ES: "invariant ES"
+lemma iteration_step:
+  assumes Inv_ES: "invariant ES"
   and    X_in_ES: "(X, xrhs) \<in> ES"
   and    not_T: "card ES \<noteq> 1"
-  shows "\<exists> ES'. (invariant ES' \<and> (\<exists> xrhs'.(X, xrhs') \<in> ES')) \<and> 
-                (card ES', card ES) \<in> less_than" (is "\<exists> ES'. ?P ES'")
+  shows "(invariant (iter X ES) \<and> (\<exists> xrhs'.(X, xrhs') \<in> (iter X ES)) \<and> 
+                (iter X ES, ES) \<in> measure card)"
 proof -
-  have finite_ES: "finite ES" using invariant_ES by (simp add:invariant_def)
+  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)
-  def ES' == "ES - {(Y, yrhs)}"
-  let ?ES'' = "subst_op_all ES' Y (arden_op Y yrhs)"
-  have "?P ?ES''"
-  proof -
-    have "invariant ?ES''" using Y_in_ES invariant_ES
-      by (rule_tac subst_op_all_satisfy_invariant, simp add:ES'_def insert_absorb)
-    moreover have "\<exists>xrhs'. (X, xrhs') \<in> ?ES''"  using not_eq X_in_ES
-      by (rule_tac ES = ES' in subst_op_all_cls_remains, auto simp add:ES'_def)
-    moreover have "(card ?ES'', card ES) \<in> less_than" 
-    proof -
-      have "finite ES'" using finite_ES ES'_def by auto
-      moreover have "card ES' < card ES" using finite_ES Y_in_ES
-        by (auto simp:ES'_def card_gt_0_iff intro:diff_Suc_less)
-      ultimately show ?thesis 
-        by (auto dest:subst_op_all_card_le elim:le_less_trans)
+  let ?ES' = "iter X ES"
+  show ?thesis
+  proof(unfold iter_def remove_op_def, rule someI2 [where a = "(Y, yrhs)"], clarsimp)
+    from X_in_ES Y_in_ES and not_eq and Inv_ES
+    show "(Y, yrhs) \<in> ES \<and> X \<noteq> Y"
+      by (auto simp: invariant_def distinct_equas_def)
+  next
+    fix x
+    let ?ES' = "let (Y, yrhs) = x in subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)"
+    assume prem: "case x of (Y, yrhs) \<Rightarrow> (Y, yrhs) \<in> ES \<and> (X \<noteq> Y)"
+    thus "invariant (?ES') \<and> (\<exists>xrhs'. (X, xrhs') \<in> ?ES') \<and> (?ES', ES) \<in> measure card"
+    proof(cases "x", simp)
+      fix Y yrhs
+      assume h: "(Y, yrhs) \<in> ES \<and>  X \<noteq> Y" 
+      show "invariant (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \<and>
+             (\<exists>xrhs'. (X, xrhs') \<in> subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \<and>
+             card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) < card ES"
+      proof -
+        have "invariant (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs))" 
+        proof(rule subst_op_all_satisfy_invariant)
+          from h have "(Y, yrhs) \<in> ES" by simp
+          hence "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto
+          with Inv_ES show "invariant (ES - {(Y, yrhs)} \<union> {(Y, yrhs)})" by auto
+        qed
+        moreover have 
+          "(\<exists>xrhs'. (X, xrhs') \<in> subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs))"
+        proof(rule subst_op_all_cls_remains)
+          from X_in_ES and h
+          show "(X, xrhs) \<in> ES - {(Y, yrhs)}" by auto
+        qed
+        moreover have 
+          "card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) < card ES"
+        proof(rule le_less_trans)
+          show 
+            "card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \<le> 
+                                                                card (ES - {(Y, yrhs)})"
+          proof(rule subst_op_all_card_le)
+            show "finite (ES - {(Y, yrhs)})" using finite_ES by auto
+          qed
+        next
+          show "card (ES - {(Y, yrhs)}) < card ES" using finite_ES h
+            by (auto simp:card_gt_0_iff intro:diff_Suc_less)
+        qed
+        ultimately show ?thesis 
+          by (auto dest: subst_op_all_card_le elim:le_less_trans)
+      qed
     qed
-    ultimately show ?thesis by simp
   qed
-  thus ?thesis by blast
 qed
 
-subsubsection {*
-  Conclusion of the proof
-  *}
+
+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 iteration_conc: 
-  assumes history: "invariant ES"
-  and    X_in_ES: "\<exists> xrhs. (X, xrhs) \<in> ES"
-  shows 
-  "\<exists> ES'. (invariant ES' \<and> (\<exists> xrhs'. (X, xrhs') \<in> ES')) \<and> card ES' = 1" 
-                                                          (is "\<exists> ES'. ?P ES'")
-proof (cases "card ES = 1")
-  case True
-  thus ?thesis using history X_in_ES
-    by blast
-next
-  case False  
-  thus ?thesis using history iteration_step X_in_ES
-    by (rule_tac f = card in wf_iter, auto)
+lemma reduce_x:
+  assumes inv: "invariant ES"
+  and contain_x: "(X, xrhs) \<in> ES" 
+  shows "\<exists> xrhs'. reduce X ES = {(X, xrhs')} \<and> invariant(reduce X ES)"
+proof -
+  let ?Inv = "\<lambda> ES. (invariant ES \<and> (\<exists> xrhs. (X, xrhs) \<in> ES))"
+  show ?thesis
+  proof (unfold reduce_def, 
+         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"
+    show "(iter X ES, ES) \<in> measure card"
+    proof -
+      from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto
+      from inv have "invariant ES" by simp
+      from iteration_step [OF this x_in crd]
+      show ?thesis by auto
+    qed
+  next
+    fix ES
+    assume inv: "?Inv ES" and crd: "card ES \<noteq> 1"
+    thus "?Inv (iter X ES)" 
+    proof -
+      from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto
+      from inv have "invariant ES" by simp
+      from iteration_step [OF this x_in crd]
+      show ?thesis by auto
+    qed
+  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
 qed
-  
+
 lemma last_cl_exists_rexp:
-  assumes ES_single: "ES = {(X, xrhs)}" 
-  and invariant_ES: "invariant ES"
+  assumes Inv_ES: "invariant {(X, xrhs)}"
   shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r")
 proof-
   def A \<equiv> "arden_op X xrhs"
@@ -1088,7 +1133,7 @@
     proof(rule rexp_of_lam_eq_lam_set)
       show "finite A" 
 	unfolding A_def
-	using invariant_ES ES_single 
+	using Inv_ES
         by (rule_tac arden_op_keeps_finite) 
            (auto simp add: invariant_def finite_rhs_def)
     qed
@@ -1096,7 +1141,7 @@
     proof-
       have "{Lam r | r. Lam r \<in> A} = A"
       proof-
-        have "classes_of A = {}" using invariant_ES ES_single
+        have "classes_of A = {}" using Inv_ES 
 	  unfolding A_def
           by (simp add:arden_op_removes_cl 
                        self_contained_def invariant_def lefts_of_def) 
@@ -1109,38 +1154,37 @@
     also have "\<dots> = X"
     unfolding A_def
     proof(rule arden_op_keeps_eq [THEN sym])
-      show "X = L xrhs" using invariant_ES ES_single 
-        by (auto simp only:invariant_def valid_eqns_def)  
+      show "X = L xrhs" using Inv_ES 
+        by (auto simp only: invariant_def valid_eqns_def)  
     next
-      from invariant_ES ES_single show "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})"
-        by(simp add:invariant_def ardenable_def rexp_of_empty finite_rhs_def)
+      from Inv_ES show "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})"
+        by(simp add: invariant_def ardenable_def rexp_of_empty finite_rhs_def)
     next
-      from invariant_ES ES_single show "finite xrhs" 
-        by (simp add:invariant_def finite_rhs_def)
+      from Inv_ES show "finite xrhs" 
+        by (simp add: invariant_def finite_rhs_def)
     qed
     finally show ?thesis by simp
   qed
   thus ?thesis by auto
 qed
-   
+
 lemma every_eqcl_has_reg: 
   assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
   and X_in_CS: "X \<in> (UNIV // (\<approx>Lang))"
   shows "\<exists> (reg::rexp). L reg = X" (is "\<exists> r. ?E r")
 proof -
-  from X_in_CS have "\<exists> xrhs. (X, xrhs) \<in> (eqs (UNIV  // (\<approx>Lang)))"
+  let ?ES = " eqs (UNIV // \<approx>Lang)"
+  from X_in_CS 
+  obtain xrhs where "(X, xrhs) \<in> ?ES"
     by (auto simp:eqs_def init_rhs_def)
-  then obtain ES xrhs where invariant_ES: "invariant ES" 
-    and X_in_ES: "(X, xrhs) \<in> ES"
-    and card_ES: "card ES = 1"
-    using finite_CS X_in_CS init_ES_satisfy_invariant iteration_conc
-    by blast
-  hence ES_single_equa: "ES = {(X, xrhs)}" 
-    by (auto simp:invariant_def dest!:card_Suc_Diff1 simp:card_eq_0_iff) 
-  thus ?thesis using invariant_ES
-    by (rule last_cl_exists_rexp)
+  from reduce_x [OF init_ES_satisfy_invariant [OF finite_CS] this]
+  have "\<exists>xrhs'. reduce X ?ES = {(X, xrhs')} \<and> invariant (reduce X ?ES)" .
+  then obtain xrhs' where "invariant {(X, xrhs')}" by auto
+  from last_cl_exists_rexp [OF this]
+  show ?thesis .
 qed
 
+
 theorem hard_direction: 
   assumes finite_CS: "finite (UNIV // \<approx>A)"
   shows   "\<exists>r::rexp. A = L r"