Theory Disjoint_Union_CFG

(*
Authors: Markus Gschoßmann, Tobias Nipkow
*)

section ‹Disjoint Union of Sets of Productions›

theory Disjoint_Union_CFG
imports
  "Regular-Sets.Regular_Set"
  Context_Free_Grammar
begin

text ‹This theory provides lemmas relevant when combining the productions of two grammars
with disjoint sets of nonterminals. In particular that the languages of the nonterminals of
one grammar is unchanged by adding productions involving only disjoint nonterminals.›

lemma derivel_disj_Un_if:
  assumes "Rhs_Nts P ∩ Lhss P' = {}"
      and "P ∪ P' ⊢ u ⇒l v"
      and "nts_syms u ∩ Lhss P' = {}"
    shows "P ⊢ u ⇒l v ∧ nts_syms v ∩ Lhss P' = {}"
proof -
  from assms(2) obtain A w u' v' where
        A_w: "(A, w)∈(P ∪ P')"
      and u: "u = map Tm u' @ Nt A # v'"
      and v: "v = map Tm u' @ w @ v'"
    unfolding derivel_iff by fast
  then have "(A,w) ∉ P'" using assms(3) unfolding nts_syms_def Lhss_def by auto
  then have "(A,w) ∈ P" using A_w by blast
  with u v have "(A, w) ∈ P"
      and u: "u = map Tm u' @ Nt A # v'"
      and v: "v = map Tm u' @ w @ v'" by auto
  then have "P ⊢ u ⇒l v" using derivel.intros by fastforce
  moreover have "nts_syms v ∩ Lhss P' = {}"
    using u v assms ‹(A, w) ∈ P› unfolding nts_syms_def Nts_def Rhs_Nts_def by auto
  ultimately show ?thesis by fast
qed

lemma derive_disj_Un_if:
  assumes "Rhs_Nts P ∩ Lhss P' = {}"
      and "P ∪ P' ⊢ u ⇒ v"
      and "nts_syms u ∩ Lhss P' = {}"
    shows "P ⊢ u ⇒ v ∧ nts_syms v ∩ Lhss P' = {}"
proof -
  from assms(2) obtain A w u' v' where
        A_w: "(A, w) ∈ P ∪ P'"
      and u: "u = u' @ Nt A # v'"
      and v: "v = u' @ w @ v'"
    unfolding derive_iff by fast
  then have "(A,w) ∉ P'" using assms(3) unfolding nts_syms_def Lhss_def by auto
  then have "(A,w) ∈ P" using A_w by blast
  with u v have "(A, w) ∈ P" and u: "u = u' @ Nt A # v'" and v: "v = u' @ w @ v'" by auto
  then have "P ⊢ u ⇒ v" using derive.intros by fastforce
  moreover have "nts_syms v ∩ Lhss P' = {}"
    using u v assms ‹(A, w) ∈ P› unfolding nts_syms_def Nts_def Rhs_Nts_def by auto
  ultimately show ?thesis by blast
qed

lemma deriveln_disj_Un_if:
assumes "Rhs_Nts P ∩ Lhss P' = {}"
shows "⟦ P ∪ P' ⊢ u ⇒l(n) v;  nts_syms u ∩ Lhss P' = {} ⟧ ⟹
  P ⊢ u ⇒l(n) v ∧ nts_syms v ∩ Lhss P' = {}"
proof (induction n arbitrary: v)
  case 0
  then show ?case by simp
next
  case (Suc n')
  then obtain v' where split: "P ∪ P' ⊢ u ⇒l(n') v' ∧ P ∪ P' ⊢ v' ⇒l v"
    by (meson relpowp_Suc_E)
  with Suc have "P ⊢ u ⇒l(n') v' ∧ nts_syms v' ∩ Lhss P' = {}"
    by fast
  with Suc show ?case using assms derivel_disj_Un_if
    by (metis split relpowp_Suc_I)
qed

lemma deriven_disj_Un_if:
assumes "Rhs_Nts P ∩ Lhss P' = {}"
shows "⟦ P ∪ P' ⊢ u ⇒(n) v;  nts_syms u ∩ Lhss P' = {} ⟧ ⟹
  P ⊢ u ⇒(n) v ∧ nts_syms v ∩ Lhss P' = {}"
proof (induction n arbitrary: v)
  case 0
  then show ?case by simp
next
  case (Suc n')
  then obtain v' where split: "P ∪ P' ⊢ u ⇒(n') v' ∧ P ∪ P' ⊢ v' ⇒ v"
    by (meson relpowp_Suc_E)
  with Suc have "P ⊢ u ⇒(n') v' ∧ nts_syms v' ∩ Lhss P' = {}"
    by fast
  with Suc show ?case using assms derive_disj_Un_if
    by (metis split relpowp_Suc_I)
qed

lemma derivel_disj_Un_iff:
  assumes "Rhs_Nts P ∩ Lhss P' = {}"
      and "nts_syms u ∩ Lhss P' = {}"
    shows "P ∪ P' ⊢ u ⇒l v ⟷ P ⊢ u ⇒l v"
using assms Un_derivel derivel_disj_Un_if by fastforce

lemma derive_disj_Un_iff:
  assumes "Rhs_Nts P ∩ Lhss P' = {}"
      and "nts_syms u ∩ Lhss P' = {}"
    shows "P ∪ P' ⊢ u ⇒ v ⟷ P ⊢ u ⇒ v"
using assms Un_derive derive_disj_Un_if by fastforce

lemma deriveln_disj_Un_iff:
  assumes "Rhs_Nts P ∩ Lhss P' = {}"
      and "nts_syms u ∩ Lhss P' = {}"
    shows "P ∪ P' ⊢ u ⇒l(n) v ⟷ P ⊢ u ⇒l(n) v"
by (metis Un_derivel assms(1,2) deriveln_disj_Un_if relpowp_mono)

lemma deriven_disj_Un_iff:
  assumes "Rhs_Nts P ∩ Lhss P' = {}"
      and "nts_syms u ∩ Lhss P' = {}"
    shows "P ∪ P' ⊢ u ⇒(n) v ⟷ P ⊢ u ⇒(n) v"
by (metis Un_derive assms(1,2) deriven_disj_Un_if relpowp_mono)

lemma derives_disj_Un_iff:
  assumes "Rhs_Nts P ∩ Lhss P' = {}"
      and "nts_syms u ∩ Lhss P' = {}"
    shows "P ∪ P' ⊢ u ⇒* v ⟷ P ⊢ u ⇒* v"
by (simp add: deriven_disj_Un_iff[OF assms] rtranclp_power)

lemma Lang_disj_Un1:
  assumes "Rhs_Nts P ∩ Lhss P' = {}"
  and "S ∉ Lhss P'"
shows "Lang P S = Lang (P ∪ P') S"
proof -
  from assms(2) have "nts_syms [Nt S] ∩ Lhss P' = {}" unfolding nts_syms_def Lhss_def by simp
  then show ?thesis unfolding Lang_def
    by (simp add: derives_disj_Un_iff[OF assms(1)])
qed


subsection ‹Disjoint Concatenation›

lemma Lang_concat_disj:
assumes "Nts P1 ∩ Nts P2 = {}" "S ∉ Nts P1 ∪ Nts P2 ∪ {S1,S2}" "S1 ∉ Nts P2" "S2 ∉ Nts P1"
shows "Lang ({(S, [Nt S1,Nt S2])} ∪ (P1 ∪ P2)) S = Lang P1 S1 @@ Lang P2 S2"
proof -
  let ?P = "{(S, [Nt S1,Nt S2])} ∪ (P1 ∪ P2)"
  let ?L1 = "Lang P1 S1"
  let ?L2 = "Lang P2 S2"
  have "Lang ?P S ⊆ ?L1 @@ ?L2" 
    proof
      fix w
      assume "w ∈ Lang ?P S"
      then have "?P ⊢ [Nt S] ⇒* map Tm w" using Lang_def by fastforce
      then obtain α where "?P ⊢ α ⇒* map Tm w ∧ (S, α) ∈ ?P" using derives_start1 by fast
      then have dervs: "?P ⊢ [Nt S1, Nt S2] ⇒* map Tm w" using assms unfolding Nts_def by auto
      then obtain w1 w2 where "?P ⊢ [Nt S1] ⇒* map Tm w1" "?P ⊢ [Nt S2] ⇒* map Tm w2" "w = w1 @ w2"
        using derives_append_decomp[of ?P "[Nt S1]" "[Nt S2]"] by (auto simp: map_eq_append_conv)
      then have "P1 ∪ ({(S, [Nt S1,Nt S2])} ∪ P2) ⊢ [Nt S1] ⇒* map Tm w1"
        and "P2 ∪ ({(S, [Nt S1,Nt S2])} ∪ P1) ⊢ [Nt S2] ⇒* map Tm w2" by (simp_all add: Un_commute)
      from derives_disj_Un_iff[THEN iffD1, OF _ _ this(1)]
        derives_disj_Un_iff[THEN iffD1, OF _ _ this(2)] assms
      have "P1 ⊢ [Nt S1] ⇒* map Tm w1" "P2 ⊢ [Nt S2] ⇒* map Tm w2"
        by (auto simp: Nts_Lhss_Rhs_Nts)
      then have "w1 ∈ ?L1" "w2 ∈ ?L2" unfolding Lang_def by simp_all
      with ‹w = _› show "w ∈ ?L1 @@ ?L2" by blast
    qed
    moreover
    have "?L1 @@ ?L2 ⊆ Lang ?P S" 
    proof
      fix w
      assume "w ∈ ?L1 @@ ?L2"
      then obtain w1 w2 where w12_src: "w1 ∈ ?L1 ∧ w2 ∈ ?L2 ∧ w = w1 @ w2" using assms by blast
      have "P1 ⊆ ?P" "P2 ⊆ ?P" by auto
      from w12_src have 1: "P1 ⊢ [Nt S1] ⇒* map Tm w1" and 2: "P2 ⊢ [Nt S2] ⇒* map Tm w2"
        using Lang_def by fast+
      have "?P ⊢ [Nt S] ⇒ [Nt S1, Nt S2]" 
        using derive.intros[of "S" "[Nt S1, Nt S2]" ?P "[]"] by auto
      also have "?P ⊢ ... ⇒* map Tm w1 @ [Nt S2]" using derives_append derives_mono[OF ‹P1 ⊆ ?P›]
        using derives_append[OF derives_mono[OF ‹P1 ⊆ ?P› 1], of "[Nt S2]"] by simp
      also have "?P ⊢ … ⇒* map Tm w1 @ map Tm w2"
        using derives_prepend[OF derives_mono[OF ‹P2 ⊆ ?P› 2]] by simp
      ultimately have "?P ⊢ [Nt S] ⇒* map Tm w" using w12_src by simp
      then show "w ∈ Lang ?P S" unfolding Lang_def by auto
    qed
    ultimately show ?thesis by blast
qed


subsection ‹Disjoint Union including start fork›

lemma derive_from_isolated_fork:
  "⟦ A ∉ Lhss P;  {(A,α1),(A,α2)} ∪ P ⊢ [Nt A] ⇒ β ⟧ ⟹ β = α1 ∨ β = α2"
unfolding derive_singleton by(auto simp: Lhss_def)

lemma derives_fork_if_derives1:
  assumes "P ⊢ [Nt B1] ⇒* map Tm w"
  shows "{(A,[Nt B1]), (A,[Nt B2])} ∪ P ⊢ [Nt A] ⇒* map Tm w" (is "?P ⊢ _ ⇒* _")
proof -
  have "?P ⊢ [Nt A] ⇒ [Nt B1]" using derive_singleton by auto
  also have "?P ⊢ [Nt B1] ⇒* map Tm w" using assms
    by (meson derives_mono sup_ge2)
  finally show ?thesis .
qed

lemma derives_disj_if_derives_fork:
  assumes "A ∉ Nts P ∪ {B1,B2}"
  and "{(A,[Nt B1]), (A,[Nt B2])} ∪ P ⊢ [Nt A] ⇒* map Tm w" (is "?P ⊢ _ ⇒* _")
  shows "P ⊢ [Nt B1] ⇒* map Tm w ∨ P ⊢ [Nt B2] ⇒* map Tm w"
proof -
  obtain β where steps: "?P ⊢ [Nt A] ⇒ β" "?P ⊢ β ⇒* map Tm w"
    using converse_rtranclpE[OF assms(2)] by blast
  have "β = [Nt B1] ∨ β = [Nt B2]"
    using steps(1) derive_from_isolated_fork[of A P] assms(1) by(auto simp: Nts_Lhss_Rhs_Nts)
  then show ?thesis
    using steps(2) derives_disj_Un_iff[of P "{(A,[Nt B1]), (A,[Nt B2])}" β] assms
    by(auto simp: Nts_Lhss_Rhs_Nts)
qed

lemma Lang_distrib_eq_Un_Lang2:
  assumes "A ∉ Nts P ∪ {B1,B2}"
  shows "Lang ({(A,[Nt B1]),(A,[Nt B2])} ∪ P) A = (Lang P B1 ∪ Lang P B2)"
    (is "Lang ?P _ = _" is "?L1 = ?L2")
proof
  show "?L2 ⊆ ?L1" unfolding Lang_def
    using derives_fork_if_derives1[of P B1 _ A B2] derives_fork_if_derives1[of P B2 _ A B1]
    by (auto simp add: insert_commute)
next
  show "?L1 ⊆ ?L2"
    unfolding Lang_def using derives_disj_if_derives_fork[OF assms] by auto
qed

lemma Lang_disj_Un2:
assumes "Nts P1 ∩ Nts P2 = {}" "S ∉ Nts(P1 ∪ P2) ∪ {S1,S2}" "S1 ∉ Nts P2" "S2 ∉ Nts P1"
shows "Lang ({(S,[Nt S1]), (S,[Nt S2])} ∪ (P1 ∪ P2)) S = Lang P1 S1 ∪ Lang P2 S2"
proof -
  let ?P = "{(S, [Nt S1]), (S, [Nt S2])} ∪ (P1 ∪ P2)"
  have "Lang ?P S = Lang (P1 ∪ P2) S1 ∪ Lang (P1 ∪ P2) S2"
    using Lang_distrib_eq_Un_Lang2[OF assms(2)] by simp
  moreover have "Lang (P1 ∪ P2) S1 = Lang P1 S1" using assms(1,3)
    apply(subst Lang_disj_Un1[of P1 P2 S1]) unfolding Nts_Lhss_Rhs_Nts by blast+
  moreover  have "Lang (P2 ∪ P1) S2 = Lang P2 S2" using assms(1,4)
    apply(subst Lang_disj_Un1[of P2 P1 S2]) unfolding Nts_Lhss_Rhs_Nts by blast+
  ultimately show ?thesis
    by (metis sup_commute)
qed

end