Theory LV_to_GTT

theory LV_to_GTT
  imports RR.Pair_Automaton Bot_Terms
begin

lemma finite_UN_I2:
  "finite A ⟹ (∀ B ∈ A. finite B) ⟹ finite (⋃ A)"
  by blast

(* Pattern recognizer automaton *)
abbreviation ffunas_terms where
  "ffunas_terms R ≡ |⋃| (ffunas_term |`| R)"

"states R ≡ {t^⊥ | s t. s ∈ R ∧ s ⊵ t}"">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
qed

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

context
includes fset.lifting
begin

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_rule :: "('f, 'v) term × ('f, 'v) term  ⇒ ('f × nat) fset" is funas_rule
  by (simp add: finite_funas_rule)

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

lemmas ffunas_rule_def' = funas_rule_def [Transfer.transferred]
lemmas ffunas_trs_def' = funas_trs_def [Transfer.transferred]

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 ffunas_trs_sig_split_fst:
  "ffunas_trs R |⊆| ℱ ⟹ ℱ |∪| |⋃| ((ffunas_term ∘ fst) |`| R) = ℱ"
  by transfer (auto simp: funas_trs_def funas_rule_def)

lemma ffunas_trs_sig_split_snd:
  "ffunas_trs R |⊆| ℱ ⟹ ℱ |∪| |⋃| ((ffunas_term ∘ snd) |`| R) = ℱ"
  by transfer (auto simp: funas_trs_def funas_rule_def)

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

end

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)
qed

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: fimage_iff fBex_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 (auto simp add: Let_def comp_def fimage_funion)
qed

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"])
qed

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)
  next
    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 fimage_iff fBex_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"])
  qed
qed

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
qed

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

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 Rel⇩f where
  "Rel⇩f 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))"

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) (Rel⇩f R) = Restr (grrstep (fset R)) (𝒯⇩G (fset ℱ))" (is "?Ls = ?Rs")
proof
  let ?t_o_g = "term_of_gterm :: 'f gterm ⇒ ('f, 'v) Term.term"
  {fix s t assume "(s, t) ∈ ?Ls"
    from pair_at_langE[OF this] obtain p q where st: "(q, p) |∈| Rel⇩f 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 Rel⇩f_def
      using assms(1) by (auto simp: fmember.abs_eq)
    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 fmember.rep_eq)
    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)[unfolded fmember.rep_eq], 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 ffunas_gterm.rep_eq less_eq_fset.rep_eq
                         ffunas_trs_sig_split_fst[OF assms(2)] ffunas_trs_sig_split_snd[OF assms(2)])
    ultimately have "(s, t) ∈ ?Rs" using tm(3)
      by (auto simp: grrstep_def rrstep_def' fmember.rep_eq) metis}
  then show "?Ls ⊆ ?Rs" by auto
next
  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' fmember.rep_eq)
    have funas: "ffunas_gterm s |⊆| ℱ" "ffunas_gterm t |⊆| ℱ" using st(4, 5)
      by (auto simp: 𝒯⇩G_equivalent_def)
         (metis ffunas_gterm.rep_eq notin_fset subsetD)+
    from st(1) have "(l⇧⊥, r⇧⊥) |∈| Rel⇩f R" unfolding Rel⇩f_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 fimage_iff fBex_def fmember.abs_eq root_pair_automaton_def gta_der_def pair_at_lang_def)}
  then show "?Rs ⊆ ?Ls" by auto
qed

lemma agtt_grrstep:
  fixes R :: "('f, 'v) rule fset"
  assumes "lv_trs (fset R)" "ffunas_trs R |⊆| ℱ"
  shows "agtt_lang (pair_at_to_agtt' (root_pair_automaton ℱ R) (Rel⇩f R)) =
     Restr (grrstep (fset R)) (𝒯⇩G (fset ℱ))"
  using root_pair_automaton_grrstep[OF assms] unfolding pair_at_agtt_cost
  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)) (Rel⇩f (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 fmember.rep_eq subset_eq)
  from root_pair_automaton_grrstep[OF _ this] assms
  show ?thesis
    by (auto simp: Abs_fset_inverse)
qed

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

end