theory Closure2
imports Closures
begin
inductive emb :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<preceq> _")
where
emb0 [Pure.intro]: "emb [] bs"
| emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)"
| emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)"
lemma emb_refl:
shows "x \<preceq> x"
apply(induct x)
apply(auto intro: emb.intros)
done
lemma emb_right:
assumes a: "x \<preceq> y"
shows "x \<preceq> y @ y'"
using a
apply(induct arbitrary: y')
apply(auto intro: emb.intros)
done
lemma emb_left:
assumes a: "x \<preceq> y"
shows "x \<preceq> y' @ y"
using a
apply(induct y')
apply(auto intro: emb.intros)
done
lemma emb_appendI:
assumes a: "x \<preceq> x'"
and b: "y \<preceq> y'"
shows "x @ y \<preceq> x' @ y'"
using a b
apply(induct)
apply(auto intro: emb.intros emb_left)
done
lemma emb_append:
assumes a: "x \<preceq> y1 @ y2"
shows "\<exists>x1 x2. x = x1 @ x2 \<and> x1 \<preceq> y1 \<and> x2 \<preceq> y2"
using a
apply(induct x y\<equiv>"y1 @ y2" arbitrary: y1 y2)
apply(auto intro: emb0)[1]
apply(simp add: Cons_eq_append_conv)
apply(auto)[1]
apply(rule_tac x="[]" in exI)
apply(rule_tac x="as" in exI)
apply(auto intro: emb.intros)[1]
apply(simp add: append_eq_append_conv2)
apply(drule_tac x="ys'" in meta_spec)
apply(drule_tac x="y2" in meta_spec)
apply(auto)[1]
apply(rule_tac x="x1" in exI)
apply(rule_tac x="x2" in exI)
apply(auto intro: emb.intros)[1]
apply(subst (asm) Cons_eq_append_conv)
apply(auto)[1]
apply(rule_tac x="[]" in exI)
apply(rule_tac x="a # as" in exI)
apply(auto intro: emb.intros)[1]
apply(simp add: append_eq_append_conv2)
apply(drule_tac x="ys'" in meta_spec)
apply(drule_tac x="y2" in meta_spec)
apply(auto)[1]
apply(rule_tac x="a # x1" in exI)
apply(rule_tac x="x2" in exI)
apply(auto intro: emb.intros)[1]
done
definition
"SUBSEQ A \<equiv> {x. \<exists>y \<in> A. x \<preceq> y}"
definition
"SUPSEQ A \<equiv> (- SUBSEQ A) \<union> A"
lemma [simp]:
"SUBSEQ {} = {}"
unfolding SUBSEQ_def
by auto
lemma [simp]:
"SUBSEQ {[]} = {[]}"
unfolding SUBSEQ_def
apply(auto)
apply(erule emb.cases)
apply(auto)[3]
apply(rule emb0)
done
lemma SUBSEQ_atom [simp]:
"SUBSEQ {[a]} = {[], [a]}"
apply(auto simp add: SUBSEQ_def)
apply(erule emb.cases)
apply(auto)[3]
apply(erule emb.cases)
apply(auto)[3]
apply(erule emb.cases)
apply(auto)[3]
apply(rule emb0)
apply(rule emb2)
apply(rule emb0)
done
lemma SUBSEQ_union [simp]:
"SUBSEQ (A \<union> B) = SUBSEQ A \<union> SUBSEQ B"
unfolding SUBSEQ_def by auto
lemma SUBSEQ_Union [simp]:
fixes A :: "nat \<Rightarrow> 'a lang"
shows "SUBSEQ (\<Union>n. (A n)) = (\<Union>n. (SUBSEQ (A n)))"
unfolding SUBSEQ_def image_def by auto
lemma SUBSEQ_conc1:
"\<lbrakk>x \<in> SUBSEQ A; y \<in> SUBSEQ B\<rbrakk> \<Longrightarrow> x @ y \<in> SUBSEQ (A \<cdot> B)"
unfolding SUBSEQ_def
apply(auto)
apply(rule_tac x="xa @ xaa" in bexI)
apply(rule emb_appendI)
apply(simp_all)
done
lemma SUBSEQ_conc2:
"x \<in> SUBSEQ (A \<cdot> B) \<Longrightarrow> x \<in> (SUBSEQ A) \<cdot> (SUBSEQ B)"
unfolding SUBSEQ_def conc_def
apply(auto)
apply(drule emb_append)
apply(auto)
done
lemma SUBSEQ_conc [simp]:
"SUBSEQ (A \<cdot> B) = SUBSEQ A \<cdot> SUBSEQ B"
apply(auto)
apply(simp add: SUBSEQ_conc2)
apply(subst (asm) conc_def)
apply(auto simp add: SUBSEQ_conc1)
done
lemma SUBSEQ_star1:
assumes a: "x \<in> (SUBSEQ A)\<star>"
shows "x \<in> SUBSEQ (A\<star>)"
using a
apply(induct rule: star_induct)
apply(simp add: SUBSEQ_def)
apply(rule_tac x="[]" in bexI)
apply(rule emb0)
apply(auto)[1]
apply(drule SUBSEQ_conc1)
apply(assumption)
apply(subst star_unfold_left)
apply(simp only: SUBSEQ_union)
apply(simp)
done
lemma SUBSEQ_star2_aux:
assumes a: "x \<in> SUBSEQ (A ^^ n)"
shows "x \<in> (SUBSEQ A)\<star>"
using a
apply(induct n arbitrary: x)
apply(simp)
apply(simp)
apply(simp add: conc_def)
apply(auto)
done
lemma SUBSEQ_star2:
assumes a: "x \<in> SUBSEQ (A\<star>)"
shows "x \<in> (SUBSEQ A)\<star>"
using a
apply(subst (asm) star_def)
apply(auto simp add: SUBSEQ_star2_aux)
done
lemma SUBSEQ_star [simp]:
shows "SUBSEQ (A\<star>) = (SUBSEQ A)\<star>"
using SUBSEQ_star1 SUBSEQ_star2 by auto
lemma SUBSEQ_fold:
shows "SUBSEQ A \<union> A = SUBSEQ A"
apply(auto simp add: SUBSEQ_def)
apply(rule_tac x="x" in bexI)
apply(auto simp add: emb_refl)
done
lemma SUPSEQ_union [simp]:
"SUPSEQ (A \<union> B) = (SUPSEQ A \<union> B) \<inter> (SUPSEQ B \<union> A)"
unfolding SUPSEQ_def
by auto
definition
Notreg :: "'a::finite rexp \<Rightarrow> 'a rexp"
where
"Notreg r \<equiv> SOME r'. lang r' = - (lang r)"
lemma [simp]:
"lang (Notreg r) = - lang r"
apply(simp add: Notreg_def)
apply(rule someI2_ex)
apply(auto)
apply(subgoal_tac "regular (lang r)")
apply(drule closure_complement)
apply(auto)
done
definition
Interreg :: "'a::finite rexp \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
where
"Interreg r1 r2 = Notreg (Plus (Notreg r1) (Notreg r2))"
lemma [simp]:
"lang (Interreg r1 r2) = (lang r1) \<inter> (lang r2)"
by (simp add: Interreg_def)
definition
Diffreg :: "'a::finite rexp \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
where
"Diffreg r1 r2 = Notreg (Plus (Notreg r1) r2)"
lemma [simp]:
"lang (Diffreg r1 r2) = (lang r1) - (lang r2)"
by (auto simp add: Diffreg_def)
definition
Allreg :: "'a::finite rexp"
where
"Allreg \<equiv> \<Uplus>(Atom ` UNIV)"
lemma Allreg_lang [simp]:
"lang Allreg = (\<Union>a. {[a]})"
unfolding Allreg_def
by auto
lemma [simp]:
"(\<Union>a. {[a]})\<star> = UNIV"
apply(auto)
apply(induct_tac x rule: list.induct)
apply(auto)
apply(subgoal_tac "[a] @ list \<in> (\<Union>a. {[a]})\<star>")
apply(simp)
apply(rule append_in_starI)
apply(auto)
done
lemma Star_Allreg_lang [simp]:
"lang (Star Allreg) = UNIV"
by (simp)
fun UP :: "'a::finite rexp \<Rightarrow> 'a rexp"
where
"UP (Zero) = Star Allreg"
| "UP (One) = Star Allreg"
| "UP (Atom c) = Times Allreg (Star Allreg)"
| "UP (Plus r1 r2) = Interreg (Plus (UP r1) (r2)) (Plus (UP r2) r1)"
| "UP (Times r1 r2) =
Plus (Notreg (Times (Plus (Notreg (UP r1)) r1) (Plus (Notreg (UP r2)) r2))) (Times r1 r2)"
| "UP (Star r) = Plus (Notreg (Star (Plus (Notreg (UP r)) r))) (Star r)"
lemma UP:
"lang (UP r) = SUPSEQ (lang r)"
apply(induct r)
apply(simp add: SUPSEQ_def)
apply(simp add: SUPSEQ_def)
apply(simp add: Compl_eq_Diff_UNIV)
apply(auto)[1]
apply(simp add: SUPSEQ_def)
apply(simp add: Compl_eq_Diff_UNIV)
apply(rule sym)
apply(rule_tac s="UNIV - {[]}" in trans)
apply(auto)[1]
apply(auto simp add: conc_def)[1]
apply(case_tac x)
apply(simp)
apply(simp)
apply(rule_tac x="[a]" in exI)
apply(simp)
apply(simp)
apply(simp)
apply(simp add: SUPSEQ_def)
apply(simp add: Un_Int_distrib2)
apply(simp add: Compl_partition2)
apply(simp add: SUBSEQ_fold)
apply(simp add: Un_Diff)
apply(simp add: SUPSEQ_def)
apply(simp add: Un_Int_distrib2)
apply(simp add: Compl_partition2)
apply(simp add: SUBSEQ_fold)
done
lemma SUPSEQ_reg:
fixes A :: "'a::finite lang"
assumes "regular A"
shows "regular (SUPSEQ A)"
proof -
from assms obtain r::"'a::finite rexp" where eq: "lang r = A" by auto
moreover
have "lang (UP r) = SUPSEQ (lang r)" by (rule UP)
ultimately show "regular (SUPSEQ A)" by auto
qed
end