Theory Abstract_Substitution.Substitution

theory Substitution ✐‹contributor ‹Balazs Toth›› 
  imports
    Abstract_Substitution
    "HOL-Library.FSet"
    Option_Extra
begin

section ‹Substitutions on variables›

locale substitution = abstract_substitution where
  subst = subst and is_ground = "λexpr. vars expr = {}"
for
  subst :: "'expr ⇒ 'subst ⇒ 'expr" (infixl "⋅" 69) and
  apply_subst :: "'v ⇒ 'subst ⇒ 'base" (infixl "⋅v" 69) and
  subst_update :: "'subst ⇒ 'v ⇒ 'base ⇒ 'subst" (‹_⟦_ := _⟧› [1000, 0, 50] 71) and
  vars :: "'expr ⇒ 'v set" +
assumes
  (* Interesting that not both directions are required *)
  subst_eq: "⋀expr σ τ. (⋀x. x ∈ vars expr ⟹ x ⋅v σ = x ⋅v τ) ⟹ expr ⋅ σ = expr ⋅ τ" and
  subst_update [simp]:
    "⋀x update. x ⋅v σ⟦x := update⟧ = update" 
    "⋀x y update. x ≠ y ⟹ x ⋅v σ⟦y := update⟧ = x ⋅v σ"
begin

abbreviation is_ground where "is_ground expr ≡ vars expr = {}"

definition vars_set :: "'expr set ⇒ 'v set" where
  "vars_set exprs ≡ ⋃expr ∈ exprs. vars expr"

lemma subst_reduntant_upd [simp]:
  assumes "x ∉ vars expr"
  shows "expr ⋅ σ⟦x := update⟧ = expr ⋅ σ"
  using assms subst_eq subst_update
  by metis

lemma subst_cannot_unground:
  assumes "¬is_ground (expr ⋅ σ)"
  shows "¬is_ground expr"
  using assms 
  by force

abbreviation (input) var_subst where
  "var_subst σ x ≡ x ⋅v σ"

abbreviation (input) expr_subst where
  "expr_subst σ expr ≡ expr ⋅ σ"

definition subst_domain :: "'subst ⇒ 'v set" where
  "subst_domain σ = {x. x ⋅v σ ≠ x ⋅v id_subst}"

abbreviation subst_range :: "'subst ⇒ 'base set" where
  "subst_range σ ≡ var_subst σ ` subst_domain σ"

lemma subst_inv:
  assumes "σ ⊙ σ_inv = id_subst"
  shows "expr ⋅ σ ⋅ σ_inv = expr"
  using assms
  by (metis subst_comp_subst subst_id_subst)

definition rename where
  "is_renaming ρ ⟹ rename ρ x ≡ SOME x'. x ⋅v ρ = x' ⋅v id_subst"

lemma is_unifier_two_iff [simp]: "is_unifier υ {expr, expr'} ⟷ expr ⋅ υ = expr' ⋅ υ"
  unfolding is_unifier_def
  using insertCI
  by fastforce

lemma is_unifier_set_two_iff [simp]: "is_unifier_set υ {{expr, expr'}} ⟷ expr ⋅ υ = expr' ⋅ υ"
  unfolding is_unifier_set_def
  by simp

lemma obtain_imgu_absorption: 
  assumes "is_unifier_set υ XX" "is_imgu μ XX" 
  obtains σ where "υ = μ ⊙ σ"
  using assms
  unfolding is_imgu_def
  by metis

end


subsection ‹Properties of substitutions›

locale all_subst_ident_iff_ground =
  substitution +
  assumes all_subst_ident_iff_ground: "⋀expr. is_ground expr ⟷ (∀σ. expr ⋅ σ = expr)"

locale exists_non_ident_subst =
  substitution where vars = vars
  for vars :: "'expr ⇒ 'v set" +
  assumes
    exists_non_ident_subst:
      "⋀expr S. finite S ⟹ ¬is_ground expr ⟹ ∃σ. expr ⋅ σ ≠ expr ∧ expr ⋅ σ ∉ S"
begin

lemma infinite_expr:
  assumes "∃expr. vars expr ≠ {}"
  shows "infinite (UNIV :: 'expr set)"
proof 
  assume finite: "finite (UNIV :: 'expr set)"

  obtain expr where expr: "vars expr ≠ {}"
    using assms
    by metis

  show False
    using exists_non_ident_subst[OF finite expr]
    by simp
qed

end

locale finite_variables = substitution where vars = vars
  for vars :: "'expr ⇒ 'v set" +
  assumes finite_vars [intro]: "⋀expr. finite (vars expr)"
begin

abbreviation finite_vars :: "'expr ⇒ 'v fset" where
  "finite_vars expr ≡ Abs_fset (vars expr)"

lemma fset_finite_vars [simp]: "fset (finite_vars expr) = vars expr"
  using Abs_fset_inverse finite_vars
  by blast

end

locale infinite_variables = substitution where vars = vars
  for vars :: "'expr ⇒ 'v set" +
  assumes infinite_vars [intro]: "infinite (UNIV :: 'v set)"

locale renaming_variables = substitution +
  assumes
    is_renaming_iff:
      "⋀ρ. is_renaming ρ ⟷ inj (var_subst ρ) ∧ (∀x. ∃x'. x ⋅v ρ = x' ⋅v id_subst)" and
    rename_variables: "⋀expr ρ. is_renaming ρ ⟹ vars (expr ⋅ ρ) = rename ρ ` (vars expr)"
begin

lemma renaming_range_id_subst:
  assumes "is_renaming ρ"
  shows "x ⋅v ρ ∈ range (var_subst id_subst)"
  using assms
  unfolding is_renaming_iff
  by auto

lemma obtain_renamed_variable:
  assumes "is_renaming ρ"
  obtains x' where "x ⋅v ρ = x' ⋅v id_subst"
  using renaming_range_id_subst[OF assms]
  by auto

lemma id_subst_rename [simp]:
  assumes "is_renaming ρ"
  shows "rename ρ x ⋅v id_subst = x ⋅v ρ"
  unfolding rename_def[OF assms]
  using obtain_renamed_variable[OF assms]
  by (metis (mono_tags, lifting) someI)

lemma rename_variables_id_subst: 
  assumes "is_renaming ρ" 
  shows "var_subst id_subst ` vars (expr ⋅ ρ) = var_subst ρ ` (vars expr)"
  using rename_variables[OF assms] id_subst_rename[OF assms]
  by (smt (verit, best) image_cong image_image)

lemma surj_inv_renaming:
  assumes "is_renaming ρ"
  shows "surj (λx. inv (var_subst ρ) (x ⋅v id_subst))"
  using assms inv_f_f
  unfolding is_renaming_iff surj_def
  by metis

lemma renaming_range:
  assumes "is_renaming ρ" "x ∈ vars (expr ⋅ ρ)"
  shows "x ⋅v id_subst ∈ range (var_subst ρ)"
  using rename_variables_id_subst[OF assms(1)] assms(2)
  by fastforce

lemma renaming_inv_into:
  assumes "is_renaming ρ" "x ∈ vars (expr ⋅ ρ)"
  shows "inv (var_subst ρ) (x ⋅v id_subst) ⋅v ρ = x ⋅v id_subst"
  using f_inv_into_f[OF renaming_range[OF assms]].

lemma inv_renaming:
  assumes "is_renaming ρ"
  shows "inv (var_subst ρ) (x ⋅v ρ)  = x"
  using assms
  unfolding is_renaming_iff
  by (simp add: inv_into_f_eq)

lemma renaming_inv_in_vars:
  assumes "is_renaming ρ" "x ∈ vars (expr ⋅ ρ)"
  shows "inv (var_subst ρ) (x ⋅v id_subst) ∈ vars expr"
  using assms rename_variables_id_subst[OF assms(1)]
  by (metis image_eqI image_inv_f_f is_renaming_iff)

lemma inj_id_subst: "inj (var_subst id_subst)"
  using is_renaming_id_subst is_renaming_iff
  by blast

end

locale grounding = substitution where vars = vars and id_subst = id_subst
  for vars :: "'expr ⇒ 'var set" and id_subst :: "'subst" +
  fixes to_ground :: "'expr ⇒ 'expr⇩G" and from_ground :: "'expr⇩G ⇒ 'expr"
  assumes
    range_from_ground_iff_is_ground: "{expr. is_ground expr} = range from_ground" and
    from_ground_inverse [simp]: "⋀expr⇩G. to_ground (from_ground expr⇩G) = expr⇩G"
begin

definition ground_instances' ::"'expr ⇒ 'expr⇩G set" where
  "ground_instances' expr = { to_ground (expr ⋅ γ) | γ. is_ground (expr ⋅ γ) }"

lemma ground_instances'_eq_ground_instances: 
  "ground_instances' expr = (to_ground ` ground_instances expr)"
  unfolding ground_instances'_def ground_instances_def generalizes_def instances_def 
  by blast

lemma to_ground_from_ground_id [simp]: "to_ground ∘ from_ground = id"
  using from_ground_inverse
  by auto

lemma surj_to_ground: "surj to_ground"
  using from_ground_inverse
  by (metis surj_def)

lemma inj_from_ground: "inj_on from_ground domain⇩G"
  by (metis from_ground_inverse inj_on_inverseI)

lemma inj_on_to_ground: "inj_on to_ground (from_ground ` domain⇩G)"
  unfolding inj_on_def
  by simp

lemma bij_betw_to_ground: "bij_betw to_ground (from_ground ` domain⇩G) domain⇩G"
  by (smt (verit, best) bij_betwI' from_ground_inverse image_iff)

lemma bij_betw_from_ground: "bij_betw from_ground domain⇩G (from_ground ` domain⇩G)"
  by (simp add: bij_betw_def inj_from_ground)

lemma ground_is_ground [simp, intro]: "is_ground (from_ground expr⇩G)"
  using range_from_ground_iff_is_ground
  by blast

lemma is_ground_iff_range_from_ground: "is_ground expr ⟷ expr ∈ range from_ground"
  using range_from_ground_iff_is_ground
  by auto

lemma to_ground_inverse [simp]:
  assumes "is_ground expr"
  shows "from_ground (to_ground expr) = expr"
  using inj_on_to_ground from_ground_inverse is_ground_iff_range_from_ground assms
  unfolding inj_on_def
  by blast

corollary obtain_grounding:
  assumes "is_ground expr"
  obtains expr⇩G where "from_ground expr⇩G = expr"
  using to_ground_inverse assms
  by blast

lemma from_ground_eq [simp]:
  "from_ground expr = from_ground expr' ⟷ expr = expr'"
  by (metis from_ground_inverse)

lemma to_ground_eq [simp]:
  assumes "is_ground expr" "is_ground expr'"
  shows "to_ground expr = to_ground expr' ⟷ expr = expr'"
  using assms obtain_grounding
  by fastforce

end

locale exists_ground_subst = substitution +
  assumes exists_ground_subst: "∃γ. is_ground_subst γ"
begin

lemma obtain_ground_subst:
  obtains γ where "is_ground_subst γ"
  using exists_ground_subst
  by metis

lemma ground_exists: "∃expr. is_ground expr"
proof -
  fix expr

  obtain γ where γ: "is_ground_subst γ"
    using obtain_ground_subst .

  show "∃expr. is_ground expr"
  proof (rule exI)
    show "is_ground (expr ⋅ γ)"
      using γ is_ground_subst_is_ground
      by blast
  qed
qed

lemma ground_subst_extension:
  assumes "is_ground (expr ⋅ γ)"
  obtains γ'
  where "expr ⋅ γ = expr ⋅ γ'" and "is_ground_subst γ'"
  using obtain_ground_subst assms
  by (metis all_subst_ident_if_ground is_ground_subst_comp_right subst_comp_subst)

end

locale subst_updates = substitution where vars = vars and apply_subst = apply_subst
 for
    vars :: "'expr ⇒ 'v set" and
    apply_subst :: "'v ⇒ 'subst ⇒ 'base"  (infixl ‹⋅v› 69) +
  fixes subst_updates :: "'subst ⇒ ('v ⇀ 'base) ⇒ 'subst" 
  assumes
    subst_updates [simp]: "⋀x. x ⋅v subst_updates σ update = get_or (update x) (x ⋅v σ)"

locale exists_imgu = substitution +
  assumes exists_imgu: "⋀υ expr expr'. expr ⋅ υ = expr' ⋅ υ ⟹ ∃μ. is_imgu μ {{expr, expr'}}"
begin

lemma obtains_imgu:
  assumes "expr ⋅ υ = expr' ⋅ υ"
  obtains μ where "is_imgu μ {{expr, expr'}}"
  using exists_imgu[OF assms]
  by metis

lemma exists_imgu_set:
  assumes finite_X: "finite X" and unifier: "is_unifier υ X" 
  shows "∃μ. is_imgu μ {X}"
  using assms
proof (cases X)
  case emptyI

  then show ?thesis
    using is_imgu_id_subst is_unifier_id_subst is_unifier_id_subst_empty
    by blast
next
  case (insertI X' x)

  then have "X ≠ {}"
    by simp

  with finite_X show ?thesis
    using unifier
  proof (induction X rule: finite_ne_induct)
    case (singleton x)

    then show ?case
      using is_imgu_id_subst_empty is_imgu_insert_singleton 
      by blast
  next
    case (insert expr X')

    then obtain μ where μ: "is_imgu μ {X'}"
      by (meson finite_insert is_unifier_subset subset_insertI)

    then have "card (subst_set X' μ) = 1"
      by (simp add: is_imgu_def is_unifier_def subst_set_def insert is_unifier_set_insert le_Suc_eq)

    then obtain expr' where X'_μ: "subst_set X' μ = {expr'}"
      using card_1_singletonE
      by blast

    then have expr': "⋀expr. expr ∈ X' ⟹ expr ⋅ μ = expr'"
      unfolding subst_set_def
      by auto

    have μ_absorbs_τ: "⋀expr. expr ⋅ μ ⋅ υ =  expr ⋅ υ"
        using μ insert.prems insert.hyps(1)
        unfolding is_imgu_def is_unifier_set_def
        by (metis comp_subst.left.monoid_action_compatibility finite_insert is_unifier_subset
            singletonD subset_insertI)

    obtain μ' where μ': "is_imgu μ' {{expr ⋅ μ, expr'}}"
    proof (rule obtains_imgu)

      obtain expr'' where "expr'' ∈ X'"
        using insert.hyps(2) by auto

      moreover then have expr': "expr' = expr'' ⋅ μ"
        using expr'
        by presburger

      ultimately show "expr ⋅ μ ⋅ υ = expr' ⋅ υ"
        using μ_absorbs_τ
        unfolding expr'
        by (metis finite.insertI insert.hyps(1) insert.prems insertI1 insertI2
            is_unifier_iff_if_finite)
    qed

    define μ'' where "μ'' = μ ⊙ μ'"

    show ?case 
    proof (rule exI)

      show "is_imgu μ'' {insert expr X'}"
      proof (unfold is_imgu_def, intro conjI allI impI)

        show "is_unifier_set μ'' {insert expr X'}"
          using μ'
          unfolding μ''_def 
          by (simp add: is_unifier_iff_if_finite is_unifier_set_insert expr' insert.hyps(1)
              subst_imgu_eq_subst_imgu)
      next
        fix τ
        assume "is_unifier_set τ {insert expr X'}"

        moreover then have "is_unifier_set τ {{expr ⋅ μ, expr'}}"
          using μ 
          unfolding is_imgu_def is_unifier_set_insert
          by (metis X'_μ is_unifier_subset subst_set_insert finite_insert insert.hyps(1) 
              is_unifier_def subset_insertI subst_set_comp_subst)

        ultimately show "μ'' ⊙ τ = τ"
          using μ μ'
          unfolding μ''_def is_imgu_def is_unifier_set_insert
          by (metis finite.insertI insert.hyps(1) is_unifier_subset assoc subset_insertI)
      qed
    qed
  qed
qed

lemma exists_imgu_sets:
  assumes finite_XX: "finite XX" and finite_X: "∀X∈XX. finite X" and unifier: "is_unifier_set υ XX"
  shows "∃μ. is_imgu μ XX"
using finite_XX finite_X unifier
proof (induction XX rule: finite_induct)
  case empty

  then show ?case
    by (metis is_imgu_id_subst_empty)
next
  case (insert X XX)

  obtain μ where μ: "is_imgu μ XX" 
    using insert.IH insert.prems is_unifier_set_insert
    by force

  define X_μ where "X_μ = subst_set X μ"

  then obtain μ' where μ': "is_imgu μ' {X_μ}" 
  proof -
    have "finite X_μ"
      unfolding X_μ_def subst_set_def
      using insert.prems(1)
      by simp

    moreover have "μ ⊙ υ = υ"
      using μ insert.prems(2)
      unfolding is_imgu_def is_unifier_set_def
      by blast

    then have "is_unifier υ X_μ"
      using insert.prems(2)
      unfolding is_unifier_set_def is_unifier_def X_μ_def
      by (metis insertCI subst_set_comp_subst)

    ultimately show ?thesis
      using that exists_imgu_set
      by blast
  qed

  define μ'' where "μ'' = μ ⊙ μ'"

  show ?case
  proof (unfold is_imgu_def, intro exI conjI allI impI)

    show "is_unifier_set μ'' (insert X XX)"
      using μ μ' insert.prems(1) is_unifier_iff_if_finite
      unfolding μ''_def is_imgu_def X_μ_def is_unifier_def is_unifier_set_def 
      by (smt (verit, best) comp_subst.left.monoid_action_compatibility insert_iff
          subst_set_comp_subst)
  next
    fix τ
    assume "is_unifier_set τ (insert X XX)"

    then show "μ'' ⊙ τ = τ"
      using μ μ'
      unfolding μ''_def X_μ_def is_imgu_def is_unifier_set_insert is_unifier_def
      by (metis comp_subst.left.assoc is_unifier_set_empty subst_set_comp_subst)
  qed
qed

end

end