Theory BasicDPLL

(*    Title:              SatSolverVerification/BasicDPLL.thy
      Author:             Filip Maric
      Maintainer:         Filip Maric <filip at matf.bg.ac.yu>
*)

section‹BasicDPLL›
theory BasicDPLL
imports SatSolverVerification
begin

text‹This theory formalizes the transition rule system BasicDPLL
 which is based on the classical DPLL procedure, but does not use the
 PureLiteral rule.›

(******************************************************************************)
subsection‹Specification›
(******************************************************************************)

text‹The state of the procedure is uniquely determined by its trail.›
record State = 
"getM" :: LiteralTrail

text‹Procedure checks the satisfiability of the formula F0 which
  does not change during the solving process. An external parameter is
  the set @{term decisionVars} which are the variables that branching
  is performed on. Usually this set contains all variables of the
  formula F0, but that does not always have to be the case.›


text‹Now we define the transition rules of the system›
definition
appliedDecide:: "State ⇒ State ⇒ Variable set ⇒ bool"
where
"appliedDecide stateA stateB decisionVars == 
  ∃ l. 
        (var l) ∈ decisionVars ∧ 
        ¬ l el (elements (getM stateA)) ∧ 
        ¬ opposite l el (elements (getM stateA)) ∧

        getM stateB = getM stateA @ [(l, True)]
"
definition
applicableDecide :: "State ⇒ Variable set ⇒ bool"
where
"applicableDecide state decisionVars == ∃ state'. appliedDecide state state' decisionVars"

definition
appliedUnitPropagate :: "State ⇒ State ⇒ Formula ⇒ bool"
where
"appliedUnitPropagate stateA stateB F0 == 
  ∃ (uc::Clause) (ul::Literal). 
       uc el F0 ∧ 
       isUnitClause uc ul (elements (getM stateA)) ∧ 

       getM stateB = getM stateA @ [(ul, False)]
"
definition
applicableUnitPropagate :: "State ⇒ Formula ⇒ bool"
where
"applicableUnitPropagate state F0 == ∃ state'. appliedUnitPropagate state state' F0"

definition
appliedBacktrack :: "State ⇒ State ⇒ Formula ⇒ bool"
where
"appliedBacktrack stateA stateB F0 == 
      formulaFalse F0 (elements (getM stateA)) ∧ 
      decisions (getM stateA) ≠ [] ∧ 

      getM stateB = prefixBeforeLastDecision (getM stateA) @ [(opposite (lastDecision (getM stateA)), False)]
"
definition
applicableBacktrack :: "State ⇒ Formula ⇒ bool"
where
"applicableBacktrack state F0 ==  ∃ state'. appliedBacktrack state state' F0"


text‹Solving starts with the empty trail.›
definition
isInitialState :: "State ⇒ Formula ⇒ bool"
where
"isInitialState state F0 == 
      getM state = []
"
text‹Transitions are preformed only by using one of the three given rules.›
definition
"transition stateA stateB F0 decisionVars == 
     appliedDecide        stateA stateB decisionVars ∨
     appliedUnitPropagate stateA stateB F0  ∨ 
     appliedBacktrack     stateA stateB F0
"

text‹Transition relation is obtained by applying transition rules
iteratively. It is defined using a reflexive-transitive closure.›
definition
"transitionRelation F0 decisionVars == ({(stateA, stateB). transition stateA stateB F0 decisionVars})^*"

text‹Final state is one in which no rules apply›
definition
isFinalState :: "State ⇒ Formula ⇒ Variable set ⇒ bool"
where
"isFinalState state F0 decisionVars == ¬ (∃ state'. transition state state' F0 decisionVars)"

text‹The following several lemmas give conditions for applicability of different rules.›
lemma applicableDecideCharacterization:
  fixes stateA::State
  shows "applicableDecide stateA decisionVars = 
  (∃ l. 
        (var l) ∈ decisionVars ∧ 
        ¬ l el (elements (getM stateA)) ∧ 
        ¬ opposite l el (elements (getM stateA))) 
  " (is "?lhs = ?rhs")
proof
  assume ?rhs
  then obtain l where 
    *: "(var l) ∈ decisionVars" "¬ l el (elements (getM stateA))" "¬ opposite l el (elements (getM stateA))"
    unfolding applicableDecide_def
    by auto
  let ?stateB = "stateA⦇ getM := (getM stateA) @ [(l, True)] ⦈"
  from * have "appliedDecide stateA ?stateB decisionVars"
    unfolding appliedDecide_def
    by auto
  thus ?lhs
    unfolding applicableDecide_def
    by auto
next
  assume ?lhs
  then obtain stateB l
    where "(var l) ∈ decisionVars" "¬ l el (elements (getM stateA))"
    "¬ opposite l el (elements (getM stateA))"
    unfolding applicableDecide_def
    unfolding appliedDecide_def
    by auto
  thus ?rhs
    by auto
qed

lemma applicableUnitPropagateCharacterization:
  fixes stateA::State and F0::Formula
  shows "applicableUnitPropagate stateA F0 = 
  (∃ (uc::Clause) (ul::Literal). 
       uc el F0 ∧ 
       isUnitClause uc ul (elements (getM stateA)))
  " (is "?lhs = ?rhs")
proof
  assume "?rhs"
  then obtain ul uc 
    where *: "uc el F0" "isUnitClause uc ul (elements (getM stateA))"
    unfolding applicableUnitPropagate_def
    by auto
  let ?stateB = "stateA⦇ getM := getM stateA @ [(ul, False)] ⦈"
  from * have "appliedUnitPropagate stateA ?stateB F0" 
    unfolding appliedUnitPropagate_def
    by auto
  thus ?lhs
    unfolding applicableUnitPropagate_def
    by auto
next
  assume ?lhs
  then obtain stateB uc ul
    where "uc el F0" "isUnitClause uc ul (elements (getM stateA))"
    unfolding applicableUnitPropagate_def
    unfolding appliedUnitPropagate_def
    by auto
  thus ?rhs
    by auto
qed

lemma applicableBacktrackCharacterization:
  fixes stateA::State
  shows "applicableBacktrack stateA F0 = 
      (formulaFalse F0 (elements (getM stateA)) ∧ 
       decisions (getM stateA) ≠ [])" (is "?lhs = ?rhs")
proof
  assume ?rhs
  hence *: "formulaFalse F0 (elements (getM stateA))" "decisions (getM stateA) ≠ []"
    by auto
  let ?stateB = "stateA⦇ getM := prefixBeforeLastDecision (getM stateA) @ [(opposite (lastDecision (getM stateA)), False)]⦈"
  from * have "appliedBacktrack stateA ?stateB F0"
    unfolding appliedBacktrack_def
    by auto
  thus ?lhs
    unfolding applicableBacktrack_def
    by auto
next
  assume "?lhs"
  then obtain stateB 
    where "appliedBacktrack stateA stateB F0"
    unfolding applicableBacktrack_def
    by auto
  hence 
    "formulaFalse F0 (elements (getM stateA))"
    "decisions (getM stateA) ≠ []"
    "getM stateB = prefixBeforeLastDecision (getM stateA) @ [(opposite (lastDecision (getM stateA)), False)]"
    unfolding appliedBacktrack_def
    by auto
  thus ?rhs
    by auto
qed

text‹Final states are the ones where no rule is applicable.›
lemma finalStateNonApplicable: 
  fixes state::State
  shows "isFinalState state F0 decisionVars = 
          (¬ applicableDecide state decisionVars ∧ 
           ¬ applicableUnitPropagate state F0 ∧ 
           ¬ applicableBacktrack state F0)"
unfolding isFinalState_def
unfolding transition_def
unfolding applicableDecide_def
unfolding applicableUnitPropagate_def
unfolding applicableBacktrack_def
by auto
  
(******************************************************************************)
subsection‹Invariants›
(******************************************************************************)
text‹Invariants that are relevant for the rest of correctness proof.›
definition
invariantsHoldInState :: "State ⇒ Formula ⇒ Variable set ⇒ bool"
where
"invariantsHoldInState state F0 decisionVars == 
    InvariantImpliedLiterals F0 (getM state) ∧
    InvariantVarsM (getM state) F0 decisionVars ∧
    InvariantConsistent (getM state) ∧
    InvariantUniq (getM state)
"

text‹Invariants hold in initial states.›
lemma invariantsHoldInInitialState:
  fixes state :: State and F0 :: Formula
  assumes "isInitialState state F0" 
  shows "invariantsHoldInState state F0 decisionVars"
using assms
by (auto simp add:
  isInitialState_def 
  invariantsHoldInState_def 
  InvariantImpliedLiterals_def 
  InvariantVarsM_def
  InvariantConsistent_def
  InvariantUniq_def
)

text‹Valid transitions preserve invariants.›
lemma transitionsPreserveInvariants: 
  fixes stateA::State and stateB::State
  assumes "transition stateA stateB F0 decisionVars" and 
  "invariantsHoldInState stateA F0 decisionVars"
  shows "invariantsHoldInState stateB F0 decisionVars"
proof-
    from ‹invariantsHoldInState stateA F0 decisionVars›
    have 
      "InvariantImpliedLiterals F0 (getM stateA)" and 
      "InvariantVarsM (getM stateA) F0 decisionVars" and
      "InvariantConsistent (getM stateA)" and
      "InvariantUniq (getM stateA)"
      unfolding invariantsHoldInState_def
      by auto
  {
    assume "appliedDecide stateA stateB decisionVars"
    then obtain l::Literal where
      "(var l) ∈ decisionVars"
      "¬ literalTrue l (elements (getM stateA))"
      "¬ literalFalse l (elements (getM stateA))"
      "getM stateB = getM stateA @ [(l, True)]"
      unfolding appliedDecide_def
      by auto

    from ‹¬ literalTrue l (elements (getM stateA))› ‹¬ literalFalse l (elements (getM stateA))› 
    have *: "var l ∉ vars (elements (getM stateA))"
      using variableDefinedImpliesLiteralDefined[of "l" "elements (getM stateA)"]
      by simp

    have "InvariantImpliedLiterals F0 (getM stateB)"
      using 
        ‹getM stateB = getM stateA @ [(l, True)]› 
        ‹InvariantImpliedLiterals F0 (getM stateA)›
        ‹InvariantUniq (getM stateA)›
        ‹var l ∉ vars (elements (getM stateA))›
        InvariantImpliedLiteralsAfterDecide[of "F0" "getM stateA" "l" "getM stateB"]
      by simp
    moreover
    have "InvariantVarsM (getM stateB) F0 decisionVars"
      using ‹getM stateB = getM stateA @ [(l, True)]› 
        ‹InvariantVarsM (getM stateA) F0 decisionVars›
        ‹var l ∈ decisionVars›
        InvariantVarsMAfterDecide[of "getM stateA" "F0" "decisionVars" "l" "getM stateB"]
      by simp
    moreover 
    have "InvariantConsistent (getM stateB)"
      using ‹getM stateB = getM stateA @ [(l, True)]› 
        ‹InvariantConsistent (getM stateA)›
        ‹var l ∉ vars (elements (getM stateA))›
        InvariantConsistentAfterDecide[of "getM stateA" "l" "getM stateB"]
      by simp
    moreover
    have "InvariantUniq (getM stateB)"
      using ‹getM stateB = getM stateA @ [(l, True)]› 
        ‹InvariantUniq (getM stateA)›
        ‹var l ∉ vars (elements (getM stateA))›
        InvariantUniqAfterDecide[of "getM stateA" "l" "getM stateB"]
      by simp
    ultimately
    have ?thesis
      unfolding invariantsHoldInState_def
      by auto
  }
  moreover
  {
    assume "appliedUnitPropagate stateA stateB F0"
    then obtain uc::Clause and ul::Literal where 
      "uc el F0"
      "isUnitClause uc ul (elements (getM stateA))"
      "getM stateB = getM stateA @ [(ul, False)]"
      unfolding appliedUnitPropagate_def
      by auto

    from ‹isUnitClause uc ul (elements (getM stateA))›
    have "ul el uc"
      unfolding isUnitClause_def
      by simp

    from ‹uc el F0›
    have "formulaEntailsClause F0 uc"
      by (simp add: formulaEntailsItsClauses)
    
    have "InvariantImpliedLiterals F0 (getM stateB)"
      using
        ‹InvariantImpliedLiterals F0 (getM stateA)› 
        ‹formulaEntailsClause F0 uc›
        ‹isUnitClause uc ul (elements (getM stateA))›
        ‹getM stateB = getM stateA @ [(ul, False)]›
        InvariantImpliedLiteralsAfterUnitPropagate[of "F0" "getM stateA" "uc" "ul" "getM stateB"]
      by simp
    moreover
    from ‹ul el uc› ‹uc el F0›
    have "ul el F0"
      by (auto simp add: literalElFormulaCharacterization)
    hence "var ul ∈ vars F0 ∪ decisionVars"
      using formulaContainsItsLiteralsVariable [of "ul" "F0"]
      by auto

    have "InvariantVarsM (getM stateB) F0 decisionVars"
      using ‹InvariantVarsM (getM stateA) F0 decisionVars›
        ‹var ul ∈ vars F0 ∪ decisionVars›
        ‹getM stateB = getM stateA @ [(ul, False)]›
        InvariantVarsMAfterUnitPropagate[of "getM stateA" "F0" "decisionVars" "ul" "getM stateB"]
      by simp
    moreover
    have "InvariantConsistent (getM stateB)"
      using ‹InvariantConsistent (getM stateA)›
        ‹isUnitClause uc ul (elements (getM stateA))›
        ‹getM stateB = getM stateA @ [(ul, False)]›
        InvariantConsistentAfterUnitPropagate [of "getM stateA" "uc" "ul" "getM stateB"]
      by simp
    moreover
    have "InvariantUniq (getM stateB)"
      using ‹InvariantUniq (getM stateA)›
        ‹isUnitClause uc ul (elements (getM stateA))›
        ‹getM stateB = getM stateA @ [(ul, False)]›
        InvariantUniqAfterUnitPropagate [of "getM stateA" "uc" "ul" "getM stateB"]
      by simp
    ultimately
    have ?thesis
      unfolding invariantsHoldInState_def
      by auto
  }
  moreover
  {
    assume "appliedBacktrack stateA stateB F0"
    hence "formulaFalse F0 (elements (getM stateA))" 
      "formulaFalse F0 (elements (getM stateA))"
      "decisions (getM stateA) ≠ []"
      "getM stateB = prefixBeforeLastDecision (getM stateA) @ [(opposite (lastDecision (getM stateA)), False)]"
      unfolding appliedBacktrack_def
      by auto      

    have "InvariantImpliedLiterals F0 (getM stateB)"
      using ‹InvariantImpliedLiterals F0 (getM stateA)›
        ‹formulaFalse F0 (elements (getM stateA))›
        ‹decisions (getM stateA) ≠ []›
        ‹getM stateB = prefixBeforeLastDecision (getM stateA) @ [(opposite (lastDecision (getM stateA)), False)]›
        ‹InvariantUniq (getM stateA)›
        ‹InvariantConsistent (getM stateA)›
        InvariantImpliedLiteralsAfterBacktrack[of "F0" "getM stateA" "getM stateB"]
      by simp
    moreover
    have "InvariantVarsM (getM stateB) F0 decisionVars"
      using ‹InvariantVarsM (getM stateA) F0 decisionVars›
        ‹decisions (getM stateA) ≠ []›
        ‹getM stateB = prefixBeforeLastDecision (getM stateA) @ [(opposite (lastDecision (getM stateA)), False)]›
        InvariantVarsMAfterBacktrack[of "getM stateA" "F0" "decisionVars" "getM stateB"]
      by simp
    moreover
    have "InvariantConsistent (getM stateB)"
      using ‹InvariantConsistent (getM stateA)›
        ‹InvariantUniq (getM stateA)›
        ‹decisions (getM stateA) ≠ []›
        ‹getM stateB = prefixBeforeLastDecision (getM stateA) @ [(opposite (lastDecision (getM stateA)), False)]›
        InvariantConsistentAfterBacktrack[of "getM stateA" "getM stateB"]
      by simp
    moreover
    have "InvariantUniq (getM stateB)"
      using ‹InvariantConsistent (getM stateA)›
        ‹InvariantUniq (getM stateA)›
        ‹decisions (getM stateA) ≠ []›
        ‹getM stateB = prefixBeforeLastDecision (getM stateA) @ [(opposite (lastDecision (getM stateA)), False)]›
        InvariantUniqAfterBacktrack[of "getM stateA" "getM stateB"]
      by simp
    ultimately
    have ?thesis
      unfolding invariantsHoldInState_def
      by auto
  }
  ultimately
  show ?thesis
    using ‹transition stateA stateB F0 decisionVars›
    unfolding transition_def
    by auto
qed

text‹The consequence is that invariants hold in all valid runs.›
lemma invariantsHoldInValidRuns: 
  fixes F0 :: Formula and decisionVars :: "Variable set"
  assumes "invariantsHoldInState stateA F0 decisionVars" and
  "(stateA, stateB) ∈ transitionRelation F0 decisionVars"
  shows "invariantsHoldInState stateB F0 decisionVars"
using assms
using transitionsPreserveInvariants
using rtrancl_induct[of "stateA" "stateB" 
  "{(stateA, stateB). transition stateA stateB F0 decisionVars}" "λ x. invariantsHoldInState x F0 decisionVars"]
unfolding transitionRelation_def
by auto

lemma invariantsHoldInValidRunsFromInitialState:
  fixes F0 :: Formula and decisionVars :: "Variable set"
  assumes "isInitialState state0 F0" 
  and "(state0, state) ∈ transitionRelation F0 decisionVars"
  shows "invariantsHoldInState state F0 decisionVars"
proof-
  from ‹isInitialState state0 F0›
  have "invariantsHoldInState state0 F0 decisionVars"
    by (simp add:invariantsHoldInInitialState)
  with assms
  show ?thesis
    using invariantsHoldInValidRuns [of "state0"  "F0" "decisionVars" "state"]
    by simp
qed

text‹
 In the following text we will show that there are two kinds of states:
 \begin{enumerate}
  \item \textit{UNSAT} states where @{term "formulaFalse F0 (elements (getM state))"}
  and @{term "decisions (getM state) = []"}. 
  \item \textit{SAT} states where @{term "¬ formulaFalse F0 (elements (getM state))"}
  and @{term "vars (elements (getM state)) ⊇ decisionVars"}.
 \end{enumerate}
  
 The soundness theorems claim that if \textit{UNSAT} state is reached
 the formula is unsatisfiable and if \textit{SAT} state is reached,
 the formula is satisfiable.

 Completeness theorems claim that every final state is either
 \textit{UNSAT} or \textit{SAT}. A consequence of this and soundness
 theorems, is that if formula is unsatisfiable the solver will finish
 in an \textit{UNSAT} state, and if the formula is satisfiable the
 solver will finish in a \textit{SAT} state.›


(******************************************************************************)
subsection‹Soundness›
(******************************************************************************)

(*----------------------------------------------------------------------------*)
theorem soundnessForUNSAT:
  fixes F0 :: Formula and decisionVars :: "Variable set" and state0 :: State and state :: State
  assumes
  "isInitialState state0 F0" and
  "(state0, state) ∈ transitionRelation F0 decisionVars"

  "formulaFalse F0 (elements (getM state))"
  "decisions (getM state) = []"
  shows "¬ satisfiable F0"
(*----------------------------------------------------------------------------*)
proof-
  from ‹isInitialState state0 F0› ‹(state0, state) ∈ transitionRelation F0 decisionVars›
  have "invariantsHoldInState state F0 decisionVars" 
    using invariantsHoldInValidRunsFromInitialState
    by simp
  hence "InvariantImpliedLiterals F0 (getM state)"
    unfolding invariantsHoldInState_def
    by auto
  with ‹formulaFalse F0 (elements (getM state))›
    ‹decisions (getM state) = []›
  show ?thesis
    using unsatReport[of "F0" "getM state" "F0"]
    unfolding InvariantEquivalent_def equivalentFormulae_def
    by simp
qed

(*----------------------------------------------------------------------------*)
theorem soundnessForSAT:
  fixes F0 :: Formula and decisionVars :: "Variable set" and state0 :: State and state :: State
  assumes
  "vars F0 ⊆ decisionVars" and

  "isInitialState state0 F0" and
  "(state0, state) ∈ transitionRelation F0 decisionVars"

  "¬ formulaFalse F0 (elements (getM state))"
  "vars (elements (getM state)) ⊇ decisionVars"  

  shows 
  "model (elements (getM state)) F0"
(*----------------------------------------------------------------------------*)
proof-
  from ‹isInitialState state0 F0› ‹(state0, state) ∈ transitionRelation F0 decisionVars›
  have "invariantsHoldInState state F0 decisionVars" 
    using invariantsHoldInValidRunsFromInitialState
    by simp
  hence 
    "InvariantConsistent (getM state)" 
    unfolding invariantsHoldInState_def
    by auto
  with assms
  show ?thesis
  using satReport[of "F0" "decisionVars" "F0" "getM state"]
  unfolding InvariantEquivalent_def equivalentFormulae_def
  InvariantVarsF_def
  by auto
qed


(******************************************************************************)
subsection‹Termination›
(******************************************************************************)
text‹We now define a termination ordering on the set of states based
on the @{term lexLessRestricted} trail ordering. This ordering will be central
in termination proof.›

definition "terminationLess (F0::Formula) decisionVars == {((stateA::State), (stateB::State)).
  (getM stateA, getM stateB) ∈ lexLessRestricted (vars F0 ∪ decisionVars)}"


text‹We want to show that every valid transition decreases a state
  with respect to the constructed termination ordering. Therefore, we
  show that $Decide$, $UnitPropagate$ and $Backtrack$ rule decrease the
  trail with respect to the restricted trail ordering. Invariants
  ensure that trails are indeed @{term uniq}, @{term consistent} and with 
  finite variable sets.›
lemma trailIsDecreasedByDeciedUnitPropagateAndBacktrack:
  fixes stateA::State and stateB::State
  assumes "invariantsHoldInState stateA F0 decisionVars" and
  "appliedDecide stateA stateB decisionVars ∨ appliedUnitPropagate stateA stateB F0 ∨ appliedBacktrack stateA stateB F0"
  shows "(getM stateB, getM stateA) ∈ lexLessRestricted (vars F0 ∪ decisionVars)"
proof-
  from ‹appliedDecide stateA stateB decisionVars ∨ appliedUnitPropagate stateA stateB F0 ∨ appliedBacktrack stateA stateB F0›
    ‹invariantsHoldInState stateA F0 decisionVars› 
  have "invariantsHoldInState stateB F0 decisionVars"
      using transitionsPreserveInvariants
      unfolding transition_def
      by auto
    from ‹invariantsHoldInState stateA F0 decisionVars› 
    have *: "uniq (elements (getM stateA))" "consistent (elements (getM stateA))" "vars (elements (getM stateA)) ⊆ vars F0 ∪ decisionVars"
      unfolding invariantsHoldInState_def
      unfolding InvariantVarsM_def
      unfolding InvariantConsistent_def
      unfolding InvariantUniq_def
      by auto
    from ‹invariantsHoldInState stateB F0 decisionVars› 
    have **: "uniq (elements (getM stateB))" "consistent (elements (getM stateB))" "vars (elements (getM stateB)) ⊆ vars F0 ∪ decisionVars"
      unfolding invariantsHoldInState_def
      unfolding InvariantVarsM_def
      unfolding InvariantConsistent_def
      unfolding InvariantUniq_def
      by auto
  {
    assume "appliedDecide stateA stateB decisionVars"
    hence "(getM stateB, getM stateA) ∈ lexLess"
      unfolding appliedDecide_def
      by (auto simp add:lexLessAppend)
    with * ** 
    have "((getM stateB), (getM stateA)) ∈ lexLessRestricted (vars F0 ∪ decisionVars)"
      unfolding lexLessRestricted_def
      by auto
  }
  moreover
  {
    assume "appliedUnitPropagate stateA stateB F0"
    hence "(getM stateB, getM stateA) ∈ lexLess"
      unfolding appliedUnitPropagate_def
      by (auto simp add:lexLessAppend)
    with * ** 
    have "(getM stateB, getM stateA) ∈ lexLessRestricted (vars F0 ∪ decisionVars)"
      unfolding lexLessRestricted_def
      by auto
  }
  moreover
  {
    assume "appliedBacktrack stateA stateB F0"
    hence
      "formulaFalse F0 (elements (getM stateA))"
      "decisions (getM stateA) ≠ []"
      "getM stateB = prefixBeforeLastDecision (getM stateA) @ [(opposite (lastDecision (getM stateA)), False)]"
      unfolding appliedBacktrack_def
      by auto
    hence "(getM stateB, getM stateA) ∈ lexLess"
      using ‹decisions (getM stateA) ≠ []›
        ‹getM stateB = prefixBeforeLastDecision (getM stateA) @ [(opposite (lastDecision (getM stateA)), False)]›
      by (simp add:lexLessBacktrack)
    with * ** 
    have "(getM stateB, getM stateA) ∈ lexLessRestricted (vars F0 ∪ decisionVars)"
      unfolding lexLessRestricted_def
      by auto
  }
  ultimately
  show ?thesis
    using assms
    by auto
qed

text‹Now we can show that every rule application decreases a state
with respect to the constructed termination ordering.›
lemma stateIsDecreasedByValidTransitions:
  fixes stateA::State and stateB::State 
  assumes "invariantsHoldInState stateA F0 decisionVars" and "transition stateA stateB F0 decisionVars"
  shows "(stateB, stateA) ∈ terminationLess F0 decisionVars"
proof-
  from ‹transition stateA stateB F0 decisionVars›
  have "appliedDecide stateA stateB decisionVars ∨ appliedUnitPropagate stateA stateB F0 ∨ appliedBacktrack stateA stateB F0"
    unfolding transition_def
    by simp 
  with ‹invariantsHoldInState stateA F0 decisionVars›
  have "(getM stateB, getM stateA) ∈ lexLessRestricted (vars F0 ∪ decisionVars)"
    using trailIsDecreasedByDeciedUnitPropagateAndBacktrack
    by simp
  thus ?thesis 
    unfolding terminationLess_def
    by simp
qed

text‹The minimal states with respect to the termination ordering are
  final i.e., no further transition rules are applicable.›
definition 
"isMinimalState stateMin F0 decisionVars == (∀ state::State. (state, stateMin) ∉ terminationLess F0 decisionVars)"

lemma minimalStatesAreFinal:
  fixes stateA::State
  assumes "invariantsHoldInState state F0 decisionVars" and "isMinimalState state F0 decisionVars"
  shows "isFinalState state F0 decisionVars"
proof-
  {
    assume "¬ ?thesis"
    then obtain state'::State 
      where "transition state state' F0 decisionVars"
      unfolding isFinalState_def
      by auto
    with ‹invariantsHoldInState state F0 decisionVars› 
    have "(state', state) ∈ terminationLess F0 decisionVars"
      using stateIsDecreasedByValidTransitions[of "state" "F0" "decisionVars" "state'"]
      unfolding transition_def
      by auto
    with ‹isMinimalState state F0 decisionVars› 
    have False
      unfolding isMinimalState_def
      by auto
  }
  thus ?thesis
    by auto
qed

text‹The following key lemma shows that the termination ordering is well founded.›
lemma wfTerminationLess: 
  fixes decisionVars :: "Variable set" and F0 :: "Formula"
  assumes "finite decisionVars"
  shows "wf (terminationLess F0 decisionVars)"
unfolding wf_eq_minimal
proof-
  show "∀Q state. state ∈ Q ⟶ (∃stateMin∈Q. ∀state'. (state', stateMin) ∈ terminationLess F0 decisionVars ⟶ state' ∉ Q)"
  proof-
    {
      fix Q :: "State set" and state :: State
      assume "state ∈ Q"
      let ?Q1 = "{M::LiteralTrail. ∃ state. state ∈ Q ∧ (getM state) = M}"
      from ‹state ∈ Q›
      have "getM state ∈ ?Q1"
        by auto
      from ‹finite decisionVars› 
      have "finite (vars F0 ∪ decisionVars)"
        using finiteVarsFormula[of "F0"]
        by simp
      hence "wf (lexLessRestricted (vars F0 ∪ decisionVars))"
      using  wfLexLessRestricted[of "vars F0 ∪ decisionVars"]
      by simp
    with ‹getM state ∈ ?Q1›
      obtain Mmin where "Mmin ∈ ?Q1" "∀M'. (M', Mmin) ∈ lexLessRestricted (vars F0 ∪ decisionVars) ⟶ M' ∉ ?Q1"
        unfolding wf_eq_minimal
        apply (erule_tac x="?Q1" in allE)
        apply (erule_tac x="getM state" in allE)
        by auto 
      from ‹Mmin ∈ ?Q1› obtain stateMin
        where "stateMin ∈ Q" "(getM stateMin) = Mmin"
        by auto
      have "∀state'. (state', stateMin) ∈ terminationLess F0 decisionVars ⟶ state' ∉ Q"
      proof
        fix state'
        show "(state', stateMin) ∈ terminationLess F0 decisionVars ⟶ state' ∉ Q"
        proof
          assume "(state', stateMin) ∈ terminationLess F0 decisionVars"
          hence "(getM state', getM stateMin) ∈ lexLessRestricted (vars F0 ∪ decisionVars)"
            unfolding terminationLess_def
            by auto
          from ‹∀M'. (M', Mmin) ∈ lexLessRestricted (vars F0 ∪ decisionVars) ⟶ M' ∉ ?Q1›
            ‹(getM state', getM stateMin) ∈ lexLessRestricted (vars F0 ∪ decisionVars)› ‹getM stateMin = Mmin›
          have "getM state' ∉ ?Q1"
            by simp
          with ‹getM stateMin = Mmin›
          show "state' ∉ Q"
            by auto
        qed
      qed
      with ‹stateMin ∈ Q›
      have "∃ stateMin ∈ Q. (∀state'. (state', stateMin) ∈ terminationLess F0 decisionVars ⟶ state' ∉ Q)"
        by auto
    }
    thus ?thesis
      by auto
  qed
qed

text‹Using the termination ordering we show that the transition
relation is well founded on states reachable from initial state.›
(*----------------------------------------------------------------------------*)
theorem wfTransitionRelation:
  fixes decisionVars :: "Variable set" and F0 :: "Formula" and state0 :: "State"
  assumes "finite decisionVars" and "isInitialState state0 F0"
  shows "wf {(stateB, stateA). 
             (state0, stateA) ∈ transitionRelation F0 decisionVars ∧ (transition stateA stateB F0 decisionVars)}"
(*----------------------------------------------------------------------------*)
proof-
  let ?rel = "{(stateB, stateA). 
                  (state0, stateA) ∈ transitionRelation F0 decisionVars ∧ (transition stateA stateB F0 decisionVars)}"
  let ?rel'= "terminationLess F0 decisionVars"

  have "∀x y. (x, y) ∈ ?rel ⟶ (x, y) ∈ ?rel'"
  proof-
    {
      fix stateA::State and stateB::State
      assume "(stateB, stateA) ∈ ?rel"
      hence "(stateB, stateA) ∈ ?rel'"
        using ‹isInitialState state0 F0›
        using invariantsHoldInValidRunsFromInitialState[of "state0" "F0" "stateA" "decisionVars"]
        using stateIsDecreasedByValidTransitions[of "stateA" "F0" "decisionVars" "stateB"]
        by simp
    }
    thus ?thesis
      by simp
  qed
  moreover 
  have "wf ?rel'"
    using ‹finite decisionVars›
    by (rule wfTerminationLess)
  ultimately
  show ?thesis
    using wellFoundedEmbed[of "?rel" "?rel'"]
    by simp
qed



text‹We will now give two corollaries of the previous theorem. First
  is a weak termination result that shows that there is a terminating
  run from every intial state to the final one.›
corollary
  fixes decisionVars :: "Variable set" and F0 :: "Formula" and state0 :: "State"
  assumes "finite decisionVars" and "isInitialState state0 F0"
  shows "∃ state. (state0, state) ∈ transitionRelation F0 decisionVars ∧ isFinalState state F0 decisionVars"
proof-
  {
    assume "¬ ?thesis"
    let ?Q = "{state. (state0, state) ∈ transitionRelation F0 decisionVars}"
    let ?rel = "{(stateB, stateA). (state0, stateA) ∈ transitionRelation F0 decisionVars ∧
                         transition stateA stateB F0 decisionVars}"
    have "state0 ∈ ?Q"
      unfolding transitionRelation_def
      by simp
    hence "∃ state. state ∈ ?Q"
      by auto

    from assms 
    have "wf ?rel"
      using wfTransitionRelation[of "decisionVars" "state0" "F0"]
      by auto
    hence "∀ Q. (∃ x. x ∈ Q) ⟶ (∃ stateMin ∈ Q. ∀ state. (state, stateMin) ∈ ?rel ⟶ state ∉ Q)"
      unfolding wf_eq_minimal
      by simp
    hence " (∃ x. x ∈ ?Q) ⟶ (∃ stateMin ∈ ?Q. ∀ state. (state, stateMin) ∈ ?rel ⟶ state ∉ ?Q)"
      by rule
    with ‹∃ state. state ∈ ?Q›
    have "∃ stateMin ∈ ?Q. ∀ state. (state, stateMin) ∈ ?rel ⟶ state ∉ ?Q"
      by simp
    then obtain stateMin
      where "stateMin ∈ ?Q" and "∀ state. (state, stateMin) ∈ ?rel ⟶ state ∉ ?Q"
      by auto
    
    from ‹stateMin ∈ ?Q› 
    have "(state0, stateMin) ∈ transitionRelation F0 decisionVars"
      by simp
    with ‹¬ ?thesis›
    have "¬ isFinalState stateMin F0 decisionVars"
      by simp
    then obtain state'::State
      where "transition stateMin state' F0 decisionVars"
      unfolding isFinalState_def
      by auto
    have "(state', stateMin) ∈ ?rel"
      using ‹(state0, stateMin) ∈ transitionRelation F0 decisionVars›
            ‹transition stateMin state' F0 decisionVars›
      by simp
    with ‹∀ state. (state, stateMin) ∈ ?rel ⟶ state ∉ ?Q›
    have "state' ∉ ?Q"
      by force
    moreover
    from ‹(state0, stateMin) ∈ transitionRelation F0 decisionVars› ‹transition stateMin state' F0 decisionVars›
    have "state' ∈ ?Q"
      unfolding transitionRelation_def
      using rtrancl_into_rtrancl[of "state0" "stateMin" "{(stateA, stateB). transition stateA stateB F0 decisionVars}" "state'"]
      by simp
    ultimately
    have False
      by simp
  }
  thus ?thesis
    by auto
qed

text‹Now we prove the final strong termination result which states
that there cannot be infinite chains of transitions. If there is an
infinite transition chain that starts from an initial state, its
elements would for a set that would contain initial state and for
every element of that set there would be another element of that set
that is directly reachable from it. We show that no such set exists.›
corollary noInfiniteTransitionChains:
  fixes F0::Formula and decisionVars::"Variable set"
  assumes "finite decisionVars"
  shows "¬ (∃ Q::(State set). ∃ state0 ∈ Q. isInitialState state0 F0 ∧ 
                              (∀ state ∈ Q. (∃ state' ∈ Q. transition state state' F0 decisionVars))
            )"
proof-
  {
  assume "¬ ?thesis"
  then obtain Q::"State set" and state0::"State"
    where "isInitialState state0 F0" "state0 ∈ Q"
          "∀ state ∈ Q. (∃ state' ∈ Q. transition state state' F0 decisionVars)"
    by auto
  let ?rel = "{(stateB, stateA). (state0, stateA) ∈ transitionRelation F0 decisionVars ∧
                         transition stateA stateB F0 decisionVars}"
  from ‹finite decisionVars› ‹isInitialState state0 F0›
  have "wf ?rel"
    using wfTransitionRelation
    by simp
  hence wfmin: "∀Q x. x ∈ Q ⟶
         (∃z∈Q. ∀y. (y, z) ∈ ?rel ⟶ y ∉ Q)"
    unfolding wf_eq_minimal 
    by simp
  let ?Q = "{state ∈ Q. (state0, state) ∈ transitionRelation F0 decisionVars}"
  from ‹state0 ∈ Q›
  have "state0 ∈ ?Q"
    unfolding transitionRelation_def
    by simp
  with wfmin
  obtain stateMin::State
    where "stateMin ∈ ?Q" and "∀y. (y, stateMin) ∈ ?rel ⟶ y ∉ ?Q"
    apply (erule_tac x="?Q" in allE)
    by auto

  from ‹stateMin ∈ ?Q›
  have "stateMin ∈ Q" "(state0, stateMin) ∈ transitionRelation F0 decisionVars"
    by auto
  with ‹∀ state ∈ Q. (∃ state' ∈ Q. transition state state' F0 decisionVars)›
  obtain state'::State
    where "state' ∈ Q" "transition stateMin state' F0 decisionVars"
    by auto

  with ‹(state0, stateMin) ∈ transitionRelation F0 decisionVars›
  have "(state', stateMin) ∈ ?rel"
    by simp
  with ‹∀y. (y, stateMin) ∈ ?rel ⟶ y ∉ ?Q›
  have "state' ∉ ?Q"
    by force
  
  from ‹state' ∈ Q› ‹(state0, stateMin) ∈ transitionRelation F0 decisionVars›
    ‹transition stateMin state' F0 decisionVars›
  have "state' ∈ ?Q"
    unfolding transitionRelation_def
    using rtrancl_into_rtrancl[of "state0" "stateMin" "{(stateA, stateB). transition stateA stateB F0 decisionVars}" "state'"]
    by simp
  with ‹state' ∉ ?Q›
  have False
    by simp
  }
  thus ?thesis
    by force
qed

(******************************************************************************)
subsection‹Completeness›
(******************************************************************************)
text‹In this section we will first show that each final state is
either \textit{SAT} or \textit{UNSAT} state.›

lemma finalNonConflictState: 
  fixes state::State and FO :: Formula
  assumes 
  "¬ applicableDecide state decisionVars"
  shows "vars (elements (getM state)) ⊇ decisionVars"
proof
  fix x :: Variable
  let ?l = "Pos x"
  assume "x ∈ decisionVars"
  hence "var ?l = x" and "var ?l ∈ decisionVars" and "var (opposite ?l) ∈ decisionVars"
    by auto
  with ‹¬ applicableDecide state decisionVars› 
  have "literalTrue ?l (elements (getM state)) ∨ literalFalse ?l (elements (getM state))"
    unfolding applicableDecideCharacterization
    by force
  with ‹var ?l = x›
  show "x ∈ vars (elements (getM state))"
    using valuationContainsItsLiteralsVariable[of "?l" "elements (getM state)"]
    using valuationContainsItsLiteralsVariable[of "opposite ?l" "elements (getM state)"]
    by auto
qed


lemma finalConflictingState: 
  fixes state :: State
  assumes 
  "¬ applicableBacktrack state F0" and
  "formulaFalse F0 (elements (getM state))"  
  shows
  "decisions (getM state) = []"
using assms
using applicableBacktrackCharacterization
by auto

lemma finalStateCharacterizationLemma:
  fixes state :: State
  assumes 
  "¬ applicableDecide state decisionVars"  and
  "¬ applicableBacktrack state F0"
  shows
  "(¬ formulaFalse F0 (elements (getM state)) ∧ vars (elements (getM state)) ⊇ decisionVars) ∨ 
   (formulaFalse F0 (elements (getM state)) ∧ decisions (getM state) = [])"
proof (cases "formulaFalse F0 (elements (getM state))")
  case True
  hence "decisions (getM state) = []"
    using assms
    using finalConflictingState
    by auto
  with True 
  show ?thesis
    by simp
next
  case False
  hence  "vars (elements (getM state)) ⊇ decisionVars"
    using assms
    using finalNonConflictState
    by auto
  with False
  show ?thesis
    by simp
qed


(*----------------------------------------------------------------------------*)
theorem finalStateCharacterization:
  fixes F0 :: Formula and decisionVars :: "Variable set" and state0 :: State and state :: State
  assumes 
  "isInitialState state0 F0" and
  "(state0, state) ∈ transitionRelation F0 decisionVars" and
  "isFinalState state F0 decisionVars"
  shows 
  "(¬ formulaFalse F0 (elements (getM state)) ∧ vars (elements (getM state)) ⊇ decisionVars) ∨ 
   (formulaFalse F0 (elements (getM state)) ∧ decisions (getM state) = [])"
(*----------------------------------------------------------------------------*)
proof-
  from ‹isFinalState state F0 decisionVars› 
  have **: 
    "¬ applicableBacktrack state F0"
    "¬ applicableDecide state decisionVars"
    unfolding finalStateNonApplicable
    by auto

  thus ?thesis
    using finalStateCharacterizationLemma[of "state" "decisionVars"]
    by simp
qed

text‹Completeness theorems are easy consequences of this characterization and 
 soundness.›
(*----------------------------------------------------------------------------*)
theorem completenessForSAT: 
  fixes F0 :: Formula and decisionVars :: "Variable set" and state0 :: State and state :: State
  assumes 
  "satisfiable F0" and

  "isInitialState state0 F0" and
  "(state0, state) ∈ transitionRelation F0 decisionVars" and
  "isFinalState state F0 decisionVars"

  shows "¬ formulaFalse F0 (elements (getM state)) ∧ vars (elements (getM state)) ⊇ decisionVars"
(*----------------------------------------------------------------------------*)
proof-
  from assms
  have *: "(¬ formulaFalse F0 (elements (getM state)) ∧ vars (elements (getM state)) ⊇ decisionVars) ∨ 
    (formulaFalse F0 (elements (getM state)) ∧ decisions (getM state) = [])"
    using finalStateCharacterization[of "state0" "F0" "state" "decisionVars"]
    by auto
  {
    assume "formulaFalse F0 (elements (getM state))"
    with * 
    have "formulaFalse F0 (elements (getM state))" "decisions (getM state) = []"
      by auto
    with assms
      have "¬ satisfiable F0"
      using soundnessForUNSAT
      by simp
    with ‹satisfiable F0›
    have False
      by simp
  }
  with * show ?thesis
    by auto
qed

(*----------------------------------------------------------------------------*)
theorem completenessForUNSAT: 
  fixes F0 :: Formula and decisionVars :: "Variable set" and state0 :: State and state :: State
  assumes 
  "vars F0 ⊆ decisionVars" and
  "¬ satisfiable F0" and

  "isInitialState state0 F0" and
  "(state0, state) ∈ transitionRelation F0 decisionVars" and
  "isFinalState state F0 decisionVars"

  shows 
  "formulaFalse F0 (elements (getM state)) ∧ decisions (getM state) = []"
(*----------------------------------------------------------------------------*)
proof-
  from assms
  have *: 
  "(¬ formulaFalse F0 (elements (getM state)) ∧ vars (elements (getM state)) ⊇ decisionVars) ∨ 
   (formulaFalse F0 (elements (getM state))  ∧ decisions (getM state) = [])"
    using finalStateCharacterization[of "state0" "F0" "state" "decisionVars"]
    by auto
  {
    assume "¬ formulaFalse F0 (elements (getM state))"
    with *
    have "¬ formulaFalse F0 (elements (getM state))" "vars (elements (getM state)) ⊇ decisionVars"
      by auto
    with assms
    have "satisfiable F0"
      using soundnessForSAT[of "F0" "decisionVars" "state0" "state"]
      unfolding satisfiable_def
      by auto
    with ‹¬ satisfiable F0›
    have False
      by simp
  }
  with * show ?thesis
    by auto
qed

(*----------------------------------------------------------------------------*)
theorem partialCorrectness: 
  fixes F0 :: Formula and decisionVars :: "Variable set" and state0 :: State and state :: State
  assumes 
  "vars F0 ⊆ decisionVars" and  

  "isInitialState state0 F0" and
  "(state0, state) ∈ transitionRelation F0 decisionVars" and
  "isFinalState state F0 decisionVars"

  shows 
  "satisfiable F0 = (¬ formulaFalse F0 (elements (getM state)))"
(*----------------------------------------------------------------------------*)
using assms
using completenessForUNSAT[of "F0" "decisionVars" "state0" "state"]
using completenessForSAT[of "F0" "state0" "state" "decisionVars"]
by auto

end