Theory Substitution
theory Substitution
imports
Abstract_Substitution
"HOL-Library.FSet"
Option_Extra
begin
section ‹Substitutions on variables›
locale substitution = abstract_substitution where
subst = subst
for
subst :: "'expr ⇒ 'subst ⇒ 'expr" (infixl "⋅" 69) and
apply_subst :: "'v ⇒ 'subst ⇒ 'base" (infixl "⋅v" 69) and
vars :: "'expr ⇒ 'v set" +
assumes no_vars_if_is_ground [intro]: "⋀expr. is_ground expr ⟹ vars expr = {}"
begin
abbreviation exists_nonground where
"exists_nonground ≡ ∃expr. ¬is_ground expr"
definition vars_set :: "'expr set ⇒ 'v set" where
"vars_set exprs ≡ ⋃expr ∈ exprs. vars expr"
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 subst_update =
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_update :: "'subst ⇒ 'v ⇒ 'base ⇒ 'subst" (‹_⟦_ := _⟧› [1000, 0, 50] 71)
assumes
subst_update_var [simp]:
"⋀x update σ. exists_nonground ⟹ x ⋅v σ⟦x := update⟧ = update"
"⋀x y update σ. x ≠ y ⟹ x ⋅v σ⟦y := update⟧ = x ⋅v σ" and
subst_update [simp]:
"⋀x expr update σ. x ∉ vars expr ⟹ expr ⋅ σ⟦x := update⟧ = expr ⋅ σ"
"⋀σ x. σ⟦x := x ⋅v σ⟧ = σ" and
subst_update_twice [simp]:
"⋀σ x a b. (σ⟦x := a⟧)⟦x := b⟧ = σ⟦x := b⟧"
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_exprs:
assumes "exists_nonground"
shows "infinite (UNIV :: 'expr set)"
using assms exists_non_ident_subst
by auto
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_imp:
"⋀ρ. exists_nonground ⟹
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 exists_nonground: "exists_nonground" and ρ: "is_renaming ρ"
shows "x ⋅v ρ ∈ range (var_subst id_subst)"
using is_renaming_imp[OF exists_nonground ρ]
by auto
lemma obtain_renamed_variable:
assumes "exists_nonground" "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 "exists_nonground" and ρ: "is_renaming ρ"
shows "rename ρ x ⋅v id_subst = x ⋅v ρ"
unfolding rename_def[OF ρ]
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) empty_is_image image_cong image_image no_vars_if_is_ground)
lemma surj_inv_renaming:
assumes exists_nonground: "exists_nonground" and ρ: "is_renaming ρ"
shows "surj (λx. inv (var_subst ρ) (x ⋅v id_subst))"
using inv_f_f is_renaming_imp[OF exists_nonground ρ]
unfolding surj_def
by metis
lemma renaming_range:
assumes ρ: "is_renaming ρ" and x: "x ∈ vars (expr ⋅ ρ)"
shows "x ⋅v id_subst ∈ range (var_subst ρ)"
using rename_variables_id_subst[OF ρ] x
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 exists_nonground: "exists_nonground" and ρ: "is_renaming ρ"
shows "inv (var_subst ρ) (x ⋅v ρ) = x"
using is_renaming_imp[OF exists_nonground ρ]
by (simp add: inv_into_f_eq)
lemma renaming_inv_in_vars:
assumes ρ: "is_renaming ρ" and x: "x ∈ vars (expr ⋅ ρ)"
shows "inv (var_subst ρ) (x ⋅v id_subst) ∈ vars expr"
using assms rename_variables_id_subst[OF ρ]
by (metis no_vars_if_is_ground imageI image_inv_f_f insert_not_empty is_renaming_imp
mk_disjoint_insert)
lemma inj_id_subst:
assumes "exists_nonground"
shows "inj (var_subst id_subst)"
using is_renaming_id_subst is_renaming_imp[OF assms]
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" (‹_⟦_⟧› [1000, 0] 71)
assumes subst_updates [simp]:
"⋀x σ update. exists_nonground ⟹ x ⋅v σ⟦update⟧ = get_or (update x) (x ⋅v σ)"
"⋀expr σ b. expr ⋅ σ⟦λx. if x ∈ vars expr then None else b x⟧ = expr ⋅ σ"
begin
lemma redundant_subst_updates [simp]:
assumes "⋀x. x ∈ vars expr ⟹ update x = None"
shows "expr ⋅ σ⟦update⟧ = expr ⋅ σ"
using assms
proof -
have "∃f. (λv. if v ∈ vars expr then None else f v) = update"
using assms
by force
then show ?thesis
by force
qed
lemma redundant_subst_updates_vars_image [simp]:
assumes "⋀x. x ∈ ⋃(vars ` X) ⟹ update x = None"
shows "(λexpr. expr ⋅ σ⟦update⟧) ` X = (λexpr. expr ⋅ σ) ` X"
using assms subst_updates
by (meson UN_I image_cong redundant_subst_updates)
lemma redundant_subst_updates_vars_set [simp]:
assumes "⋀x. x ∈ X ⟹ update x = None" exists_nonground
shows "(λx. x ⋅v σ⟦update⟧) ` X = (λx. x ⋅v σ) ` X"
using assms subst_updates
by auto
end
locale exists_imgu = substitution +
assumes
"⋀υ expr expr'. exists_nonground ⟹ expr ⋅ υ = expr' ⋅ υ ⟹ ∃μ. is_imgu μ {{expr, expr'}}"
begin
lemma exists_imgu:
assumes "expr ⋅ υ = expr' ⋅ υ"
shows "∃μ. is_imgu μ {{expr, expr'}}"
proof (cases exists_nonground)
case True
then show ?thesis
by (metis assms exists_imgu_axioms exists_imgu_axioms_def exists_imgu_def)
next
case False
then have "expr = expr'"
using assms
by simp
then show ?thesis
by (metis insert_absorb2 is_imgu_id_subst_empty is_imgu_insert_singleton)
qed
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 finite_X unifier
proof (cases X)
case emptyI
then show ?thesis
using is_imgu_id_subst
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 is_unifier_subset comp_subst.left.monoid_action_compatibility
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 insert.prems insertCI is_unifier_iff)
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: expr' is_unifier_iff is_unifier_set_insert 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_def is_unifier_subset subst_set_insert empty_iff insertCI
subset_insertI subst_set_comp_subst)
ultimately show "μ'' ⊙ τ = τ"
using μ μ'
unfolding μ''_def is_imgu_def is_unifier_set_insert
by (metis 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_iff X_μ_def subst_set_def
by (smt (verit, ccfv_threshold) comp_subst.left.monoid_action_compatibility image_iff
insertCI)
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)
unfolding μ''_def is_imgu_def X_μ_def is_unifier_iff is_unifier_set_def
by (metis comp_subst.left.monoid_action_compatibility insert_absorb insert_iff
subst_set_insert)
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 abstract_substitution_ops.subst_set_empty comp_subst.left.assoc
is_unifier_set_empty subst_set_comp_subst)
qed
qed
end
locale create_renaming =
subst_updates +
assumes create_renaming: "⋀f. inj f ⟹ is_renaming (id_subst⟦λx. Some (f x ⋅v id_subst)⟧)"
locale subst_updates_compat =
subst_updates +
assumes subst_updates_compat:
"⋀expr X σ b. vars expr ⊆ X ⟹
expr ⋅ id_subst⟦λx. if x ∈ X then Some (x ⋅v σ) else b x⟧ = expr ⋅ σ"
"⋀expr X σ b. vars expr ∩ X = {} ⟹
expr ⋅ id_subst⟦λx. if x ∈ X then b x else Some (x ⋅v σ)⟧ = expr ⋅ σ"
locale subst_eq =
substitution +
assumes subst_eq: "⋀expr σ τ. (⋀x. x ∈ vars expr ⟹ x ⋅v σ = x ⋅v τ) ⟹ expr ⋅ σ = expr ⋅ τ"
begin
lemma subset_subst_eq:
assumes "∀x∈vars C. x ⋅v σ⇩1 = x ⋅v σ⇩2" "vars D ⊆ vars C"
shows "D ⋅ σ⇩1 = D ⋅ σ⇩2"
using assms
by (meson subset_iff subst_eq)
end
locale is_ground_if_no_vars = substitution +
assumes is_ground_if_no_vars: "⋀expr. vars expr = {} ⟹ is_ground expr"
begin
lemma is_ground_iff_no_vars: "is_ground expr ⟷ vars expr = {}"
by (metis is_ground_if_no_vars no_vars_if_is_ground)
end
end