Theory Abstract_Substitution.Substitution

theory Substitution
  imports Main
begin

section ‹General Results on Groups›

lemma (in monoid) right_inverse_idem:
  fixes inv
  assumes right_inverse:  "⋀a. a ❙* inv a = ❙1"
  shows "⋀a. inv (inv a) = a"
    by (metis assoc right_inverse right_neutral)

lemma (in monoid) left_inverse_if_right_inverse:
  fixes inv
  assumes
    right_inverse:  "⋀a. a ❙* inv a = ❙1"
  shows "inv a ❙* a = ❙1"
  by (metis right_inverse_idem right_inverse)

lemma (in monoid) group_wrt_right_inverse:
  fixes inv
  assumes right_inverse:  "⋀a. a ❙* inv a = ❙1"
  shows "group (❙*) ❙1 inv"
proof unfold_locales
  show "⋀a. ❙1 ❙* a = a"
    by simp
next
  show "⋀a. inv a ❙* a = ❙1"
    by (metis left_inverse_if_right_inverse right_inverse)
qed


section ‹Semigroup Action›

text ‹We define both left and right semigroup actions. Left semigroup actions seem to be prevalent
in algebra, but right semigroup actions directly uses the usual notation of term/atom/literal/clause
substitution.›

locale left_semigroup_action = semigroup +
  fixes action :: "'a ⇒ 'b ⇒ 'b" (infix "⋅" 70)
  assumes action_compatibility[simp]: "⋀a b x. (a ❙* b) ⋅ x = a ⋅ (b ⋅ x)"

locale right_semigroup_action = semigroup +
  fixes action :: "'b ⇒ 'a ⇒ 'b" (infix "⋅" 70)
  assumes action_compatibility[simp]: "⋀x a b. x ⋅ (a ❙* b) = (x ⋅ a) ⋅ b"

text ‹We then instantiate the right action in the context of the left action in order to get access
to any lemma proven in the context of the other locale. We do analogously in the context of the
right locale.›

sublocale left_semigroup_action ⊆ right: right_semigroup_action where
  f = "λx y. f y x" and action = "λx y. action y x"
proof unfold_locales
  show "⋀a b c. c ❙* (b ❙* a) = c ❙* b ❙* a"
    by (simp only: assoc)
next
  show "⋀x a b. (b ❙* a) ⋅ x = b ⋅ (a ⋅ x)"
    by simp
qed

sublocale right_semigroup_action ⊆ left: left_semigroup_action where
  f = "λx y. f y x" and action = "λx y. action y x"
proof unfold_locales
  show "⋀a b c. c ❙* (b ❙* a) = c ❙* b ❙* a"
    by (simp only: assoc)
next
  show "⋀a b x. x ⋅ (b ❙* a) = (x ⋅ b) ⋅ a"
    by simp
qed

lemma (in right_semigroup_action) lifting_semigroup_action_to_set:
  "right_semigroup_action (❙*) (λX a. (λx. action x a) ` X)"
proof unfold_locales
  show "⋀x a b. (λx. x ⋅ (a ❙* b)) ` x = (λx. x ⋅ b) ` (λx. x ⋅ a) ` x"
    by (simp add: image_comp)
qed

lemma (in right_semigroup_action) lifting_semigroup_action_to_list:
  "right_semigroup_action (❙*) (λxs a. map (λx. action x a) xs)"
proof unfold_locales
  show "⋀x a b. map (λx. x ⋅ (a ❙* b)) x = map (λx. x ⋅ b) (map (λx. x ⋅ a) x)"
    by (simp add: image_comp)
qed


section ‹Monoid Action›

locale left_monoid_action = monoid +
  fixes action :: "'a ⇒ 'b ⇒ 'b" (infix "⋅" 70)
  assumes
    monoid_action_compatibility: "⋀a b x. (a ❙* b) ⋅ x = a ⋅ (b ⋅ x)" and
    action_neutral[simp]: "⋀x. ❙1 ⋅ x = x"

locale right_monoid_action = monoid +
  fixes action :: "'b ⇒ 'a ⇒ 'b" (infix "⋅" 70)
  assumes
    monoid_action_compatibility: "⋀x a b. x ⋅ (a ❙* b) = (x ⋅ a) ⋅ b" and
    action_neutral[simp]: "⋀x. x ⋅ ❙1 = x"

sublocale left_monoid_action ⊆ left_semigroup_action
  by unfold_locales (fact monoid_action_compatibility)

sublocale right_monoid_action ⊆ right_semigroup_action
  by unfold_locales (fact monoid_action_compatibility)

sublocale left_monoid_action ⊆ right: right_monoid_action where
  f = "λx y. f y x" and action = "λx y. action y x"
  by unfold_locales simp_all

sublocale right_monoid_action ⊆ left: left_monoid_action where
  f = "λx y. f y x" and action = "λx y. action y x"
  by unfold_locales simp_all

lemma (in right_monoid_action) lifting_monoid_action_to_set:
  "right_monoid_action (❙*) ❙1 (λX a. (λx. action x a) ` X)"
proof (unfold_locales)
  show "⋀x a b. (λx. x ⋅ (a ❙* b)) ` x = (λx. x ⋅ b) ` (λx. x ⋅ a) ` x"
    by (simp add: image_comp)
next
  show "⋀x. (λx. x ⋅ ❙1) ` x = x"
    by simp
qed

lemma (in right_monoid_action) lifting_monoid_action_to_list:
  "right_monoid_action (❙*) ❙1 (λxs a. map (λx. action x a) xs)"
proof unfold_locales
  show "⋀x a b. map (λx. x ⋅ (a ❙* b)) x = map (λx. x ⋅ b) (map (λx. x ⋅ a) x)"
    by simp
next
  show "⋀x. map (λx. x ⋅ ❙1) x = x"
    by simp
qed


section ‹Group Action›

locale left_group_action = group +
  fixes action :: "'a ⇒ 'b ⇒ 'b" (infix "⋅" 70)
  assumes
    group_action_compatibility: "⋀a b x. (a ❙* b) ⋅ x = a ⋅ (b ⋅ x)" and
    group_action_neutral: "⋀x. ❙1 ⋅ x = x"

locale right_group_action = group +
  fixes action :: "'b ⇒ 'a ⇒ 'b" (infixl "⋅" 70)
  assumes
    group_action_compatibility: "⋀x a b. x ⋅ (a ❙* b) = (x ⋅ a) ⋅ b" and
    group_action_neutral: "⋀x. x ⋅ ❙1 = x"

sublocale left_group_action ⊆ left_monoid_action
  by unfold_locales (fact group_action_compatibility group_action_neutral)+

sublocale right_group_action ⊆ right_monoid_action
  by unfold_locales (fact group_action_compatibility group_action_neutral)+

sublocale left_group_action ⊆ right: right_group_action where
  f = "λx y. f y x" and action = "λx y. action y x"
  by unfold_locales simp_all

sublocale right_group_action ⊆ left: left_group_action where
  f = "λx y. f y x" and action = "λx y. action y x"
  by unfold_locales simp_all


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)

(* This corresponds to the maximal subgroup of the monoid on (⊙) and id_subst *)
definition is_renaming :: "'s ⇒ bool" where
  "is_renaming ρ ⟷ (∃ρ_inv. ρ ⊙ ρ_inv = id_subst)"

definition renaming_inverse where
  "is_renaming ρ ⟹ renaming_inverse ρ = (SOME ρ_inv. ρ ⊙ ρ_inv = id_subst)"

lemma renaming_comp_renaming_inverse[simp]:
  "is_renaming ρ ⟹ ρ ⊙ renaming_inverse ρ = id_subst"
  by (auto simp: is_renaming_def renaming_inverse_def intro: someI_ex)

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 ⟶ μ ⊙ τ = τ)"

definition is_idem :: "'s ⇒ bool" where
  "is_idem σ ⟷ σ ⊙ σ = σ"

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_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›

(* Rename to abstract substitution *)
locale substitution =
  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 "⋅" 70) 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_renaming_id_subst[simp]: "is_renaming id_subst"
  by (simp add: is_renaming_def)

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_idem_id_subst[simp]: "is_idem id_subst"
  by (simp add: is_idem_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


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 subst_mgu_eq_subst_mgu: 
  assumes "is_mgu μ {{t⇩1, t⇩2}}" 
  shows "t⇩1 ⋅ μ = t⇩2 ⋅ μ"
  using assms is_unifier_iff_if_finite[of "{t⇩1, t⇩2}"]
  unfolding is_mgu_def is_unifier_set_def
  by blast

lemma subst_imgu_eq_subst_imgu: 
  assumes "is_imgu μ {{t⇩1, t⇩2}}" 
  shows "t⇩1 ⋅ μ = t⇩2 ⋅ μ"
  using assms is_unifier_iff_if_finite[of "{t⇩1, t⇩2}"]
  unfolding is_imgu_def is_unifier_set_def
  by blast


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: comp_subst.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