Theory First_Order_Terms.Matching

(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
Author:  René Thiemann <rene.thiemann@uibk.ac.at>
License: LGPL
*)
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⇧*"
    by (simp add: MATCH1_matchrel_conv)
  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⇧*"
    by (simp add: MATCH1_matchrel_conv ac_simps)
  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