regexp: comparison Myhill

equal deleted inserted replaced

-:f460d5f75cb5
+:5bd73aa805a7
 Every equation in @{text ES} (represented by @{text "(X, rhs)"})
 is valid, i.e. @{text "X = L rhs"}.
 *}
 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
 transitional items of @{text "rhs"} do not contain empty string. This is
 necessary for the application of Arden's transformation to @{text "rhs"}.
 @{text "classes_of rhs"} returns all variables (or equivalent classes)
 occuring in @{text "rhs"}.
 *}
 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
 equational system @{text "ES"}.
 *}
 definition
 "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 {*
 The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints.
 *}
 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"
+assumes "sound_eqs ES" "finite ES" "distinct_equas ES" "ardenable ES"
-"finite_rhs ES" "self_contained ES"
+"finite_rhs ES" "valid_eqs ES"
 shows "invariant ES"
 using assms by (simp add: invariant_def)
 subsection {* The proof of this direction *}
 lemma lang_of_append_rhs:
 "L (append_rhs_rexp rhs r) = L rhs ;; L r"
 unfolding append_rhs_rexp_def
 by (auto simp add: Seq_def lang_of_append)
-lemma classes_of_union_distrib:
+lemma rhss_union_distrib:
-shows "classes_of (A \<union> B) = classes_of A \<union> classes_of B"
+shows "rhss (A \<union> B) = rhss A \<union> rhss B"
-by (auto simp add: classes_of_def)
+by (auto simp add: rhss_def)
 lemma lhss_union_distrib:
 shows "lhss (A \<union> B) = lhss A \<union> lhss B"
 by (auto simp add: lhss_def)
 lemma Init_ES_satisfies_invariant:
 assumes finite_CS: "finite (UNIV // \<approx>A)"
 shows "invariant (Init (UNIV // \<approx>A))"
 proof (rule invariantI)
-show "valid_eqns (Init (UNIV // \<approx>A))"
+show "sound_eqs (Init (UNIV // \<approx>A))"
-unfolding valid_eqns_def
+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
 show "distinct_equas (Init (UNIV // \<approx>A))"
 unfolding distinct_equas_def Init_def by simp
 unfolding ardenable_def Init_def Init_rhs_def rhs_nonempty_def
 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))"
+show "valid_eqs (Init (UNIV // \<approx>A))"
-unfolding self_contained_def Init_def Init_rhs_def classes_of_def lhss_def
+unfolding valid_eqs_def Init_def Init_rhs_def rhss_def lhss_def
 by auto
 qed
 subsubsection {* Interation step *}
 lemma Subst_all_keeps_finite_rhs:
 "\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)"
 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"
+"rhss (append_rhs_rexp rhs r) = rhss rhs"
-apply (auto simp:classes_of_def append_rhs_rexp_def)
+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>
+"X \<notin> rhss xrhs \<Longrightarrow>
-classes_of (Subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}"
+rhss (Subst rhs X xrhs) = rhss rhs \<union> rhss xrhs - {X}"
-apply (simp only:Subst_def append_rhs_keeps_cls classes_of_union_distrib)
+apply (simp only:Subst_def append_rhs_keeps_cls rhss_union_distrib)
-by (auto simp:classes_of_def)
+by (auto simp:rhss_def)
-lemma Subst_all_keeps_self_contained:
+lemma Subst_all_keeps_valid_eqs:
-assumes sc: "self_contained (ES \<union> {(Y, yrhs)})" (is "self_contained ?A")
+assumes sc: "valid_eqs (ES \<union> {(Y, yrhs)})" (is "valid_eqs ?A")
-shows "self_contained (Subst_all ES Y (Arden Y yrhs))"
+shows "valid_eqs (Subst_all ES Y (Arden Y yrhs))"
-(is "self_contained ?B")
+(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>
+have "rhss xrhs' \<subseteq>
-classes_of xrhs \<union> classes_of (Arden Y yrhs) - {Y}"
+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
+moreover have "rhss xrhs \<subseteq> lhss ES \<union> {Y}" using X_in sc
-apply (simp only:self_contained_def lhss_union_distrib)
+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:
 assumes invariant_ES: "invariant (ES \<union> {(Y, yrhs)})"
 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
 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
+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))"
 using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
 show "distinct_equas (Subst_all ES Y (Arden Y yrhs))"
 thus ?thesis using Arden_keeps_finite by simp
 qed
 ultimately show ?thesis
 by (simp add:Subst_all_keeps_finite_rhs)
 qed
-show "self_contained (Subst_all ES Y (Arden Y yrhs))"
+show "valid_eqs (Subst_all ES Y (Arden Y yrhs))"
-using invariant_ES Subst_all_keeps_self_contained by (simp add:invariant_def)
+using invariant_ES Subst_all_keeps_valid_eqs by (simp add:invariant_def)
 qed
 lemma Remove_in_card_measure:
 assumes finite: "finite ES"
 and     in_ES: "(X, rhs) \<in> ES"
 subsubsection {* Conclusion of the proof *}
 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
 { fix ES
 assume inv: "Inv ES" and crd: "Cond 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"
+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
 moreover
 { fix ES
 apply(clarify)
 apply(rule_tac iteration_step_measure)
 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
 lemma last_cl_exists_rexp:
 assumes Inv_ES: "invariant {(X, xrhs)}"
 shows "\<exists>r::rexp. L r = X"
 proof-
 def A \<equiv> "Arden X xrhs"
 have eq: "{Lam r | r. Lam r \<in> A} = A"
 proof -
-have "classes_of A = {}" using Inv_ES
+have "rhss A = {}" using Inv_ES
-unfolding A_def self_contained_def invariant_def lhss_def
+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)
 done
 qed
 then have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in>  A})"
 by auto
 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})"
 unfolding invariant_def ardenable_def finite_rhs_def
 by(simp add: rexp_of_empty)

changeset 104	5bd73aa805a7
parent 103	f460d5f75cb5
child 105	ae6ad1363eb9