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

abbreviation (input) is_ground where
  "is_ground t ≡ vars_of t = {}"

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
  apply_subst = "λx σ. subst_apply (Var x) σ" and is_ground = is_ground
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 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)
next
  fix t and γ :: "'v subst"
  assume "is_ground (t ⋅ γ)"

  then show "∀x∈vars_of t. is_ground (Var x ⋅ γ)"
    by transfer (metis occs_vars_subset subset_empty subst_mono vars_iff_occseq)
qed simp


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

global_interpretation "term": based_subst_update where
  comp_subst = subst_comp and id_subst = subst_id and subst = subst_apply and vars = vars_of and
  is_ground = is_ground and apply_subst = "λx σ. subst_apply (Var x) σ" and
  subst_update = "λσ x update. subst_update (x, update) σ" and
  base_subst = subst_apply and base_vars = vars_of and base_is_ground = is_ground
proof unfold_locales
  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" and t update and σ :: "'v subst"
  assume "x ∉ vars_of t"

  then show "t ⋅ subst_update (x, update) σ = t ⋅ σ"
    by transfer (simp add: repl_invariance)
next
  fix σ :: "'v subst" and x

  show "subst_update (x, Var x ⋅ σ) σ = σ"
    by transfer (simp add: agreement subst_eq_intro)
next
  fix σ  :: "'v subst" and x a b

  show "subst_update (x, b)(subst_update (x, a) σ) = subst_update (x, b) σ"
    by transfer (simp add: agreement subst_eq_def)
next
  fix γ :: "'v subst" and u t :: "'v trm" and x
  assume "is_ground u" "is_ground (t ⋅ γ)" "x ∈ vars_of t"

  then show "is_ground (t ⋅ subst_update (x, u) γ)"
  proof (induction t)
    case (Var x')
    
    then show ?case
      by transfer simp
  next
    case (Const x')

    then show ?case 
      by transfer simp
  next
    case (Comb t1 t2)

    then show ?case
      by transfer (fastforce simp: repl_invariance)
  qed
qed

global_interpretation "term": finite_variables where
  comp_subst = subst_comp and id_subst = subst_id and subst = subst_apply and vars = vars_of and
  apply_subst = "λx σ. subst_apply (Var x) σ" and is_ground = is_ground
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 is_ground = is_ground 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 "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

global_interpretation "term": renaming_variables where
  comp_subst = subst_comp and id_subst = "subst_id :: 'v subst" and
  subst = subst_apply and vars = vars_of and is_ground = is_ground and
  apply_subst = "λx σ. subst_apply (Var x) σ" 
proof (unfold_locales, intro conjI)
  fix ρ :: "'v subst" and t
  assume ρ: "term.is_renaming ρ"

  then show "inj (λx. Var x ⋅ ρ)"
    unfolding inj_def term.is_renaming_def
    by (metis term.subst_inv trm.inject(1))

  show rename: "∀x. ∃x'. Var x ⋅ ρ = Var x' ⋅ subst_id"
    using ρ term.subst_inv term.comp_subst_iff
    unfolding term.is_renaming_def subst_apply.rep_eq 
    by (metis subst_apply_eq_Var)

  show "vars_of (t ⋅ ρ) = term.rename ρ ` vars_of t"
  proof (induction t)
    case (Var y)

    have "Var y ⋅ ρ = Var (term.rename ρ y)"
      using rename someI_ex[of "λx'. Var y ⋅ ρ = Var x' ⋅ subst_id"] 
      unfolding term.rename_def[OF ρ]
      by auto

    then show ?case
      by simp
  next
    case (Const c)

    then show ?case
      by auto
  next
    case (Comb t1 t2)

    then show ?case
      by (simp add: image_Un subst_apply.rep_eq)
  qed
qed

text‹@{locale subst_updates} just works with this representation if we have finitely many variables›
definition subst_updates_list_finite ::
  "('v :: enum × 'v trm) list ⇒ ('v ⇀ 'v trm) ⇒ ('v × 'v trm) list" where
  "subst_updates_list_finite σ update = (map (λx. (x, get_or (update x) (Var x ⊲ σ))) (Enum.enum))"

lift_definition subst_updates_finite ::
  "('v :: enum) subst ⇒ ('v ⇀ 'v trm) ⇒ 'v subst" (‹_⟦_⟧› [1000, 0] 71)
  is "subst_updates_list_finite" 
  unfolding subst_updates_list_finite_def Unification.subst_eq_def
  by presburger

lemma assoc_map_enum:
  fixes g :: "'v::enum ⇒ 'b"
  shows "assoc x d (map (λy. (y, g y)) Enum.enum) = g x"
proof -

  have "x ∈ set (Enum.enum :: 'v list)"
    by (simp add: Enum.enum_UNIV)

  then obtain xs ys where enum_split: "Enum.enum = xs @ x # ys"
    by (meson split_list)

  have "distinct (Enum.enum :: 'v list)"
    by (rule enum_distinct)

  then have "distinct (xs @ x # ys)"
    unfolding enum_split .

  then have "x ∉ set xs"
    by simp

  then show ?thesis
    unfolding enum_split
    by (induction xs arbitrary: d) auto
qed

(* TODO: Would this be the better representation for the locale assumption? *)
lemma subst_updates_list_finite_nochange:
  fixes σ :: "('v::enum × 'v trm) list"
  assumes "⋀x. x ∈ vars_of t ⟹ update x = None"
  shows "t ⊲ subst_updates_list_finite σ update = t ⊲ σ"
  using assms
proof (induction t)
  case (Var x)
  then show ?case
    unfolding subst_updates_list_finite_def
    by (simp add: assoc_map_enum)
next
  case (Const c)
  show ?case
    by simp
next
  case (Comb t1 t2)

  then show ?case
    by simp
qed


global_interpretation "term": subst_updates where
  comp_subst = subst_comp and id_subst = "subst_id :: 'v :: enum subst" and
  subst = subst_apply and vars = vars_of and is_ground = is_ground and
  apply_subst = "λx σ. subst_apply (Var x) σ"  and subst_updates = subst_updates_finite
proof unfold_locales
  fix x update and σ :: "'v :: enum subst"

  show "Var x ⋅ σ⟦update⟧ = get_or (update x) (Var x ⋅ σ)"
  proof transfer
    fix x update and σ :: "('v :: enum × 'v trm) list"

    show "Var x ⊲ subst_updates_list_finite σ update = get_or (update x) (Var x ⊲ σ)"
      unfolding subst_updates_list_finite_def subst.simps assoc_map_enum ..
  qed
next
  fix t b and σ :: "'v :: enum subst"
  
  show "t ⋅ σ⟦λx. if x ∈ vars_of t then None else b x⟧ = t ⋅ σ"
  proof transfer
    fix t b and σ :: "('v :: enum × 'v trm) list"

    let ?update = "(λx. if x ∈ vars_of t then None else b x) :: 'v ⇀ 'v trm"

    show "t ⊲ subst_updates_list_finite σ ?update = t ⊲ σ"
    proof(rule subst_updates_list_finite_nochange)

      show "⋀x. x ∈ vars_of t ⟹ ?update x = None"
        by simp
    qed
  qed
qed

global_interpretation "term": create_renaming where
  comp_subst = subst_comp and id_subst = "subst_id :: 'v :: enum subst" and
  subst = subst_apply and vars = vars_of and is_ground = is_ground and
  apply_subst = "λx σ. subst_apply (Var x) σ"  and subst_updates = subst_updates_finite
proof (unfold_locales, unfold term.is_renaming_def, transfer)
  fix f :: "'v ⇒ 'v"
  assume inj: "inj f"

  let ?ρ  = "subst_updates_list_finite [] (λx. Some (Var (f x) ⊲ []))"
  let ?ρ' = "subst_updates_list_finite [] (λx. Some (Var (inv f x) ⊲ []))"

  show "∃ρ'. ?ρ ◊ ρ' ≐ []"
  proof (rule exI, unfold Unification.subst_eq_def, intro allI)
    fix t

    show "t ⊲ ?ρ ◊ ?ρ' = t ⊲ []"
      by (induction t) (auto simp: subst_updates_list_finite_def assoc_map_enum inj)
  qed
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 is_ground = is_ground 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
  is_ground = is_ground 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