Theory Abstract_Substitution
section ‹Abstract Substitutions›
theory Abstract_Substitution
imports Clausal_Logic Map2
begin
text ‹
Atoms and substitutions are abstracted away behind some locales, to avoid having a direct dependency
on the IsaFoR library.
Conventions: ‹'s› substitutions, ‹'a› atoms.
›
subsection ‹Library›
lemma f_Suc_decr_eventually_const:
fixes f :: "nat ⇒ nat"
assumes leq: "∀i. f (Suc i) ≤ f i"
shows "∃l. ∀l' ≥ l. f l' = f (Suc l')"
proof (rule ccontr)
assume a: "∄l. ∀l' ≥ l. f l' = f (Suc l')"
have "∀i. ∃i'. i' > i ∧ f i' < f i"
proof
fix i
from a have "∃l' ≥ i. f l' ≠ f (Suc l')"
by auto
then obtain l' where
l'_p: "l' ≥ i ∧ f l' ≠ f (Suc l')"
by metis
then have "f l' > f (Suc l')"
using leq le_eq_less_or_eq by auto
moreover have "f i ≥ f l'"
using leq l'_p by (induction l' arbitrary: i) (blast intro: lift_Suc_antimono_le)+
ultimately show "∃i' > i. f i' < f i"
using l'_p less_le_trans by blast
qed
then obtain g_sm :: "nat ⇒ nat" where
g_sm_p: "∀i. g_sm i > i ∧ f (g_sm i) < f i"
by metis
define c :: "nat ⇒ nat" where
"⋀n. c n = (g_sm ^^ n) 0"
have "f (c i) > f (c (Suc i))" for i
by (induction i) (auto simp: c_def g_sm_p)
then have "∀i. (f ∘ c) i > (f ∘ c) (Suc i)"
by auto
then have "∃fc :: nat ⇒ nat. ∀i. fc i > fc (Suc i)"
by metis
then show False
using wf_less_than by (simp add: wf_iff_no_infinite_down_chain)
qed
subsection ‹Substitution Operators›
locale substitution_ops =
fixes
subst_atm :: "'a ⇒ 's ⇒ 'a" and
id_subst :: 's and
comp_subst :: "'s ⇒ 's ⇒ 's"
begin
abbreviation subst_atm_abbrev :: "'a ⇒ 's ⇒ 'a" (infixl "⋅a" 67) where
"subst_atm_abbrev ≡ subst_atm"
abbreviation comp_subst_abbrev :: "'s ⇒ 's ⇒ 's" (infixl "⊙" 67) where
"comp_subst_abbrev ≡ comp_subst"
definition comp_substs :: "'s list ⇒ 's list ⇒ 's list" (infixl "⊙s" 67) where
"σs ⊙s τs = map2 comp_subst σs τs"
definition subst_atms :: "'a set ⇒ 's ⇒ 'a set" (infixl "⋅as" 67) where
"AA ⋅as σ = (λA. A ⋅a σ) ` AA"
definition subst_atmss :: "'a set set ⇒ 's ⇒ 'a set set" (infixl "⋅ass" 67) where
"AAA ⋅ass σ = (λAA. AA ⋅as σ) ` AAA"
definition subst_atm_list :: "'a list ⇒ 's ⇒ 'a list" (infixl "⋅al" 67) where
"As ⋅al σ = map (λA. A ⋅a σ) As"
definition subst_atm_mset :: "'a multiset ⇒ 's ⇒ 'a multiset" (infixl "⋅am" 67) where
"AA ⋅am σ = image_mset (λA. A ⋅a σ) AA"
definition
subst_atm_mset_list :: "'a multiset list ⇒ 's ⇒ 'a multiset list" (infixl "⋅aml" 67)
where
"AAA ⋅aml σ = map (λAA. AA ⋅am σ) AAA"
definition
subst_atm_mset_lists :: "'a multiset list ⇒ 's list ⇒ 'a multiset list" (infixl "⋅⋅aml" 67)
where
"AAs ⋅⋅aml σs = map2 (⋅am) AAs σs"
definition subst_lit :: "'a literal ⇒ 's ⇒ 'a literal" (infixl "⋅l" 67) where
"L ⋅l σ = map_literal (λA. A ⋅a σ) L"
lemma atm_of_subst_lit[simp]: "atm_of (L ⋅l σ) = atm_of L ⋅a σ"
unfolding subst_lit_def by (cases L) simp+
definition subst_cls :: "'a clause ⇒ 's ⇒ 'a clause" (infixl "⋅" 67) where
"AA ⋅ σ = image_mset (λA. A ⋅l σ) AA"
definition subst_clss :: "'a clause set ⇒ 's ⇒ 'a clause set" (infixl "⋅cs" 67) where
"AA ⋅cs σ = (λA. A ⋅ σ) ` AA"
definition subst_cls_list :: "'a clause list ⇒ 's ⇒ 'a clause list" (infixl "⋅cl" 67) where
"Cs ⋅cl σ = map (λA. A ⋅ σ) Cs"
definition subst_cls_lists :: "'a clause list ⇒ 's list ⇒ 'a clause list" (infixl "⋅⋅cl" 67) where
"Cs ⋅⋅cl σs = map2 (⋅) Cs σs"
definition subst_cls_mset :: "'a clause multiset ⇒ 's ⇒ 'a clause multiset" (infixl "⋅cm" 67) where
"CC ⋅cm σ = image_mset (λA. A ⋅ σ) CC"
lemma subst_cls_add_mset[simp]: "add_mset L C ⋅ σ = add_mset (L ⋅l σ) (C ⋅ σ)"
unfolding subst_cls_def by simp
lemma subst_cls_mset_add_mset[simp]: "add_mset C CC ⋅cm σ = add_mset (C ⋅ σ) (CC ⋅cm σ)"
unfolding subst_cls_mset_def by simp
definition generalizes_atm :: "'a ⇒ 'a ⇒ bool" where
"generalizes_atm A B ⟷ (∃σ. A ⋅a σ = B)"
definition strictly_generalizes_atm :: "'a ⇒ 'a ⇒ bool" where
"strictly_generalizes_atm A B ⟷ generalizes_atm A B ∧ ¬ generalizes_atm B A"
definition generalizes_lit :: "'a literal ⇒ 'a literal ⇒ bool" where
"generalizes_lit L M ⟷ (∃σ. L ⋅l σ = M)"
definition strictly_generalizes_lit :: "'a literal ⇒ 'a literal ⇒ bool" where
"strictly_generalizes_lit L M ⟷ generalizes_lit L M ∧ ¬ generalizes_lit M L"
definition generalizes :: "'a clause ⇒ 'a clause ⇒ bool" where
"generalizes C D ⟷ (∃σ. C ⋅ σ = D)"
definition strictly_generalizes :: "'a clause ⇒ 'a clause ⇒ bool" where
"strictly_generalizes C D ⟷ generalizes C D ∧ ¬ generalizes D C"
definition subsumes :: "'a clause ⇒ 'a clause ⇒ bool" where
"subsumes C D ⟷ (∃σ. C ⋅ σ ⊆# D)"
definition strictly_subsumes :: "'a clause ⇒ 'a clause ⇒ bool" where
"strictly_subsumes C D ⟷ subsumes C D ∧ ¬ subsumes D C"
definition variants :: "'a clause ⇒ 'a clause ⇒ bool" where
"variants C D ⟷ generalizes C D ∧ generalizes D C"
definition is_renaming :: "'s ⇒ bool" where
"is_renaming σ ⟷ (∃τ. σ ⊙ τ = id_subst)"
definition is_renaming_list :: "'s list ⇒ bool" where
"is_renaming_list σs ⟷ (∀σ ∈ set σs. is_renaming σ)"
definition inv_renaming :: "'s ⇒ 's" where
"inv_renaming σ = (SOME τ. σ ⊙ τ = id_subst)"
definition is_ground_atm :: "'a ⇒ bool" where
"is_ground_atm A ⟷ (∀σ. A = A ⋅a σ)"
definition is_ground_atms :: "'a set ⇒ bool" where
"is_ground_atms AA = (∀A ∈ AA. is_ground_atm A)"
definition is_ground_atm_list :: "'a list ⇒ bool" where
"is_ground_atm_list As ⟷ (∀A ∈ set As. is_ground_atm A)"
definition is_ground_atm_mset :: "'a multiset ⇒ bool" where
"is_ground_atm_mset AA ⟷ (∀A. A ∈# AA ⟶ is_ground_atm A)"
definition is_ground_lit :: "'a literal ⇒ bool" where
"is_ground_lit L ⟷ is_ground_atm (atm_of L)"
definition is_ground_cls :: "'a clause ⇒ bool" where
"is_ground_cls C ⟷ (∀L. L ∈# C ⟶ is_ground_lit L)"
definition is_ground_clss :: "'a clause set ⇒ bool" where
"is_ground_clss CC ⟷ (∀C ∈ CC. is_ground_cls C)"
definition is_ground_cls_list :: "'a clause list ⇒ bool" where
"is_ground_cls_list CC ⟷ (∀C ∈ set CC. is_ground_cls C)"
definition is_ground_subst :: "'s ⇒ bool" where
"is_ground_subst σ ⟷ (∀A. is_ground_atm (A ⋅a σ))"
definition is_ground_subst_list :: "'s list ⇒ bool" where
"is_ground_subst_list σs ⟷ (∀σ ∈ set σs. is_ground_subst σ)"
definition grounding_of_cls :: "'a clause ⇒ 'a clause set" where
"grounding_of_cls C = {C ⋅ σ |σ. is_ground_subst σ}"
definition grounding_of_clss :: "'a clause set ⇒ 'a clause set" where
"grounding_of_clss CC = (⋃C ∈ CC. grounding_of_cls C)"
definition is_unifier :: "'s ⇒ 'a set ⇒ bool" where
"is_unifier σ AA ⟷ card (AA ⋅as σ) ≤ 1"
definition is_unifiers :: "'s ⇒ 'a set set ⇒ bool" where
"is_unifiers σ AAA ⟷ (∀AA ∈ AAA. is_unifier σ AA)"
definition is_mgu :: "'s ⇒ 'a set set ⇒ bool" where
"is_mgu σ AAA ⟷ is_unifiers σ AAA ∧ (∀τ. is_unifiers τ AAA ⟶ (∃γ. τ = σ ⊙ γ))"
definition is_imgu :: "'s ⇒ 'a set set ⇒ bool" where
"is_imgu σ AAA ⟷ is_unifiers σ AAA ∧ (∀τ. is_unifiers τ AAA ⟶ τ = σ ⊙ τ)"
definition var_disjoint :: "'a clause list ⇒ bool" where
"var_disjoint Cs ⟷
(∀σs. length σs = length Cs ⟶ (∃τ. ∀i < length Cs. ∀S. S ⊆# Cs ! i ⟶ S ⋅ σs ! i = S ⋅ τ))"
end
subsection ‹Substitution Lemmas›
locale substitution = substitution_ops subst_atm id_subst comp_subst
for
subst_atm :: "'a ⇒ 's ⇒ 'a" and
id_subst :: 's and
comp_subst :: "'s ⇒ 's ⇒ 's" +
assumes
subst_atm_id_subst[simp]: "A ⋅a id_subst = A" and
subst_atm_comp_subst[simp]: "A ⋅a (σ ⊙ τ) = (A ⋅a σ) ⋅a τ" and
subst_ext: "(⋀A. A ⋅a σ = A ⋅a τ) ⟹ σ = τ" and
make_ground_subst: "is_ground_cls (C ⋅ σ) ⟹ ∃τ. is_ground_subst τ ∧C ⋅ τ = C ⋅ σ" and
wf_strictly_generalizes_atm: "wfP strictly_generalizes_atm"
begin
lemma subst_ext_iff: "σ = τ ⟷ (∀A. A ⋅a σ = A ⋅a τ)"
by (blast intro: subst_ext)
subsubsection ‹Identity Substitution›
lemma id_subst_comp_subst[simp]: "id_subst ⊙ σ = σ"
by (rule subst_ext) simp
lemma comp_subst_id_subst[simp]: "σ ⊙ id_subst = σ"
by (rule subst_ext) simp
lemma id_subst_comp_substs[simp]: "replicate (length σs) id_subst ⊙s σs = σs"
using comp_substs_def by (induction σs) auto
lemma comp_substs_id_subst[simp]: "σs ⊙s replicate (length σs) id_subst = σs"
using comp_substs_def by (induction σs) auto
lemma subst_atms_id_subst[simp]: "AA ⋅as id_subst = AA"
unfolding subst_atms_def by simp
lemma subst_atmss_id_subst[simp]: "AAA ⋅ass id_subst = AAA"
unfolding subst_atmss_def by simp
lemma subst_atm_list_id_subst[simp]: "As ⋅al id_subst = As"
unfolding subst_atm_list_def by auto
lemma subst_atm_mset_id_subst[simp]: "AA ⋅am id_subst = AA"
unfolding subst_atm_mset_def by simp
lemma subst_atm_mset_list_id_subst[simp]: "AAs ⋅aml id_subst = AAs"
unfolding subst_atm_mset_list_def by simp
lemma subst_atm_mset_lists_id_subst[simp]: "AAs ⋅⋅aml replicate (length AAs) id_subst = AAs"
unfolding subst_atm_mset_lists_def by (induct AAs) auto
lemma subst_lit_id_subst[simp]: "L ⋅l id_subst = L"
unfolding subst_lit_def by (simp add: literal.map_ident)
lemma subst_cls_id_subst[simp]: "C ⋅ id_subst = C"
unfolding subst_cls_def by simp
lemma subst_clss_id_subst[simp]: "CC ⋅cs id_subst = CC"
unfolding subst_clss_def by simp
lemma subst_cls_list_id_subst[simp]: "Cs ⋅cl id_subst = Cs"
unfolding subst_cls_list_def by simp
lemma subst_cls_lists_id_subst[simp]: "Cs ⋅⋅cl replicate (length Cs) id_subst = Cs"
unfolding subst_cls_lists_def by (induct Cs) auto
lemma subst_cls_mset_id_subst[simp]: "CC ⋅cm id_subst = CC"
unfolding subst_cls_mset_def by simp
subsubsection ‹Associativity of Composition›
lemma comp_subst_assoc[simp]: "σ ⊙ (τ ⊙ γ) = σ ⊙ τ ⊙ γ"
by (rule subst_ext) simp
subsubsection ‹Compatibility of Substitution and Composition›
lemma subst_atms_comp_subst[simp]: "AA ⋅as (τ ⊙ σ) = AA ⋅as τ ⋅as σ"
unfolding subst_atms_def by auto
lemma subst_atmss_comp_subst[simp]: "AAA ⋅ass (τ ⊙ σ) = AAA ⋅ass τ ⋅ass σ"
unfolding subst_atmss_def by auto
lemma subst_atm_list_comp_subst[simp]: "As ⋅al (τ ⊙ σ) = As ⋅al τ ⋅al σ"
unfolding subst_atm_list_def by auto
lemma subst_atm_mset_comp_subst[simp]: "AA ⋅am (τ ⊙ σ) = AA ⋅am τ ⋅am σ"
unfolding subst_atm_mset_def by auto
lemma subst_atm_mset_list_comp_subst[simp]: "AAs ⋅aml (τ ⊙ σ) = (AAs ⋅aml τ) ⋅aml σ"
unfolding subst_atm_mset_list_def by auto
lemma subst_atm_mset_lists_comp_substs[simp]: "AAs ⋅⋅aml (τs ⊙s σs) = AAs ⋅⋅aml τs ⋅⋅aml σs"
unfolding subst_atm_mset_lists_def comp_substs_def map_zip_map map_zip_map2 map_zip_assoc
by (simp add: split_def)
lemma subst_lit_comp_subst[simp]: "L ⋅l (τ ⊙ σ) = L ⋅l τ ⋅l σ"
unfolding subst_lit_def by (auto simp: literal.map_comp o_def)
lemma subst_cls_comp_subst[simp]: "C ⋅ (τ ⊙ σ) = C ⋅ τ ⋅ σ"
unfolding subst_cls_def by auto
lemma subst_clsscomp_subst[simp]: "CC ⋅cs (τ ⊙ σ) = CC ⋅cs τ ⋅cs σ"
unfolding subst_clss_def by auto
lemma subst_cls_list_comp_subst[simp]: "Cs ⋅cl (τ ⊙ σ) = Cs ⋅cl τ ⋅cl σ"
unfolding subst_cls_list_def by auto
lemma subst_cls_lists_comp_substs[simp]: "Cs ⋅⋅cl (τs ⊙s σs) = Cs ⋅⋅cl τs ⋅⋅cl σs"
unfolding subst_cls_lists_def comp_substs_def map_zip_map map_zip_map2 map_zip_assoc
by (simp add: split_def)
lemma subst_cls_mset_comp_subst[simp]: "CC ⋅cm (τ ⊙ σ) = CC ⋅cm τ ⋅cm σ"
unfolding subst_cls_mset_def by auto
subsubsection ‹``Commutativity'' of Membership and Substitution›
lemma Melem_subst_atm_mset[simp]: "A ∈# AA ⋅am σ ⟷ (∃B. B ∈# AA ∧ A = B ⋅a σ)"
unfolding subst_atm_mset_def by auto
lemma Melem_subst_cls[simp]: "L ∈# C ⋅ σ ⟷ (∃M. M ∈# C ∧ L = M ⋅l σ)"
unfolding subst_cls_def by auto
lemma Melem_subst_cls_mset[simp]: "AA ∈# CC ⋅cm σ ⟷ (∃BB. BB ∈# CC ∧ AA = BB ⋅ σ)"
unfolding subst_cls_mset_def by auto
subsubsection ‹Signs and Substitutions›
lemma subst_lit_is_neg[simp]: "is_neg (L ⋅l σ) = is_neg L"
unfolding subst_lit_def by auto
lemma subst_lit_is_pos[simp]: "is_pos (L ⋅l σ) = is_pos L"
unfolding subst_lit_def by auto
lemma subst_minus[simp]: "(- L) ⋅l μ = - (L ⋅l μ)"
by (simp add: literal.map_sel subst_lit_def uminus_literal_def)
subsubsection ‹Substitution on Literal(s)›
lemma eql_neg_lit_eql_atm[simp]: "(Neg A' ⋅l η) = Neg A ⟷ A' ⋅a η = A"
by (simp add: subst_lit_def)
lemma eql_pos_lit_eql_atm[simp]: "(Pos A' ⋅l η) = Pos A ⟷ A' ⋅a η = A"
by (simp add: subst_lit_def)
lemma subst_cls_negs[simp]: "(negs AA) ⋅ σ = negs (AA ⋅am σ)"
unfolding subst_cls_def subst_lit_def subst_atm_mset_def by auto
lemma subst_cls_poss[simp]: "(poss AA) ⋅ σ = poss (AA ⋅am σ)"
unfolding subst_cls_def subst_lit_def subst_atm_mset_def by auto
lemma atms_of_subst_atms: "atms_of C ⋅as σ = atms_of (C ⋅ σ)"
proof -
have "atms_of (C ⋅ σ) = set_mset (image_mset atm_of (image_mset (map_literal (λA. A ⋅a σ)) C))"
unfolding subst_cls_def subst_atms_def subst_lit_def atms_of_def by auto
also have "... = set_mset (image_mset (λA. A ⋅a σ) (image_mset atm_of C))"
by simp (meson literal.map_sel)
finally show "atms_of C ⋅as σ = atms_of (C ⋅ σ)"
unfolding subst_atms_def atms_of_def by auto
qed
lemma in_image_Neg_is_neg[simp]: "L ⋅l σ ∈ Neg ` AA ⟹ is_neg L"
by (metis bex_imageD literal.disc(2) literal.map_disc_iff subst_lit_def)
lemma subst_lit_in_negs_subst_is_neg: "L ⋅l σ ∈# (negs AA) ⋅ τ ⟹ is_neg L"
by simp
lemma subst_lit_in_negs_is_neg: "L ⋅l σ ∈# negs AA ⟹ is_neg L"
by simp
subsubsection ‹Substitution on Empty›
lemma subst_atms_empty[simp]: "{} ⋅as σ = {}"
unfolding subst_atms_def by auto
lemma subst_atmss_empty[simp]: "{} ⋅ass σ = {}"
unfolding subst_atmss_def by auto
lemma comp_substs_empty_iff[simp]: "σs ⊙s ηs = [] ⟷ σs = [] ∨ ηs = []"
using comp_substs_def map2_empty_iff by auto
lemma subst_atm_list_empty[simp]: "[] ⋅al σ = []"
unfolding subst_atm_list_def by auto
lemma subst_atm_mset_empty[simp]: "{#} ⋅am σ = {#}"
unfolding subst_atm_mset_def by auto
lemma subst_atm_mset_list_empty[simp]: "[] ⋅aml σ = []"
unfolding subst_atm_mset_list_def by auto
lemma subst_atm_mset_lists_empty[simp]: "[] ⋅⋅aml σs = []"
unfolding subst_atm_mset_lists_def by auto
lemma subst_cls_empty[simp]: "{#} ⋅ σ = {#}"
unfolding subst_cls_def by auto
lemma subst_clss_empty[simp]: "{} ⋅cs σ = {}"
unfolding subst_clss_def by auto
lemma subst_cls_list_empty[simp]: "[] ⋅cl σ = []"
unfolding subst_cls_list_def by auto
lemma subst_cls_lists_empty[simp]: "[] ⋅⋅cl σs = []"
unfolding subst_cls_lists_def by auto
lemma subst_scls_mset_empty[simp]: "{#} ⋅cm σ = {#}"
unfolding subst_cls_mset_def by auto
lemma subst_atms_empty_iff[simp]: "AA ⋅as η = {} ⟷ AA = {}"
unfolding subst_atms_def by auto
lemma subst_atmss_empty_iff[simp]: "AAA ⋅ass η = {} ⟷ AAA = {}"
unfolding subst_atmss_def by auto
lemma subst_atm_list_empty_iff[simp]: "As ⋅al η = [] ⟷ As = []"
unfolding subst_atm_list_def by auto
lemma subst_atm_mset_empty_iff[simp]: "AA ⋅am η = {#} ⟷ AA = {#}"
unfolding subst_atm_mset_def by auto
lemma subst_atm_mset_list_empty_iff[simp]: "AAs ⋅aml η = [] ⟷ AAs = []"
unfolding subst_atm_mset_list_def by auto
lemma subst_atm_mset_lists_empty_iff[simp]: "AAs ⋅⋅aml ηs = [] ⟷ (AAs = [] ∨ ηs = [])"
using map2_empty_iff subst_atm_mset_lists_def by auto
lemma subst_cls_empty_iff[simp]: "C ⋅ η = {#} ⟷ C = {#}"
unfolding subst_cls_def by auto
lemma subst_clss_empty_iff[simp]: "CC ⋅cs η = {} ⟷ CC = {}"
unfolding subst_clss_def by auto
lemma subst_cls_list_empty_iff[simp]: "Cs ⋅cl η = [] ⟷ Cs = []"
unfolding subst_cls_list_def by auto
lemma subst_cls_lists_empty_iff[simp]: "Cs ⋅⋅cl ηs = [] ⟷ Cs = [] ∨ ηs = []"
using map2_empty_iff subst_cls_lists_def by auto
lemma subst_cls_mset_empty_iff[simp]: "CC ⋅cm η = {#} ⟷ CC = {#}"
unfolding subst_cls_mset_def by auto
subsubsection ‹Substitution on a Union›
lemma subst_atms_union[simp]: "(AA ∪ BB) ⋅as σ = AA ⋅as σ ∪ BB ⋅as σ"
unfolding subst_atms_def by auto
lemma subst_atmss_union[simp]: "(AAA ∪ BBB) ⋅ass σ = AAA ⋅ass σ ∪ BBB ⋅ass σ"
unfolding subst_atmss_def by auto
lemma subst_atm_list_append[simp]: "(As @ Bs) ⋅al σ = As ⋅al σ @ Bs ⋅al σ"
unfolding subst_atm_list_def by auto
lemma subst_atm_mset_union[simp]: "(AA + BB) ⋅am σ = AA ⋅am σ + BB ⋅am σ"
unfolding subst_atm_mset_def by auto
lemma subst_atm_mset_list_append[simp]: "(AAs @ BBs) ⋅aml σ = AAs ⋅aml σ @ BBs ⋅aml σ"
unfolding subst_atm_mset_list_def by auto
lemma subst_cls_union[simp]: "(C + D) ⋅ σ = C ⋅ σ + D ⋅ σ"
unfolding subst_cls_def by auto
lemma subst_clss_union[simp]: "(CC ∪ DD) ⋅cs σ = CC ⋅cs σ ∪ DD ⋅cs σ"
unfolding subst_clss_def by auto
lemma subst_cls_list_append[simp]: "(Cs @ Ds) ⋅cl σ = Cs ⋅cl σ @ Ds ⋅cl σ"
unfolding subst_cls_list_def by auto
lemma subst_cls_lists_append[simp]:
"length Cs = length σs ⟹ length Cs' = length σs' ⟹
(Cs @ Cs') ⋅⋅cl (σs @ σs') = Cs ⋅⋅cl σs @ Cs' ⋅⋅cl σs'"
unfolding subst_cls_lists_def by auto
lemma subst_cls_mset_union[simp]: "(CC + DD) ⋅cm σ = CC ⋅cm σ + DD ⋅cm σ"
unfolding subst_cls_mset_def by auto
subsubsection ‹Substitution on a Singleton›
lemma subst_atms_single[simp]: "{A} ⋅as σ = {A ⋅a σ}"
unfolding subst_atms_def by auto
lemma subst_atmss_single[simp]: "{AA} ⋅ass σ = {AA ⋅as σ}"
unfolding subst_atmss_def by auto
lemma subst_atm_list_single[simp]: "[A] ⋅al σ = [A ⋅a σ]"
unfolding subst_atm_list_def by auto
lemma subst_atm_mset_single[simp]: "{#A#} ⋅am σ = {#A ⋅a σ#}"
unfolding subst_atm_mset_def by auto
lemma subst_atm_mset_list[simp]: "[AA] ⋅aml σ = [AA ⋅am σ]"
unfolding subst_atm_mset_list_def by auto
lemma subst_cls_single[simp]: "{#L#} ⋅ σ = {#L ⋅l σ#}"
by simp
lemma subst_clss_single[simp]: "{C} ⋅cs σ = {C ⋅ σ}"
unfolding subst_clss_def by auto
lemma subst_cls_list_single[simp]: "[C] ⋅cl σ = [C ⋅ σ]"
unfolding subst_cls_list_def by auto
lemma subst_cls_lists_single[simp]: "[C] ⋅⋅cl [σ] = [C ⋅ σ]"
unfolding subst_cls_lists_def by auto
lemma subst_cls_mset_single[simp]: "{#C#} ⋅cm σ = {#C ⋅ σ#}"
by simp
subsubsection ‹Substitution on @{term Cons}›
lemma subst_atm_list_Cons[simp]: "(A # As) ⋅al σ = A ⋅a σ # As ⋅al σ"
unfolding subst_atm_list_def by auto
lemma subst_atm_mset_list_Cons[simp]: "(A # As) ⋅aml σ = A ⋅am σ # As ⋅aml σ"
unfolding subst_atm_mset_list_def by auto
lemma subst_atm_mset_lists_Cons[simp]: "(C # Cs) ⋅⋅aml (σ # σs) = C ⋅am σ # Cs ⋅⋅aml σs"
unfolding subst_atm_mset_lists_def by auto
lemma subst_cls_list_Cons[simp]: "(C # Cs) ⋅cl σ = C ⋅ σ # Cs ⋅cl σ"
unfolding subst_cls_list_def by auto
lemma subst_cls_lists_Cons[simp]: "(C # Cs) ⋅⋅cl (σ # σs) = C ⋅ σ # Cs ⋅⋅cl σs"
unfolding subst_cls_lists_def by auto
subsubsection ‹Substitution on @{term tl}›
lemma subst_atm_list_tl[simp]: "tl (As ⋅al σ) = tl As ⋅al σ"
by (cases As) auto
lemma subst_atm_mset_list_tl[simp]: "tl (AAs ⋅aml σ) = tl AAs ⋅aml σ"
by (cases AAs) auto
lemma subst_cls_list_tl[simp]: "tl (Cs ⋅cl σ) = tl Cs ⋅cl σ"
by (cases Cs) auto
lemma subst_cls_lists_tl[simp]: "length Cs = length σs ⟹ tl (Cs ⋅⋅cl σs) = tl Cs ⋅⋅cl tl σs"
by (cases Cs; cases σs) auto
subsubsection ‹Substitution on @{term nth}›
lemma comp_substs_nth[simp]:
"length τs = length σs ⟹ i < length τs ⟹ (τs ⊙s σs) ! i = (τs ! i) ⊙ (σs ! i)"
by (simp add: comp_substs_def)
lemma subst_atm_list_nth[simp]: "i < length As ⟹ (As ⋅al τ) ! i = As ! i ⋅a τ"
unfolding subst_atm_list_def using less_Suc_eq_0_disj nth_map by force
lemma subst_atm_mset_list_nth[simp]: "i < length AAs ⟹ (AAs ⋅aml η) ! i = (AAs ! i) ⋅am η"
unfolding subst_atm_mset_list_def by auto
lemma subst_atm_mset_lists_nth[simp]:
"length AAs = length σs ⟹ i < length AAs ⟹ (AAs ⋅⋅aml σs) ! i = (AAs ! i) ⋅am (σs ! i)"
unfolding subst_atm_mset_lists_def by auto
lemma subst_cls_list_nth[simp]: "i < length Cs ⟹ (Cs ⋅cl τ) ! i = (Cs ! i) ⋅ τ"
unfolding subst_cls_list_def using less_Suc_eq_0_disj nth_map by (induction Cs) auto
lemma subst_cls_lists_nth[simp]:
"length Cs = length σs ⟹ i < length Cs ⟹ (Cs ⋅⋅cl σs) ! i = (Cs ! i) ⋅ (σs ! i)"
unfolding subst_cls_lists_def by auto
subsubsection ‹Substitution on Various Other Functions›
lemma subst_clss_image[simp]: "image f X ⋅cs σ = {f x ⋅ σ | x. x ∈ X}"
unfolding subst_clss_def by auto
lemma subst_cls_mset_image_mset[simp]: "image_mset f X ⋅cm σ = {# f x ⋅ σ. x ∈# X #}"
unfolding subst_cls_mset_def by auto
lemma mset_subst_atm_list_subst_atm_mset[simp]: "mset (As ⋅al σ) = mset (As) ⋅am σ"
unfolding subst_atm_list_def subst_atm_mset_def by auto
lemma mset_subst_cls_list_subst_cls_mset: "mset (Cs ⋅cl σ) = (mset Cs) ⋅cm σ"
unfolding subst_cls_mset_def subst_cls_list_def by auto
lemma sum_list_subst_cls_list_subst_cls[simp]: "sum_list (Cs ⋅cl η) = sum_list Cs ⋅ η"
unfolding subst_cls_list_def by (induction Cs) auto
lemma set_mset_subst_cls_mset_subst_clss: "set_mset (CC ⋅cm μ) = (set_mset CC) ⋅cs μ"
by (simp add: subst_cls_mset_def subst_clss_def)
lemma Neg_Melem_subst_atm_subst_cls[simp]: "Neg A ∈# C ⟹ Neg (A ⋅a σ) ∈# C ⋅ σ "
by (metis Melem_subst_cls eql_neg_lit_eql_atm)
lemma Pos_Melem_subst_atm_subst_cls[simp]: "Pos A ∈# C ⟹ Pos (A ⋅a σ) ∈# C ⋅ σ "
by (metis Melem_subst_cls eql_pos_lit_eql_atm)
lemma in_atms_of_subst[simp]: "B ∈ atms_of C ⟹ B ⋅a σ ∈ atms_of (C ⋅ σ)"
by (metis atms_of_subst_atms image_iff subst_atms_def)
subsubsection ‹Renamings›
lemma is_renaming_id_subst[simp]: "is_renaming id_subst"
unfolding is_renaming_def by simp
lemma is_renamingD: "is_renaming σ ⟹ (∀A1 A2. A1 ⋅a σ = A2 ⋅a σ ⟷ A1 = A2)"
by (metis is_renaming_def subst_atm_comp_subst subst_atm_id_subst)
lemma inv_renaming_cancel_r[simp]: "is_renaming r ⟹ r ⊙ inv_renaming r = id_subst"
unfolding inv_renaming_def is_renaming_def by (metis (mono_tags) someI_ex)
lemma inv_renaming_cancel_r_list[simp]:
"is_renaming_list rs ⟹ rs ⊙s map inv_renaming rs = replicate (length rs) id_subst"
unfolding is_renaming_list_def by (induction rs) (auto simp add: comp_substs_def)
lemma Nil_comp_substs[simp]: "[] ⊙s s = []"
unfolding comp_substs_def by auto
lemma comp_substs_Nil[simp]: "s ⊙s [] = []"
unfolding comp_substs_def by auto
lemma is_renaming_idempotent_id_subst: "is_renaming r ⟹ r ⊙ r = r ⟹ r = id_subst"
by (metis comp_subst_assoc comp_subst_id_subst inv_renaming_cancel_r)
lemma is_renaming_left_id_subst_right_id_subst:
"is_renaming r ⟹ s ⊙ r = id_subst ⟹ r ⊙ s = id_subst"
by (metis comp_subst_assoc comp_subst_id_subst is_renaming_def)
lemma is_renaming_closure: "is_renaming r1 ⟹ is_renaming r2 ⟹ is_renaming (r1 ⊙ r2)"
unfolding is_renaming_def by (metis comp_subst_assoc comp_subst_id_subst)
lemma is_renaming_inv_renaming_cancel_atm[simp]: "is_renaming ρ ⟹ A ⋅a ρ ⋅a inv_renaming ρ = A"
by (metis inv_renaming_cancel_r subst_atm_comp_subst subst_atm_id_subst)
lemma is_renaming_inv_renaming_cancel_atms[simp]: "is_renaming ρ ⟹ AA ⋅as ρ ⋅as inv_renaming ρ = AA"
by (metis inv_renaming_cancel_r subst_atms_comp_subst subst_atms_id_subst)
lemma is_renaming_inv_renaming_cancel_atmss[simp]: "is_renaming ρ ⟹ AAA ⋅ass ρ ⋅ass inv_renaming ρ = AAA"
by (metis inv_renaming_cancel_r subst_atmss_comp_subst subst_atmss_id_subst)
lemma is_renaming_inv_renaming_cancel_atm_list[simp]: "is_renaming ρ ⟹ As ⋅al ρ ⋅al inv_renaming ρ = As"
by (metis inv_renaming_cancel_r subst_atm_list_comp_subst subst_atm_list_id_subst)
lemma is_renaming_inv_renaming_cancel_atm_mset[simp]: "is_renaming ρ ⟹ AA ⋅am ρ ⋅am inv_renaming ρ = AA"
by (metis inv_renaming_cancel_r subst_atm_mset_comp_subst subst_atm_mset_id_subst)
lemma is_renaming_inv_renaming_cancel_atm_mset_list[simp]: "is_renaming ρ ⟹ (AAs ⋅aml ρ) ⋅aml inv_renaming ρ = AAs"
by (metis inv_renaming_cancel_r subst_atm_mset_list_comp_subst subst_atm_mset_list_id_subst)
lemma is_renaming_list_inv_renaming_cancel_atm_mset_lists[simp]:
"length AAs = length ρs ⟹ is_renaming_list ρs ⟹ AAs ⋅⋅aml ρs ⋅⋅aml map inv_renaming ρs = AAs"
by (metis inv_renaming_cancel_r_list subst_atm_mset_lists_comp_substs
subst_atm_mset_lists_id_subst)
lemma is_renaming_inv_renaming_cancel_lit[simp]: "is_renaming ρ ⟹ (L ⋅l ρ) ⋅l inv_renaming ρ = L"
by (metis inv_renaming_cancel_r subst_lit_comp_subst subst_lit_id_subst)
lemma is_renaming_inv_renaming_cancel_cls[simp]: "is_renaming ρ ⟹ C ⋅ ρ ⋅ inv_renaming ρ = C"
by (metis inv_renaming_cancel_r subst_cls_comp_subst subst_cls_id_subst)
lemma is_renaming_inv_renaming_cancel_clss[simp]:
"is_renaming ρ ⟹ CC ⋅cs ρ ⋅cs inv_renaming ρ = CC"
by (metis inv_renaming_cancel_r subst_clss_id_subst subst_clsscomp_subst)
lemma is_renaming_inv_renaming_cancel_cls_list[simp]:
"is_renaming ρ ⟹ Cs ⋅cl ρ ⋅cl inv_renaming ρ = Cs"
by (metis inv_renaming_cancel_r subst_cls_list_comp_subst subst_cls_list_id_subst)
lemma is_renaming_list_inv_renaming_cancel_cls_list[simp]:
"length Cs = length ρs ⟹ is_renaming_list ρs ⟹ Cs ⋅⋅cl ρs ⋅⋅cl map inv_renaming ρs = Cs"
by (metis inv_renaming_cancel_r_list subst_cls_lists_comp_substs subst_cls_lists_id_subst)
lemma is_renaming_inv_renaming_cancel_cls_mset[simp]:
"is_renaming ρ ⟹ CC ⋅cm ρ ⋅cm inv_renaming ρ = CC"
by (metis inv_renaming_cancel_r subst_cls_mset_comp_subst subst_cls_mset_id_subst)
subsubsection ‹Monotonicity›
lemma subst_cls_mono: "set_mset C ⊆ set_mset D ⟹ set_mset (C ⋅ σ) ⊆ set_mset (D ⋅ σ)"
by force
lemma subst_cls_mono_mset: "C ⊆# D ⟹ C ⋅ σ ⊆# D ⋅ σ"
unfolding subst_clss_def by (metis mset_subset_eq_exists_conv subst_cls_union)
lemma subst_subset_mono: "D ⊂# C ⟹ D ⋅ σ ⊂# C ⋅ σ"
unfolding subst_cls_def by (simp add: image_mset_subset_mono)
subsubsection ‹Size after Substitution›
lemma size_subst[simp]: "size (D ⋅ σ) = size D"
unfolding subst_cls_def by auto
lemma subst_atm_list_length[simp]: "length (As ⋅al σ) = length As"
unfolding subst_atm_list_def by auto
lemma length_subst_atm_mset_list[simp]: "length (AAs ⋅aml η) = length AAs"
unfolding subst_atm_mset_list_def by auto
lemma subst_atm_mset_lists_length[simp]: "length (AAs ⋅⋅aml σs) = min (length AAs) (length σs)"
unfolding subst_atm_mset_lists_def by auto
lemma subst_cls_list_length[simp]: "length (Cs ⋅cl σ) = length Cs"
unfolding subst_cls_list_def by auto
lemma comp_substs_length[simp]: "length (τs ⊙s σs) = min (length τs) (length σs)"
unfolding comp_substs_def by auto
lemma subst_cls_lists_length[simp]: "length (Cs ⋅⋅cl σs) = min (length Cs) (length σs)"
unfolding subst_cls_lists_def by auto
subsubsection ‹Variable Disjointness›
lemma var_disjoint_clauses:
assumes "var_disjoint Cs"
shows "∀σs. length σs = length Cs ⟶ (∃τ. Cs ⋅⋅cl σs = Cs ⋅cl τ)"
proof clarify
fix σs :: "'s list"
assume a: "length σs = length Cs"
then obtain τ where "∀i < length Cs. ∀S. S ⊆# Cs ! i ⟶ S ⋅ σs ! i = S ⋅ τ"
using assms unfolding var_disjoint_def by blast
then have "∀i < length Cs. (Cs ! i) ⋅ σs ! i = (Cs ! i) ⋅ τ"
by auto
then have "Cs ⋅⋅cl σs = Cs ⋅cl τ"
using a by (auto intro: nth_equalityI)
then show "∃τ. Cs ⋅⋅cl σs = Cs ⋅cl τ"
by auto
qed
subsubsection ‹Ground Expressions and Substitutions›
lemma ex_ground_subst: "∃σ. is_ground_subst σ"
using make_ground_subst[of "{#}"]
by (simp add: is_ground_cls_def)
lemma is_ground_cls_list_Cons[simp]:
"is_ground_cls_list (C # Cs) = (is_ground_cls C ∧ is_ground_cls_list Cs)"
unfolding is_ground_cls_list_def by auto
paragraph ‹Ground union›
lemma is_ground_atms_union[simp]: "is_ground_atms (AA ∪ BB) ⟷ is_ground_atms AA ∧ is_ground_atms BB"
unfolding is_ground_atms_def by auto
lemma is_ground_atm_mset_union[simp]:
"is_ground_atm_mset (AA + BB) ⟷ is_ground_atm_mset AA ∧ is_ground_atm_mset BB"
unfolding is_ground_atm_mset_def by auto
lemma is_ground_cls_union[simp]: "is_ground_cls (C + D) ⟷ is_ground_cls C ∧ is_ground_cls D"
unfolding is_ground_cls_def by auto
lemma is_ground_clss_union[simp]:
"is_ground_clss (CC ∪ DD) ⟷ is_ground_clss CC ∧ is_ground_clss DD"
unfolding is_ground_clss_def by auto
lemma is_ground_cls_list_is_ground_cls_sum_list[simp]:
"is_ground_cls_list Cs ⟹ is_ground_cls (sum_list Cs)"
by (meson in_mset_sum_list2 is_ground_cls_def is_ground_cls_list_def)
paragraph ‹Grounding simplifications›
lemma grounding_of_clss_empty[simp]: "grounding_of_clss {} = {}"
by (simp add: grounding_of_clss_def)
lemma grounding_of_clss_singleton[simp]: "grounding_of_clss {C} = grounding_of_cls C"
by (simp add: grounding_of_clss_def)
lemma grounding_of_clss_insert:
"grounding_of_clss (insert C N) = grounding_of_cls C ∪ grounding_of_clss N"
by (simp add: grounding_of_clss_def)
lemma grounding_of_clss_union:
"grounding_of_clss (A ∪ B) = grounding_of_clss A ∪ grounding_of_clss B"
by (simp add: grounding_of_clss_def)
paragraph ‹Grounding monotonicity›
lemma is_ground_cls_mono: "C ⊆# D ⟹ is_ground_cls D ⟹ is_ground_cls C"
unfolding is_ground_cls_def by (metis set_mset_mono subsetD)
lemma is_ground_clss_mono: "CC ⊆ DD ⟹ is_ground_clss DD ⟹ is_ground_clss CC"
unfolding is_ground_clss_def by blast
lemma grounding_of_clss_mono: "CC ⊆ DD ⟹ grounding_of_clss CC ⊆ grounding_of_clss DD"
using grounding_of_clss_def by auto
lemma sum_list_subseteq_mset_is_ground_cls_list[simp]:
"sum_list Cs ⊆# sum_list Ds ⟹ is_ground_cls_list Ds ⟹ is_ground_cls_list Cs"
by (meson in_mset_sum_list is_ground_cls_def is_ground_cls_list_is_ground_cls_sum_list
is_ground_cls_mono is_ground_cls_list_def)
paragraph ‹Substituting on ground expression preserves ground›
lemma is_ground_comp_subst[simp]: "is_ground_subst σ ⟹ is_ground_subst (τ ⊙ σ)"
unfolding is_ground_subst_def is_ground_atm_def by auto
lemma ground_subst_ground_atm[simp]: "is_ground_subst σ ⟹ is_ground_atm (A ⋅a σ)"
by (simp add: is_ground_subst_def)
lemma ground_subst_ground_lit[simp]: "is_ground_subst σ ⟹ is_ground_lit (L ⋅l σ)"
unfolding is_ground_lit_def subst_lit_def by (cases L) auto
lemma ground_subst_ground_cls[simp]: "is_ground_subst σ ⟹ is_ground_cls (C ⋅ σ)"
unfolding is_ground_cls_def by auto
lemma ground_subst_ground_clss[simp]: "is_ground_subst σ ⟹ is_ground_clss (CC ⋅cs σ)"
unfolding is_ground_clss_def subst_clss_def by auto
lemma ground_subst_ground_cls_list[simp]: "is_ground_subst σ ⟹ is_ground_cls_list (Cs ⋅cl σ)"
unfolding is_ground_cls_list_def subst_cls_list_def by auto
lemma ground_subst_ground_cls_lists[simp]:
"∀σ ∈ set σs. is_ground_subst σ ⟹ is_ground_cls_list (Cs ⋅⋅cl σs)"
unfolding is_ground_cls_list_def subst_cls_lists_def by (auto simp: set_zip)
lemma subst_cls_eq_grounding_of_cls_subset_eq:
assumes "D ⋅ σ = C"
shows "grounding_of_cls C ⊆ grounding_of_cls D"
proof
fix Cσ'
assume "Cσ' ∈ grounding_of_cls C"
then obtain σ' where
Cσ': "C ⋅ σ' = Cσ'" "is_ground_subst σ'"
unfolding grounding_of_cls_def by auto
then have "C ⋅ σ' = D ⋅ σ ⋅ σ' ∧ is_ground_subst (σ ⊙ σ')"
using assms by auto
then show "Cσ' ∈ grounding_of_cls D"
unfolding grounding_of_cls_def using Cσ'(1) by force
qed
paragraph ‹Substituting on ground expression has no effect›
lemma is_ground_subst_atm[simp]: "is_ground_atm A ⟹ A ⋅a σ = A"
unfolding is_ground_atm_def by simp
lemma is_ground_subst_atms[simp]: "is_ground_atms AA ⟹ AA ⋅as σ = AA"
unfolding is_ground_atms_def subst_atms_def image_def by auto
lemma is_ground_subst_atm_mset[simp]: "is_ground_atm_mset AA ⟹ AA ⋅am σ = AA"
unfolding is_ground_atm_mset_def subst_atm_mset_def by auto
lemma is_ground_subst_atm_list[simp]: "is_ground_atm_list As ⟹ As ⋅al σ = As"
unfolding is_ground_atm_list_def subst_atm_list_def by (auto intro: nth_equalityI)
lemma is_ground_subst_atm_list_member[simp]:
"is_ground_atm_list As ⟹ i < length As ⟹ As ! i ⋅a σ = As ! i"
unfolding is_ground_atm_list_def by auto
lemma is_ground_subst_lit[simp]: "is_ground_lit L ⟹ L ⋅l σ = L"
unfolding is_ground_lit_def subst_lit_def by (cases L) simp_all
lemma is_ground_subst_cls[simp]: "is_ground_cls C ⟹ C ⋅ σ = C"
unfolding is_ground_cls_def subst_cls_def by simp
lemma is_ground_subst_clss[simp]: "is_ground_clss CC ⟹ CC ⋅cs σ = CC"
unfolding is_ground_clss_def subst_clss_def image_def by auto
lemma is_ground_subst_cls_lists[simp]:
assumes "length P = length Cs" and "is_ground_cls_list Cs"
shows "Cs ⋅⋅cl P = Cs"
using assms by (metis is_ground_cls_list_def is_ground_subst_cls min.idem nth_equalityI nth_mem
subst_cls_lists_nth subst_cls_lists_length)
lemma is_ground_subst_lit_iff: "is_ground_lit L ⟷ (∀σ. L = L ⋅l σ)"
using is_ground_atm_def is_ground_lit_def subst_lit_def by (cases L) auto
lemma is_ground_subst_cls_iff: "is_ground_cls C ⟷ (∀σ. C = C ⋅ σ)"
by (metis ex_ground_subst ground_subst_ground_cls is_ground_subst_cls)
paragraph ‹Grounding of substitutions›
lemma grounding_of_subst_cls_subset: "grounding_of_cls (C ⋅ μ) ⊆ grounding_of_cls C"
proof (rule subsetI)
fix D
assume "D ∈ grounding_of_cls (C ⋅ μ)"
then obtain γ where D_def: "D = C ⋅ μ ⋅ γ" and gr_γ: "is_ground_subst γ"
unfolding grounding_of_cls_def mem_Collect_eq by auto
show "D ∈ grounding_of_cls C"
unfolding grounding_of_cls_def mem_Collect_eq D_def
using is_ground_comp_subst[OF gr_γ, of μ]
by force
qed
lemma grounding_of_subst_clss_subset: "grounding_of_clss (CC ⋅cs μ) ⊆ grounding_of_clss CC"
using grounding_of_subst_cls_subset
by (auto simp: grounding_of_clss_def subst_clss_def)
lemma grounding_of_subst_cls_renaming_ident[simp]:
assumes "is_renaming ρ"
shows "grounding_of_cls (C ⋅ ρ) = grounding_of_cls C"
by (metis (no_types, lifting) assms subset_antisym subst_cls_comp_subst
subst_cls_eq_grounding_of_cls_subset_eq subst_cls_id_subst is_renaming_def)
lemma grounding_of_subst_clss_renaming_ident[simp]:
assumes "is_renaming ρ"
shows "grounding_of_clss (CC ⋅cs ρ) = grounding_of_clss CC"
by (metis assms dual_order.eq_iff grounding_of_subst_clss_subset
is_renaming_inv_renaming_cancel_clss)
paragraph ‹Members of ground expressions are ground›
lemma is_ground_cls_as_atms: "is_ground_cls C ⟷ (∀A ∈ atms_of C. is_ground_atm A)"
by (auto simp: atms_of_def is_ground_cls_def is_ground_lit_def)
lemma is_ground_cls_imp_is_ground_lit: "L ∈# C ⟹ is_ground_cls C ⟹ is_ground_lit L"
by (simp add: is_ground_cls_def)
lemma is_ground_cls_imp_is_ground_atm: "A ∈ atms_of C ⟹ is_ground_cls C ⟹ is_ground_atm A"
by (simp add: is_ground_cls_as_atms)
lemma is_ground_cls_is_ground_atms_atms_of[simp]: "is_ground_cls C ⟹ is_ground_atms (atms_of C)"
by (simp add: is_ground_cls_imp_is_ground_atm is_ground_atms_def)
lemma grounding_ground: "C ∈ grounding_of_clss M ⟹ is_ground_cls C"
unfolding grounding_of_clss_def grounding_of_cls_def by auto
lemma is_ground_cls_if_in_grounding_of_cls: "C' ∈ grounding_of_cls C ⟹ is_ground_cls C'"
using grounding_ground grounding_of_clss_singleton by blast
lemma in_subset_eq_grounding_of_clss_is_ground_cls[simp]:
"C ∈ CC ⟹ CC ⊆ grounding_of_clss DD ⟹ is_ground_cls C"
unfolding grounding_of_clss_def grounding_of_cls_def by auto
lemma is_ground_cls_empty[simp]: "is_ground_cls {#}"
unfolding is_ground_cls_def by simp
lemma is_ground_cls_add_mset[simp]:
"is_ground_cls (add_mset L C) ⟷ is_ground_lit L ∧ is_ground_cls C"
by (auto simp: is_ground_cls_def)
lemma grounding_of_cls_ground: "is_ground_cls C ⟹ grounding_of_cls C = {C}"
unfolding grounding_of_cls_def by (simp add: ex_ground_subst)
lemma grounding_of_cls_empty[simp]: "grounding_of_cls {#} = {{#}}"
by (simp add: grounding_of_cls_ground)
lemma union_grounding_of_cls_ground: "is_ground_clss (⋃ (grounding_of_cls ` N))"
by (simp add: grounding_ground grounding_of_clss_def is_ground_clss_def)
lemma is_ground_clss_grounding_of_clss[simp]: "is_ground_clss (grounding_of_clss N)"
using grounding_of_clss_def union_grounding_of_cls_ground by metis
paragraph ‹Grounding idempotence›
lemma grounding_of_grounding_of_cls: "E ∈ grounding_of_cls D ⟹ D ∈ grounding_of_cls C ⟹ E = D"
using grounding_of_cls_def by auto
lemma image_grounding_of_cls_grounding_of_cls:
"grounding_of_cls ` grounding_of_cls C = (λx. {x}) ` grounding_of_cls C"
proof (rule image_cong)
show "⋀x. x ∈ grounding_of_cls C ⟹ grounding_of_cls x = {x}"
using grounding_of_cls_ground is_ground_cls_if_in_grounding_of_cls by blast
qed simp
lemma grounding_of_clss_grounding_of_clss[simp]:
"grounding_of_clss (grounding_of_clss N) = grounding_of_clss N"
unfolding grounding_of_clss_def UN_UN_flatten
unfolding image_grounding_of_cls_grounding_of_cls
by simp
subsubsection ‹Subsumption›
lemma subsumes_empty_left[simp]: "subsumes {#} C"
unfolding subsumes_def subst_cls_def by simp
lemma strictly_subsumes_empty_left[simp]: "strictly_subsumes {#} C ⟷ C ≠ {#}"
unfolding strictly_subsumes_def subsumes_def subst_cls_def by simp
subsubsection ‹Unifiers›
lemma card_le_one_alt: "finite X ⟹ card X ≤ 1 ⟷ X = {} ∨ (∃x. X = {x})"
by (induct rule: finite_induct) auto
lemma is_unifier_subst_atm_eqI:
assumes "finite AA"
shows "is_unifier σ AA ⟹ A ∈ AA ⟹ B ∈ AA ⟹ A ⋅a σ = B ⋅a σ"
unfolding is_unifier_def subst_atms_def card_le_one_alt[OF finite_imageI[OF assms]]
by (metis equals0D imageI insert_iff)
lemma is_unifier_alt:
assumes "finite AA"
shows "is_unifier σ AA ⟷ (∀A ∈ AA. ∀B ∈ AA. A ⋅a σ = B ⋅a σ)"
unfolding is_unifier_def subst_atms_def card_le_one_alt[OF finite_imageI[OF assms(1)]]
by (rule iffI, metis empty_iff insert_iff insert_image, blast)
lemma is_unifiers_subst_atm_eqI:
assumes "finite AA" "is_unifiers σ AAA" "AA ∈ AAA" "A ∈ AA" "B ∈ AA"
shows "A ⋅a σ = B ⋅a σ"
by (metis assms is_unifiers_def is_unifier_subst_atm_eqI)
theorem is_unifiers_comp:
"is_unifiers σ (set_mset ` set (map2 add_mset As Bs) ⋅ass η) ⟷
is_unifiers (η ⊙ σ) (set_mset ` set (map2 add_mset As Bs))"
unfolding is_unifiers_def is_unifier_def subst_atmss_def by auto
subsubsection ‹Most General Unifier›
lemma is_mgu_is_unifiers: "is_mgu σ AAA ⟹ is_unifiers σ AAA"
using is_mgu_def by blast
lemma is_mgu_is_most_general: "is_mgu σ AAA ⟹ is_unifiers τ AAA ⟹ ∃γ. τ = σ ⊙ γ"
using is_mgu_def by blast
lemma is_unifiers_is_unifier: "is_unifiers σ AAA ⟹ AA ∈ AAA ⟹ is_unifier σ AA"
using is_unifiers_def by simp
lemma is_imgu_is_mgu[intro]: "is_imgu σ AAA ⟹ is_mgu σ AAA"
by (auto simp: is_imgu_def is_mgu_def)
lemma is_imgu_comp_idempotent[simp]: "is_imgu σ AAA ⟹ σ ⊙ σ = σ"
by (simp add: is_imgu_def)
lemma is_imgu_subst_atm_idempotent[simp]: "is_imgu σ AAA ⟹ A ⋅a σ ⋅a σ = A ⋅a σ"
using is_imgu_comp_idempotent[of σ] subst_atm_comp_subst[of A σ σ] by simp
lemma is_imgu_subst_atms_idempotent[simp]: "is_imgu σ AAA ⟹ AA ⋅as σ ⋅as σ = AA ⋅as σ"
using is_imgu_comp_idempotent[of σ] subst_atms_comp_subst[of AA σ σ] by simp
lemma is_imgu_subst_lit_idemptotent[simp]: "is_imgu σ AAA ⟹ L ⋅l σ ⋅l σ = L ⋅l σ"
using is_imgu_comp_idempotent[of σ] subst_lit_comp_subst[of L σ σ] by simp
lemma is_imgu_subst_cls_idemptotent[simp]: "is_imgu σ AAA ⟹ C ⋅ σ ⋅ σ = C ⋅ σ"
using is_imgu_comp_idempotent[of σ] subst_cls_comp_subst[of C σ σ] by simp
lemma is_imgu_subst_clss_idemptotent[simp]: "is_imgu σ AAA ⟹ CC ⋅cs σ ⋅cs σ = CC ⋅cs σ"
using is_imgu_comp_idempotent[of σ] subst_clsscomp_subst[of CC σ σ] by simp
subsubsection ‹Generalization and Subsumption›
lemma variants_sym: "variants D D' ⟷ variants D' D"
unfolding variants_def by auto
lemma variants_iff_subsumes: "variants C D ⟷ subsumes C D ∧ subsumes D C"
proof
assume "variants C D"
then show "subsumes C D ∧ subsumes D C"
unfolding variants_def generalizes_def subsumes_def
by (metis subset_mset.refl)
next
assume sub: "subsumes C D ∧ subsumes D C"
then have "size C = size D"
unfolding subsumes_def by (metis antisym size_mset_mono size_subst)
then show "variants C D"
using sub unfolding subsumes_def variants_def generalizes_def
by (metis leD mset_subset_size size_mset_mono size_subst
subset_mset.not_eq_order_implies_strict)
qed
lemma strict_subset_subst_strictly_subsumes: "C ⋅ η ⊂# D ⟹ strictly_subsumes C D"
by (metis leD mset_subset_size size_mset_mono size_subst strictly_subsumes_def
subset_mset.dual_order.strict_implies_order substitution_ops.subsumes_def)
lemma generalizes_lit_refl[simp]: "generalizes_lit L L"
unfolding generalizes_lit_def by (rule exI[of _ id_subst]) simp
lemma generalizes_lit_trans:
"generalizes_lit L1 L2 ⟹ generalizes_lit L2 L3 ⟹ generalizes_lit L1 L3"
unfolding generalizes_lit_def using subst_lit_comp_subst by blast
lemma generalizes_refl[simp]: "generalizes C C"
unfolding generalizes_def by (rule exI[of _ id_subst]) simp
lemma generalizes_trans: "generalizes C D ⟹ generalizes D E ⟹ generalizes C E"
unfolding generalizes_def using subst_cls_comp_subst by blast
lemma subsumes_refl: "subsumes C C"
unfolding subsumes_def by (rule exI[of _ id_subst]) auto
lemma subsumes_trans: "subsumes C D ⟹ subsumes D E ⟹ subsumes C E"
unfolding subsumes_def
by (metis (no_types) subset_mset.trans subst_cls_comp_subst subst_cls_mono_mset)
lemma strictly_generalizes_irrefl: "¬ strictly_generalizes C C"
unfolding strictly_generalizes_def by blast
lemma strictly_generalizes_antisym: "strictly_generalizes C D ⟹ ¬ strictly_generalizes D C"
unfolding strictly_generalizes_def by blast
lemma strictly_generalizes_trans:
"strictly_generalizes C D ⟹ strictly_generalizes D E ⟹ strictly_generalizes C E"
unfolding strictly_generalizes_def using generalizes_trans by blast
lemma strictly_subsumes_irrefl: "¬ strictly_subsumes C C"
unfolding strictly_subsumes_def by blast
lemma strictly_subsumes_antisym: "strictly_subsumes C D ⟹ ¬ strictly_subsumes D C"
unfolding strictly_subsumes_def by blast
lemma strictly_subsumes_trans:
"strictly_subsumes C D ⟹ strictly_subsumes D E ⟹ strictly_subsumes C E"
unfolding strictly_subsumes_def using subsumes_trans by blast
lemma subset_strictly_subsumes: "C ⊂# D ⟹ strictly_subsumes C D"
using strict_subset_subst_strictly_subsumes[of C id_subst] by auto
lemma strictly_generalizes_neq: "strictly_generalizes D' D ⟹ D' ≠ D ⋅ σ"
unfolding strictly_generalizes_def generalizes_def by blast
lemma strictly_subsumes_neq: "strictly_subsumes D' D ⟹ D' ≠ D ⋅ σ"
unfolding strictly_subsumes_def subsumes_def by blast
lemma variants_imp_exists_substitution: "variants D D' ⟹ ∃σ. D ⋅ σ = D'"
unfolding variants_iff_subsumes subsumes_def
by (meson strictly_subsumes_def subset_mset_def strict_subset_subst_strictly_subsumes subsumes_def)
lemma strictly_subsumes_variants:
assumes "strictly_subsumes E D" and "variants D D'"
shows "strictly_subsumes E D'"
proof -
from assms obtain σ σ' where
σ_σ'_p: "D ⋅ σ = D' ∧ D' ⋅ σ' = D"
using variants_imp_exists_substitution variants_sym by metis
from assms obtain σ'' where
"E ⋅ σ'' ⊆# D"
unfolding strictly_subsumes_def subsumes_def by auto
then have "E ⋅ σ'' ⋅ σ ⊆# D ⋅ σ"
using subst_cls_mono_mset by blast
then have "E ⋅ (σ'' ⊙ σ) ⊆# D'"
using σ_σ'_p by auto
moreover from assms have n: "∄σ. D ⋅ σ ⊆# E"
unfolding strictly_subsumes_def subsumes_def by auto
have "∄σ. D' ⋅ σ ⊆# E"
proof
assume "∃σ'''. D' ⋅ σ''' ⊆# E"
then obtain σ''' where
"D' ⋅ σ''' ⊆# E"
by auto
then have "D ⋅ (σ ⊙ σ''') ⊆# E"
using σ_σ'_p by auto
then show False
using n by metis
qed
ultimately show ?thesis
unfolding strictly_subsumes_def subsumes_def by metis
qed
lemma neg_strictly_subsumes_variants:
assumes "¬ strictly_subsumes E D" and "variants D D'"
shows "¬ strictly_subsumes E D'"
using assms strictly_subsumes_variants variants_sym by auto
end
locale substitution_renamings = substitution subst_atm id_subst comp_subst
for
subst_atm :: "'a ⇒ 's ⇒ 'a" and
id_subst :: 's and
comp_subst :: "'s ⇒ 's ⇒ 's" +
fixes
renamings_apart :: "'a clause list ⇒ 's list" and
atm_of_atms :: "'a list ⇒ 'a"
assumes
renamings_apart_length: "length (renamings_apart Cs) = length Cs" and
renamings_apart_renaming: "ρ ∈ set (renamings_apart Cs) ⟹ is_renaming ρ" and
renamings_apart_var_disjoint: "var_disjoint (Cs ⋅⋅cl (renamings_apart Cs))" and
atm_of_atms_subst:
"⋀As Bs. atm_of_atms As ⋅a σ = atm_of_atms Bs ⟷ map (λA. A ⋅a σ) As = Bs"
begin
subsubsection ‹Generalization and Subsumption›
lemma wf_strictly_generalizes: "wfP strictly_generalizes"
proof -
{
assume "∃C_at. ∀i. strictly_generalizes (C_at (Suc i)) (C_at i)"
then obtain C_at :: "nat ⇒ 'a clause" where
sg_C: "⋀i. strictly_generalizes (C_at (Suc i)) (C_at i)"
by blast
define n :: nat where
"n = size (C_at 0)"
have sz_C: "size (C_at i) = n" for i
proof (induct i)
case (Suc i)
then show ?case
using sg_C[of i] unfolding strictly_generalizes_def generalizes_def subst_cls_def
by (metis size_image_mset)
qed (simp add: n_def)
obtain σ_at :: "nat ⇒ 's" where
C_σ: "⋀i. image_mset (λL. L ⋅l σ_at i) (C_at (Suc i)) = C_at i"
using sg_C[unfolded strictly_generalizes_def generalizes_def subst_cls_def] by metis
define Ls_at :: "nat ⇒ 'a literal list" where
"Ls_at = rec_nat (SOME Ls. mset Ls = C_at 0)
(λi Lsi. SOME Ls. mset Ls = C_at (Suc i) ∧ map (λL. L ⋅l σ_at i) Ls = Lsi)"
have
Ls_at_0: "Ls_at 0 = (SOME Ls. mset Ls = C_at 0)" and
Ls_at_Suc: "⋀i. Ls_at (Suc i) =
(SOME Ls. mset Ls = C_at (Suc i) ∧ map (λL. L ⋅l σ_at i) Ls = Ls_at i)"
unfolding Ls_at_def by simp+
have mset_Lt_at_0: "mset (Ls_at 0) = C_at 0"
unfolding Ls_at_0 by (rule someI_ex) (metis list_of_mset_exi)
have "mset (Ls_at (Suc i)) = C_at (Suc i) ∧ map (λL. L ⋅l σ_at i) (Ls_at (Suc i)) = Ls_at i"
for i
proof (induct i)
case 0
then show ?case
by (simp add: Ls_at_Suc, rule someI_ex,
metis C_σ image_mset_of_subset_list mset_Lt_at_0)
next
case Suc
then show ?case
by (subst (1 2) Ls_at_Suc) (rule someI_ex, metis C_σ image_mset_of_subset_list)
qed
note mset_Ls = this[THEN conjunct1] and Ls_σ = this[THEN conjunct2]
have len_Ls: "⋀i. length (Ls_at i) = n"
by (metis mset_Ls mset_Lt_at_0 not0_implies_Suc size_mset sz_C)
have is_pos_Ls: "⋀i j. j < n ⟹ is_pos (Ls_at (Suc i) ! j) ⟷ is_pos (Ls_at i ! j)"
using Ls_σ len_Ls by (metis literal.map_disc_iff nth_map subst_lit_def)
have Ls_τ_strict_lit: "⋀i τ. map (λL. L ⋅l τ) (Ls_at i) ≠ Ls_at (Suc i)"
by (metis C_σ mset_Ls Ls_σ mset_map sg_C generalizes_def strictly_generalizes_def
subst_cls_def)
have Ls_τ_strict_tm:
"map ((λt. t ⋅a τ) ∘ atm_of) (Ls_at i) ≠ map atm_of (Ls_at (Suc i))" for i τ
proof -
obtain j :: nat where
j_lt: "j < n" and
j_τ: "Ls_at i ! j ⋅l τ ≠ Ls_at (Suc i) ! j"
using Ls_τ_strict_lit[of τ i] len_Ls
by (metis (no_types, lifting) length_map list_eq_iff_nth_eq nth_map)
have "atm_of (Ls_at i ! j) ⋅a τ ≠ atm_of (Ls_at (Suc i) ! j)"
using j_τ is_pos_Ls[OF j_lt]
by (metis (mono_guards) literal.expand literal.map_disc_iff literal.map_sel subst_lit_def)
then show ?thesis
using j_lt len_Ls by (metis nth_map o_apply)
qed
define tm_at :: "nat ⇒ 'a" where
"⋀i. tm_at i = atm_of_atms (map atm_of (Ls_at i))"
have "⋀i. generalizes_atm (tm_at (Suc i)) (tm_at i)"
unfolding tm_at_def generalizes_atm_def atm_of_atms_subst
using Ls_σ[THEN arg_cong, of "map atm_of"] by (auto simp: comp_def)
moreover have "⋀i. ¬ generalizes_atm (tm_at i) (tm_at (Suc i))"
unfolding tm_at_def generalizes_atm_def atm_of_atms_subst by (simp add: Ls_τ_strict_tm)
ultimately have "⋀i. strictly_generalizes_atm (tm_at (Suc i)) (tm_at i)"
unfolding strictly_generalizes_atm_def by blast
then have False
using wf_strictly_generalizes_atm[unfolded wfP_def wf_iff_no_infinite_down_chain] by blast
}
then show "wfP (strictly_generalizes :: 'a clause ⇒ _ ⇒ _)"
unfolding wfP_def by (blast intro: wf_iff_no_infinite_down_chain[THEN iffD2])
qed
lemma strictly_subsumes_has_minimum:
assumes "CC ≠ {}"
shows "∃C ∈ CC. ∀D ∈ CC. ¬ strictly_subsumes D C"
proof (rule ccontr)
assume "¬ (∃C ∈ CC. ∀D∈CC. ¬ strictly_subsumes D C)"
then have "∀C ∈ CC. ∃D ∈ CC. strictly_subsumes D C"
by blast
then obtain f where
f_p: "∀C ∈ CC. f C ∈ CC ∧ strictly_subsumes (f C) C"
by metis
from assms obtain C where
C_p: "C ∈ CC"
by auto
define c :: "nat ⇒ 'a clause" where
"⋀n. c n = (f ^^ n) C"
have incc: "c i ∈ CC" for i
by (induction i) (auto simp: c_def f_p C_p)
have ps: "∀i. strictly_subsumes (c (Suc i)) (c i)"
using incc f_p unfolding c_def by auto
have "∀i. size (c i) ≥ size (c (Suc i))"
using ps unfolding strictly_subsumes_def subsumes_def by (metis size_mset_mono size_subst)
then have lte: "∀i. (size ∘ c) i ≥ (size ∘ c) (Suc i)"
unfolding comp_def .
then have "∃l. ∀l' ≥ l. size (c l') = size (c (Suc l'))"
using f_Suc_decr_eventually_const comp_def by auto
then obtain l where
l_p: "∀l' ≥ l. size (c l') = size (c (Suc l'))"
by metis
then have "∀l' ≥ l. strictly_generalizes (c (Suc l')) (c l')"
using ps unfolding strictly_generalizes_def generalizes_def
by (metis size_subst less_irrefl strictly_subsumes_def mset_subset_size subset_mset_def
subsumes_def strictly_subsumes_neq)
then have "∀i. strictly_generalizes (c (Suc i + l)) (c (i + l))"
unfolding strictly_generalizes_def generalizes_def by auto
then have "∃f. ∀i. strictly_generalizes (f (Suc i)) (f i)"
by (rule exI[of _ "λx. c (x + l)"])
then show False
using wf_strictly_generalizes
wf_iff_no_infinite_down_chain[of "{(x, y). strictly_generalizes x y}"]
unfolding wfP_def by auto
qed
lemma wf_strictly_subsumes: "wfP strictly_subsumes"
using strictly_subsumes_has_minimum by (metis equals0D wfP_eq_minimal)
end
subsection ‹Most General Unifiers›
locale mgu = substitution_renamings subst_atm id_subst comp_subst renamings_apart atm_of_atms
for
subst_atm :: "'a ⇒ 's ⇒ 'a" and
id_subst :: 's and
comp_subst :: "'s ⇒ 's ⇒ 's" and
renamings_apart :: "'a literal multiset list ⇒ 's list" and
atm_of_atms :: "'a list ⇒ 'a"+
fixes
mgu :: "'a set set ⇒ 's option"
assumes
mgu_sound: "finite AAA ⟹ (∀AA ∈ AAA. finite AA) ⟹ mgu AAA = Some σ ⟹ is_mgu σ AAA" and
mgu_complete:
"finite AAA ⟹ (∀AA ∈ AAA. finite AA) ⟹ is_unifiers σ AAA ⟹ ∃τ. mgu AAA = Some τ"
begin
lemmas is_unifiers_mgu = mgu_sound[unfolded is_mgu_def, THEN conjunct1]
lemmas is_mgu_most_general = mgu_sound[unfolded is_mgu_def, THEN conjunct2]
lemma mgu_unifier:
assumes
aslen: "length As = n" and
aaslen: "length AAs = n" and
mgu: "Some σ = mgu (set_mset ` set (map2 add_mset As AAs))" and
i_lt: "i < n" and
a_in: "A ∈# AAs ! i"
shows "A ⋅a σ = As ! i ⋅a σ"
proof -
from mgu have "is_mgu σ (set_mset ` set (map2 add_mset As AAs))"
using mgu_sound by auto
then have "is_unifiers σ (set_mset ` set (map2 add_mset As AAs))"
using is_mgu_is_unifiers by auto
then have "is_unifier σ (set_mset (add_mset (As ! i) (AAs ! i)))"
using i_lt aslen aaslen unfolding is_unifiers_def is_unifier_def
by simp (metis length_zip min.idem nth_mem nth_zip prod.case set_mset_add_mset_insert)
then show ?thesis
using aslen aaslen a_in is_unifier_subst_atm_eqI
by (metis finite_set_mset insertCI set_mset_add_mset_insert)
qed
end
subsection ‹Idempotent Most General Unifiers›
locale imgu = mgu subst_atm id_subst comp_subst renamings_apart atm_of_atms mgu
for
subst_atm :: "'a ⇒ 's ⇒ 'a" and
id_subst :: 's and
comp_subst :: "'s ⇒ 's ⇒ 's" and
renamings_apart :: "'a literal multiset list ⇒ 's list" and
atm_of_atms :: "'a list ⇒ 'a" and
mgu :: "'a set set ⇒ 's option" +
assumes
mgu_is_imgu: "finite AAA ⟹ (∀AA ∈ AAA. finite AA) ⟹ mgu AAA = Some σ ⟹ is_imgu σ AAA"
end