Cleanup.
This commit is contained in:
parent
c7d277b9da
commit
d7ad9cd51f
|
|
@ -1,375 +0,0 @@
|
|||
section "Derivatives of regular expressions"
|
||||
|
||||
(* Author: Christian Urban *)
|
||||
|
||||
theory Derivatives
|
||||
imports Regular_Exp
|
||||
begin
|
||||
|
||||
text\<open>This theory is based on work by Brozowski \cite{Brzozowski64} and Antimirov \cite{Antimirov95}.\<close>
|
||||
|
||||
subsection \<open>Brzozowski's derivatives of regular expressions\<close>
|
||||
|
||||
primrec
|
||||
deriv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
|
||||
where
|
||||
"deriv c (Zero) = Zero"
|
||||
| "deriv c (One) = Zero"
|
||||
| "deriv c (Atom c') = (if c = c' then One else Zero)"
|
||||
| "deriv c (Plus r1 r2) = Plus (deriv c r1) (deriv c r2)"
|
||||
| "deriv c (Times r1 r2) =
|
||||
(if nullable r1 then Plus (Times (deriv c r1) r2) (deriv c r2) else Times (deriv c r1) r2)"
|
||||
| "deriv c (Star r) = Times (deriv c r) (Star r)"
|
||||
|
||||
primrec
|
||||
derivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
|
||||
where
|
||||
"derivs [] r = r"
|
||||
| "derivs (c # s) r = derivs s (deriv c r)"
|
||||
|
||||
|
||||
lemma atoms_deriv_subset: "atoms (deriv x r) \<subseteq> atoms r"
|
||||
by (induction r) (auto)
|
||||
|
||||
lemma atoms_derivs_subset: "atoms (derivs w r) \<subseteq> atoms r"
|
||||
by (induction w arbitrary: r) (auto dest: atoms_deriv_subset[THEN subsetD])
|
||||
|
||||
lemma lang_deriv: "lang (deriv c r) = Deriv c (lang r)"
|
||||
by (induct r) (simp_all add: nullable_iff)
|
||||
|
||||
lemma lang_derivs: "lang (derivs s r) = Derivs s (lang r)"
|
||||
by (induct s arbitrary: r) (simp_all add: lang_deriv)
|
||||
|
||||
text \<open>A regular expression matcher:\<close>
|
||||
|
||||
definition matcher :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> bool" where
|
||||
"matcher r s = nullable (derivs s r)"
|
||||
|
||||
lemma matcher_correctness: "matcher r s \<longleftrightarrow> s \<in> lang r"
|
||||
by (induct s arbitrary: r)
|
||||
(simp_all add: nullable_iff lang_deriv matcher_def Deriv_def)
|
||||
|
||||
|
||||
subsection \<open>Antimirov's partial derivatives\<close>
|
||||
|
||||
abbreviation
|
||||
"Timess rs r \<equiv> (\<Union>r' \<in> rs. {Times r' r})"
|
||||
|
||||
lemma Timess_eq_image:
|
||||
"Timess rs r = (\<lambda>r'. Times r' r) ` rs"
|
||||
by auto
|
||||
|
||||
primrec
|
||||
pderiv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set"
|
||||
where
|
||||
"pderiv c Zero = {}"
|
||||
| "pderiv c One = {}"
|
||||
| "pderiv c (Atom c') = (if c = c' then {One} else {})"
|
||||
| "pderiv c (Plus r1 r2) = (pderiv c r1) \<union> (pderiv c r2)"
|
||||
| "pderiv c (Times r1 r2) =
|
||||
(if nullable r1 then Timess (pderiv c r1) r2 \<union> pderiv c r2 else Timess (pderiv c r1) r2)"
|
||||
| "pderiv c (Star r) = Timess (pderiv c r) (Star r)"
|
||||
|
||||
primrec
|
||||
pderivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
|
||||
where
|
||||
"pderivs [] r = {r}"
|
||||
| "pderivs (c # s) r = \<Union> (pderivs s ` pderiv c r)"
|
||||
|
||||
abbreviation
|
||||
pderiv_set :: "'a \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set"
|
||||
where
|
||||
"pderiv_set c rs \<equiv> \<Union> (pderiv c ` rs)"
|
||||
|
||||
abbreviation
|
||||
pderivs_set :: "'a list \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set"
|
||||
where
|
||||
"pderivs_set s rs \<equiv> \<Union> (pderivs s ` rs)"
|
||||
|
||||
lemma pderivs_append:
|
||||
"pderivs (s1 @ s2) r = \<Union> (pderivs s2 ` pderivs s1 r)"
|
||||
by (induct s1 arbitrary: r) (simp_all)
|
||||
|
||||
lemma pderivs_snoc:
|
||||
shows "pderivs (s @ [c]) r = pderiv_set c (pderivs s r)"
|
||||
by (simp add: pderivs_append)
|
||||
|
||||
lemma pderivs_simps [simp]:
|
||||
shows "pderivs s Zero = (if s = [] then {Zero} else {})"
|
||||
and "pderivs s One = (if s = [] then {One} else {})"
|
||||
and "pderivs s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pderivs s r1) \<union> (pderivs s r2))"
|
||||
by (induct s) (simp_all)
|
||||
|
||||
lemma pderivs_Atom:
|
||||
shows "pderivs s (Atom c) \<subseteq> {Atom c, One}"
|
||||
by (induct s) (simp_all)
|
||||
|
||||
subsection \<open>Relating left-quotients and partial derivatives\<close>
|
||||
|
||||
lemma Deriv_pderiv:
|
||||
shows "Deriv c (lang r) = \<Union> (lang ` pderiv c r)"
|
||||
by (induct r) (auto simp add: nullable_iff conc_UNION_distrib)
|
||||
|
||||
lemma Derivs_pderivs:
|
||||
shows "Derivs s (lang r) = \<Union> (lang ` pderivs s r)"
|
||||
proof (induct s arbitrary: r)
|
||||
case (Cons c s)
|
||||
have ih: "\<And>r. Derivs s (lang r) = \<Union> (lang ` pderivs s r)" by fact
|
||||
have "Derivs (c # s) (lang r) = Derivs s (Deriv c (lang r))" by simp
|
||||
also have "\<dots> = Derivs s (\<Union> (lang ` pderiv c r))" by (simp add: Deriv_pderiv)
|
||||
also have "\<dots> = Derivss s (lang ` (pderiv c r))"
|
||||
by (auto simp add: Derivs_def)
|
||||
also have "\<dots> = \<Union> (lang ` (pderivs_set s (pderiv c r)))"
|
||||
using ih by auto
|
||||
also have "\<dots> = \<Union> (lang ` (pderivs (c # s) r))" by simp
|
||||
finally show "Derivs (c # s) (lang r) = \<Union> (lang ` pderivs (c # s) r)" .
|
||||
qed (simp add: Derivs_def)
|
||||
|
||||
subsection \<open>Relating derivatives and partial derivatives\<close>
|
||||
|
||||
lemma deriv_pderiv:
|
||||
shows "\<Union> (lang ` (pderiv c r)) = lang (deriv c r)"
|
||||
unfolding lang_deriv Deriv_pderiv by simp
|
||||
|
||||
lemma derivs_pderivs:
|
||||
shows "\<Union> (lang ` (pderivs s r)) = lang (derivs s r)"
|
||||
unfolding lang_derivs Derivs_pderivs by simp
|
||||
|
||||
|
||||
subsection \<open>Finiteness property of partial derivatives\<close>
|
||||
|
||||
definition
|
||||
pderivs_lang :: "'a lang \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set"
|
||||
where
|
||||
"pderivs_lang A r \<equiv> \<Union>x \<in> A. pderivs x r"
|
||||
|
||||
lemma pderivs_lang_subsetI:
|
||||
assumes "\<And>s. s \<in> A \<Longrightarrow> pderivs s r \<subseteq> C"
|
||||
shows "pderivs_lang A r \<subseteq> C"
|
||||
using assms unfolding pderivs_lang_def by (rule UN_least)
|
||||
|
||||
lemma pderivs_lang_union:
|
||||
shows "pderivs_lang (A \<union> B) r = (pderivs_lang A r \<union> pderivs_lang B r)"
|
||||
by (simp add: pderivs_lang_def)
|
||||
|
||||
lemma pderivs_lang_subset:
|
||||
shows "A \<subseteq> B \<Longrightarrow> pderivs_lang A r \<subseteq> pderivs_lang B r"
|
||||
by (auto simp add: pderivs_lang_def)
|
||||
|
||||
definition
|
||||
"UNIV1 \<equiv> UNIV - {[]}"
|
||||
|
||||
lemma pderivs_lang_Zero [simp]:
|
||||
shows "pderivs_lang UNIV1 Zero = {}"
|
||||
unfolding UNIV1_def pderivs_lang_def by auto
|
||||
|
||||
lemma pderivs_lang_One [simp]:
|
||||
shows "pderivs_lang UNIV1 One = {}"
|
||||
unfolding UNIV1_def pderivs_lang_def by (auto split: if_splits)
|
||||
|
||||
lemma pderivs_lang_Atom [simp]:
|
||||
shows "pderivs_lang UNIV1 (Atom c) = {One}"
|
||||
unfolding UNIV1_def pderivs_lang_def
|
||||
apply(auto)
|
||||
apply(frule rev_subsetD)
|
||||
apply(rule pderivs_Atom)
|
||||
apply(simp)
|
||||
apply(case_tac xa)
|
||||
apply(auto split: if_splits)
|
||||
done
|
||||
|
||||
lemma pderivs_lang_Plus [simp]:
|
||||
shows "pderivs_lang UNIV1 (Plus r1 r2) = pderivs_lang UNIV1 r1 \<union> pderivs_lang UNIV1 r2"
|
||||
unfolding UNIV1_def pderivs_lang_def by auto
|
||||
|
||||
|
||||
text \<open>Non-empty suffixes of a string (needed for the cases of @{const Times} and @{const Star} below)\<close>
|
||||
|
||||
definition
|
||||
"PSuf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
|
||||
|
||||
lemma PSuf_snoc:
|
||||
shows "PSuf (s @ [c]) = (PSuf s) @@ {[c]} \<union> {[c]}"
|
||||
unfolding PSuf_def conc_def
|
||||
by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv)
|
||||
|
||||
lemma PSuf_Union:
|
||||
shows "(\<Union>v \<in> PSuf s @@ {[c]}. f v) = (\<Union>v \<in> PSuf s. f (v @ [c]))"
|
||||
by (auto simp add: conc_def)
|
||||
|
||||
lemma pderivs_lang_snoc:
|
||||
shows "pderivs_lang (PSuf s @@ {[c]}) r = (pderiv_set c (pderivs_lang (PSuf s) r))"
|
||||
unfolding pderivs_lang_def
|
||||
by (simp add: PSuf_Union pderivs_snoc)
|
||||
|
||||
lemma pderivs_Times:
|
||||
shows "pderivs s (Times r1 r2) \<subseteq> Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2)"
|
||||
proof (induct s rule: rev_induct)
|
||||
case (snoc c s)
|
||||
have ih: "pderivs s (Times r1 r2) \<subseteq> Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2)"
|
||||
by fact
|
||||
have "pderivs (s @ [c]) (Times r1 r2) = pderiv_set c (pderivs s (Times r1 r2))"
|
||||
by (simp add: pderivs_snoc)
|
||||
also have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2))"
|
||||
using ih by fastforce
|
||||
also have "\<dots> = pderiv_set c (Timess (pderivs s r1) r2) \<union> pderiv_set c (pderivs_lang (PSuf s) r2)"
|
||||
by (simp)
|
||||
also have "\<dots> = pderiv_set c (Timess (pderivs s r1) r2) \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
|
||||
by (simp add: pderivs_lang_snoc)
|
||||
also
|
||||
have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs s r1) r2) \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
|
||||
by auto
|
||||
also
|
||||
have "\<dots> \<subseteq> Timess (pderiv_set c (pderivs s r1)) r2 \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
|
||||
by (auto simp add: if_splits)
|
||||
also have "\<dots> = Timess (pderivs (s @ [c]) r1) r2 \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
|
||||
by (simp add: pderivs_snoc)
|
||||
also have "\<dots> \<subseteq> Timess (pderivs (s @ [c]) r1) r2 \<union> pderivs_lang (PSuf (s @ [c])) r2"
|
||||
unfolding pderivs_lang_def by (auto simp add: PSuf_snoc)
|
||||
finally show ?case .
|
||||
qed (simp)
|
||||
|
||||
lemma pderivs_lang_Times_aux1:
|
||||
assumes a: "s \<in> UNIV1"
|
||||
shows "pderivs_lang (PSuf s) r \<subseteq> pderivs_lang UNIV1 r"
|
||||
using a unfolding UNIV1_def PSuf_def pderivs_lang_def by auto
|
||||
|
||||
lemma pderivs_lang_Times_aux2:
|
||||
assumes a: "s \<in> UNIV1"
|
||||
shows "Timess (pderivs s r1) r2 \<subseteq> Timess (pderivs_lang UNIV1 r1) r2"
|
||||
using a unfolding pderivs_lang_def by auto
|
||||
|
||||
lemma pderivs_lang_Times:
|
||||
shows "pderivs_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pderivs_lang UNIV1 r1) r2 \<union> pderivs_lang UNIV1 r2"
|
||||
apply(rule pderivs_lang_subsetI)
|
||||
apply(rule subset_trans)
|
||||
apply(rule pderivs_Times)
|
||||
using pderivs_lang_Times_aux1 pderivs_lang_Times_aux2
|
||||
apply auto
|
||||
apply blast
|
||||
done
|
||||
|
||||
lemma pderivs_Star:
|
||||
assumes a: "s \<noteq> []"
|
||||
shows "pderivs s (Star r) \<subseteq> Timess (pderivs_lang (PSuf s) r) (Star r)"
|
||||
using a
|
||||
proof (induct s rule: rev_induct)
|
||||
case (snoc c s)
|
||||
have ih: "s \<noteq> [] \<Longrightarrow> pderivs s (Star r) \<subseteq> Timess (pderivs_lang (PSuf s) r) (Star r)" by fact
|
||||
{ assume asm: "s \<noteq> []"
|
||||
have "pderivs (s @ [c]) (Star r) = pderiv_set c (pderivs s (Star r))" by (simp add: pderivs_snoc)
|
||||
also have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs_lang (PSuf s) r) (Star r))"
|
||||
using ih[OF asm] by fast
|
||||
also have "\<dots> \<subseteq> Timess (pderiv_set c (pderivs_lang (PSuf s) r)) (Star r) \<union> pderiv c (Star r)"
|
||||
by (auto split: if_splits)
|
||||
also have "\<dots> \<subseteq> Timess (pderivs_lang (PSuf (s @ [c])) r) (Star r) \<union> (Timess (pderiv c r) (Star r))"
|
||||
by (simp only: PSuf_snoc pderivs_lang_snoc pderivs_lang_union)
|
||||
(auto simp add: pderivs_lang_def)
|
||||
also have "\<dots> = Timess (pderivs_lang (PSuf (s @ [c])) r) (Star r)"
|
||||
by (auto simp add: PSuf_snoc PSuf_Union pderivs_snoc pderivs_lang_def)
|
||||
finally have ?case .
|
||||
}
|
||||
moreover
|
||||
{ assume asm: "s = []"
|
||||
then have ?case by (auto simp add: pderivs_lang_def pderivs_snoc PSuf_def)
|
||||
}
|
||||
ultimately show ?case by blast
|
||||
qed (simp)
|
||||
|
||||
lemma pderivs_lang_Star:
|
||||
shows "pderivs_lang UNIV1 (Star r) \<subseteq> Timess (pderivs_lang UNIV1 r) (Star r)"
|
||||
apply(rule pderivs_lang_subsetI)
|
||||
apply(rule subset_trans)
|
||||
apply(rule pderivs_Star)
|
||||
apply(simp add: UNIV1_def)
|
||||
apply(simp add: UNIV1_def PSuf_def)
|
||||
apply(auto simp add: pderivs_lang_def)
|
||||
done
|
||||
|
||||
lemma finite_Timess [simp]:
|
||||
assumes a: "finite A"
|
||||
shows "finite (Timess A r)"
|
||||
using a by auto
|
||||
|
||||
lemma finite_pderivs_lang_UNIV1:
|
||||
shows "finite (pderivs_lang UNIV1 r)"
|
||||
apply(induct r)
|
||||
apply(simp_all add:
|
||||
finite_subset[OF pderivs_lang_Times]
|
||||
finite_subset[OF pderivs_lang_Star])
|
||||
done
|
||||
|
||||
lemma pderivs_lang_UNIV:
|
||||
shows "pderivs_lang UNIV r = pderivs [] r \<union> pderivs_lang UNIV1 r"
|
||||
unfolding UNIV1_def pderivs_lang_def
|
||||
by blast
|
||||
|
||||
lemma finite_pderivs_lang_UNIV:
|
||||
shows "finite (pderivs_lang UNIV r)"
|
||||
unfolding pderivs_lang_UNIV
|
||||
by (simp add: finite_pderivs_lang_UNIV1)
|
||||
|
||||
lemma finite_pderivs_lang:
|
||||
shows "finite (pderivs_lang A r)"
|
||||
by (metis finite_pderivs_lang_UNIV pderivs_lang_subset rev_finite_subset subset_UNIV)
|
||||
|
||||
|
||||
text\<open>The following relationship between the alphabetic width of regular expressions
|
||||
(called @{text awidth} below) and the number of partial derivatives was proved
|
||||
by Antimirov~\cite{Antimirov95} and formalized by Max Haslbeck.\<close>
|
||||
|
||||
fun awidth :: "'a rexp \<Rightarrow> nat" where
|
||||
"awidth Zero = 0" |
|
||||
"awidth One = 0" |
|
||||
"awidth (Atom a) = 1" |
|
||||
"awidth (Plus r1 r2) = awidth r1 + awidth r2" |
|
||||
"awidth (Times r1 r2) = awidth r1 + awidth r2" |
|
||||
"awidth (Star r1) = awidth r1"
|
||||
|
||||
lemma card_Timess_pderivs_lang_le:
|
||||
"card (Timess (pderivs_lang A r) s) \<le> card (pderivs_lang A r)"
|
||||
using finite_pderivs_lang unfolding Timess_eq_image by (rule card_image_le)
|
||||
|
||||
lemma card_pderivs_lang_UNIV1_le_awidth: "card (pderivs_lang UNIV1 r) \<le> awidth r"
|
||||
proof (induction r)
|
||||
case (Plus r1 r2)
|
||||
have "card (pderivs_lang UNIV1 (Plus r1 r2)) = card (pderivs_lang UNIV1 r1 \<union> pderivs_lang UNIV1 r2)" by simp
|
||||
also have "\<dots> \<le> card (pderivs_lang UNIV1 r1) + card (pderivs_lang UNIV1 r2)"
|
||||
by(simp add: card_Un_le)
|
||||
also have "\<dots> \<le> awidth (Plus r1 r2)" using Plus.IH by simp
|
||||
finally show ?case .
|
||||
next
|
||||
case (Times r1 r2)
|
||||
have "card (pderivs_lang UNIV1 (Times r1 r2)) \<le> card (Timess (pderivs_lang UNIV1 r1) r2 \<union> pderivs_lang UNIV1 r2)"
|
||||
by (simp add: card_mono finite_pderivs_lang pderivs_lang_Times)
|
||||
also have "\<dots> \<le> card (Timess (pderivs_lang UNIV1 r1) r2) + card (pderivs_lang UNIV1 r2)"
|
||||
by (simp add: card_Un_le)
|
||||
also have "\<dots> \<le> card (pderivs_lang UNIV1 r1) + card (pderivs_lang UNIV1 r2)"
|
||||
by (simp add: card_Timess_pderivs_lang_le)
|
||||
also have "\<dots> \<le> awidth (Times r1 r2)" using Times.IH by simp
|
||||
finally show ?case .
|
||||
next
|
||||
case (Star r)
|
||||
have "card (pderivs_lang UNIV1 (Star r)) \<le> card (Timess (pderivs_lang UNIV1 r) (Star r))"
|
||||
by (simp add: card_mono finite_pderivs_lang pderivs_lang_Star)
|
||||
also have "\<dots> \<le> card (pderivs_lang UNIV1 r)" by (rule card_Timess_pderivs_lang_le)
|
||||
also have "\<dots> \<le> awidth (Star r)" by (simp add: Star.IH)
|
||||
finally show ?case .
|
||||
qed (auto)
|
||||
|
||||
text\<open>Antimirov's Theorem 3.4:\<close>
|
||||
theorem card_pderivs_lang_UNIV_le_awidth: "card (pderivs_lang UNIV r) \<le> awidth r + 1"
|
||||
proof -
|
||||
have "card (insert r (pderivs_lang UNIV1 r)) \<le> Suc (card (pderivs_lang UNIV1 r))"
|
||||
by(auto simp: card_insert_if[OF finite_pderivs_lang_UNIV1])
|
||||
also have "\<dots> \<le> Suc (awidth r)" by(simp add: card_pderivs_lang_UNIV1_le_awidth)
|
||||
finally show ?thesis by(simp add: pderivs_lang_UNIV)
|
||||
qed
|
||||
|
||||
text\<open>Antimirov's Corollary 3.5:\<close>
|
||||
corollary card_pderivs_lang_le_awidth: "card (pderivs_lang A r) \<le> awidth r + 1"
|
||||
by(rule order_trans[OF
|
||||
card_mono[OF finite_pderivs_lang_UNIV pderivs_lang_subset[OF subset_UNIV]]
|
||||
card_pderivs_lang_UNIV_le_awidth])
|
||||
|
||||
end
|
||||
|
|
@ -1,230 +0,0 @@
|
|||
section \<open>Deciding Regular Expression Equivalence\<close>
|
||||
|
||||
theory Equivalence_Checking
|
||||
imports
|
||||
NDerivative
|
||||
"HOL-Library.While_Combinator"
|
||||
begin
|
||||
|
||||
|
||||
subsection \<open>Bisimulation between languages and regular expressions\<close>
|
||||
|
||||
coinductive bisimilar :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> bool" where
|
||||
"([] \<in> K \<longleftrightarrow> [] \<in> L)
|
||||
\<Longrightarrow> (\<And>x. bisimilar (Deriv x K) (Deriv x L))
|
||||
\<Longrightarrow> bisimilar K L"
|
||||
|
||||
lemma equal_if_bisimilar:
|
||||
assumes "bisimilar K L" shows "K = L"
|
||||
proof (rule set_eqI)
|
||||
fix w
|
||||
from \<open>bisimilar K L\<close> show "w \<in> K \<longleftrightarrow> w \<in> L"
|
||||
proof (induct w arbitrary: K L)
|
||||
case Nil thus ?case by (auto elim: bisimilar.cases)
|
||||
next
|
||||
case (Cons a w K L)
|
||||
from \<open>bisimilar K L\<close> have "bisimilar (Deriv a K) (Deriv a L)"
|
||||
by (auto elim: bisimilar.cases)
|
||||
then have "w \<in> Deriv a K \<longleftrightarrow> w \<in> Deriv a L" by (rule Cons(1))
|
||||
thus ?case by (auto simp: Deriv_def)
|
||||
qed
|
||||
qed
|
||||
|
||||
lemma language_coinduct:
|
||||
fixes R (infixl "\<sim>" 50)
|
||||
assumes "K \<sim> L"
|
||||
assumes "\<And>K L. K \<sim> L \<Longrightarrow> ([] \<in> K \<longleftrightarrow> [] \<in> L)"
|
||||
assumes "\<And>K L x. K \<sim> L \<Longrightarrow> Deriv x K \<sim> Deriv x L"
|
||||
shows "K = L"
|
||||
apply (rule equal_if_bisimilar)
|
||||
apply (rule bisimilar.coinduct[of R, OF \<open>K \<sim> L\<close>])
|
||||
apply (auto simp: assms)
|
||||
done
|
||||
|
||||
type_synonym 'a rexp_pair = "'a rexp * 'a rexp"
|
||||
type_synonym 'a rexp_pairs = "'a rexp_pair list"
|
||||
|
||||
definition is_bisimulation :: "'a::order list \<Rightarrow> 'a rexp_pair set \<Rightarrow> bool"
|
||||
where
|
||||
"is_bisimulation as R =
|
||||
(\<forall>(r,s)\<in> R. (atoms r \<union> atoms s \<subseteq> set as) \<and> (nullable r \<longleftrightarrow> nullable s) \<and>
|
||||
(\<forall>a\<in>set as. (nderiv a r, nderiv a s) \<in> R))"
|
||||
|
||||
lemma bisim_lang_eq:
|
||||
assumes bisim: "is_bisimulation as ps"
|
||||
assumes "(r, s) \<in> ps"
|
||||
shows "lang r = lang s"
|
||||
proof -
|
||||
define ps' where "ps' = insert (Zero, Zero) ps"
|
||||
from bisim have bisim': "is_bisimulation as ps'"
|
||||
by (auto simp: ps'_def is_bisimulation_def)
|
||||
let ?R = "\<lambda>K L. (\<exists>(r,s)\<in>ps'. K = lang r \<and> L = lang s)"
|
||||
show ?thesis
|
||||
proof (rule language_coinduct[where R="?R"])
|
||||
from \<open>(r, s) \<in> ps\<close>
|
||||
have "(r, s) \<in> ps'" by (auto simp: ps'_def)
|
||||
thus "?R (lang r) (lang s)" by auto
|
||||
next
|
||||
fix K L assume "?R K L"
|
||||
then obtain r s where rs: "(r, s) \<in> ps'"
|
||||
and KL: "K = lang r" "L = lang s" by auto
|
||||
with bisim' have "nullable r \<longleftrightarrow> nullable s"
|
||||
by (auto simp: is_bisimulation_def)
|
||||
thus "[] \<in> K \<longleftrightarrow> [] \<in> L" by (auto simp: nullable_iff KL)
|
||||
fix a
|
||||
show "?R (Deriv a K) (Deriv a L)"
|
||||
proof cases
|
||||
assume "a \<in> set as"
|
||||
with rs bisim'
|
||||
have "(nderiv a r, nderiv a s) \<in> ps'"
|
||||
by (auto simp: is_bisimulation_def)
|
||||
thus ?thesis by (force simp: KL lang_nderiv)
|
||||
next
|
||||
assume "a \<notin> set as"
|
||||
with bisim' rs
|
||||
have "a \<notin> atoms r" "a \<notin> atoms s" by (auto simp: is_bisimulation_def)
|
||||
then have "nderiv a r = Zero" "nderiv a s = Zero"
|
||||
by (auto intro: deriv_no_occurrence)
|
||||
then have "Deriv a K = lang Zero"
|
||||
"Deriv a L = lang Zero"
|
||||
unfolding KL lang_nderiv[symmetric] by auto
|
||||
thus ?thesis by (auto simp: ps'_def)
|
||||
qed
|
||||
qed
|
||||
qed
|
||||
|
||||
subsection \<open>Closure computation\<close>
|
||||
|
||||
definition closure ::
|
||||
"'a::order list \<Rightarrow> 'a rexp_pair \<Rightarrow> ('a rexp_pairs * 'a rexp_pair set) option"
|
||||
where
|
||||
"closure as = rtrancl_while (%(r,s). nullable r = nullable s)
|
||||
(%(r,s). map (\<lambda>a. (nderiv a r, nderiv a s)) as)"
|
||||
|
||||
definition pre_bisim :: "'a::order list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp \<Rightarrow>
|
||||
'a rexp_pairs * 'a rexp_pair set \<Rightarrow> bool"
|
||||
where
|
||||
"pre_bisim as r s = (\<lambda>(ws,R).
|
||||
(r,s) \<in> R \<and> set ws \<subseteq> R \<and>
|
||||
(\<forall>(r,s)\<in> R. atoms r \<union> atoms s \<subseteq> set as) \<and>
|
||||
(\<forall>(r,s)\<in> R - set ws. (nullable r \<longleftrightarrow> nullable s) \<and>
|
||||
(\<forall>a\<in>set as. (nderiv a r, nderiv a s) \<in> R)))"
|
||||
|
||||
theorem closure_sound:
|
||||
assumes result: "closure as (r,s) = Some([],R)"
|
||||
and atoms: "atoms r \<union> atoms s \<subseteq> set as"
|
||||
shows "lang r = lang s"
|
||||
proof-
|
||||
let ?test = "While_Combinator.rtrancl_while_test (%(r,s). nullable r = nullable s)"
|
||||
let ?step = "While_Combinator.rtrancl_while_step (%(r,s). map (\<lambda>a. (nderiv a r, nderiv a s)) as)"
|
||||
{ fix st assume inv: "pre_bisim as r s st" and test: "?test st"
|
||||
have "pre_bisim as r s (?step st)"
|
||||
proof (cases st)
|
||||
fix ws R assume "st = (ws, R)"
|
||||
with test obtain r s t where st: "st = ((r, s) # t, R)" and "nullable r = nullable s"
|
||||
by (cases ws) auto
|
||||
with inv show ?thesis using atoms_nderiv[of _ r] atoms_nderiv[of _ s]
|
||||
unfolding st rtrancl_while_test.simps rtrancl_while_step.simps pre_bisim_def Ball_def
|
||||
by simp_all blast+
|
||||
qed
|
||||
}
|
||||
moreover
|
||||
from atoms
|
||||
have "pre_bisim as r s ([(r,s)],{(r,s)})" by (simp add: pre_bisim_def)
|
||||
ultimately have pre_bisim_ps: "pre_bisim as r s ([],R)"
|
||||
by (rule while_option_rule[OF _ result[unfolded closure_def rtrancl_while_def]])
|
||||
then have "is_bisimulation as R" "(r, s) \<in> R"
|
||||
by (auto simp: pre_bisim_def is_bisimulation_def)
|
||||
thus "lang r = lang s" by (rule bisim_lang_eq)
|
||||
qed
|
||||
|
||||
subsection \<open>Bisimulation-free proof of closure computation\<close>
|
||||
|
||||
text\<open>The equivalence check can be viewed as the product construction
|
||||
of two automata. The state space is the reflexive transitive closure of
|
||||
the pair of next-state functions, i.e. derivatives.\<close>
|
||||
|
||||
lemma rtrancl_nderiv_nderivs: defines "nderivs == foldl (%r a. nderiv a r)"
|
||||
shows "{((r,s),(nderiv a r,nderiv a s))| r s a. a : A}^* =
|
||||
{((r,s),(nderivs r w,nderivs s w))| r s w. w : lists A}" (is "?L = ?R")
|
||||
proof-
|
||||
note [simp] = nderivs_def
|
||||
{ fix r s r' s'
|
||||
have "((r,s),(r',s')) : ?L \<Longrightarrow> ((r,s),(r',s')) : ?R"
|
||||
proof(induction rule: converse_rtrancl_induct2)
|
||||
case refl show ?case by (force intro!: foldl.simps(1)[symmetric])
|
||||
next
|
||||
case step thus ?case by(force intro!: foldl.simps(2)[symmetric])
|
||||
qed
|
||||
} moreover
|
||||
{ fix r s r' s'
|
||||
{ fix w have "\<forall>x\<in>set w. x \<in> A \<Longrightarrow> ((r, s), nderivs r w, nderivs s w) :?L"
|
||||
proof(induction w rule: rev_induct)
|
||||
case Nil show ?case by simp
|
||||
next
|
||||
case snoc thus ?case by (auto elim!: rtrancl_into_rtrancl)
|
||||
qed
|
||||
}
|
||||
hence "((r,s),(r',s')) : ?R \<Longrightarrow> ((r,s),(r',s')) : ?L" by auto
|
||||
} ultimately show ?thesis by (auto simp: in_lists_conv_set) blast
|
||||
qed
|
||||
|
||||
lemma nullable_nderivs:
|
||||
"nullable (foldl (%r a. nderiv a r) r w) = (w : lang r)"
|
||||
by (induct w arbitrary: r) (simp_all add: nullable_iff lang_nderiv Deriv_def)
|
||||
|
||||
theorem closure_sound_complete:
|
||||
assumes result: "closure as (r,s) = Some(ws,R)"
|
||||
and atoms: "set as = atoms r \<union> atoms s"
|
||||
shows "ws = [] \<longleftrightarrow> lang r = lang s"
|
||||
proof -
|
||||
have leq: "(lang r = lang s) =
|
||||
(\<forall>(r',s') \<in> {((r0,s0),(nderiv a r0,nderiv a s0))| r0 s0 a. a : set as}^* `` {(r,s)}.
|
||||
nullable r' = nullable s')"
|
||||
by(simp add: atoms rtrancl_nderiv_nderivs Ball_def lang_eq_ext imp_ex nullable_nderivs
|
||||
del:Un_iff)
|
||||
have "{(x,y). y \<in> set ((\<lambda>(p,q). map (\<lambda>a. (nderiv a p, nderiv a q)) as) x)} =
|
||||
{((r,s), nderiv a r, nderiv a s) |r s a. a \<in> set as}"
|
||||
by auto
|
||||
with atoms rtrancl_while_Some[OF result[unfolded closure_def]]
|
||||
show ?thesis by (auto simp add: leq Ball_def split: if_splits)
|
||||
qed
|
||||
|
||||
subsection \<open>The overall procedure\<close>
|
||||
|
||||
primrec add_atoms :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> 'a list"
|
||||
where
|
||||
"add_atoms Zero = id"
|
||||
| "add_atoms One = id"
|
||||
| "add_atoms (Atom a) = List.insert a"
|
||||
| "add_atoms (Plus r s) = add_atoms s o add_atoms r"
|
||||
| "add_atoms (Times r s) = add_atoms s o add_atoms r"
|
||||
| "add_atoms (Star r) = add_atoms r"
|
||||
|
||||
lemma set_add_atoms: "set (add_atoms r as) = atoms r \<union> set as"
|
||||
by (induct r arbitrary: as) auto
|
||||
|
||||
|
||||
definition check_eqv :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> bool" where
|
||||
"check_eqv r s =
|
||||
(let nr = norm r; ns = norm s; as = add_atoms nr (add_atoms ns [])
|
||||
in case closure as (nr, ns) of
|
||||
Some([],_) \<Rightarrow> True | _ \<Rightarrow> False)"
|
||||
|
||||
lemma soundness:
|
||||
assumes "check_eqv r s" shows "lang r = lang s"
|
||||
proof -
|
||||
let ?nr = "norm r" let ?ns = "norm s"
|
||||
let ?as = "add_atoms ?nr (add_atoms ?ns [])"
|
||||
obtain R where 1: "closure ?as (?nr,?ns) = Some([],R)"
|
||||
using assms by (auto simp: check_eqv_def Let_def split:option.splits list.splits)
|
||||
then have "lang (norm r) = lang (norm s)"
|
||||
by (rule closure_sound) (auto simp: set_add_atoms dest!: subsetD[OF atoms_norm])
|
||||
thus "lang r = lang s" by simp
|
||||
qed
|
||||
|
||||
text\<open>Test:\<close>
|
||||
lemma "check_eqv (Plus One (Times (Atom 0) (Star(Atom 0)))) (Star(Atom 0))"
|
||||
by eval
|
||||
|
||||
end
|
||||
|
|
@ -1,318 +0,0 @@
|
|||
section \<open>Deciding Equivalence of Extended Regular Expressions\<close>
|
||||
|
||||
theory Equivalence_Checking2
|
||||
imports Regular_Exp2 "HOL-Library.While_Combinator"
|
||||
begin
|
||||
|
||||
subsection \<open>Term ordering\<close>
|
||||
|
||||
fun le_rexp :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> bool"
|
||||
where
|
||||
"le_rexp Zero _ = True"
|
||||
| "le_rexp _ Zero = False"
|
||||
| "le_rexp One _ = True"
|
||||
| "le_rexp _ One = False"
|
||||
| "le_rexp (Atom a) (Atom b) = (a <= b)"
|
||||
| "le_rexp (Atom _) _ = True"
|
||||
| "le_rexp _ (Atom _) = False"
|
||||
| "le_rexp (Star r) (Star s) = le_rexp r s"
|
||||
| "le_rexp (Star _) _ = True"
|
||||
| "le_rexp _ (Star _) = False"
|
||||
| "le_rexp (Not r) (Not s) = le_rexp r s"
|
||||
| "le_rexp (Not _) _ = True"
|
||||
| "le_rexp _ (Not _) = False"
|
||||
| "le_rexp (Plus r r') (Plus s s') =
|
||||
(if r = s then le_rexp r' s' else le_rexp r s)"
|
||||
| "le_rexp (Plus _ _) _ = True"
|
||||
| "le_rexp _ (Plus _ _) = False"
|
||||
| "le_rexp (Times r r') (Times s s') =
|
||||
(if r = s then le_rexp r' s' else le_rexp r s)"
|
||||
| "le_rexp (Times _ _) _ = True"
|
||||
| "le_rexp _ (Times _ _) = False"
|
||||
| "le_rexp (Inter r r') (Inter s s') =
|
||||
(if r = s then le_rexp r' s' else le_rexp r s)"
|
||||
|
||||
subsection \<open>Normalizing operations\<close>
|
||||
|
||||
text \<open>associativity, commutativity, idempotence, zero\<close>
|
||||
|
||||
fun nPlus :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> nat rexp"
|
||||
where
|
||||
"nPlus Zero r = r"
|
||||
| "nPlus r Zero = r"
|
||||
| "nPlus (Plus r s) t = nPlus r (nPlus s t)"
|
||||
| "nPlus r (Plus s t) =
|
||||
(if r = s then (Plus s t)
|
||||
else if le_rexp r s then Plus r (Plus s t)
|
||||
else Plus s (nPlus r t))"
|
||||
| "nPlus r s =
|
||||
(if r = s then r
|
||||
else if le_rexp r s then Plus r s
|
||||
else Plus s r)"
|
||||
|
||||
lemma lang_nPlus[simp]: "lang S (nPlus r s) = lang S (Plus r s)"
|
||||
by (induct r s rule: nPlus.induct) auto
|
||||
|
||||
text \<open>associativity, zero, one\<close>
|
||||
|
||||
fun nTimes :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> nat rexp"
|
||||
where
|
||||
"nTimes Zero _ = Zero"
|
||||
| "nTimes _ Zero = Zero"
|
||||
| "nTimes One r = r"
|
||||
| "nTimes r One = r"
|
||||
| "nTimes (Times r s) t = Times r (nTimes s t)"
|
||||
| "nTimes r s = Times r s"
|
||||
|
||||
lemma lang_nTimes[simp]: "lang S (nTimes r s) = lang S (Times r s)"
|
||||
by (induct r s rule: nTimes.induct) (auto simp: conc_assoc)
|
||||
|
||||
text \<open>more optimisations:\<close>
|
||||
|
||||
fun nInter :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> nat rexp"
|
||||
where
|
||||
"nInter Zero _ = Zero"
|
||||
| "nInter _ Zero = Zero"
|
||||
| "nInter r s = Inter r s"
|
||||
|
||||
lemma lang_nInter[simp]: "lang S (nInter r s) = lang S (Inter r s)"
|
||||
by (induct r s rule: nInter.induct) (auto)
|
||||
|
||||
primrec norm :: "nat rexp \<Rightarrow> nat rexp"
|
||||
where
|
||||
"norm Zero = Zero"
|
||||
| "norm One = One"
|
||||
| "norm (Atom a) = Atom a"
|
||||
| "norm (Plus r s) = nPlus (norm r) (norm s)"
|
||||
| "norm (Times r s) = nTimes (norm r) (norm s)"
|
||||
| "norm (Star r) = Star (norm r)"
|
||||
| "norm (Not r) = Not (norm r)"
|
||||
| "norm (Inter r1 r2) = nInter (norm r1) (norm r2)"
|
||||
|
||||
lemma lang_norm[simp]: "lang S (norm r) = lang S r"
|
||||
by (induct r) auto
|
||||
|
||||
|
||||
subsection \<open>Derivative\<close>
|
||||
|
||||
primrec nderiv :: "nat \<Rightarrow> nat rexp \<Rightarrow> nat rexp"
|
||||
where
|
||||
"nderiv _ Zero = Zero"
|
||||
| "nderiv _ One = Zero"
|
||||
| "nderiv a (Atom b) = (if a = b then One else Zero)"
|
||||
| "nderiv a (Plus r s) = nPlus (nderiv a r) (nderiv a s)"
|
||||
| "nderiv a (Times r s) =
|
||||
(let r's = nTimes (nderiv a r) s
|
||||
in if nullable r then nPlus r's (nderiv a s) else r's)"
|
||||
| "nderiv a (Star r) = nTimes (nderiv a r) (Star r)"
|
||||
| "nderiv a (Not r) = Not (nderiv a r)"
|
||||
| "nderiv a (Inter r1 r2) = nInter (nderiv a r1) (nderiv a r2)"
|
||||
|
||||
lemma lang_nderiv: "a:S \<Longrightarrow> lang S (nderiv a r) = Deriv a (lang S r)"
|
||||
by (induct r) (auto simp: Let_def nullable_iff[where S=S])
|
||||
|
||||
lemma atoms_nPlus[simp]: "atoms (nPlus r s) = atoms r \<union> atoms s"
|
||||
by (induct r s rule: nPlus.induct) auto
|
||||
|
||||
lemma atoms_nTimes: "atoms (nTimes r s) \<subseteq> atoms r \<union> atoms s"
|
||||
by (induct r s rule: nTimes.induct) auto
|
||||
|
||||
lemma atoms_nInter: "atoms (nInter r s) \<subseteq> atoms r \<union> atoms s"
|
||||
by (induct r s rule: nInter.induct) auto
|
||||
|
||||
lemma atoms_norm: "atoms (norm r) \<subseteq> atoms r"
|
||||
by (induct r) (auto dest!:subsetD[OF atoms_nTimes]subsetD[OF atoms_nInter])
|
||||
|
||||
lemma atoms_nderiv: "atoms (nderiv a r) \<subseteq> atoms r"
|
||||
by (induct r) (auto simp: Let_def dest!:subsetD[OF atoms_nTimes]subsetD[OF atoms_nInter])
|
||||
|
||||
|
||||
subsection \<open>Bisimulation between languages and regular expressions\<close>
|
||||
|
||||
context
|
||||
fixes S :: "'a set"
|
||||
begin
|
||||
|
||||
coinductive bisimilar :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> bool" where
|
||||
"K \<subseteq> lists S \<Longrightarrow> L \<subseteq> lists S
|
||||
\<Longrightarrow> ([] \<in> K \<longleftrightarrow> [] \<in> L)
|
||||
\<Longrightarrow> (\<And>x. x:S \<Longrightarrow> bisimilar (Deriv x K) (Deriv x L))
|
||||
\<Longrightarrow> bisimilar K L"
|
||||
|
||||
lemma equal_if_bisimilar:
|
||||
assumes "K \<subseteq> lists S" "L \<subseteq> lists S" "bisimilar K L" shows "K = L"
|
||||
proof (rule set_eqI)
|
||||
fix w
|
||||
from assms show "w \<in> K \<longleftrightarrow> w \<in> L"
|
||||
proof (induction w arbitrary: K L)
|
||||
case Nil thus ?case by (auto elim: bisimilar.cases)
|
||||
next
|
||||
case (Cons a w K L)
|
||||
show ?case
|
||||
proof cases
|
||||
assume "a : S"
|
||||
with \<open>bisimilar K L\<close> have "bisimilar (Deriv a K) (Deriv a L)"
|
||||
by (auto elim: bisimilar.cases)
|
||||
then have "w \<in> Deriv a K \<longleftrightarrow> w \<in> Deriv a L"
|
||||
by (metis Cons.IH bisimilar.cases)
|
||||
thus ?case by (auto simp: Deriv_def)
|
||||
next
|
||||
assume "a \<notin> S"
|
||||
thus ?case using Cons.prems by auto
|
||||
qed
|
||||
qed
|
||||
qed
|
||||
|
||||
lemma language_coinduct:
|
||||
fixes R (infixl "\<sim>" 50)
|
||||
assumes "\<And>K L. K \<sim> L \<Longrightarrow> K \<subseteq> lists S \<and> L \<subseteq> lists S"
|
||||
assumes "K \<sim> L"
|
||||
assumes "\<And>K L. K \<sim> L \<Longrightarrow> ([] \<in> K \<longleftrightarrow> [] \<in> L)"
|
||||
assumes "\<And>K L x. K \<sim> L \<Longrightarrow> x : S \<Longrightarrow> Deriv x K \<sim> Deriv x L"
|
||||
shows "K = L"
|
||||
apply (rule equal_if_bisimilar)
|
||||
apply (metis assms(1) assms(2))
|
||||
apply (metis assms(1) assms(2))
|
||||
apply (rule bisimilar.coinduct[of R, OF \<open>K \<sim> L\<close>])
|
||||
apply (auto simp: assms)
|
||||
done
|
||||
|
||||
end
|
||||
|
||||
type_synonym rexp_pair = "nat rexp * nat rexp"
|
||||
type_synonym rexp_pairs = "rexp_pair list"
|
||||
|
||||
definition is_bisimulation :: "nat list \<Rightarrow> rexp_pairs \<Rightarrow> bool"
|
||||
where
|
||||
"is_bisimulation as ps =
|
||||
(\<forall>(r,s)\<in> set ps. (atoms r \<union> atoms s \<subseteq> set as) \<and> (nullable r \<longleftrightarrow> nullable s) \<and>
|
||||
(\<forall>a\<in>set as. (nderiv a r, nderiv a s) \<in> set ps))"
|
||||
|
||||
|
||||
lemma bisim_lang_eq:
|
||||
assumes bisim: "is_bisimulation as ps"
|
||||
assumes "(r, s) \<in> set ps"
|
||||
shows "lang (set as) r = lang (set as) s"
|
||||
proof -
|
||||
let ?R = "\<lambda>K L. (\<exists>(r,s)\<in>set ps. K = lang (set as) r \<and> L = lang (set as) s)"
|
||||
show ?thesis
|
||||
proof (rule language_coinduct[where R="?R" and S = "set as"])
|
||||
from \<open>(r, s) \<in> set ps\<close> show "?R (lang (set as) r) (lang (set as) s)"
|
||||
by auto
|
||||
next
|
||||
fix K L assume "?R K L"
|
||||
then obtain r s where rs: "(r, s) \<in> set ps"
|
||||
and KL: "K = lang (set as) r" "L = lang (set as) s" by auto
|
||||
with bisim have "nullable r \<longleftrightarrow> nullable s"
|
||||
by (auto simp: is_bisimulation_def)
|
||||
thus "[] \<in> K \<longleftrightarrow> [] \<in> L" by (auto simp: nullable_iff[where S="set as"] KL)
|
||||
txt\<open>next case, but shared context\<close>
|
||||
from bisim rs KL lang_subset_lists[of _ "set as"]
|
||||
show "K \<subseteq> lists (set as) \<and> L \<subseteq> lists (set as)"
|
||||
unfolding is_bisimulation_def by blast
|
||||
txt\<open>next case, but shared context\<close>
|
||||
fix a assume "a \<in> set as"
|
||||
with rs bisim
|
||||
have "(nderiv a r, nderiv a s) \<in> set ps"
|
||||
by (auto simp: is_bisimulation_def)
|
||||
thus "?R (Deriv a K) (Deriv a L)" using \<open>a \<in> set as\<close>
|
||||
by (force simp: KL lang_nderiv)
|
||||
qed
|
||||
qed
|
||||
|
||||
subsection \<open>Closure computation\<close>
|
||||
|
||||
fun test :: "rexp_pairs * rexp_pairs \<Rightarrow> bool"
|
||||
where "test (ws, ps) = (case ws of [] \<Rightarrow> False | (p,q)#_ \<Rightarrow> nullable p = nullable q)"
|
||||
|
||||
fun step :: "nat list \<Rightarrow> rexp_pairs * rexp_pairs \<Rightarrow> rexp_pairs * rexp_pairs"
|
||||
where "step as (ws,ps) =
|
||||
(let
|
||||
(r, s) = hd ws;
|
||||
ps' = (r, s) # ps;
|
||||
succs = map (\<lambda>a. (nderiv a r, nderiv a s)) as;
|
||||
new = filter (\<lambda>p. p \<notin> set ps' \<union> set ws) succs
|
||||
in (new @ tl ws, ps'))"
|
||||
|
||||
definition closure ::
|
||||
"nat list \<Rightarrow> rexp_pairs * rexp_pairs
|
||||
\<Rightarrow> (rexp_pairs * rexp_pairs) option" where
|
||||
"closure as = while_option test (step as)"
|
||||
|
||||
definition pre_bisim :: "nat list \<Rightarrow> nat rexp \<Rightarrow> nat rexp \<Rightarrow>
|
||||
rexp_pairs * rexp_pairs \<Rightarrow> bool"
|
||||
where
|
||||
"pre_bisim as r s = (\<lambda>(ws,ps).
|
||||
((r, s) \<in> set ws \<union> set ps) \<and>
|
||||
(\<forall>(r,s)\<in> set ws \<union> set ps. atoms r \<union> atoms s \<subseteq> set as) \<and>
|
||||
(\<forall>(r,s)\<in> set ps. (nullable r \<longleftrightarrow> nullable s) \<and>
|
||||
(\<forall>a\<in>set as. (nderiv a r, nderiv a s) \<in> set ps \<union> set ws)))"
|
||||
|
||||
theorem closure_sound:
|
||||
assumes result: "closure as ([(r,s)],[]) = Some([],ps)"
|
||||
and atoms: "atoms r \<union> atoms s \<subseteq> set as"
|
||||
shows "lang (set as) r = lang (set as) s"
|
||||
proof-
|
||||
{ fix st have "pre_bisim as r s st \<Longrightarrow> test st \<Longrightarrow> pre_bisim as r s (step as st)"
|
||||
unfolding pre_bisim_def
|
||||
by (cases st) (auto simp: split_def split: list.splits prod.splits
|
||||
dest!: subsetD[OF atoms_nderiv]) }
|
||||
moreover
|
||||
from atoms
|
||||
have "pre_bisim as r s ([(r,s)],[])" by (simp add: pre_bisim_def)
|
||||
ultimately have pre_bisim_ps: "pre_bisim as r s ([],ps)"
|
||||
by (rule while_option_rule[OF _ result[unfolded closure_def]])
|
||||
then have "is_bisimulation as ps" "(r, s) \<in> set ps"
|
||||
by (auto simp: pre_bisim_def is_bisimulation_def)
|
||||
thus "lang (set as) r = lang (set as) s" by (rule bisim_lang_eq)
|
||||
qed
|
||||
|
||||
|
||||
subsection \<open>The overall procedure\<close>
|
||||
|
||||
primrec add_atoms :: "nat rexp \<Rightarrow> nat list \<Rightarrow> nat list"
|
||||
where
|
||||
"add_atoms Zero = id"
|
||||
| "add_atoms One = id"
|
||||
| "add_atoms (Atom a) = List.insert a"
|
||||
| "add_atoms (Plus r s) = add_atoms s o add_atoms r"
|
||||
| "add_atoms (Times r s) = add_atoms s o add_atoms r"
|
||||
| "add_atoms (Not r) = add_atoms r"
|
||||
| "add_atoms (Inter r s) = add_atoms s o add_atoms r"
|
||||
| "add_atoms (Star r) = add_atoms r"
|
||||
|
||||
lemma set_add_atoms: "set (add_atoms r as) = atoms r \<union> set as"
|
||||
by (induct r arbitrary: as) auto
|
||||
|
||||
definition check_eqv :: "nat list \<Rightarrow> nat rexp \<Rightarrow> nat rexp \<Rightarrow> bool"
|
||||
where
|
||||
"check_eqv as r s \<longleftrightarrow> set(add_atoms r (add_atoms s [])) \<subseteq> set as \<and>
|
||||
(case closure as ([(norm r, norm s)], []) of
|
||||
Some([],_) \<Rightarrow> True | _ \<Rightarrow> False)"
|
||||
|
||||
lemma soundness:
|
||||
assumes "check_eqv as r s" shows "lang (set as) r = lang (set as) s"
|
||||
proof -
|
||||
obtain ps where cl: "closure as ([(norm r,norm s)],[]) = Some([],ps)"
|
||||
and at: "atoms r \<union> atoms s \<subseteq> set as"
|
||||
using assms
|
||||
by (auto simp: check_eqv_def set_add_atoms split:option.splits list.splits)
|
||||
hence "atoms(norm r) \<union> atoms(norm s) \<subseteq> set as"
|
||||
using atoms_norm by blast
|
||||
hence "lang (set as) (norm r) = lang (set as) (norm s)"
|
||||
by (rule closure_sound[OF cl])
|
||||
thus "lang (set as) r = lang (set as) s" by simp
|
||||
qed
|
||||
|
||||
lemma "check_eqv [0] (Plus One (Times (Atom 0) (Star(Atom 0)))) (Star(Atom 0))"
|
||||
by eval
|
||||
|
||||
lemma "check_eqv [0,1] (Not(Atom 0))
|
||||
(Plus One (Times (Plus (Atom 1) (Times (Atom 0) (Plus (Atom 0) (Atom 1))))
|
||||
(Star(Plus (Atom 0) (Atom 1)))))"
|
||||
by eval
|
||||
|
||||
lemma "check_eqv [0] (Atom 0) (Inter (Star (Atom 0)) (Atom 0))"
|
||||
by eval
|
||||
|
||||
end
|
||||
|
|
@ -1,85 +0,0 @@
|
|||
section \<open>Normalizing Derivative\<close>
|
||||
|
||||
theory NDerivative
|
||||
imports
|
||||
Regular_Exp
|
||||
begin
|
||||
|
||||
subsection \<open>Normalizing operations\<close>
|
||||
|
||||
text \<open>associativity, commutativity, idempotence, zero\<close>
|
||||
|
||||
fun nPlus :: "'a::order rexp \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
|
||||
where
|
||||
"nPlus Zero r = r"
|
||||
| "nPlus r Zero = r"
|
||||
| "nPlus (Plus r s) t = nPlus r (nPlus s t)"
|
||||
| "nPlus r (Plus s t) =
|
||||
(if r = s then (Plus s t)
|
||||
else if le_rexp r s then Plus r (Plus s t)
|
||||
else Plus s (nPlus r t))"
|
||||
| "nPlus r s =
|
||||
(if r = s then r
|
||||
else if le_rexp r s then Plus r s
|
||||
else Plus s r)"
|
||||
|
||||
lemma lang_nPlus[simp]: "lang (nPlus r s) = lang (Plus r s)"
|
||||
by (induction r s rule: nPlus.induct) auto
|
||||
|
||||
text \<open>associativity, zero, one\<close>
|
||||
|
||||
fun nTimes :: "'a::order rexp \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
|
||||
where
|
||||
"nTimes Zero _ = Zero"
|
||||
| "nTimes _ Zero = Zero"
|
||||
| "nTimes One r = r"
|
||||
| "nTimes r One = r"
|
||||
| "nTimes (Times r s) t = Times r (nTimes s t)"
|
||||
| "nTimes r s = Times r s"
|
||||
|
||||
lemma lang_nTimes[simp]: "lang (nTimes r s) = lang (Times r s)"
|
||||
by (induction r s rule: nTimes.induct) (auto simp: conc_assoc)
|
||||
|
||||
primrec norm :: "'a::order rexp \<Rightarrow> 'a rexp"
|
||||
where
|
||||
"norm Zero = Zero"
|
||||
| "norm One = One"
|
||||
| "norm (Atom a) = Atom a"
|
||||
| "norm (Plus r s) = nPlus (norm r) (norm s)"
|
||||
| "norm (Times r s) = nTimes (norm r) (norm s)"
|
||||
| "norm (Star r) = Star (norm r)"
|
||||
|
||||
lemma lang_norm[simp]: "lang (norm r) = lang r"
|
||||
by (induct r) auto
|
||||
|
||||
primrec nderiv :: "'a::order \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
|
||||
where
|
||||
"nderiv _ Zero = Zero"
|
||||
| "nderiv _ One = Zero"
|
||||
| "nderiv a (Atom b) = (if a = b then One else Zero)"
|
||||
| "nderiv a (Plus r s) = nPlus (nderiv a r) (nderiv a s)"
|
||||
| "nderiv a (Times r s) =
|
||||
(let r's = nTimes (nderiv a r) s
|
||||
in if nullable r then nPlus r's (nderiv a s) else r's)"
|
||||
| "nderiv a (Star r) = nTimes (nderiv a r) (Star r)"
|
||||
|
||||
lemma lang_nderiv: "lang (nderiv a r) = Deriv a (lang r)"
|
||||
by (induction r) (auto simp: Let_def nullable_iff)
|
||||
|
||||
lemma deriv_no_occurrence:
|
||||
"x \<notin> atoms r \<Longrightarrow> nderiv x r = Zero"
|
||||
by (induction r) auto
|
||||
|
||||
lemma atoms_nPlus[simp]: "atoms (nPlus r s) = atoms r \<union> atoms s"
|
||||
by (induction r s rule: nPlus.induct) auto
|
||||
|
||||
lemma atoms_nTimes: "atoms (nTimes r s) \<subseteq> atoms r \<union> atoms s"
|
||||
by (induction r s rule: nTimes.induct) auto
|
||||
|
||||
lemma atoms_norm: "atoms (norm r) \<subseteq> atoms r"
|
||||
by (induction r) (auto dest!:subsetD[OF atoms_nTimes])
|
||||
|
||||
lemma atoms_nderiv: "atoms (nderiv a r) \<subseteq> atoms r"
|
||||
by (induction r) (auto simp: Let_def dest!:subsetD[OF atoms_nTimes])
|
||||
|
||||
end
|
||||
|
|
@ -1,12 +0,0 @@
|
|||
chapter AFP
|
||||
|
||||
session "Regular-Sets" (AFP) = "HOL-Library" +
|
||||
options [timeout = 600]
|
||||
theories
|
||||
Regexp_Method
|
||||
Regexp_Constructions
|
||||
pEquivalence_Checking
|
||||
Equivalence_Checking2
|
||||
document_files
|
||||
"root.bib"
|
||||
"root.tex"
|
||||
|
|
@ -1,395 +0,0 @@
|
|||
(*
|
||||
File: Regexp_Constructions.thy
|
||||
Author: Manuel Eberl <eberlm@in.tum.de>
|
||||
|
||||
Some simple constructions on regular expressions to illustrate closure properties of regular
|
||||
languages: reversal, substitution, prefixes, suffixes, subwords ("fragments")
|
||||
*)
|
||||
section \<open>Basic constructions on regular expressions\<close>
|
||||
theory Regexp_Constructions
|
||||
imports
|
||||
Main
|
||||
"HOL-Library.Sublist"
|
||||
Regular_Exp
|
||||
begin
|
||||
|
||||
subsection \<open>Reverse language\<close>
|
||||
|
||||
lemma rev_conc [simp]: "rev ` (A @@ B) = rev ` B @@ rev ` A"
|
||||
unfolding conc_def image_def by force
|
||||
|
||||
lemma rev_compower [simp]: "rev ` (A ^^ n) = (rev ` A) ^^ n"
|
||||
by (induction n) (simp_all add: conc_pow_comm)
|
||||
|
||||
lemma rev_star [simp]: "rev ` star A = star (rev ` A)"
|
||||
by (simp add: star_def image_UN)
|
||||
|
||||
|
||||
subsection \<open>Substituting characters in a language\<close>
|
||||
|
||||
definition subst_word :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
|
||||
"subst_word f xs = concat (map f xs)"
|
||||
|
||||
lemma subst_word_Nil [simp]: "subst_word f [] = []"
|
||||
by (simp add: subst_word_def)
|
||||
|
||||
lemma subst_word_singleton [simp]: "subst_word f [x] = f x"
|
||||
by (simp add: subst_word_def)
|
||||
|
||||
lemma subst_word_append [simp]: "subst_word f (xs @ ys) = subst_word f xs @ subst_word f ys"
|
||||
by (simp add: subst_word_def)
|
||||
|
||||
lemma subst_word_Cons [simp]: "subst_word f (x # xs) = f x @ subst_word f xs"
|
||||
by (simp add: subst_word_def)
|
||||
|
||||
lemma subst_word_conc [simp]: "subst_word f ` (A @@ B) = subst_word f ` A @@ subst_word f ` B"
|
||||
unfolding conc_def image_def by force
|
||||
|
||||
lemma subst_word_compower [simp]: "subst_word f ` (A ^^ n) = (subst_word f ` A) ^^ n"
|
||||
by (induction n) simp_all
|
||||
|
||||
lemma subst_word_star [simp]: "subst_word f ` (star A) = star (subst_word f ` A)"
|
||||
by (simp add: star_def image_UN)
|
||||
|
||||
|
||||
text \<open>Suffix language\<close>
|
||||
|
||||
definition Suffixes :: "'a list set \<Rightarrow> 'a list set" where
|
||||
"Suffixes A = {w. \<exists>q. q @ w \<in> A}"
|
||||
|
||||
lemma Suffixes_altdef [code]: "Suffixes A = (\<Union>w\<in>A. set (suffixes w))"
|
||||
unfolding Suffixes_def set_suffixes_eq suffix_def by blast
|
||||
|
||||
lemma Nil_in_Suffixes_iff [simp]: "[] \<in> Suffixes A \<longleftrightarrow> A \<noteq> {}"
|
||||
by (auto simp: Suffixes_def)
|
||||
|
||||
lemma Suffixes_empty [simp]: "Suffixes {} = {}"
|
||||
by (auto simp: Suffixes_def)
|
||||
|
||||
lemma Suffixes_empty_iff [simp]: "Suffixes A = {} \<longleftrightarrow> A = {}"
|
||||
by (auto simp: Suffixes_altdef)
|
||||
|
||||
lemma Suffixes_singleton [simp]: "Suffixes {xs} = set (suffixes xs)"
|
||||
by (auto simp: Suffixes_altdef)
|
||||
|
||||
lemma Suffixes_insert: "Suffixes (insert xs A) = set (suffixes xs) \<union> Suffixes A"
|
||||
by (simp add: Suffixes_altdef)
|
||||
|
||||
lemma Suffixes_conc [simp]: "A \<noteq> {} \<Longrightarrow> Suffixes (A @@ B) = Suffixes B \<union> (Suffixes A @@ B)"
|
||||
unfolding Suffixes_altdef conc_def by (force simp: suffix_append)
|
||||
|
||||
lemma Suffixes_union [simp]: "Suffixes (A \<union> B) = Suffixes A \<union> Suffixes B"
|
||||
by (auto simp: Suffixes_def)
|
||||
|
||||
lemma Suffixes_UNION [simp]: "Suffixes (UNION A f) = UNION A (\<lambda>x. Suffixes (f x))"
|
||||
by (auto simp: Suffixes_def)
|
||||
|
||||
lemma Suffixes_compower:
|
||||
assumes "A \<noteq> {}"
|
||||
shows "Suffixes (A ^^ n) = insert [] (Suffixes A @@ (\<Union>k<n. A ^^ k))"
|
||||
proof (induction n)
|
||||
case (Suc n)
|
||||
from Suc have "Suffixes (A ^^ Suc n) =
|
||||
insert [] (Suffixes A @@ ((\<Union>k<n. A ^^ k) \<union> A ^^ n))"
|
||||
by (simp_all add: assms conc_Un_distrib)
|
||||
also have "(\<Union>k<n. A ^^ k) \<union> A ^^ n = (\<Union>k\<in>insert n {..<n}. A ^^ k)" by blast
|
||||
also have "insert n {..<n} = {..<Suc n}" by auto
|
||||
finally show ?case .
|
||||
qed simp_all
|
||||
|
||||
lemma Suffixes_star [simp]:
|
||||
assumes "A \<noteq> {}"
|
||||
shows "Suffixes (star A) = Suffixes A @@ star A"
|
||||
proof -
|
||||
have "star A = (\<Union>n. A ^^ n)" unfolding star_def ..
|
||||
also have "Suffixes \<dots> = (\<Union>x. Suffixes (A ^^ x))" by simp
|
||||
also have "\<dots> = (\<Union>n. insert [] (Suffixes A @@ (\<Union>k<n. A ^^ k)))"
|
||||
using assms by (subst Suffixes_compower) auto
|
||||
also have "\<dots> = insert [] (Suffixes A @@ (\<Union>n. (\<Union>k<n. A ^^ k)))"
|
||||
by (simp_all add: conc_UNION_distrib)
|
||||
also have "(\<Union>n. (\<Union>k<n. A ^^ k)) = (\<Union>n. A ^^ n)" by auto
|
||||
also have "\<dots> = star A" unfolding star_def ..
|
||||
also have "insert [] (Suffixes A @@ star A) = Suffixes A @@ star A"
|
||||
using assms by auto
|
||||
finally show ?thesis .
|
||||
qed
|
||||
|
||||
text \<open>Prefix language\<close>
|
||||
|
||||
definition Prefixes :: "'a list set \<Rightarrow> 'a list set" where
|
||||
"Prefixes A = {w. \<exists>q. w @ q \<in> A}"
|
||||
|
||||
lemma Prefixes_altdef [code]: "Prefixes A = (\<Union>w\<in>A. set (prefixes w))"
|
||||
unfolding Prefixes_def set_prefixes_eq prefix_def by blast
|
||||
|
||||
lemma Nil_in_Prefixes_iff [simp]: "[] \<in> Prefixes A \<longleftrightarrow> A \<noteq> {}"
|
||||
by (auto simp: Prefixes_def)
|
||||
|
||||
lemma Prefixes_empty [simp]: "Prefixes {} = {}"
|
||||
by (auto simp: Prefixes_def)
|
||||
|
||||
lemma Prefixes_empty_iff [simp]: "Prefixes A = {} \<longleftrightarrow> A = {}"
|
||||
by (auto simp: Prefixes_altdef)
|
||||
|
||||
lemma Prefixes_singleton [simp]: "Prefixes {xs} = set (prefixes xs)"
|
||||
by (auto simp: Prefixes_altdef)
|
||||
|
||||
lemma Prefixes_insert: "Prefixes (insert xs A) = set (prefixes xs) \<union> Prefixes A"
|
||||
by (simp add: Prefixes_altdef)
|
||||
|
||||
lemma Prefixes_conc [simp]: "B \<noteq> {} \<Longrightarrow> Prefixes (A @@ B) = Prefixes A \<union> (A @@ Prefixes B)"
|
||||
unfolding Prefixes_altdef conc_def by (force simp: prefix_append)
|
||||
|
||||
lemma Prefixes_union [simp]: "Prefixes (A \<union> B) = Prefixes A \<union> Prefixes B"
|
||||
by (auto simp: Prefixes_def)
|
||||
|
||||
lemma Prefixes_UNION [simp]: "Prefixes (UNION A f) = UNION A (\<lambda>x. Prefixes (f x))"
|
||||
by (auto simp: Prefixes_def)
|
||||
|
||||
|
||||
lemma Prefixes_rev: "Prefixes (rev ` A) = rev ` Suffixes A"
|
||||
by (auto simp: Prefixes_altdef prefixes_rev Suffixes_altdef)
|
||||
|
||||
lemma Suffixes_rev: "Suffixes (rev ` A) = rev ` Prefixes A"
|
||||
by (auto simp: Prefixes_altdef suffixes_rev Suffixes_altdef)
|
||||
|
||||
|
||||
lemma Prefixes_compower:
|
||||
assumes "A \<noteq> {}"
|
||||
shows "Prefixes (A ^^ n) = insert [] ((\<Union>k<n. A ^^ k) @@ Prefixes A)"
|
||||
proof -
|
||||
have "A ^^ n = rev ` ((rev ` A) ^^ n)" by (simp add: image_image)
|
||||
also have "Prefixes \<dots> = insert [] ((\<Union>k<n. A ^^ k) @@ Prefixes A)"
|
||||
unfolding Prefixes_rev
|
||||
by (subst Suffixes_compower) (simp_all add: image_UN image_image Suffixes_rev assms)
|
||||
finally show ?thesis .
|
||||
qed
|
||||
|
||||
lemma Prefixes_star [simp]:
|
||||
assumes "A \<noteq> {}"
|
||||
shows "Prefixes (star A) = star A @@ Prefixes A"
|
||||
proof -
|
||||
have "star A = rev ` star (rev ` A)" by (simp add: image_image)
|
||||
also have "Prefixes \<dots> = star A @@ Prefixes A"
|
||||
unfolding Prefixes_rev
|
||||
by (subst Suffixes_star) (simp_all add: assms image_image Suffixes_rev)
|
||||
finally show ?thesis .
|
||||
qed
|
||||
|
||||
|
||||
subsection \<open>Subword language\<close>
|
||||
|
||||
text \<open>
|
||||
The language of all sub-words, i.e. all words that are a contiguous sublist of a word in
|
||||
the original language.
|
||||
\<close>
|
||||
definition Sublists :: "'a list set \<Rightarrow> 'a list set" where
|
||||
"Sublists A = {w. \<exists>q\<in>A. sublist w q}"
|
||||
|
||||
lemma Sublists_altdef [code]: "Sublists A = (\<Union>w\<in>A. set (sublists w))"
|
||||
by (auto simp: Sublists_def)
|
||||
|
||||
lemma Sublists_empty [simp]: "Sublists {} = {}"
|
||||
by (auto simp: Sublists_def)
|
||||
|
||||
lemma Sublists_singleton [simp]: "Sublists {w} = set (sublists w)"
|
||||
by (auto simp: Sublists_altdef)
|
||||
|
||||
lemma Sublists_insert: "Sublists (insert w A) = set (sublists w) \<union> Sublists A"
|
||||
by (auto simp: Sublists_altdef)
|
||||
|
||||
lemma Sublists_Un [simp]: "Sublists (A \<union> B) = Sublists A \<union> Sublists B"
|
||||
by (auto simp: Sublists_altdef)
|
||||
|
||||
lemma Sublists_UN [simp]: "Sublists (UNION A f) = UNION A (\<lambda>x. Sublists (f x))"
|
||||
by (auto simp: Sublists_altdef)
|
||||
|
||||
lemma Sublists_conv_Prefixes: "Sublists A = Prefixes (Suffixes A)"
|
||||
by (auto simp: Sublists_def Prefixes_def Suffixes_def sublist_def)
|
||||
|
||||
lemma Sublists_conv_Suffixes: "Sublists A = Suffixes (Prefixes A)"
|
||||
by (auto simp: Sublists_def Prefixes_def Suffixes_def sublist_def)
|
||||
|
||||
lemma Sublists_conc [simp]:
|
||||
assumes "A \<noteq> {}" "B \<noteq> {}"
|
||||
shows "Sublists (A @@ B) = Sublists A \<union> Sublists B \<union> Suffixes A @@ Prefixes B"
|
||||
using assms unfolding Sublists_conv_Suffixes by auto
|
||||
|
||||
lemma star_not_empty [simp]: "star A \<noteq> {}"
|
||||
by auto
|
||||
|
||||
lemma Sublists_star:
|
||||
"A \<noteq> {} \<Longrightarrow> Sublists (star A) = Sublists A \<union> Suffixes A @@ star A @@ Prefixes A"
|
||||
by (simp add: Sublists_conv_Prefixes)
|
||||
|
||||
lemma Prefixes_subset_Sublists: "Prefixes A \<subseteq> Sublists A"
|
||||
unfolding Prefixes_def Sublists_def by auto
|
||||
|
||||
lemma Suffixes_subset_Sublists: "Suffixes A \<subseteq> Sublists A"
|
||||
unfolding Suffixes_def Sublists_def by auto
|
||||
|
||||
|
||||
subsection \<open>Fragment language\<close>
|
||||
|
||||
text \<open>
|
||||
The following is the fragment language of a given language, i.e. the set of all words that
|
||||
are (not necessarily contiguous) sub-sequences of a word in the original language.
|
||||
\<close>
|
||||
definition Subseqs where "Subseqs A = (\<Union>w\<in>A. set (subseqs w))"
|
||||
|
||||
lemma Subseqs_empty [simp]: "Subseqs {} = {}"
|
||||
by (simp add: Subseqs_def)
|
||||
|
||||
lemma Subseqs_insert [simp]: "Subseqs (insert xs A) = set (subseqs xs) \<union> Subseqs A"
|
||||
by (simp add: Subseqs_def)
|
||||
|
||||
lemma Subseqs_singleton [simp]: "Subseqs {xs} = set (subseqs xs)"
|
||||
by simp
|
||||
|
||||
lemma Subseqs_Un [simp]: "Subseqs (A \<union> B) = Subseqs A \<union> Subseqs B"
|
||||
by (simp add: Subseqs_def)
|
||||
|
||||
lemma Subseqs_UNION [simp]: "Subseqs (UNION A f) = UNION A (\<lambda>x. Subseqs (f x))"
|
||||
by (simp add: Subseqs_def)
|
||||
|
||||
lemma Subseqs_conc [simp]: "Subseqs (A @@ B) = Subseqs A @@ Subseqs B"
|
||||
proof safe
|
||||
fix xs assume "xs \<in> Subseqs (A @@ B)"
|
||||
then obtain ys zs where *: "ys \<in> A" "zs \<in> B" "subseq xs (ys @ zs)"
|
||||
by (auto simp: Subseqs_def conc_def)
|
||||
from *(3) obtain xs1 xs2 where "xs = xs1 @ xs2" "subseq xs1 ys" "subseq xs2 zs"
|
||||
by (rule subseq_appendE)
|
||||
with *(1,2) show "xs \<in> Subseqs A @@ Subseqs B" by (auto simp: Subseqs_def set_subseqs_eq)
|
||||
next
|
||||
fix xs assume "xs \<in> Subseqs A @@ Subseqs B"
|
||||
then obtain xs1 xs2 ys zs
|
||||
where "xs = xs1 @ xs2" "subseq xs1 ys" "subseq xs2 zs" "ys \<in> A" "zs \<in> B"
|
||||
by (auto simp: conc_def Subseqs_def)
|
||||
thus "xs \<in> Subseqs (A @@ B)" by (force simp: Subseqs_def conc_def intro: list_emb_append_mono)
|
||||
qed
|
||||
|
||||
lemma Subseqs_compower [simp]: "Subseqs (A ^^ n) = Subseqs A ^^ n"
|
||||
by (induction n) simp_all
|
||||
|
||||
lemma Subseqs_star [simp]: "Subseqs (star A) = star (Subseqs A)"
|
||||
by (simp add: star_def)
|
||||
|
||||
lemma Sublists_subset_Subseqs: "Sublists A \<subseteq> Subseqs A"
|
||||
by (auto simp: Sublists_def Subseqs_def dest!: sublist_imp_subseq)
|
||||
|
||||
|
||||
subsection \<open>Various regular expression constructions\<close>
|
||||
|
||||
text \<open>A construction for language reversal of a regular expression:\<close>
|
||||
|
||||
primrec rexp_rev where
|
||||
"rexp_rev Zero = Zero"
|
||||
| "rexp_rev One = One"
|
||||
| "rexp_rev (Atom x) = Atom x"
|
||||
| "rexp_rev (Plus r s) = Plus (rexp_rev r) (rexp_rev s)"
|
||||
| "rexp_rev (Times r s) = Times (rexp_rev s) (rexp_rev r)"
|
||||
| "rexp_rev (Star r) = Star (rexp_rev r)"
|
||||
|
||||
lemma lang_rexp_rev [simp]: "lang (rexp_rev r) = rev ` lang r"
|
||||
by (induction r) (simp_all add: image_Un)
|
||||
|
||||
|
||||
text \<open>The obvious construction for a singleton-language regular expression:\<close>
|
||||
|
||||
fun rexp_of_word where
|
||||
"rexp_of_word [] = One"
|
||||
| "rexp_of_word [x] = Atom x"
|
||||
| "rexp_of_word (x#xs) = Times (Atom x) (rexp_of_word xs)"
|
||||
|
||||
lemma lang_rexp_of_word [simp]: "lang (rexp_of_word xs) = {xs}"
|
||||
by (induction xs rule: rexp_of_word.induct) (simp_all add: conc_def)
|
||||
|
||||
lemma size_rexp_of_word [simp]: "size (rexp_of_word xs) = Suc (2 * (length xs - 1))"
|
||||
by (induction xs rule: rexp_of_word.induct) auto
|
||||
|
||||
|
||||
text \<open>Character substitution in a regular expression:\<close>
|
||||
|
||||
primrec rexp_subst where
|
||||
"rexp_subst f Zero = Zero"
|
||||
| "rexp_subst f One = One"
|
||||
| "rexp_subst f (Atom x) = rexp_of_word (f x)"
|
||||
| "rexp_subst f (Plus r s) = Plus (rexp_subst f r) (rexp_subst f s)"
|
||||
| "rexp_subst f (Times r s) = Times (rexp_subst f r) (rexp_subst f s)"
|
||||
| "rexp_subst f (Star r) = Star (rexp_subst f r)"
|
||||
|
||||
lemma lang_rexp_subst: "lang (rexp_subst f r) = subst_word f ` lang r"
|
||||
by (induction r) (simp_all add: image_Un)
|
||||
|
||||
|
||||
text \<open>Suffix language of a regular expression:\<close>
|
||||
|
||||
primrec suffix_rexp :: "'a rexp \<Rightarrow> 'a rexp" where
|
||||
"suffix_rexp Zero = Zero"
|
||||
| "suffix_rexp One = One"
|
||||
| "suffix_rexp (Atom a) = Plus (Atom a) One"
|
||||
| "suffix_rexp (Plus r s) = Plus (suffix_rexp r) (suffix_rexp s)"
|
||||
| "suffix_rexp (Times r s) =
|
||||
(if rexp_empty r then Zero else Plus (Times (suffix_rexp r) s) (suffix_rexp s))"
|
||||
| "suffix_rexp (Star r) =
|
||||
(if rexp_empty r then One else Times (suffix_rexp r) (Star r))"
|
||||
|
||||
theorem lang_suffix_rexp [simp]:
|
||||
"lang (suffix_rexp r) = Suffixes (lang r)"
|
||||
by (induction r) (auto simp: rexp_empty_iff)
|
||||
|
||||
|
||||
text \<open>Prefix language of a regular expression:\<close>
|
||||
|
||||
primrec prefix_rexp :: "'a rexp \<Rightarrow> 'a rexp" where
|
||||
"prefix_rexp Zero = Zero"
|
||||
| "prefix_rexp One = One"
|
||||
| "prefix_rexp (Atom a) = Plus (Atom a) One"
|
||||
| "prefix_rexp (Plus r s) = Plus (prefix_rexp r) (prefix_rexp s)"
|
||||
| "prefix_rexp (Times r s) =
|
||||
(if rexp_empty s then Zero else Plus (Times r (prefix_rexp s)) (prefix_rexp r))"
|
||||
| "prefix_rexp (Star r) =
|
||||
(if rexp_empty r then One else Times (Star r) (prefix_rexp r))"
|
||||
|
||||
theorem lang_prefix_rexp [simp]:
|
||||
"lang (prefix_rexp r) = Prefixes (lang r)"
|
||||
by (induction r) (auto simp: rexp_empty_iff)
|
||||
|
||||
|
||||
text \<open>Sub-word language of a regular expression\<close>
|
||||
|
||||
primrec sublist_rexp :: "'a rexp \<Rightarrow> 'a rexp" where
|
||||
"sublist_rexp Zero = Zero"
|
||||
| "sublist_rexp One = One"
|
||||
| "sublist_rexp (Atom a) = Plus (Atom a) One"
|
||||
| "sublist_rexp (Plus r s) = Plus (sublist_rexp r) (sublist_rexp s)"
|
||||
| "sublist_rexp (Times r s) =
|
||||
(if rexp_empty r \<or> rexp_empty s then Zero else
|
||||
Plus (sublist_rexp r) (Plus (sublist_rexp s) (Times (suffix_rexp r) (prefix_rexp s))))"
|
||||
| "sublist_rexp (Star r) =
|
||||
(if rexp_empty r then One else
|
||||
Plus (sublist_rexp r) (Times (suffix_rexp r) (Times (Star r) (prefix_rexp r))))"
|
||||
|
||||
theorem lang_sublist_rexp [simp]:
|
||||
"lang (sublist_rexp r) = Sublists (lang r)"
|
||||
by (induction r) (auto simp: rexp_empty_iff Sublists_star)
|
||||
|
||||
|
||||
text \<open>Fragment language of a regular expression:\<close>
|
||||
|
||||
primrec subseqs_rexp :: "'a rexp \<Rightarrow> 'a rexp" where
|
||||
"subseqs_rexp Zero = Zero"
|
||||
| "subseqs_rexp One = One"
|
||||
| "subseqs_rexp (Atom x) = Plus (Atom x) One"
|
||||
| "subseqs_rexp (Plus r s) = Plus (subseqs_rexp r) (subseqs_rexp s)"
|
||||
| "subseqs_rexp (Times r s) = Times (subseqs_rexp r) (subseqs_rexp s)"
|
||||
| "subseqs_rexp (Star r) = Star (subseqs_rexp r)"
|
||||
|
||||
lemma lang_subseqs_rexp [simp]: "lang (subseqs_rexp r) = Subseqs (lang r)"
|
||||
by (induction r) auto
|
||||
|
||||
|
||||
text \<open>Subword language of a regular expression\<close>
|
||||
|
||||
|
||||
end
|
||||
|
|
@ -1,67 +0,0 @@
|
|||
section \<open>Proving Relation (In)equalities via Regular Expressions\<close>
|
||||
|
||||
theory Regexp_Method
|
||||
imports Equivalence_Checking Relation_Interpretation
|
||||
begin
|
||||
|
||||
primrec rel_of_regexp :: "('a * 'a) set list \<Rightarrow> nat rexp \<Rightarrow> ('a * 'a) set" where
|
||||
"rel_of_regexp vs Zero = {}" |
|
||||
"rel_of_regexp vs One = Id" |
|
||||
"rel_of_regexp vs (Atom i) = vs ! i" |
|
||||
"rel_of_regexp vs (Plus r s) = rel_of_regexp vs r \<union> rel_of_regexp vs s " |
|
||||
"rel_of_regexp vs (Times r s) = rel_of_regexp vs r O rel_of_regexp vs s" |
|
||||
"rel_of_regexp vs (Star r) = (rel_of_regexp vs r)^*"
|
||||
|
||||
lemma rel_of_regexp_rel: "rel_of_regexp vs r = rel (\<lambda>i. vs ! i) r"
|
||||
by (induct r) auto
|
||||
|
||||
primrec rel_eq where
|
||||
"rel_eq (r, s) vs = (rel_of_regexp vs r = rel_of_regexp vs s)"
|
||||
|
||||
lemma rel_eqI: "check_eqv r s \<Longrightarrow> rel_eq (r, s) vs"
|
||||
unfolding rel_eq.simps rel_of_regexp_rel
|
||||
by (rule Relation_Interpretation.soundness)
|
||||
(rule Equivalence_Checking.soundness)
|
||||
|
||||
lemmas regexp_reify = rel_of_regexp.simps rel_eq.simps
|
||||
lemmas regexp_unfold = trancl_unfold_left subset_Un_eq
|
||||
|
||||
ML \<open>
|
||||
local
|
||||
|
||||
fun check_eqv (ct, b) = Thm.mk_binop @{cterm "Pure.eq :: bool \<Rightarrow> bool \<Rightarrow> prop"}
|
||||
ct (if b then @{cterm True} else @{cterm False});
|
||||
|
||||
val (_, check_eqv_oracle) = Context.>>> (Context.map_theory_result
|
||||
(Thm.add_oracle (@{binding check_eqv}, check_eqv)));
|
||||
|
||||
in
|
||||
|
||||
val regexp_conv =
|
||||
@{computation_conv bool terms: check_eqv datatypes: "nat rexp"}
|
||||
(fn _ => fn b => fn ct => check_eqv_oracle (ct, b))
|
||||
|
||||
end
|
||||
\<close>
|
||||
|
||||
method_setup regexp = \<open>
|
||||
Scan.succeed (fn ctxt =>
|
||||
SIMPLE_METHOD' (
|
||||
(TRY o eresolve_tac ctxt @{thms rev_subsetD})
|
||||
THEN' (Subgoal.FOCUS_PARAMS (fn {context = ctxt', ...} =>
|
||||
TRY (Local_Defs.unfold_tac ctxt' @{thms regexp_unfold})
|
||||
THEN Reification.tac ctxt' @{thms regexp_reify} NONE 1
|
||||
THEN resolve_tac ctxt' @{thms rel_eqI} 1
|
||||
THEN CONVERSION (HOLogic.Trueprop_conv (regexp_conv ctxt')) 1
|
||||
THEN resolve_tac ctxt' [TrueI] 1) ctxt)))
|
||||
\<close> \<open>decide relation equalities via regular expressions\<close>
|
||||
|
||||
hide_const (open) le_rexp nPlus nTimes norm nullable bisimilar is_bisimulation closure
|
||||
pre_bisim add_atoms check_eqv rel word_rel rel_eq
|
||||
|
||||
text \<open>Example:\<close>
|
||||
|
||||
lemma "(r \<union> s^+)^* = (r \<union> s)^*"
|
||||
by regexp
|
||||
|
||||
end
|
||||
|
|
@ -1,176 +0,0 @@
|
|||
(* Author: Tobias Nipkow *)
|
||||
|
||||
section "Regular expressions"
|
||||
|
||||
theory Regular_Exp
|
||||
imports Regular_Set
|
||||
begin
|
||||
|
||||
datatype (atoms: 'a) rexp =
|
||||
is_Zero: Zero |
|
||||
is_One: One |
|
||||
Atom 'a |
|
||||
Plus "('a rexp)" "('a rexp)" |
|
||||
Times "('a rexp)" "('a rexp)" |
|
||||
Star "('a rexp)"
|
||||
|
||||
primrec lang :: "'a rexp => 'a lang" where
|
||||
"lang Zero = {}" |
|
||||
"lang One = {[]}" |
|
||||
"lang (Atom a) = {[a]}" |
|
||||
"lang (Plus r s) = (lang r) Un (lang s)" |
|
||||
"lang (Times r s) = conc (lang r) (lang s)" |
|
||||
"lang (Star r) = star(lang r)"
|
||||
|
||||
abbreviation (input) regular_lang where "regular_lang A \<equiv> (\<exists>r. lang r = A)"
|
||||
|
||||
primrec nullable :: "'a rexp \<Rightarrow> bool" where
|
||||
"nullable Zero = False" |
|
||||
"nullable One = True" |
|
||||
"nullable (Atom c) = False" |
|
||||
"nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)" |
|
||||
"nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)" |
|
||||
"nullable (Star r) = True"
|
||||
|
||||
lemma nullable_iff [code_abbrev]: "nullable r \<longleftrightarrow> [] \<in> lang r"
|
||||
by (induct r) (auto simp add: conc_def split: if_splits)
|
||||
|
||||
primrec rexp_empty where
|
||||
"rexp_empty Zero \<longleftrightarrow> True"
|
||||
| "rexp_empty One \<longleftrightarrow> False"
|
||||
| "rexp_empty (Atom a) \<longleftrightarrow> False"
|
||||
| "rexp_empty (Plus r s) \<longleftrightarrow> rexp_empty r \<and> rexp_empty s"
|
||||
| "rexp_empty (Times r s) \<longleftrightarrow> rexp_empty r \<or> rexp_empty s"
|
||||
| "rexp_empty (Star r) \<longleftrightarrow> False"
|
||||
|
||||
(* TODO Fixme: This code_abbrev rule does not work. Why? *)
|
||||
lemma rexp_empty_iff [code_abbrev]: "rexp_empty r \<longleftrightarrow> lang r = {}"
|
||||
by (induction r) auto
|
||||
|
||||
|
||||
|
||||
text\<open>Composition on rhs usually complicates matters:\<close>
|
||||
lemma map_map_rexp:
|
||||
"map_rexp f (map_rexp g r) = map_rexp (\<lambda>r. f (g r)) r"
|
||||
unfolding rexp.map_comp o_def ..
|
||||
|
||||
lemma map_rexp_ident[simp]: "map_rexp (\<lambda>x. x) = (\<lambda>r. r)"
|
||||
unfolding id_def[symmetric] fun_eq_iff rexp.map_id id_apply by (intro allI refl)
|
||||
|
||||
lemma atoms_lang: "w : lang r \<Longrightarrow> set w \<subseteq> atoms r"
|
||||
proof(induction r arbitrary: w)
|
||||
case Times thus ?case by fastforce
|
||||
next
|
||||
case Star thus ?case by (fastforce simp add: star_conv_concat)
|
||||
qed auto
|
||||
|
||||
lemma lang_eq_ext: "(lang r = lang s) =
|
||||
(\<forall>w \<in> lists(atoms r \<union> atoms s). w \<in> lang r \<longleftrightarrow> w \<in> lang s)"
|
||||
by (auto simp: atoms_lang[unfolded subset_iff])
|
||||
|
||||
lemma lang_eq_ext_Nil_fold_Deriv:
|
||||
fixes r s
|
||||
defines "\<BB> \<equiv> {(fold Deriv w (lang r), fold Deriv w (lang s))| w. w\<in>lists (atoms r \<union> atoms s)}"
|
||||
shows "lang r = lang s \<longleftrightarrow> (\<forall>(K, L) \<in> \<BB>. [] \<in> K \<longleftrightarrow> [] \<in> L)"
|
||||
unfolding lang_eq_ext \<BB>_def by (subst (1 2) in_fold_Deriv[of "[]", simplified, symmetric]) auto
|
||||
|
||||
|
||||
subsection \<open>Term ordering\<close>
|
||||
|
||||
instantiation rexp :: (order) "{order}"
|
||||
begin
|
||||
|
||||
fun le_rexp :: "('a::order) rexp \<Rightarrow> ('a::order) rexp \<Rightarrow> bool"
|
||||
where
|
||||
"le_rexp Zero _ = True"
|
||||
| "le_rexp _ Zero = False"
|
||||
| "le_rexp One _ = True"
|
||||
| "le_rexp _ One = False"
|
||||
| "le_rexp (Atom a) (Atom b) = (a <= b)"
|
||||
| "le_rexp (Atom _) _ = True"
|
||||
| "le_rexp _ (Atom _) = False"
|
||||
| "le_rexp (Star r) (Star s) = le_rexp r s"
|
||||
| "le_rexp (Star _) _ = True"
|
||||
| "le_rexp _ (Star _) = False"
|
||||
| "le_rexp (Plus r r') (Plus s s') =
|
||||
(if r = s then le_rexp r' s' else le_rexp r s)"
|
||||
| "le_rexp (Plus _ _) _ = True"
|
||||
| "le_rexp _ (Plus _ _) = False"
|
||||
| "le_rexp (Times r r') (Times s s') =
|
||||
(if r = s then le_rexp r' s' else le_rexp r s)"
|
||||
|
||||
(* The class instance stuff is by Dmitriy Traytel *)
|
||||
|
||||
definition less_eq_rexp where "r \<le> s \<equiv> le_rexp r s"
|
||||
definition less_rexp where "r < s \<equiv> le_rexp r s \<and> r \<noteq> s"
|
||||
|
||||
lemma le_rexp_Zero: "le_rexp r Zero \<Longrightarrow> r = Zero"
|
||||
by (induction r) auto
|
||||
|
||||
lemma le_rexp_refl: "le_rexp r r"
|
||||
by (induction r) auto
|
||||
|
||||
lemma le_rexp_antisym: "\<lbrakk>le_rexp r s; le_rexp s r\<rbrakk> \<Longrightarrow> r = s"
|
||||
by (induction r s rule: le_rexp.induct) (auto dest: le_rexp_Zero)
|
||||
|
||||
lemma le_rexp_trans: "\<lbrakk>le_rexp r s; le_rexp s t\<rbrakk> \<Longrightarrow> le_rexp r t"
|
||||
proof (induction r s arbitrary: t rule: le_rexp.induct)
|
||||
fix v t assume "le_rexp (Atom v) t" thus "le_rexp One t" by (cases t) auto
|
||||
next
|
||||
fix s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp One t" by (cases t) auto
|
||||
next
|
||||
fix s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp One t" by (cases t) auto
|
||||
next
|
||||
fix s t assume "le_rexp (Star s) t" thus "le_rexp One t" by (cases t) auto
|
||||
next
|
||||
fix v u t assume "le_rexp (Atom v) (Atom u)" "le_rexp (Atom u) t"
|
||||
thus "le_rexp (Atom v) t" by (cases t) auto
|
||||
next
|
||||
fix v s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp (Atom v) t" by (cases t) auto
|
||||
next
|
||||
fix v s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Atom v) t" by (cases t) auto
|
||||
next
|
||||
fix v s t assume "le_rexp (Star s) t" thus "le_rexp (Atom v) t" by (cases t) auto
|
||||
next
|
||||
fix r s t
|
||||
assume IH: "\<And>t. le_rexp r s \<Longrightarrow> le_rexp s t \<Longrightarrow> le_rexp r t"
|
||||
and "le_rexp (Star r) (Star s)" "le_rexp (Star s) t"
|
||||
thus "le_rexp (Star r) t" by (cases t) auto
|
||||
next
|
||||
fix r s1 s2 t assume "le_rexp (Plus s1 s2) t" thus "le_rexp (Star r) t" by (cases t) auto
|
||||
next
|
||||
fix r s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Star r) t" by (cases t) auto
|
||||
next
|
||||
fix r1 r2 s1 s2 t
|
||||
assume "\<And>t. r1 = s1 \<Longrightarrow> le_rexp r2 s2 \<Longrightarrow> le_rexp s2 t \<Longrightarrow> le_rexp r2 t"
|
||||
"\<And>t. r1 \<noteq> s1 \<Longrightarrow> le_rexp r1 s1 \<Longrightarrow> le_rexp s1 t \<Longrightarrow> le_rexp r1 t"
|
||||
"le_rexp (Plus r1 r2) (Plus s1 s2)" "le_rexp (Plus s1 s2) t"
|
||||
thus "le_rexp (Plus r1 r2) t" by (cases t) (auto split: if_split_asm intro: le_rexp_antisym)
|
||||
next
|
||||
fix r1 r2 s1 s2 t assume "le_rexp (Times s1 s2) t" thus "le_rexp (Plus r1 r2) t" by (cases t) auto
|
||||
next
|
||||
fix r1 r2 s1 s2 t
|
||||
assume "\<And>t. r1 = s1 \<Longrightarrow> le_rexp r2 s2 \<Longrightarrow> le_rexp s2 t \<Longrightarrow> le_rexp r2 t"
|
||||
"\<And>t. r1 \<noteq> s1 \<Longrightarrow> le_rexp r1 s1 \<Longrightarrow> le_rexp s1 t \<Longrightarrow> le_rexp r1 t"
|
||||
"le_rexp (Times r1 r2) (Times s1 s2)" "le_rexp (Times s1 s2) t"
|
||||
thus "le_rexp (Times r1 r2) t" by (cases t) (auto split: if_split_asm intro: le_rexp_antisym)
|
||||
qed auto
|
||||
|
||||
instance proof
|
||||
qed (auto simp add: less_eq_rexp_def less_rexp_def
|
||||
intro: le_rexp_refl le_rexp_antisym le_rexp_trans)
|
||||
|
||||
end
|
||||
|
||||
instantiation rexp :: (linorder) "{linorder}"
|
||||
begin
|
||||
|
||||
lemma le_rexp_total: "le_rexp (r :: 'a :: linorder rexp) s \<or> le_rexp s r"
|
||||
by (induction r s rule: le_rexp.induct) auto
|
||||
|
||||
instance proof
|
||||
qed (unfold less_eq_rexp_def less_rexp_def, rule le_rexp_total)
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
|
|
@ -1,51 +0,0 @@
|
|||
(* Author: Tobias Nipkow *)
|
||||
|
||||
section "Extended Regular Expressions"
|
||||
|
||||
theory Regular_Exp2
|
||||
imports Regular_Set
|
||||
begin
|
||||
|
||||
datatype (atoms: 'a) rexp =
|
||||
is_Zero: Zero |
|
||||
is_One: One |
|
||||
Atom 'a |
|
||||
Plus "('a rexp)" "('a rexp)" |
|
||||
Times "('a rexp)" "('a rexp)" |
|
||||
Star "('a rexp)" |
|
||||
Not "('a rexp)" |
|
||||
Inter "('a rexp)" "('a rexp)"
|
||||
|
||||
context
|
||||
fixes S :: "'a set"
|
||||
begin
|
||||
|
||||
primrec lang :: "'a rexp => 'a lang" where
|
||||
"lang Zero = {}" |
|
||||
"lang One = {[]}" |
|
||||
"lang (Atom a) = {[a]}" |
|
||||
"lang (Plus r s) = (lang r) Un (lang s)" |
|
||||
"lang (Times r s) = conc (lang r) (lang s)" |
|
||||
"lang (Star r) = star(lang r)" |
|
||||
"lang (Not r) = lists S - lang r" |
|
||||
"lang (Inter r s) = (lang r Int lang s)"
|
||||
|
||||
end
|
||||
|
||||
lemma lang_subset_lists: "atoms r \<subseteq> S \<Longrightarrow> lang S r \<subseteq> lists S"
|
||||
by(induction r)(auto simp: conc_subset_lists star_subset_lists)
|
||||
|
||||
primrec nullable :: "'a rexp \<Rightarrow> bool" where
|
||||
"nullable Zero = False" |
|
||||
"nullable One = True" |
|
||||
"nullable (Atom c) = False" |
|
||||
"nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)" |
|
||||
"nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)" |
|
||||
"nullable (Star r) = True" |
|
||||
"nullable (Not r) = (\<not> (nullable r))" |
|
||||
"nullable (Inter r s) = (nullable r \<and> nullable s)"
|
||||
|
||||
lemma nullable_iff: "nullable r \<longleftrightarrow> [] \<in> lang S r"
|
||||
by (induct r) (auto simp add: conc_def split: if_splits)
|
||||
|
||||
end
|
||||
|
|
@ -1,456 +0,0 @@
|
|||
(* Author: Tobias Nipkow, Alex Krauss, Christian Urban *)
|
||||
|
||||
section "Regular sets"
|
||||
|
||||
theory Regular_Set
|
||||
imports Main
|
||||
begin
|
||||
|
||||
type_synonym 'a lang = "'a list set"
|
||||
|
||||
definition conc :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang" (infixr "@@" 75) where
|
||||
"A @@ B = {xs@ys | xs ys. xs:A & ys:B}"
|
||||
|
||||
text \<open>checks the code preprocessor for set comprehensions\<close>
|
||||
export_code conc checking SML
|
||||
|
||||
overloading lang_pow == "compow :: nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
|
||||
begin
|
||||
primrec lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where
|
||||
"lang_pow 0 A = {[]}" |
|
||||
"lang_pow (Suc n) A = A @@ (lang_pow n A)"
|
||||
end
|
||||
|
||||
text \<open>for code generation\<close>
|
||||
|
||||
definition lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where
|
||||
lang_pow_code_def [code_abbrev]: "lang_pow = compow"
|
||||
|
||||
lemma [code]:
|
||||
"lang_pow (Suc n) A = A @@ (lang_pow n A)"
|
||||
"lang_pow 0 A = {[]}"
|
||||
by (simp_all add: lang_pow_code_def)
|
||||
|
||||
hide_const (open) lang_pow
|
||||
|
||||
definition star :: "'a lang \<Rightarrow> 'a lang" where
|
||||
"star A = (\<Union>n. A ^^ n)"
|
||||
|
||||
|
||||
subsection\<open>@{term "(@@)"}\<close>
|
||||
|
||||
lemma concI[simp,intro]: "u : A \<Longrightarrow> v : B \<Longrightarrow> u@v : A @@ B"
|
||||
by (auto simp add: conc_def)
|
||||
|
||||
lemma concE[elim]:
|
||||
assumes "w \<in> A @@ B"
|
||||
obtains u v where "u \<in> A" "v \<in> B" "w = u@v"
|
||||
using assms by (auto simp: conc_def)
|
||||
|
||||
lemma conc_mono: "A \<subseteq> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> A @@ B \<subseteq> C @@ D"
|
||||
by (auto simp: conc_def)
|
||||
|
||||
lemma conc_empty[simp]: shows "{} @@ A = {}" and "A @@ {} = {}"
|
||||
by auto
|
||||
|
||||
lemma conc_epsilon[simp]: shows "{[]} @@ A = A" and "A @@ {[]} = A"
|
||||
by (simp_all add:conc_def)
|
||||
|
||||
lemma conc_assoc: "(A @@ B) @@ C = A @@ (B @@ C)"
|
||||
by (auto elim!: concE) (simp only: append_assoc[symmetric] concI)
|
||||
|
||||
lemma conc_Un_distrib:
|
||||
shows "A @@ (B \<union> C) = A @@ B \<union> A @@ C"
|
||||
and "(A \<union> B) @@ C = A @@ C \<union> B @@ C"
|
||||
by auto
|
||||
|
||||
lemma conc_UNION_distrib:
|
||||
shows "A @@ UNION I M = UNION I (%i. A @@ M i)"
|
||||
and "UNION I M @@ A = UNION I (%i. M i @@ A)"
|
||||
by auto
|
||||
|
||||
lemma conc_subset_lists: "A \<subseteq> lists S \<Longrightarrow> B \<subseteq> lists S \<Longrightarrow> A @@ B \<subseteq> lists S"
|
||||
by(fastforce simp: conc_def in_lists_conv_set)
|
||||
|
||||
lemma Nil_in_conc[simp]: "[] \<in> A @@ B \<longleftrightarrow> [] \<in> A \<and> [] \<in> B"
|
||||
by (metis append_is_Nil_conv concE concI)
|
||||
|
||||
lemma concI_if_Nil1: "[] \<in> A \<Longrightarrow> xs : B \<Longrightarrow> xs \<in> A @@ B"
|
||||
by (metis append_Nil concI)
|
||||
|
||||
lemma conc_Diff_if_Nil1: "[] \<in> A \<Longrightarrow> A @@ B = (A - {[]}) @@ B \<union> B"
|
||||
by (fastforce elim: concI_if_Nil1)
|
||||
|
||||
lemma concI_if_Nil2: "[] \<in> B \<Longrightarrow> xs : A \<Longrightarrow> xs \<in> A @@ B"
|
||||
by (metis append_Nil2 concI)
|
||||
|
||||
lemma conc_Diff_if_Nil2: "[] \<in> B \<Longrightarrow> A @@ B = A @@ (B - {[]}) \<union> A"
|
||||
by (fastforce elim: concI_if_Nil2)
|
||||
|
||||
lemma singleton_in_conc:
|
||||
"[x] : A @@ B \<longleftrightarrow> [x] : A \<and> [] : B \<or> [] : A \<and> [x] : B"
|
||||
by (fastforce simp: Cons_eq_append_conv append_eq_Cons_conv
|
||||
conc_Diff_if_Nil1 conc_Diff_if_Nil2)
|
||||
|
||||
|
||||
subsection\<open>@{term "A ^^ n"}\<close>
|
||||
|
||||
lemma lang_pow_add: "A ^^ (n + m) = A ^^ n @@ A ^^ m"
|
||||
by (induct n) (auto simp: conc_assoc)
|
||||
|
||||
lemma lang_pow_empty: "{} ^^ n = (if n = 0 then {[]} else {})"
|
||||
by (induct n) auto
|
||||
|
||||
lemma lang_pow_empty_Suc[simp]: "({}::'a lang) ^^ Suc n = {}"
|
||||
by (simp add: lang_pow_empty)
|
||||
|
||||
lemma conc_pow_comm:
|
||||
shows "A @@ (A ^^ n) = (A ^^ n) @@ A"
|
||||
by (induct n) (simp_all add: conc_assoc[symmetric])
|
||||
|
||||
lemma length_lang_pow_ub:
|
||||
"\<forall>w \<in> A. length w \<le> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<le> k*n"
|
||||
by(induct n arbitrary: w) (fastforce simp: conc_def)+
|
||||
|
||||
lemma length_lang_pow_lb:
|
||||
"\<forall>w \<in> A. length w \<ge> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<ge> k*n"
|
||||
by(induct n arbitrary: w) (fastforce simp: conc_def)+
|
||||
|
||||
lemma lang_pow_subset_lists: "A \<subseteq> lists S \<Longrightarrow> A ^^ n \<subseteq> lists S"
|
||||
by(induct n)(auto simp: conc_subset_lists)
|
||||
|
||||
|
||||
subsection\<open>@{const star}\<close>
|
||||
|
||||
lemma star_subset_lists: "A \<subseteq> lists S \<Longrightarrow> star A \<subseteq> lists S"
|
||||
unfolding star_def by(blast dest: lang_pow_subset_lists)
|
||||
|
||||
lemma star_if_lang_pow[simp]: "w : A ^^ n \<Longrightarrow> w : star A"
|
||||
by (auto simp: star_def)
|
||||
|
||||
lemma Nil_in_star[iff]: "[] : star A"
|
||||
proof (rule star_if_lang_pow)
|
||||
show "[] : A ^^ 0" by simp
|
||||
qed
|
||||
|
||||
lemma star_if_lang[simp]: assumes "w : A" shows "w : star A"
|
||||
proof (rule star_if_lang_pow)
|
||||
show "w : A ^^ 1" using \<open>w : A\<close> by simp
|
||||
qed
|
||||
|
||||
lemma append_in_starI[simp]:
|
||||
assumes "u : star A" and "v : star A" shows "u@v : star A"
|
||||
proof -
|
||||
from \<open>u : star A\<close> obtain m where "u : A ^^ m" by (auto simp: star_def)
|
||||
moreover
|
||||
from \<open>v : star A\<close> obtain n where "v : A ^^ n" by (auto simp: star_def)
|
||||
ultimately have "u@v : A ^^ (m+n)" by (simp add: lang_pow_add)
|
||||
thus ?thesis by simp
|
||||
qed
|
||||
|
||||
lemma conc_star_star: "star A @@ star A = star A"
|
||||
by (auto simp: conc_def)
|
||||
|
||||
lemma conc_star_comm:
|
||||
shows "A @@ star A = star A @@ A"
|
||||
unfolding star_def conc_pow_comm conc_UNION_distrib
|
||||
by simp
|
||||
|
||||
lemma star_induct[consumes 1, case_names Nil append, induct set: star]:
|
||||
assumes "w : star A"
|
||||
and "P []"
|
||||
and step: "!!u v. u : A \<Longrightarrow> v : star A \<Longrightarrow> P v \<Longrightarrow> P (u@v)"
|
||||
shows "P w"
|
||||
proof -
|
||||
{ fix n have "w : A ^^ n \<Longrightarrow> P w"
|
||||
by (induct n arbitrary: w) (auto intro: \<open>P []\<close> step star_if_lang_pow) }
|
||||
with \<open>w : star A\<close> show "P w" by (auto simp: star_def)
|
||||
qed
|
||||
|
||||
lemma star_empty[simp]: "star {} = {[]}"
|
||||
by (auto elim: star_induct)
|
||||
|
||||
lemma star_epsilon[simp]: "star {[]} = {[]}"
|
||||
by (auto elim: star_induct)
|
||||
|
||||
lemma star_idemp[simp]: "star (star A) = star A"
|
||||
by (auto elim: star_induct)
|
||||
|
||||
lemma star_unfold_left: "star A = A @@ star A \<union> {[]}" (is "?L = ?R")
|
||||
proof
|
||||
show "?L \<subseteq> ?R" by (rule, erule star_induct) auto
|
||||
qed auto
|
||||
|
||||
lemma concat_in_star: "set ws \<subseteq> A \<Longrightarrow> concat ws : star A"
|
||||
by (induct ws) simp_all
|
||||
|
||||
lemma in_star_iff_concat:
|
||||
"w \<in> star A = (\<exists>ws. set ws \<subseteq> A \<and> w = concat ws)"
|
||||
(is "_ = (\<exists>ws. ?R w ws)")
|
||||
proof
|
||||
assume "w : star A" thus "\<exists>ws. ?R w ws"
|
||||
proof induct
|
||||
case Nil have "?R [] []" by simp
|
||||
thus ?case ..
|
||||
next
|
||||
case (append u v)
|
||||
then obtain ws where "set ws \<subseteq> A \<and> v = concat ws" by blast
|
||||
with append have "?R (u@v) (u#ws)" by auto
|
||||
thus ?case ..
|
||||
qed
|
||||
next
|
||||
assume "\<exists>us. ?R w us" thus "w : star A"
|
||||
by (auto simp: concat_in_star)
|
||||
qed
|
||||
|
||||
lemma star_conv_concat: "star A = {concat ws|ws. set ws \<subseteq> A}"
|
||||
by (fastforce simp: in_star_iff_concat)
|
||||
|
||||
lemma star_insert_eps[simp]: "star (insert [] A) = star(A)"
|
||||
proof-
|
||||
{ fix us
|
||||
have "set us \<subseteq> insert [] A \<Longrightarrow> \<exists>vs. concat us = concat vs \<and> set vs \<subseteq> A"
|
||||
(is "?P \<Longrightarrow> \<exists>vs. ?Q vs")
|
||||
proof
|
||||
let ?vs = "filter (%u. u \<noteq> []) us"
|
||||
show "?P \<Longrightarrow> ?Q ?vs" by (induct us) auto
|
||||
qed
|
||||
} thus ?thesis by (auto simp: star_conv_concat)
|
||||
qed
|
||||
|
||||
lemma star_unfold_left_Nil: "star A = (A - {[]}) @@ (star A) \<union> {[]}"
|
||||
by (metis insert_Diff_single star_insert_eps star_unfold_left)
|
||||
|
||||
lemma star_Diff_Nil_fold: "(A - {[]}) @@ star A = star A - {[]}"
|
||||
proof -
|
||||
have "[] \<notin> (A - {[]}) @@ star A" by simp
|
||||
thus ?thesis using star_unfold_left_Nil by blast
|
||||
qed
|
||||
|
||||
lemma star_decom:
|
||||
assumes a: "x \<in> star A" "x \<noteq> []"
|
||||
shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> star A"
|
||||
using a by (induct rule: star_induct) (blast)+
|
||||
|
||||
|
||||
subsection \<open>Left-Quotients of languages\<close>
|
||||
|
||||
definition Deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
|
||||
where "Deriv x A = { xs. x#xs \<in> A }"
|
||||
|
||||
definition Derivs :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
|
||||
where "Derivs xs A = { ys. xs @ ys \<in> A }"
|
||||
|
||||
abbreviation
|
||||
Derivss :: "'a list \<Rightarrow> 'a lang set \<Rightarrow> 'a lang"
|
||||
where
|
||||
"Derivss s As \<equiv> \<Union> (Derivs s ` As)"
|
||||
|
||||
|
||||
lemma Deriv_empty[simp]: "Deriv a {} = {}"
|
||||
and Deriv_epsilon[simp]: "Deriv a {[]} = {}"
|
||||
and Deriv_char[simp]: "Deriv a {[b]} = (if a = b then {[]} else {})"
|
||||
and Deriv_union[simp]: "Deriv a (A \<union> B) = Deriv a A \<union> Deriv a B"
|
||||
and Deriv_inter[simp]: "Deriv a (A \<inter> B) = Deriv a A \<inter> Deriv a B"
|
||||
and Deriv_compl[simp]: "Deriv a (-A) = - Deriv a A"
|
||||
and Deriv_Union[simp]: "Deriv a (Union M) = Union(Deriv a ` M)"
|
||||
and Deriv_UN[simp]: "Deriv a (UN x:I. S x) = (UN x:I. Deriv a (S x))"
|
||||
by (auto simp: Deriv_def)
|
||||
|
||||
lemma Der_conc [simp]:
|
||||
shows "Deriv c (A @@ B) = (Deriv c A) @@ B \<union> (if [] \<in> A then Deriv c B else {})"
|
||||
unfolding Deriv_def conc_def
|
||||
by (auto simp add: Cons_eq_append_conv)
|
||||
|
||||
lemma Deriv_star [simp]:
|
||||
shows "Deriv c (star A) = (Deriv c A) @@ star A"
|
||||
proof -
|
||||
have "Deriv c (star A) = Deriv c ({[]} \<union> A @@ star A)"
|
||||
by (metis star_unfold_left sup.commute)
|
||||
also have "... = Deriv c (A @@ star A)"
|
||||
unfolding Deriv_union by (simp)
|
||||
also have "... = (Deriv c A) @@ (star A) \<union> (if [] \<in> A then Deriv c (star A) else {})"
|
||||
by simp
|
||||
also have "... = (Deriv c A) @@ star A"
|
||||
unfolding conc_def Deriv_def
|
||||
using star_decom by (force simp add: Cons_eq_append_conv)
|
||||
finally show "Deriv c (star A) = (Deriv c A) @@ star A" .
|
||||
qed
|
||||
|
||||
lemma Deriv_diff[simp]:
|
||||
shows "Deriv c (A - B) = Deriv c A - Deriv c B"
|
||||
by(auto simp add: Deriv_def)
|
||||
|
||||
lemma Deriv_lists[simp]: "c : S \<Longrightarrow> Deriv c (lists S) = lists S"
|
||||
by(auto simp add: Deriv_def)
|
||||
|
||||
lemma Derivs_simps [simp]:
|
||||
shows "Derivs [] A = A"
|
||||
and "Derivs (c # s) A = Derivs s (Deriv c A)"
|
||||
and "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)"
|
||||
unfolding Derivs_def Deriv_def by auto
|
||||
|
||||
lemma in_fold_Deriv: "v \<in> fold Deriv w L \<longleftrightarrow> w @ v \<in> L"
|
||||
by (induct w arbitrary: L) (simp_all add: Deriv_def)
|
||||
|
||||
lemma Derivs_alt_def [code]: "Derivs w L = fold Deriv w L"
|
||||
by (induct w arbitrary: L) simp_all
|
||||
|
||||
lemma Deriv_code [code]:
|
||||
"Deriv x A = tl ` Set.filter (\<lambda>xs. case xs of x' # _ \<Rightarrow> x = x' | _ \<Rightarrow> False) A"
|
||||
by (auto simp: Deriv_def Set.filter_def image_iff tl_def split: list.splits)
|
||||
|
||||
subsection \<open>Shuffle product\<close>
|
||||
|
||||
definition Shuffle (infixr "\<parallel>" 80) where
|
||||
"Shuffle A B = \<Union>{shuffle xs ys | xs ys. xs \<in> A \<and> ys \<in> B}"
|
||||
|
||||
lemma Deriv_Shuffle[simp]:
|
||||
"Deriv a (A \<parallel> B) = Deriv a A \<parallel> B \<union> A \<parallel> Deriv a B"
|
||||
unfolding Shuffle_def Deriv_def by (fastforce simp: Cons_in_shuffle_iff neq_Nil_conv)
|
||||
|
||||
lemma shuffle_subset_lists:
|
||||
assumes "A \<subseteq> lists S" "B \<subseteq> lists S"
|
||||
shows "A \<parallel> B \<subseteq> lists S"
|
||||
unfolding Shuffle_def proof safe
|
||||
fix x and zs xs ys :: "'a list"
|
||||
assume zs: "zs \<in> shuffle xs ys" "x \<in> set zs" and "xs \<in> A" "ys \<in> B"
|
||||
with assms have "xs \<in> lists S" "ys \<in> lists S" by auto
|
||||
with zs show "x \<in> S" by (induct xs ys arbitrary: zs rule: shuffle.induct) auto
|
||||
qed
|
||||
|
||||
lemma Nil_in_Shuffle[simp]: "[] \<in> A \<parallel> B \<longleftrightarrow> [] \<in> A \<and> [] \<in> B"
|
||||
unfolding Shuffle_def by force
|
||||
|
||||
lemma shuffle_Un_distrib:
|
||||
shows "A \<parallel> (B \<union> C) = A \<parallel> B \<union> A \<parallel> C"
|
||||
and "A \<parallel> (B \<union> C) = A \<parallel> B \<union> A \<parallel> C"
|
||||
unfolding Shuffle_def by fast+
|
||||
|
||||
lemma shuffle_UNION_distrib:
|
||||
shows "A \<parallel> UNION I M = UNION I (%i. A \<parallel> M i)"
|
||||
and "UNION I M \<parallel> A = UNION I (%i. M i \<parallel> A)"
|
||||
unfolding Shuffle_def by fast+
|
||||
|
||||
lemma Shuffle_empty[simp]:
|
||||
"A \<parallel> {} = {}"
|
||||
"{} \<parallel> B = {}"
|
||||
unfolding Shuffle_def by auto
|
||||
|
||||
lemma Shuffle_eps[simp]:
|
||||
"A \<parallel> {[]} = A"
|
||||
"{[]} \<parallel> B = B"
|
||||
unfolding Shuffle_def by auto
|
||||
|
||||
|
||||
subsection \<open>Arden's Lemma\<close>
|
||||
|
||||
lemma arden_helper:
|
||||
assumes eq: "X = A @@ X \<union> B"
|
||||
shows "X = (A ^^ Suc n) @@ X \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)"
|
||||
proof (induct n)
|
||||
case 0
|
||||
show "X = (A ^^ Suc 0) @@ X \<union> (\<Union>m\<le>0. (A ^^ m) @@ B)"
|
||||
using eq by simp
|
||||
next
|
||||
case (Suc n)
|
||||
have ih: "X = (A ^^ Suc n) @@ X \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" by fact
|
||||
also have "\<dots> = (A ^^ Suc n) @@ (A @@ X \<union> B) \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" using eq by simp
|
||||
also have "\<dots> = (A ^^ Suc (Suc n)) @@ X \<union> ((A ^^ Suc n) @@ B) \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)"
|
||||
by (simp add: conc_Un_distrib conc_assoc[symmetric] conc_pow_comm)
|
||||
also have "\<dots> = (A ^^ Suc (Suc n)) @@ X \<union> (\<Union>m\<le>Suc n. (A ^^ m) @@ B)"
|
||||
by (auto simp add: atMost_Suc)
|
||||
finally show "X = (A ^^ Suc (Suc n)) @@ X \<union> (\<Union>m\<le>Suc n. (A ^^ m) @@ B)" .
|
||||
qed
|
||||
|
||||
lemma Arden:
|
||||
assumes "[] \<notin> A"
|
||||
shows "X = A @@ X \<union> B \<longleftrightarrow> X = star A @@ B"
|
||||
proof
|
||||
assume eq: "X = A @@ X \<union> B"
|
||||
{ fix w assume "w : X"
|
||||
let ?n = "size w"
|
||||
from \<open>[] \<notin> A\<close> have "\<forall>u \<in> A. length u \<ge> 1"
|
||||
by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)
|
||||
hence "\<forall>u \<in> A^^(?n+1). length u \<ge> ?n+1"
|
||||
by (metis length_lang_pow_lb nat_mult_1)
|
||||
hence "\<forall>u \<in> A^^(?n+1)@@X. length u \<ge> ?n+1"
|
||||
by(auto simp only: conc_def length_append)
|
||||
hence "w \<notin> A^^(?n+1)@@X" by auto
|
||||
hence "w : star A @@ B" using \<open>w : X\<close> using arden_helper[OF eq, where n="?n"]
|
||||
by (auto simp add: star_def conc_UNION_distrib)
|
||||
} moreover
|
||||
{ fix w assume "w : star A @@ B"
|
||||
hence "\<exists>n. w \<in> A^^n @@ B" by(auto simp: conc_def star_def)
|
||||
hence "w : X" using arden_helper[OF eq] by blast
|
||||
} ultimately show "X = star A @@ B" by blast
|
||||
next
|
||||
assume eq: "X = star A @@ B"
|
||||
have "star A = A @@ star A \<union> {[]}"
|
||||
by (rule star_unfold_left)
|
||||
then have "star A @@ B = (A @@ star A \<union> {[]}) @@ B"
|
||||
by metis
|
||||
also have "\<dots> = (A @@ star A) @@ B \<union> B"
|
||||
unfolding conc_Un_distrib by simp
|
||||
also have "\<dots> = A @@ (star A @@ B) \<union> B"
|
||||
by (simp only: conc_assoc)
|
||||
finally show "X = A @@ X \<union> B"
|
||||
using eq by blast
|
||||
qed
|
||||
|
||||
|
||||
lemma reversed_arden_helper:
|
||||
assumes eq: "X = X @@ A \<union> B"
|
||||
shows "X = X @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))"
|
||||
proof (induct n)
|
||||
case 0
|
||||
show "X = X @@ (A ^^ Suc 0) \<union> (\<Union>m\<le>0. B @@ (A ^^ m))"
|
||||
using eq by simp
|
||||
next
|
||||
case (Suc n)
|
||||
have ih: "X = X @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" by fact
|
||||
also have "\<dots> = (X @@ A \<union> B) @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" using eq by simp
|
||||
also have "\<dots> = X @@ (A ^^ Suc (Suc n)) \<union> (B @@ (A ^^ Suc n)) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))"
|
||||
by (simp add: conc_Un_distrib conc_assoc)
|
||||
also have "\<dots> = X @@ (A ^^ Suc (Suc n)) \<union> (\<Union>m\<le>Suc n. B @@ (A ^^ m))"
|
||||
by (auto simp add: atMost_Suc)
|
||||
finally show "X = X @@ (A ^^ Suc (Suc n)) \<union> (\<Union>m\<le>Suc n. B @@ (A ^^ m))" .
|
||||
qed
|
||||
|
||||
theorem reversed_Arden:
|
||||
assumes nemp: "[] \<notin> A"
|
||||
shows "X = X @@ A \<union> B \<longleftrightarrow> X = B @@ star A"
|
||||
proof
|
||||
assume eq: "X = X @@ A \<union> B"
|
||||
{ fix w assume "w : X"
|
||||
let ?n = "size w"
|
||||
from \<open>[] \<notin> A\<close> have "\<forall>u \<in> A. length u \<ge> 1"
|
||||
by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq)
|
||||
hence "\<forall>u \<in> A^^(?n+1). length u \<ge> ?n+1"
|
||||
by (metis length_lang_pow_lb nat_mult_1)
|
||||
hence "\<forall>u \<in> X @@ A^^(?n+1). length u \<ge> ?n+1"
|
||||
by(auto simp only: conc_def length_append)
|
||||
hence "w \<notin> X @@ A^^(?n+1)" by auto
|
||||
hence "w : B @@ star A" using \<open>w : X\<close> using reversed_arden_helper[OF eq, where n="?n"]
|
||||
by (auto simp add: star_def conc_UNION_distrib)
|
||||
} moreover
|
||||
{ fix w assume "w : B @@ star A"
|
||||
hence "\<exists>n. w \<in> B @@ A^^n" by (auto simp: conc_def star_def)
|
||||
hence "w : X" using reversed_arden_helper[OF eq] by blast
|
||||
} ultimately show "X = B @@ star A" by blast
|
||||
next
|
||||
assume eq: "X = B @@ star A"
|
||||
have "star A = {[]} \<union> star A @@ A"
|
||||
unfolding conc_star_comm[symmetric]
|
||||
by(metis Un_commute star_unfold_left)
|
||||
then have "B @@ star A = B @@ ({[]} \<union> star A @@ A)"
|
||||
by metis
|
||||
also have "\<dots> = B \<union> B @@ (star A @@ A)"
|
||||
unfolding conc_Un_distrib by simp
|
||||
also have "\<dots> = B \<union> (B @@ star A) @@ A"
|
||||
by (simp only: conc_assoc)
|
||||
finally show "X = X @@ A \<union> B"
|
||||
using eq by blast
|
||||
qed
|
||||
|
||||
end
|
||||
|
|
@ -1,53 +0,0 @@
|
|||
section \<open>Regular Expressions as Homogeneous Binary Relations\<close>
|
||||
|
||||
theory Relation_Interpretation
|
||||
imports Regular_Exp
|
||||
begin
|
||||
|
||||
primrec rel :: "('a \<Rightarrow> ('b * 'b) set) \<Rightarrow> 'a rexp \<Rightarrow> ('b * 'b) set"
|
||||
where
|
||||
"rel v Zero = {}" |
|
||||
"rel v One = Id" |
|
||||
"rel v (Atom a) = v a" |
|
||||
"rel v (Plus r s) = rel v r \<union> rel v s" |
|
||||
"rel v (Times r s) = rel v r O rel v s" |
|
||||
"rel v (Star r) = (rel v r)^*"
|
||||
|
||||
primrec word_rel :: "('a \<Rightarrow> ('b * 'b) set) \<Rightarrow> 'a list \<Rightarrow> ('b * 'b) set"
|
||||
where
|
||||
"word_rel v [] = Id"
|
||||
| "word_rel v (a#as) = v a O word_rel v as"
|
||||
|
||||
lemma word_rel_append:
|
||||
"word_rel v w O word_rel v w' = word_rel v (w @ w')"
|
||||
by (rule sym) (induct w, auto)
|
||||
|
||||
lemma rel_word_rel: "rel v r = (\<Union>w\<in>lang r. word_rel v w)"
|
||||
proof (induct r)
|
||||
case Times thus ?case
|
||||
by (auto simp: rel_def word_rel_append conc_def relcomp_UNION_distrib relcomp_UNION_distrib2)
|
||||
next
|
||||
case (Star r)
|
||||
{ fix n
|
||||
have "(rel v r) ^^ n = (\<Union>w \<in> lang r ^^ n. word_rel v w)"
|
||||
proof (induct n)
|
||||
case 0 show ?case by simp
|
||||
next
|
||||
case (Suc n) thus ?case
|
||||
unfolding relpow.simps relpow_commute[symmetric]
|
||||
by (auto simp add: Star conc_def word_rel_append
|
||||
relcomp_UNION_distrib relcomp_UNION_distrib2)
|
||||
qed }
|
||||
|
||||
thus ?case unfolding rel.simps
|
||||
by (force simp: rtrancl_power star_def)
|
||||
qed auto
|
||||
|
||||
|
||||
text \<open>Soundness:\<close>
|
||||
|
||||
lemma soundness:
|
||||
"lang r = lang s \<Longrightarrow> rel v r = rel v s"
|
||||
unfolding rel_word_rel by auto
|
||||
|
||||
end
|
||||
|
|
@ -1,36 +0,0 @@
|
|||
@article{KraussN-JAR,author={Alexander Krauss and Tobias Nipkow},
|
||||
title={Proof Pearl: Regular Expression Equivalence and Relation Algebra},
|
||||
journal={J. Automated Reasoning},volume=49,pages={95--106},year=2012,note={published online March 2011}}
|
||||
|
||||
@inproceedings{Rutten98,
|
||||
author = {Jan J. M. M. Rutten},
|
||||
title = {Automata and Coinduction (An Exercise in Coalgebra)},
|
||||
editor = {Davide Sangiorgi and Robert de Simone},
|
||||
booktitle = {Concurrency Theory (CONCUR'98)},
|
||||
pages = {194--218},
|
||||
publisher = {Springer},
|
||||
series = {Lecture Notes in Computer Science},
|
||||
volume = {1466},
|
||||
year = {1998},
|
||||
}
|
||||
|
||||
@article{Brzozowski64,
|
||||
author = {J.~A.~Brzozowski},
|
||||
title = {{D}erivatives of {R}egular {E}xpressions},
|
||||
journal = {Journal of the ACM},
|
||||
volume = {11},
|
||||
issue = {4},
|
||||
year = {1964},
|
||||
pages = {481--494},
|
||||
publisher = {ACM}
|
||||
}
|
||||
|
||||
@ARTICLE{Antimirov95,
|
||||
author = {V.~Antimirov},
|
||||
title = {{P}artial {D}erivatives of {R}egular {E}xpressions and
|
||||
{F}inite {A}utomata {C}onstructions},
|
||||
journal = {Theoretical Computer Science},
|
||||
year = {1995},
|
||||
volume = {155},
|
||||
pages = {291--319}
|
||||
}
|
||||
|
|
@ -1,47 +0,0 @@
|
|||
\documentclass[11pt,a4paper]{article}
|
||||
\usepackage{isabelle,isabellesym}
|
||||
\usepackage{eufrak}
|
||||
|
||||
% this should be the last package used
|
||||
\usepackage{pdfsetup}
|
||||
|
||||
% urls in roman style, theory text in math-similar italics
|
||||
\urlstyle{rm}
|
||||
\isabellestyle{it}
|
||||
|
||||
|
||||
\begin{document}
|
||||
|
||||
\title{Regular Sets, Expressions, Derivatives and Relation Algebra}
|
||||
\author{Alexander Krauss, Tobias Nipkow,\\
|
||||
Chunhan Wu, Xingyuan Zhang and Christian Urban}
|
||||
\maketitle
|
||||
|
||||
\begin{abstract}
|
||||
This is a library of constructions on regular expressions and languages. It
|
||||
provides the operations of concatenation, Kleene star and left-quotients of
|
||||
languages. A theory of derivatives and partial derivatives is
|
||||
provided. Arden's lemma and finiteness of partial derivatives is
|
||||
established. A simple regular expression matcher based on Brozowski's
|
||||
derivatives is proved to be correct. An executable equivalence checker for
|
||||
regular expressions is verified; it does not need automata but works directly
|
||||
on regular expressions. By mapping regular expressions to binary relations, an
|
||||
automatic and complete proof method for (in)equalities of binary relations
|
||||
over union, concatenation and (reflexive) transitive closure is obtained.
|
||||
|
||||
For an exposition of the equivalence checker for regular and relation
|
||||
algebraic expressions see the paper by Krauss and Nipkow~\cite{KraussN-JAR}.
|
||||
|
||||
Extended regular expressions with complement and intersection
|
||||
are also defined and an equivalence checker is provided.
|
||||
\end{abstract}
|
||||
|
||||
\tableofcontents
|
||||
|
||||
% include generated text of all theories
|
||||
\input{session}
|
||||
|
||||
\bibliographystyle{abbrv}
|
||||
\bibliography{root}
|
||||
|
||||
\end{document}
|
||||
|
|
@ -1,306 +0,0 @@
|
|||
section \<open>Deciding Regular Expression Equivalence (2)\<close>
|
||||
|
||||
theory pEquivalence_Checking
|
||||
imports Equivalence_Checking Derivatives
|
||||
begin
|
||||
|
||||
text\<open>\noindent Similar to theory @{theory "Regular-Sets.Equivalence_Checking"}, but
|
||||
with partial derivatives instead of derivatives.\<close>
|
||||
|
||||
text\<open>Lifting many notions to sets:\<close>
|
||||
|
||||
definition "Lang R == UN r:R. lang r"
|
||||
definition "Nullable R == EX r:R. nullable r"
|
||||
definition "Pderiv a R == UN r:R. pderiv a r"
|
||||
definition "Atoms R == UN r:R. atoms r"
|
||||
|
||||
(* FIXME: rename pderiv_set in Derivatives to Pderiv and drop the one above *)
|
||||
|
||||
lemma Atoms_pderiv: "Atoms(pderiv a r) \<subseteq> atoms r"
|
||||
apply (induct r)
|
||||
apply (auto simp: Atoms_def UN_subset_iff)
|
||||
apply (fastforce)+
|
||||
done
|
||||
|
||||
lemma Atoms_Pderiv: "Atoms(Pderiv a R) \<subseteq> Atoms R"
|
||||
using Atoms_pderiv by (fastforce simp: Atoms_def Pderiv_def)
|
||||
|
||||
lemma pderiv_no_occurrence:
|
||||
"x \<notin> atoms r \<Longrightarrow> pderiv x r = {}"
|
||||
by (induct r) auto
|
||||
|
||||
lemma Pderiv_no_occurrence:
|
||||
"x \<notin> Atoms R \<Longrightarrow> Pderiv x R = {}"
|
||||
by(auto simp:pderiv_no_occurrence Atoms_def Pderiv_def)
|
||||
|
||||
lemma Deriv_Lang: "Deriv c (Lang R) = Lang (Pderiv c R)"
|
||||
by(auto simp: Deriv_pderiv Pderiv_def Lang_def)
|
||||
|
||||
lemma Nullable_pderiv[simp]: "Nullable(pderivs w r) = (w : lang r)"
|
||||
apply(induction w arbitrary: r)
|
||||
apply (simp add: Nullable_def nullable_iff singleton_iff)
|
||||
using eqset_imp_iff[OF Deriv_pderiv[where 'a = 'a]]
|
||||
apply (simp add: Nullable_def Deriv_def)
|
||||
done
|
||||
|
||||
|
||||
type_synonym 'a Rexp_pair = "'a rexp set * 'a rexp set"
|
||||
type_synonym 'a Rexp_pairs = "'a Rexp_pair list"
|
||||
|
||||
definition is_Bisimulation :: "'a list \<Rightarrow> 'a Rexp_pairs \<Rightarrow> bool"
|
||||
where
|
||||
"is_Bisimulation as ps =
|
||||
(\<forall>(R,S)\<in> set ps. Atoms R \<union> Atoms S \<subseteq> set as \<and>
|
||||
(Nullable R \<longleftrightarrow> Nullable S) \<and>
|
||||
(\<forall>a\<in>set as. (Pderiv a R, Pderiv a S) \<in> set ps))"
|
||||
|
||||
lemma Bisim_Lang_eq:
|
||||
assumes Bisim: "is_Bisimulation as ps"
|
||||
assumes "(R, S) \<in> set ps"
|
||||
shows "Lang R = Lang S"
|
||||
proof -
|
||||
define ps' where "ps' = ({}, {}) # ps"
|
||||
from Bisim have Bisim': "is_Bisimulation as ps'"
|
||||
by (fastforce simp: ps'_def is_Bisimulation_def UN_subset_iff Pderiv_def Atoms_def)
|
||||
let ?R = "\<lambda>K L. (\<exists>(R,S)\<in>set ps'. K = Lang R \<and> L = Lang S)"
|
||||
show ?thesis
|
||||
proof (rule language_coinduct[where R="?R"])
|
||||
from \<open>(R,S) \<in> set ps\<close>
|
||||
have "(R,S) \<in> set ps'" by (auto simp: ps'_def)
|
||||
thus "?R (Lang R) (Lang S)" by auto
|
||||
next
|
||||
fix K L assume "?R K L"
|
||||
then obtain R S where rs: "(R, S) \<in> set ps'"
|
||||
and KL: "K = Lang R" "L = Lang S" by auto
|
||||
with Bisim' have "Nullable R \<longleftrightarrow> Nullable S"
|
||||
by (auto simp: is_Bisimulation_def)
|
||||
thus "[] \<in> K \<longleftrightarrow> [] \<in> L"
|
||||
by (auto simp: nullable_iff KL Nullable_def Lang_def)
|
||||
fix a
|
||||
show "?R (Deriv a K) (Deriv a L)"
|
||||
proof cases
|
||||
assume "a \<in> set as"
|
||||
with rs Bisim'
|
||||
have "(Pderiv a R, Pderiv a S) \<in> set ps'"
|
||||
by (auto simp: is_Bisimulation_def)
|
||||
thus ?thesis by (fastforce simp: KL Deriv_Lang)
|
||||
next
|
||||
assume "a \<notin> set as"
|
||||
with Bisim' rs
|
||||
have "a \<notin> Atoms R \<union> Atoms S"
|
||||
by (fastforce simp: is_Bisimulation_def UN_subset_iff)
|
||||
then have "Pderiv a R = {}" "Pderiv a S = {}"
|
||||
by (metis Pderiv_no_occurrence Un_iff)+
|
||||
then have "Deriv a K = Lang {}" "Deriv a L = Lang {}"
|
||||
unfolding KL Deriv_Lang by auto
|
||||
thus ?thesis by (auto simp: ps'_def)
|
||||
qed
|
||||
qed
|
||||
qed
|
||||
|
||||
|
||||
subsection \<open>Closure computation\<close>
|
||||
|
||||
fun test :: "'a Rexp_pairs * 'a Rexp_pairs \<Rightarrow> bool" where
|
||||
"test (ws, ps) = (case ws of [] \<Rightarrow> False | (R,S)#_ \<Rightarrow> Nullable R = Nullable S)"
|
||||
|
||||
fun step :: "'a list \<Rightarrow>
|
||||
'a Rexp_pairs * 'a Rexp_pairs \<Rightarrow> 'a Rexp_pairs * 'a Rexp_pairs"
|
||||
where "step as (ws,ps) =
|
||||
(let
|
||||
(R,S) = hd ws;
|
||||
ps' = (R,S) # ps;
|
||||
succs = map (\<lambda>a. (Pderiv a R, Pderiv a S)) as;
|
||||
new = filter (\<lambda>p. p \<notin> set ps \<union> set ws) succs
|
||||
in (remdups new @ tl ws, ps'))"
|
||||
|
||||
definition closure ::
|
||||
"'a list \<Rightarrow> 'a Rexp_pairs * 'a Rexp_pairs
|
||||
\<Rightarrow> ('a Rexp_pairs * 'a Rexp_pairs) option" where
|
||||
"closure as = while_option test (step as)"
|
||||
|
||||
definition pre_Bisim :: "'a list \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set \<Rightarrow>
|
||||
'a Rexp_pairs * 'a Rexp_pairs \<Rightarrow> bool"
|
||||
where
|
||||
"pre_Bisim as R S = (\<lambda>(ws,ps).
|
||||
((R,S) \<in> set ws \<union> set ps) \<and>
|
||||
(\<forall>(R,S)\<in> set ws \<union> set ps. Atoms R \<union> Atoms S \<subseteq> set as) \<and>
|
||||
(\<forall>(R,S)\<in> set ps. (Nullable R \<longleftrightarrow> Nullable S) \<and>
|
||||
(\<forall>a\<in>set as. (Pderiv a R, Pderiv a S) \<in> set ps \<union> set ws)))"
|
||||
|
||||
lemma step_set_eq: "\<lbrakk> test (ws,ps); step as (ws,ps) = (ws',ps') \<rbrakk>
|
||||
\<Longrightarrow> set ws' \<union> set ps' =
|
||||
set ws \<union> set ps
|
||||
\<union> (\<Union>a\<in>set as. {(Pderiv a (fst(hd ws)), Pderiv a (snd(hd ws)))})"
|
||||
by(auto split: list.splits)
|
||||
|
||||
theorem closure_sound:
|
||||
assumes result: "closure as ([(R,S)],[]) = Some([],ps)"
|
||||
and atoms: "Atoms R \<union> Atoms S \<subseteq> set as"
|
||||
shows "Lang R = Lang S"
|
||||
proof-
|
||||
{ fix st
|
||||
have "pre_Bisim as R S st \<Longrightarrow> test st \<Longrightarrow> pre_Bisim as R S (step as st)"
|
||||
unfolding pre_Bisim_def
|
||||
proof(split prod.splits, elim case_prodE conjE, intro allI impI conjI, goal_cases)
|
||||
case 1 thus ?case by(auto split: list.splits)
|
||||
next
|
||||
case prems: (2 ws ps ws' ps')
|
||||
note prems(2)[simp]
|
||||
from \<open>test st\<close> obtain wstl R S where [simp]: "ws = (R,S)#wstl"
|
||||
by (auto split: list.splits)
|
||||
from \<open>step as st = (ws',ps')\<close> obtain P where [simp]: "ps' = (R,S) # ps"
|
||||
and [simp]: "ws' = remdups(filter P (map (\<lambda>a. (Pderiv a R, Pderiv a S)) as)) @ wstl"
|
||||
by auto
|
||||
have "\<forall>(R',S')\<in>set wstl \<union> set ps'. Atoms R' \<union> Atoms S' \<subseteq> set as"
|
||||
using prems(4) by auto
|
||||
moreover
|
||||
have "\<forall>a\<in>set as. Atoms(Pderiv a R) \<union> Atoms(Pderiv a S) \<subseteq> set as"
|
||||
using prems(4) by simp (metis (lifting) Atoms_Pderiv order_trans)
|
||||
ultimately show ?case by simp blast
|
||||
next
|
||||
case 3 thus ?case
|
||||
apply (clarsimp simp: image_iff split: prod.splits list.splits)
|
||||
by hypsubst_thin metis
|
||||
qed
|
||||
}
|
||||
moreover
|
||||
from atoms
|
||||
have "pre_Bisim as R S ([(R,S)],[])" by (simp add: pre_Bisim_def)
|
||||
ultimately have pre_Bisim_ps: "pre_Bisim as R S ([],ps)"
|
||||
by (rule while_option_rule[OF _ result[unfolded closure_def]])
|
||||
then have "is_Bisimulation as ps" "(R,S) \<in> set ps"
|
||||
by (auto simp: pre_Bisim_def is_Bisimulation_def)
|
||||
thus "Lang R = Lang S" by (rule Bisim_Lang_eq)
|
||||
qed
|
||||
|
||||
|
||||
subsection \<open>The overall procedure\<close>
|
||||
|
||||
definition check_eqv :: "'a rexp \<Rightarrow> 'a rexp \<Rightarrow> bool"
|
||||
where
|
||||
"check_eqv r s =
|
||||
(case closure (add_atoms r (add_atoms s [])) ([({r}, {s})], []) of
|
||||
Some([],_) \<Rightarrow> True | _ \<Rightarrow> False)"
|
||||
|
||||
lemma soundness: assumes "check_eqv r s" shows "lang r = lang s"
|
||||
proof -
|
||||
let ?as = "add_atoms r (add_atoms s [])"
|
||||
obtain ps where 1: "closure ?as ([({r},{s})],[]) = Some([],ps)"
|
||||
using assms by (auto simp: check_eqv_def split:option.splits list.splits)
|
||||
then have "lang r = lang s"
|
||||
by(rule closure_sound[of _ "{r}" "{s}", simplified Lang_def, simplified])
|
||||
(auto simp: set_add_atoms Atoms_def)
|
||||
thus "lang r = lang s" by simp
|
||||
qed
|
||||
|
||||
text\<open>Test:\<close>
|
||||
lemma "check_eqv
|
||||
(Plus One (Times (Atom 0) (Star(Atom 0))))
|
||||
(Star(Atom(0::nat)))"
|
||||
by eval
|
||||
|
||||
|
||||
subsection "Termination and Completeness"
|
||||
|
||||
definition PDERIVS :: "'a rexp set => 'a rexp set" where
|
||||
"PDERIVS R = (UN r:R. pderivs_lang UNIV r)"
|
||||
|
||||
lemma PDERIVS_incr[simp]: "R \<subseteq> PDERIVS R"
|
||||
apply(auto simp add: PDERIVS_def pderivs_lang_def)
|
||||
by (metis pderivs.simps(1) insertI1)
|
||||
|
||||
lemma Pderiv_PDERIVS: assumes "R' \<subseteq> PDERIVS R" shows "Pderiv a R' \<subseteq> PDERIVS R"
|
||||
proof
|
||||
fix r assume "r : Pderiv a R'"
|
||||
then obtain r' where "r' : R'" "r : pderiv a r'" by(auto simp: Pderiv_def)
|
||||
from \<open>r' : R'\<close> \<open>R' \<subseteq> PDERIVS R\<close> obtain s w where "s : R" "r' : pderivs w s"
|
||||
by(auto simp: PDERIVS_def pderivs_lang_def)
|
||||
hence "r \<in> pderivs (w @ [a]) s" using \<open>r : pderiv a r'\<close> by(auto simp add:pderivs_snoc)
|
||||
thus "r : PDERIVS R" using \<open>s : R\<close> by(auto simp: PDERIVS_def pderivs_lang_def)
|
||||
qed
|
||||
|
||||
lemma finite_PDERIVS: "finite R \<Longrightarrow> finite(PDERIVS R)"
|
||||
by(simp add: PDERIVS_def finite_pderivs_lang_UNIV)
|
||||
|
||||
lemma closure_Some: assumes "finite R0" "finite S0" shows "\<exists>p. closure as ([(R0,S0)],[]) = Some p"
|
||||
proof(unfold closure_def)
|
||||
let ?Inv = "%(ws,bs). distinct ws \<and> (ALL (R,S) : set ws. R \<subseteq> PDERIVS R0 \<and> S \<subseteq> PDERIVS S0 \<and> (R,S) \<notin> set bs)"
|
||||
let ?m1 = "%bs. Pow(PDERIVS R0) \<times> Pow(PDERIVS S0) - set bs"
|
||||
let ?m2 = "%(ws,bs). card(?m1 bs)"
|
||||
have Inv0: "?Inv ([(R0, S0)], [])" by simp
|
||||
{ fix s assume "test s" "?Inv s"
|
||||
obtain ws bs where [simp]: "s = (ws,bs)" by fastforce
|
||||
from \<open>test s\<close> obtain R S ws' where [simp]: "ws = (R,S)#ws'"
|
||||
by(auto split: prod.splits list.splits)
|
||||
let ?bs' = "(R,S) # bs"
|
||||
let ?succs = "map (\<lambda>a. (Pderiv a R, Pderiv a S)) as"
|
||||
let ?new = "filter (\<lambda>p. p \<notin> set bs \<union> set ws) ?succs"
|
||||
let ?ws' = "remdups ?new @ ws'"
|
||||
have *: "?Inv (step as s)"
|
||||
proof -
|
||||
from \<open>?Inv s\<close> have "distinct ?ws'" by auto
|
||||
have "ALL (R,S) : set ?ws'. R \<subseteq> PDERIVS R0 \<and> S \<subseteq> PDERIVS S0 \<and> (R,S) \<notin> set ?bs'" using \<open>?Inv s\<close>
|
||||
by(simp add: Ball_def image_iff) (metis Pderiv_PDERIVS)
|
||||
with \<open>distinct ?ws'\<close> show ?thesis by(simp)
|
||||
qed
|
||||
have "?m2(step as s) < ?m2 s"
|
||||
proof -
|
||||
have "finite(?m1 bs)"
|
||||
by(metis assms finite_Diff finite_PDERIVS finite_cartesian_product finite_Pow_iff)
|
||||
moreover have "?m2(step as s) < ?m2 s" using \<open>?Inv s\<close>
|
||||
by(auto intro: psubset_card_mono[OF \<open>finite(?m1 bs)\<close>])
|
||||
then show ?thesis using \<open>?Inv s\<close> by simp
|
||||
qed
|
||||
note * and this
|
||||
} note step = this
|
||||
show "\<exists>p. while_option test (step as) ([(R0, S0)], []) = Some p"
|
||||
by(rule measure_while_option_Some [where P = ?Inv and f = ?m2, OF _ Inv0])(simp add: step)
|
||||
qed
|
||||
|
||||
theorem closure_Some_Inv: assumes "closure as ([({r},{s})],[]) = Some p"
|
||||
shows "\<forall>(R,S)\<in>set(fst p). \<exists>w. R = pderivs w r \<and> S = pderivs w s" (is "?Inv p")
|
||||
proof-
|
||||
from assms have 1: "while_option test (step as) ([({r},{s})],[]) = Some p"
|
||||
by(simp add: closure_def)
|
||||
have Inv0: "?Inv ([({r},{s})],[])" by simp (metis pderivs.simps(1))
|
||||
{ fix p assume "?Inv p" "test p"
|
||||
obtain ws bs where [simp]: "p = (ws,bs)" by fastforce
|
||||
from \<open>test p\<close> obtain R S ws' where [simp]: "ws = (R,S)#ws'"
|
||||
by(auto split: prod.splits list.splits)
|
||||
let ?succs = "map (\<lambda>a. (Pderiv a R, Pderiv a S)) as"
|
||||
let ?new = "filter (\<lambda>p. p \<notin> set bs \<union> set ws) ?succs"
|
||||
let ?ws' = "remdups ?new @ ws'"
|
||||
from \<open>?Inv p\<close> obtain w where [simp]: "R = pderivs w r" "S = pderivs w s"
|
||||
by auto
|
||||
{ fix x assume "x : set as"
|
||||
have "EX w. Pderiv x R = pderivs w r \<and> Pderiv x S = pderivs w s"
|
||||
by(rule_tac x="w@[x]" in exI)(simp add: pderivs_append Pderiv_def)
|
||||
}
|
||||
with \<open>?Inv p\<close> have "?Inv (step as p)" by auto
|
||||
} note Inv_step = this
|
||||
show ?thesis
|
||||
apply(rule while_option_rule[OF _ 1])
|
||||
apply(erule (1) Inv_step)
|
||||
apply(rule Inv0)
|
||||
done
|
||||
qed
|
||||
|
||||
lemma closure_complete: assumes "lang r = lang s"
|
||||
shows "EX bs. closure as ([({r},{s})],[]) = Some([],bs)" (is ?C)
|
||||
proof(rule ccontr)
|
||||
assume "\<not> ?C"
|
||||
then obtain R S ws bs
|
||||
where cl: "closure as ([({r},{s})],[]) = Some((R,S)#ws,bs)"
|
||||
using closure_Some[of "{r}" "{s}", simplified]
|
||||
by (metis (hide_lams, no_types) list.exhaust prod.exhaust)
|
||||
from assms closure_Some_Inv[OF this]
|
||||
while_option_stop[OF cl[unfolded closure_def]]
|
||||
show "False" by auto
|
||||
qed
|
||||
|
||||
corollary completeness: "lang r = lang s \<Longrightarrow> check_eqv r s"
|
||||
by(auto simp add: check_eqv_def dest!: closure_complete
|
||||
split: option.split list.split)
|
||||
|
||||
end
|
||||
Loading…
Reference in New Issue