Theory equational_clausal_logic

theory equational_clausal_logic

(* N. Peltier - http://membres-lig.imag.fr/peltier/ *)

imports Main terms "HOL-Library.Multiset"

begin

section ‹Equational Clausal Logic›

text ‹The syntax and semantics of clausal equational logic are defined as usual. 
Interpretations are congruences on binary trees.›

subsection ‹Syntax›

text ‹We first define the syntax of equational clauses.›

datatype 'a equation = Eq "'a trm" "'a trm"

fun lhs
  where "lhs (Comb t1 t2) = t1" |
     "lhs (Var x) = (Var x)" |
     "lhs (Const x) = (Const x)"

fun rhs 
  where "rhs (Comb t1 t2) = t2" |
     "rhs (Var x) = (Var x)" |
     "rhs (Const x) = (Const x)"

datatype 'a literal = Pos "'a equation" | Neg "'a equation"

fun atom :: "'a literal ⇒ 'a equation"
  where 
    "(atom (Pos x)) = x" |
    "(atom (Neg x)) = x"

datatype sign = pos | neg
 
fun get_sign :: "'a literal ⇒ sign"
  where 
    "(get_sign (Pos x)) = pos" |
    "(get_sign (Neg x)) = neg"

fun positive_literal :: "'a literal ⇒ bool"
  where
    "(positive_literal (Pos x)) = True" |
    "(positive_literal (Neg x)) = False"

fun negative_literal :: "'a literal ⇒ bool"
  where
    "(negative_literal (Pos x)) = False" |
    "(negative_literal (Neg x)) = True"

fun mk_lit :: "sign ⇒ 'a equation ⇒ 'a literal"
  where 
    "(mk_lit pos x) = (Pos x)" |
    "(mk_lit neg x) = (Neg x)"

definition decompose_equation   
  where "decompose_equation e t s = (e = (Eq t s) ∨ (e = (Eq s t)))"

definition decompose_literal 
  where "decompose_literal L t s p = 
            (∃e. ((p = pos ∧ (L = (Pos e)) ∧ decompose_equation e t s)
            ∨ (p = neg ∧ (L = (Neg e)) ∧ decompose_equation e t s)))"

fun subterms_of_eq 
  where "subterms_of_eq (Eq t s) = (subterms_of t ∪ subterms_of s)"

fun vars_of_eq 
  where "vars_of_eq (Eq t s) = (vars_of t ∪ vars_of s)"

lemma decompose_equation_vars:
  assumes "decompose_equation e t s"
  shows "vars_of t ⊆ vars_of_eq e"
by (metis assms decompose_equation_def sup.cobounded1 sup_commute vars_of_eq.simps)

fun subterms_of_lit 
  where 
    "subterms_of_lit (Pos e) = (subterms_of_eq e)" |
    "subterms_of_lit (Neg e) = (subterms_of_eq e)"

fun vars_of_lit 
  where 
    "vars_of_lit (Pos e) = (vars_of_eq e)" |
    "vars_of_lit (Neg e) = (vars_of_eq e)"

fun vars_of_cl 
  where "vars_of_cl C = { x. ∃L. x ∈ (vars_of_lit L) ∧ L ∈ C }"

fun subterms_of_cl 
  where "subterms_of_cl C = { x. ∃L. x ∈ (subterms_of_lit L) ∧ L ∈ C }"

text ‹Note that clauses are defined as sets and not as multisets 
(identical literals are always merged).›

type_synonym 'a clause = "'a literal set"

fun ground_clause :: "'a clause ⇒ bool"
where
  "(ground_clause C) = ((vars_of_cl C) = {})"

fun subst_equation :: "'a equation ⇒ 'a subst ⇒ 'a equation"
where
  "(subst_equation (Eq u v) s) 
    = (Eq (subst u s) (subst v s))"

fun subst_lit :: "'a literal ⇒ 'a subst ⇒ 'a literal"
where
  "(subst_lit (Pos e) s) 
    = (Pos (subst_equation e s))" |
  "(subst_lit (Neg e) s) 
    = (Neg (subst_equation e s))" 

fun subst_cl :: "'a clause ⇒ 'a subst ⇒ 'a clause"
where
  "(subst_cl C s) = { L. (∃L'. (L' ∈ C) ∧ (L = (subst_lit L' s))) }" 

text ‹We establish some properties of the functions returning the set of variables occurring in 
an object.›

lemma decompose_literal_vars:
  assumes "decompose_literal L t s p"
  shows "vars_of t ⊆ vars_of_lit L"
by (metis assms decompose_equation_vars decompose_literal_def vars_of_lit.simps(1) vars_of_lit.simps(2))

lemma vars_of_cl_lem:
  assumes "L ∈ C"
  shows "vars_of_lit L ⊆ vars_of_cl C"
using assms by auto

lemma set_of_variables_is_finite_eq:
  shows "finite (vars_of_eq e)"
proof -
  obtain t and s where "e = Eq t s" using equation.exhaust by auto  
  then have "vars_of_eq e = (vars_of t) ∪ (vars_of s)" by auto
  from this show ?thesis by auto
qed

lemma set_of_variables_is_finite_lit:
  shows "finite (vars_of_lit l)"
proof -
  obtain e where "l = Pos e ∨ l = Neg e" using literal.exhaust by auto 
  then have "vars_of_lit l = (vars_of_eq e)" by auto
  from this show ?thesis using set_of_variables_is_finite_eq by auto
qed

lemma set_of_variables_is_finite_cl:
  assumes "finite C"
  shows "finite (vars_of_cl C)"
proof -
  let ?S = "{ x. ∃l. x = vars_of_lit l ∧ l ∈ C }"
  have "vars_of_cl C = ⋃ ?S" by auto
  from assms have "finite ?S" by auto
  { fix x have "x ∈ ?S ⟹ finite x" using set_of_variables_is_finite_lit by auto }
  from this and ‹finite ?S› have "finite (⋃ ?S)" using finite_Union by auto
  from this and ‹vars_of_cl C = ⋃ ?S› show ?thesis by auto
qed

lemma subterm_lit_vars :
  assumes "u ∈ subterms_of_lit L"
  shows "vars_of u ⊆ vars_of_lit L"
proof -
  obtain e where def_e: "L = (Pos e) ∨ L = (Neg e)" and "vars_of_lit L = vars_of_eq e"
    by (metis negative_literal.elims(2) negative_literal.elims(3) 
      vars_of_lit.simps(1) vars_of_lit.simps(2))
  obtain t and s where def_ts: "e = (Eq t s) ∨ e = (Eq s t)" and "vars_of_eq e = vars_of t ∪ vars_of s"
    by (metis equation.exhaust vars_of_eq.simps)
  from this and ‹vars_of_lit L = vars_of_eq e› have "vars_of_lit L = vars_of t ∪ vars_of s" by auto
  from assms(1) and def_e def_ts have "u ∈ subterms_of t ∪ subterms_of s" by auto
  from this have "vars_of u ⊆ vars_of t ∪ vars_of s"
    by (meson UnE sup.coboundedI1 sup.coboundedI2 vars_subterms_of)
  from this and ‹vars_of_lit L = vars_of t ∪ vars_of s› show ?thesis by auto
qed

lemma subterm_vars :
  assumes "u ∈ subterms_of_cl C"
  shows "vars_of u ⊆ vars_of_cl C"
proof -
  from assms(1) obtain L where "u ∈ subterms_of_lit L" and "L ∈ C" by auto
  from ‹u ∈ subterms_of_lit L› have "vars_of u ⊆ vars_of_lit L" using subterm_lit_vars by auto
  from  ‹L ∈ C› have "vars_of_lit L ⊆ vars_of_cl C" using vars_of_cl.simps by auto
  from this and ‹vars_of u ⊆ vars_of_lit L› show ?thesis by auto
qed

text ‹We establish some basic properties of substitutions.›

lemma subterm_cl_subst:
  assumes "x ∈ (subterms_of_cl C)"
  shows "(subst x σ) ∈  (subterms_of_cl (subst_cl C σ))"
proof -
  from assms(1) obtain L where "L ∈ C" and "x ∈ subterms_of_lit L" by auto
  from ‹L ∈ C› have "(subst_lit L σ) ∈ (subst_cl C σ)" by auto
  obtain e where "L = (Pos e) ∨ L = (Neg e)" using literal.exhaust by auto
  then show ?thesis
  proof
    assume "L = (Pos e)" 
    from this and ‹x ∈ subterms_of_lit L› have "x ∈ subterms_of_eq e" by auto
    from ‹L = (Pos e)› have "(subst_lit L σ) = (Pos (subst_equation e σ))"
      by auto
    obtain t s where "e = (Eq t s)" using equation.exhaust by auto
    from this have "(subst_equation e σ) = (Eq (subst t σ)  (subst s σ))"
      by auto
    from ‹x ∈ subterms_of_eq e› and ‹e = (Eq t s)› have "x ∈ subterms_of t ∨ x ∈ subterms_of s" by auto
    then show ?thesis
    proof
      assume "x ∈ subterms_of t"
      then have "occurs_in x t" by auto
      then obtain p where "subterm t p x" unfolding occurs_in_def by blast
      from this have "subterm (subst t σ) p (subst x σ)"
        using substs_preserve_subterms by auto 
      from this have "occurs_in (subst x σ) (subst t σ)" unfolding occurs_in_def by auto
      then have "(subst x σ) ∈ subterms_of (subst t σ)" by auto
      then have "(subst x σ) ∈ subterms_of_eq (Eq (subst t σ) (subst s σ))" by auto
      from this and ‹L = (Pos e)› and ‹e = Eq t s› 
        have "(subst x σ) ∈ (subterms_of_lit (subst_lit L σ))" by auto
      from this and ‹(subst_lit L σ) ∈ (subst_cl C σ)› 
        show "(subst x σ) ∈ subterms_of_cl (subst_cl C σ)" by auto
    next
      assume "x ∈ subterms_of s"
      then have "occurs_in x s" by auto
      then obtain p where "subterm s p x" unfolding occurs_in_def by blast
      from this have "subterm (subst s σ) p (subst x σ)"
        using substs_preserve_subterms by auto 
      from this have "occurs_in (subst x σ) (subst s σ)" unfolding occurs_in_def by auto
      then have "(subst x σ) ∈ subterms_of (subst s σ)" by auto
      then have "(subst x σ) ∈ subterms_of_eq (Eq (subst t σ) (subst s σ))" by auto
      from this and ‹L = (Pos e)› and ‹e = Eq t s› 
        have "(subst x σ) ∈ (subterms_of_lit (subst_lit L σ))" by auto
      from this and ‹(subst_lit L σ) ∈ (subst_cl C σ)› 
        show "(subst x σ) ∈ subterms_of_cl (subst_cl C σ)" by auto
    qed
    next
    assume "L = (Neg e)" 
    from this and ‹x ∈ subterms_of_lit L› have "x ∈ subterms_of_eq e" by auto
    from ‹L = (Neg e)› have "(subst_lit L σ) = (Neg (subst_equation e σ))"
      by auto
    obtain t s where "e = (Eq t s)" using equation.exhaust by auto
    from this have "(subst_equation e σ) = (Eq (subst t σ)  (subst s σ))"
      by auto
    from ‹x ∈ subterms_of_eq e› and ‹e = (Eq t s)› have "x ∈ subterms_of t ∨ x ∈ subterms_of s" by auto
    then show ?thesis
    proof
      assume "x ∈ subterms_of t"
      then have "occurs_in x t" by auto
      then obtain p where "subterm t p x" unfolding occurs_in_def by blast
      from this have "subterm (subst t σ) p (subst x σ)"
        using substs_preserve_subterms by auto 
      from this have "occurs_in (subst x σ) (subst t σ)" unfolding occurs_in_def by auto
      then have "(subst x σ) ∈ subterms_of (subst t σ)" by auto
      then have "(subst x σ) ∈ subterms_of_eq (Eq (subst t σ) (subst s σ))" by auto
      from this and ‹L = (Neg e)› and ‹e = Eq t s› 
        have "(subst x σ) ∈ (subterms_of_lit (subst_lit L σ))" by auto
      from this and ‹(subst_lit L σ) ∈ (subst_cl C σ)› 
        show "(subst x σ) ∈ subterms_of_cl (subst_cl C σ)" by auto
    next
      assume "x ∈ subterms_of s"
      then have "occurs_in x s" by auto
      then obtain p where "subterm s p x" unfolding occurs_in_def by blast
      from this have "subterm (subst s σ) p (subst x σ)"
        using substs_preserve_subterms by auto 
      from this have "occurs_in (subst x σ) (subst s σ)" unfolding occurs_in_def by auto
      then have "(subst x σ) ∈ subterms_of (subst s σ)" by auto
      then have "(subst x σ) ∈ subterms_of_eq (Eq (subst t σ) (subst s σ))" by auto
      from this and ‹L = (Neg e)› and ‹e = Eq t s› 
        have "(subst x σ) ∈ (subterms_of_lit (subst_lit L σ))" by auto
      from this and ‹(subst_lit L σ) ∈ (subst_cl C σ)› 
        show "(subst x σ) ∈ subterms_of_cl (subst_cl C σ)" by auto
    qed
  qed
qed

lemma ground_substs_yield_ground_clause:
  assumes "ground_on (vars_of_cl C) σ"
  shows "ground_clause (subst_cl C σ)"
proof (rule ccontr)
    let ?D = "(subst_cl C σ)"
    let ?V = "(vars_of_cl C)"
    assume "¬(ground_clause ?D)"
    then obtain x where "x ∈ (vars_of_cl ?D)" by auto
    then obtain l where "l ∈ C" and "x ∈ (vars_of_lit (subst_lit l  σ))" by auto
    from ‹l ∈ C› have "vars_of_lit l ⊆ vars_of_cl C" by auto
    obtain e  where "l = Pos e ∨ l = Neg e" using literal.exhaust by auto 
    then have "vars_of_lit l = vars_of_eq e" by auto
    let ?l' = "(subst_lit l σ)" 
    let ?e' = "(subst_equation e σ)" 
    obtain t and s where "e = Eq t s" using equation.exhaust by auto 
    then have "vars_of_eq e = vars_of t ∪ vars_of s" by auto
    let ?t' = "(subst t σ)" 
    let ?s' = "(subst s σ)" 
    from ‹e = Eq t s› have "?e' = (Eq ?t' ?s')" by auto
    from ‹l = Pos e ∨ l = Neg e› have "?l' = Pos ?e' ∨ ?l' = Neg ?e'" by auto    
    from ‹l ∈ C› have "?l' ∈ ?D" by auto
    from ‹?l' = Pos ?e' ∨ ?l' = Neg ?e'› and ‹x ∈ (vars_of_lit ?l')› 
      have "x ∈ (vars_of_eq ?e')" by auto
    from this and ‹?e' = (Eq ?t' ?s')› have "x ∈ (vars_of ?t' ∪ vars_of ?s')" by auto 
    then have i:"¬(ground_term ?t') ∨ ¬(ground_term ?s')" unfolding ground_term_def by auto
    from ‹vars_of_eq e = vars_of t ∪ vars_of s› and ‹vars_of_lit l = vars_of_eq e› and
      ‹vars_of_lit l ⊆ ?V› have "vars_of t ⊆ ?V" and "vars_of s ⊆ ?V" by auto
    from ‹vars_of t  ⊆ ?V› and ‹ground_on ?V σ› have  "ground_on (vars_of t) σ" 
      unfolding ground_on_def by auto
    then have ii:"ground_term ?t'" using ground_instance by auto
    from ‹vars_of s  ⊆ ?V› and ‹ground_on ?V σ› have  "ground_on (vars_of s) σ" 
      unfolding ground_on_def by auto
    then have iii:"ground_term ?s'" using ground_instance by auto
    from i and ii and iii show False by auto
qed

lemma ground_clauses_and_ground_substs:
  assumes "ground_clause (subst_cl C σ)"
  shows "ground_on (vars_of_cl C) σ"
proof (rule ccontr)
  assume "¬ground_on (vars_of_cl C) σ"
  from this obtain x where "x ∈ vars_of_cl C" and "¬ ground_term (subst (Var x) σ)"
    unfolding ground_on_def by auto
  from ‹¬ ground_term (subst (Var x) σ)› obtain y where 
    "y ∈ vars_of (subst (Var x) σ)" unfolding ground_term_def by auto
  from ‹x ∈ vars_of_cl C› obtain L where "L ∈ C" and "x ∈ vars_of_lit L" by auto
  from ‹x ∈ vars_of_lit L› obtain e where "L = Pos e ∨ L = Neg e" and "x ∈ vars_of_eq e"
    by (metis vars_of_lit.elims) 
  from ‹x ∈ vars_of_eq e› obtain t s where "e = (Eq t s)" and "x ∈ vars_of t ∪ vars_of s"
    by (metis vars_of_eq.elims) 
  from this have "x ∈ vars_of t ∨ x ∈ vars_of s" by auto
  then have "y ∈ vars_of_eq (subst_equation e σ)"
  proof
    assume "x ∈ vars_of t"
    have i: "vars_of (subst t σ) = ⋃{V. ∃x. x ∈ vars_of t ∧ V = vars_of (subst (Var x) σ) }"
      using vars_of_instances [of t σ] by meson 
    from ‹x ∈ vars_of t›  i 
      have "vars_of (subst (Var x) σ) ⊆ vars_of (subst t σ)" 
      by auto
    from this and ‹y ∈ vars_of (subst (Var x) σ)› ‹e = (Eq t s)› show ?thesis by auto
  next
    assume "x ∈ vars_of s"
    have i: "vars_of (subst s σ) = ⋃{V. ∃x. x ∈ vars_of s ∧ V = vars_of (subst (Var x) σ) }"
      using vars_of_instances [of s σ] by meson 
    from ‹x ∈ vars_of s› i 
      have "vars_of (subst (Var x) σ) ⊆ vars_of (subst s σ)" 
      by auto
    from this and ‹y ∈ vars_of (subst (Var x) σ)› ‹e = (Eq t s)› show ?thesis by auto
  qed
  from this and ‹L = Pos e ∨ L = Neg e› have "y ∈ vars_of_lit (subst_lit L σ)"
    by auto
  from this and ‹L ∈ C› have "y ∈ vars_of_cl (subst_cl C σ)" by auto
  from this and assms(1) show False by auto
qed

lemma ground_instance_exists:
  assumes "finite C"
  shows "∃σ. (ground_clause (subst_cl C σ))"
proof -
  let ?V = "(vars_of_cl C)"
  from assms have "finite ?V" using set_of_variables_is_finite_cl by auto
  from this obtain σ where "ground_on ?V σ" 
    using ground_subst_exists by blast
  let ?D = "(subst_cl C σ)"
  from ‹ground_on ?V σ› have "(ground_clause ?D)" using ground_substs_yield_ground_clause [of C σ] by auto
  then show ?thesis by auto
qed

lemma composition_of_substs :
  shows "(subst (subst t  σ) η) 
    = (subst t (comp σ η))"
by simp

lemma composition_of_substs_eq :
  shows "(subst_equation (subst_equation e σ) η) 
    = (subst_equation e (comp σ η))"
by (metis subst_equation.simps composition_of_substs vars_of_eq.elims)

lemma composition_of_substs_lit :
  shows "(subst_lit (subst_lit l σ) η) 
    = (subst_lit l (comp σ η))"
by (metis subst_lit.simps(1) subst_lit.simps(2) 
    composition_of_substs_eq positive_literal.cases)

lemma composition_of_substs_cl :
  shows "(subst_cl (subst_cl C σ) η) 
    = (subst_cl C (comp σ η))"
proof -
  let ?f = "(λx. (subst_lit (subst_lit x  σ) η))"
  let ?f' = "(λx. (subst_lit x (comp σ η)))"
  have "∀l. (?f l) = (?f' l)" using composition_of_substs_lit by auto
  then show ?thesis by auto
qed

lemma substs_preserve_ground_lit :
  assumes "ground_clause C"
  assumes "y ∈ C"
  shows "subst_lit y σ = y"
proof - 
    obtain t and s where "y = Pos (Eq t s) ∨ y = Neg (Eq t s)" 
      by (metis subst_equation.elims get_sign.elims)
    from this have "vars_of t ⊆ vars_of_lit y" by auto 
    from this and ‹y ∈ C› have "vars_of t ⊆ vars_of_cl C" by auto 
    from this and assms(1) have "ground_term t" unfolding ground_term_def by auto
    then have "subst t σ = t" using substs_preserve_ground_terms by auto
    from ‹y = Pos (Eq t s) ∨ y = Neg (Eq t s)› have "vars_of s ⊆ vars_of_lit y" by auto 
    from this and ‹y ∈ C› have "vars_of s ⊆ vars_of_cl C" by auto 
    from this and assms(1) have "ground_term s" unfolding ground_term_def by auto
    then have "subst s σ = s" using substs_preserve_ground_terms by auto
    from ‹subst s σ = s› and ‹subst t σ = t› and ‹y = Pos (Eq t s) ∨ y = Neg (Eq t s)›
    show "subst_lit y σ = y" by auto
qed
  
lemma substs_preserve_ground_clause :
  assumes "ground_clause C"
  shows "subst_cl C σ = C"
proof 
  show "subst_cl C σ ⊆ C"
  proof
    fix x assume "x ∈ subst_cl C σ"
    then obtain y where "y ∈ C" and "x = subst_lit y σ" by auto
    from assms(1) and ‹y ∈ C› and ‹x = subst_lit y σ› 
      have "x = y" using substs_preserve_ground_lit by auto
    from this and ‹y ∈ C› show "x ∈ C" by auto
  qed
next
  show "C ⊆ subst_cl C σ"
  proof 
    fix x assume "x ∈ C"
    then have "subst_lit x σ ∈ subst_cl C σ" by auto
    from assms(1) and ‹x ∈ C› have "x = subst_lit x σ" 
      using substs_preserve_ground_lit [of C x] by auto
    from this and ‹x ∈ C› show "x ∈ subst_cl C σ" by auto
  qed
qed

lemma substs_preserve_finiteness :
  assumes "finite C"
  shows "finite (subst_cl C σ)"
proof -
  from assms(1) show ?thesis using Finite_Set.finite_imageI by auto
qed

text ‹We prove that two equal substitutions yield the same objects.›
 
lemma subst_eq_eq :
  assumes "subst_eq σ η"
  shows "subst_equation e σ = subst_equation e η"
proof -
  obtain t and s where "e = Eq t s" using equation.exhaust by auto 
  from assms(1) have "subst s σ = subst s η" by auto
  from assms(1) have "subst t σ = subst t η" by auto
  from ‹subst s σ = subst s η› ‹subst t σ = subst t η›
    and ‹e = Eq t s› show ?thesis by auto
qed

lemma subst_eq_lit :
  assumes "subst_eq σ η"
  shows "subst_lit l σ = subst_lit l η"
proof -
  obtain e where "l = Pos e ∨ l = Neg e" using literal.exhaust by auto 
  from assms(1)  have "subst_equation e σ = subst_equation e η" using subst_eq_eq by auto
  from this and ‹l = Pos e ∨ l = Neg e› show ?thesis by auto
qed

lemma subst_eq_cl:
  assumes "subst_eq σ η"
  shows "subst_cl C σ = subst_cl C η"
proof (rule ccontr)
  assume "subst_cl C σ ≠ subst_cl C η"
  then obtain L where "L ∈ C" and "subst_lit L σ ≠ subst_lit L η"
    by force
  from assms(1) and ‹subst_lit L σ ≠ subst_lit L η› 
    show False using subst_eq_lit by auto
qed

lemma coincide_on_eq :
  assumes "coincide_on σ η (vars_of_eq e)"
  shows "subst_equation e σ = subst_equation e η"
proof -
  obtain t and s where "e = Eq t s" using equation.exhaust by auto 
  then have "vars_of t ⊆ vars_of_eq e" by simp
  from this and ‹coincide_on σ η (vars_of_eq e)› have "coincide_on σ η (vars_of t)" 
    unfolding coincide_on_def by auto
  from this have "subst t σ = subst t η" using coincide_on_term by auto
  from ‹e = Eq t s›  have "vars_of s ⊆ vars_of_eq e" by simp
  from this and ‹coincide_on σ η (vars_of_eq e)› have "coincide_on σ η (vars_of s)" 
    unfolding coincide_on_def by auto
  from this have "subst s σ = subst s η" using coincide_on_term by auto
  from ‹subst t σ = subst t η› 
    and ‹subst s σ = subst s η› 
    and ‹e = Eq t s› show ?thesis by auto
qed

lemma coincide_on_lit :
  assumes "coincide_on σ η (vars_of_lit l)"
  shows "subst_lit l σ = subst_lit l η"
proof -
  obtain e where "l = Pos e ∨ l = Neg e" using literal.exhaust by auto 
  then have "vars_of_eq e ⊆ vars_of_lit l" by auto 
  from this and ‹coincide_on σ η (vars_of_lit l)› have "coincide_on σ η (vars_of_eq e)" 
    unfolding coincide_on_def by auto
  from this have "subst_equation e σ = subst_equation e η" 
    using coincide_on_eq by auto
  from this and ‹l = Pos e ∨ l = Neg e› show ?thesis by auto
qed

lemma coincide_on_cl :
  assumes "coincide_on σ η (vars_of_cl C)"
  shows "subst_cl C σ = subst_cl C η"
proof (rule ccontr)
  assume "subst_cl C σ ≠ subst_cl C η"
  then obtain L where "L ∈ C" and "subst_lit L σ ≠ subst_lit L η"
    by force
  from ‹L ∈ C› have "vars_of_lit L ⊆ vars_of_cl C" by auto
  from this and assms have "coincide_on σ η (vars_of_lit L)" unfolding coincide_on_def by auto
  from this and ‹subst_lit L σ ≠ subst_lit L η› 
    show False using coincide_on_lit by auto
qed

subsection ‹Semantics›

text ‹Interpretations are congruences on the set of terms.›

definition fo_interpretation :: "'a binary_relation_on_trms ⇒ bool"
where 
  "(fo_interpretation x) = (congruence x)"

fun validate_ground_eq :: "'a binary_relation_on_trms ⇒ 'a equation  ⇒ bool"
where
"(validate_ground_eq I (Eq t s) = (I t s))"

fun validate_ground_lit :: "'a binary_relation_on_trms ⇒ 'a literal  ⇒ bool"
where
"validate_ground_lit I (Pos E) = (validate_ground_eq I E)" |
"validate_ground_lit I (Neg E) = (¬(validate_ground_eq I E))"

fun validate_ground_clause :: "'a binary_relation_on_trms ⇒ 'a clause ⇒ bool"
where
"validate_ground_clause I C = (∃L.(L ∈ C) ∧ (validate_ground_lit I L))"

fun validate_clause :: "'a binary_relation_on_trms ⇒ 'a clause ⇒ bool"
where
"validate_clause I C = (∀s. (ground_clause (subst_cl C s)) 
  ⟶ (validate_ground_clause I (subst_cl C s)))"

fun validate_clause_set :: "'a binary_relation_on_trms ⇒ 'a clause set ⇒ bool"
where
"validate_clause_set I S = (∀C. (C ∈ S  ⟶ (validate_clause I C)))"

definition clause_entails_clause :: "'a clause ⇒ 'a clause ⇒ bool"
where
  "clause_entails_clause C D = (∀I. (fo_interpretation I ⟶ validate_clause I C ⟶ validate_clause I D))"

definition set_entails_clause :: "'a clause set ⇒ 'a clause ⇒ bool"
where
  "set_entails_clause S C = (∀I. (fo_interpretation I ⟶ validate_clause_set I S ⟶ validate_clause I C))"

definition satisfiable_clause_set :: "'a clause set ⇒ bool"
 where  
 "(satisfiable_clause_set S) = (∃I. (fo_interpretation I) ∧ (validate_clause_set I S))"

text ‹We state basic properties of the entailment relation.›

lemma set_entails_clause_member:
  assumes "C ∈ S"
  shows "set_entails_clause S C"
proof (rule ccontr)
  assume "¬ ?thesis"
  from this obtain I where "fo_interpretation I" "validate_clause_set I S" "¬ validate_clause I C" 
    unfolding set_entails_clause_def by auto
  from ‹validate_clause_set I S› and assms(1) ‹¬ validate_clause I C› show False  by auto
qed

lemma instances_are_entailed :
  assumes "validate_clause I C"
  shows "validate_clause I (subst_cl C σ)"
proof (rule ccontr)
  assume "¬validate_clause I (subst_cl C σ)"
  then obtain η 
    where "¬validate_ground_clause I (subst_cl (subst_cl C σ) η)" 
      and "ground_clause (subst_cl (subst_cl C σ) η)"
    by auto
  then have i: "¬validate_ground_clause I (subst_cl C (comp σ η))"
   using composition_of_substs_cl by metis 
  from ‹ground_clause (subst_cl (subst_cl C σ) η)› 
    have ii: "ground_clause (subst_cl C (comp σ η))" 
    using composition_of_substs_cl by metis
  from i and ii have "¬validate_clause I C" by auto
  from ‹¬validate_clause I C› and ‹validate_clause I C› show False by blast
qed

text ‹We prove that two equivalent substitutions yield equivalent objects.›

lemma equivalent_on_eq :
  assumes "equivalent_on σ η (vars_of_eq e) I"
  assumes "fo_interpretation I"
  shows "(validate_ground_eq I (subst_equation e σ)) = (validate_ground_eq I (subst_equation e η))"
proof -
  obtain t and s where "e = Eq t s" using equation.exhaust by auto 
  then have "vars_of t ⊆ vars_of_eq e" by simp
  from this and assms(1) have "equivalent_on σ η (vars_of t) I" 
    unfolding equivalent_on_def by auto
  from this assms(2) 
    have "I (subst t σ) (subst t η)" using equivalent_on_term 
    unfolding fo_interpretation_def by auto
  from ‹e = Eq t s›  have "vars_of s ⊆ vars_of_eq e" by simp
  from this and ‹equivalent_on σ η (vars_of_eq e) I› have "equivalent_on σ η (vars_of s) I" 
    unfolding equivalent_on_def by auto
  from this assms(2) have "I (subst s σ) (subst s η)" 
    using equivalent_on_term unfolding fo_interpretation_def by auto
  from assms(2) ‹I (subst t σ) (subst t η)› 
    and ‹I (subst s σ) (subst s η)› 
    and ‹e = Eq t s› show ?thesis unfolding fo_interpretation_def congruence_def equivalence_relation_def 
    transitive_def symmetric_def reflexive_def
    by (metis (full_types) subst_equation.simps validate_ground_eq.simps)   
qed

lemma equivalent_on_lit :
  assumes "equivalent_on σ η (vars_of_lit l) I"
  assumes "fo_interpretation I"
  shows "(validate_ground_lit I (subst_lit l σ)) 
    = (validate_ground_lit I (subst_lit l η))"
proof -
  obtain e where "l = Pos e ∨ l = Neg e" using literal.exhaust by auto 
  then have "vars_of_eq e ⊆ vars_of_lit l" by auto 
  from this and ‹equivalent_on σ η (vars_of_lit l) I› have "equivalent_on σ η (vars_of_eq e) I" 
    unfolding equivalent_on_def by auto
  from this assms(2) have "(validate_ground_eq I (subst_equation e σ)) = (validate_ground_eq I (subst_equation e η))" 
    using equivalent_on_eq by auto
  from this and ‹l = Pos e ∨ l = Neg e› show ?thesis by auto
qed

lemma equivalent_on_cl :
  assumes "equivalent_on σ η (vars_of_cl C) I"
  assumes "fo_interpretation I"
  shows "(validate_ground_clause I (subst_cl C σ)) 
    = (validate_ground_clause I (subst_cl C η))"
proof (rule ccontr)
  assume "(validate_ground_clause I (subst_cl C σ)) 
    ≠ (validate_ground_clause I (subst_cl C η))"
  then obtain L where "L ∈ C" and "(validate_ground_lit I (subst_lit L σ)) 
    ≠ (validate_ground_lit I (subst_lit L η))"
    by force
  from ‹L ∈ C› have "vars_of_lit L ⊆ vars_of_cl C" by auto
  from this and assms have "equivalent_on σ η (vars_of_lit L) I" unfolding equivalent_on_def by auto
  from this assms(2) and ‹(validate_ground_lit I (subst_lit L σ)) 
    ≠ (validate_ground_lit I (subst_lit L η))› 
    show False using equivalent_on_lit by metis
qed

end