Theory Abstract_Substitution.Based_Substitution

theory Based_Substitution ✐‹contributor ‹Balazs Toth›› 
  imports Substitution
begin

section ‹Substitutions on base expressions›

locale base_substitution = substitution where vars = vars and apply_subst = apply_subst
  for vars :: "'base ⇒ 'v set" and apply_subst :: "'v ⇒ 'subst ⇒ 'base" (infixl ‹⋅v› 69) +
  assumes 
    vars_id_subst [simp]: "⋀x. vars (x ⋅v id_subst) = {x}" and
    comp_subst_iff: "⋀σ σ' x. x ⋅v σ ⊙ σ' = subst (x ⋅v σ) σ'" and
    base_vars_subst: "⋀expr ρ. vars (expr ⋅ ρ) = ⋃ (vars ` var_subst ρ ` vars expr)"

locale based_substitution =
  substitution where vars = vars and apply_subst = "apply_subst :: 'v ⇒ 'subst ⇒ 'base" +
  base: base_substitution where subst = base_subst and vars = base_vars 
for
  base_subst :: "'base ⇒ 'subst ⇒ 'base" and
  base_vars :: "'base ⇒ 'v set" and
  vars :: "'expr ⇒ 'v set"  +
assumes
  ground_subst_iff_base_ground_subst [simp]: "⋀γ. is_ground_subst γ ⟷ base.is_ground_subst γ" and
  vars_subst: "⋀expr ρ. vars (expr ⋅ ρ) = ⋃ (base_vars ` var_subst ρ ` vars expr)"
begin

lemma id_subst_subst [simp]: "base_subst (x ⋅v id_subst) σ = x ⋅v σ"
  by (metis base.comp_subst_iff left_neutral)

lemma vars_id_subst_update: "vars (expr ⋅ id_subst⟦x := b⟧) ⊆ vars expr ∪ base_vars b"
  unfolding fun_upd_def vars_subst
  using subst_update
  by (smt (verit, del_insts) SUP_least UnCI base.vars_id_subst image_iff singletonD subsetI)

lemma is_grounding_iff_vars_grounded:
  "is_ground (expr ⋅ γ) ⟷ (∀x ∈ vars expr. base.is_ground (x ⋅v γ))"
  using vars_subst
  by auto

lemma variable_grounding:
  assumes "is_ground (expr ⋅ γ)" "x ∈ vars expr"
  shows "base.is_ground (x ⋅v γ)"
  using assms is_grounding_iff_vars_grounded
  by blast

definition range_vars :: "'subst ⇒ 'v set" where
  "range_vars σ = ⋃(base_vars ` subst_range σ)"

lemma vars_subst_subset: "vars (expr ⋅ σ) ⊆ (vars expr - subst_domain σ) ∪ range_vars σ"
  unfolding subst_domain_def range_vars_def vars_subst
  using base.vars_id_subst
  by (smt (verit, del_insts) Diff_iff UN_iff UnCI image_iff mem_Collect_eq singletonD subsetI)

lemma ground_subst_update [simp]:
  assumes "base.is_ground update" "is_ground (expr ⋅ γ)"
  shows "is_ground (expr ⋅ γ⟦x := update⟧)"
  using assms is_grounding_iff_vars_grounded
  by (metis subst_update)

end

context base_substitution
begin

sublocale based_substitution
  where base_subst = subst and base_vars = vars
  by unfold_locales (simp_all add: base_vars_subst)

declare ground_subst_iff_base_ground_subst [simp del]

end

hide_fact base_substitution.base_vars_subst


section ‹Properties of substitutions on base expressions›

locale base_exists_ground_subst = 
  base_substitution where
    vars = "vars :: 'base ⇒ 'v set" and apply_subst = "apply_subst  :: 'v ⇒ 'subst ⇒ 'base" +
  subst_updates + 
  assumes
    base_ground_exists: "∃expr. is_ground expr"
begin

lemma redundant_subst_updates [simp]:
  assumes "⋀x. x ∈ vars expr ⟹ update x = None"
  shows "expr ⋅ subst_updates σ update = expr ⋅ σ"
proof (rule subst_eq)
  fix x
  assume "x ∈ vars expr"

  then have "update x = None"
    using assms
    by metis

  then show "x ⋅v subst_updates σ update = x ⋅v σ"
    by simp
qed

lemma redundant_subst_updates_vars_set [simp]:
  assumes "⋀x. x ∈ X ⟹ update x = None"
  shows "(λx. x ⋅v subst_updates σ update) ` X = (λx. x ⋅v σ) ` X"
  using assms subst_updates 
  by auto

lemma redundant_subst_updates_vars_image [simp]:
  assumes "⋀x. x ∈ ⋃(vars ` X) ⟹ update x = None"
  shows "(λexpr. expr ⋅ subst_updates σ update) ` X = (λexpr. expr ⋅ σ) ` X"
  using assms subst_updates 
  by (meson UN_I image_cong redundant_subst_updates)

sublocale exists_ground_subst
proof unfold_locales
   obtain b where is_ground: "is_ground b"
    using base_ground_exists 
    by blast

  define γ :: 'subst where
    "⋀x. γ ≡ subst_updates id_subst (λ_. Some b)"

  show "∃γ. is_ground_subst γ"
  proof (rule exI)
    show "is_ground_subst γ"
      unfolding is_ground_subst_def γ_def
      by (simp add: is_ground is_grounding_iff_vars_grounded)
  qed
qed

end

locale base_exists_non_ident_subst =
  base_substitution where vars = vars + 
  finite_variables where vars = vars +
  infinite_variables where vars = vars +
  all_subst_ident_iff_ground where vars = vars
  for vars :: "'expr ⇒ 'v set" 
begin

sublocale exists_non_ident_subst
proof unfold_locales
  fix expr and S :: "'expr set"
  assume finite_S: "finite S" and vars_not_empty: "vars expr ≠ {}"

  obtain x where x: "x ∈ vars expr"
    using vars_not_empty
    by blast

  have "finite (vars_set S)"
    using finite_S finite_vars
    unfolding vars_set_def
    by blast

  obtain y where y: "y ∉ vars expr" "y ∉ vars_set S"
  proof -

    have "finite (vars_set S)"
      using finite_S finite_vars
      unfolding vars_set_def
      by blast

    then have "finite (vars expr ∪ vars_set S)"
      using finite_vars
      by simp

    then show ?thesis
      using that infinite_vars finite_vars
      by (meson UnCI ex_new_if_finite)
  qed

  define σ where "σ ≡ id_subst⟦x := y ⋅v id_subst⟧"

  show "∃σ. expr ⋅ σ ≠ expr ∧ expr ⋅ σ ∉ S"
  proof (intro exI conjI)

    have y_in_expr_σ: "y ∈ vars (expr ⋅ σ)"
      unfolding σ_def
      using x vars_subst
      by fastforce

    then show "expr ⋅ σ ≠ expr"
      using y
      by metis

    show "expr ⋅ σ ∉ S"
      using y_in_expr_σ y(2)
      unfolding vars_set_def
      by auto
  qed
qed

end

locale variables_in_base_imgu = based_substitution +
  assumes variables_in_base_imgu:
    "⋀expr μ XX.
        base.is_imgu μ XX ⟹ finite XX ⟹ ∀X ∈ XX. finite X ⟹
        vars (expr ⋅ μ) ⊆ vars expr ∪ (⋃(base_vars ` ⋃ XX))"

locale base_variables_in_base_imgu =
  base_substitution where vars = "vars :: 'expr ⇒ 'v set" and
  subst_update = "subst_update :: 'subst ⇒ 'v ⇒ 'expr ⇒ 'subst" + 
  finite_variables +
  infinite_variables +
assumes
  not_back_to_id_subst: "⋀expr σ. ∃x. expr ⋅ σ = x ⋅v id_subst ⟹ ∃x. expr = x ⋅v id_subst"
begin

lemma imgu_subst_domain_subset:
  assumes imgu: "is_imgu μ XX" and finite_X: "∀X∈XX. finite X" and finite_XX: "finite XX"
  shows "subst_domain μ ⊆ ⋃ (vars ` ⋃ XX)"
proof (intro Set.subsetI)
  fix x
  assume "x ∈ subst_domain μ"

  then have x_μ: "x ⋅v μ ≠ x ⋅v id_subst"
    unfolding subst_domain_def
    by auto

  show "x ∈ ⋃ (vars ` ⋃ XX)"
  proof (rule ccontr)
    assume x: "x ∉ ⋃ (vars ` ⋃ XX)"

    define τ where 
      "τ ≡ μ⟦x := x ⋅v id_subst⟧"

    have "x ⋅v μ ⊙ τ ≠ x ⋅v τ"
    proof (cases "∃y. x ⋅v μ = y ⋅v id_subst")
      case True

      then obtain y where y: "x ⋅v μ = y ⋅v id_subst"
        by auto

      then have "x ≠ y"
        using x_μ
        by blast

      moreover have "y ⋅v μ ≠ x ⋅v id_subst"
      proof (rule notI)
        assume "y ⋅v μ = x ⋅v id_subst"

        then show False
          using imgu x_μ
          unfolding is_imgu_def
          by (metis comp_subst_iff id_subst_subst)
      qed

      ultimately show ?thesis
        unfolding comp_subst_iff y τ_def
        by auto
    next
      case False

      then show ?thesis
        unfolding τ_def comp_subst_iff
        using not_back_to_id_subst
        by (metis subst_update(1))
    qed

    then have "μ ⊙ τ ≠ τ"
      by metis

    moreover have "is_unifier_set τ XX"
      using imgu is_imgu_def
      unfolding τ_def is_unifier_set_def is_unifier_def subst_set_def
      using x
      by auto

    ultimately show False
      using imgu
      unfolding is_imgu_def
      by auto
  qed
qed

lemma imgu_subst_domain_finite:
  assumes imgu: "is_imgu μ XX" and finite_X: "∀X∈XX. finite X" and finite_XX: "finite XX"
  shows "finite (subst_domain μ)"
  using imgu_subst_domain_subset[OF assms(1-3)] finite_XX finite_X finite_vars
  by (simp add: finite_subset)

lemma imgu_range_vars_finite:
  assumes imgu: "is_imgu μ XX" and finite_X: "∀X∈XX. finite X" and finite_XX: "finite XX"
  shows "finite (range_vars μ)"
  using imgu_subst_domain_finite[OF assms] finite_vars
  unfolding range_vars_def
  by blast

lemma imgu_range_vars_vars_subset:
  assumes imgu: "is_imgu μ XX" and finite_X: "∀X∈XX. finite X" and finite_XX: "finite XX"
  shows "⋃(vars ` expr_subst μ ` ⋃ XX) ⊆ ⋃ (vars ` ⋃ XX)"
proof (intro Set.subsetI)
  fix y
  assume y: "y ∈ ⋃ (vars ` expr_subst μ ` ⋃ XX)"

  then obtain x where
    x: "x ∈ ⋃(vars ` ⋃ XX)" "y ∈ vars (x ⋅v μ)"
    using vars_subst
    by auto

  show "y ∈ ⋃ (vars ` ⋃ XX)"
  proof (rule ccontr)
    assume y': "y ∉ ⋃ (vars ` ⋃ XX)"

    then have x_neq_y: "x ≠ y"
      using x
      by auto

    obtain z where z: "z ∉ range_vars μ" "z ∉ subst_domain μ"
      using 
        imgu_subst_domain_finite[OF assms]
        imgu_range_vars_finite[OF assms]
        infinite_vars
      by (metis Diff_iff finite_Diff2 infinite_super subsetI)

    define τ where
      "τ ≡ id_subst⟦y := z ⋅v id_subst⟧ ⊙ μ"

    have "x ⋅v μ ⊙ τ ≠ x ⋅v τ"
    proof -

      have "z ∉ vars (x ⋅v μ)"
        using z(1) x(2) x_neq_y
        unfolding range_vars_def subst_domain_def
        by force

      moreover have "z ∈ vars (x ⋅v μ ⋅ id_subst⟦y := z ⋅v id_subst⟧)"
        using x(2) vars_subst
        by fastforce

      then have "z ∈ vars (x ⋅v μ ⋅ id_subst⟦y := z ⋅v id_subst⟧ ⋅ μ)"
        using z(2) vars_subst
        unfolding range_vars_def subst_domain_def
        by fastforce

      ultimately show ?thesis
        using x_neq_y
        unfolding τ_def comp_subst_iff
        by auto
    qed

    then have "μ ⊙ τ ≠ τ"
      by metis

    moreover have "is_unifier_set τ XX"
      using imgu is_imgu_def
      unfolding τ_def is_unifier_set_def is_unifier_def subst_set_def
      using y'
      by auto

    ultimately show False
      using imgu
      unfolding is_imgu_def
      by auto
  qed
qed

lemma range_vars_subset_if_is_imgu:
  assumes "is_imgu μ XX" "∀X∈XX. finite X" "finite XX"
  shows "range_vars μ ⊆ (⋃expr∈⋃XX. vars expr)"
proof -
  have "range_vars μ = (⋃x ∈ subst_domain μ. vars (x ⋅v μ))"
    by (simp add: range_vars_def)

  also have "… ⊆ (⋃(vars ` (λexpr. expr ⋅ μ) ` ⋃ XX))"
    using imgu_subst_domain_subset[OF assms] subsetD vars_subst 
    by fastforce

  also have "… ⊆ (⋃expr∈⋃XX. vars expr)"
    using imgu_range_vars_vars_subset[OF assms] .

  finally show ?thesis .
qed

sublocale variables_in_base_imgu where 
  base_subst = subst and base_vars = vars
  using range_vars_subset_if_is_imgu vars_subst_subset
  by unfold_locales fastforce

end

locale range_vars_subset_if_is_imgu = base_substitution +
  assumes range_vars_subset_if_is_imgu: 
    "⋀μ XX. is_imgu μ XX ⟹ ∀X∈XX. finite X ⟹ finite XX ⟹
        range_vars μ ⊆ (⋃expr∈⋃XX. vars expr)"
begin

sublocale variables_in_base_imgu where 
  base_subst = subst and base_vars = vars
  using range_vars_subset_if_is_imgu vars_subst_subset
  by unfold_locales fastforce

end

end