Theory Saturation_Algorithms
section ‹Compute Productive, Reachable, Useful, Nullable, Prestar›
theory Saturation_Algorithms
imports
"HOL-Library.While_Combinator"
Context_Free_Grammar
begin
text ‹Saturation algorithms (using ‹while_sat›) for a number of elementary CFG problems -
directly, without using the ‹Pre_Star_CFG› entry.
Currently: productive, nullable and reachable nonterminals, and prestar.›
subsection ‹Productive›
definition productive_fun :: "('n,'t)Prods ⇒ 'n set ⇒ 'n set" where
"productive_fun P N = (⋃(A,α) ∈ P. if ∀B ∈ Nts_syms α. B ∈ N then {A} else {})"
definition productive_sat :: "('n,'t)Prods ⇒ 'n set" where
"productive_sat P = the (while_saturate (productive_fun P) {})"
lemma mono_productive_fun:
"mono (productive_fun P)"
unfolding mono_def productive_fun_def by(fastforce split: prod.splits if_splits)
lemma productive_Some: assumes "finite P"
shows "∃N. while_saturate (productive_fun P) {} = Some N"
apply(rule while_saturate_finite_subset_Some[OF mono_productive_fun _ finite_Nts[OF assms]])
unfolding productive_fun_def by (auto simp add: Nts_Lhss_Rhs_Nts in_LhssI split: prod.splits if_splits)
lemma productive_sat_sound: assumes "finite P" and "A ∈ productive_sat P"
shows "productive P A"
proof -
obtain N where w: "while_saturate (productive_fun P) {} = Some N"
using assms(1) productive_Some by blast
hence "A ∈ N" using assms(2) unfolding productive_sat_def by simp
let ?P = "productive P"
have "?P A" if PM: "⋀B. B ∈ M ⟹ ?P B" and A: "A ∈ productive_fun P M" for M A
proof -
from A obtain α where "(A,α) ∈ P" "∀B∈Nts_syms α. B ∈ M"
unfolding productive_fun_def by (auto split: if_splits)
hence "∀B∈Nts_syms α. productive P B" using PM by blast
thus ?thesis using ‹(A,α) ∈ P› productives_if_Nts_productive[of α P]
by (metis converse_rtranclp_into_rtranclp derive_singleton in_Nts_syms)
qed
thus ?thesis using while_saturate_rule1[of ?P _ _ N A] w ‹A ∈ N› by blast
qed
lemma productive_sat_complete: assumes "finite P"
shows "P ⊢ [Nt A] ⇒(n) map Tm w ⟹ A ∈ productive_sat P"
proof (induction n arbitrary: A w rule: less_induct)
case (less n)
then obtain α m where "(A,α) ∈ P" and der: "P ⊢ α ⇒(m) map Tm w" and "n = Suc m"
by (meson deriven_Nt_map_TmD)
from deriven_to_map_TmD[OF der] have "∀B ∈ Nts_syms α. ∃u k. P ⊢ [Nt B] ⇒(k) map Tm u ∧ k ≤ m"
by(fastforce simp: Nts_syms_def in_set_conv_nth elem_le_sum_list)
then have "∀B ∈ Nts_syms α. B ∈ productive_sat P" using less ‹n = Suc m› le_imp_less_Suc by blast
with ‹(A,α) ∈ P› show ?case
using productive_Some[OF assms] while_saturate_saturated
unfolding productive_sat_def productive_fun_def by fastforce
qed
text ‹Code setup:›
definition "productive_set P = {A. productive P A}"
corollary productive_sat_productive_set_if_fin: "finite P ⟹ productive_set P = productive_sat P"
using productive_sat_sound productive_sat_complete unfolding productive_set_def rtranclp_power
by fastforce
corollary productive_set_code[code]: "productive_set (set ps) = productive_sat (set ps)"
using productive_sat_productive_set_if_fin by fast
lemma productives_code[code_unfold]: "productives P α = (Nts_syms α ⊆ productive_set P)"
unfolding productives_if_Productive[of P α] productive_set_def by blast
text ‹Test:›
lemma "let P = {(0,[Nt 1, Nt 1]), (1,[Tm 0]), (1, [Nt 2]), (2,[Nt 2]), (2,[Nt 0,Nt 2]::(int,nat)syms)}
in productive_set P = {0,1} ∧ productive P 0 ∧ productive P 1 ∧ productives P [Nt 0, Nt 1] ∧
restrict_productive P = {(0,[Nt 1, Nt 1]), (1,[Tm 0])}"
by eval
subsection ‹Nullable›
text ‹Nullable means ‹[] ∈ Lang P A››
definition nullable_fun :: "('n,'t)Prods ⇒ 'n set ⇒ 'n set" where
"nullable_fun P N = (⋃(A,α) ∈ P. if Tms_syms α = {} ∧ (∀B ∈ Nts_syms α. B ∈ N) then {A} else {})"
definition nullable :: "('n,'t)Prods ⇒ 'n set" where
"nullable P = the (while_saturate (nullable_fun P) {})"
lemma mono_nullable_fun:
"mono (nullable_fun P)"
unfolding mono_def nullable_fun_def by(force split: prod.splits if_splits)
lemma nullable_Some: assumes "finite P"
shows "∃N. while_saturate (nullable_fun P) {} = Some N"
apply(rule while_saturate_finite_subset_Some[OF mono_nullable_fun _ finite_Nts[OF assms]])
unfolding nullable_fun_def by (auto simp add: Nts_Lhss_Rhs_Nts in_LhssI split: prod.splits if_splits)
lemma nullable_if_Nts_nullable:
"⟦ Tms_syms α = {}; ∀A∈Nts_syms α. ∃u. P ⊢ [Nt A] ⇒* [] ⟧ ⟹ ∃u. P ⊢ α ⇒* []"
proof (induction α)
case (Cons s α)
show ?case
proof (cases s)
case (Nt x1)
then show ?thesis
using Cons.IH Cons.prems by (fastforce simp: derives_Cons_iff map_eq_append_conv)
next
case (Tm x2)
then show ?thesis using Cons.IH Cons.prems by (auto simp: derives_Tm_Cons map_eq_Cons_conv)
qed
qed simp
lemma nullable_sound: assumes "finite P" and "A ∈ nullable P"
shows "∃w. P ⊢ [Nt A] ⇒* []"
proof -
obtain N where w: "while_saturate (nullable_fun P) {} = Some N"
using assms(1) nullable_Some by blast
hence "A ∈ N" using assms(2) unfolding nullable_def by simp
let ?P = "λA. P ⊢ [Nt A] ⇒* []"
have "?P A" if PM: "⋀B. B ∈ M ⟹ ?P B" and A: "A ∈ nullable_fun P M" for M A
proof -
from A obtain α where "(A,α) ∈ P" "Tms_syms α = {}" "∀B∈Nts_syms α. B ∈ M"
unfolding nullable_fun_def by (auto split: if_splits)
hence "∀B∈Nts_syms α. P ⊢ [Nt B] ⇒* []" using PM by blast
thus ?thesis using ‹(A,α) ∈ P› nullable_if_Nts_nullable[OF ‹Tms_syms α = {}›]
by (meson derives_Cons_Nil rtranclp.rtrancl_refl)
qed
thus ?thesis using while_saturate_rule1[of ?P _ _ N A] w ‹A ∈ N› by blast
qed
lemma nullable_complete: assumes "finite P"
shows "P ⊢ [Nt A] ⇒(n) [] ⟹ A ∈ nullable P"
proof (induction n arbitrary: A rule: less_induct)
case (less n)
obtain α m where "(A,α) ∈ P" and der: "P ⊢ α ⇒(m) []" and "n = Suc m"
using deriven_Nt_map_TmD[where w= "[]", simplified, OF less.prems] by auto
from derivenD[OF der] have "Tms_syms α = {}"
unfolding Tms_syms_def in_set_conv_nth
using deriven_Tm_Cons nth_mem by fastforce
from derivenD[OF der] have "∀B ∈ Nts_syms α. ∃u k. P ⊢ [Nt B] ⇒(k) [] ∧ k ≤ m"
by(simp add: Nts_syms_def in_set_conv_nth) (metis elem_le_sum_list in_set_conv_nth)
then have "∀B ∈ Nts_syms α. B ∈ nullable P" using less.IH ‹n = Suc m› le_imp_less_Suc by metis
with ‹(A,α) ∈ P› show ?case
using nullable_Some[OF assms] while_saturate_saturated ‹Tms_syms α = {}›
unfolding nullable_def nullable_fun_def by fastforce
qed
lemma nullable_correct: "finite P ⟹ P ⊢ [Nt A] ⇒* [] ⟷ A ∈ nullable P"
by (metis nullable_complete nullable_sound rtranclp_imp_relpowp)
text ‹Test:›
lemma assumes "P = {(0,[Nt 1, Nt 1]), (1,[]), (2,[Nt 2]), (2,[Nt 0,Nt 2]::(int,nat)syms)}"
shows "P ⊢ [Nt 0] ⇒* []"
proof -
have "0 ∈ nullable P" unfolding assms by eval
thus ?thesis
by (simp add: assms nullable_correct)
qed
subsection ‹Prestar›
text ‹Prestar computes the set of words from which some set of words is reachable via ‹P›.›
definition prestar_fun :: "('n,'t)Prods ⇒ ('n,'t) syms set ⇒ ('n,'t) syms set" where
"prestar_fun P S = (⋃(A,α) ∈ P. ⋃β ∈ S. if length α ≤ length β then ⋃i ≤ length β - length α.
if take (length α) (drop i β) = α then {take i β @ [Nt A] @ drop (i + length α) β} else {} else {})"
lemma prestar_fun1: "β ∈ prestar_fun P S ⟹ ∃β' ∈ S. P ⊢ β ⇒ β'"
apply(auto simp: prestar_fun_def derive.simps)
by (metis (no_types, lifting) add.commute append_take_drop_id drop_drop)
lemma prestar_fun2: assumes "β' ∈ S" "P ⊢ β ⇒ β'" shows "β ∈ prestar_fun P S"
proof -
from assms obtain A α β1 β2 where "(A,α) ∈ P" "β = β1 @ [Nt A] @ β2" "β' = β1 @ α @ β2"
by (meson derive.simps)
hence **: "length α ≤ length β' ∧ length β1 ≤ length β' - length α"
"take (length α) (drop (length β1) β') = α"
and *: "β = take (length β1) β' @ [Nt A] @ drop (length β1 + length α) β'" by simp+
from ** show ?thesis unfolding prestar_fun_def * using ‹(A,α) ∈ P› ‹β' ∈ S›
by auto
qed
definition prestar :: "('n,'t)Prods ⇒ ('n,'t) syms set ⇒ ('n,'t) syms set" where
"prestar P S = the (while_saturate (prestar_fun P) S)"
lemma mono_prestar_fun:
"mono (prestar_fun P)"
unfolding mono_def prestar_fun_def by(fastforce split: prod.splits if_splits)
lemma derive_set_subset2:
"P ⊢ u ⇒ v ⟹ set u ⊆ set v ∪ Syms P"
by (auto simp: derive_iff Syms_def)
lemma prestar_Some: assumes "finite P" "Eps_free P" "finite S0"
shows "∃S. while_saturate (prestar_fun P) S0 = Some S"
proof -
let ?Z = "Syms P ∪ ⋃(set ` S0)"
let ?S = "{β. set β ⊆ ?Z ∧ length β ≤ Max (length ` S0)}"
have "finite (?Z)" using assms(1,3) finite_Syms by blast
from finite_lists_length_le[OF this] have "finite ?S" by blast
have "S0 ⊆ ?S" using assms(3) by fastforce
have "prestar_fun P X ⊆ ?S" if "X ⊆ ?S" for X
proof
fix β assume "β ∈ prestar_fun P X"
from prestar_fun1[OF this] obtain β' where β': "β' ∈ X" "P ⊢ β ⇒ β'" by blast
hence "length β ≤ length β'" using assms(2) derives_measures_if_Eps_free by blast
hence "length β ≤ Max (length ` S0)" using ‹β' ∈ X› that by auto
moreover have "set β ⊆ ?Z" using β' that derive_set_subset2[of P β β'] by auto
ultimately show "β ∈ ?S" by blast
qed
from while_saturate_finite_subset_Some[OF mono_prestar_fun this ‹finite ?S› ‹S0 ⊆ ?S›]
show ?thesis .
qed
lemma prestar_sound: assumes "finite P" "Eps_free P" "finite S0" and "β ∈ prestar P S0"
shows "∃β' ∈ S0. P ⊢ β ⇒* β'"
proof -
obtain S where w: "while_saturate (prestar_fun P) S0 = Some S"
using assms(1-3) prestar_Some by blast
hence "β ∈ S" using assms(4) unfolding prestar_def by simp
let ?P = "λβ. ∃β' ∈ S0. P ⊢ β ⇒* β'"
have "?P β" if PM: "⋀B. B ∈ M ⟹ ?P B" and "β ∈ prestar_fun P M" for M β
proof -
from ‹β ∈ _› obtain β' where "β' ∈ M" "P ⊢ β ⇒ β'" by (metis prestar_fun1)
thus ?thesis using PM
by (meson converse_rtranclp_into_rtranclp)
qed
thus ?thesis using while_saturate_rule1[of ?P, OF _ w] ‹β ∈ S› by blast
qed
lemma prestar_complete: assumes "finite P" "Eps_free P" "finite S0"
shows "β' ∈ S0 ⟹ P ⊢ β ⇒(n) β' ⟹ β ∈ prestar P S0"
proof (induction n arbitrary: β rule: less_induct)
case (less n)
show ?case
proof (cases n)
case 0
then show ?thesis unfolding prestar_def
using less.prems prestar_Some[OF assms(1-3)] while_saturate_incr by fastforce
next
case (Suc m)
then obtain β'' where "P ⊢ β ⇒ β''" "P ⊢ β'' ⇒(m) β'"
by (metis less.prems(2) relpowp_Suc_D2)
then have "β'' ∈ prestar P S0" using Suc less.IH[of m] less.prems(1) by blast
then show ?thesis unfolding prestar_def
using prestar_Some[OF assms(1-3)] while_saturate_saturated[of "(prestar_fun P)" S0]
prestar_fun2[OF _ ‹P ⊢ β ⇒ β''›]
by fastforce
qed
qed
text ‹Test:›
lemma "prestar {(0,[Nt 1, Nt 1]), (1,[Tm 0]), (2,[Nt 2]), (2,[Nt 0,Nt 2]::(int,nat)syms)}
{[Tm 0], [Tm 0, Tm 0]} = {[Tm 0], [Tm 0, Tm 0], [Nt 1], [Nt 1, Tm 0], [Tm 0, Nt 1], [Nt 1, Nt 1], [Nt 0]}"
by eval
subsection ‹Reachable›
definition reachable_fun :: "('n,'t)Prods ⇒ 'n set ⇒ 'n set" where
"reachable_fun P R = ⋃ (Nts_syms ` (⋃(Rhss P ` R)))"
definition reachable_sat :: "('n,'t)Prods ⇒ 'n set ⇒ 'n set" where
"reachable_sat P S = the (while_saturate (reachable_fun P) S)"
lemma mono_reachable_fun:
"mono (reachable_fun P)"
unfolding mono_def reachable_fun_def by(fastforce split: prod.splits if_splits)
locale finP =
fixes P :: "('n,'t)Prods"
assumes finP: "finite P"
begin
lemma reachable_Some: assumes "S ⊆ Nts P"
shows "∃N. while_saturate (reachable_fun P) S = Some N"
apply(rule while_saturate_finite_subset_Some[OF mono_reachable_fun _ finite_Nts[OF finP]])
unfolding reachable_fun_def using assms
by (auto simp add: Nts_Lhss_Rhs_Nts Rhs_Nts_def Lhss_def Nts_syms_def Rhss_def split: prod.splits if_splits)
lemma reachable_sat_sound_aux: assumes "S ⊆ Nts P" and "B ∈ reachable_sat P S"
shows "∃A ∈ S. ∃β. P ⊢ [Nt A] ⇒* β ∧ Nt B ∈ set β"
proof -
obtain R where w: "while_saturate (reachable_fun P) S = Some R"
using reachable_Some[OF assms(1)] by blast
hence "B ∈ R" using assms(2) unfolding reachable_sat_def by simp
let ?P = "λB. ∃A ∈ S. ∃β. P ⊢ [Nt A] ⇒* β ∧ Nt B ∈ set β"
have 0: "?P B" if PM: "⋀B. B ∈ R ⟹ ?P B" and B: "B ∈ reachable_fun P R" for R B
proof -
from B obtain A β where A: "A ∈ R" "P ⊢ [Nt A] ⇒ β" "Nt B ∈ set β"
unfolding reachable_fun_def by (auto simp: derive_singleton Nts_syms_def Rhss_def split: if_splits)
from PM[OF ‹A ∈ R›] obtain A0 β0 where "A0∈S" "P ⊢ [Nt A0] ⇒* β0" "Nt A ∈ set β0"
by (auto)
from split_list[OF this(3)] obtain β1 β2 where "β0 = β1 @ [Nt A] @ β2" by auto
then have "P ⊢ [Nt A0] ⇒* β1 @ β @ β2" using A(2) ‹A0∈S› ‹P ⊢ [Nt A0] ⇒* β0›
by (meson derives_append derives_prepend r_into_rtranclp rtranclp_trans)
then show ?thesis using ‹A0∈S› A(3) by fastforce
qed
show ?thesis using while_saturate_rule1[OF _ w, of "?P", OF _ _ ‹B ∈ R›] 0
by fastforce
qed
corollary reachable_sat_sound: assumes "S ⊆ Nts P" "B ∈ reachable_sat P S"
shows "∃A∈S. reachable P A B"
using reachable_sat_sound_aux[OF assms] unfolding reachable_def by metis
lemma reachable_sat_closed: assumes "S ⊆ Nts P" "A ∈ reachable_sat P S" "(A,α) ∈ P" "Nt B ∈ set α"
shows "B ∈ reachable_sat P S"
proof -
obtain R where w: "while_saturate (reachable_fun P) S = Some R"
using reachable_Some[OF assms(1)] by blast
from while_saturate_saturated[OF w] assms(2-) w
show ?thesis unfolding reachable_sat_def reachable_fun_def
by(auto simp:Rhss_def Nts_syms_def)
qed
lemma reachable_sat_complete_aux: assumes "S ⊆ Nts P" and "A ∈ S"
shows "P ⊢ [Nt A] ⇒(n) β ⟹ Nt B ∈ set β ⟹ B ∈ reachable_sat P S"
proof (induction n arbitrary: B β rule: less_induct)
case (less n)
obtain R where w: "while_saturate (reachable_fun P) S = Some R"
using reachable_Some[OF assms(1)] by blast
show ?case
proof (cases n)
case 0 thus ?thesis using less.prems ‹A ∈ S› while_saturate_incr[OF w] w
unfolding reachable_sat_def by auto
next
case (Suc m)
with less.prems(1) obtain α where 0: "P ⊢ [Nt A] ⇒(m) α" "P ⊢ α ⇒ β" by auto
from this(2) obtain α1 α2 A' α' where "(A',α') ∈ P" "α = α1 @ [Nt A'] @ α2" "β = α1 @ α' @ α2"
by (meson derive.cases)
thus ?thesis using Suc less.prems(2) less.IH[OF _ 0(1)] reachable_sat_closed[OF assms(1) _ ‹(A',α') ∈ P›]
by auto
qed
qed
corollary reachable_sat_complete: assumes "S ⊆ Nts P" "A ∈ S"
shows "reachable P A B ⟹ B ∈ reachable_sat P S"
using reachable_sat_complete_aux[OF assms] unfolding reachable_def
by (metis rtranclp_power)
subsubsection ‹Code setup›
lemma reachable_code[code]:
"reachable P S A = (if S ∈ Nts P then A ∈ reachable_sat P {S} else S=A)"
proof -
have "reachable P S S" using reachable_def by fastforce
moreover have "S ∉ Nts P ⟹ reachable P S A ⟹ S=A"
by (auto simp: reachable_def derives_Cons_iff Nts_Lhss_Rhs_Nts in_LhssI)
ultimately show ?thesis
using reachable_sat_sound[of "{S}" A] by (auto simp: reachable_sat_complete)
qed
lemma set_reachable_code: "{A ∈ Nts P. reachable P S A} = reachable_sat P ({S} ∩ Nts P)"
proof -
have "A ∈ reachable_sat P ({S} ∩ Nts P)" if "A ∈ Nts P" "reachable P S A" for A
using that by (simp add: in_Nts_iff_if_derives reachable_sat_complete)
moreover have "A ∈ Nts P ∧ reachable P S A" if "A ∈ reachable_sat P ({S} ∩ Nts P)" for A
using reachable_sat_sound[OF _ that] by (auto simp: in_Nts_iff_if_derives)
ultimately show ?thesis by blast
qed
end
lemma reachable_code[code]:
"reachable (set ps) S A = (if S ∈ Nts (set ps) then A ∈ reachable_sat (set ps) {S} else S=A)"
by (simp add: finP.reachable_code finP_def)
definition reachable_set :: "('n,'t)Prods ⇒ 'n ⇒ 'n set" where
"reachable_set P S = {A ∈ Nts P. reachable P S A}"
lemma reachable_set[code]:
"reachable_set (set ps) S = reachable_sat (set ps) ({S} ∩ Nts (set ps))"
using finP.set_reachable_code[of "set ps"] unfolding reachable_set_def finP_def by blast
text ‹Test:›
lemma "let P = {(0,[Nt 1, Nt 1]), (1,[Tm 0]), (1, [Nt 2]), (2,[Nt 2]), (2,[Nt 0,Nt 2]::(int,nat)syms)}
in reachable P 0 2 ∧ {A ∈ Nts P. reachable P 1 A} = {0,1,2} ∧ reachable_set P 2 = {0,1,2}"
unfolding reachable_set_def[symmetric]
by eval
subsection ‹Useful›
text ‹Code setup›
lemma useful_iff_reachable_productive_code[code]:
"useful P S A = (if productive P S then reachable (restrict_productive P) S A else False)"
by (metis (mono_tags, lifting) rtranclp_trans useful_def useful_iff_reachable_productive)
text ‹Test:›
lemma "let P = {(0,[Nt 1, Nt 1]), (1,[Tm 0]), (2,[Nt 2]), (2,[Nt 0,Nt 2]::(int,nat)syms)}
in useful P 0 0"
by eval
corollary useful_reachable_productive_code[code]:
"restrict_Nts (useful P S) P =
(if productive P S then
(let P' = restrict_productive P in restrict_Nts (reachable P' S) P')
else {})"
apply (simp add: useful_reachable_productive)
by (auto simp add: restrict_Nts_def useful_iff_reachable_productive_code)
lemma "let P = {(0,[Nt 1, Nt 1]), (1,[Tm 0]), (1,[Nt 2]), (2,[Nt 2]), (2,[Nt 0,Nt 2]::(int,nat)syms)}
in restrict_Nts (useful P 0) P = {(0, [Nt 1, Nt 1]), (1, [Tm 0])}"
by eval
end