theory Regular+ −
imports Main Folds+ −
begin+ −
+ −
section {* Preliminary definitions *}+ −
+ −
type_synonym lang = "string set"+ −
+ −
+ −
text {* Sequential composition of two languages *}+ −
+ −
definition + −
Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100)+ −
where + −
"A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"+ −
+ −
+ −
text {* Some properties of operator @{text ";;"}. *}+ −
+ −
lemma seq_add_left:+ −
assumes a: "A = B"+ −
shows "C ;; A = C ;; B"+ −
using a by simp+ −
+ −
lemma seq_union_distrib_right:+ −
shows "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)"+ −
unfolding Seq_def by auto+ −
+ −
lemma seq_union_distrib_left:+ −
shows "C ;; (A \<union> B) = (C ;; A) \<union> (C ;; B)"+ −
unfolding Seq_def by auto+ −
+ −
lemma seq_intro:+ −
assumes a: "x \<in> A" "y \<in> B"+ −
shows "x @ y \<in> A ;; B "+ −
using a by (auto simp: Seq_def)+ −
+ −
lemma seq_assoc:+ −
shows "(A ;; B) ;; C = A ;; (B ;; C)"+ −
unfolding Seq_def+ −
apply(auto)+ −
apply(blast)+ −
by (metis append_assoc)+ −
+ −
lemma seq_empty [simp]:+ −
shows "A ;; {[]} = A"+ −
and "{[]} ;; A = A"+ −
by (simp_all add: Seq_def)+ −
+ −
lemma seq_null [simp]:+ −
shows "A ;; {} = {}"+ −
and "{} ;; A = {}"+ −
by (simp_all add: Seq_def)+ −
+ −
+ −
text {* Power and Star of a language *}+ −
+ −
fun + −
pow :: "lang \<Rightarrow> nat \<Rightarrow> lang" (infixl "\<up>" 100)+ −
where+ −
"A \<up> 0 = {[]}"+ −
| "A \<up> (Suc n) = A ;; (A \<up> n)" + −
+ −
definition+ −
Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102)+ −
where+ −
"A\<star> \<equiv> (\<Union>n. A \<up> n)"+ −
+ −
+ −
lemma star_start[intro]:+ −
shows "[] \<in> A\<star>"+ −
proof -+ −
have "[] \<in> A \<up> 0" by auto+ −
then show "[] \<in> A\<star>" unfolding Star_def by blast+ −
qed+ −
+ −
lemma star_step [intro]:+ −
assumes a: "s1 \<in> A" + −
and b: "s2 \<in> A\<star>"+ −
shows "s1 @ s2 \<in> A\<star>"+ −
proof -+ −
from b obtain n where "s2 \<in> A \<up> n" unfolding Star_def by auto+ −
then have "s1 @ s2 \<in> A \<up> (Suc n)" using a by (auto simp add: Seq_def)+ −
then show "s1 @ s2 \<in> A\<star>" unfolding Star_def by blast+ −
qed+ −
+ −
lemma star_induct[consumes 1, case_names start step]:+ −
assumes a: "x \<in> A\<star>" + −
and b: "P []"+ −
and c: "\<And>s1 s2. \<lbrakk>s1 \<in> A; s2 \<in> A\<star>; P s2\<rbrakk> \<Longrightarrow> P (s1 @ s2)"+ −
shows "P x"+ −
proof -+ −
from a obtain n where "x \<in> A \<up> n" unfolding Star_def by auto+ −
then show "P x"+ −
by (induct n arbitrary: x)+ −
(auto intro!: b c simp add: Seq_def Star_def)+ −
qed+ −
+ −
lemma star_intro1:+ −
assumes a: "x \<in> A\<star>"+ −
and b: "y \<in> A\<star>"+ −
shows "x @ y \<in> A\<star>"+ −
using a b+ −
by (induct rule: star_induct) (auto)+ −
+ −
lemma star_intro2: + −
assumes a: "y \<in> A"+ −
shows "y \<in> A\<star>"+ −
proof -+ −
from a have "y @ [] \<in> A\<star>" by blast+ −
then show "y \<in> A\<star>" by simp+ −
qed+ −
+ −
lemma star_intro3:+ −
assumes a: "x \<in> A\<star>"+ −
and b: "y \<in> A"+ −
shows "x @ y \<in> A\<star>"+ −
using a b by (blast intro: star_intro1 star_intro2)+ −
+ −
lemma star_cases:+ −
shows "A\<star> = {[]} \<union> A ;; A\<star>"+ −
proof+ −
{ fix x+ −
have "x \<in> A\<star> \<Longrightarrow> x \<in> {[]} \<union> A ;; A\<star>"+ −
unfolding Seq_def+ −
by (induct rule: star_induct) (auto)+ −
}+ −
then show "A\<star> \<subseteq> {[]} \<union> A ;; A\<star>" by auto+ −
next+ −
show "{[]} \<union> A ;; A\<star> \<subseteq> A\<star>"+ −
unfolding Seq_def by auto+ −
qed+ −
+ −
lemma star_decom: + −
assumes a: "x \<in> A\<star>" "x \<noteq> []"+ −
shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> A\<star>"+ −
using a+ −
by (induct rule: star_induct) (blast)++ −
+ −
lemma+ −
shows seq_Union_left: "B ;; (\<Union>n. A \<up> n) = (\<Union>n. B ;; (A \<up> n))"+ −
and seq_Union_right: "(\<Union>n. A \<up> n) ;; B = (\<Union>n. (A \<up> n) ;; B)"+ −
unfolding Seq_def by auto+ −
+ −
lemma seq_pow_comm:+ −
shows "A ;; (A \<up> n) = (A \<up> n) ;; A"+ −
by (induct n) (simp_all add: seq_assoc[symmetric])+ −
+ −
lemma seq_star_comm:+ −
shows "A ;; A\<star> = A\<star> ;; A"+ −
unfolding Star_def seq_Union_left+ −
unfolding seq_pow_comm seq_Union_right + −
by simp+ −
+ −
+ −
text {* Two lemmas about the length of strings in @{text "A \<up> n"} *}+ −
+ −
lemma pow_length:+ −
assumes a: "[] \<notin> A"+ −
and b: "s \<in> A \<up> Suc n"+ −
shows "n < length s"+ −
using b+ −
proof (induct n arbitrary: s)+ −
case 0+ −
have "s \<in> A \<up> Suc 0" by fact+ −
with a have "s \<noteq> []" by auto+ −
then show "0 < length s" by auto+ −
next+ −
case (Suc n)+ −
have ih: "\<And>s. s \<in> A \<up> Suc n \<Longrightarrow> n < length s" by fact+ −
have "s \<in> A \<up> Suc (Suc n)" by fact+ −
then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A \<up> Suc n"+ −
by (auto simp add: Seq_def)+ −
from ih ** have "n < length s2" by simp+ −
moreover have "0 < length s1" using * a by auto+ −
ultimately show "Suc n < length s" unfolding eq + −
by (simp only: length_append)+ −
qed+ −
+ −
lemma seq_pow_length:+ −
assumes a: "[] \<notin> A"+ −
and b: "s \<in> B ;; (A \<up> Suc n)"+ −
shows "n < length s"+ −
proof -+ −
from b obtain s1 s2 where eq: "s = s1 @ s2" and *: "s2 \<in> A \<up> Suc n"+ −
unfolding Seq_def by auto+ −
from * have " n < length s2" by (rule pow_length[OF a])+ −
then show "n < length s" using eq by simp+ −
qed+ −
+ −
+ −
section {* A modified version of Arden's lemma *}+ −
+ −
text {* A helper lemma for Arden *}+ −
+ −
lemma arden_helper:+ −
assumes eq: "X = X ;; A \<union> B"+ −
shows "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"+ −
proof (induct n)+ −
case 0 + −
show "X = X ;; (A \<up> Suc 0) \<union> (\<Union>(m::nat)\<in>{0..0}. B ;; (A \<up> m))"+ −
using eq by simp+ −
next+ −
case (Suc n)+ −
have ih: "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" by fact+ −
also have "\<dots> = (X ;; A \<union> B) ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))" using eq by simp+ −
also have "\<dots> = X ;; (A \<up> Suc (Suc n)) \<union> (B ;; (A \<up> Suc n)) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"+ −
by (simp add: seq_union_distrib_right seq_assoc)+ −
also have "\<dots> = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))"+ −
by (auto simp add: le_Suc_eq)+ −
finally show "X = X ;; (A \<up> Suc (Suc n)) \<union> (\<Union>m\<in>{0..Suc n}. B ;; (A \<up> m))" .+ −
qed+ −
+ −
theorem arden:+ −
assumes nemp: "[] \<notin> A"+ −
shows "X = X ;; A \<union> B \<longleftrightarrow> X = B ;; A\<star>"+ −
proof+ −
assume eq: "X = B ;; A\<star>"+ −
have "A\<star> = {[]} \<union> A\<star> ;; A" + −
unfolding seq_star_comm[symmetric]+ −
by (rule star_cases)+ −
then have "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"+ −
by (rule seq_add_left)+ −
also have "\<dots> = B \<union> B ;; (A\<star> ;; A)"+ −
unfolding seq_union_distrib_left by simp+ −
also have "\<dots> = B \<union> (B ;; A\<star>) ;; A" + −
by (simp only: seq_assoc)+ −
finally show "X = X ;; A \<union> B" + −
using eq by blast + −
next+ −
assume eq: "X = X ;; A \<union> B"+ −
{ fix n::nat+ −
have "B ;; (A \<up> n) \<subseteq> X" using arden_helper[OF eq, of "n"] by auto }+ −
then have "B ;; A\<star> \<subseteq> X" + −
unfolding Seq_def Star_def UNION_def by auto+ −
moreover+ −
{ fix s::string+ −
obtain k where "k = length s" by auto+ −
then have not_in: "s \<notin> X ;; (A \<up> Suc k)" + −
using seq_pow_length[OF nemp] by blast+ −
assume "s \<in> X"+ −
then have "s \<in> X ;; (A \<up> Suc k) \<union> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))"+ −
using arden_helper[OF eq, of "k"] by auto+ −
then have "s \<in> (\<Union>m\<in>{0..k}. B ;; (A \<up> m))" using not_in by auto+ −
moreover+ −
have "(\<Union>m\<in>{0..k}. B ;; (A \<up> m)) \<subseteq> (\<Union>n. B ;; (A \<up> n))" by auto+ −
ultimately + −
have "s \<in> B ;; A\<star>" + −
unfolding seq_Union_left Star_def by auto }+ −
then have "X \<subseteq> B ;; A\<star>" by auto+ −
ultimately + −
show "X = B ;; A\<star>" by simp+ −
qed+ −
+ −
+ −
section {* Regular Expressions *}+ −
+ −
datatype rexp =+ −
NULL+ −
| EMPTY+ −
| CHAR char+ −
| SEQ rexp rexp+ −
| ALT rexp rexp+ −
| STAR rexp+ −
+ −
+ −
text {* + −
The function @{text L} is overloaded, with the idea that @{text "L x"} + −
evaluates to the language represented by the object @{text x}.+ −
*}+ −
+ −
consts L:: "'a \<Rightarrow> lang"+ −
+ −
overloading L_rexp \<equiv> "L:: rexp \<Rightarrow> lang"+ −
begin+ −
fun+ −
L_rexp :: "rexp \<Rightarrow> lang"+ −
where+ −
"L_rexp (NULL) = {}"+ −
| "L_rexp (EMPTY) = {[]}"+ −
| "L_rexp (CHAR c) = {[c]}"+ −
| "L_rexp (SEQ r1 r2) = (L_rexp r1) ;; (L_rexp r2)"+ −
| "L_rexp (ALT r1 r2) = (L_rexp r1) \<union> (L_rexp r2)"+ −
| "L_rexp (STAR r) = (L_rexp r)\<star>"+ −
end+ −
+ −
+ −
text {* ALT-combination for a set of regular expressions *}+ −
+ −
abbreviation+ −
Setalt ("\<Uplus>_" [1000] 999) + −
where+ −
"\<Uplus>A \<equiv> folds ALT NULL A"+ −
+ −
text {* + −
For finite sets, @{term Setalt} is preserved under @{term L}.+ −
*}+ −
+ −
lemma folds_alt_simp [simp]:+ −
fixes rs::"rexp set"+ −
assumes a: "finite rs"+ −
shows "L (\<Uplus>rs) = \<Union> (L ` rs)"+ −
unfolding folds_def+ −
apply(rule set_eqI)+ −
apply(rule someI2_ex)+ −
apply(rule_tac finite_imp_fold_graph[OF a])+ −
apply(erule fold_graph.induct)+ −
apply(auto)+ −
done+ −
+ −
end+ −