Theory Applications

(* Authors: Tassilo Lemke, Tobias Nipkow *)

section ‹Application to Elementary CFG Problems›
text‹\label{sec:applications}›

theory Applications
imports Pre_Star
begin

text‹This theory turns @{const pre_star_auto} into executable decision procedures
for different CFG problems. The methos: @{const pre_star_auto} is applied to different
suitable automata/languages. This happens behind the scenes via code equations.›

text‹These lemmas link @{const pre_star} to different properties of context-free grammars:›

lemma pre_star_term:
  "x ∈ pre_star P L ⟷ (∃w. w ∈ L ∧ P ⊢ x ⇒* w)"
  unfolding pre_star_def by blast

lemma pre_star_word:
  "[Nt S] ∈ pre_star P (map Tm ` L) ⟷ (∃w. w ∈ L ∧ w ∈ Lang P S)"
  unfolding Lang_def pre_star_def by blast

lemma pre_star_lang:
  "Lang P S ∩ L = {} ⟷ [(Nt S)] ∉ pre_star P (map Tm ` L)"
  using pre_star_word[where P=P] by blast

(* TODO: rm with next release: rename tms_syms → Tms_syms elsewehere; rm tms_syms *)
subsection‹Preliminaries›

lemma tms_syms_code[code]:
  "tms_syms w = ⋃((λA. case A of Tm x ⇒ {x} | _ ⇒ {}) ` set w)"
  by (auto simp: tms_syms_def split: sym.splits)


subsection‹Derivability›

text‹A decision procedure for derivability can be constructed.›

definition is_derivable :: "('n, 't) Prods ⇒ ('n, 't) syms ⇒ ('n, 't) syms ⇒ bool" where
[simp]: "is_derivable P α β = (P ⊢ α ⇒* β)"

declare is_derivable_def[symmetric, code_unfold]

theorem pre_star_derivability:
  shows "P ⊢ α ⇒* β ⟷ α ∈ pre_star P {β}"
  by (simp add: Lang_def pre_star_def)

lemma pre_star_derivability_code[code]:
  fixes P :: "('n, 't) prods"
  shows "is_derivable (set P) α β = (α ∈ Lang_auto (pre_star_auto (set P) (word_auto β)))"
proof -
  define M where [simp]: "M ≡ word_auto β"
  have "Lang_auto (pre_star_auto (set P) M) = pre_star (set P) (Lang_auto M)"
    by (intro pre_star_auto_correct; simp add: word_auto_finite_lts)
  then show ?thesis
    using pre_star_derivability by force
qed


subsection‹Membership Problem›

― ‹Directly follows from derivability:›
lemma pre_star_membership[code_unfold]: "(w ∈ Lang P S) = (P ⊢ [Nt S] ⇒* map Tm w)"
  by (simp add: Lang_def)


subsection‹Nullable Variables›

definition is_nullable :: "('n, 't) Prods ⇒ 'n ⇒ bool" where
  "is_nullable P X ≡ (P ⊢ [Nt X] ⇒* [])"

― ‹Directly follows from derivability:›
lemma pre_star_nullable[code]: "is_nullable P X = (P ⊢ [Nt X] ⇒* [])"
  by (simp add: is_nullable_def)


subsection‹Emptiness Problem›

definition is_empty :: "('n, 't) Prods ⇒ 'n ⇒ bool" where
[simp]:  "is_empty P S = (Lang P S = {})"

lemma cfg_derives_Syms:
  assumes "P ⊢ α ⇒* β" and "set α ⊆ Syms P"
  shows "set β ⊆ Syms P"
  using assms proof (induction rule: converse_rtranclp_induct[where r="derive P"])
  case base
  then show ?case
    by simp
next
  case (step y z)
  then have "set z ⊆ Syms P"
    using derives_set_subset by blast
  then show ?case
    using step by simp
qed

lemma cfg_Lang_univ: "P ⊢ [Nt X] ⇒* map Tm β ⟹ set β ⊆ Tms P"
proof -
  assume "P ⊢ [Nt X] ⇒* map Tm β"
  moreover have "Nt X ∈ Syms P"
    using Syms_def calculation derives_start1 by fastforce
  ultimately have "set (map Tm β) ⊆ Syms P"
    using cfg_derives_Syms by force
  moreover have "⋀t. (t ∈ Tms P) ⟷ Tm t ∈ Syms P"
    unfolding Tms_def Syms_def tms_syms_def by blast
  ultimately show "set β ⊆ Tms P"
    by force
qed

lemma inj_Tm: "inj Tm"
  by (simp add: inj_def)

(* TODO: rm with next release *)
lemma finite_tms_syms: "finite (tms_syms w)"
proof -
  have "Tm ` {A. Tm A ∈ set w} ⊆ set w"
    by auto
  from finite_inverse_image[OF _ inj_Tm] show ?thesis
    unfolding tms_syms_def using finite_inverse_image[OF _ inj_Tm] by auto
qed

lemma finite_Tms: "finite P ⟹ finite (Tms P)"
  unfolding Tms_def by (rule finite_Union; auto simp: finite_tms_syms)

definition pre_star_emptiness_auto :: "('n, 't) Prods ⇒ (unit, ('n, 't) sym) auto" where
  "pre_star_emptiness_auto P ≡
    let T = Tm ` ⋃((λA. case A of Nt X ⇒ {} | Tm x ⇒ {x}) ` ⋃(set ` snd ` P)) :: ('n, 't) sym set in
    ⦇ auto.lts = {()} × T × {()}, start = (), finals = {()} ⦈"

theorem pre_star_emptiness:
  fixes P :: "('n, 't) Prods"
  shows "Lang P S = {} ⟷ [(Nt S)] ∉ pre_star P {w. set w ⊆ Tm ` Tms P}"
proof -
  have "Lang P S = {} ⟷ (∄w. P ⊢ [Nt S] ⇒* map Tm w)"
    by (simp add: Lang_def)
  also have "... ⟷ (∄w. P ⊢ [Nt S] ⇒* map Tm w ∧ set w ⊆ Tms P)"
    using cfg_Lang_univ by fast
  also have "... ⟷ (∄w. P ⊢ [Nt S] ⇒* w ∧ set w ⊆ Tm ` Tms P)"
    by (smt (verit, best) cfg_Lang_univ ex_map_conv imageE image_mono list.set_map subset_iff)
  also have "... ⟷ [Nt S] ∉ pre_star P {w. set w ⊆ Tm ` Tms P}"
    unfolding pre_star_def by blast
  finally show ?thesis .
qed

lemma pre_star_emptiness_code[code]:
  fixes P :: "('n, 't) prods"
  shows "is_empty (set P) S = ([Nt S] ∉ Lang_auto (pre_star_auto (set P) (auto_univ (Tm ` Tms (set P)))))"
proof -
  define M :: "(unit, ('n, 't) sym) auto" where [simp]: "M ≡ auto_univ (Tm ` Tms (set P))"
  have "finite (Tm ` Tms (set P))"
    using finite_Tms by blast
  then have "Lang_auto (pre_star_auto (set P) M) = pre_star (set P) (Lang_auto M)"
    by (intro pre_star_auto_correct; auto simp: auto_univ_def intro: loop_lts_fin)
  then show ?thesis
    using pre_star_emptiness unfolding M_def auto_univ_lang by fastforce
qed


subsection‹Useless Variables›

definition is_reachable_from :: "('n, 't) Prods ⇒ 'n ⇒ 'n ⇒ bool"
    ("(2_ ⊢/ (_/ ⇒⇧? / _))" [50, 0, 50] 50) where
  "(P ⊢ X ⇒⇧? Y) ≡ (∃α β. P ⊢ [Nt X] ⇒* (α@[Nt Y]@β))"

―‹‹X ∈ V› is useful, iff ‹V› can be reached from ‹S› and it is productive:›
definition is_useful :: "('n, 't) Prods ⇒ 'n ⇒ 'n ⇒ bool" where
  "is_useful P S X ≡ (P ⊢ S ⇒⇧? X) ∧ Lang P X ≠ {}"

definition pre_star_reachable_auto :: "('n, 't) Prods ⇒ 'n ⇒ (nat, ('n, 't) sym) auto" where
  "pre_star_reachable_auto P X ≡ (
    let T = ⋃(set ` snd ` P) in
    ⦇ auto.lts = ({0} × T × {0}) ∪ ({1} × T × {1}) ∪ {(0, Nt X, 1)}, start = 0, finals = {1} ⦈
  )"

theorem pre_star_reachable:
  fixes P :: "('n, 't) Prods"
  shows "(P ⊢ S ⇒⇧? X) ⟷ [Nt S] ∈ pre_star P { α@[Nt X]@β | α β. set α ⊆ Syms P ∧ set β ⊆ Syms P }"
proof -
  define L where "L ≡ { (α::('n, 't) syms)@[Nt X]@β | α β. set α ⊆ Syms P ∧ set β ⊆ Syms P }"
  have "[Nt S] ∈ pre_star P L  ⟷ (∃w. w ∈ L ∧ P ⊢ [Nt S] ⇒* w)"
    by (simp add: pre_star_term)
  also have "... ⟷ (∃α β. P ⊢ [Nt S] ⇒* (α@[Nt X]@β) ∧ set α ⊆ Syms P ∧ set β ⊆ Syms P)"
    unfolding L_def by blast
  also have "... ⟷ (∃α β. P ⊢ [Nt S] ⇒* (α@[Nt X]@β))"
  proof -
    have "⋀w. P ⊢ [Nt S] ⇒ w ⟹ set w ⊆ Syms P"
      by (smt (verit, best) Syms_def UN_I UnCI case_prod_conv derive_singleton subset_eq)
    then have "⋀w. w ≠ [Nt S] ⟹ P ⊢ [Nt S] ⇒* w ⟹ set w ⊆ Syms P"
      by (metis cfg_derives_Syms converse_rtranclpE)
    then have "⋀α β. P ⊢ [Nt S] ⇒* (α@[Nt X]@β) ⟹ set α ⊆ Syms P ∧ set β ⊆ Syms P"
      by (smt (verit) Cons_eq_append_conv append_is_Nil_conv empty_set empty_subsetI le_supE list.discI set_append)
    then show ?thesis
      by blast
  qed
  finally show ?thesis
    by (simp add: is_reachable_from_def L_def)
qed

lemma pre_star_reachable_code[code]:
  fixes P :: "('n, 't) prods"
  shows "(set P ⊢ S ⇒⇧? X) = ([Nt S] ∈ Lang_auto (pre_star_auto (set P) (cps_auto (Nt X) (Syms (set P)))))"
proof -
  define M :: "(nat, ('n, 't) sym) auto" where [simp]: "M ≡ cps_auto (Nt X) (Syms (set P))"
  have "finite (Syms (set P))"
    unfolding Syms_def by fast
  then have "Lang_auto (pre_star_auto (set P) M) = pre_star (set P) (Lang_auto M)"
    by (intro pre_star_auto_correct; auto simp: cps_auto_def intro: pcs_lts_fin)
  then show ?thesis
    using pre_star_reachable unfolding M_def cps_auto_lang by fastforce
qed


subsection‹Disjointness and Subset Problem›

theorem pre_star_disjointness: "Lang P S ∩ L = {} ⟷ [(Nt S)] ∉ pre_star P (map Tm ` L)"
  by (simp add: pre_star_lang)

theorem pre_star_subset: "Lang P S ⊆ L ⟷ [(Nt S)] ∉ pre_star P (map Tm ` (-L))"
proof -
  have "Lang P S ⊆ L ⟷ Lang P S ∩ -L = {}"
    by blast
  then show ?thesis
    by (simp add: pre_star_disjointness)
qed

end