Theory First_Order_Terms.Abstract_Matching

(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
Author:  René Thiemann <rene.thiemann@uibk.ac.at>
License: LGPL
*)
section ‹Abstract Matching›

theory Abstract_Matching
  imports
    Term_Pair_Multiset
    "Abstract-Rewriting.Abstract_Rewriting"
begin

(*FIXME: move(?)*)
lemma singleton_eq_union_iff [iff]:
  "{#x#} = M + {#y#} ⟷ M = {#} ∧ x = y"
  by (metis multi_self_add_other_not_self single_eq_single single_is_union)

text ‹Turning functional maps into substitutions.›
definition "subst_of_map d σ x =
  (case σ x of
    None ⇒ d x
  | Some t ⇒ t)"

lemma size_mset_mset_less [simp]:
  assumes "length ss = length ts"
  shows "size_mset (mset (zip ss ts)) < 3 + (size_list size ss + size_list size ts)"
  using assms by (induct ss ts rule: list_induct2) (auto simp: pair_size_def)

definition matchers :: "(('f, 'v) term × ('f, 'w) term) set ⇒ ('f, 'v, 'w) gsubst set"
  where
    "matchers P = {σ. ∀e∈P. fst e ⋅ σ = snd e}"

lemma matchers_vars_term_eq:
  assumes "σ ∈ matchers P" and "τ ∈ matchers P"
    and "(s, t) ∈ P"
  shows "∀x∈vars_term s. σ x = τ x"
  using assms unfolding term_subst_eq_conv [symmetric] by (force simp: matchers_def)

lemma matchers_empty [simp]:
  "matchers {} = UNIV"
  by (simp add: matchers_def)

lemma matchers_insert [simp]:
  "matchers (insert e P) = {σ. fst e ⋅ σ = snd e} ∩ matchers P"
  by (auto simp: matchers_def)

lemma matchers_Un [simp]:
  "matchers (P ∪ P') = matchers P ∩ matchers P'"
  by (auto simp: matchers_def)

lemma matchers_set_zip [simp]:
  assumes "length ss = length ts"
  shows "matchers (set (zip ss ts)) = {σ. map (λt. t ⋅ σ) ss = ts}"
  using assms by (induct ss ts rule: list_induct2) auto

definition "matchers_map m = matchers ((λx. (Var x, the (m x))) ` Map.dom m)"

lemma matchers_map_empty [simp]:
  "matchers_map Map.empty = UNIV"
  by (simp add: matchers_map_def)

lemma matchers_map_upd [simp]:
  assumes "σ x = None ∨ σ x = Some t"
  shows "matchers_map (λy. if y = x then Some t else σ y) =
    matchers_map σ ∩ {τ. τ x = t}" (is "?L = ?R")
proof
  show "?L ⊇ ?R" by (auto simp: matchers_map_def matchers_def)
next
  show "?L ⊆ ?R"
    by (rule subsetI)
       (insert assms, auto simp: matchers_map_def matchers_def dom_def)
qed

lemma matchers_map_upd' [simp]:
  assumes "σ x = None ∨ σ x = Some t"
  shows "matchers_map (σ (x ↦ t)) = matchers_map σ ∩ {τ. τ x = t}"
  using matchers_map_upd [of σ x t, OF assms]
  by (simp add: matchers_map_def matchers_def dom_def)

inductive MATCH1 where
  Var [intro!, simp]: "σ x = None ∨ σ x = Some t ⟹
    MATCH1 (P + {#(Var x, t)#}, σ) (P, σ (x ↦ t))" |
  Fun [intro]: "length ss = length ts ⟹
    MATCH1 (P + {#(Fun f ss, Fun f ts)#}, σ) (P + mset (zip ss ts), σ)"
  
lemma MATCH1_matchers [simp]:
  assumes "MATCH1 x y"
  shows "matchers_map (snd x) ∩ matchers (set_mset (fst x)) =
    matchers_map (snd y) ∩ matchers (set_mset (fst y))"
  using assms by (induct) (simp_all add: ac_simps)

definition "matchrel = {(x, y). MATCH1 x y}"

lemma MATCH1_matchrel_conv:
  "MATCH1 x y ⟷ (x, y) ∈ matchrel"
  by (simp add: matchrel_def)

lemma matchrel_rtrancl_matchers [simp]:
  assumes "(x, y) ∈ matchrel⇧*"
  shows "matchers_map (snd x) ∩ matchers (set_mset (fst x)) =
    matchers_map (snd y) ∩ matchers (set_mset (fst y))"
  using assms by (induct) (simp_all add: matchrel_def)

lemma subst_of_map_in_matchers_map [simp]:
  "subst_of_map d m ∈ matchers_map m"
  by (auto simp: subst_of_map_def [abs_def] matchers_map_def matchers_def)

lemma matchrel_sound:
  assumes "((P, Map.empty), ({#}, σ)) ∈ matchrel⇧*"
  shows "subst_of_map d σ ∈ matchers (set_mset P)"
  using matchrel_rtrancl_matchers [OF assms] by simp

lemma MATCH1_size_mset:
  assumes "MATCH1 x y"
  shows "size_mset (fst x) > size_mset (fst y)"
  using assms by (cases) (auto simp: pair_size_def)+

definition "matchless = inv_image (measure size_mset) fst"

lemma wf_matchless:
  "wf matchless"
  by (auto simp: matchless_def)

lemma MATCH1_matchless:
  assumes "MATCH1 x y"
  shows "(y, x) ∈ matchless"
  using MATCH1_size_mset [OF assms]
  by (simp add: matchless_def)

lemma converse_matchrel_subset_matchless:
  "matchrel¯ ⊆ matchless"
  using MATCH1_matchless by (auto simp: matchrel_def)

lemma wf_converse_matchrel:
  "wf (matchrel¯)"
  by (rule wf_subset [OF wf_matchless converse_matchrel_subset_matchless])

lemma MATCH1_singleton_Var [intro]:
  "σ x = None ⟹ MATCH1 ({#(Var x, t)#}, σ) ({#}, σ (x ↦ t))"
  "σ x = Some t ⟹ MATCH1 ({#(Var x, t)#}, σ) ({#}, σ (x ↦ t))"
  using MATCH1.Var [of σ x t "{#}"] by simp_all

lemma MATCH1_singleton_Fun [intro]:
  "length ss = length ts ⟹ MATCH1 ({#(Fun f ss, Fun f ts)#}, σ) (mset (zip ss ts), σ)"
  using MATCH1.Fun [of ss ts "{#}" f σ] by simp

lemma not_MATCH1_singleton_Var [dest]:
  "¬ MATCH1 ({#(Var x, t)#}, σ) ({#}, σ (x ↦ t)) ⟹ σ x ≠ None ∧ σ x ≠ Some t"
  by auto

lemma not_matchrelD:
  assumes "¬ (∃y. (({#e#}, σ), y) ∈ matchrel)"
  shows "(∃f ss x. e = (Fun f ss, Var x)) ∨
    (∃x t. e = (Var x, t) ∧ σ x ≠ None ∧ σ x ≠ Some t) ∨
    (∃f g ss ts. e = (Fun f ss, Fun g ts) ∧ (f ≠ g ∨ length ss ≠ length ts))"
proof (rule ccontr)
  assume *: "¬ ?thesis"
  show False
  proof (cases e)
    case (Pair s t)
    with assms and * show ?thesis
      by (cases s) (cases t, auto simp: matchrel_def)+
  qed
qed

lemma ne_matchers_imp_matchrel:
  assumes "matchers_map σ ∩ matchers {e} ≠ {}"
  shows "∃y. (({#e#}, σ), y) ∈ matchrel"
proof (rule ccontr)
  assume "¬ ?thesis"
  from not_matchrelD [OF this] and assms
    show False by (auto simp: matchers_map_def matchers_def dom_def)
qed

lemma MATCH1_mono:
  assumes "MATCH1 (P, σ) (P', σ')"
  shows "MATCH1 (P + M, σ) (P' + M, σ')"
  using assms apply (cases) apply (auto simp: ac_simps)
  using Var apply force
  using Var apply force
  using Fun
  by (metis (no_types, lifting) add.assoc add_mset_add_single)

lemma matchrel_mono:
  assumes "(x, y) ∈ matchrel"
  shows "((fst x + M, snd x), (fst y + M, snd y)) ∈ matchrel"
  using assms and MATCH1_mono [of "fst x"]
  by (simp add: MATCH1_matchrel_conv)

lemma matchrel_rtrancl_mono:
  assumes "(x, y) ∈ matchrel⇧*"
  shows "((fst x + M, snd x), (fst y + M, snd y)) ∈ matchrel⇧*"
  using assms by (induct) (auto dest:  matchrel_mono [of _ _ M])

lemma ne_matchers_imp_empty_or_matchrel:
  assumes "matchers_map σ ∩ matchers (set_mset P) ≠ {}"
  shows "P = {#} ∨ (∃y. ((P, σ), y) ∈ matchrel)"
proof (cases P)
  case (add e P')
  then have [simp]: "P = P' + {#e#}" by simp
  from assms have "matchers_map σ ∩ matchers {e} ≠ {}" by auto
  from ne_matchers_imp_matchrel [OF this]
    obtain P'' σ' where "MATCH1 ({#e#}, σ) (P'', σ')"
    by (auto simp: matchrel_def)
  from MATCH1_mono [OF this, of P'] have "MATCH1 (P, σ) (P' + P'', σ')" by (simp add: ac_simps)
  then show ?thesis by (auto simp: matchrel_def)
qed simp

lemma matchrel_imp_converse_matchless [dest]:
  "(x, y) ∈ matchrel ⟹ (y, x) ∈ matchless"
  using MATCH1_matchless by (cases x, cases y) (auto simp: matchrel_def)

lemma ne_matchers_imp_empty:
  fixes P :: "(('f, 'v) term × ('f, 'w) term) multiset"
  assumes "matchers_map σ ∩ matchers (set_mset P) ≠ {}"
  shows "∃σ'. ((P, σ), ({#}, σ')) ∈ matchrel⇧*"
using assms
proof (induct P arbitrary: σ rule: wf_induct [OF wf_measure [of size_mset]])
  fix P :: "(('f, 'v) term × ('f, 'w) term) multiset"
    and σ
  presume IH: "⋀P' σ. ⟦(P', P) ∈ measure size_mset; matchers_map σ ∩ matchers (set_mset P') ≠ {}⟧ ⟹
    ∃σ'. ((P', σ), {#}, σ') ∈ matchrel⇧*"
    and *: "matchers_map σ ∩ matchers (set_mset P) ≠ {}"
  show "∃σ'. ((P, σ), {#}, σ') ∈ matchrel⇧*"
  proof (cases "P = {#}")
    assume "P ≠ {#}"
    with ne_matchers_imp_empty_or_matchrel [OF *]
      obtain P' σ' where **: "((P, σ), (P', σ')) ∈ matchrel" by (auto)
    with * have "(P', P) ∈ measure size_mset"
      and "matchers_map σ' ∩ matchers (set_mset P') ≠ {}"
      using MATCH1_matchers [of "(P, σ)" "(P', σ')"]
      by (auto simp: matchrel_def dest: MATCH1_size_mset)
    from IH [OF this] and **
      show ?thesis by (auto intro: converse_rtrancl_into_rtrancl)
  qed force
qed simp

lemma empty_not_reachable_imp_matchers_empty:
  assumes "⋀σ'. ((P, σ), ({#}, σ')) ∉ matchrel⇧*"
  shows "matchers_map σ ∩ matchers (set_mset P) = {}"
  using ne_matchers_imp_empty [of σ P] and assms by blast

lemma irreducible_reachable_imp_matchers_empty:
  assumes "((P, σ), y) ∈ matchrel⇧!" and "fst y ≠ {#}"
  shows "matchers_map σ ∩ matchers (set_mset P) = {}"
proof -
  have "((P, σ), y) ∈ matchrel⇧*"
    and "⋀τ. (y, ({#}, τ)) ∉ matchrel⇧*"
    using assms by  auto (metis NF_not_suc fst_conv normalizability_E)
  moreover with empty_not_reachable_imp_matchers_empty
    have "matchers_map (snd y) ∩ matchers (set_mset (fst y)) = {}" by (cases y) auto
  ultimately show ?thesis using matchrel_rtrancl_matchers [of "(P, σ)"] by simp
qed

lemma matchers_map_not_empty [simp]:
  "matchers_map σ ≠ {}"
  "{} ≠ matchers_map σ"
  by (auto simp: matchers_map_def matchers_def)

lemma matchers_empty_imp_not_empty_NF:
  assumes "matchers (set_mset P) = {}"
  shows "∃y. fst y ≠ {#} ∧ ((P, Map.empty), y) ∈ matchrel⇧!"
proof (rule ccontr)
  assume "¬ ?thesis"
  then have *: "⋀y. ((P, Map.empty), y) ∈ matchrel⇧! ⟹ fst y = {#}" by auto
  have "SN matchrel" using wf_converse_matchrel by (auto simp: SN_iff_wf)
  then obtain y where "((P, Map.empty), y) ∈ matchrel⇧!"
    by (metis SN_imp_WN UNIV_I WN_onE)
  with * [OF this] obtain τ where "((P, Map.empty), ({#}, τ)) ∈ matchrel⇧*" by (cases y) auto
  from matchrel_rtrancl_matchers [OF this] and assms
    show False by simp
qed

end