Theory Renaming_CFG

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

section ‹Renaming Nonterminals›

theory Renaming_CFG
imports Context_Free_Grammar
begin

text ‹This theory provides lemmas that relate derivations w.r.t. some set of productions ‹P›
to derivations w.r.t. a renaming of the nonterminals in ‹P›.›

fun rename_sym :: "('old ⇒ 'new) ⇒ ('old,'t) sym ⇒ ('new,'t) sym" where
"rename_sym f (Nt n) = Nt (f n)" |
"rename_sym f (Tm t) = Tm t"

abbreviation "rename_syms f ≡ map (rename_sym f)"

fun rename_prod :: "('old ⇒ 'new) ⇒ ('old,'t) prod ⇒ ('new,'t) prod" where
"rename_prod f (A,w) = (f A, rename_syms f w)"

abbreviation "rename_Prods f P ≡ rename_prod f ` P"

lemma rename_sym_o_Tm[simp]: "rename_sym f ∘ Tm = Tm"
by(rule ext) simp

lemma Nt_notin_rename_syms_if_notin_range:
  "x ∉ range f ⟹ Nt x ∉ set (rename_syms f w)"
by(auto elim!: rename_sym.elims[OF sym])

lemma in_Nts_rename_Prods: "B ∈ Nts (rename_Prods f P) = (∃A ∈ Nts P. f A = B)"
unfolding Nts_def nts_syms_def by(force split: prod.splits elim!: rename_sym.elims[OF sym])

lemma rename_preserves_deriven:
   "P ⊢ α ⇒(n) β ⟹ rename_Prods f P ⊢ rename_syms f α ⇒(n) rename_syms f β"
proof (induction rule: deriven_induct)
  case 0
  then show ?case by simp
next
  let ?F = "rename_syms f"
  case (Suc n u A v w)
  then have "(f A, rename_syms f w) ∈ rename_Prods f P"
    by (metis image_eqI rename_prod.simps) 
  from derive.intros[OF this] have "rename_Prods f P ⊢ ?F u @ ?F [Nt A] @ ?F v ⇒ ?F u @ ?F w @ ?F v"
    by auto
  with Suc show ?case
    by (simp add: relpowp_Suc_I)
qed

lemma rename_preserves_derives:
   "P ⊢ α ⇒* β ⟹ rename_Prods f P ⊢ rename_syms f α ⇒* rename_syms f β"
by (meson rename_preserves_deriven rtranclp_power)

lemma rename_preserves_derivel:
  assumes "P ⊢ α ⇒l β"
  shows "rename_Prods f P ⊢ rename_syms f α ⇒l rename_syms f β"
proof -
  from assms obtain A w u1 u2
    where A_w_u1_u2: "(A,w) ∈ P ∧ α = map Tm u1 @ Nt A # u2 ∧ β = map Tm u1 @ w @ u2"
    unfolding derivel_iff by fast
  then have "(f A, rename_syms f w) ∈ (rename_Prods f P) ∧ 
             rename_syms f α = map Tm u1 @ Nt (f A) # rename_syms f u2 ∧
             rename_syms f β = map Tm u1 @ rename_syms f w @ rename_syms f u2"
    by force
  then have "∃ (A,w) ∈ rename_Prods f P.
        ∃u1 u2. rename_syms f α = map Tm u1 @ Nt A # u2 ∧ rename_syms f β = map Tm u1 @ w @ u2"
    by blast
  then show ?thesis by (simp only: derivel_iff)
qed

lemma rename_preserves_deriveln:
  "P ⊢ α ⇒l(n) β ⟹ rename_Prods f P ⊢ rename_syms f α ⇒l(n) rename_syms f β"
proof (induction n arbitrary: β)
  case 0
  then show ?case by simp
next
  case Suc then show ?case
    by (metis relpowp_Suc_E relpowp_Suc_I rename_preserves_derivel)
qed

lemma rename_preserves_derivels:
  "P ⊢ α ⇒l* β ⟹ rename_Prods f P ⊢ rename_syms f α ⇒l* rename_syms f β"
by (meson rename_preserves_deriveln rtranclp_power)

lemma rename_deriven_iff_inj:
fixes P :: "('a,'t)Prods"
assumes "inj_on f (Nts P ∪ nts_syms α ∪ nts_syms β)"
shows "rename_Prods f P ⊢ rename_syms f α ⇒(n) rename_syms f β ⟷ P ⊢ α ⇒(n) β" (is "?l ⟷ ?r")
proof
  show "?r ⟹ ?l" by (rule rename_preserves_deriven)
next
  (* since f is injective, the second direction follows from the first by using the inverse *)
  let ?M = "Nts P ∪ nts_syms α ∪ nts_syms β"
  obtain "g" where "g = the_inv_into ?M f" and inv: "(⋀x. x ∈ ?M ⟹ (g (f x) = x))"
    using assms by (simp add: the_inv_into_f_f inj_on_Un)
  then have "s ∈ Syms P ∪ set α ∪ set β ⟹ rename_sym g (rename_sym f s) = s" for s::"('a,'t) sym"
    by (cases s) (auto simp: Nts_def Syms_def nts_syms_def)
  then have inv_rename_syms: "⋀(ss::('a,'t) syms). set ss ⊆ Syms P ∪ set α ∪ set β ⟹ rename_syms g (rename_syms f ss) = ss"
    by (simp add: list.map_ident_strong subset_iff)
  with inv have "p ∈ P ⟹ rename_prod g (rename_prod f p) = p" for p::"('a,'t) prod"
    by(cases p)(auto simp: Nts_def Syms_def)
  then have inv_rename_prods: "rename_Prods g (rename_Prods f P) = P"
    using image_iff by fastforce
  then show "?l ⟹ ?r"
    using rename_preserves_deriven inv_rename_syms by (metis Un_upper2 le_supI1)
qed

lemma rename_derives_iff_inj:
  assumes "inj_on f (Nts P ∪ nts_syms α ∪ nts_syms β)"
  shows "rename_Prods f P ⊢ rename_syms f α ⇒* rename_syms f β ⟷ P ⊢ α ⇒* β"
by (meson assms relpowp_imp_rtranclp rename_deriven_iff_inj rtranclp_imp_relpowp)

lemma rename_deriveln_iff_inj:
fixes P :: "('a,'t)Prods"
assumes "inj_on f (Nts P ∪ nts_syms α ∪ nts_syms β)"
shows "rename_Prods f P ⊢ rename_syms f α ⇒l(n) rename_syms f β ⟷ P ⊢ α ⇒l(n) β" (is "?l ⟷ ?r")
proof
  show "?r ⟹ ?l" by (rule rename_preserves_deriveln)
next
  let ?M = "Nts P ∪ nts_syms α ∪ nts_syms β"
  obtain "g" where "g = the_inv_into ?M f" and inv: "(⋀x. x ∈ ?M ⟹ (g (f x) = x))"
    using assms by (simp add: the_inv_into_f_f inj_on_Un)
  then have "s ∈ Syms P ∪ set α ∪ set β ⟹ rename_sym g (rename_sym f s) = s" for s::"('a,'t) sym"
    by (cases s) (auto simp: Nts_def Syms_def nts_syms_def)
  then have inv_rename_syms: "⋀(ss::('a,'t) syms). set ss ⊆ Syms P ∪ set α ∪ set β ⟹ rename_syms g (rename_syms f ss) = ss"
    by (simp add: list.map_ident_strong subset_iff)
  with inv have "p ∈ P ⟹ rename_prod g (rename_prod f p) = p" for p::"('a,'t) prod"
    by(cases p)(auto simp: Nts_def Syms_def)
  then have inv_rename_prods: "rename_Prods g (rename_Prods f P) = P"
    using image_iff by fastforce
  then show "?l ⟹ ?r"
    using rename_preserves_deriveln inv_rename_syms by (metis Un_upper2 le_supI1)
qed

lemma rename_derivels_iff_inj:
  assumes "inj_on f (Nts P ∪ nts_syms α ∪ nts_syms β)"
  shows "rename_Prods f P ⊢ rename_syms f α ⇒l* rename_syms f β ⟷ P ⊢ α ⇒l* β"
by (meson assms relpowp_imp_rtranclp rename_deriveln_iff_inj rtranclp_imp_relpowp)

lemma Lang_rename_Prods:
  assumes "inj_on f (Nts P ∪ {S})"
  shows "Lang (rename_Prods f P) (f S) = Lang P S"
proof -
  from assms rename_derives_iff_inj[of f P "[Nt S]" "map Tm _"]
  show ?thesis unfolding Lang_def by (simp)
qed

lemma derives_preserves_renaming:
  assumes "rename_Prods f P ⊢ rename_syms f u ⇒* fv"
  shows "∃v. fv = rename_syms f v"
  using assms
proof(induction rule: derives_induct)
  case base
  then show ?case by auto
next
  case (step u A v w)
  then obtain A' where A'_src: "rename_syms f [Nt A'] = [Nt A]" by auto
  from step obtain drvW where "rename_syms f drvW = u @ [Nt A] @ v" by auto
  then have uAv_split: "u @ rename_syms f [Nt A'] @ v = rename_syms f drvW" using A'_src by simp
  from uAv_split obtain u' where u'_src: "rename_syms f u' = u" by (metis map_eq_append_conv)
  from uAv_split obtain v' where v'_src: "rename_syms f v' = v" by (metis map_eq_append_conv)
  from step obtain w' where "rename_syms f w' = w" by auto
  then have "u @ w @ v = rename_syms f (u' @ w' @ v')" using u'_src v'_src by auto
  then show ?case by fast
qed

end