Theory Unit_Elimination
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_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 ps ps' ≡ ps' = (Unit_rm ps ∪ New_prods ps)"
corollary Unit_elim_correct: "Unit_elim_rel (set ps) (Unit_elim (set ps))"
by (metis Unit_elim_def Unit_elim_rel_def)
definition Unit_free :: "('n, 't) Prods ⇒ bool" where
"Unit_free P = (∄A B. (A,[Nt B]) ∈ P)"
lemma Unit_free_if_Unit_elim_rel: "Unit_elim_rel ps ps' ⟹ Unit_free ps'"
unfolding Unit_elim_rel_def Unit_rm_def New_prods_def Unit_prods_def Unit_free_def by simp
lemma Unit_elim_rel_Eps_free:
assumes "Eps_free ps" and "Unit_elim_rel ps ps'"
shows "Eps_free ps'"
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)
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 ps ⟹ finite (Unit_prods ps)"
unfolding Unit_prods_def
by (metis (no_types, lifting) case_prodE finite_subset mem_Collect_eq subsetI)
definition NtsCross :: "('n, 't) Prods ⇒ ('n × 'n) set" where
"NtsCross Ps = Nts Ps × Nts Ps"
lemma finite_Unit_rtc:
assumes "finite ps"
shows "finite (Unit_rtc ps)"
proof -
have "finite (Nts ps)"
unfolding Nts_def using assms finite_Nts_syms by auto
hence "finite (NtsCross ps)"
unfolding NtsCross_def by auto
moreover have "Unit_rtc ps ⊆ NtsCross ps"
unfolding Unit_rtc_def NtsCross_def by blast
ultimately show ?thesis
using assms infinite_super by fastforce
qed
definition nPSlambda :: "('n, 't) Prods ⇒ ('n × 'n) ⇒ ('n, 't) Prods" where
"nPSlambda Ps d = {fst d} × {r. (snd d, r) ∈ Ps}"
lemma npsImage: "⋃((nPSlambda (Unit_rm ps)) ` (Unit_rtc (Unit_prods ps))) = New_prods ps"
unfolding New_prods_def nPSlambda_def by fastforce
lemma finite_nPSlambda:
assumes "finite Ps"
shows "finite (nPSlambda Ps d)"
proof -
have "{(B, r). (B, r) ∈ Ps ∧ B = snd d} ⊆ Ps"
by blast
hence "finite {(B, r). (B, r) ∈ Ps ∧ B = snd d}"
using assms finite_subset by blast
hence "finite (snd ` {(B, r). (B, r) ∈ Ps ∧ B = snd d})"
by simp
moreover have "{r. (snd d, r) ∈ Ps} = (snd ` {(B, r). (B, r) ∈ Ps ∧ B = snd d})"
by force
ultimately show ?thesis
using assms unfolding nPSlambda_def by simp
qed
lemma finite_Unit_rm: "finite ps ⟹ finite (Unit_rm ps)"
unfolding Unit_rm_def by simp
lemma finite_New_prods: assumes "finite ps" shows "finite (New_prods ps)"
proof -
have "finite (Unit_rtc (Unit_prods ps))"
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 ps ⟹ finite (Unit_rm ps ∪ New_prods ps)"
by (simp add: finite_New_prods finite_Unit_rm)
lemma Unit_elim_rel_exists: "finite ps ⟹ ∃ps'. Unit_elim_rel ps ps' ∧ finite ps'"
unfolding Unit_elim_rel_def using finite_list[OF finiteUnit_elim_relRules] by blast
lemma inNonUnitProds:
"p ∈ Unit_rm ps ⟹ p ∈ ps"
unfolding Unit_rm_def by blast
lemma psubDeriv:
assumes "ps ⊢ u ⇒ v"
and "∀p ∈ ps. p ∈ ps'"
shows "ps' ⊢ u ⇒ v"
using assms by (meson derive_iff)
lemma psubRtcDeriv:
assumes "ps ⊢ u ⇒* v"
and "∀p ∈ ps. p ∈ ps'"
shows "ps' ⊢ u ⇒* v"
using assms by (induction rule: rtranclp.induct) (auto simp: psubDeriv rtranclp.rtrancl_into_rtrancl)
lemma Unit_prods_deriv:
assumes "Unit_prods ps ⊢ u ⇒* v"
shows "ps ⊢ u ⇒* v"
proof -
have "∀p ∈ Unit_prods ps. p ∈ ps"
unfolding Unit_prods_def by blast
thus ?thesis
using assms psubRtcDeriv by blast
qed
lemma Unit_elim_rel_r3:
assumes "Unit_elim_rel ps ps'" and "ps' ⊢ u ⇒ v"
shows "ps ⊢ u ⇒* v"
proof -
obtain A α r1 r2 where A: "(A, α) ∈ ps' ∧ u = r1 @ [Nt A] @ r2 ∧ v = r1 @ α @ r2"
using assms derive.cases by meson
hence "(A, α) ∈ Unit_rm ps ∨ (A, α) ∈ New_prods ps"
using assms(1) unfolding Unit_elim_rel_def by simp
thus ?thesis
proof
assume "(A, α) ∈ Unit_rm ps"
hence "(A, α) ∈ ps"
using inNonUnitProds by blast
hence "ps ⊢ r1 @ [Nt A] @ r2 ⇒ r1 @ α @ r2"
by (auto simp: derive.simps)
thus ?thesis using A by simp
next
assume "(A, α) ∈ New_prods ps"
from this obtain B where B: "(B, α) ∈ Unit_rm ps ∧ (A, B) ∈ Unit_rtc (Unit_prods ps)"
unfolding New_prods_def by blast
hence "Unit_prods ps ⊢ [Nt A] ⇒* [Nt B]"
unfolding Unit_rtc_def by simp
hence "ps ⊢ [Nt A] ⇒* [Nt B]"
using Unit_prods_deriv by blast
hence 1: "ps ⊢ r1 @ [Nt A] @ r2 ⇒* r1 @ [Nt B] @ r2"
using derives_append derives_prepend by blast
have "(B, α) ∈ ps"
using B inNonUnitProds by blast
hence "ps ⊢ 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 "ps' ⊢ u ⇒* v"
and "Unit_elim_rel ps ps'"
shows "ps ⊢ u ⇒* v"
using assms by (induction rule: rtranclp.induct) (auto simp: Unit_elim_rel_r3 rtranclp_trans)
lemma deriv_Unit_rtc:
assumes "ps ⊢ [Nt A] ⇒ [Nt B]"
shows "(A, B) ∈ Unit_rtc (Unit_prods ps)"
proof -
have "(A, [Nt B]) ∈ ps"
using assms by (simp add: derive_singleton)
hence "(A, [Nt B]) ∈ Unit_prods ps"
unfolding Unit_prods_def by blast
hence "Unit_prods ps ⊢ [Nt A] ⇒ [Nt B]"
by (simp add: derive_singleton)
moreover have "B ∈ Nts (Unit_prods ps) ∧ A ∈ Nts (Unit_prods ps)"
using ‹(A, [Nt B]) ∈ Unit_prods ps› 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 ps ps'" "(A, α) ∈ ps'"
shows "(A, α) ∉ Unit_prods ps"
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 ps ps'"
and "ps ⊢ [Nt A] ⇒ [Nt B]" "ps' ⊢ [Nt B] ⇒ v"
shows "ps' ⊢ [Nt A] ⇒ v"
proof -
have 1: "(A, B) ∈ Unit_rtc (Unit_prods ps)"
using deriv_Unit_rtc assms(2) by fast
have 2: "(B, v) ∈ ps'"
using assms(3) by (simp add: derive_singleton)
thus ?thesis
proof (cases "(B, v) ∈ ps")
case True
hence "(B, v) ∈ Unit_rm ps"
unfolding Unit_rm_def using assms(1) assms(3) Unit_elim_rel_r12[of ps ps' 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 ps"
using assms(1) 2 unfolding Unit_rm_def Unit_elim_rel_def by simp
from this obtain C where C: "(C, v) ∈ Unit_rm ps ∧ (B, C) ∈ Unit_rtc (Unit_prods ps)"
unfolding New_prods_def by blast
hence "Unit_prods ps ⊢ [Nt A] ⇒* [Nt C]"
using 1 unfolding Unit_rtc_def by auto
hence "(A, C) ∈ Unit_rtc (Unit_prods ps)"
unfolding Unit_rtc_def using 1 C Unit_rtc_def by fastforce
hence "(A, v) ∈ New_prods ps"
unfolding New_prods_def using C by blast
hence "(A, v) ∈ ps'"
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 "ps ⊢ l @ [Nt A] @ r ⇒* map Tm v"
shows "∃α. ps ⊢ l @ [Nt A] @ r ⇒ l @ α @ r ∧ ps ⊢ l @ α @ r ⇒* map Tm v ∧ (A, α) ∈ ps"
proof -
obtain l' w r' where w: "ps ⊢ l ⇒* l' ∧ ps ⊢ [Nt A] ⇒* w ∧ ps ⊢ 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 α: "ps ⊢ [Nt A] ⇒ α ∧ ps ⊢ α ⇒* w"
by (metis w converse_rtranclpE)
hence "(A, α) ∈ ps"
by (simp add: derive_singleton)
thus ?thesis by (metis α w derive.intros derives_append_decomp)
qed
lemma Unit_elim_rel_r20:
assumes "ps ⊢ u ⇒* map Tm v" "Unit_elim_rel ps ps'"
shows "ps' ⊢ 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 ps")
case True
from this obtain B where "w = [Nt B]"
unfolding Unit_prods_def by blast
have "ps' ⊢ l @ w @ r ⇒* map Tm v ∧ Nt B ∉ set (map Tm v)"
using step.IH assms(2) by auto
obtain α where α: "ps' ⊢ l @ [Nt B] @ r ⇒ l @ α @ r ∧ ps' ⊢ l @ α @ r ⇒* map Tm v ∧ (B, α) ∈ ps'"
using assms(2) step.IH ‹w=_› Unit_elim_rel_r20_aux[of ps' l B r v] by blast
hence "(A, α) ∈ ps'"
using assms(2) step.hyps(2) ‹w=_› Unit_elim_rel_r14[of ps ps' A B α] by (simp add: derive_singleton)
hence "ps' ⊢ 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 ps"
unfolding Unit_rm_def using step.hyps(2) by blast
hence "(A, w) ∈ ps'"
using assms(2) unfolding Unit_elim_rel_def by simp
hence "ps' ⊢ 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 (set ps)) A = lang ps A"
by (rule Unit_elim_rel_Lang_eq[OF Unit_elim_correct])
corollary lang_unit_elim: "lang (unit_elim ps) A = lang ps A"
by (metis unit_elim_correct Unit_elim_rel_Lang_eq)
end