Set Implicit Arguments.

Require Export tools algebra language regexp words positive_regexp.

Section s.
  Context {atom : Set}{𝐀 : Atom atom}.
  Context {X : Set} {𝐗 : Alphabet 𝐀 X}.

  Global Instance actReg : Action 𝐀 (@regexp letter) :=
    fix act p e {struct e} :=
      match e with
      | ⟪x⟫ ⇒ ⟪p∙x⟫
      | e_un ⇒ e_un
      | e_zero ⇒ e_zero
      | e_add e f ⇒ e_add (act p e) (act p f)
      | e_prod e f ⇒ e_prod (act p e) (act p f)
      | e_star e ⇒ e_star (act p e)
      end.

  Global Instance supReg : Support 𝐀 (@regexp letter) :=
    fix sup e {struct e} :=
      match e with
      | ⟪x⟫ ⇒ ⌊x⌋
      | e_un ⇒ []
      | e_zero ⇒ []
      | e_add e f ⇒ sup e ++ sup f
      | e_prod e f ⇒ sup e ++ sup f
      | e_star e ⇒ sup e
      end.

  Global Instance nominalReg : Nominal 𝐀 (@regexp letter).

  Lemma support_lang e u : ⟦e⟧ u → ⌊u⌋ ⊆ ⌊e⌋.

  Lemma Σ_support L : ⌊L⌋ ≈ ⌊Σ L⌋.

  Lemma prefixes_support e : ⌊prefixes e⌋ ⊆ ⌊e⌋.

  Lemma fresh_lang e a u : a # e → ⟦e⟧ u → a # u.

  Lemma support_join e f : ⌊e∪f⌋ = ⌊e⌋++⌊f⌋.

  Lemma support_prod e f : ⌊e·f⌋ = ⌊e⌋++⌊f⌋.

  Lemma support_star e : ⌊e⋆⌋ = ⌊e⌋.

  Lemma support_Var e : ⌊e⌋ ≈ ⌊Var e⌋.

  Lemma support_ϵ e : ⌊ϵ e⌋ = [].

  Lemma act_lang e p u : ⟦p∙e⟧ u ↔ ⟦e⟧ (p∗∙u).

    Lemma ϵ_act p e : ϵ (p∙e) = ϵ e.

  Lemma δ_act p l e : δ l (p∙e) = p∙ δ (p∗∙l) e.

  Lemma test0_act p e : test0 (p∙e) = test0 e.

  Lemma sizeExpr_act p e : sizeExpr (p∙e) = sizeExpr e.

  Lemma Σ_act p L : p ∙ Σ L = Σ (p∙L).

  Lemma positive_act p e : positive (p∙e) = p ∙ (positive e).

  Lemma KA_act p e f : e =KA f → p ∙ e =KA p ∙ f.

  Fixpoint sizeAt e (a : atom) :=
    match e with
    | e_un | e_zero | ⟪var _⟫ ⇒ 0
    | ⟪open b⟫ | ⟪close b⟫ ⇒ if a=?=b then 1 else 0
    | e_add e f | e_prod e f ⇒ sizeAt e a + sizeAt f a
    | e_star e ⇒ sizeAt e a
    end.

  Lemma sizeAt_fresh e a : a # e → sizeAt e a = 0.

  Lemma size_sizeAt e : sum (sizeAt e) {{⌊e⌋}} ≤ sizeExpr e.


End s.