diff -r 3b9deda4f459 -r 70485955c934 Myhill_1.thy
--- a/Myhill_1.thy	Thu Feb 10 21:00:40 2011 +0000
+++ b/Myhill_1.thy	Fri Feb 11 12:13:35 2011 +0000
@@ -249,33 +249,6 @@
   show "X = B ;; A\<star>" by simp
 qed
 
-(*
-corollary arden_eq:
-  assumes nemp: "[] \<notin> A"
-  shows "(X ;; A \<union> B) = (B ;; A\<star>)"
-proof -
-  { assume "X = X ;; A \<union> B"
-    then have "X = B ;; A\<star>"
-    then have ?thesis
-      thm arden[THEN iffD1]
-apply(rule set_eqI)
-thm arden[THEN iffD1]
-apply(rule iffI)
-apply(rule trans)
-apply(rule arden[THEN iffD2, symmetric])
-apply(rule arden[OF iffD1, symmetric])
-thm trans
-proof -
-  { assume "X = X ;; A \<union> B"
-    then have "X = B ;; A\<star>" using arden[OF nemp] by blast
-    moreover 
-  
-    
-using arden[of "A" "X" "B", OF nemp]
-apply(erule_tac iffE)
-apply(blast)
-*)
-
 
 section {* Regular Expressions *}
 
@@ -468,7 +441,11 @@
   equation of the equational system @{text ES}.
 *}
 
+types esystem = "(lang \<times> rhs_item set) set"
+
 definition
+  Subst_all :: "esystem \<Rightarrow> lang \<Rightarrow> rhs_item set \<Rightarrow> esystem"
+where
   "Subst_all ES X xrhs \<equiv> {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
 
 text {*
@@ -495,36 +472,57 @@
   "Iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> X \<noteq> Y
                 in Remove ES Y yrhs)"
 
+lemma IterI2:
+  assumes "(Y, yrhs) \<in> ES"
+  and     "X \<noteq> Y"
+  and     "\<And>Y yrhs. \<lbrakk>(Y, yrhs) \<in> ES; X \<noteq> Y\<rbrakk> \<Longrightarrow> Q (Remove ES Y yrhs)"
+  shows "Q (Iter X ES)"
+unfolding Iter_def using assms
+by (rule_tac a="(Y, yrhs)" in someI2) (auto)
+
+
 text {*
   The following term @{text "Reduce X ES"} repeatedly removes characteriztion equations
   for unknowns other than @{text "X"} until one is left.
 *}
 
+abbreviation
+  "Test ES \<equiv> card ES \<noteq> 1"
+
 definition 
-  "Reduce X ES \<equiv> while (\<lambda> ES. card ES \<noteq> 1) (Iter X) ES"
+  "Solve X ES \<equiv> while Test (Iter X) ES"
+
+
+(* test *)
+partial_function (tailrec)
+  solve
+where
+  "solve X ES = (if (card ES = 1) then ES else solve X (Iter X ES))"
+
 
 text {*
-  Since the @{text "while"} combinator from HOL library is used to implement @{text "Reduce X ES"},
+  Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve 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
+  of @{text "Solve X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined
   in terms of a series of auxilliary predicates:
 *}
 
 section {* Invariants *}
 
-text {* Every variable is defined at most onece in @{text ES}. *}
+text {* Every variable is defined at most once in @{text ES}. *}
 
 definition 
   "distinct_equas ES \<equiv> 
      \<forall> X rhs rhs'. (X, rhs) \<in> ES \<and> (X, rhs') \<in> ES \<longrightarrow> rhs = rhs'"
 
+
 text {* 
   Every equation in @{text ES} (represented by @{text "(X, rhs)"}) 
-  is valid, i.e. @{text "(X = L rhs)"}.
+  is valid, i.e. @{text "X = L rhs"}.
 *}
 
 definition 
-  "valid_eqns ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> (X = L rhs)"
+  "valid_eqns ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs"
 
 text {*
   @{text "rhs_nonempty rhs"} requires regular expressions occuring in 
@@ -541,7 +539,7 @@
 *}
 
 definition 
-  "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> rhs_nonempty rhs"
+  "ardenable ES \<equiv> \<forall>(X, rhs) \<in> ES. rhs_nonempty rhs"
 
 text {* 
   @{text "finite_rhs ES"} requires every equation in @{text "rhs"} 
@@ -556,7 +554,7 @@
   *}
 
 definition 
-  "classes_of rhs \<equiv> {X. \<exists> r. Trn X r \<in> rhs}"
+  "classes_of rhs \<equiv> {X | X r. Trn X r \<in> rhs}"
 
 text {*
   @{text "lefts_of ES"} returns all variables defined by an 
@@ -570,7 +568,7 @@
   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> lefts_of ES"
 
 
 text {*
@@ -629,7 +627,7 @@
   shows "[] \<notin> L (\<Uplus> {r. Trn X r \<in> rhs})"
 using finite nonempty rhs_nonempty_def
 using finite_Trn[OF finite]
-by (auto)
+by auto
 
 lemma lang_of_rexp_of:
   assumes finite:"finite rhs"
@@ -758,7 +756,7 @@
 proof (rule invariantI)
   show "valid_eqns (Init (UNIV // \<approx>A))"
     unfolding valid_eqns_def 
-    using l_eq_r_in_eqs by simp
+    using l_eq_r_in_eqs by auto
   show "finite (Init (UNIV // \<approx>A))" using finite_CS
     unfolding Init_def by simp
   show "distinct_equas (Init (UNIV // \<approx>A))"     
@@ -873,8 +871,8 @@
   have "finite {(Ya, Subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \<in> ES}" 
                                                                   (is "finite ?A")
   proof-
-    def eqns' \<equiv> "{((Ya::string set), yrhsa)| Ya yrhsa. (Ya, yrhsa) \<in> ES}"
-    def h \<equiv> "\<lambda> ((Ya::string set), yrhsa). (Ya, Subst yrhsa Y yrhs)"
+    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      
@@ -958,7 +956,7 @@
       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 (clarsimp simp add:valid_eqns_def 
+      by (auto simp add:valid_eqns_def 
         Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def
         simp del:L_rhs.simps)
   qed
@@ -972,7 +970,7 @@
     { fix X rhs
       assume "(X, rhs) \<in> ES"
       hence "rhs_nonempty rhs"  using prems invariant_ES  
-        by (simp add:invariant_def ardenable_def)
+        by (auto simp add:invariant_def ardenable_def)
       with nonempty_yrhs 
       have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))"
         by (simp add:nonempty_yrhs 
@@ -996,98 +994,112 @@
     using invariant_ES Subst_all_keeps_self_contained by (simp add:invariant_def)
 qed
 
-lemma Subst_all_card_le: 
-  assumes finite: "finite (ES::(string set \<times> rhs_item set) set)"
-  shows "card (Subst_all ES Y yrhs) <= card ES"
-proof-
-  def f \<equiv> "\<lambda> x. ((fst x)::string set, Subst (snd x) Y yrhs)"
-  have "Subst_all ES Y yrhs = f ` ES" 
-    apply (auto simp:Subst_all_def f_def image_def)
-    by (rule_tac x = "(Ya, yrhsa)" in bexI, simp+)
-  thus ?thesis using finite by (auto intro:card_image_le)
+lemma Remove_in_card_measure:
+  assumes finite: "finite ES"
+  and     in_ES: "(X, rhs) \<in> ES"
+  shows "(Remove ES X rhs, ES) \<in> measure card"
+proof -
+  def f \<equiv> "\<lambda> x. ((fst x)::lang, Subst (snd x) X (Arden X rhs))"
+  def ES' \<equiv> "ES - {(X, rhs)}"
+  have "Subst_all ES' X (Arden X rhs) = f ` ES'" 
+    apply (auto simp: Subst_all_def f_def image_def)
+    by (rule_tac x = "(Y, yrhs)" in bexI, simp+)
+  then have "card (Subst_all ES' X (Arden X rhs)) \<le> card ES'"
+    unfolding ES'_def using finite by (auto intro: card_image_le)
+  also have "\<dots> < card ES" unfolding ES'_def 
+    using in_ES finite by (rule_tac card_Diff1_less)
+  finally show "(Remove ES X rhs, ES) \<in> measure card" 
+    unfolding Remove_def ES'_def by simp
 qed
+    
 
 lemma Subst_all_cls_remains: 
   "(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (Subst_all ES Y yrhs)"
-by (auto simp:Subst_all_def)
+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'" 
+  obtains e' where "e' \<in> S \<and> e \<noteq> e'"
 proof-
   have "card (S - {e}) > 0"
   proof -
-    have "card S > 1" using card e_in finite  
-      by (case_tac "card S", auto) 
+    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
 qed
 
-lemma iteration_step:
+
+
+lemma iteration_step_measure:
   assumes Inv_ES: "invariant ES"
   and    X_in_ES: "(X, xrhs) \<in> ES"
   and    not_T: "card ES \<noteq> 1"
-  shows "(invariant (Iter X ES) \<and> (\<exists> xrhs'.(X, xrhs') \<in> (Iter X ES)) \<and> 
-                (Iter X ES, ES) \<in> measure card)"
+  shows "(Iter X ES, ES) \<in> measure card"
+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 show "(Iter X ES, ES) \<in> measure card" 
+  apply(rule IterI2)
+  apply(rule Remove_in_card_measure)
+  apply(simp_all add: finite_ES)
+  done
+qed
+
+lemma iteration_step_invariant:
+  assumes Inv_ES: "invariant ES"
+  and    X_in_ES: "(X, xrhs) \<in> ES"
+  and    not_T: "card ES \<noteq> 1"
+  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)
-  let ?ES' = "Iter X ES"
-  show ?thesis
-  proof(unfold Iter_def Remove_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_all (ES - {(Y, yrhs)}) Y (Arden 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_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<and>
-             (\<exists>xrhs'. (X, xrhs') \<in> Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<and>
-             card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES"
-      proof -
-        have "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))" 
-        proof(rule Subst_all_satisfies_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_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))"
-        proof(rule Subst_all_cls_remains)
-          from X_in_ES and h
-          show "(X, xrhs) \<in> ES - {(Y, yrhs)}" by auto
-        qed
-        moreover have 
-          "card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES"
-        proof(rule le_less_trans)
-          show 
-            "card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<le> 
-                                                                card (ES - {(Y, yrhs)})"
-          proof(rule Subst_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_all_card_le elim:le_less_trans)
-      qed
-    qed
+    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 show "invariant (Iter X ES)" 
+  proof(rule IterI2)
+    fix Y yrhs
+    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) 
   qed
 qed
 
+lemma iteration_step_ex:
+  assumes Inv_ES: "invariant ES"
+  and    X_in_ES: "(X, xrhs) \<in> ES"
+  and    not_T: "card ES \<noteq> 1"
+  shows "\<exists>xrhs'. (X, xrhs') \<in> (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 show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" 
+  apply(rule IterI2)
+  unfolding Remove_def
+  apply(rule Subst_all_cls_remains)
+  using X_in_ES
+  apply(auto)
+  done
+qed
+
 
 subsubsection {* Conclusion of the proof *}
 
@@ -1096,38 +1108,37 @@
   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'. Reduce X ES = {(X, xrhs')} \<and> invariant(Reduce X ES)"
+  shows "\<exists> xrhs'. Solve X ES = {(X, xrhs')} \<and> invariant(Solve 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"])
+  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"
-    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
+    then show "(Iter X ES, ES) \<in> measure card"
+      apply(clarify)
+      apply(rule iteration_step_measure)
+      apply(auto)
+      done
   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
+    then show "?Inv (Iter X ES)"
+      apply -
+      apply(auto)
+      apply(rule iteration_step_invariant)
+      apply(auto)
+      apply(rule iteration_step_ex)
+      apply(auto)
+      done
   next
     fix ES
     assume "?Inv ES" and "\<not> card ES \<noteq> 1"
@@ -1189,7 +1200,7 @@
   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 "Reduce X ES = {(X, xrhs')}" "invariant (Reduce X ES)"
+  obtain xrhs' where "Solve X ES = {(X, xrhs')}" "invariant (Solve X ES)"
     using reduce_x by blast
   then show "\<exists>r::rexp. L r = X"
   using last_cl_exists_rexp by auto