# Theory NF

```theory NF
imports
Saturation
Bot_Terms
Regular_Tree_Relations.Tree_Automata
begin

subsection ‹Recognizing normal forms of left linear TRSs›

interpretation lift_total: semilattice_closure_partial_operator "λ x y. (x, y) ∈ mergeP" "(↑)" "λ x y. x ≤⇩b y" Bot
apply unfold_locales apply (auto simp: merge_refl merge_symmetric merge_terms_assoc merge_terms_idem merge_bot_args_bless_eq_merge)
using merge_dist apply blast
using megeP_ass apply blast
using merge_terms_commutative apply blast
apply (metis bless_eq_mergeP bless_eq_trans merge_bot_args_bless_eq_merge merge_dist merge_symmetric merge_terms_commutative)
apply (metis merge_bot_args_bless_eq_merge merge_symmetric merge_terms_commutative)
using bless_eq_closued_under_supremum bless_eq_trans bless_eq_anti_sym
by blast+

abbreviation "psubt_lhs_bot R ≡ {t⇧⊥ | s t. s ∈ R ∧ s ⊳ t}"
abbreviation "closure S ≡ lift_total.cl.pred_closure S"

definition states where
"states R = insert Bot (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 lift_total.cl.closure_mono[OF psubt_mono[of R S]]
by auto

lemma finite_lhs_subt [simp, intro]:
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 have "finite {t | s t . s ∈ R ∧ s ⊳ t}"
then show ?thesis using conv by auto
qed

lemma states_ref_closure:
"states R ⊆ insert Bot (closure (psubt_lhs_bot R))"
unfolding states_def by auto

lemma finite_R_finite_states [simp, intro]:
"finite R ⟹ finite (states R)"
using finite_lhs_subt states_ref_closure
using lift_total.cl.finite_S_finite_closure finite_subset
by fastforce

abbreviation "lift_sup_small s S ≡ lift_total.supremum (lift_total.smaller_subset (Some s) (Some ` S))"
abbreviation "bound_max s S ≡ the (lift_sup_small s S)"

lemma bound_max_state_set:
assumes "finite R"
shows "bound_max t (psubt_lhs_bot R) ∈ states R"
using lift_total.supremum_neut_or_in_closure[OF finite_lhs_subt[OF assms], of t]
unfolding states_def by auto

context
includes fset.lifting
begin
lift_definition fstates :: "('a, 'b) term fset ⇒ 'a bot_term fset" is states
by simp

lemma bound_max_state_fset:
"bound_max t (psubt_lhs_bot (fset R)) |∈| fstates R"
using bound_max_state_set[of "fset R" t]
using fstates.rep_eq by fastforce

end

definition nf_rules where
"nf_rules R ℱ = {|TA_rule f qs q | f qs q. (f, length qs) |∈| ℱ ∧ fset_of_list qs |⊆| fstates R ∧
¬(∃ l |∈| R. l⇧⊥ ≤⇩b BFun f qs) ∧ q = bound_max (BFun f qs) (psubt_lhs_bot (fset R))|}"

lemma nf_rules_fmember:
"TA_rule f qs q |∈| nf_rules R ℱ ⟷ (f, length qs) |∈| ℱ ∧ fset_of_list qs |⊆| fstates R ∧
¬(∃ l |∈| R. l⇧⊥ ≤⇩b BFun f qs) ∧ q = bound_max (BFun f qs) (psubt_lhs_bot (fset R))"
proof -
let ?subP = "λ n qs. fset_of_list qs |⊆| fstates R ∧ length qs = n"
let ?sub = "λ n. Collect (?subP n)"
have *: "finite (?sub n)" for n
using finite_lists_length_eq[of "fset (fstates R)" n]
{fix f n assume mem: "(f, n) ∈ fset ℱ"
have **: "{f} × (?sub n) = {(f, qs) |qs. ?subP n qs}" by auto
from mem have "finite {(f, qs) |qs. ?subP n qs}" using *
using finite_cartesian_product[OF _ *[of n], of "{f}"] unfolding ** by simp}
then have *: "finite (⋃ (f, n) ∈ fset ℱ . {(f, qs) | qs. ?subP n qs})" by auto
have **: "(⋃ (f, n) ∈ fset ℱ . {(f, qs) | qs. ?subP n qs}) = {(f, qs) | f qs. (f, length qs) |∈| ℱ ∧ ?subP (length qs) qs}"
by auto
have *: "finite ({(f, qs) | f qs. (f, length qs) |∈| ℱ ∧ ?subP (length qs) qs} × fset (fstates R))"
using * unfolding ** by (intro finite_cartesian_product) auto
have **: "{TA_rule f qs q | f qs q. (f, length qs) |∈| ℱ ∧ fset_of_list qs |⊆| fstates R ∧ q |∈| fstates R} =
(λ ((f, qs), q). TA_rule f qs q) ` ({(f, qs) | f qs. (f, length qs) |∈| ℱ ∧ ?subP (length qs) qs} × fset (fstates R))"
by (auto simp: image_def split!: prod.splits)
have f: "finite {TA_rule f qs q | f qs q. (f, length qs) |∈| ℱ ∧ fset_of_list qs |⊆| fstates R ∧ q |∈| fstates R}"
unfolding ** using * by auto
show ?thesis
by (auto simp: nf_rules_def bound_max_state_fset intro!: finite_subset[OF _ f])
qed

definition nf_ta where
"nf_ta R ℱ = TA (nf_rules R ℱ) {||}"

definition nf_reg where
"nf_reg R ℱ = Reg (fstates R) (nf_ta R ℱ)"

lemma bound_max_sound:
assumes "finite R"
shows "bound_max t (psubt_lhs_bot R) ≤⇩b t"
using assms lift_total.lift_ord.supremum_smaller_subset[of "Some ` psubt_lhs_bot R" "Some t"]
by auto (metis (no_types, lifting) lift_less_eq_total.elims(2) option.sel option.simps(3))

lemma Bot_in_filter:
"Bot ∈ Set.filter (λs. s ≤⇩b t) (states R)"
by (auto simp: Set.filter_def states_def)

lemma bound_max_exists:
"∃ p. p = bound_max t (psubt_lhs_bot R)"
by blast

lemma bound_max_unique:
assumes "p = bound_max t (psubt_lhs_bot R)" and "q = bound_max t (psubt_lhs_bot R)"
shows "p = q" using assms by force

lemma nf_rule_to_bound_max:
"f qs → q |∈| nf_rules R ℱ ⟹ q = bound_max (BFun f qs) (psubt_lhs_bot (fset R))"
by (auto simp: nf_rules_fmember)

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_der (nf_ta R ℱ) (adapt_vars t)" and "ground t"
shows "q ≤⇩b t⇧⊥" using assms(1, 2)
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_der (nf_ta R ℱ) (adapt_vars (ts ! i))"
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) bound_max_sound[of "fset R"]
by (auto simp: nf_rules_fmember)
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_der (nf_ta R ℱ) (adapt_vars t)"
shows "s⇧⊥ ≤⇩b q" using assms(2-)
proof (induction t arbitrary: q s)
case (Var x)
then show ?case using lift_total.anti_sym by fastforce
next
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_der (nf_ta R ℱ) (adapt_vars (ts ! i))"
have q: "lift_sup_small (BFun f qs) (psubt_lhs_bot (fset R)) = Some q"
using nf_rule_to_bound_max[OF rule]
using lift_total.supremum_smaller_exists_unique[OF finite_lhs_subt, of "fset R" "BFun f qs"]
by simp (metis option.collapse option.distinct(1))
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 (fset R)" using Fun(2 - 4)
by auto
then have "lift_total.lifted_less_eq (Some (s⇧⊥)) (lift_sup_small (BFun f qs) (psubt_lhs_bot (fset R)))"
using subst
by (intro lift_total.lift_ord.supremum_sound)
(auto simp: lift_total.lift_ord.smaller_subset_def)
then show ?case using subst q finite_lhs_subt
by auto
qed

lemma ta_nf_sound1:
assumes ground: "ground t" and lhs: "l |∈| R" and inst: "l⇧⊥ ≤⇩b t⇧⊥"
shows "ta_der (nf_ta R ℱ) (adapt_vars t) = {||}"
proof (rule ccontr)
assume ass: "ta_der (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_der (nf_ta R ℱ) (adapt_vars (Fun f ts))" and
rule: "(f qs → q) |∈| rules (nf_ta R ℱ)" "length qs = length ts" and
reach: "∀ i < length ts. qs ! i |∈| ta_der (nf_ta R ℱ) (adapt_vars (ts ! i))"
by (auto simp add: nf_ta_def) blast
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_der (nf_ta R ℱ) (adapt_vars t)"
shows "q |∈| fstates R" using assms bound_max_state_fset
by (cases t) (auto simp: states_def nf_ta_def nf_rules_def)

lemma ta_nf_sound2:
assumes linear: "∀ l |∈| R. linear_term l"
and "ground (t :: ('f, 'v) term)" and "funas_term t ⊆ fset ℱ"
and NF: "⋀ l s. l |∈| R ⟹ t ⊵ s ⟹ ¬ l⇧⊥ ≤⇩b s⇧⊥"
shows "∃ q. q |∈| ta_der (nf_ta R ℱ) (adapt_vars t)" using assms(2 - 4)
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_der (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_der (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 "q = bound_max (BFun f qs) (psubt_lhs_bot (fset R))" by blast
then have "f qs → q |∈| 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_fmember)
(metis (no_types, lifting) in_fset_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 (fstates R) (nf_ta R ℱ)"
proof (rule ccontr, simp del: ta_lang_to_gta_lang)
assume *: "C⟨l ⋅ σ⟩ ∈ ta_lang (fstates R) (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(1) this] have res: "ta_der (nf_ta R ℱ) (adapt_vars (l ⋅ σ)) = {||}" .
from ta_langE * obtain q where "q |∈| ta_der (nf_ta R ℱ) (adapt_vars (C⟨l⋅σ⟩))"
show False by blast
qed

lemma ta_nf_lang_complete:
assumes linear: "∀ l |∈| R. linear_term l"
and ground: "ground (t :: ('f, 'v) term)" and sig: "funas_term t ⊆ fset ℱ"
and nf: "⋀C σ l. l |∈| R ⟹ C⟨l⋅σ⟩ ≠ t"
shows "t ∈ ta_lang (fstates R) (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 linear ground sig] this
obtain q where "q |∈| ta_der (nf_ta R ℱ) (adapt_vars t)" by blast
from this ta_nf_tr_to_state[OF ground this] ground show ?thesis
by (intro ta_langI) (auto simp add: nf_ta_def)
qed

lemma ta_nf_ℒ_complete:
assumes linear: "∀ l |∈| R. linear_term l"
and sig: "funas_gterm t ⊆ fset ℱ"
and nf: "⋀C σ l. l |∈| R ⟹ C⟨l⋅σ⟩ ≠ (term_of_gterm t)"
shows "t ∈ ℒ (nf_reg R ℱ)"
using ta_nf_lang_complete[of R "term_of_gterm t" ℱ] assms
by (force simp: ℒ_def nf_reg_def funas_term_of_gterm_conv)

lemma nf_ta_funas:
assumes "ground t" "q |∈| ta_der (nf_ta R ℱ) t"
shows "funas_term t ⊆ fset ℱ" using assms
proof (induct t arbitrary: q)
case (Fun f ts)
from Fun(2-) have "(f, length ts) |∈| ℱ"
by (auto simp: nf_ta_def nf_rules_def)
then show ?case using Fun
apply simp
by (smt (verit) Union_least image_iff in_set_idx)
qed auto

lemma gta_lang_nf_ta_funas:
assumes "t ∈ ℒ (nf_reg R ℱ)"
shows "funas_gterm t ⊆ fset ℱ" using assms nf_ta_funas[of "term_of_gterm t" _ R ℱ]
unfolding nf_reg_def ℒ_def
by (auto simp: funas_term_of_gterm_conv)

end
```