Theory 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
    ―‹The precondition of the assumption ensures noop substitutions›
    vars_id_subst: "⋀x. exists_nonground ⟹ 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)" and
    base_vars_grounded_if_is_grounding:
      "⋀expr γ. is_ground (expr ⋅ γ) ⟹ ∀x ∈ vars expr. is_ground (x ⋅v γ)"

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 and is_ground = base_is_ground
for
  base_subst :: "'base ⇒ 'subst ⇒ 'base" and
  base_vars :: "'base ⇒ 'v set" and
  vars :: "'expr ⇒ 'v set" and
  base_is_ground +
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)" and
  vars_grounded_if_is_grounding:
    "⋀expr γ. is_ground (expr ⋅ γ) ⟹ ∀x ∈ vars expr. base_is_ground (x ⋅v γ)"
begin

lemma exists_nonground_iff_base_exists_nonground:
  "exists_nonground ⟷ base.exists_nonground"
  by (metis base.is_ground_subst_def base.subst_id_subst ground_subst_iff_base_ground_subst
      is_ground_subst_def subst_id_subst)

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

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

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

lemma vars_id_subst_subset: "base_vars (x ⋅v id_subst) ⊆ {x}"
  using base.vars_id_subst base.no_vars_if_is_ground
  by blast

lemma vars_subst_subset: "vars (expr ⋅ σ) ⊆ (vars expr - subst_domain σ) ∪ range_vars σ"
  unfolding subst_domain_def range_vars_def vars_subst subset_eq
  using base.vars_id_subst
  by (smt (verit, del_insts) DiffI UN_iff UN_simps(10) UnCI base.no_vars_if_is_ground empty_iff
      mem_Collect_eq singleton_iff)

end

context base_substitution
begin

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

declare ground_subst_iff_base_ground_subst [simp del]

end

hide_fact base_substitution.base_vars_subst
hide_fact base_substitution.base_vars_grounded_if_is_grounding


section ‹Properties of substitutions on base expressions›

locale based_subst_update =
  based_substitution + 
  subst_update +
  assumes ground_subst_update_in_vars:
    "⋀update expr γ x. base_is_ground update ⟹ is_ground (expr ⋅ γ) ⟹ x ∈ vars expr ⟹ 
      is_ground (expr ⋅ γ⟦x := update⟧)"
begin

lemma vars_id_subst_update: "vars (expr ⋅ id_subst⟦x := b⟧) ⊆ vars expr ∪ base_vars b"
proof (cases exists_nonground)
  case True
  then show ?thesis
    unfolding vars_subst 
    using subst_update base.vars_id_subst
    by (smt (verit, ccfv_threshold) SUP_least UnCI exists_nonground_iff_base_exists_nonground
        imageE singleton_iff subset_eq subst_update_var(1,2))
next
  case False
  then show ?thesis
    by simp
qed

lemma ground_subst_update [simp]:
  assumes "base_is_ground update" "is_ground (expr ⋅ γ)"
  shows "is_ground (expr ⋅ γ⟦x := update⟧)"
  using assms
proof (cases "x ∈ vars expr")
  case True

  show ?thesis
    using ground_subst_update_in_vars[OF assms True] .
next
  case False

  then show ?thesis
    by (simp add: assms(2))
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 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 and base_is_ground = is_ground
  using range_vars_subset_if_is_imgu vars_subst_subset
  by unfold_locales fastforce

end

(* TODO Try using compactness instead of infinite variables ∃Y ⊆ X. finite Y ∧ (∀τ. is_unifier τ X ⟷ is_unifier τ Y)
 *)
locale base_variables_in_base_imgu =
  base_substitution where vars = "vars :: 'expr ⇒ 'v set" + 
  subst_update + 
  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"
  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 (metis all_subst_ident_if_ground id_subst_subst subst_update_var)
    next
      case False

      then show ?thesis
        unfolding τ_def comp_subst_iff
        using not_back_to_id_subst
        by (metis all_subst_ident_if_ground id_subst_subst subst_update_var(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 imgu] 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 "∀x. x ⋅v μ = x ⋅v id_subst ∨ z ∉ vars (x ⋅v μ)"
        using range_vars_def subst_domain_def z(1)
        by auto

      then have "z ∉ vars (x ⋅v μ)"
        using z(1) x(2) x_neq_y
        unfolding range_vars_def subst_domain_def
        by (metis all_not_in_conv no_vars_if_is_ground singleton_iff vars_id_subst)

      moreover have "z ∈ vars (x ⋅v μ ⋅ id_subst⟦y := z ⋅v id_subst⟧)"
        using x(2) vars_id_subst subst_update_var(1)
        unfolding vars_subst
        by (metis UN_I equals0D imageI insertI1 no_vars_if_is_ground)
       
      then have "z ∈ vars (x ⋅v μ ⋅ id_subst⟦y := z ⋅v id_subst⟧ ⋅ μ)"
        using z(2) vars_id_subst no_vars_if_is_ground
        unfolding range_vars_def subst_domain_def vars_subst
        by fastforce
        
      ultimately show ?thesis
        using x_neq_y
        unfolding τ_def comp_subst_iff
        by (metis id_subst_subst subst_comp_subst subst_update_var(2))
    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(1)] 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 and base_is_ground = is_ground
  using range_vars_subset_if_is_imgu vars_subst_subset
  by unfold_locales fastforce

end

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

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

sublocale exists_ground_subst
proof unfold_locales

  obtain b where is_ground: "is_ground b"
    using base_ground_exists 
    by blast

  define γ :: 'subst where
    "γ ≡ id_subst⟦λ_. Some b⟧"

  have vars: "⋀x. vars (x ⋅v γ) = {}"
    unfolding γ_def
    by (metis is_ground no_vars_if_is_ground option.simps(5) subst_updates(1))

  show "∃γ. is_ground_subst γ"
  proof (rule exI)
    
    show "is_ground_subst γ"
      using vars
      unfolding is_ground_subst_def is_ground_iff_no_vars γ_def vars_subst
      by fast
  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 +
  subst_update where vars = vars +
  is_ground_if_no_vars 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: "¬ is_ground expr"

  obtain x where x: "x ∈ vars expr"
    using is_ground_iff_no_vars vars_not_empty 
    by auto

  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 vars_subst
      using x
      by (metis UN_iff image_eqI singletonI subst_update_var(1) vars_id_subst vars_not_empty)

    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 vars_grounded_iff_is_grounding = base_substitution +
  assumes is_grounding_if_vars_grounded:
    "⋀expr γ. ∀x ∈ vars expr. is_ground (x ⋅v γ) ⟹ is_ground (expr ⋅ γ)"
begin

lemma vars_grounded_iff_is_grounding: "(∀x ∈ vars b. is_ground (x ⋅v γ)) ⟷ is_ground (b ⋅ γ)"
  using is_grounding_if_vars_grounded vars_grounded_if_is_grounding
  by blast

end


end