Theory Ordered_Resolution_Prover.Abstract_Substitution

(*  Title:       Abstract Substitutions
    Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
    Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
    Author:      Anders Schlichtkrull <andschl at dtu.dk>, 2016, 2017
    Author:      Martin Desharnais <desharnais at mpi-inf.mpg.de>, 2022
    Maintainer:  Anders Schlichtkrull <andschl at dtu.dk>
*)

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. DCC. ¬ 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