Theory Abstract_Substitution.Substitution

theory Substitution
  imports Monoid_Action
begin

abbreviation set_prod where
  "set_prod ≡ λ(t, t'). {t, t'}"

section ‹Assumption-free Substitution›

locale substitution_ops =
  fixes
    subst :: "'x ⇒ 's ⇒ 'x" (infixl ‹⋅› 67) and
    id_subst :: 's and
    comp_subst :: "'s ⇒ 's ⇒ 's" (infixl ‹⊙› 67) and
    is_ground :: "'x ⇒ bool"
begin

definition subst_set :: "'x set ⇒ 's ⇒ 'x set" where
  "subst_set X σ = (λx. subst x σ) ` X"

definition subst_list :: "'x list ⇒ 's ⇒ 'x list" where
  "subst_list xs σ = map (λx. subst x σ) xs"

definition is_ground_set :: "'x set ⇒ bool" where
  "is_ground_set X ⟷ (∀x ∈ X. is_ground x)"

definition is_ground_subst :: "'s ⇒ bool" where
  "is_ground_subst γ ⟷ (∀x. is_ground (x ⋅ γ))"

definition generalizes :: "'x ⇒ 'x ⇒ bool" where
  "generalizes x y ⟷ (∃σ. x ⋅ σ = y)"

definition specializes :: "'x ⇒ 'x ⇒ bool" where
  "specializes x y ≡ generalizes y x"

definition strictly_generalizes :: "'x ⇒ 'x ⇒ bool" where
  "strictly_generalizes x y ⟷ generalizes x y ∧ ¬ generalizes y x"

definition strictly_specializes :: "'x ⇒ 'x ⇒ bool" where
  "strictly_specializes x y ≡ strictly_generalizes y x"

definition instances :: "'x ⇒ 'x set" where
  "instances x = {y. generalizes x y}"

definition instances_set :: "'x set ⇒ 'x set" where
  "instances_set X = (⋃x ∈ X. instances x)"

definition ground_instances :: "'x ⇒ 'x set" where
  "ground_instances x = {x⇩𝒢 ∈ instances x. is_ground x⇩𝒢}"

definition ground_instances_set :: "'x set ⇒ 'x set" where
  "ground_instances_set X = {x⇩𝒢 ∈ instances_set X. is_ground x⇩𝒢}"

lemma ground_instances_set_eq_Union_ground_instances:
  "ground_instances_set X = (⋃x ∈ X. ground_instances x)"
  unfolding ground_instances_set_def ground_instances_def
  unfolding instances_set_def
  by auto

lemma ground_instances_eq_Collect_subst_grounding:
  "ground_instances x = {x ⋅ γ | γ. is_ground (x ⋅ γ)}"
  by (auto simp: ground_instances_def instances_def generalizes_def)

lemma mem_ground_instancesE[elim]:
  fixes x x⇩G :: 'x
  assumes "x⇩G ∈ ground_instances x"
  obtains γ :: 's where "x⇩G = x ⋅ γ" and "is_ground (x ⋅ γ)"
  using assms
  unfolding ground_instances_eq_Collect_subst_grounding mem_Collect_eq
  by iprover

lemma mem_ground_instances_setE[elim]:
  fixes x⇩G :: 'x and X :: "'x set"
  assumes "x⇩G ∈ ground_instances_set X"
  obtains x :: 'x and γ :: 's where "x ∈ X" and "x⇩G = x ⋅ γ" and "is_ground (x ⋅ γ)"
  using assms
  unfolding ground_instances_set_eq_Union_ground_instances
  by blast

definition is_unifier :: "'s ⇒ 'x set ⇒ bool" where
  "is_unifier υ X ⟷ card (subst_set X υ) ≤ 1"

definition is_unifier_set :: "'s ⇒ 'x set set ⇒ bool" where
  "is_unifier_set υ XX ⟷ (∀X ∈ XX. is_unifier υ X)"

definition is_mgu :: "'s ⇒ 'x set set ⇒ bool" where
  "is_mgu μ XX ⟷ is_unifier_set μ XX ∧ (∀υ. is_unifier_set υ XX ⟶ (∃σ. μ ⊙ σ = υ))"

definition is_imgu :: "'s ⇒ 'x set set ⇒ bool" where
  "is_imgu μ XX ⟷ is_unifier_set μ XX ∧ (∀τ. is_unifier_set τ XX ⟶ μ ⊙ τ = τ)"

lemma is_unifier_iff_if_finite:
  assumes "finite X"
  shows "is_unifier σ X ⟷ (∀x∈X. ∀y∈X. x ⋅ σ = y ⋅ σ)"
proof (rule iffI)
  show "is_unifier σ X ⟹ (∀x∈X. ∀y∈X. x ⋅ σ = y ⋅ σ)"
    using assms
    unfolding is_unifier_def
    by (metis One_nat_def card_le_Suc0_iff_eq finite_imageI image_eqI subst_set_def)
next
  show "(∀x∈X. ∀y∈X. x ⋅ σ = y ⋅ σ) ⟹ is_unifier σ X"
    unfolding is_unifier_def
    by (smt (verit, del_insts) One_nat_def substitution_ops.subst_set_def card_eq_0_iff
        card_le_Suc0_iff_eq dual_order.eq_iff imageE le_Suc_eq)
qed

lemma is_unifier_singleton[simp]: "is_unifier υ {x}"
  by (simp add: is_unifier_iff_if_finite)

lemma is_unifier_set_empty[simp]:
  "is_unifier_set σ {}"
  by (simp add: is_unifier_set_def)

lemma is_unifier_set_insert:
  "is_unifier_set σ (insert X XX) ⟷ is_unifier σ X ∧ is_unifier_set σ XX"
  by (simp add: is_unifier_set_def)

lemma is_unifier_set_insert_singleton[simp]:
  "is_unifier_set σ (insert {x} XX) ⟷ is_unifier_set σ XX"
  by (simp add: is_unifier_set_def)

lemma is_mgu_insert_singleton[simp]: "is_mgu μ (insert {x} XX) ⟷ is_mgu μ XX"
  by (simp add: is_mgu_def)

lemma is_imgu_insert_singleton[simp]: "is_imgu μ (insert {x} XX) ⟷ is_imgu μ XX"
  by (simp add: is_imgu_def)

lemma subst_set_empty[simp]: "subst_set {} σ = {}"
  by (simp only: subst_set_def image_empty)

lemma subst_set_insert[simp]: "subst_set (insert x X) σ = insert (x ⋅ σ) (subst_set X σ)"
  by (simp only: subst_set_def image_insert)

lemma subst_set_union[simp]: "subst_set (X1 ∪ X2) σ = subst_set X1 σ ∪ subst_set X2 σ"
  by (simp only: subst_set_def image_Un)

lemma subst_list_Nil[simp]: "subst_list [] σ = []"
  by (simp only: subst_list_def list.map)

lemma subst_list_insert[simp]: "subst_list (x # xs) σ = (x ⋅ σ) # (subst_list xs σ)"
  by (simp only: subst_list_def list.map)

lemma subst_list_append[simp]: "subst_list (xs⇩1 @ xs⇩2) σ = subst_list xs⇩1 σ @ subst_list xs⇩2 σ"
  by (simp only: subst_list_def map_append)

lemma is_unifier_set_union:
  "is_unifier_set υ (XX⇩1 ∪ XX⇩2) ⟷ is_unifier_set υ XX⇩1 ∧ is_unifier_set υ XX⇩2"
  by (auto simp add: is_unifier_set_def)

lemma is_unifier_subset: "is_unifier υ A ⟹ finite A ⟹ B ⊆ A ⟹ is_unifier υ B"
  by (smt (verit, best) card_mono dual_order.trans finite_imageI image_mono is_unifier_def
      subst_set_def)

lemma is_ground_set_subset: "is_ground_set A ⟹ B ⊆ A ⟹ is_ground_set B"
  by (auto simp: is_ground_set_def)

lemma is_ground_set_ground_instances[simp]: "is_ground_set (ground_instances x)"
  by (simp add: ground_instances_def is_ground_set_def)

lemma is_ground_set_ground_instances_set[simp]: "is_ground_set (ground_instances_set x)"
  by (simp add: ground_instances_set_def is_ground_set_def)

end


section ‹Basic Substitution›

locale substitution_monoid = monoid comp_subst id_subst ✐‹contributor ‹Balazs Toth››
  for
    comp_subst :: "'s ⇒ 's ⇒ 's" and
    id_subst :: 's
begin

abbreviation is_renaming where
 "is_renaming ≡ is_right_invertible"

lemmas is_renaming_def = is_right_invertible_def

abbreviation renaming_inverse where
  "renaming_inverse ≡ right_inverse"

lemmas renaming_inverse_def = right_inverse_def

lemmas is_renaming_id_subst = neutral_is_right_invertible

definition is_idem :: "'s ⇒ bool" where
  "is_idem a ⟷ comp_subst a a = a"

lemma is_idem_id_subst [simp]: "is_idem id_subst"
  by (simp add: is_idem_def)

end

(* Rename to abstract substitution *)
locale substitution =
  substitution_monoid comp_subst id_subst +
  comp_subst: right_monoid_action comp_subst id_subst subst +
  substitution_ops subst id_subst comp_subst is_ground
  for
    comp_subst :: "'s ⇒ 's ⇒ 's" (infixl ‹⊙› 70) and
    id_subst :: 's and
    subst :: "'x ⇒ 's ⇒ 'x" (infixl ‹⋅› 69) and

    ― ‹Predicate identifying the fixed elements w.r.t. the monoid action›
    is_ground :: "'x ⇒ bool" +
  assumes
    all_subst_ident_if_ground: "is_ground x ⟹ (∀σ. x ⋅ σ = x)"
begin

sublocale comp_subst_set: right_monoid_action comp_subst id_subst subst_set
  using comp_subst.lifting_monoid_action_to_set unfolding subst_set_def .

sublocale comp_subst_list: right_monoid_action comp_subst id_subst subst_list
  using comp_subst.lifting_monoid_action_to_list unfolding subst_list_def .


subsection ‹Substitution Composition›

lemmas subst_comp_subst = comp_subst.action_compatibility
lemmas subst_set_comp_subst = comp_subst_set.action_compatibility
lemmas subst_list_comp_subst = comp_subst_list.action_compatibility


subsection ‹Substitution Identity›

lemmas subst_id_subst = comp_subst.action_neutral
lemmas subst_set_id_subst = comp_subst_set.action_neutral
lemmas subst_list_id_subst = comp_subst_list.action_neutral

lemma is_unifier_id_subst_empty[simp]: "is_unifier id_subst {}"
  by (simp add: is_unifier_def)

lemma is_unifier_set_id_subst_empty[simp]: "is_unifier_set id_subst {}"
  by (simp add: is_unifier_set_def)

lemma is_mgu_id_subst_empty[simp]: "is_mgu id_subst {}"
  by (simp add: is_mgu_def)

lemma is_imgu_id_subst_empty[simp]: "is_imgu id_subst {}"
  by (simp add: is_imgu_def)

lemma is_unifier_id_subst: "is_unifier id_subst X ⟷ card X ≤ 1"
  by (simp add: is_unifier_def)

lemma is_unifier_set_id_subst: "is_unifier_set id_subst XX ⟷ (∀X ∈ XX. card X ≤ 1)"
  by (simp add: is_unifier_set_def is_unifier_id_subst)

lemma is_mgu_id_subst: "is_mgu id_subst XX ⟷ (∀X ∈ XX. card X ≤ 1)"
  by (simp add: is_mgu_def is_unifier_set_id_subst)

lemma is_imgu_id_subst: "is_imgu id_subst XX ⟷ (∀X ∈ XX. card X ≤ 1)"
  by (simp add: is_imgu_def is_unifier_set_id_subst)


subsection ‹Generalization›

sublocale generalizes: preorder generalizes strictly_generalizes
proof unfold_locales
  show "⋀x y. strictly_generalizes x y = (generalizes x y ∧ ¬ generalizes y x)"
    unfolding strictly_generalizes_def generalizes_def by blast
next
  show "⋀x. generalizes x x"
    unfolding generalizes_def using subst_id_subst by metis
next
  show "⋀x y z. generalizes x y ⟹ generalizes y z ⟹ generalizes x z"
    unfolding generalizes_def using subst_comp_subst by metis
qed

lemma generalizes_antisym_if:
  assumes "⋀σ⇩1 σ⇩2 x. x ⋅ (σ⇩1 ⊙ σ⇩2) = x ⟹ x ⋅ σ⇩1 = x"
  shows "⋀x y. generalizes x y ⟹ generalizes y x ⟹ x = y"
  using assms
  by (metis generalizes_def subst_comp_subst)

lemma order_generalizes_if:
  assumes "⋀σ⇩1 σ⇩2 x. x ⋅ (σ⇩1 ⊙ σ⇩2) = x ⟹ x ⋅ σ⇩1 = x"
  shows "class.order generalizes strictly_generalizes"
proof unfold_locales
  show "⋀x y. generalizes x y ⟹ generalizes y x ⟹ x = y"
    using generalizes_antisym_if assms by iprover
qed


subsection ‹Substituting on Ground Expressions›

lemma subst_ident_if_ground[simp]: "is_ground x ⟹ x ⋅ σ = x"
  using all_subst_ident_if_ground by simp

lemma subst_set_ident_if_ground[simp]: "is_ground_set X ⟹ subst_set X σ = X"
  unfolding is_ground_set_def subst_set_def by simp


subsection ‹Instances of Ground Expressions›

lemma instances_ident_if_ground[simp]: "is_ground x ⟹ instances x = {x}"
  unfolding instances_def generalizes_def by simp

lemma instances_set_ident_if_ground[simp]: "is_ground_set X ⟹ instances_set X = X"
  unfolding instances_set_def is_ground_set_def by simp

lemma ground_instances_ident_if_ground[simp]: "is_ground x ⟹ ground_instances x = {x}"
  unfolding ground_instances_def by auto

lemma ground_instances_set_ident_if_ground[simp]: "is_ground_set X ⟹ ground_instances_set X = X"
  unfolding is_ground_set_def ground_instances_set_eq_Union_ground_instances by simp


subsection ‹Unifier of Ground Expressions›

lemma ground_eq_ground_if_unifiable:
  assumes "is_unifier υ {t⇩1, t⇩2}" and "is_ground t⇩1" and "is_ground t⇩2"
  shows "t⇩1 = t⇩2"
  using assms by (simp add: card_Suc_eq is_unifier_def le_Suc_eq subst_set_def)

lemma ball_eq_constant_if_unifier:
  assumes "finite X" and "x ∈ X" and "is_unifier υ X" and "is_ground_set X"
  shows "∀y ∈ X. y = x"
  using assms
proof (induction X rule: finite_induct)
  case empty
  show ?case by simp
next
  case (insert z F)
  then show ?case
    by (metis is_ground_set_def finite.insertI is_unifier_iff_if_finite subst_ident_if_ground)
qed

lemma is_mgu_unifies: ✐‹contributor ‹Balazs Toth››
  assumes "is_mgu μ XX" "∀X ∈ XX. finite X"
  shows "∀X ∈ XX. ∀t ∈ X. ∀t' ∈ X. t ⋅ μ = t' ⋅ μ"
  using assms is_unifier_iff_if_finite
  unfolding is_mgu_def is_unifier_set_def
  by blast

corollary is_mgu_unifies_pair: ✐‹contributor ‹Balazs Toth›› 
  assumes "is_mgu μ {{t, t'}}"
  shows "t ⋅ μ = t' ⋅ μ"
  using is_mgu_unifies[OF assms]
  by (metis finite.emptyI finite.insertI insertCI singletonD)

lemmas subst_mgu_eq_subst_mgu = is_mgu_unifies_pair

lemma is_imgu_unifies: ✐‹contributor ‹Balazs Toth››
  assumes "is_imgu μ XX" "∀X ∈ XX. finite X"
  shows "∀X ∈ XX. ∀t ∈ X. ∀t' ∈ X. t ⋅ μ = t' ⋅ μ"
  using assms is_unifier_iff_if_finite
  unfolding is_imgu_def is_unifier_set_def
  by blast

corollary is_imgu_unifies_pair: ✐‹contributor ‹Balazs Toth››
  assumes "is_imgu μ {{t, t'}}"
  shows "t ⋅ μ = t' ⋅ μ"
  using is_imgu_unifies[OF assms]
  by (metis finite.emptyI finite.insertI insertCI singletonD)

lemmas subst_imgu_eq_subst_imgu = is_imgu_unifies_pair


subsection ‹Ground Substitutions›

lemma is_ground_subst_comp_left: "is_ground_subst σ ⟹ is_ground_subst (σ ⊙ τ)"
  by (simp add: is_ground_subst_def)

lemma is_ground_subst_comp_right: "is_ground_subst τ ⟹ is_ground_subst (σ ⊙ τ)"
  by (simp add: is_ground_subst_def)

lemma is_ground_subst_is_ground:
  assumes "is_ground_subst γ"
  shows "is_ground (t ⋅ γ)"
  using assms is_ground_subst_def by blast


subsection ‹IMGU is Idempotent and an MGU›

lemma is_imgu_iff_is_idem_and_is_mgu: "is_imgu μ XX ⟷ is_idem μ ∧ is_mgu μ XX"
  by (auto simp add: is_imgu_def is_idem_def is_mgu_def simp flip: assoc)


subsection ‹IMGU can be used before unification›

lemma subst_imgu_subst_unifier:
  assumes unif: "is_unifier υ X" and imgu: "is_imgu μ {X}" and "x ∈ X"
  shows "x ⋅ μ ⋅ υ = x ⋅ υ"
proof -
  have "x ⋅ μ ⋅ υ = x ⋅ (μ ⊙ υ)"
    by simp

  also have "… = x ⋅ υ"
    using imgu unif by (simp add: is_imgu_def is_unifier_set_def)

  finally show ?thesis .
qed


subsection ‹Groundings Idempotence›

lemma image_ground_instances_ground_instances:
  "ground_instances ` ground_instances x = (λx. {x}) ` ground_instances x"
proof (rule image_cong)
  show "⋀x⇩𝒢. x⇩𝒢 ∈ ground_instances x ⟹ ground_instances x⇩𝒢 = {x⇩𝒢}"
    using ground_instances_ident_if_ground ground_instances_def by auto
qed simp

lemma grounding_of_set_grounding_of_set_idem[simp]:
  "ground_instances_set (ground_instances_set X) = ground_instances_set X"
  unfolding ground_instances_set_eq_Union_ground_instances UN_UN_flatten
  unfolding image_ground_instances_ground_instances
  by simp


subsection ‹Instances of Substitution›

lemma instances_subst:
  "instances (x ⋅ σ) ⊆ instances x"
proof (rule subsetI)
  fix x⇩σ assume "x⇩σ ∈ instances (x ⋅ σ)"
  thus "x⇩σ ∈ instances x"
    by (metis CollectD CollectI generalizes_def instances_def subst_comp_subst)
qed

lemma instances_set_subst_set:
  "instances_set (subst_set X σ) ⊆ instances_set X"
  unfolding instances_set_def subst_set_def
  using instances_subst by auto

lemma ground_instances_subst:
  "ground_instances (x ⋅ σ) ⊆ ground_instances x"
  unfolding ground_instances_def
  using instances_subst by auto

lemma ground_instances_set_subst_set:
  "ground_instances_set (subst_set X σ) ⊆ ground_instances_set X"
  unfolding ground_instances_set_def
  using instances_set_subst_set by auto


subsection ‹Instances of Renamed Expressions›

lemma instances_subst_ident_if_renaming[simp]:
  "is_renaming ρ ⟹ instances (x ⋅ ρ) = instances x"
  by (metis instances_subst is_renaming_def subset_antisym subst_comp_subst subst_id_subst)

lemma instances_set_subst_set_ident_if_renaming[simp]:
  "is_renaming ρ ⟹ instances_set (subst_set X ρ) = instances_set X"
  by (simp add: instances_set_def subst_set_def)

lemma ground_instances_subst_ident_if_renaming[simp]:
  "is_renaming ρ ⟹ ground_instances (x ⋅ ρ) = ground_instances x"
  by (simp add: ground_instances_def)

lemma ground_instances_set_subst_set_ident_if_renaming[simp]:
  "is_renaming ρ ⟹ ground_instances_set (subst_set X ρ) = ground_instances_set X"
  by (simp add: ground_instances_set_def)

end

end