# Theory Matching

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

theory Matching
imports
Abstract_Matching
Unification (* for decompose *)
begin

function match_term_list
where
"match_term_list [] σ = Some σ" |
"match_term_list ((Var x, t) # P) σ =
(if σ x = None ∨ σ x = Some t then match_term_list P (σ (x ↦ t))
else None)" |
"match_term_list ((Fun f ss, Fun g ts) # P) σ =
(case decompose (Fun f ss) (Fun g ts) of
None ⇒ None
| Some us ⇒ match_term_list (us @ P) σ)" |
"match_term_list ((Fun f ss, Var x) # P) σ = None"
by (pat_completeness) auto
termination
by (standard, rule wf_inv_image [OF wf_measure [of size_mset], of "mset ∘ fst"]) (auto simp: pair_size_def)

lemma match_term_list_Some_matchrel:
assumes "match_term_list P σ = Some τ"
shows "((mset P, σ), ({#}, τ)) ∈ matchrel⇧*"
using assms
proof (induction P σ rule: match_term_list.induct)
case (2 x t P σ)
from "2.prems"
have *: "σ x = None ∨ σ x = Some t"
and **: "match_term_list P (σ (x ↦ t)) = Some τ" by (auto split: if_splits)
from MATCH1.Var [of σ x t "mset P", OF *]
have "((mset ((Var x, t) # P), σ), (mset P, σ (x ↦ t))) ∈ matchrel⇧*"
with "2.IH" [OF * **] show ?case by (blast dest: rtrancl_trans)
next
case (3 f ss g ts P σ)
let ?s = "Fun f ss" and ?t = "Fun g ts"
from "3.prems" have [simp]: "f = g"
and *: "length ss = length ts"
and **: "decompose ?s ?t = Some (zip ss ts)"
"match_term_list (zip ss ts @ P) σ = Some τ"
by (auto split: option.splits)
from MATCH1.Fun [OF *, of "mset P" g σ]
have "((mset ((?s, ?t) # P), σ), (mset (zip ss ts @ P), σ)) ∈ matchrel⇧*"
with "3.IH" [OF **] show ?case by (blast dest: rtrancl_trans)
qed simp_all

lemma match_term_list_None:
assumes "match_term_list P σ = None"
shows "matchers_map σ ∩ matchers (set P) = {}"
using assms
proof (induction P σ rule: match_term_list.induct)
case (2 x t P σ)
have "¬ (σ x = None ∨ σ x = Some t) ∨
(σ x = None ∨ σ x = Some t) ∧ match_term_list P (σ (x ↦ t)) = None"
using "2.prems" by (auto split: if_splits)
then show ?case
proof
assume *: "¬ (σ x = None ∨ σ x = Some t)"
have "¬ (∃y. (({#(Var x, t)#}, σ), y) ∈ matchrel)"
proof
presume "¬ ?thesis"
then obtain y where "MATCH1 ({#(Var x, t)#}, σ) y"
by (auto simp: MATCH1_matchrel_conv)
then show False using * by (cases) simp_all
qed simp
moreover have "(({#(Var x, t)#}, σ), ({#(Var x, t)#}, σ)) ∈ matchrel⇧*" by simp
ultimately have "(({#(Var x, t)#}, σ), ({#(Var x, t)#}, σ)) ∈ matchrel⇧!"
by (metis NF_I normalizability_I)
from irreducible_reachable_imp_matchers_empty [OF this]
have "matchers_map σ ∩ matchers {(Var x, t)} = {}" by simp
then show ?case by auto
next
presume *: "σ x = None ∨ σ x = Some t"
and "match_term_list P (σ (x ↦ t)) = None"
from "2.IH" [OF this] have "matchers_map (σ (x ↦ t)) ∩ matchers (set P) = {}" .
with MATCH1_matchers [OF MATCH1.Var [of σ x, OF *], of "mset P"]
show ?case by simp
qed auto
next
case (3 f ss g ts P σ)
let ?s = "Fun f ss" and ?t = "Fun g ts"
have "decompose ?s ?t = None ∨
decompose ?s ?t = Some (zip ss ts) ∧ match_term_list (zip ss ts @ P) σ = None"
using "3.prems" by (auto split: option.splits)
then show ?case
proof
assume "decompose ?s ?t = None"
then show ?case by auto
next
presume "decompose ?s ?t = Some (zip ss ts)"
and "match_term_list (zip ss ts @ P) σ = None"
from "3.IH" [OF this] show ?case by auto
qed auto
qed simp_all

text ‹Compute a matching substitution for a list of term pairs @{term P},
where left-hand sides are "patterns" against which the right-hand sides are matched.›
definition match_list ::
"('v ⇒ ('f, 'w) term) ⇒ (('f, 'v) term × ('f, 'w) term) list ⇒ ('f, 'v, 'w) gsubst option"
where
"match_list d P = map_option (subst_of_map d) (match_term_list P Map.empty)"

lemma match_list_sound:
assumes "match_list d P = Some σ"
shows "σ ∈ matchers (set P)"
using matchrel_sound [of "mset P"]
and match_term_list_Some_matchrel [of P Map.empty]
and assms by (auto simp: match_list_def)

lemma match_list_matches:
assumes "match_list d P = Some σ"
shows "⋀p t. (p, t) ∈ set P ⟹ p ⋅ σ = t"
using match_list_sound [OF assms] by (force simp: matchers_def)

lemma match_list_complete:
assumes "match_list d P = None"
shows "matchers (set P) = {}"
using match_term_list_None [of P Map.empty] and assms by (simp add: match_list_def)

lemma match_list_None_conv:
"match_list d P = None ⟷ matchers (set P) = {}"
using match_list_sound [of d P] and match_list_complete [of d P]
by (metis empty_iff not_None_eq)

definition "match t l = match_list Var [(l, t)]"

lemma match_sound:
assumes "match t p = Some σ"
shows "σ ∈ matchers {(p, t)}"
using match_list_sound [of Var "[(p, t)]"] and assms by (simp add: match_def)

lemma match_matches:
assumes "match t p = Some σ"
shows "p ⋅ σ = t"
using match_sound [OF assms] by (force simp: matchers_def)

lemma match_complete:
assumes "match t p = None"
shows "matchers {(p, t)} = {}"
using match_list_complete [of Var "[(p, t)]"] and assms by (simp add: match_def)

definition matches :: "('f, 'w) term ⇒ ('f, 'v) term ⇒ bool"
where
"matches t p = (case match_list (λ _. t) [(p,t)] of None ⇒ False | Some _ ⇒ True)"

lemma matches_iff:
"matches t p ⟷ (∃σ. p ⋅ σ = t)"
using match_list_sound [of _ "[(p,t)]"]
and match_list_complete [of _ "[(p,t)]"]
unfolding matches_def matchers_def
by (force simp: split: option.splits)

lemma match_complete':
assumes "p ⋅ σ = t"
shows "∃τ. match t p = Some τ ∧ (∀x∈vars_term p. σ x = τ x)"
proof -
from assms have σ: "σ ∈ matchers {(p,t)}" by (simp add: matchers_def)
with match_complete[of t p]
obtain τ where match: "match t p = Some τ" by (auto split: option.splits)
from match_sound[OF this]
have "τ ∈ matchers {(p, t)}" .
from matchers_vars_term_eq[OF σ this] match show ?thesis by auto
qed

abbreviation lvars :: "(('f, 'v) term × ('f, 'w) term) list ⇒ 'v set"
where
"lvars P ≡ ⋃ ((vars_term ∘ fst) ` set P)"

lemma match_list_complete':
assumes "⋀s t. (s, t) ∈ set P ⟹ s ⋅ σ = t"
shows "∃τ. match_list d P = Some τ ∧ (∀x∈lvars P. σ x = τ x)"
proof -
from assms have "σ ∈ matchers (set P)" by (force simp: matchers_def)
moreover with match_list_complete [of d P] obtain τ
where "match_list d P = Some τ" by auto
moreover with match_list_sound [of d P]
have "τ ∈ matchers (set P)"
by (auto simp: match_def split: option.splits)
ultimately show ?thesis
using matchers_vars_term_eq [of σ "set P" "τ"] by auto
qed

end
```