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