Theory 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 = {σ. eP. fst e  σ = snd e}"

lemma matchers_vars_term_eq:
  assumes "σ  matchers P" and "τ  matchers P"
    and "(s, t)  P"
  shows "xvars_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