Theory LV_to_GTT

section ‹Primitive constructions›

theory LV_to_GTT
  imports Regular_Tree_Relations.Pair_Automaton   

subsection ‹Recognizing subterms of linear terms›
(* Pattern recognizer automaton *)
abbreviation ffunas_terms where
  "ffunas_terms R  |⋃| (ffunas_term |`| R)"

definition "states R  {t | s t. s  R  s  t}"

lemma states_conv:
  "states R = term_to_bot_term ` ( s  R. subterms s)"
  unfolding states_def set_all_subteq_subterms
  by auto

lemma finite_states:
  assumes "finite R" shows "finite (states R)"
proof -
  have conv: "states R = term_to_bot_term ` ( s  R. {t | t. s  t})"
    unfolding states_def by auto
  from assms have "finite ( s  R. {t | t. s  t})"
    by (intro finite_UN_I2 finite_imageI) (simp add: finite_subterms)+
  then show ?thesis using conv by auto

lemma root_bot_diff:
  "root_bot ` (R - {Bot}) = (root_bot ` R) - {None}"
  using root_bot.elims by auto

lemma root_bot_states_root_subterms:
  "the ` (root_bot ` (states R - {Bot})) = the ` (root ` ( s  R. subterms s) - {None})"
  unfolding states_conv root_bot_diff
  unfolding image_comp
  by simp

includes fset.lifting

lift_definition fstates :: "('f, 'v) term fset  'f bot_term fset" is states
  by (simp add: finite_states)

lift_definition fsubterms :: "('f, 'v) term  ('f, 'v) term fset" is subterms
  by (simp add: finite_subterms_fun)

lemmas fsubterms [code] = subterms.simps[Transfer.transferred]

lift_definition ffunas_trs :: "(('f, 'v) term × ('f, 'v) term) fset  ('f × nat) fset" is funas_trs
  by (simp add: finite_funas_trs)

lemma fstates_def':
  "t |∈| fstates R  ( s u. s |∈| R  s  u  u = t)"
  by transfer (auto simp: states_def)

lemma fstates_fmemberE [elim!]:
  assumes "t |∈| fstates R"
  obtains s u where "s |∈| R  s  u  u = t"
  using assms unfolding fstates_def'
  by blast

lemma fstates_fmemberI [intro]:
  "s |∈| R  s  u  u |∈| fstates R"
  unfolding fstates_def' by blast

lemmas froot_bot_states_root_subterms = root_bot_states_root_subterms[Transfer.transferred]
lemmas root_fsubsterms_ffunas_term_fset = root_substerms_funas_term_set[Transfer.transferred]

lemma fstates[code]:
  "fstates R = term_to_bot_term |`| ( |⋃| (fsubterms |`| R))"
  by transfer (auto simp: states_conv)


definition ta_rule_sig where 
  "ta_rule_sig = (λ r. (r_root r, length (r_lhs_states r)))"

primrec term_to_ta_rule where
 "term_to_ta_rule (BFun f ts) = TA_rule f ts (BFun f ts)"

lemma ta_rule_sig_term_to_ta_rule_root:
  "t  Bot  ta_rule_sig (term_to_ta_rule t) = the (root_bot t)"
  by (cases t) (auto simp: ta_rule_sig_def)

lemma ta_rule_sig_term_to_ta_rule_root_set:
  assumes "Bot |∉| R"
  shows "ta_rule_sig |`| (term_to_ta_rule |`| R) = the |`| (root_bot |`| R)"
proof -
  {fix x assume "x |∈| R" then have "ta_rule_sig (term_to_ta_rule x) = the (root_bot x)"
      using ta_rule_sig_term_to_ta_rule_root[of x] assms
      by auto}
  then show ?thesis
    by (force simp: fimage_iff)

definition pattern_automaton_rules where
  "pattern_automaton_rules  R =
    (let states = (fstates R) - {|Bot|} in
    term_to_ta_rule |`| states |∪| (λ (f, n). TA_rule f (replicate n Bot) Bot) |`| )"

lemma pattern_automaton_rules_BotD:
  assumes "TA_rule f ss Bot |∈| pattern_automaton_rules  R"
  shows "TA_rule f ss Bot |∈| (λ (f, n). TA_rule f (replicate n Bot) Bot) |`| " using assms
  by (auto simp: pattern_automaton_rules_def)
     (metis ta_rule.inject term_to_bot_term.elims term_to_ta_rule.simps)

lemma pattern_automaton_rules_FunD:
  assumes "TA_rule f ss (BFun g ts) |∈| pattern_automaton_rules  R"
  shows "g = f  ts = ss 
     TA_rule f ss (BFun g ts) |∈| term_to_ta_rule |`| ((fstates R) - {|Bot|})" using assms
  apply (auto simp: pattern_automaton_rules_def)
  apply (metis bot_term.exhaust ta_rule.inject term_to_ta_rule.simps)
  by (metis (no_types, lifting) ta_rule.inject term_to_bot_term.elims term_to_ta_rule.simps)

definition pattern_automaton where
  "pattern_automaton  R = TA (pattern_automaton_rules  R) {||}"

lemma ta_sig_pattern_automaton [simp]:
  "ta_sig (pattern_automaton  R) =  |∪| ffunas_terms R"
proof -
  let ?r = "ta_rule_sig"
  have *:"Bot |∉| (fstates R) - {|Bot|}" by simp
  have f: " = ?r |`| ((λ (f, n). TA_rule f (replicate n Bot) Bot) |`| )"
    by (auto simp: image_iff Bex_def ta_rule_sig_def split!: prod.splits)
  moreover have "ffunas_terms R = ?r |`| (term_to_ta_rule |`| ((fstates R) - {|Bot|}))"
    unfolding ta_rule_sig_term_to_ta_rule_root_set[OF *]
    unfolding froot_bot_states_root_subterms root_fsubsterms_ffunas_term_fset
    by simp
  ultimately show ?thesis unfolding pattern_automaton_def ta_sig_def
    unfolding ta_rule_sig_def pattern_automaton_rules_def
    by (simp add: fimage_funion comp_def) blast

lemma terms_reach_Bot:
  assumes "ffunas_gterm t |⊆| "
  shows "Bot |∈| ta_der (pattern_automaton  R) (term_of_gterm t)" using assms
proof (induct t)
  case (GFun f ts)
  have [simp]: "s  set ts  ffunas_gterm s |⊆| " for s using GFun(2)
    using in_set_idx by fastforce
  from GFun show ?case
    by (auto simp: pattern_automaton_def pattern_automaton_rules_def rev_fimage_eqI
             intro!: exI[of _ "replicate (length ts) Bot"])

lemma pattern_automaton_reach_smaller_term:
  assumes "l |∈| R" "l  s" "s b (term_of_gterm t)" "ffunas_gterm t |⊆| "
  shows "s |∈| ta_der (pattern_automaton  R) (term_of_gterm t)" using assms(2-)
proof (induct t arbitrary: s)
  case (GFun f ts) show ?case
  proof (cases s)
    case (Var x)
    then show ?thesis using terms_reach_Bot[OF GFun(4)]
      by (auto simp del: ta_der_Fun)
    case [simp]: (Fun g ss)
    let ?ss = "map term_to_bot_term ss"
    have [simp]: "s  set ts  ffunas_gterm s |⊆| " for s using GFun(4)
      using in_set_idx by fastforce
    from GFun(3) have s: "g = f" "length ss = length ts" by auto
    from GFun(2) s(2) assms(1) have rule: "TA_rule f ?ss (BFun f ?ss) |∈| pattern_automaton_rules  R"
      by (auto simp: s(1) pattern_automaton_rules_def image_iff Bex_def)
    {fix i assume bound: "i < length ts"
      then have sub: "l  ss ! i" using GFun(2) arg_subteq[OF nth_mem, of i ss f]
        unfolding Fun s(1) using s(2) by (metis subterm.order.trans)
      have "ss ! i b (term_of_gterm (ts ! i):: ('a, 'c) term)" using GFun(3) bound s(2)
        by (auto simp: s elim!: bless_eq.cases)
      from GFun(1)[OF nth_mem sub this] bound
      have "ss ! i |∈| ta_der (pattern_automaton  R) (term_of_gterm (ts ! i))"
        by auto}
    then show ?thesis using GFun(2-) s(2) rule
      by (auto simp: s(1) pattern_automaton_def intro!: exI[of _ ?ss] exI[of _ "BFun f ?ss"])

lemma bot_term_of_gterm_conv:
  "term_of_gterm s = term_of_gterm s"
  by (induct s) auto

lemma pattern_automaton_ground_instance_reach:
  assumes "l |∈| R" "l  σ = (term_of_gterm t)" "ffunas_gterm t |⊆| "
  shows "l |∈| ta_der (pattern_automaton  R) (term_of_gterm t)"
proof -
  let ?t = "(term_of_gterm t) :: ('a, 'a bot_term) term"
  from instance_to_bless_eq[OF assms(2)] have sm: "l b ?t"
    using bot_term_of_gterm_conv by metis
  show ?thesis using pattern_automaton_reach_smaller_term[OF assms(1) _ sm] assms(3-)
    by auto

lemma pattern_automaton_reach_smallet_term:
  assumes "l |∈| ta_der (pattern_automaton  R) t" "ground t"
  shows "l b t" using assms
proof (induct t arbitrary: l)
  case (Fun f ts) note IH = this show ?case
  proof (cases l)
    case (Fun g ss)
    let ?ss = "map term_to_bot_term ss"
    from IH(2) have rule: "g = f" "length ss = length ts"
      "TA_rule f ?ss (BFun f ?ss) |∈| rules (pattern_automaton  R)"
        by (auto simp: Fun pattern_automaton_def dest: pattern_automaton_rules_FunD)
    {fix i assume "i < length ts" 
      then have "ss ! i b ts ! i" using IH(2, 3) rule(2)
        by (intro IH(1)) (auto simp: Fun pattern_automaton_def dest: pattern_automaton_rules_FunD)}
    then show ?thesis using rule(2)
      by (auto simp: Fun rule(1))  
  qed auto
qed auto

subsection ‹Recognizing root step relation of LV-TRSs›

definition lv_trs :: "('f, 'v) trs  bool" where
  "lv_trs R  (l, r)  R. linear_term l  linear_term r  (vars_term l  vars_term r = {})"

lemma subst_unification:
   assumes "vars_term s  vars_term t = {}"
   obtains μ where "s  σ = s  μ" "t  τ = t  μ"
   using assms
   by (auto intro!: that[of "λx. if x  vars_term s then σ x else τ x"] simp: term_subst_eq_conv)

lemma lv_trs_subst_unification:
  assumes "lv_trs R" "(l, r)  R" "s = l  σ" "t = r  τ"
  obtains μ where "s = l  μ  t = r  μ"
  using assms subst_unification[of l r σ τ]
  unfolding lv_trs_def
  by (force split!: prod.splits)

definition Relf where
  "Relf R = map_both term_to_bot_term |`| R"

definition root_pair_automaton where
  "root_pair_automaton  R = (pattern_automaton  (fst |`| R),
     pattern_automaton  (snd |`| R))"

definition agtt_grrstep where
  "agtt_grrstep   = pair_at_to_agtt' (root_pair_automaton  ) (Relf )"

lemma agtt_grrstep_eps_trancl [simp]:
  "(eps (fst (agtt_grrstep  )))|+| = eps (fst (agtt_grrstep  ))"
  "(eps (snd (agtt_grrstep  ))) = {||}"
  by (auto simp add: agtt_grrstep_def pair_at_to_agtt'_def
     pair_at_to_agtt_def Let_def root_pair_automaton_def pattern_automaton_def
     fmap_states_ta_def intro!: frelcomp_empty_ftrancl_simp)

lemma root_pair_automaton_grrstep:
  fixes R :: "('f, 'v) rule fset"
  assumes "lv_trs (fset R)" "ffunas_trs R |⊆| "
  shows "pair_at_lang (root_pair_automaton  R) (Relf R) = Restr (grrstep (fset R)) (𝒯G (fset ))" (is "?Ls = ?Rs")
  let ?t_o_g = "term_of_gterm :: 'f gterm  ('f, 'v) Term.term"
  have [simp]: " |∪| |⋃| ((ffunas_term  fst) |`| R) = "
    " |∪| |⋃| ((ffunas_term  snd) |`| R) = " using assms(2)
    by (force simp: less_eq_fset.rep_eq ffunas_trs.rep_eq funas_trs_def ffunas_term.rep_eq ffUnion.rep_eq)+
  {fix s t assume "(s, t)  ?Ls"
    from pair_at_langE[OF this] obtain p q where st: "(q, p) |∈| Relf R"
      "q |∈| gta_der (fst (root_pair_automaton  R)) s" "p |∈| gta_der (snd (root_pair_automaton  R)) t"
      by blast
    from st(1) obtain l r where tm: "q = l" "p = r" "(l, r) |∈| R" unfolding Relf_def
      using assms(1) by auto
    have sm: "l b (?t_o_g s)" "r b (?t_o_g t)"
      using pattern_automaton_reach_smallet_term[of l  "fst |`| R" "term_of_gterm s"]
      using pattern_automaton_reach_smallet_term[of r  "snd |`| R" "term_of_gterm t"]
      using st(2, 3) tm(3) unfolding tm
      by (auto simp: gta_der_def root_pair_automaton_def) (smt bot_term_of_gterm_conv)+
    have "linear_term l" "linear_term r" using tm(3) assms(1)
      by (auto simp: lv_trs_def)
    then obtain σ τ where "l  σ = ?t_o_g s" "r  τ = ?t_o_g t" using sm
      by (auto dest!: bless_eq_to_instance)
    then obtain μ where subst: "l  μ = ?t_o_g s" "r  μ = ?t_o_g t"
      using lv_trs_subst_unification[OF assms(1) tm(3), of "?t_o_g s" σ "?t_o_g t" τ]
      by metis
    moreover have "s  𝒯G (fset )" "t  𝒯G (fset )" using st(2-) assms
      using ta_der_gterm_sig[of q "pattern_automaton  (fst |`| R)" s]
      using ta_der_gterm_sig[of p "pattern_automaton  (snd |`| R)" t]
      by (auto simp: gta_der_def root_pair_automaton_def 𝒯G_equivalent_def less_eq_fset.rep_eq ffunas_gterm.rep_eq)
    ultimately have "(s, t)  ?Rs" using tm(3)
      by (auto simp: grrstep_def rrstep_def') metis}
  then show "?Ls  ?Rs" by auto
  let ?t_o_g = "term_of_gterm :: 'f gterm  ('f, 'v) Term.term"
  {fix s t assume "(s, t)  ?Rs"
    then obtain σ l r where st: "(l, r) |∈| R" "l  σ = ?t_o_g s" "r  σ = ?t_o_g t" "s  𝒯G (fset )" "t  𝒯G (fset )"
      by (auto simp: grrstep_def rrstep_def')
    have funas: "ffunas_gterm s |⊆| " "ffunas_gterm t |⊆| " using st(4, 5)
      by (auto simp: 𝒯G_equivalent_def)
         (metis ffunas_gterm.rep_eq subsetD)+
    from st(1) have "(l, r) |∈| Relf R" unfolding Relf_def using assms(1)
      by (auto simp: fimage_iff fBex_def)
    then have "(s, t)  ?Ls" using st
      using pattern_automaton_ground_instance_reach[of l "fst |`| R" σ, OF _ _ funas(1)]
      using pattern_automaton_ground_instance_reach[of r "snd |`| R" σ, OF _ _ funas(2)]
      by (auto simp: 𝒯G_equivalent_def image_iff Bex_def root_pair_automaton_def gta_der_def pair_at_lang_def)}
  then show "?Rs  ?Ls" by auto

lemma agtt_grrstep:
  fixes R :: "('f, 'v) rule fset"
  assumes "lv_trs (fset R)" "ffunas_trs R |⊆| "
  shows "agtt_lang (agtt_grrstep R ) = Restr (grrstep (fset R)) (𝒯G (fset ))"
  using root_pair_automaton_grrstep[OF assms] unfolding pair_at_agtt_cost agtt_grrstep_def
  by simp

(* Results for set as input *)
lemma root_pair_automaton_grrstep_set:
  fixes R :: "('f, 'v) rule set"
  assumes "finite R" "finite " "lv_trs R" "funas_trs R  "
  shows "pair_at_lang (root_pair_automaton (Abs_fset ) (Abs_fset R)) (Relf (Abs_fset R)) = Restr (grrstep R) (𝒯G )"
proof -
  from assms(1, 2, 4) have "ffunas_trs (Abs_fset R) |⊆| Abs_fset "
    by (auto simp add: Abs_fset_inverse ffunas_trs.rep_eq subset_eq)
  from root_pair_automaton_grrstep[OF _ this] assms
  show ?thesis
    by (auto simp: Abs_fset_inverse)

lemma agtt_grrstep_set:
  fixes R :: "('f, 'v) rule set"
  assumes "finite R" "finite " "lv_trs R" "funas_trs R  "
  shows "agtt_lang (agtt_grrstep (Abs_fset R) (Abs_fset )) = Restr (grrstep R) (𝒯G )"
  using root_pair_automaton_grrstep_set[OF assms] unfolding pair_at_agtt_cost agtt_grrstep_def
  by simp