theory NF
imports TA.Tree_Automata Tree_Automata_Utils Basic_Utils Saturation
begin
datatype 'f bot_term = BFun 'f (args: "'f bot_term list") | Bot
inductive_set mergeP where
base_l [simp]: "(Bot, t) ∈ mergeP"
| base_r [simp]: "(t, Bot) ∈ mergeP"
| step [intro]: "length ss = length ts ⟹ (∀ i < length ts. (ss ! i, ts ! i) ∈ mergeP) ⟹
(BFun f ss, BFun f ts) ∈ mergeP"
lemma merge_refl:
"(s, s) ∈ mergeP"
by (induct s) auto
lemma merge_symmetric:
assumes "(s, t) ∈ mergeP"
shows "(t, s) ∈ mergeP"
using assms by induct auto
fun merge_terms :: "'f bot_term ⇒ 'f bot_term ⇒ 'f bot_term" (infixr "↑" 67) where
"Bot ↑ s = s"
| "s ↑ Bot = s"
| "(BFun f ss) ↑ (BFun g ts) = (if f = g ∧ length ss = length ts
then BFun f (map (case_prod (↑)) (zip ss ts))
else undefined)"
lemma merge_terms_bot_rhs[simp]:
"s ↑ Bot = s" by (cases s) auto
lemma merge_terms_idem: "s ↑ s = s"
by (induct s) (auto simp add: map_nth_eq_conv)
lemma merge_terms_assoc [ac_simps]:
assumes "(s, t) ∈ mergeP" and "(t, u) ∈ mergeP"
shows "(s ↑ t) ↑ u = s ↑ t ↑ u"
using assms by (induct s t arbitrary: u) (auto elim!: mergeP.cases intro!: nth_equalityI)
lemma merge_terms_commutative [ac_simps]:
shows "s ↑ t = t ↑ s"
by (induct s t rule: merge_terms.induct)
(fastforce simp: in_set_conv_nth intro!: nth_equalityI)+
lemma merge_dist:
assumes "(s, t ↑ u) ∈ mergeP" and "(t, u) ∈ mergeP"
shows "(s, t) ∈ mergeP" using assms
by (induct t arbitrary: s u) (auto elim!: mergeP.cases, metis mergeP.step nth_mem)
lemma megeP_ass:
"(s, t ↑ u) ∈ mergeP ⟹ (t, u) ∈ mergeP ⟹ (s ↑ t, u) ∈ mergeP"
by (induct t arbitrary: s u) (auto simp: mergeP.step elim!: mergeP.cases)
interpretation cl: closure_under_pred_fun "(↑)" "λ x y. (x, y) ∈ mergeP"
by unfold_locales (metis merge_symmetric merge_dist megeP_ass merge_refl megeP_ass
merge_terms_assoc merge_terms_commutative merge_terms_idem merge_terms_commutative)+
inductive_set bless_eq where
base_l [simp]: "(Bot, t) ∈ bless_eq"
| step [intro]: "length ss = length ts ⟹ (∀ i < length ts. (ss ! i, ts ! i) ∈ bless_eq) ⟹
(BFun f ss, BFun f ts) ∈ bless_eq"
text ‹Infix syntax.›
abbreviation "bless_eq_pred s t ≡ (s, t) ∈ bless_eq"
notation
bless_eq ("{≤⇩b}") and
bless_eq_pred ("(_/ ≤⇩b _)" [56, 56] 55)
lemma BFun_leq_Bot_False [simp]:
"BFun f ts ≤⇩b Bot ⟷ False"
using bless_eq.cases by auto
lemma BFun_lesseqE [elim]:
assumes "BFun f ts ≤⇩b t"
obtains us where "length ts = length us" "t = BFun f us"
using assms bless_eq.cases by blast
lemma bless_eq_refl: "s ≤⇩b s"
by (induct s) auto
lemma bless_eq_trans [trans]:
assumes "s ≤⇩b t" and "t ≤⇩b u"
shows "s ≤⇩b u" using assms
proof (induct arbitrary: u)
case (step ss ts f)
from step(3) obtain us where [simp]: "u = BFun f us" "length ts = length us" by auto
from step(3, 1, 2) have "i < length ss ⟹ ss ! i ≤⇩b us ! i" for i
by (cases rule: bless_eq.cases) auto
then show ?case using step(1) by auto
qed auto
lemma bless_eq_anti_sym:
"s ≤⇩b t ⟹ t ≤⇩b s ⟹ s = t"
by (induct rule: bless_eq.induct) (auto elim!: bless_eq.cases intro: nth_equalityI)
lemma bless_eq_mergeP:
"s ≤⇩b t ⟹ (s, t) ∈ mergeP"
by (induct s arbitrary: t) (auto elim!: bless_eq.cases)
lemma merge_bot_args_bless_eq_merge:
assumes "(s, t) ∈ mergeP"
shows "s ≤⇩b s ↑ t" using assms
by (induct s arbitrary: t) (auto simp: bless_eq_refl elim!: mergeP.cases intro!: step)
lemma bless_eq_closued_under_merge:
assumes "(s, t) ∈ mergeP" "(u, v) ∈ mergeP" "s ≤⇩b u" "t ≤⇩b v"
shows "s ↑ t ≤⇩b u ↑ v" using assms(3, 4, 1, 2)
proof (induct arbitrary: t v)
case (base_l t)
then show ?case using bless_eq_trans cl.com cl.sym merge_bot_args_bless_eq_merge by fastforce
next
case (step ss ts f)
then show ?case apply (auto elim!: mergeP.cases intro!: bless_eq.step)
using bless_eq_trans merge_bot_args_bless_eq_merge apply blast
by (metis bless_eq.cases bot_term.distinct(1) bot_term.sel(2))
qed
fun term_to_bot_term :: "('f, 'v) term ⇒ 'f bot_term" ("_⇧⊥" [80] 80) where
"(Var _)⇧⊥ = Bot"
| "(Fun f ts)⇧⊥ = BFun f (map term_to_bot_term ts)"
lemma bless_eq_to_instance:
assumes "s⇧⊥ ≤⇩b t⇧⊥" and "linear_term s"
shows "∃ σ. s ⋅ σ = t" using assms
proof (induct s arbitrary: t)
case (Fun f ts)
from Fun(2) obtain us where [simp]: "t = Fun f us" "length ts = length us" by (cases t) auto
have "i < length ts ⟹ ∃σ. ts ! i ⋅ σ = us ! i" for i
using Fun(2, 3) Fun(1)[OF nth_mem, of i "us ! i" for i]
by (auto elim: bless_eq.cases)
then show ?case using Ex_list_of_length_P[of "length ts" "λ σ i. ts ! i ⋅ σ = us ! i"]
using linear_term_comb_subst[OF Fun(3)] by auto
qed auto
lemma instance_to_bless_eq:
assumes "s ⋅ σ = t"
shows "s⇧⊥ ≤⇩b t⇧⊥" using assms
proof (induct s arbitrary: t)
case (Fun f ts) then show ?case
by (cases t) auto
qed auto
abbreviation "psubt_lhs_bot R ≡ {t⇧⊥ | s t. s ∈ R ∧ s ⊳ t}"
definition states where
"states R = insert Bot (cl.closure (psubt_lhs_bot R))"
lemma psubt_mono:
"R ⊆ S ⟹ psubt_lhs_bot R ⊆ psubt_lhs_bot S" by auto
lemma states_mono:
"R ⊆ S ⟹ states R ⊆ states S"
unfolding states_def using cl.closure_mono[OF psubt_mono[of R S]]
by auto
lemma finite_lhs_subt:
assumes "finite R"
shows "finite (psubt_lhs_bot R)"
proof -
have conv: "psubt_lhs_bot R = term_to_bot_term ` {t | s t . s ∈ R ∧ s ⊳ t}" by auto
from assms subterm_set_finite have "finite {t | s t . s ∈ R ∧ s ⊳ t}" by auto
then show ?thesis using conv by auto
qed
lemma states_ref_closure:
"states R ⊆ insert Bot (cl.closure (psubt_lhs_bot R))"
unfolding states_def by auto
lemma finite_R_finite_states:
"finite R ⟹ finite (states R)"
using finite_lhs_subt states_ref_closure
using cl.finite_S_finite_closure finite_subset
by fastforce
abbreviation "bound_max q s S ≡ (let F = Set.filter (λ t. t ≤⇩b s) S in
q ∈ F ∧ (∀ t ∈ F. q ≤⇩b t ⟶ q = t))"
definition nf_rules where
"nf_rules R ℱ = {TA_rule f qs q | f qs q. (f, length qs) ∈ ℱ ∧ set qs ⊆ states R ∧
¬(∃ l ∈ R. l⇧⊥ ≤⇩b BFun f qs) ∧ bound_max q (BFun f qs) (states R)}"
definition nf_ta where
"nf_ta R ℱ = ta.make (states R) (nf_rules R ℱ) {}"
lemma bound_max_state_set:
"bound_max q t (states R) ⟹ q ∈ states R"
by (auto simp: states_def Set.filter_def)
lemma bound_max_join:
assumes "bound_max p t (states R)" and "q ∈ Set.filter (λ s. s ≤⇩b t) (states R)"
shows "q ≤⇩b p"
proof -
note p_state = bound_max_state_set[OF assms(1)]
from assms have less: "p ≤⇩b t" "q ≤⇩b t" by auto
from bless_eq_mergeP[OF this(1)] bless_eq_mergeP[OF this(2)] have merge: "(p, q) ∈ mergeP"
by (metis ‹q ≤⇩b t› bless_eq_mergeP bless_eq_trans cl.com cl.sym merge_bot_args_bless_eq_merge merge_dist)
show ?thesis
proof (cases "p = Bot ∨ q = Bot")
case True then show ?thesis using p_state assms by (metis bless_eq.base_l)
next
case False
from p_state assms(2) False have states: "p ∈ cl.closure (psubt_lhs_bot R)" "q ∈ cl.closure (psubt_lhs_bot R)"
by (auto simp: states_def)
from states merge have "p ↑ q ∈ cl.closure (psubt_lhs_bot R)" using states by auto
moreover have "p ↑ q ≤⇩b t" using less bless_eq_closued_under_merge
by (metis cl.refl merge merge_terms_idem)
ultimately show ?thesis using assms False
by (smt cl.closure.step cl.com insertCI insertE member_filter merge merge_bot_args_bless_eq_merge merge_symmetric states_def)
qed
qed
lemma Bot_in_filter:
"Bot ∈ Set.filter (λs. s ≤⇩b t) (states R)"
by (auto simp: Set.filter_def states_def)
lemma t:
assumes "finite R"
and "⋀ p. p ≤⇩b t ⟹ p ∈ states R ⟹ ∃ u ∈ states R. p ≤⇩b u ∧ p ≠ u ∧ u ≤⇩b t"
and "p ∈ states R" "p ≠ Bot" "p ≤⇩b t"
shows False
proof -
let ?P = "λ u v. p ≤⇩b u ∧ p ≠ u ∧ u ≤⇩b t ∧ p ≤⇩b t"
from assms(2-) have "⋀ p. p ≤⇩b t ⟹ p ∈ cl.closure (psubt_lhs_bot R) ⟹
∃ u ∈ cl.closure (psubt_lhs_bot R). p ≤⇩b u ∧ p ≠ u ∧ u ≤⇩b t"
using bless_eq.base_l bless_eq_anti_sym unfolding states_def by blast
from this assms(3-) obtain f where
f: "∀ x. x ≤⇩b t ∧ x ∈ cl.closure (psubt_lhs_bot R) ⟶ f x ∈ cl.closure (psubt_lhs_bot R) ∧ x ≤⇩b f x ∧ x ≠ f x ∧ f x ≤⇩b t"
using choice[of "λ p u. p ≤⇩b t ∧ p ∈ cl.closure (psubt_lhs_bot R) ⟶ u ∈ cl.closure (psubt_lhs_bot R) ∧ p ≤⇩b u ∧ p ≠ u ∧ u ≤⇩b t"]
by auto
define h where "h = (λ i. (f ^^i) p)"
from assms(3, 4) have mem: "p ∈ cl.closure (psubt_lhs_bot R)" unfolding states_def by blast
have mem: "h n ∈ cl.closure (psubt_lhs_bot R) ∧ h n ≤⇩b t" for n
proof (induct n)
case (Suc n)
then show ?case using f by (auto simp: h_def)
qed (auto simp add: mem assms(5) h_def)
then have sub: "{h n |n. True} ⊆ cl.closure (psubt_lhs_bot R)" by auto
have "i < n ⟹ h i ≤⇩b h n ∧ h i ≠ h n" for i n
proof (induct "n - i" arbitrary: n)
case (Suc x) note IS = this then show ?case
proof (cases n)
case [simp]: (Suc m)
from IS(1)[of m] have "h i ≤⇩b h m ∧ h i ≠ h m ∨ m = i" using IS(2) by auto force
moreover have "h m ≤⇩b h n ∧ h m ≠ h n" using f h_def mem by auto
ultimately show ?thesis unfolding Suc
using bless_eq_anti_sym bless_eq_trans by fastforce
qed auto
qed auto
then have "i ≠ j ⟹ h i ≠ h j" for i j
by (cases "i < j", auto simp: not_less nat_less_le[symmetric]) (metis le_neq_implies_less)
then have "inj h" using mem f by (auto simp: h_def inj_on_def)
then have "infinite {h n | n. True}" using infinite_iff_countable_subset by auto
from infinite_super[OF sub this] have "infinite (cl.closure (psubt_lhs_bot R))" .
then show ?thesis using cl.finite_S_finite_closure[OF finite_lhs_subt[OF assms(1)]]
by auto
qed
lemma bound_max_exists:
assumes "finite R"
shows "∃ p. bound_max p t (states R)"
proof (rule ccontr)
assume ass: "∄p. bound_max p t (states R)"
then obtain p where "p ∈ states R" "p ≠ Bot" "p ≤⇩b t"
by (auto simp: Set.filter_def) (metis (no_types, lifting) bless_eq.base_l insertI1 states_def)
from t[OF assms(1) _ this] show False using ass by (auto simp: Set.filter_def)
qed
lemma bound_max_unique:
assumes "bound_max p t (states R)" and "bound_max q t (states R)"
shows "p = q"
using assms bound_max_join[OF assms(1)] bound_max_join[OF assms(2)]
using bless_eq_anti_sym by force
lemma nf_rule_to_bound_max:
"f qs → q ∈ nf_rules R ℱ ⟹ bound_max q (BFun f qs) (states R)"
by (auto simp: nf_rules_def)
lemma nf_rules_unique:
assumes "f qs → q ∈ nf_rules R ℱ" and "f qs → q' ∈ nf_rules R ℱ"
shows "q = q'" using assms unfolding nf_rules_def
using nf_rule_to_bound_max[OF assms(1)] nf_rule_to_bound_max[OF assms(2)]
using bound_max_unique by blast
lemma nf_ta_det:
shows "ta_det (nf_ta R ℱ)"
by (auto simp add: ta_det_def nf_ta_def nf_rules_unique)
lemma term_instance_of_reach_state:
assumes "q ∈ ta_res (nf_ta R ℱ) (adapt_vars t)" and "ground t"
shows "q ≤⇩b t⇧⊥" using assms
proof(induct t arbitrary: q)
case (Fun f ts)
from Fun(2) obtain qs where wit: "f qs → q ∈ nf_rules R ℱ" "length qs = length ts"
"∀ i < length ts. qs ! i ∈ ta_res (nf_ta R ℱ) (adapt_vars (ts ! i))"
by (auto simp add: nf_ta_def)
then have "BFun f qs ≤⇩b Fun f ts⇧⊥" using Fun(1)[OF nth_mem, of i "qs !i" for i] using Fun(3)
by auto
then show ?case using bless_eq_trans wit(1)
by (auto simp: nf_rules_def)
qed auto
lemma [simp]: "i < length ss ⟹ l ⊳ Fun f ss ⟹ l ⊳ ss ! i"
by (meson nth_mem subterm.dual_order.strict_trans supt.arg)
lemma subt_less_eq_res_less_eq:
assumes ground: "ground t" and "l ∈ R" and "l ⊳ s" and "s⇧⊥ ≤⇩b t⇧⊥"
and "q ∈ ta_res (nf_ta R ℱ) (adapt_vars t)"
shows "s⇧⊥ ≤⇩b q" using assms
proof (induction t arbitrary: q s)
case (Fun f ts) note IN = this
from IN obtain qs where rule: "f qs → q ∈ nf_rules R ℱ" and
reach: "length qs = length ts" "∀ i < length ts. qs ! i ∈ ta_res (nf_ta R ℱ) (adapt_vars (ts ! i))"
by (auto simp add: nf_ta_def)
have subst: "s⇧⊥ ≤⇩b BFun f qs" using IN(1)[OF nth_mem, of i "term.args s ! i" "qs ! i" for i] IN(2-) reach
by (cases s) (auto elim!: bless_eq.cases)
have "s⇧⊥ ∈ psubt_lhs_bot R" using Fun(3, 4) by auto
then have "s⇧⊥ ∈ states R" by (auto simp: states_def)
then show ?case using subst bound_max_join[OF nf_rule_to_bound_max[OF rule]]
by auto
qed auto
lemma ta_nf_sound1:
assumes ground: "ground t" and lhs: "l ∈ R" and inst: "l⇧⊥ ≤⇩b t⇧⊥"
shows "ta_res (nf_ta R ℱ) (adapt_vars t) = {}"
proof (rule ccontr)
assume ass: "ta_res (nf_ta R ℱ) (adapt_vars t) ≠ {}"
show False proof (cases t)
case [simp]: (Fun f ts) from ass
obtain q qs where fin: "q ∈ ta_res (nf_ta R ℱ) (adapt_vars (Fun f ts))" and
rule: "(f qs → q) ∈ ta_rules (nf_ta R ℱ)" "length qs = length ts" and
reach: "∀ i < length ts. qs ! i ∈ ta_res (nf_ta R ℱ) (adapt_vars (ts ! i))"
by (auto simp add: nf_ta_def)
have "l⇧⊥ ≤⇩b BFun f qs" using reach assms(1) inst rule(2)
using subt_less_eq_res_less_eq[OF _ lhs, of "ts ! i" "term.args l ! i" "qs ! i" for i]
by (cases l) (auto elim!: bless_eq.cases intro!: bless_eq.step)
then show ?thesis using lhs rule by (auto simp: nf_ta_def nf_rules_def)
qed (metis ground ground.simps(1))
qed
lemma ta_nf_tr_to_state:
assumes "ground t" and "q ∈ ta_res (nf_ta R ℱ) (adapt_vars t)"
shows "q ∈ states R" using assms
by (cases t) (auto simp: nf_ta_def nf_rules_def)
lemma ta_nf_sound2:
assumes fin: "finite R" and linear: "∀ l ∈ R. linear_term l"
and "ground (t :: ('f, 'v) term)" and "funas_term t ⊆ ℱ"
and NF: "⋀ l s. l ∈ R ⟹ t ⊵ s ⟹ ¬ l⇧⊥ ≤⇩b s⇧⊥"
shows "∃ q. q ∈ ta_res (nf_ta R ℱ) (adapt_vars t)" using assms(3 - 5)
proof (induct t)
case (Fun f ts)
have sub: "⋀ i. i < length ts ⟹ (⋀l s. l ∈ R ⟹ ts ! i ⊵ s ⟹ ¬ l⇧⊥ ≤⇩b s⇧⊥) " using Fun(4) nth_mem by blast
from Fun(1)[OF nth_mem] this Fun(2, 3) obtain qs where
reach: "(∀ i < length ts. qs ! i ∈ ta_res (nf_ta R ℱ) (adapt_vars (ts ! i)))" and len: "length qs = length ts"
using Ex_list_of_length_P[of "length ts" "λ x i. x ∈ (ta_res (nf_ta R ℱ) (adapt_vars (ts ! i)))"]
by auto (meson UN_subset_iff nth_mem)
have nt_inst: "¬ (∃ s ∈ R. s⇧⊥ ≤⇩b BFun f qs)"
proof (rule ccontr, simp)
assume ass: "∃ s ∈ R. s⇧⊥ ≤⇩b BFun f qs"
from term_instance_of_reach_state[of "qs ! i" R ℱ "ts ! i" for i] reach Fun(2) len
have "BFun f qs ≤⇩b Fun f ts⇧⊥" by auto
then show False using ass Fun(4) bless_eq_trans by blast
qed
obtain q where "bound_max q (BFun f qs) (states R)"
using bound_max_exists[OF assms(1), of "BFun f qs"] by blast
then have "f qs → q ∈ ta_rules (nf_ta R ℱ)" using Fun(2 - 4)
using ta_nf_tr_to_state[of "ts ! i" "qs ! i" R ℱ for i] len nt_inst reach
by (auto simp: nf_ta_def nf_rules_def) (metis (no_types, lifting) in_set_idx nth_mem)
then show ?case using reach len by auto
qed auto
lemma ta_nf_lang_sound:
assumes "l ∈ R"
shows "C⟨l ⋅ σ⟩ ∉ ta_lang (nf_ta R ℱ)"
proof (rule ccontr, simp)
assume *: "C⟨l⋅σ⟩ ∈ ta_lang (nf_ta R ℱ)"
then have cgr:"ground (C⟨l⋅σ⟩)" unfolding ta_lang_def by force
then have gr: "ground (l ⋅ σ)" by simp
then have "l⇧⊥ ≤⇩b (l ⋅ σ)⇧⊥" using instance_to_bless_eq by blast
from ta_nf_sound1[OF gr assms this] have res: "ta_res (nf_ta R ℱ) (adapt_vars (l ⋅ σ)) = {}" .
from ta_langE2 * obtain q where "q ∈ ta_res (nf_ta R ℱ) (adapt_vars (C⟨l⋅σ⟩))" by blast
with ta_res_ctxt_decompose[OF this[unfolded adapt_vars_ctxt]] res show False by blast
qed
lemma ta_nf_lang_complete:
assumes fin: "finite (R :: ('f, 'v) term set)" and linear: "∀l ∈ R. linear_term l"
and ground: "ground (t :: ('f, 'v) term)" and sig: "funas_term t ⊆ ℱ"
and nf: "⋀C σ l. l ∈ R ⟹ C⟨l⋅σ⟩ ≠ t"
shows "t ∈ ta_lang (nf_ta R ℱ)"
proof -
from nf have "⋀ l s. l ∈ R ⟹ t ⊵ s ⟹ ¬ l⇧⊥ ≤⇩b s⇧⊥"
using bless_eq_to_instance linear by blast
from ta_nf_sound2[OF fin linear ground sig] this
obtain q where "q ∈ ta_res (nf_ta R ℱ) (adapt_vars t)" by blast
from this ta_nf_tr_to_state[OF ground this] show ?thesis
by (intro ta_langI2[OF ground], auto simp add: nf_ta_def)
qed
end