(* Authors: Fabian Lehr *)

section ‹Parikh images›

theory Parikh_Img
  imports 
    "Reg_Lang_Exp"
    "HOL-Library.Multiset"
begin


subsection ‹Definition and basic lemmas›

text ‹The Parikh vector of a finite word describes how often each symbol of the alphabet occurs in the word.
  represent parikh vectors by multisets. The Parikh image of a language ‹L›, denoted by ‹Ψ L›,
  then the set of Parikh vectors of all words in the language.›

definition parikh_img :: "'a lang → 'a multiset set" where
  "parikh_img L = mset ` L"

notation parikh_img ("Ψ")

lemma parikh_img_Un [simp]: "Ψ (L1 ∪ L2) = Ψ L1 ∪ Ψ L2"
  by (auto simp add: parikh_img_def)

lemma parikh_img_UNION: "Ψ (∪(L ` I)) = ∪ ((λi. Ψ (L i)) ` I)"
  by (auto simp add: parikh_img_def)

lemma parikh_img_conc: "Ψ (L1 @@ L2) = { m1 + m2 | m1 m2. m1 ∈ Ψ L1 ∧ m2 ∈ Ψ L2 }"
  unfolding parikh_img_def by force

lemma parikh_img_commut: "Ψ (L1 @@ L2) = Ψ (L2 @@ L1)"
proof -
  have "{ m1 + m2 | m1 m2. m1 ∈ Ψ L1 ∧ m2 ∈ Ψ L2 } =
        { m2 + m1 | m1 m2. m1 ∈ Ψ L1 ∧ m2 ∈ Ψ L2 }"
    using add.commute by blast
  then show ?thesis
    using parikh_img_conc[of L1] parikh_img_conc[of L2] by auto
qed


subsection ‹Monotonicity properties›

lemma parikh_img_mono: "A ⊆ B ==> Ψ A ⊆ Ψ B"
  unfolding parikh_img_def by fast

lemma parikh_conc_right_subset: "Ψ A ⊆ Ψ B ==> Ψ (A @@ C) ⊆ Ψ (B @@ C)"
  by (auto simp add: parikh_img_conc)

lemma parikh_conc_left_subset: "Ψ A ⊆ Ψ B ==> Ψ (C @@ A) ⊆ Ψ (C @@ B)"
  by (auto simp add: parikh_img_conc)

lemma parikh_conc_subset:
  assumes "Ψ A ⊆ Ψ C"
      and "Ψ B ⊆ Ψ D"
    shows "Ψ (A @@ B) ⊆ Ψ (C @@ D)"
  using assms parikh_conc_right_subset parikh_conc_left_subset by blast

lemma parikh_conc_right: "Ψ A = Ψ B ==> Ψ (A @@ C) = Ψ (B @@ C)"
  by (auto simp add: parikh_img_conc)

lemma parikh_conc_left: "Ψ A = Ψ B ==> Ψ (C @@ A) = Ψ (C @@ B)"
  by (auto simp add: parikh_img_conc)

lemma parikh_pow_mono: "Ψ A ⊆ Ψ B ==> Ψ (A ^^ n) ⊆ Ψ (B ^^ n)"
  by (induction n) (auto simp add: parikh_img_conc)


lemma parikh_star_mono:
  assumes "Ψ A ⊆ Ψ B"
  shows "Ψ (star A) ⊆ Ψ (star B)"
proof
  fix v
  assume "v ∈ Ψ (star A)"
  then obtain w where w_intro: "mset w = v ∧ w ∈ star A" unfolding parikh_img_def by blast
  then obtain n where "w ∈ A ^^ n" unfolding star_def by blast
  then have "v ∈ Ψ (A ^^ n)" using w_intro unfolding parikh_img_def by blast
  with assms have "v ∈ Ψ (B ^^ n)" using parikh_pow_mono by blast
  then show "v ∈ Ψ (star B)" unfolding star_def using parikh_img_UNION by fastforce
qed

lemma parikh_star_mono_eq:
  assumes "Ψ A = Ψ B"
  shows "Ψ (star A) = Ψ (star B)"
  using parikh_star_mono by (metis Orderings.order_eq_iff assms)


lemma parikh_img_subst_mono:
  assumes "∀i. Ψ (eval (A i) v) ⊆ Ψ (eval (B i) v)"
  shows "Ψ (eval (subst A f) v) ⊆ Ψ (eval (subst B f) v)"
proof (induction f)
  case (Concat f1 f2)
  then have "Ψ (eval (subst A f1) v @@ eval (subst A f2) v)
              ⊆ Ψ (eval (subst B f1) v @@ eval (subst B f2) v)"
    using parikh_conc_subset by blast
  then show ?case by simp
next
  case (Star f)
  then have "Ψ (star (eval (subst A f) v)) ⊆ Ψ (star (eval (subst B f) v))"
    using parikh_star_mono by blast
  then show ?case by simp
qed (use assms(1) in auto)

lemma parikh_img_subst_mono_upd:
  assumes "Ψ (eval A v) ⊆ Ψ (eval B v)"
  shows "Ψ (eval (subst (Var(x := A)) f) v) ⊆ Ψ (eval (subst (Var(x := B)) f) v)"
  using parikh_img_subst_mono[of "Var(x := A)" v "Var(x := B)"] assms by auto

lemma rlexp_mono_parikh:
  assumes "∀i ∈ vars f. Ψ (v i) ⊆ Ψ (v' i)"
  shows "Ψ (eval f v) ⊆ Ψ (eval f v')"
using assms proof (induction f rule: rlexp.induct)
case (Concat f1 f2)
  then have "Ψ (eval f1 v @@ eval f2 v) ⊆ Ψ (eval f1 v' @@ eval f2 v')"
    using parikh_conc_subset by (metis UnCI vars.simps(4))
  then show ?case by simp
qed (auto simp add: SUP_mono' parikh_img_UNION parikh_star_mono)

lemma rlexp_mono_parikh_eq:
  assumes "∀i ∈ vars f. Ψ (v i) = Ψ (v' i)"
  shows "Ψ (eval f v) = Ψ (eval f v')"
  using assms rlexp_mono_parikh by blast



subsection ‹$\Psi \; (A \cup B)^* = \Psi \; A^* B^*$›

text ‹\label{sec:parikh_img_star}›
text ‹This property is claimed by Pilling in cite‹Pilling› and will be needed later.›

lemma parikh_img_union_pow_aux1:
  assumes "v ∈ Ψ ((A ∪ B) ^^ n)"
    shows "v ∈ Ψ (∪i ≤ n. A ^^ i @@ B ^^ (n-i))"
using assms proof (induction n arbitrary: v)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then obtain w where w_intro: "w ∈ (A ∪ B) ^^ (Suc n) ∧ mset w = v"
    unfolding parikh_img_def by auto
  then obtain w1 w2 where w1_w2_intro: "w = w1@w2 ∧ w1 ∈ A ∪ B ∧ w2 ∈ (A ∪ B) ^^ n" by fastforce
  let ?v1 = "mset w1" and ?v2 = "mset w2"
  from w1_w2_intro have "?v2 ∈ Ψ ((A ∪ B) ^^ n)" unfolding parikh_img_def by blast
  with Suc.IH have "?v2 ∈ Ψ (∪i ≤ n. A ^^ i @@ B ^^ (n-i))" by auto
  then obtain w2' where w2'_intro: "mset w2' = mset w2 ∧
      w2' ∈ (∪i ≤ n. A ^^ i @@ B ^^ (n-i))" unfolding parikh_img_def by fastforce
  then obtain i where i_intro: "i ≤ n ∧ w2' ∈ A ^^ i @@ B ^^ (n-i)" by blast
  from w1_w2_intro w2'_intro have "mset w = mset (w1@w2')"
    by simp
  moreover have "mset (w1@w2') ∈ Ψ (∪i ≤ Suc n. A ^^ i @@ B ^^ (Suc n-i))"
  proof (cases "w1 ∈ A")
    case True
    with i_intro have Suc_i_valid: "Suc i ≤ Suc n" and "w1@w2' ∈ A ^^ (Suc i) @@ B ^^ (Suc n - Suc i)"
      by (auto simp add: conc_assoc)
    then have "mset (w1@w2') ∈ Ψ (A ^^ (Suc i) @@ B ^^ (Suc n - Suc i))"
      unfolding parikh_img_def by blast
    with Suc_i_valid parikh_img_UNION show ?thesis by fast
  next
    case False
    with w1_w2_intro have "w1 ∈ B" by blast
    with i_intro have "mset (w1@w2') ∈ Ψ (B @@ A ^^ i @@ B ^^ (n-i))"
      unfolding parikh_img_def by blast
    then have "mset (w1@w2') ∈ Ψ (A ^^ i @@ B ^^ (Suc n-i))"
      using parikh_img_commut conc_assoc
      by (metis Suc_diff_le conc_pow_comm i_intro lang_pow.simps(2))
    with i_intro parikh_img_UNION show ?thesis by fastforce
  qed
  ultimately show ?case using w_intro by auto
qed

lemma parikh_img_star_aux1:
  assumes "v ∈ Ψ (star (A ∪ B))"
  shows "v ∈ Ψ (star A @@ star B)"
proof -
  from assms have "v ∈ (∪n. Ψ ((A ∪ B) ^^ n))"
    unfolding star_def using parikh_img_UNION by metis
  then obtain n where "v ∈ Ψ ((A ∪ B) ^^ n)" by blast
  then have "v ∈ Ψ (∪i ≤ n. A ^^ i @@ B ^^ (n-i))"
    using parikh_img_union_pow_aux1 by auto
  then have "v ∈ (∪i≤n. Ψ (A ^^ i @@ B ^^ (n-i)))" using parikh_img_UNION by metis
  then obtain i where "i≤n ∧ v ∈ Ψ (A ^^ i @@ B ^^ (n-i))" by blast
  then obtain w where w_intro: "mset w = v ∧ w ∈ A ^^ i @@ B ^^ (n-i)"
    unfolding parikh_img_def by blast
  then obtain w1 w2 where w_decomp: "w=w1@w2 ∧ w1 ∈ A ^^ i ∧ w2 ∈ B ^^ (n-i)" by blast
  then have "w1 ∈ star A" and "w2 ∈ star B" by auto
  with w_decomp have "w ∈ star A @@ star B" by auto
  with w_intro show ?thesis unfolding parikh_img_def by blast
qed

lemma parikh_img_star_aux2:
  assumes "v ∈ Ψ (star A @@ star B)"
  shows "v ∈ Ψ (star (A ∪ B))"
proof -
  from assms obtain w where w_intro: "mset w = v ∧ w ∈ star A @@ star B"
    unfolding parikh_img_def by blast
  then obtain w1 w2 where w_decomp: "w=w1@w2 ∧ w1 ∈ star A ∧ w2 ∈ star B" by blast
  then obtain i j where "w1 ∈ A ^^ i" and w2_intro: "w2 ∈ B ^^ j" unfolding star_def by blast
  then have w1_in_union: "w1 ∈ (A ∪ B) ^^ i" using lang_pow_mono by blast
  from w2_intro have "w2 ∈ (A ∪ B) ^^ j" using lang_pow_mono by blast
  with w1_in_union w_decomp have "w ∈ (A ∪ B) ^^ (i+j)" using lang_pow_add by fast
  with w_intro show ?thesis unfolding parikh_img_def by auto
qed

lemma parikh_img_star: "Ψ (star (A ∪ B)) = Ψ (star A @@ star B)"
proof
  show "Ψ (star (A ∪ B)) ⊆ Ψ (star A @@ star B)" using parikh_img_star_aux1 by auto
  show "Ψ (star A @@ star B) ⊆ Ψ (star (A ∪ B))" using parikh_img_star_aux2 by auto
qed



subsection ‹$\Psi \; (E^* F)^* = \Psi \; \left(\{\varepsilon\} \cup E^* F^* F\right)$›

text ‹\label{sec:parikh_img_star2}›
text ‹This property (where $\varepsilon$ denotes the empty word) is claimed by
  as well cite‹Pilling›; we will use it later.›

(* It even holds = but \<subseteq> suffices for the proof *)
lemma parikh_img_conc_pow: "Ψ ((A @@ B) ^^ n) ⊆ Ψ (A ^^ n @@ B ^^ n)"
proof (induction n)
  case (Suc n)
  then have "Ψ ((A @@ B) ^^ n @@ A @@ B) ⊆ Ψ (A ^^ n @@ B ^^ n @@ A @@ B)"
    using parikh_conc_right_subset conc_assoc by metis
  also have "… = Ψ (A ^^ n @@ A @@ B ^^ n @@ B)"
    by (metis parikh_img_commut conc_assoc parikh_conc_left)
  finally show ?case by (simp add: conc_assoc conc_pow_comm)
qed simp

lemma parikh_img_conc_star: "Ψ (star (A @@ B)) ⊆ Ψ (star A @@ star B)"
proof
  fix v
  assume "v ∈ Ψ (star (A @@ B))"
  then have "∃n. v ∈ Ψ ((A @@ B) ^^ n)" unfolding star_def by (simp add: parikh_img_UNION)
  then obtain n where "v ∈ Ψ ((A @@ B) ^^ n)" by blast
  with parikh_img_conc_pow have "v ∈ Ψ (A ^^ n @@ B ^^ n)" by fast
  then have "v ∈ Ψ (A ^^ n @@ star B)"
    unfolding star_def using parikh_conc_left_subset
    by (metis (no_types, lifting) Sup_upper parikh_img_mono rangeI subset_eq)
  then show "v ∈ Ψ (star A @@ star B)"
    unfolding star_def using parikh_conc_right_subset
    by (metis (no_types, lifting) Sup_upper parikh_img_mono rangeI subset_eq)
qed

lemma parikh_img_conc_pow2: "Ψ ((A @@ B) ^^ Suc n) ⊆ Ψ (star A @@ star B @@ B)"
proof
  fix v
  assume "v ∈ Ψ ((A @@ B) ^^ Suc n)"
  with parikh_img_conc_pow have "v ∈ Ψ (A ^^ Suc n @@ B ^^ n @@ B)"
    by (metis conc_pow_comm lang_pow.simps(2) subsetD)
  then have "v ∈ Ψ (star A @@ B ^^ n @@ B)"
    unfolding star_def using parikh_conc_right_subset
    by (metis (no_types, lifting) Sup_upper parikh_img_mono rangeI subset_eq)
  then show "v ∈ Ψ (star A @@ star B @@ B)"
    unfolding star_def using parikh_conc_right_subset parikh_conc_left_subset
    by (metis (no_types, lifting) Sup_upper parikh_img_mono rangeI subset_eq)
qed

lemma parikh_img_star2_aux1:
  "Ψ (star (star E @@ F)) ⊆ Ψ ({[]} ∪ star E @@ star F @@ F)"
proof
  fix v
  assume "v ∈ Ψ (star (star E @@ F))"
  then have "∃n. v ∈ Ψ ((star E @@ F) ^^ n)"
    unfolding star_def by (simp add: parikh_img_UNION)
  then obtain n where v_in_pow_n: "v ∈ Ψ ((star E @@ F) ^^ n)" by blast
  show "v ∈ Ψ ({[]} ∪ star E @@ star F @@ F)"
  proof (cases n)
    case 0
    with v_in_pow_n have "v = mset []" unfolding parikh_img_def by simp
    then show ?thesis unfolding parikh_img_def by blast
  next
    case (Suc m)
    with parikh_img_conc_pow2 v_in_pow_n have "v ∈ Ψ (star (star E) @@ star F @@ F)" by blast
    then show ?thesis by (metis UnCI parikh_img_Un star_idemp)
  qed
qed

lemma parikh_img_star2_aux2: "Ψ (star E @@ star F @@ F) ⊆ Ψ (star (star E @@ F))"
proof -
  have "F ⊆ star E @@ F" unfolding star_def using Nil_in_star
    by (metis concI_if_Nil1 star_def subsetI)
  then have "Ψ (star E @@ F @@ star F) ⊆ Ψ (star E @@ F @@ star (star E @@ F))"
    using parikh_conc_left_subset parikh_img_mono parikh_star_mono by meson
  also have "… ⊆ Ψ (star (star E @@ F))"
    by (metis conc_assoc inf_sup_ord(3) parikh_img_mono star_unfold_left)
  finally show ?thesis using conc_star_comm by metis
qed

lemma parikh_img_star2: "Ψ (star (star E @@ F)) = Ψ ({[]} ∪ star E @@ star F @@ F)"
proof
  from parikh_img_star2_aux1
    show "Ψ (star (star E @@ F)) ⊆ Ψ ({[]} ∪ star E @@ star F @@ F)" .
  from parikh_img_star2_aux2
    show "Ψ ({[]} ∪ star E @@ star F @@ F) ⊆ Ψ (star (star E @@ F))"
    by (metis le_sup_iff parikh_img_Un star_unfold_left sup.cobounded2)
qed



subsection ‹A homogeneous-like property for regular language expressions›

text ‹\label{sec:rlexp_homogeneous}›

lemma rlexp_homogeneous_aux:
  assumes "v x = star Y @@ Z"
    shows "Ψ (eval f v) ⊆ Ψ (star Y @@ eval f (v(x := Z)))"
proof (induction f)
  case (Var y)
  show ?case
  proof (cases "x = y")
    case True
    with Var assms show ?thesis by simp
  next
    case False
    have "eval (Var y) v ⊆ star Y @@ eval (Var y) v" by (metis Nil_in_star concI_if_Nil1 subsetI)
    with False parikh_img_mono show ?thesis by auto
  qed
next
  case (Const l)
  have "eval (Const l) v ⊆ star Y @@ eval (Const l) v" using concI_if_Nil1 by blast
  then show ?case by (simp add: parikh_img_mono)
next
  case (Union f g)
  then have "Ψ (eval (Union f g) v) ⊆ Ψ (star Y @@ eval f (v(x := Z)) ∪
                                                            star Y @@ eval g (v(x := Z)))"
    by (metis eval.simps(3) parikh_img_Un sup.mono)
  then show ?case by (metis conc_Un_distrib(1) eval.simps(3))
next
  case (Concat f g)
  then have "Ψ (eval (Concat f g) v) ⊆ Ψ ((star Y @@ eval f (v(x := Z)))
                                                          @@ star Y @@ eval g (v(x := Z)))"
    by (metis eval.simps(4) parikh_conc_subset)
  also have "… = Ψ (star Y @@ star Y @@ eval f (v(x := Z)) @@ eval g (v(x := Z)))"
    by (metis conc_assoc parikh_conc_right parikh_img_commut)
  also have "… = Ψ (star Y @@ eval f (v(x := Z)) @@ eval g (v(x := Z)))"
    by (metis conc_assoc conc_star_star)
  finally show ?case by (metis eval.simps(4))
next
  case (Star f)
  then have "Ψ (star (eval f v)) ⊆ Ψ (star (star Y @@ eval f (v(x := Z))))"
    using parikh_star_mono by metis
  also from parikh_img_conc_star have "… ⊆ Ψ (star Y @@ star (eval f (v(x := Z))))"
    by fastforce
  finally show ?case by (metis eval.simps(5))
qed

text ‹Now we can prove the desired homogeneous-like property which will become useful later.
  this property slightly differs from the property claimed in cite‹Pilling›. However, our
  is easier to prove formally and it suffices for the rest of the proof.›
lemma rlexp_homogeneous:  "Ψ (eval (subst (Var(x := Concat (Star y) z)) f) v)
                          ⊆ Ψ (eval (Concat (Star y) (subst (Var(x := z)) f)) v)"
                          (is "Ψ ?L ⊆ Ψ ?R")
proof -
  let ?v' = "v(x := star (eval y v) @@ eval z v)"
  have "Ψ ?L = Ψ (eval f ?v')" using substitution_lemma_upd[where f=f] by simp
  also have "… ⊆ Ψ (star (eval y v) @@ eval f (?v'(x := eval z v)))"
    using rlexp_homogeneous_aux[of ?v'] unfolding fun_upd_def by auto
  also have "… = Ψ ?R" using substitution_lemma[of "v(x := eval z v)"] by simp
  finally show ?thesis .
qed


subsection ‹Extension of Arden's lemma to Parikh images›

text ‹\label{sec:parikh_arden}›

lemma parikh_img_arden_aux:
  assumes "Ψ (A @@ X ∪ B) ⊆ Ψ X"
  shows "Ψ (A ^^ n @@ B) ⊆ Ψ X"
proof (induction n)
  case 0
  with assms show ?case by auto
next
  case (Suc n)
  then have "Ψ (A ^^ (Suc n) @@ B) ⊆ Ψ (A @@ A ^^ n @@B)"
    by (simp add: conc_assoc)
  moreover from Suc parikh_conc_left have "… ⊆ Ψ (A @@ X)"
    by (metis conc_Un_distrib(1) parikh_img_Un sup.orderE sup.orderI)
  moreover from Suc.prems assms have "… ⊆ Ψ X" by auto
  ultimately show ?case by fast
qed

lemma parikh_img_arden:
  assumes "Ψ (A @@ X ∪ B) ⊆ Ψ X"
  shows "Ψ (star A @@ B) ⊆ Ψ X"
proof
  fix x
  assume "x ∈ Ψ (star A @@ B)"
  then have "∃n. x ∈ Ψ (A ^^ n @@ B)"
    unfolding star_def by (simp add: conc_UNION_distrib(2) parikh_img_UNION)
  then obtain n where "x ∈ Ψ (A ^^ n @@ B)" by blast
  then show "x ∈ Ψ X" using parikh_img_arden_aux[OF assms] by fast
qed


subsection ‹Equivalence class of languages with identical Parikh image›

text ‹\label{sec:parikh_eq_class}›
text ‹For a given language ‹L›, we define the equivalence class of all languages with identical Parikh
 :›

definition parikh_img_eq_class :: "'a lang → 'a lang set" where
  "parikh_img_eq_class L = {L'. Ψ L' = Ψ L}"

lemma parikh_img_Union_class: "Ψ A = Ψ (∪(parikh_img_eq_class A))"
proof
  let ?A' = "∪(parikh_img_eq_class A)"
  show "Ψ A ⊆ Ψ ?A'"
    unfolding parikh_img_eq_class_def by (simp add: Union_upper parikh_img_mono)
  show "Ψ ?A' ⊆ Ψ A"
  proof
    fix v
    assume "v ∈ Ψ ?A'"
    then obtain a where a_intro: "mset a = v ∧ a ∈ ?A'"
      unfolding parikh_img_def by blast
    then obtain L where L_intro: "a ∈ L ∧ L ∈ parikh_img_eq_class A"
      unfolding parikh_img_eq_class_def by blast
    then have "Ψ L = Ψ A" unfolding parikh_img_eq_class_def by fastforce
    with a_intro L_intro show "v ∈ Ψ A" unfolding parikh_img_def by blast
  qed
qed

lemma subseteq_comm_subseteq:
  assumes "Ψ A ⊆ Ψ B"
  shows "A ⊆ ∪(parikh_img_eq_class B)" (is "A ⊆ ?B'")
proof
  fix a
  assume a_in_A: "a ∈ A"
  from assms have "Ψ A ⊆ Ψ ?B'"
    using parikh_img_Union_class by blast
  with a_in_A have vec_a_in_B': "mset a ∈ Ψ ?B'" unfolding parikh_img_def by fast
  then have "∃b. mset b = mset a ∧ b ∈ ?B'"
    unfolding parikh_img_def by fastforce
  then obtain b where b_intro: "mset b = mset a ∧ b ∈ ?B'" by blast
  with vec_a_in_B' have "Ψ (?B' ∪ {a}) = Ψ ?B'"unfolding parikh_img_def by blast
  with parikh_img_Union_class have "Ψ (?B' ∪ {a}) = Ψ B" by blast
  then show "a ∈ ?B'" unfolding parikh_img_eq_class_def by blast
qed

end