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}"
    by (simp add: finite_strict_subterms) 
  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]
    by (simp add: less_eq_fset.rep_eq fset_of_list.rep_eq)
  {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))"
    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) 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))"
    by (auto simp add: nf_ta_def)
  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⋅σ⟩))"
    by (metis adapt_vars_adapt_vars)
  with ta_der_ctxt_decompose[OF this[unfolded adapt_vars_ctxt]] res
  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