Theory Grounded_Multiset_Extension

theory Grounded_Multiset_Extension
  imports Grounded_Order Multiset_Extension
begin

section ‹Grounded Multiset Extensions›

locale functional_substitution_multiset_extension =
  sub: strict_order where less = "(≺) :: 'sub ⇒ 'sub ⇒ bool" +
  multiset_extension where to_mset = to_mset +
  functional_substitution_lifting where id_subst = id_subst and to_set = to_set
for
  to_mset :: "'expr ⇒ 'sub multiset" and
  id_subst :: "'var ⇒ 'base" and
  to_set :: "'expr ⇒ 'sub set" +
assumes
    (* TODO: Does it make sense to have these in separate locales? *)
  to_mset_to_set: "⋀expr. set_mset (to_mset expr) = to_set expr" and
  to_mset_map: "⋀f b. to_mset (map f b) = image_mset f (to_mset b)" and
  inj_to_mset: "inj to_mset"
begin

(* TODO *)
no_notation less_eq (infix "≼" 50)
notation sub.less_eq (infix "≼" 50)

lemma lesseq_if_all_lesseq:
  assumes "∀sub ∈# to_mset expr. sub ⋅s σ' ≼ sub ⋅s σ"
  shows "expr ⋅ σ' ≼m expr ⋅ σ"
  using multp_image_lesseq_if_all_lesseq[OF sub.asymp sub.transp assms] inj_to_mset
  unfolding multiset_extension_def subst_def inj_def
  by (auto simp: to_mset_map)

lemma less_if_all_lesseq_ex_less:
  assumes
    "∀sub∈#to_mset expr. sub ⋅s σ' ≼ sub ⋅s σ"
    "∃sub∈#to_mset expr. sub ⋅s σ' ≺ sub ⋅s σ"
  shows
    "expr ⋅ σ' ≺m expr ⋅ σ"
  using multp_image_less_if_all_lesseq_ex_less[OF sub.asymp sub.transp assms]
  unfolding multiset_extension_def subst_def to_mset_map.

end

locale grounded_multiset_extension =
  grounding_lifting where
  id_subst = "id_subst :: 'var ⇒ 'base" and to_set = "to_set :: 'expr ⇒ 'sub set" and
  to_set_ground = to_set_ground +
  functional_substitution_multiset_extension where to_mset = to_mset
for
  to_mset :: "'expr ⇒ 'sub multiset" and
  to_set_ground :: "'exprG ⇒ 'subG set"
begin

sublocale strict_order_restriction "(≺m)" from_ground
  by unfold_locales (rule inj_from_ground)

end

(* TODO: Name → restriction is just total_on *)
locale total_grounded_multiset_extension =
  grounded_multiset_extension +
  sub: total_strict_order_restriction where lift = "sub_from_ground"
begin

sublocale total_strict_order_restriction "(≺m)" from_ground
proof unfold_locales
  have "totalp_on {expr. set_mset expr ⊆ range sub_from_ground} (multp (≺))"
    using sub.totalp totalp_on_multp
    by force

  then have "totalp_on {expr. set_mset (to_mset expr) ⊆ range sub_from_ground} (≺m)"
    using inj_to_mset
    unfolding inj_def multiset_extension_def totalp_on_def
    by blast

  then show "totalp_on (range from_ground) (≺m)"
    unfolding multiset_extension_def totalp_on_def from_ground_def
    by (simp add: image_mono to_mset_to_set)
qed

end

locale based_grounded_multiset_extension =
  based_functional_substitution_lifting where base_vars = base_vars +
  grounded_multiset_extension +
  base: strict_order where less = base_less
for
  base_vars :: "'base ⇒ 'var set" and
  base_less :: "'base ⇒ 'base ⇒ bool"

subsection ‹Ground substitution stability›

locale ground_subst_stable_total_multiset_extension =
  grounded_multiset_extension +
  sub: ground_subst_stable_grounded_order where
  less = less and subst = sub_subst and vars = sub_vars and from_ground = sub_from_ground and
  to_ground = sub_to_ground
begin

sublocale ground_subst_stable_grounded_order where
  less = "(≺m)" and subst = subst and vars = vars and from_ground = from_ground and
  to_ground = to_ground
proof unfold_locales

  fix expr1 expr2 γ

  assume grounding: "is_ground (expr1 ⋅ γ)" "is_ground (expr2 ⋅ γ)" and less: "expr1 ≺m expr2"

  show "expr1 ⋅ γ ≺m expr2 ⋅ γ"
  proof(
      unfold multiset_extension_def subst_def to_mset_map,
      rule multp_map_strong[OF sub.transp _ less[unfolded multiset_extension_def]])

    show "monotone_on (set_mset (to_mset expr1 + to_mset expr2)) (≺) (≺) (λsub. sub ⋅s γ)"
      using grounding monotone_onI sub.ground_subst_stability
      by (metis (mono_tags, lifting) to_mset_to_set to_set_is_ground_subst union_iff)
  qed
qed

end

subsection ‹Substitution update stability›

locale subst_update_stable_multiset_extension =
  based_grounded_multiset_extension +
  sub: subst_update_stable_grounded_order where
  vars = sub_vars and subst = sub_subst and to_ground = sub_to_ground and
  from_ground = sub_from_ground
begin

(* TODO *)
no_notation less_eq (infix "≼" 50)

sublocale subst_update_stable_grounded_order where
  less = "(≺m)"  and vars = vars and subst = subst and from_ground = from_ground and
  to_ground = to_ground
proof unfold_locales
  fix update x γ expr

  assume assms:
    "base.is_ground update" "base_less update (γ x)" "is_ground (expr ⋅ γ)" "x ∈ vars expr"

  moreover then have "∀sub ∈# to_mset expr. sub ⋅s γ(x := update) ≼ sub ⋅s γ"
    using
      sub.subst_update_stability
      sub.subst_reduntant_upd
      to_mset_to_set
      to_set_is_ground_subst
    by blast

  moreover have "∃sub ∈# to_mset expr. sub ⋅s γ(x := update) ≺ (sub ⋅s γ)"
    using sub.subst_update_stability assms
    unfolding vars_def subst_def to_mset_to_set
    by fastforce

  ultimately show "expr ⋅ γ(x := update) ≺m expr ⋅ γ"
    using less_if_all_lesseq_ex_less
    by blast
qed

end

end