regexp: comparison Myhill

equal deleted inserted replaced

-:2335fcb96052
+:d63baacbdb16
 theory Myhill_1
-imports Main List_Prefix Prefix_subtract Prelude
+imports Main
 begin
 (*
 text {*
 \begin{figure}
 *}
 lemma folds_alt_simp [simp]:
 assumes a: "finite rs"
 shows "L (folds ALT NULL rs) = \<Union> (L ` rs)"
-apply(rule set_eq_intro)
+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
 text {* Just a technical lemma for collections and pairs *}
-lemma [simp]:
+lemma Pair_Collect[simp]:
 shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
 by simp
 text {*
 @{text "\<approx>A"} is an equivalence class defined by language @{text "A"}.
 the equation describing the formation of @{text "X"}. The definition of @{text "init_rhs"}
 is:
 *}
 definition
-transition :: "lang \<Rightarrow> char \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)
+transition :: "lang \<Rightarrow> rexp \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)
 where
-"Y \<Turnstile>c\<Rightarrow> X \<equiv> Y ;; {[c]} \<subseteq> X"
+"Y \<Turnstile>r\<Rightarrow> X \<equiv> Y ;; (L r) \<subseteq> X"
 definition
 "init_rhs CS X \<equiv>
 if ([] \<in> X) then
-{Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}
+{Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}
 else
-{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"
+{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}"
 text {*
 In the definition of @{text "init_rhs"}, the term
 @{text "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y ;; {[c]} \<subseteq> X}"} appearing on both branches
 describes the formation of strings in @{text "X"} out of transitions, while
 equivalent class inside @{text "CS"} is given by the following @{text "eqs(CS)"}.
 *}
 definition "eqs CS \<equiv> {(X, init_rhs CS X) | X.  X \<in> CS}"
 (************ arden's lemma variation ********************)
 text {*
 The following @{text "items_of rhs X"} returns all @{text "X"}-items in @{text "rhs"}.
 *}
 definition
 "rexp_of rhs X \<equiv> folds ALT NULL ((snd o the_Trn) ` items_of rhs X)"
 text {*
 The following @{text "lam_of rhs"} returns all pure regular expression items in @{text "rhs"}.
 *}
 definition
 "lam_of rhs \<equiv> {Lam r | r. Lam r \<in> rhs}"
 text {*
 The following @{text "rexp_of_lam rhs"} combines pure regular expression items in @{text "rhs"}
 using @{text "ALT"} to form a single regular expression.
 When all variables inside @{text "rhs"} are eliminated, @{text "rexp_of_lam rhs"}
 is used to compute compute the regular expression corresponds to @{text "rhs"}.
 *}
 definition
 "rexp_of_lam rhs \<equiv> folds ALT NULL (the_r ` lam_of rhs)"
 text {*
 The following @{text "attach_rexp rexp' itm"} attach
 the regular expression @{text "rexp'"} to
 the right of right hand side item @{text "itm"}.
 *}
 fun
 attach_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"
 where
 "attach_rexp rexp' (Lam rexp)   = Lam (SEQ rexp rexp')"
 | "attach_rexp rexp' (Trn X rexp) = Trn X (SEQ rexp rexp')"
 text {*
 The following @{text "append_rhs_rexp rhs rexp"} attaches
 @{text "rexp"} to every item in @{text "rhs"}.
 *}
 definition
 "append_rhs_rexp rhs rexp \<equiv> (attach_rexp rexp) ` rhs"
 text {*
 qed
 qed
 qed
 text {*
-The @{text "P"} in lemma @{text "wf_iter"} is an invaiant kept throughout the iteration procedure.
+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"}.
 *}
 text {*
 Every variable is defined at most onece 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 {*
 where "Y \<in> UNIV // (\<approx>Lang)"
 and "Y ;; {[c]} \<subseteq> X"
 and "clist \<in> Y"
 using decom "(1)" every_eqclass_has_transition by blast
 hence
-"x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y \<Turnstile>c\<Rightarrow> X}"
+"x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}"
 unfolding transition_def
 	using "(1)" decom
 by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)
 thus ?thesis using X_in_eqs "(1)"
 by (simp add: eqs_def init_rhs_def)

changeset 75	d63baacbdb16
parent 71	426070e68b21
child 76	1589bf5c1ad8