Theory Unit_Elimination

(*
Author: August Martin Stimpfle; Tobias Nipkow (simplification)
Based on HOL4 theories by Aditi Barthwal
*)

section ‹Elimination of Unit Productions›

theory Unit_Elimination
imports Context_Free_Grammar
begin

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

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

definition Unit_elim :: "('n, 't) Prods ⇒ ('n, 't) Prods" where 
"Unit_elim P = {(A,r). ∃B. Unit_prods P ⊢ [Nt A] ⇒* [Nt B] ∧ (B,r) ∈ Unit_rm P}"

lemma Unit_Free_Unit_elim: "Unit_free (Unit_elim P)" 
unfolding Unit_elim_def Unit_rm_def Unit_prods_def Unit_free_def by simp

lemma Unit_elim_Eps_free:
  assumes "Eps_free P"
  shows "Eps_free (Unit_elim P)"
  using assms 
  unfolding Unit_elim_def Eps_free_def Unit_rm_def Unit_prods_def by auto

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

lemma derives_Unit_in_Nts: "⟦ P ⊢ [Nt A] ⇒* [Nt B]; A ∈ Nts P ⟧ ⟹ B ∈ Nts P"
by (meson in_Nts_iff_if_derives list.set_intros(1) reachable_def)

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 unit_elim :: "('n, 't) prods ⇒ ('n, 't) prods" where
"unit_elim ps = [(A,r). (B,r) ← unit_rm ps, (A,B') ← (B,B)#trancl_list(unit_pairs ps), B'=B]"

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 (set ps) ∧ B ∈ Rhs_Nts (set ps)"
apply(auto simp: image_def Nts_Lhss_Rhs_Nts Lhss_def Rhs_Nts_def unit_pairs_def Bex_def
           split: prod.splits)
  apply blast
by force

lemma rtc_Unit_prods_if_tc_unit_pairs:
  "(A,B) ∈ (set(unit_pairs ps))^+ ⟹ Unit_prods (set ps) ⊢ [Nt A] ⇒* [Nt B]"
proof(induction rule: converse_trancl_induct)
  case (base A)
  then show ?case
  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
    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 "Unit_prods (set ps) ⊢ [Nt A] ⇒* [Nt B]"
  shows "A=B ∨ (A,B) ∈ (set(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)
qed

lemma Unit_elim_set[code]: "Unit_elim (set ps) = set (unit_elim ps)"
unfolding Unit_elim_def unit_elim_def
by (auto simp: set_unit_rm Unit_rm_def set_trancl_list tc_unit_pairs_if_rtc_Unit_prods
  intro: rtc_Unit_prods_if_tc_unit_pairs)

(* 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 finite_Unit_elim: "finite P ⟹ finite (Unit_elim P)"
by (metis List.finite_set Unit_elim_set finite_list)

lemma Unit_prods_subset: "Unit_prods P ⊆ P"
  unfolding Unit_prods_def by auto

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

lemma Unit_elim_rel_r3:
  assumes "Unit_elim P ⊢ u ⇒ v"
  shows "P ⊢ u ⇒* v"
proof -
  obtain A α r1 r2 where A: "(A, α) ∈ Unit_elim P ∧ u = r1 @ [Nt A] @ r2 ∧ v = r1 @ α @ r2"
    using assms derive.cases by meson
  hence "(A, α) ∈ Unit_elim P"
    using assms(1) unfolding Unit_elim_def by simp
  from this obtain B where B: "(B, α) ∈ Unit_rm P ∧ Unit_prods P ⊢ [Nt A] ⇒* [Nt B]"
    unfolding Unit_elim_def by blast
  hence "P ⊢ [Nt A] ⇒* [Nt B]"
    using  Unit_prods_subset derives_mono 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

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

lemma Unit_elim_rel_r14:
  assumes "P ⊢ [Nt A] ⇒ [Nt B]" "Unit_elim P ⊢ [Nt B] ⇒ v"
  shows "Unit_elim P ⊢ [Nt A] ⇒ v"
proof -
  have 1: "Unit_prods P ⊢ [Nt A] ⇒* [Nt B]" using assms(1)
    by(auto simp: Unit_prods_def derive_singleton)
  have 2: "(B, v) ∈ Unit_elim P"
    using assms(2) by (simp add: derive_singleton)
  thus ?thesis
  proof (cases "(B, v) ∈ P")
    case True
    hence "(B, v) ∈ Unit_rm P"
      using 2 unfolding Unit_rm_def Unit_elim_def Unit_prods_def by blast
    then show ?thesis
    using 1 by (auto simp: Unit_elim_def derive_singleton)
  next
    case False
    hence "(B, v) ∈ Unit_elim P"
      using assms(1) 2 unfolding Unit_rm_def Unit_elim_def  by simp
    from this obtain C where C: "(C, v) ∈ Unit_rm P ∧ Unit_prods P ⊢ [Nt B] ⇒* [Nt C]"
      unfolding Unit_elim_def by blast
    hence "Unit_prods P ⊢ [Nt A] ⇒* [Nt C]"
      using 1 by auto
    hence "(A, v) ∈ Unit_elim P"
      unfolding Unit_elim_def using C by blast
    hence "(A, v) ∈ Unit_elim P"
      using assms(1) unfolding Unit_elim_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_appendD)
  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_appendD) 
qed

lemma Unit_elim_rel_complete: 
  assumes "P ⊢ u ⇒* map Tm v"
  shows "Unit_elim 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)
  let ?P = "Unit_elim P"
  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 by auto
    obtain α where α: "?P ⊢ l @ [Nt B] @ r ⇒ l @ α @ r ∧ ?P ⊢ l @ α @ r ⇒* map Tm v ∧ (B, α) ∈ ?P"
      using step.IH ‹w=_›  Unit_elim_rel_r20_aux[of ?P l B r v] by blast
    hence "(A, α) ∈ ?P"
      using step.hyps(2) ‹w=_› Unit_elim_rel_r14[of P] 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(1) step.hyps(2) unfolding Unit_elim_def by auto
    hence "?P ⊢ l @ [Nt A] @ r ⇒ l @ w @ r"
      by (auto simp: derive.simps)
    then show ?thesis
      using step by simp
  qed
qed

theorem Lang_Unit_elim: "Lang (Unit_elim P) S = Lang P S"
  unfolding Lang_def using Unit_elim_rel_r4 Unit_elim_rel_complete by blast

corollary lang_unit_elim: "lang (unit_elim ps) A = lang ps A"
by (metis Lang_Unit_elim Unit_elim_set)

end