Theory Functional_Substitution

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

locale functional_substitution = substitution where
  subst = subst and is_ground = "λexpr. vars expr = {}"
  for
    subst :: "'expr ⇒ ('var ⇒ 'base) ⇒ 'expr" (infixl "⋅" 69) and
    vars :: "'expr ⇒ 'var set" +
  assumes
    subst_eq: "⋀expr σ τ. (⋀x. x ∈ vars expr ⟹ σ x = τ x) ⟹ expr ⋅ σ = expr ⋅ τ"
begin

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

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

lemma subst_reduntant_upd [simp]:
  assumes "var ∉ vars expr"
  shows "expr ⋅ σ(var := update) = expr ⋅ σ"
  using assms subst_eq
  by fastforce

lemma subst_reduntant_if [simp]:
  assumes "vars expr ⊆ vars'"
  shows "expr ⋅ (λvar. if var ∈ vars' then σ var else σ' var) = expr ⋅ σ"
  using assms
  by (smt (verit, best) subset_eq subst_eq)

lemma subst_reduntant_if' [simp]:
  assumes "vars expr ∩ vars' = {}"
  shows "expr ⋅ (λvar. if var ∈ vars' then σ' var else σ var) = expr ⋅ σ"
  using assms subst_eq
  unfolding disjoint_iff
  by presburger

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

definition subst_domain :: "('var ⇒ 'base) ⇒ 'var set" where
  "subst_domain σ = {x. σ x ≠ id_subst x}"

abbreviation subst_range :: "('var ⇒ 'base) ⇒ 'base set" where
  "subst_range σ ≡ σ ` 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 = id_subst x'"

end

locale all_subst_ident_iff_ground =
  functional_substitution +
  assumes
    all_subst_ident_iff_ground: "⋀expr. is_ground expr ⟷ (∀σ. subst expr σ = expr)" and
    exists_non_ident_subst:
      "⋀expr S. finite S ⟹ ¬is_ground expr ⟹ ∃σ. subst expr σ ≠ expr ∧ subst expr σ ∉ S"

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

abbreviation finite_vars :: "'expr ⇒ 'var 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 renaming_variables = functional_substitution +
  assumes
    is_renaming_iff: "⋀ρ. is_renaming ρ ⟷ inj ρ ∧ (∀x. ∃x'. ρ x = id_subst x')" and
    rename_variables: "⋀expr ρ. is_renaming ρ ⟹ vars (expr ⋅ ρ) = rename ρ ` (vars expr)"
begin

lemma renaming_range_id_subst:
  assumes "is_renaming ρ"
  shows "ρ x ∈ range id_subst"
  using assms
  unfolding is_renaming_iff
  by auto

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

lemma id_subst_rename [simp]:
  assumes "is_renaming ρ"
  shows "id_subst (rename ρ x) = ρ x"
  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 "id_subst ` vars (expr ⋅ ρ) = ρ ` (vars expr)"
  using rename_variables[OF assms] id_subst_rename[OF assms]
  by (metis (no_types, lifting) image_cong image_image)

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

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

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

lemma inv_renaming:
  assumes "is_renaming ρ"
  shows "inv ρ (ρ x) = x"
  using assms
  unfolding is_renaming_iff
  by simp

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

end

locale grounding = functional_substitution where vars = vars and id_subst = id_subst
  for vars :: "'expr ⇒ 'var set" and id_subst :: "'var ⇒ 'base" +
  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 base_functional_substitution = functional_substitution
  where id_subst = id_subst and vars = vars
  for id_subst :: "'var ⇒ 'expr" and vars :: "'expr ⇒ 'var set" +
  assumes
    vars_subst_vars: "⋀expr ρ. vars (expr ⋅ ρ) = ⋃ (vars ` ρ ` vars expr)" and
    base_ground_exists: "∃expr. is_ground expr" and
    vars_id_subst: "⋀x. vars (id_subst x) = {x}" and
    comp_subst_iff: "⋀σ σ' x. (σ ⊙ σ') x = σ x ⋅ σ'"

locale based_functional_substitution =
  base: base_functional_substitution where subst = base_subst and vars = base_vars +
  functional_substitution where vars = vars
for
  base_subst :: "'base ⇒ ('var ⇒ 'base) ⇒ 'base" and
  base_vars and
  vars :: "'expr ⇒ 'var set" +
assumes
  ground_subst_iff_base_ground_subst [simp]: "⋀γ. is_ground_subst γ ⟷ base.is_ground_subst γ" and
  vars_subst: "⋀expr ρ.  vars (expr ⋅ ρ) = ⋃ (base_vars ` ρ ` vars expr)"
begin

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

lemma obtain_ground_subst:
  obtains γ
  where "is_ground_subst γ"
  unfolding ground_subst_iff_base_ground_subst base.is_ground_subst_def
  using base.base_ground_exists base.vars_subst_vars
  by (meson is_ground_subst_def is_grounding_iff_vars_grounded that)

lemma exists_ground_subst [intro]: "∃γ. is_ground_subst γ"
  by (metis obtain_ground_subst)

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)

lemma ground_subst_extension':
  assumes "is_ground (expr ⋅ γ)"
  obtains γ'
  where "expr ⋅ γ = expr ⋅ γ'" and "base.is_ground_subst γ'"
  using ground_subst_extension assms
  by auto

lemma ground_subst_update [simp]:
  assumes "base.is_ground update" "is_ground (expr ⋅ γ)"
  shows "is_ground (expr ⋅ γ(var := update))"
  using assms is_grounding_iff_vars_grounded
  by auto

lemma ground_exists: "∃expr. is_ground expr"
  using base.base_ground_exists
  by (meson is_grounding_iff_vars_grounded)

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

definition range_vars :: "('var ⇒ 'base) ⇒ 'var 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)

end

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

context base_functional_substitution
begin

sublocale based_functional_substitution
  where base_subst = subst and base_vars = vars
  by unfold_locales (simp_all add: vars_subst_vars)

declare ground_subst_iff_base_ground_subst [simp del]

end

hide_fact base_functional_substitution.base_ground_exists
hide_fact base_functional_substitution.vars_subst_vars

end