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