regexp: comparison Myhill

equal deleted inserted replaced

-:2aa3756dcc9f
+:5b12cd0a3b3c
 then have "X \<subseteq> B ;; A\<star>" by auto
 ultimately
 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 *}
 datatype rexp =
 NULL
 text {* ALT-combination of a set or regulare expressions *}
 abbreviation
 Setalt  ("\<Uplus>_" [1000] 999)
 where
-"\<Uplus>A == folds ALT NULL A"
+"\<Uplus>A \<equiv> folds ALT NULL A"
 text {*
 For finite sets, @{term Setalt} is preserved under @{term L}.
 *}
 lemma folds_alt_simp [simp]:
 fixes rs::"rexp set"
 assumes a: "finite rs"
 shows "L (\<Uplus>rs) = \<Union> (L ` rs)"
+unfolding folds_def
 apply(rule set_eqI)
-apply(simp add: folds_def)
 apply(rule someI2_ex)
 apply(rule_tac finite_imp_fold_graph[OF a])
 apply(erule fold_graph.induct)
 apply(auto)
 done
 apply(auto)
 done
 lemma finals_in_partitions:
 shows "finals A \<subseteq> (UNIV // \<approx>A)"
-unfolding finals_def
+unfolding finals_def quotient_def
-unfolding quotient_def
 by auto
 section {* Equational systems *}
 fun L_rhs:: "rhs_item set \<Rightarrow> lang"
 where
 "L_rhs rhs = \<Union> (L ` rhs)"
 end
-definition
-"trns_of rhs X \<equiv> {Trn X r | r. Trn X r \<in> rhs}"
 text {* Transitions between equivalence classes *}
 definition
 transition :: "lang \<Rightarrow> char \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)
 where
 definition
 "append_rhs_rexp rhs rexp \<equiv> (append_rexp rexp) ` rhs"
 definition
-"arden_op X rhs \<equiv>
+"Arden X rhs \<equiv>
-append_rhs_rexp (rhs - trns_of rhs X) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))"
+append_rhs_rexp (rhs - {Trn X r | r. Trn X r \<in> rhs}) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))"
 section {* Substitution Operation on equations *}
 text {*
 Suppose and equation @{text "X = xrhs"}, @{text "subst_op"} substitutes
 all occurences of @{text "X"} in @{text "rhs"} by @{text "xrhs"}.
 *}
 definition
-"subst_op rhs X xrhs \<equiv>
+"Subst rhs X xrhs \<equiv>
-(rhs - (trns_of rhs X)) \<union> (append_rhs_rexp xrhs (\<Uplus> {r. Trn X r \<in> rhs}))"
+(rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> (append_rhs_rexp xrhs (\<Uplus> {r. Trn X r \<in> rhs}))"
 text {*
 @{text "eqs_subst ES X xrhs"} substitutes @{text xrhs} into every
 equation of the equational system @{text ES}.
 *}
 definition
-"subst_op_all ES X xrhs \<equiv> {(Y, subst_op yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
+"Subst_all ES X xrhs \<equiv> {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}"
 section {* While-combinator *}
 text {*
 @{text "arden_variate Y yrhs"}.
 *}
 definition
 "remove_op ES Y yrhs \<equiv>
-subst_op_all  (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)"
+Subst_all  (ES - {(Y, yrhs)}) Y (Arden 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.
 *}
 text {*
 From this point until @{text "iteration_step"},
 the correctness of the iteration step @{text "iter X ES"} is proved.
 *}
-lemma arden_op_keeps_eq:
+lemma Arden_keeps_eq:
 assumes l_eq_r: "X = L rhs"
 and not_empty: "[] \<notin> L (\<Uplus>{r. Trn X r \<in> rhs})"
 and finite: "finite rhs"
-shows "X = L (arden_op X rhs)"
+shows "X = L (Arden X rhs)"
 proof -
 def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})"
-def b \<equiv> "rhs - trns_of rhs X"
+def b \<equiv> "rhs - {Trn X r | r. Trn X r \<in> rhs}"
 def B \<equiv> "L b"
 have "X = B ;; A\<star>"
 proof-
-have "L rhs = L(trns_of rhs X \<union> b)" by (auto simp: b_def trns_of_def)
+have "L rhs = L({Trn X r | r. Trn X r \<in> rhs} \<union> b)" by (auto simp: b_def)
 also have "\<dots> = X ;; A \<union> B"
-unfolding trns_of_def
 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)
 done
 qed
-moreover have "L (arden_op X rhs) = (B ;; A\<star>)"
+moreover have "L (Arden X rhs) = B ;; A\<star>"
-by (simp only:arden_op_def L_rhs_union_distrib lang_of_append_rhs
+by (simp only:Arden_def L_rhs_union_distrib lang_of_append_rhs
 B_def A_def b_def L_rexp.simps seq_union_distrib_left)
 ultimately show ?thesis by simp
 qed
 lemma append_keeps_finite:
 "finite rhs \<Longrightarrow> finite (append_rhs_rexp rhs r)"
 by (auto simp:append_rhs_rexp_def)
-lemma arden_op_keeps_finite:
+lemma Arden_keeps_finite:
-"finite rhs \<Longrightarrow> finite (arden_op X rhs)"
+"finite rhs \<Longrightarrow> finite (Arden X rhs)"
-by (auto simp:arden_op_def append_keeps_finite)
+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)
 by (case_tac x, auto simp:Seq_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)
-lemma arden_op_keeps_nonempty:
+lemma Arden_keeps_nonempty:
-"rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (arden_op X rhs)"
+"rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (Arden X rhs)"
-by (simp only:arden_op_def append_keeps_nonempty nonempty_set_sub)
+by (simp only:Arden_def append_keeps_nonempty nonempty_set_sub)
-lemma subst_op_keeps_nonempty:
+lemma Subst_keeps_nonempty:
-"\<lbrakk>rhs_nonempty rhs; rhs_nonempty xrhs\<rbrakk> \<Longrightarrow> rhs_nonempty (subst_op rhs X xrhs)"
+"\<lbrakk>rhs_nonempty rhs; rhs_nonempty xrhs\<rbrakk> \<Longrightarrow> rhs_nonempty (Subst rhs X xrhs)"
-by (simp only:subst_op_def append_keeps_nonempty  nonempty_set_union nonempty_set_sub)
+by (simp only:Subst_def append_keeps_nonempty  nonempty_set_union nonempty_set_sub)
-lemma subst_op_keeps_eq:
+lemma Subst_keeps_eq:
 assumes substor: "X = L xrhs"
 and finite: "finite rhs"
-shows "L (subst_op rhs X xrhs) = L rhs" (is "?Left = ?Right")
+shows "L (Subst rhs X xrhs) = L rhs" (is "?Left = ?Right")
 proof-
-def A \<equiv> "L (rhs - trns_of rhs X)"
+def A \<equiv> "L (rhs - {Trn X r | r. Trn X r \<in> rhs})"
 have "?Left = A \<union> L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs}))"
-unfolding subst_op_def
+unfolding Subst_def
 unfolding L_rhs_union_distrib[symmetric]
 by (simp add: A_def)
 moreover have "?Right = A \<union> L ({Trn X r | r. Trn X r \<in> rhs})"
 proof-
-have "rhs = (rhs - trns_of rhs X) \<union> (trns_of rhs X)" by (auto simp add: trns_of_def)
+have "rhs = (rhs - {Trn X r | r. Trn X r \<in> rhs}) \<union> ({Trn X r | r. Trn X r \<in> rhs})" by auto
 thus ?thesis
 unfolding A_def
 unfolding L_rhs_union_distrib
-unfolding trns_of_def
 by simp
 qed
 moreover have "L (append_rhs_rexp xrhs (\<Uplus>{r. Trn X r \<in> rhs})) = L ({Trn X r | r. Trn X r \<in> rhs})"
 using finite substor  by (simp only:lang_of_append_rhs lang_of_rexp_of)
 ultimately show ?thesis by simp
 qed
-lemma subst_op_keeps_finite_rhs:
+lemma Subst_keeps_finite_rhs:
-"\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (subst_op rhs Y yrhs)"
+"\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (Subst rhs Y yrhs)"
-by (auto simp:subst_op_def append_keeps_finite)
+by (auto simp:Subst_def append_keeps_finite)
-lemma subst_op_all_keeps_finite:
+lemma Subst_all_keeps_finite:
 assumes finite:"finite (ES:: (string set \<times> rhs_item set) set)"
-shows "finite (subst_op_all ES Y yrhs)"
+shows "finite (Subst_all ES Y yrhs)"
 proof -
-have "finite {(Ya, subst_op yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \<in> ES}"
+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_op yrhsa Y yrhs)"
+def h \<equiv> "\<lambda> ((Ya::string set), 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_op_all_def)
+thus ?thesis by (simp add:Subst_all_def)
 qed
-lemma subst_op_all_keeps_finite_rhs:
+lemma Subst_all_keeps_finite_rhs:
-"\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (subst_op_all ES Y yrhs)"
+"\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)"
-by (auto intro:subst_op_keeps_finite_rhs simp add:subst_op_all_def finite_rhs_def)
+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)
 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_op_removes_cl:
+lemma Arden_removes_cl:
-"classes_of (arden_op Y yrhs) = classes_of yrhs - {Y}"
+"classes_of (Arden Y yrhs) = classes_of yrhs - {Y}"
-apply (simp add:arden_op_def append_rhs_keeps_cls trns_of_def)
+apply (simp add:Arden_def append_rhs_keeps_cls)
 by (auto simp:classes_of_def)
 lemma lefts_of_keeps_cls:
-"lefts_of (subst_op_all ES Y yrhs) = lefts_of ES"
+"lefts_of (Subst_all ES Y yrhs) = lefts_of ES"
-by (auto simp:lefts_of_def subst_op_all_def)
+by (auto simp:lefts_of_def Subst_all_def)
-lemma subst_op_updates_cls:
+lemma Subst_updates_cls:
 "X \<notin> classes_of xrhs \<Longrightarrow>
-classes_of (subst_op rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
+classes_of (Subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
-apply (simp only:subst_op_def append_rhs_keeps_cls
+apply (simp only:Subst_def append_rhs_keeps_cls
 classes_of_union_distrib[THEN sym])
-by (auto simp:classes_of_def trns_of_def)
+by (auto simp:classes_of_def)
-lemma subst_op_all_keeps_self_contained:
+lemma Subst_all_keeps_self_contained:
 fixes Y
 assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A")
-shows "self_contained (subst_op_all ES Y (arden_op Y yrhs))"
+shows "self_contained (Subst_all ES Y (Arden Y yrhs))"
 (is "self_contained ?B")
 proof-
 { fix X xrhs'
 assume "(X, xrhs') \<in> ?B"
 then obtain xrhs
-where xrhs_xrhs': "xrhs' = subst_op xrhs Y (arden_op Y yrhs)"
+where xrhs_xrhs': "xrhs' = Subst xrhs Y (Arden Y yrhs)"
-and X_in: "(X, xrhs) \<in> ES" by (simp add:subst_op_all_def, blast)
+and X_in: "(X, xrhs) \<in> ES" by (simp add:Subst_all_def, blast)
 have "classes_of xrhs' \<subseteq> lefts_of ?B"
 proof-
-have "lefts_of ?B = lefts_of ES" by (auto simp add:lefts_of_def subst_op_all_def)
+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"
 proof-
 have "classes_of xrhs' \<subseteq>
-classes_of xrhs \<union> classes_of (arden_op Y yrhs) - {Y}"
+classes_of xrhs \<union> classes_of (Arden Y yrhs) - {Y}"
 proof-
-have "Y \<notin> classes_of (arden_op Y yrhs)"
+have "Y \<notin> classes_of (Arden Y yrhs)"
-using arden_op_removes_cl by simp
+using Arden_removes_cl by simp
-thus ?thesis using xrhs_xrhs' by (auto simp:subst_op_updates_cls)
+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[THEN sym])
 by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def)
-moreover have "classes_of (arden_op Y yrhs) \<subseteq> lefts_of ES \<union> {Y}"
+moreover have "classes_of (Arden Y yrhs) \<subseteq> lefts_of ES \<union> {Y}"
 using sc
-by (auto simp add:arden_op_removes_cl self_contained_def lefts_of_def)
+by (auto simp add:Arden_removes_cl self_contained_def lefts_of_def)
 ultimately show ?thesis by auto
 qed
 ultimately show ?thesis by simp
 qed
-} thus ?thesis by (auto simp only:subst_op_all_def self_contained_def)
+} thus ?thesis by (auto simp only:Subst_all_def self_contained_def)
 qed
-lemma subst_op_all_satisfy_invariant:
+lemma Subst_all_satisfy_invariant:
 assumes invariant_ES: "invariant (ES \<union> {(Y, yrhs)})"
-shows "invariant (subst_op_all ES Y (arden_op Y yrhs))"
+shows "invariant (Subst_all ES Y (Arden Y yrhs))"
 proof -
 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 Y_eq_yrhs: "Y = L yrhs"
 using invariant_ES by (simp only:invariant_def valid_eqns_def, blast)
-have "distinct_equas (subst_op_all ES Y (arden_op Y yrhs))"
+have "distinct_equas (Subst_all ES Y (Arden Y yrhs))"
 using invariant_ES
-by (auto simp:distinct_equas_def subst_op_all_def invariant_def)
+by (auto simp:distinct_equas_def Subst_all_def invariant_def)
-moreover have "finite (subst_op_all ES Y (arden_op Y yrhs))"
+moreover have "finite (Subst_all ES Y (Arden Y yrhs))"
-using invariant_ES by (simp add:invariant_def subst_op_all_keeps_finite)
+using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
-moreover have "finite_rhs (subst_op_all ES Y (arden_op Y yrhs))"
+moreover have "finite_rhs (Subst_all ES Y (Arden Y yrhs))"
 proof-
 have "finite_rhs ES" using invariant_ES
 by (simp add:invariant_def finite_rhs_def)
-moreover have "finite (arden_op Y yrhs)"
+moreover have "finite (Arden Y yrhs)"
 proof -
 have "finite yrhs" using invariant_ES
 by (auto simp:invariant_def finite_rhs_def)
-thus ?thesis using arden_op_keeps_finite by simp
+thus ?thesis using Arden_keeps_finite by simp
 qed
 ultimately show ?thesis
-by (simp add:subst_op_all_keeps_finite_rhs)
+by (simp add:Subst_all_keeps_finite_rhs)
 qed
-moreover have "ardenable (subst_op_all ES Y (arden_op Y yrhs))"
+moreover have "ardenable (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 (simp add:invariant_def ardenable_def)
 with nonempty_yrhs
-have "rhs_nonempty (subst_op rhs Y (arden_op Y yrhs))"
+have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))"
 by (simp add:nonempty_yrhs
-subst_op_keeps_nonempty arden_op_keeps_nonempty)
+Subst_keeps_nonempty Arden_keeps_nonempty)
-} thus ?thesis by (auto simp add:ardenable_def subst_op_all_def)
+} thus ?thesis by (auto simp add:ardenable_def Subst_all_def)
 qed
-moreover have "valid_eqns (subst_op_all ES Y (arden_op Y yrhs))"
+moreover have "valid_eqns (Subst_all ES Y (Arden Y yrhs))"
 proof-
-have "Y = L (arden_op Y yrhs)"
+have "Y = L (Arden Y yrhs)"
 using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs
-by (rule_tac arden_op_keeps_eq, (simp add:rexp_of_empty)+)
+by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+)
 thus ?thesis using invariant_ES
 by (clarsimp simp add:valid_eqns_def
-subst_op_all_def subst_op_keeps_eq invariant_def finite_rhs_def
+Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def
 simp del:L_rhs.simps)
 qed
 moreover
-have self_subst: "self_contained (subst_op_all ES Y (arden_op Y yrhs))"
+have self_subst: "self_contained (Subst_all ES Y (Arden Y yrhs))"
-using invariant_ES subst_op_all_keeps_self_contained by (simp add:invariant_def)
+using invariant_ES Subst_all_keeps_self_contained by (simp add:invariant_def)
 ultimately show ?thesis using invariant_ES by (simp add:invariant_def)
 qed
-lemma subst_op_all_card_le:
+lemma Subst_all_card_le:
 assumes finite: "finite (ES::(string set \<times> rhs_item set) set)"
-shows "card (subst_op_all ES Y yrhs) <= card ES"
+shows "card (Subst_all ES Y yrhs) <= card ES"
 proof-
-def f \<equiv> "\<lambda> x. ((fst x)::string set, subst_op (snd x) Y yrhs)"
+def f \<equiv> "\<lambda> x. ((fst x)::string set, Subst (snd x) Y yrhs)"
-have "subst_op_all ES Y yrhs = f ` ES"
+have "Subst_all ES Y yrhs = f ` ES"
-apply (auto simp:subst_op_all_def f_def image_def)
+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)
 qed
-lemma subst_op_all_cls_remains:
+lemma Subst_all_cls_remains:
-"(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (subst_op_all ES Y yrhs)"
+"(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (Subst_all ES Y yrhs)"
-by (auto simp:subst_op_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"
 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)"
+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_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \<and>
+show "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<and>
-(\<exists>xrhs'. (X, xrhs') \<in> subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \<and>
+(\<exists>xrhs'. (X, xrhs') \<in> Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<and>
-card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) < card ES"
+card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES"
 proof -
-have "invariant (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs))"
+have "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))"
-proof(rule subst_op_all_satisfy_invariant)
+proof(rule Subst_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))"
+"(\<exists>xrhs'. (X, xrhs') \<in> Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))"
-proof(rule subst_op_all_cls_remains)
+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_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) < card ES"
+"card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES"
 proof(rule le_less_trans)
 show
-"card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \<le>
+"card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \<le>
 card (ES - {(Y, yrhs)})"
-proof(rule subst_op_all_card_le)
+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_op_all_card_le elim:le_less_trans)
+by (auto dest: Subst_all_card_le elim:le_less_trans)
 qed
 qed
 qed
 qed
 lemma last_cl_exists_rexp:
 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"
+def A \<equiv> "Arden X xrhs"
 have "?P (\<Uplus>{r. Lam r \<in> A})"
 proof -
 have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in>  A})"
 proof(rule rexp_of_lam_eq_lam_set)
 show "finite A"
 	unfolding A_def
 	using Inv_ES
-by (rule_tac arden_op_keeps_finite)
+by (rule_tac Arden_keeps_finite)
 (auto simp add: invariant_def finite_rhs_def)
 qed
 also have "\<dots> = L A"
 proof-
 have "{Lam r | r. Lam r \<in> A} = A"
 proof-
 have "classes_of A = {}" using Inv_ES
 	  unfolding A_def
-by (simp add:arden_op_removes_cl
+by (simp add:Arden_removes_cl
 self_contained_def invariant_def lefts_of_def)
 thus ?thesis
 	  unfolding A_def
 by (auto simp only: classes_of_def, case_tac x, auto)
 qed
 thus ?thesis by simp
 qed
 also have "\<dots> = X"
 unfolding A_def
-proof(rule arden_op_keeps_eq [THEN sym])
+proof(rule Arden_keeps_eq [THEN sym])
 show "X = L xrhs" using Inv_ES
 by (auto simp only: invariant_def valid_eqns_def)
 next
 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)

changeset 94	5b12cd0a3b3c
parent 92	a9ebc410a5c8
child 95	9540c2f2ea77