Theory Substitution_HOL_ex_Unification

theory Substitution_HOL_ex_Unification
  imports
    Based_Substitution
    "HOL-ex.Unification"
    Fresh_Identifiers.Fresh
begin

section ‹Substitutions for first order terms as binary tree›

no_notation Comb (infix ‹⋅› 60)

quotient_type 'v subst = "('v × 'v trm) list" / "(≐)"
proof (rule equivpI)
  show "reflp (≐)"
    using reflpI subst_refl by metis
next
  show "symp (≐)"
    using sympI subst_sym by metis
next
  show "transp (≐)"
    using transpI subst_trans by metis
qed


subsection ‹Substitution monoid›

lift_definition subst_comp :: "'v subst ⇒ 'v subst ⇒ 'v subst" (infixl ‹⊙› 67)
  is Unification.comp
  using Unification.subst_cong .

lift_definition subst_id :: "'v subst"
  is "[]" .

global_interpretation subst_comp: monoid subst_comp subst_id
proof unfold_locales
  fix σ σ' σ'' :: "'v subst"

  show "σ ⊙ σ' ⊙ σ'' = σ ⊙ (σ' ⊙  σ'')"
    by transfer auto
next
  fix σ :: "'v subst"

  show "subst_id ⊙ σ = σ"
    by transfer simp

  show "σ ⊙ subst_id = σ"
    by transfer simp
qed


subsection ‹Transfer definitions and lemmas from HOL-ex.Unification› ✐‹contributor ‹Balazs Toth›› 

lift_definition subst_apply :: "'v trm ⇒ 'v subst ⇒ 'v trm" (infixl ‹⋅› 61)
  is Unification.subst
  using Unification.subst_eq_dest .

lift_definition subst_domain :: "'v subst ⇒ 'v set"
  is Unification.subst_domain
  by (metis (no_types, lifting) ext subst_domain_def subst_eq_def)

lift_definition range_vars :: "'v subst ⇒ 'v set"
  is Unification.range_vars
  by (metis (no_types, lifting) ext range_vars_def subst_eq_def)

lift_definition Unifier :: "'v subst ⇒ 'v trm ⇒ 'v trm ⇒ bool"
  is Unification.Unifier
  unfolding subst_eq_def Unifier_def
  by auto

lift_definition IMGU :: "'v subst ⇒ 'v trm ⇒ 'v trm ⇒ bool"
  is Unification.IMGU
  unfolding subst_eq_def IMGU_def
  by (simp add: Unification.Unifier_def)

lift_definition unify :: "'v trm ⇒ 'v trm ⇒ 'v subst option"
  is Unification.unify.

lemma unify_eq_Some_if_Unifier:
  assumes "Unifier σ t t'"
  shows "∃τ. unify t t' = Some τ"
proof -
  obtain rep_σ where σ_def: "σ = abs_subst rep_σ"
    by transfer simp

  from assms have "Unification.Unifier rep_σ t t'"
    unfolding σ_def
    by transfer

  then obtain rep_τ where "Unification.unify t t' = Some rep_τ"
    using Unification.unify_eq_Some_if_Unifier
    by blast

  then have "unify t t' = Some (abs_subst rep_τ)"
    by (simp add: unify.abs_eq)

  thus ?thesis
    by blast
qed

lemma unify_computes_IMGU:
  assumes "unify t t' = Some σ"
  shows "IMGU σ t t'"
proof -
  obtain rep_σ where σ_def: "σ = abs_subst rep_σ"
    by transfer simp

  have "map_option abs_subst (Unification.unify t t') = Some (abs_subst rep_σ)"
    using assms σ_def
    by (simp add: unify.abs_eq)

  then obtain rep_σ' where
    "Unification.unify t t' = Some rep_σ'" and
    rep_σ': "abs_subst rep_σ' = abs_subst rep_σ"
    by (cases "Unification.unify t t'") auto

  then have "Unification.IMGU rep_σ' t t'"
    using Unification.unify_computes_IMGU
    by blast

  hence "IMGU (abs_subst rep_σ') t t'"
    by transfer

  thus "IMGU σ t t'"
    using rep_σ' σ_def
    by simp
qed

lift_definition subst_update :: "'v × 'v trm ⇒ 'v subst ⇒ 'v subst"
  is "(#)"
proof -
  fix update and σ σ' :: "('v × 'v trm) list"
  assume subst_eq: "σ ≐ σ'"

  {
    fix t 
    have "t ⊲ update # σ = t ⊲ update # σ'"
    proof (induction t)
      case Var

      then show ?case
        using subst_eq
        unfolding subst_eq_def
        by (metis assoc.simps(2) prod.exhaust subst.simps(1))     
    qed simp_all
  }

  then show "update # σ ≐ update # σ' "
    unfolding subst_eq_def
    by satx
qed


subsection ‹Base Substitution› ✐‹contributor ‹Balazs Toth›› 

global_interpretation "term": base_substitution where
  comp_subst = subst_comp and id_subst = subst_id and subst = subst_apply and vars = vars_of and
  subst_update = "λσ x update. subst_update (x, update) σ" and
  apply_subst = "λx σ. subst_apply (Var x) σ"
proof unfold_locales
  fix t and σ σ' :: "'v subst"

  show "t ⋅ σ ⊙ σ' = t ⋅ σ ⋅ σ'"
    by transfer simp
next
  fix t :: "'v trm"

  show "t ⋅ subst_id = t"
    by transfer simp
next
  fix t :: "'v trm"

  assume "vars_of t = {}"

  then show "∀σ. t ⋅ σ = t"
    by transfer (metis agreement empty_iff subst_Nil)
next
  fix t and σ τ :: "'v subst"

  assume "⋀x. x ∈ vars_of t ⟹ Var x ⋅ σ = Var x ⋅ τ"

  then show "t ⋅ σ = t ⋅ τ"
    by (simp add: agreement subst_apply.rep_eq)
next
  fix σ x and update :: "'v trm"
  
  show "Var x ⋅ subst_update (x, update) σ = update"
    by transfer simp
next
  fix σ :: "'v subst" and x y :: 'v and update
  assume "x ≠ y"

  then show "Var x ⋅ subst_update (y, update) σ = Var x ⋅ σ"
    by transfer simp
next
  fix x :: 'v

  show "vars_of (Var x ⋅ subst_id) = {x}"
    by transfer simp
next
  fix σ σ' :: "'v subst" and x

  show "Var x ⋅ σ ⊙ σ' = Var x ⋅ σ ⋅ σ'"
    by transfer simp
next
  fix t and σ :: "'v subst"

  show "vars_of (t ⋅ σ) = ⋃ (vars_of ` (λx. Var x ⋅ σ) ` vars_of t)"
    by transfer (simp add: vars_of_subst_conv_Union)
qed


subsection ‹Substitution Properties› ✐‹contributor ‹Balazs Toth›› 

global_interpretation "term": finite_variables where
  comp_subst = subst_comp and id_subst = subst_id and subst = subst_apply and vars = vars_of and
  subst_update = "λσ x update. subst_update (x, update) σ" and
  apply_subst = "λx σ. subst_apply (Var x) σ"
proof unfold_locales
  fix t :: "'v trm"

  show "finite (vars_of t)"
    by blast
qed

text‹We could also prove @{locale all_subst_ident_iff_ground} and
     @{locale exists_non_ident_subst} directly without needing infinite variables.›
global_interpretation "term": base_exists_non_ident_subst where
  comp_subst = subst_comp and id_subst = "subst_id :: 'v :: infinite subst" and
  subst = subst_apply and vars = vars_of and
  subst_update = "λσ x update. subst_update (x, update) σ" and
  apply_subst = "λx σ. subst_apply (Var x) σ"
proof unfold_locales
  fix t :: "'v trm"
  
  show "term.is_ground t = (∀σ. t ⋅ σ = t)"
    by transfer (metis agreement all_not_in_conv remove_var subst_Nil vars_of.simps(2))
   
next

  show "infinite (UNIV :: 'v set)"
    using infinite_UNIV
    by simp
qed


subsection ‹Compatibility with HOL-ex.Unification› ✐‹contributor ‹Balazs Toth›› 

lemma subst_domain_eq_term_subst_domain [simp]: "subst_domain σ = term.subst_domain σ"
  unfolding term.subst_domain_def 
  by transfer (simp add: Unification.subst_domain_def)

lemma range_vars_eq_term_range_vars [simp]: "range_vars σ = term.range_vars σ"
  unfolding term.range_vars_def subst_domain_eq_term_subst_domain[symmetric]
  by transfer (auto simp: Unification.range_vars_def Unification.subst_domain_def)

lemma Unifier_iff_term_is_unifier:
   "Unifier μ t t' ⟷ term.is_unifier μ {t, t'}"
  unfolding term.is_unifier_def term.subst_set_def
  by transfer (use Unification.Unifier_def subset_singleton_iff in fastforce)

lemma Unifier_iff_is_unifier_set:
   "Unifier μ t t' ⟷ term.is_unifier_set μ {{t, t'}}"
  using Unifier_iff_term_is_unifier
  unfolding term.is_unifier_set_def
  by auto

lemma IMGU_iff_term_is_mgu:
  "IMGU μ t t' ⟷ term.is_imgu μ {{t, t'}}" 
  unfolding term.is_imgu_def Unifier_iff_is_unifier_set[symmetric]
  by transfer (meson Unification.IMGU_def subst_sym)

lemma IMGU_range_vars_subset:
  assumes "IMGU μ t u"
  shows "range_vars μ ⊆ vars_of t ∪ vars_of u"
  using assms
  by transfer (rule IMGU_range_vars_subset)


subsection ‹Interpretations for IMGUs› ✐‹contributor ‹Balazs Toth›› 

text‹We could also prove @{locale range_vars_subset_if_is_imgu}
     without needing infinite variables.›
global_interpretation "term": base_variables_in_base_imgu where
  comp_subst = subst_comp and id_subst = "subst_id :: 'v :: infinite subst" and
  subst = subst_apply and vars = vars_of and
  subst_update = "λσ x update. subst_update (x, update) σ" and
  apply_subst = "λx σ. subst_apply (Var x) σ"
proof(unfold_locales, transfer)
  fix t :: "'v trm" and σ

  show "∃x. t ⊲ σ = Var x ⊲ [] ⟹ ∃x. t = Var x ⊲ []"
    using subst_apply_eq_Var 
    by fastforce
qed

global_interpretation "term": exists_imgu where
  comp_subst = subst_comp and id_subst = subst_id and subst = subst_apply and vars = vars_of and
  subst_update = "λσ x update. subst_update (x, update) σ" and
  apply_subst = "λx σ. subst_apply (Var x) σ"
proof unfold_locales
  fix υ and t t' :: "'v trm"
  assume "t ⋅ υ = t' ⋅ υ"

  then have "Unifier υ t t'"
    by transfer (simp add: Unification.Unifier_def)

  then obtain μ where "unify t t' = Some μ"
    using unify_eq_Some_if_Unifier by blast

  then have IMGU: "IMGU μ t t'"
    by (simp add: unify_computes_IMGU)

  show "∃μ. term.is_imgu μ {{t, t'}}"
  proof (rule exI)

    show "term.is_imgu μ {{t, t'}}"
      using IMGU IMGU_iff_term_is_mgu 
      by auto
  qed
qed
  
end