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 "Cl  σ  ta_lang (fstates R) (nf_ta R )"
proof (rule ccontr, simp del: ta_lang_to_gta_lang)
  assume *: "Cl  σ  ta_lang (fstates R) (nf_ta R )"
  then have cgr:"ground (Clσ)" 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 (Clσ))"
    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  Clσ  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  Clσ  (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