Theory Subterm_Multiset

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2016)
License: LGPL (see file COPYING.LESSER)
*)

chapter ‹Multiset-Extension of Subterm Relation›

theory Subterm_Multiset
imports
  "../Auxiliaries/Multiset_Extension2"
  QTRS.Term_More
begin

(*TODO: move*)
lemma trans_supt: "trans {⊳}" by (auto simp: trans_def dest: supt_trans)

(*TODO: move*)
lemma relcomp3_I:
  assumes "(t, u) ∈ A" and "(s, t) ∈ B" and "(u, v) ∈ B"
  shows "(s, v) ∈ B O A O B"
using assms by blast

(*TODO: move*)
lemma relcomp3_transI:
  assumes "trans B" and "(t, u) ∈ B O A O B" and "(s, t) ∈ B" and "(u, v) ∈ B"
  shows "(s, v) ∈ B O A O B"
using assms by (auto simp: trans_def intro: relcomp3_I)

abbreviation suptmulex ("{⊳⇩#}")
where
  "{⊳⇩#} ≡ s_mul_ext Id {⊳}"

abbreviation suptmulexeq ("{⊵⇩#}")
where
  "{⊵⇩#} ≡ ns_mul_ext Id {⊳}"

abbreviation suptmulex_pred (infix "⊳⇩#" 55)
where
  "s ⊳⇩# t ≡ (s, t) ∈ s_mul_ext Id {⊳}"

abbreviation suptmulexeq_pred (infix "⊵⇩#" 55)
where
  "s ⊵⇩# t ≡ (s, t) ∈ ns_mul_ext Id {⊳}"

lemma suptmulexeq_refl [simp]:
  "T ⊵⇩# T"
  by (auto simp: locally_refl_def ns_mul_ext_refl_local)


lemma args_in_suptmulex:
  "{#Fun f ts#} ⊳⇩# mset ts"
by (intro all_s_s_mul_ext) (auto simp: in_multiset_in_set)

lemma args_in_suptmulexeq:
  "{#Fun f ts#} ⊵⇩# mset ts"
using args_in_suptmulex [of f ts] by (auto simp: ns_mul_ext_Id_eq)

lemma suptmulex_trans:
  assumes "A ⊳⇩# B" and "B ⊳⇩# C"
  shows "A ⊳⇩# C"
by (rule s_mul_ext_trans [OF _ _ _ _ _ assms])
   (auto simp: trans_def refl_on_def compatible_l_def compatible_r_def dest: supt_trans)

lemma suptmulexeq_trans:
  assumes "A ⊵⇩# B" and "B ⊵⇩# C"
  shows "A ⊵⇩# C"
using assms by (auto simp: ns_mul_ext_Id_eq dest: suptmulex_trans)

lemma supt_order_pair: "order_pair {⊳} Id"
by (standard) (auto simp: refl_on_def trans_def dest: supt_trans)

lemma SN_suptmulex:
  "SN {⊳⇩#}"
proof -
  { fix M :: "('f, 'v) term multiset"
    have "SN_on {⊳⇩#} {M}"
      using SN_supt by (intro SN_s_mul_ext_strong [OF supt_order_pair]) (auto simp: SN_defs) }
  then show ?thesis by (auto simp: SN_defs)
qed

lemma suptmulex_not_refl:
  "(M, M) ∉ {⊳⇩#}"
using refl_not_SN [of M "{⊳⇩#}"] and SN_suptmulex by blast

lemma suptmulex_eq:
  "{⊳⇩#} = {⊵⇩#} - Id"
unfolding ns_mul_ext_Id_eq by (auto simp: suptmulex_not_refl)

lemma mult_subt_converse: "(mult {⊲})¯ = {⊳⇩#}"
using mult_s_mul_ext_conv [OF trans_supt] .

lemma trans_subt: "trans {⊲}"
by (simp add: trans_supt)

end