Theory Inlining1Prod

(*
Authors: Kaan Taskin, Tobias Nipkow
*)

section ‹Inlining a Single Production›

theory Inlining1Prod
imports Context_Free_Grammar
begin

text 
‹A single production of ‹(A,α)› can be removed from ‹ps› by inlining
(= replacing ‹Nt A› by ‹α› everywhere in ‹ps›) without changing the language
if ‹Nt A ∉ set α› and ‹A ∉ lhss ps›.›

text
‹‹substP ps s u› replaces every occurrence of the symbol ‹s› with the list of symbols ‹u› on the right-hand sides of the production list ‹ps››

definition substP :: "('n, 't) sym ⇒  ('n, 't) syms ⇒ ('n, 't) prods ⇒ ('n, 't) prods" where
  "substP s u ps = map (λ(A,v). (A, substs s u v)) ps"

lemma substP_split: "substP s u (ps @ ps') = substP s u ps @ substP s u ps'"
  by (simp add: substP_def)

lemma substP_skip1: "s ∉ set v ⟹ substP s u ((A,v) # ps) = (A,v) # substP s u ps"
  by (auto simp add: substs_skip substP_def)

lemma substP_skip2: "s ∉ syms ps ⟹ substP s u ps = ps"
  by (induction ps) (auto simp add: substP_def substs_skip)

lemma substP_rev: "Nt B ∉ syms ps ⟹ substP (Nt B) [s] (substP s [Nt B] ps) = ps"
proof (induction ps)
  case Nil
  then show ?case
    by (simp add: substP_def)
next
  case (Cons a ps)
  let ?A = "fst a" let ?u = "snd a" let ?substs = "substs s [Nt B]"
  have "substP (Nt B) [s] (substP s [Nt B] (a # ps)) = substP (Nt B) [s] (map (λ(A,v). (A, ?substs v)) (a#ps))"
    by (simp add: substP_def)
  also have "... = substP (Nt B) [s] ((?A, ?substs ?u) # map (λ(A,v). (A, ?substs v)) ps)"
    by (simp add: case_prod_unfold)
  also have "... = map ((λ(A,v). (A, substsNt B [s] v))) ((?A, ?substs ?u) # map (λ(A,v). (A, ?substs v)) ps)"
    by (simp add: substP_def)
  also have "... = (?A, substsNt B [s] (?substs ?u)) # substP (Nt B) [s] (substP s [Nt B] ps)"
    by (simp add: substP_def)
  also from Cons have "... = (?A, substsNt B [s] (?substs ?u)) # ps"
    using set_subset_Cons unfolding Syms_def by auto
  also from Cons.prems have "... = (?A, ?u) # ps"
    using substs_rev unfolding Syms_def by force
  also have "... = a # ps" by simp
  finally show ?case .
qed

lemma substP_der:
  "(A,u) ∈ set (substP (Nt B) v ps) ⟹ set ((B,v) # ps) ⊢ [Nt A] ⇒* u"
proof -
  assume "(A,u) ∈ set (substP (Nt B) v ps)"
  then have "∃u'. (A,u') ∈ set ps ∧ u = substsNt B v u'" unfolding substP_def by auto
  then obtain u' where u'_def: "(A,u') ∈ set ps ∧ u = substsNt B v u'" by blast
  then have path1: "set ((B,v) # ps) ⊢ [Nt A] ⇒* u'"
    by (simp add: derive_singleton r_into_rtranclp)
  have "set ((B,v) # ps) ⊢ u' ⇒* substsNt B v u'"
    using substs_der by (metis list.set_intros(1))
  with u'_def have path2: "set ((B,v) # ps) ⊢ u' ⇒* u" by simp
  from path1 path2 show ?thesis by simp
qed

text‹A list of symbols ‹u› can be derived before inlining if ‹u› can be derived after inlining.›

lemma if_part:
  "set (substP (Nt B) v ps) ⊢ [Nt A] ⇒* u ⟹ set ((B,v) # ps) ⊢ [Nt A] ⇒* u"
proof (induction rule: derives_induct)
  case (step u A v w)
  then show ?case
    by (meson derives_append derives_prepend rtranclp_trans substP_der)
qed simp

text
‹For the other implication we need to take care that ‹B› can be derived in the original ‹ps›.
Thus, after inlining, ‹B› must also be substituted in the derived sentence ‹u›:›

lemma only_if_lemma:
assumes "A ≠ B"
    and "B ∉ lhss ps"
    and "Nt B ∉ set v"
shows "set ((B,v)#ps) ⊢ [Nt A] ⇒* u ⟹ set (substP (Nt B) v ps) ⊢ [Nt A] ⇒* substsNt B v u"
proof (induction rule: derives_induct)
  case base
  then show ?case using assms(1) by simp
next
  case (step s B' w v')
  then show ?case
  proof (cases "B = B'")
    case True
    then have "v = v'" 
      using ‹B ∉ lhss ps› step.hyps unfolding Lhss_def by auto
    then have "substsNt B v (s @ [Nt B'] @ w) = substsNt B v (s @ v' @ w)" 
      using step.prems ‹Nt B ∉ set v› True by (simp add: substs_skip)
    then show ?thesis
      using step.IH by argo
  next
    case False
    then have "(B',v') ∈ set ps"
      using step by auto
    then have "(B', substsNt B v v') ∈ set (substP (Nt B) v ps)"
      by (metis (no_types, lifting) list.set_map pair_imageI substP_def)
    from derives_rule[OF this _ rtranclp.rtrancl_refl] step.IH False show ?thesis
      by simp
  qed
qed

text
‹With the assumption that the non-terminal ‹B› is not in the list of symbols ‹u›, ‹substs u (Nt B) v› reduces to ‹u››

corollary only_if_part: 
assumes "A ≠ B"
    and "B ∉ lhss ps"
    and "Nt B ∉ set v"
    and "Nt B ∉ set u"
shows "set ((B,v)#ps) ⊢ [Nt A] ⇒* u ⟹ set (substP (Nt B) v ps) ⊢ [Nt A] ⇒* u"
by (metis assms substs_skip only_if_lemma)

text
‹Combining the two implications gives us the desired property of language preservation›

lemma derives_inlining: 
assumes "B ∉ lhss ps" and
        "Nt B ∉ set v" and
        "Nt B ∉ set u" and
        "A ≠ B"
shows "set (substP (Nt B) v ps) ⊢ [Nt A] ⇒* u ⟷ set ((B,v) # ps) ⊢ [Nt A] ⇒* u"
using assms if_part only_if_part by metis

end