# Theory Abstract_Matching

```(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
Author:  René Thiemann <rene.thiemann@uibk.ac.at>
*)
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"

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"

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"

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"

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]

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

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

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