Theory Expansion

(*<*)
theory Expansion
  imports Context_Free_Grammar.Context_Free_Grammar
begin
(*>*)

section ‹Expansion of Grammars›

lemma conc_eq_empty_iff: "X @@ Y = {} ⟷ X = {} ∨ Y = {}"
  by auto

lemma Nts_syms_conc: "⋃(Nts_syms ` (X @@ Y)) =
 (if X = {} ∨ Y = {} then {} else ⋃(Nts_syms ` X) ∪ ⋃(Nts_syms ` Y))"
  by (force elim!: concE)

text ‹We consider the set of admissible expansions of grammars.

For a symbol,
one option is not to expand it,
and the other option for (expandable) nonterminals is to expand to the all rhss.›

definition Expand_sym_ops :: "('n,'t) Prods ⇒ 'n set ⇒ ('n,'t) sym ⇒ ('n,'t) syms set set" where
"Expand_sym_ops P X x =
  insert {[x]} (case x of Nt A ⇒ if A ∈ X then {Rhss P A} else {} | _ ⇒ {})"

lemma Expand_sym_ops_simps:
  "Expand_sym_ops P X (Tm a) = {{[Tm a]}}"
  "Expand_sym_ops P X (Nt A) = insert {[Nt A]} (if A ∈ X then {Rhss P A} else {})"
  by (auto simp: Expand_sym_ops_def)

lemma Expand_sym_ops_self: "{[x]} ∈ Expand_sym_ops P X x"
  by (simp add: Expand_sym_ops_def)

text ‹Mixed words allow all possible combinations of the options for the symbols.›

fun Expand_syms_ops :: "('n,'t) Prods ⇒ 'n set ⇒ ('n,'t) syms ⇒ ('n,'t) syms set set" where
  "Expand_syms_ops P X [] = {{[]}}"
| "Expand_syms_ops P X (x#xs) =
   {αs @@ βs | αs βs. αs ∈ Expand_sym_ops P X x ∧ βs ∈ Expand_syms_ops P X xs}"

lemma Expand_syms_ops_self: "{α} ∈ Expand_syms_ops P X α"
proof (induction α)
  case Nil
  show ?case by simp
next
  case (Cons x α)
  have "{x # α} = {[x]} @@ {α}" by (auto simp: insert_conc)
  with Cons show ?case by (auto intro!: Expand_sym_ops_self)
qed

lemma Expand_sym_ops_Lang_of_Cons:
  assumes U: "U ∈ Expand_sym_ops P X x" and X: "Lhss Q ∩ X = {}"
  shows "Lang_of (P ∪ Q) (x#xs) = Lang_of_set (P ∪ Q) U @@ Lang_of (P ∪ Q) xs"
proof-
  { fix A assume "A ∈ X"
    with X have "A ∉ Lhss Q" by auto
    then have "Rhss (P ∪ Q) A = Rhss P A" by (auto simp: Rhss_Un notin_Lhss_iff_Rhss)
    with Lang_of_set_Rhss[of "P ∪ Q" A]
    have "Lang_of_set (P ∪ Q) (Rhss P A) = Lang (P ∪ Q) A" by auto
  } note * = this
  from assms
  show ?thesis
    by (auto simp: Expand_sym_ops_simps Lang_of_Cons * split: if_splits sym.splits)
qed

lemma Expand_syms_ops_Lang_of:
  assumes U: "U ∈ Expand_syms_ops P L α" and L: "Lhss Q ∩ L = {}"
  shows "Lang_of (P ∪ Q) α = Lang_of_set (P ∪ Q) U"
proof (insert U, induction α arbitrary: U)
  case Nil
  then show ?case by simp
next
  case (Cons x α)
  from Cons.prems obtain V W
    where U: "U = V @@ W"
      and V: "V ∈ Expand_sym_ops P L x"
      and W: "W ∈ Expand_syms_ops P L α"
    by auto
  show ?case by (simp add: U Cons.IH[OF W] Expand_sym_ops_Lang_of_Cons[OF V L] Lang_of_set_conc)
qed

definition Expand :: "(('n,'t) syms ⇒ ('n,'t) syms set) ⇒ ('n,'t) Prods ⇒ ('n,'t) Prods" where
"Expand f P = {(A,α') |A α'. ∃α. (A,α) ∈ P ∧ α' ∈ f α}"

lemma Expand_eq_UN[code]:
  "Expand f P = (⋃(A,α) ∈ P. Pair A ` f α)"
  by (auto simp: Expand_def)

lemma Expand_via_Rhss:
  "Expand f P = {(A,α). α ∈ ⋃(f ` Rhss P A)}"
  by (auto simp: Expand_def Rhss_def)

lemma Lhss_Expand: "Lhss (Expand f P) ⊆ Lhss P"
  by (auto simp: Lhss_def Expand_def split: prod.splits)

lemma Rhss_Expand: "Rhss (Expand f P) A = ⋃(f ` Rhss P A)"
  by (auto simp: Rhss_def Expand_def)

lemma Rhs_Nts_Expand: "Rhs_Nts (Expand f P) = (⋃(A,α) ∈ P. ⋃β ∈ f α. Nts_syms β)"
  by (auto simp: Expand_def Rhs_Nts_def)

text ‹When each production is expanded in an admissible way,
then the language is preserved.›

definition Expand_ops :: "('n,'t) Prods ⇒ 'n set ⇒ (('n,'t) syms ⇒ ('n,'t) syms set) set" where
"Expand_ops P X = {f. ∀α. f α ∈ Expand_syms_ops P X α}"

theorem Lang_Un_Expand:
  assumes f: "f ∈ Expand_ops P X" and X: "X ∩ Lhss Q = {}"
  shows "Lang (P ∪ Expand f Q) = Lang (P ∪ Q)"
  unfolding Lang_eq_iff_Lang_of_eq
proof (safe intro!: ext elim!: Lang_ofE_deriven)
  show "P ∪ Expand f Q ⊢ xs ⇒(n) map Tm w ⟹ w ∈ Lang_of (P ∪ Q) xs" for xs w n
  proof (induction n arbitrary: xs w rule: less_induct)
    case (less n)
    show ?case
    proof (cases "∃A. Nt A ∈ set xs")
      case False
      with less.prems have "xs = map Tm w"
        by (metis (no_types, lifting) deriven_from_TmsD destTm.cases ex_map_conv)
      then show ?thesis by (auto simp: Lang_of_map_Tm)
    next
      case True
      then obtain ys zs A where xs: "xs = ys @ Nt A # zs" by (metis split_list) 
      from less.prems[unfolded this deriven_Nt_map_Tm]
      obtain δ m l k v u t where Aδ: "(A,δ) ∈ P ∪ Expand f Q"
        and Lys: "P ∪ Expand f Q ⊢ ys ⇒(m) map Tm v"
        and Lδ: "P ∪ Expand f Q ⊢ δ ⇒(l) map Tm u"
        and Lzs: "P ∪ Expand f Q ⊢ zs ⇒(k) map Tm t"
        and n: "n = Suc (m + l + k)"
        and w: "w = v @ u @ t" by force
      from n have mn: "m < n" and ln: "l < n" and kn: "k < n" by auto
      with less.IH Lδ Lys Lzs
      have u: "u ∈ Lang_of (P ∪ Q) δ"
        and v: "v ∈ Lang_of (P ∪ Q) ys"
        and t: "t ∈ Lang_of (P ∪ Q) zs" by auto
      show ?thesis
      proof (cases "(A,δ) ∈ P")
        case True
        have "Lang_of (P ∪ Q) δ ⊆ Lang (P ∪ Q) A"
          apply (rule Lang_of_prod_subset)
          using True by simp
        with u v t
        show ?thesis by (auto simp: xs w Lang_of_append Lang_of_Nt_Cons)
      next
        case False
        with Aδ obtain α where AQ: "(A,α) ∈ Q" and δ: "δ ∈ f α" by (auto simp: Expand_def)
        from Lδ[unfolded δ] less.IH[of l] n
        have "u ∈ Lang_of (P ∪ Q) δ" by auto
        with δ have "u ∈ Lang_of_set (P ∪ Q) (f α)"
          by (auto simp: Lang_of_def)
        also have "… = Lang_of (P ∪ Q) α"
          apply (subst Expand_syms_ops_Lang_of)
          using f AQ X by (auto simp: Expand_ops_def)
        also have "… ⊆ Lang (P ∪ Q) A"
          apply (rule Lang_of_prod_subset)
          using AQ by auto
        finally have u: "u ∈ Lang (P ∪ Q) A" by auto
        with v t
        show ?thesis by (simp add: xs w Lang_of_append Lang_of_Nt_Cons)
      qed
    qed
  qed
next
  show "P ∪ Q ⊢ xs ⇒(n) map Tm w ⟹ w ∈ Lang_of (P ∪ Expand f Q) xs" for xs w n
  proof (induction n arbitrary: xs w rule: less_induct)
    case (less n)
    show ?case
    proof (cases "∃A. Nt A ∈ set xs")
      case False
      with less.prems have "xs = map Tm w"
        by (metis (no_types, lifting) deriven_from_TmsD destTm.cases ex_map_conv)
      then show ?thesis by (auto simp: Lang_of_map_Tm)
    next
      case True
      then obtain ys zs A where xs: "xs = ys @ Nt A # zs" by (metis split_list) 
      from less.prems[unfolded this deriven_Nt_map_Tm]
      obtain α m l k v u t where Aα: "(A,α) ∈ P ∪ Q"
        and Rys: "P ∪ Q ⊢ ys ⇒(m) map Tm v"
        and Rα: "P ∪ Q ⊢ α ⇒(l) map Tm u"
        and Rzs: "P ∪ Q ⊢ zs ⇒(k) map Tm t"
        and n: "n = Suc (m + l + k)"
        and w: "w = v @ u @ t" by force
      from n have mn: "m < n" and ln: "l < n" and kn: "k < n" by auto
      with Rα Rys Rzs
      have u: "u ∈ Lang_of (P ∪ Expand f Q) α"
        and v: "v ∈ Lang_of (P ∪ Expand f Q) ys"
        and t: "t ∈ Lang_of (P ∪ Expand f Q) zs" by (auto simp: less.IH)
      show ?thesis
      proof (cases "(A,α) ∈ P")
        case True
        then have "(A,α) ∈ P ∪ Expand f Q" by simp
        from Lang_of_prod_subset[OF this] u
        have "u ∈ Lang (P ∪ Expand f Q) A" by auto
        with v w t
        show ?thesis by (auto simp: xs w Lang_of_append Lang_of_Nt_Cons)
      next
        case False
        with Aα have AαQ: "(A,α) ∈ Q" by simp
        with f have fα: "f α ∈ Expand_syms_ops P X α" by (auto simp: Expand_ops_def)
        from X Lhss_Expand[of f Q]
        have Lhss: "Lhss (Expand f Q) ∩ X = {}" by auto
        from X AαQ have Rhss: "f α ⊆ Rhss (Expand f Q) A"
          by (auto simp: Rhss_def Expand_def)
        from u Expand_syms_ops_Lang_of[OF fα Lhss]
        have "u ∈ Lang_of_set (P ∪ Expand f Q) (f α)" by auto
        also have "… ⊆ Lang (P ∪ Expand f Q) A" using Rhss
          by (auto simp flip: Lang_of_set_Rhss simp: Rhss_Un)
        finally have "u ∈ …".
        with v t show ?thesis by (simp add: xs w Lang_of_append Lang_of_Nt_Cons)
      qed
    qed
  qed
qed

corollary Lang_Expand_Un:
  assumes "f ∈ Expand_ops P X" and "X ∩ Lhss Q = {}"
  shows "Lang (Expand f Q ∪ P) = Lang (Q ∪ P)"
  using Lang_Un_Expand[OF assms] by (simp add: ac_simps)

subsection ‹Instances›

text ‹For symbols, we just provide a function to expand it.›

definition Expand_sym :: "('n,'t) Prods ⇒ 'n set ⇒ ('n,'t) sym ⇒ ('n,'t) syms set" where
"Expand_sym P X x = (case x of Nt A ⇒ if A ∈ X then Rhss P A else {[x]} | _ ⇒ {[x]})"

lemma Expand_sym_ops: "Expand_sym P L x ∈ Expand_sym_ops P L x"
  by (auto simp: Expand_sym_def Expand_sym_ops_simps split: sym.splits)

subsubsection ‹Expanding all nonterminals›

fun Expand_all_syms :: "('n,'t) Prods ⇒ 'n set ⇒ ('n,'t) syms ⇒ ('n,'t) syms set" where
  "Expand_all_syms P X [] = {[]}"
| "Expand_all_syms P X (x#xs) = Expand_sym P X x @@ Expand_all_syms P X xs"

lemma Expand_all_syms_eq_foldr:
  "Expand_all_syms P X α = foldr (@@) (map (Expand_sym P X) α) {[]}"
  by (induction α, simp_all)

lemma Expand_all_syms_append:
  "Expand_all_syms P X (α@β) = Expand_all_syms P X α @@ Expand_all_syms P X β"
  by (induction α arbitrary: β, simp_all add: conc_assoc)

lemma Expand_all_syms_ops: "Expand_all_syms P X α ∈ Expand_syms_ops P X α"
  by (induction α, simp, force simp: Expand_sym_ops)

lemma Expand_all_ops: "Expand_all_syms P X ∈ Expand_ops P X"
  by (auto simp: Expand_ops_def Expand_all_syms_ops)

abbreviation Expand_all :: "('n,'t) Prods ⇒ 'n set ⇒ ('n,'t) Prods ⇒ ('n,'t) Prods" where
  "Expand_all P X Q ≡ Expand (Expand_all_syms P X) Q"

corollary Lang_Un_Expand_all:
  assumes "X ∩ Lhss Q = {}"
  shows "Lang (P ∪ Expand_all P X Q) = Lang (P ∪ Q)"
  using Lang_Un_Expand[OF Expand_all_ops assms].

corollary Lang_Expand_all_Un:
  assumes "X ∩ Lhss Q = {}"
  shows "Lang (Expand_all P X Q ∪ P) = Lang (Q ∪ P)"
  using Lang_Expand_Un[OF Expand_all_ops assms].

text ‹@{term Expand_all} removes expanded nonterminals and adds those which the
expanded nonterminals depends.›

lemma Expand_all_syms_eq_empty: "Expand_all_syms P X α = {} ⟷ ¬ Nts_syms α ∩ X ⊆ Lhss P"
  by (induction α)
    (auto simp: Expand_sym_def conc_eq_empty_iff notin_Lhss_iff_Rhss[symmetric] split: sym.splits)

lemma Nts_syms_Expand_all:
  "⋃(Nts_syms ` Expand_all_syms P X α) =
   (if Nts_syms α ∩ X ⊆ Lhss P
    then Nts_syms α - X ∪ ⋃(Nts_syms ` ⋃(Rhss P ` (Nts_syms α ∩ X)))
    else {})"
proof (induction α)
  case Nil
  show ?case by simp
next
  case (Cons x α)
  then show ?case
    by (auto simp: Expand_sym_def Nts_syms_conc Cons Expand_all_syms_eq_empty
        notin_Lhss_iff_Rhss[symmetric] split: sym.splits)
qed

lemma Rhs_Nts_Expand_all:
  "Rhs_Nts (Expand_all P X Q) =
   (⋃(A,α) ∈ Q. if Nts_syms α ∩ X ⊆ Lhss P
    then Nts_syms α - X ∪ ⋃(Nts_syms ` ⋃(Rhss P ` (Nts_syms α ∩ X)))
    else {})"
  apply (unfold Rhs_Nts_Expand)
  apply (rule SUP_cong[OF refl])
  apply (rule prod.case_cong[OF refl])
  by (rule Nts_syms_Expand_all)

lemma Rhs_Nts_Expand_all_le:
  "Rhs_Nts (Expand_all P X Q) ⊆ Rhs_Nts Q - X ∪ ⋃(Nts_syms ` ⋃(Rhss P ` (Rhs_Nts Q ∩ X)))"
  (is "?l ⊆ ?r")
proof-
  have "?l ⊆ (⋃(A,α) ∈ Q. Nts_syms α - X ∪ ⋃(Nts_syms ` ⋃(Rhss P ` (Nts_syms α ∩ X))))"
    apply (unfold Rhs_Nts_Expand_all)
    apply (rule SUP_mono')
    by (auto simp: if_splits)
  also have "… = ?r" by (auto simp: Rhs_Nts_def)
  finally show ?thesis.
qed

text ‹Approximately, ‹Expand_all› depends on nonterminals that are not expanded and
those that the expanding grammar depends.›

lemma Rhs_Nts_Expand_all_le_Rhs_Nts:
  "Rhs_Nts (Expand_all P X Q) ⊆ Rhs_Nts Q - X ∪ Rhs_Nts P"
  (is "?l ⊆ ?r")
proof-
  note Rhs_Nts_Expand_all_le
  also have "Rhs_Nts Q - X ∪ ⋃(Nts_syms ` ⋃(Rhss P ` (Rhs_Nts Q ∩ X))) ⊆ ?r"
    by (auto simp: Rhss_def Rhs_Nts_def)
  finally show ?thesis.
qed

text ‹One can remove a non-recursive part of grammar by expanding others
with respect to it.›

lemma Lang_Expand_all_idem:
  assumes PP: "Rhs_Nts P ∩ Lhss P = {}"
    and PQ: "Lhss P ∩ Lhss Q = {}" and AP: "A ∉ Lhss P"
  shows "Lang (Expand_all P (Lhss P) Q) A = Lang (P ∪ Q) A"
  (is "?l = ?r")
proof-
  have "?l = Lang (P ∪ Expand_all P (Lhss P) Q) A"
    apply (rule Lang_disj_Lhss_Un[symmetric])
    using Rhs_Nts_Expand_all_le_Rhs_Nts[of P "Lhss P" Q] PP AP by auto
  also have "… = Lang (P ∪ Q) A" by (simp add: Lang_Un_Expand_all[OF PQ])
  finally show ?thesis.
qed

lemma Lang_of_Expand_all_idem:
  assumes PP: "Rhs_Nts P ∩ Lhss P = {}" and PQ: "Lhss P ∩ Lhss Q = {}"
    and AP: "Nts_syms α ∩ Lhss P = {}"
  shows "Lang_of (Expand_all P (Lhss P) Q) α = Lang_of (P ∪ Q) α"
  apply (insert AP, induction α)
  using Lang_Expand_all_idem[OF PP PQ]
  by (simp_all split: sym.splits add: Lang_of_Cons)

lemma Lang_Expand_all_idem_new:
  assumes PP: "Rhs_Nts P ∩ Lhss P = {}" and PQ: "Lhss P ∩ Lhss Q = {}"
    and AP: "A ∈ Lhss P"
  shows "Lang_of_set (Expand_all P (Lhss P) Q) (Rhss P A) = Lang (P ∪ Q) A"
    (is "?l = ?r")
proof-
  have "α ∈ Rhss P A ⟹ Lang_of (Expand_all P (Lhss P) Q) α = Lang_of (P ∪ Q) α" for α
    apply (rule Lang_of_Expand_all_idem[OF PP PQ])
    using PP by (auto simp: Rhss_def Rhs_Nts_def)
  then have "?l = Lang_of_set (P ∪ Q) (Rhss P A)" by auto
  moreover have "Rhss P A = Rhss (P ∪ Q) A" using AP PQ by (auto simp: Rhss_def dest: in_LhssI)
  ultimately show ?thesis by (simp add: Lang_of_set_Rhss)
qed

lemma Lang_idem_Un_via_Expand_all:
  assumes PP: "Rhs_Nts P ∩ Lhss P = {}" and PQ: "Lhss P ∩ Lhss Q = {}"
  shows "Lang (P ∪ Q) A =
    (if A ∈ Lhss P then Lang_of_set (Expand_all P (Lhss P) Q) (Rhss P A)
     else Lang (Expand_all P (Lhss P) Q) A)"
  using Lang_Expand_all_idem[OF assms] Lang_Expand_all_idem_new[OF assms]
  by auto

corollary Lang_Un_idem_via_Expand_all:
  assumes PQ: "Lhss P ∩ Lhss Q = {}" and QQ: "Rhs_Nts Q ∩ Lhss Q = {}"
  shows "Lang (P ∪ Q) A =
    (if A ∈ Lhss Q then Lang_of_set (Expand_all Q (Lhss Q) P) (Rhss Q A)
     else Lang (Expand_all Q (Lhss Q) P) A)"
  using Lang_idem_Un_via_Expand_all[of Q P A] assms by (auto simp: ac_simps)

subsubsection ‹Expanding head nonterminals›

definition Expand_hd_syms :: "('n,'t) Prods ⇒ 'n set ⇒ ('n,'t) syms ⇒ ('n,'t) syms set" where
  "Expand_hd_syms P X α = (case α of [] ⇒ {[]} | x#xs ⇒ Expand_sym P X x @@ {xs})"

lemma Expand_hd_ops: "Expand_hd_syms P X ∈ Expand_ops P X"
  by (auto simp: Expand_hd_syms_def Expand_ops_def intro!: Expand_sym_ops Expand_syms_ops_self split: list.split)

abbreviation Expand_hd :: "('n,'t) Prods ⇒ 'n set ⇒ ('n,'t) Prods ⇒ ('n,'t) Prods" where
  "Expand_hd P X Q ≡ Expand (Expand_hd_syms P X) Q"

theorem Lang_Expand_hd:
  assumes "X ∩ Lhss Q = {}"
  shows "Lang (Expand_hd P X Q ∪ P) = Lang (Q ∪ P)"
  using Lang_Expand_Un[OF Expand_hd_ops assms].

end