Theory Unit_Elimination

(*
Author: August Martin Stimpfle
Based on HOL4 theories by Aditi Barthwal
*)

section ‹Elimination of Unit Productions›

theory Unit_Elimination
imports Context_Free_Grammar (*"HOL-Library.While_Combinator"*)
begin

definition Unit_prods :: "('n,'t) Prods ⇒ ('n,'t) Prods" where
"Unit_prods P = {(l,r) ∈ P. ∃A. r = [Nt A]}"

definition Unit_rtc :: "('n, 't) Prods ⇒ ('n × 'n) set" where
"Unit_rtc P = {(A,B). P ⊢ [Nt A] ⇒* [Nt B] ∧ {A,B} ⊆ Nts P}"

definition Unit_rm :: "('n, 't) Prods ⇒ ('n, 't) Prods" where
"Unit_rm P = P - Unit_prods P"

definition New_prods :: "('n, 't) Prods ⇒ ('n, 't) Prods" where 
"New_prods P = {(A,r). ∃B. (B,r) ∈ Unit_rm P ∧ (A, B) ∈ Unit_rtc (Unit_prods P)}"

definition Unit_elim :: "('n, 't) Prods ⇒ ('n, 't) Prods" where
"Unit_elim P = Unit_rm P ∪ New_prods P"

definition Unit_elim_rel :: "('n, 't) Prods ⇒ ('n, 't) Prods ⇒ bool" where
"Unit_elim_rel P P' ≡ P' = (Unit_rm P ∪ New_prods P)"

corollary Unit_elim_correct: "Unit_elim_rel P (Unit_elim P)"
by (metis Unit_elim_def Unit_elim_rel_def)

lemma Unit_free_if_Unit_elim_rel: "Unit_elim_rel P P' ⟹ Unit_free P'" 
unfolding Unit_elim_rel_def Unit_rm_def New_prods_def Unit_prods_def Unit_free_def by simp

corollary Unit_Free_Unit_elim: "Unit_free (Unit_elim P)"
by (simp add: Unit_elim_def Unit_elim_rel_def Unit_free_if_Unit_elim_rel)

lemma Unit_elim_rel_Eps_free:
  assumes "Eps_free P" and "Unit_elim_rel P P'"
  shows "Eps_free P'"
  using assms 
  unfolding Unit_elim_rel_def Eps_free_def Unit_rm_def Unit_prods_def New_prods_def by auto

lemma Tms_Unit_elim_subset: "Tms (Unit_elim P) ⊆ Tms P"
unfolding Unit_elim_def Unit_rm_def New_prods_def Tms_def by(auto)

subsection ‹Code on lists›

definition unit_prods :: "('n,'t) prods ⇒ ('n,'t) prods" where
"unit_prods ps = [(l,[Nt A]). (l,[Nt A]) ← ps]"

definition unit_pairs :: "('n,'t) prods ⇒ ('n × 'n) list" where
"unit_pairs ps = [(A,B). (A,[Nt B]) ← ps]"

definition unit_rm :: "('n, 't) prods ⇒ ('n, 't) prods" where
"unit_rm ps = minus_list_set ps (unit_prods ps)"

definition new_prods :: "('n, 't) prods ⇒ ('n, 't) prods" where
"new_prods ps = [(A,r). (B,r) ← unit_rm ps, (A,B') ← trancl_list(unit_pairs ps), B'=B]"

definition unit_elim :: "('n, 't) prods ⇒ ('n, 't) prods" where
"unit_elim ps = unit_rm ps @ new_prods ps"

lemma set_unit_prods: "set (unit_prods ps) = Unit_prods (set ps)"
unfolding unit_prods_def Unit_prods_def
by auto

lemma set_unit_rm: "set (unit_rm ps) = Unit_rm (set ps)"
unfolding unit_rm_def Unit_rm_def set_minus_list_set set_unit_prods ..

lemma Unit_prods_unit_pairs[code]:
  "Unit_prods (set ps) = set(map (λ(A,B). (A,[Nt B])) (unit_pairs ps))"
unfolding Unit_prods_def unit_pairs_def by (auto)

lemma Unit_prods_iff_unit_pairs:
  "Unit_prods (set ps) ⊢ [Nt A] ⇒ [Nt B] ⟷ (A, B) ∈ set(unit_pairs ps)"
unfolding unit_pairs_def Unit_prods_def by(auto simp add: derive_singleton)

lemma Nts_Unit_prods: "(A, B) ∈ set(unit_pairs ps)
  ⟹ A ∈ Lhss (Unit_prods (set ps)) ∧ B ∈ Rhs_Nts (Unit_prods(set ps))"
apply(auto simp: Unit_prods_unit_pairs image_def Nts_Lhss_Rhs_Nts Lhss_def Rhs_Nts_def
           split: prod.splits)
 apply blast
by force

lemma rtc_Unit_prods_if_tc_unit_pairs:
  "(A,B) ∈ set(trancl_list(unit_pairs ps)) ⟹ (A,B) ∈ Unit_rtc (Unit_prods (set ps))"
unfolding set_trancl_list
proof(induction rule: converse_trancl_induct)
  case (base A)
  then show ?case unfolding Unit_rtc_def
  by (auto simp add: r_into_rtranclp Unit_prods_iff_unit_pairs Nts_Unit_prods Nts_Lhss_Rhs_Nts)
next
  case (step A A')
  then show ?case unfolding Unit_rtc_def
    by (auto simp add: Nts_Lhss_Rhs_Nts Nts_Unit_prods
        intro: converse_rtranclp_into_rtranclp[of "derive (Unit_prods(set ps))"]
               Unit_prods_iff_unit_pairs[THEN iffD2])
qed

lemma tc_unit_pairs_if_rtc_Unit_prods:
  fixes ps :: "('n,'t)prods"
  assumes "(A,B) ∈ Unit_rtc (Unit_prods(set ps))"
  shows "A=B ∨ (A,B) ∈ set(trancl_list(unit_pairs ps))"
proof -
  have *: "Unit_prods(set ps) ⊢ [Nt B] ⇒* [Nt A] ⟹ B=A ∨ (B,A) ∈ (set(unit_pairs ps))^+" for A B
  proof(induction "[Nt B]::('n,'t)syms" arbitrary: B rule: converse_rtranclp_induct)
    case base thus ?case by simp
  next
    case (step α C)
    from step.hyps(1) obtain C' where "(C,C') ∈ set(unit_pairs ps)" "α = [Nt C']"
      by (auto simp: derive_singleton Unit_prods_def unit_pairs_def)
    with step.hyps(2-)
    show ?case
      by (metis trancl.r_into_trancl trancl_into_trancl2)
  qed
  with assms show ?thesis
    by (simp add: set_trancl_list Unit_rtc_def)
qed

lemma Unit_rm_Un_New_prods_eq: "Unit_rm (set ps) ∪ New_prods (set ps) = Unit_rm (set ps) ∪
  {(A,r). ∃B. (B,r) ∈ Unit_rm (set ps) ∧ (A, B) ∈ set(trancl_list(unit_pairs ps))}"
unfolding New_prods_def Unit_rm_def
by(auto intro: rtc_Unit_prods_if_tc_unit_pairs dest: tc_unit_pairs_if_rtc_Unit_prods)

lemma Unit_elim_set_code[code]: "Unit_elim (set ps) = set(unit_elim ps)"
unfolding unit_elim_def Unit_elim_def Unit_rm_Un_New_prods_eq
by(auto simp add: set_unit_rm new_prods_def)

corollary unit_elim_correct: "Unit_elim_rel (set ps) (set(unit_elim ps))"
by (metis Unit_elim_set_code Unit_elim_correct)


(* Test for executability only *)
lemma "Unit_elim {(0::int, [Nt 1]), (1, [Tm(2::int)])} = {(0, [Tm 2]), (1, [Tm 2])}"
by eval


subsection ‹Finiteness and Existence›

lemma finiteUnit_prods: "finite P ⟹ finite (Unit_prods P)"
unfolding Unit_prods_def
by (metis (no_types, lifting) case_prodE finite_subset mem_Collect_eq subsetI)

(* finiteness for Unit_rtc *)
definition NtsCross :: "('n, 't) Prods  ⇒ ('n × 'n) set" where
"NtsCross P = Nts P × Nts P"

lemma finite_Unit_rtc: 
  assumes "finite P"
  shows  "finite (Unit_rtc P)"
proof -
  have "finite (Nts P)"
    unfolding Nts_def using assms finite_Nts_syms by auto
  hence "finite (NtsCross P)"
    unfolding NtsCross_def by auto
  moreover have "Unit_rtc P ⊆ NtsCross P"
    unfolding Unit_rtc_def NtsCross_def by blast
  ultimately show ?thesis
    using assms infinite_super by fastforce 
qed

(* finiteness for New_prods *)
definition nPSlambda :: "('n, 't) Prods ⇒ ('n × 'n) ⇒ ('n, 't) Prods" where
"nPSlambda P d = {fst d} × {r. (snd d, r) ∈ P}"

lemma npsImage: "⋃((nPSlambda (Unit_rm P)) ` (Unit_rtc (Unit_prods P))) = New_prods P"
  unfolding New_prods_def nPSlambda_def by fastforce

lemma finite_nPSlambda:
  assumes "finite P" 
  shows "finite (nPSlambda P d)"
proof -
  have "{(B, r). (B, r) ∈ P ∧ B = snd d} ⊆ P" 
    by blast
  hence "finite {(B, r). (B, r) ∈ P ∧ B = snd d}"
    using assms finite_subset by blast
  hence "finite (snd ` {(B, r). (B, r) ∈ P ∧ B = snd d})" 
    by simp
  moreover have "{r. (snd d, r) ∈ P} = (snd ` {(B, r). (B, r) ∈ P ∧ B = snd d})"
    by force
  ultimately show ?thesis
    using assms unfolding nPSlambda_def by simp
qed

lemma finite_Unit_rm: "finite P ⟹ finite (Unit_rm P)"
unfolding Unit_rm_def by simp

lemma finite_New_prods: assumes "finite P" shows "finite (New_prods P)"
proof -
  have "finite (Unit_rtc (Unit_prods P))"
    using finiteUnit_prods finite_Unit_rtc assms by blast
  then show ?thesis
    using assms finite_Unit_rm npsImage finite_nPSlambda finite_UN by metis
qed

lemma finiteUnit_elim_relRules: "finite P ⟹ finite (Unit_rm P ∪ New_prods P)"
by (simp add: finite_New_prods finite_Unit_rm)

lemma Unit_elim_rel_exists: "finite P ⟹ ∃P'. Unit_elim_rel P P' ∧ finite P'"
unfolding Unit_elim_rel_def using finite_list[OF finiteUnit_elim_relRules] by blast

(* towards theorem 4.4 *)

lemma inNonUnitProds:
  "p ∈ Unit_rm P ⟹ p ∈ P"
  unfolding Unit_rm_def by blast

lemma psubDeriv:
  assumes "P ⊢ u ⇒ v"
    and "∀p ∈ P. p ∈ P'"
  shows "P' ⊢ u ⇒ v"
  using assms by (meson derive_iff)

lemma psubRtcDeriv:
  assumes "P ⊢ u ⇒* v"
    and "∀p ∈ P. p ∈ P'"
  shows "P' ⊢ u ⇒* v"
  using assms by (induction rule: rtranclp.induct) (auto simp: psubDeriv rtranclp.rtrancl_into_rtrancl)

lemma Unit_prods_deriv: 
  assumes "Unit_prods P ⊢ u ⇒* v"
  shows "P ⊢ u ⇒* v"
proof -
  have "∀p ∈ Unit_prods P. p ∈ P"
    unfolding Unit_prods_def by blast
  thus ?thesis 
    using assms psubRtcDeriv by blast
qed

lemma Unit_elim_rel_r3:
  assumes "Unit_elim_rel P P'" and "P' ⊢ u ⇒ v"
  shows "P ⊢ u ⇒* v"
proof -
  obtain A α r1 r2 where A: "(A, α) ∈ P' ∧ u = r1 @ [Nt A] @ r2 ∧ v = r1 @ α @ r2"
    using assms derive.cases by meson
  hence "(A, α) ∈ Unit_rm P ∨ (A, α) ∈ New_prods P"
    using assms(1) unfolding Unit_elim_rel_def by simp
  thus ?thesis
  proof
    assume "(A, α) ∈ Unit_rm P"
    hence "(A, α) ∈ P"
      using inNonUnitProds by blast
    hence "P ⊢ r1 @ [Nt A] @ r2 ⇒ r1 @ α @ r2"
      by (auto simp: derive.simps)
    thus ?thesis using A by simp
  next 
    assume "(A, α) ∈ New_prods P"
    from this obtain B where B: "(B, α) ∈ Unit_rm P ∧ (A, B) ∈ Unit_rtc (Unit_prods P)"
      unfolding New_prods_def by blast
    hence "Unit_prods P ⊢ [Nt A] ⇒* [Nt B]"
      unfolding Unit_rtc_def by simp
    hence "P ⊢ [Nt A] ⇒* [Nt B]"
      using Unit_prods_deriv by blast
    hence 1: "P ⊢ r1 @ [Nt A] @ r2 ⇒* r1 @ [Nt B] @ r2"
      using derives_append derives_prepend by blast
    have "(B, α) ∈ P"
      using B inNonUnitProds by blast
    hence "P ⊢ r1 @ [Nt B] @ r2 ⇒ r1 @ α @ r2"
      by (auto simp: derive.simps)
    thus ?thesis 
      using 1 A by simp
  qed
qed

lemma Unit_elim_rel_r4: 
  assumes "P' ⊢ u ⇒* v"
    and "Unit_elim_rel P P'"
  shows "P ⊢ u ⇒* v"
  using assms by (induction rule: rtranclp.induct) (auto simp: Unit_elim_rel_r3 rtranclp_trans)

lemma deriv_Unit_rtc:
  assumes "P ⊢ [Nt A] ⇒ [Nt B]"
  shows "(A, B) ∈ Unit_rtc (Unit_prods P)"
proof -
  have "(A, [Nt B]) ∈ P"
    using assms by (simp add: derive_singleton)
  hence "(A, [Nt B]) ∈ Unit_prods P"
    unfolding Unit_prods_def by blast
  hence "Unit_prods P ⊢ [Nt A] ⇒ [Nt B]"
    by (simp add: derive_singleton)
  moreover have "B ∈ Nts (Unit_prods P) ∧ A ∈ Nts (Unit_prods P)"
    using ‹(A, [Nt B]) ∈ Unit_prods P› Nts_def Nts_syms_def by fastforce
  ultimately show ?thesis
    unfolding Unit_rtc_def by blast
qed

lemma Unit_elim_rel_r12: 
  assumes "Unit_elim_rel P P'" "(A, α) ∈ P'"
  shows "(A, α) ∉ Unit_prods P"
  using assms unfolding Unit_elim_rel_def Unit_rm_def Unit_prods_def New_prods_def by blast

lemma Unit_elim_rel_r14: 
  assumes "Unit_elim_rel P P'" 
    and "P ⊢ [Nt A] ⇒ [Nt B]" "P' ⊢ [Nt B] ⇒ v"
  shows "P' ⊢ [Nt A] ⇒ v"
proof -
  have 1: "(A, B) ∈ Unit_rtc (Unit_prods P)"
    using deriv_Unit_rtc assms(2) by fast
  have 2: "(B, v) ∈ P'"
    using assms(3) by (simp add: derive_singleton)
  thus ?thesis
  proof (cases "(B, v) ∈ P")
    case True
    hence "(B, v) ∈ Unit_rm P"
      unfolding Unit_rm_def using assms(1) assms(3) Unit_elim_rel_r12[of P P' B v] by (simp add: derive_singleton)
    then show ?thesis
    using 1 assms(1) unfolding Unit_elim_rel_def New_prods_def derive_singleton by blast
  next
    case False
    hence "(B, v) ∈ New_prods P"
      using assms(1) 2 unfolding Unit_rm_def Unit_elim_rel_def  by simp
    from this obtain C where C: "(C, v) ∈ Unit_rm P ∧ (B, C) ∈ Unit_rtc (Unit_prods P)"
      unfolding New_prods_def by blast
    hence "Unit_prods P ⊢ [Nt A] ⇒* [Nt C]"
      using 1 unfolding Unit_rtc_def by auto
    hence "(A, C) ∈ Unit_rtc (Unit_prods P)"
      unfolding Unit_rtc_def using 1 C Unit_rtc_def by fastforce
    hence "(A, v) ∈ New_prods P"
      unfolding New_prods_def using C by blast
    hence "(A, v) ∈ P'"
      using assms(1) unfolding Unit_elim_rel_def  by blast
    thus ?thesis by (simp add: derive_singleton)
  qed
qed

lemma Unit_elim_rel_r20_aux:
  assumes "P ⊢ l @ [Nt A] @ r ⇒* map Tm v" 
  shows "∃α. P ⊢ l @ [Nt A] @ r ⇒ l @ α @ r ∧ P ⊢ l @ α @ r ⇒* map Tm v ∧ (A, α) ∈ P"
proof -
  obtain l' w r' where w: "P ⊢ l ⇒* l'  ∧ P ⊢ [Nt A] ⇒* w ∧  P ⊢ r ⇒* r' ∧ map Tm v = l' @ w @ r'"
    using assms(1) by (metis derives_append_decomp)
  have "Nt A ∉ set (map Tm v)" 
    using assms(1) by auto
  hence "[Nt A] ≠ w" 
    using w by auto
  from this obtain α where α: "P ⊢ [Nt A] ⇒ α ∧ P ⊢ α ⇒* w"
    by (metis w converse_rtranclpE)
  hence "(A, α) ∈ P" 
    by (simp add: derive_singleton)
  thus ?thesis by (metis α w derive.intros derives_append_decomp) 
qed

lemma Unit_elim_rel_r20: 
  assumes "P ⊢ u ⇒* map Tm v" "Unit_elim_rel P P'"
  shows "P' ⊢ u ⇒* map Tm v"
  using assms proof (induction rule: converse_derives_induct)
  case base
  then show ?case by blast
next
  case (step l A r w)
  then show ?case 
  proof (cases "(A, w) ∈ Unit_prods P")
    case True
    from this obtain B where "w = [Nt B]"
      unfolding Unit_prods_def by blast
    have "P' ⊢ l @ w @ r ⇒* map Tm v ∧ Nt B ∉ set (map Tm v)"
      using step.IH assms(2) by auto
    obtain α where α: "P' ⊢ l @ [Nt B] @ r ⇒ l @ α @ r ∧ P' ⊢ l @ α @ r ⇒* map Tm v ∧ (B, α) ∈ P'"
      using assms(2) step.IH ‹w=_›  Unit_elim_rel_r20_aux[of P' l B r v] by blast
    hence "(A, α) ∈ P'"
      using assms(2) step.hyps(2) ‹w=_› Unit_elim_rel_r14[of P P' A B α] by (simp add: derive_singleton)
    hence "P' ⊢ l @ [Nt A] @ r ⇒* l @ α @ r"
      using derive.simps by fastforce
    then show ?thesis 
      using α by auto
  next
    case False
    hence "(A, w) ∈ Unit_rm P"
      unfolding Unit_rm_def using step.hyps(2) by blast
    hence "(A, w) ∈ P'"
      using assms(2) unfolding Unit_elim_rel_def  by simp
    hence "P' ⊢ l @ [Nt A] @ r ⇒ l @ w @ r"
      by (auto simp: derive.simps)
    then show ?thesis
      using step by simp
  qed
qed

theorem Unit_elim_rel_Lang_eq: "Unit_elim_rel P P' ⟹ Lang P' S = Lang P S"
  unfolding Lang_def using Unit_elim_rel_r4 Unit_elim_rel_r20 by blast

corollary Lang_Unit_elim: "Lang (Unit_elim P) A = Lang P A"
by (simp add: Unit_elim_def Unit_elim_rel_Lang_eq Unit_elim_rel_def)

corollary lang_unit_elim: "lang (unit_elim ps) A = lang ps A"
by (metis unit_elim_correct Unit_elim_rel_Lang_eq)

end