Theory Relaxed_Assignment

section ‹Relaxed Partial Assignments›
theory Relaxed_Assignment
imports Unit_Propagation
begin
  (* TODO: Move *)      
  lemma sat_add_taut[simp]: "is_syn_taut C ⟹ sat (insert C F) = sat F"
    by (simp add: sat_def)  
    
  lemma sat_antimono: "F⊆F' ⟹ sat F' ⟹ sat F"
    unfolding sat_def sem_cnf_def by auto  
        
  
    
  subsection ‹Abstract Ideas of LRUP (for paper)›
  text ‹These theorems back the description of the abstract idea behind LRUP in the paper›

  definition neg_clause :: "'a clause ⇒ 'a cnf" where
    "neg_clause C ≡ { {neg_lit l} | l. l∈C }"

  lemma sem_neg_clause[simp]: "sem_cnf (neg_clause C) A ⟷ ¬sem_clause C A"  
    unfolding neg_clause_def sem_cnf_def sem_clause_def 
    apply (safe; simp)
    using sem_neg_lit by blast
    
  text ‹Equisatisfiability when inserting clause can be checked by showing that formula and negated clause is unsatisfiable. ›
  theorem pres_sat_by_conj_negated: "(¬sat (F ∪ neg_clause C)) ⟹ (sat F ⟷ sat (insert C F))"
    by (auto simp: sat_def)

  text ‹Abstract idea of unit propagation›  
  theorem abs_unit_propagation:
    assumes "{l}∈F"  
    shows "sat F ⟷ sat ({ C - {neg_lit l} | C. C∈F ∧ l ∉ C })"
  proof -
    from assms obtain F' where [simp]: "F = insert {l} F'" by blast
  
    have [simp]: "set_lit (insert {l} F') l = set_lit F' l"
      unfolding set_lit_def by blast
    
    have [simp]: "sem_lit l (σ(var_of_lit l := is_pos l))" for σ
      by (cases l; simp)
      
    have "sat F ⟷ sat (set_lit F l)"
      unfolding sat_def
      apply (safe; clarsimp)
      subgoal for σ
        apply (rule exI[where x=σ])
        unfolding sem_cnf_def sem_clause_def set_lit_def
        by fastforce
      subgoal for σ
        apply (rule exI[where x="σ(var_of_lit l := is_pos l)"])
        apply (simp add: sem_cnf_set)
        done
      done
      
    thus ?thesis unfolding set_lit_def by auto
  qed  
    
      
  lemma sat'_and_not_C_conv: "¬is_syn_taut C ⟹ sat' F (and_not_C (λ_. None) C) ⟷ sat (F ∪ neg_clause C)"
    apply rule
    subgoal
      unfolding sat_iff_sat' is_syn_taut_conv sat'_def models'_def
      apply (clarsimp simp: sem_clause_def)
      using compat_lit sem_lit_and_not_C_conv by blast
    subgoal
      unfolding sat'_def models'_def sat_iff_sat'
      apply clarsimp
      using compat_and_not_C compat_assignment_empty by blast
    done
    
    
    
  text ‹May be inconsistent, i.e., assigning a literal to true and false at the same time.›

  subsection ‹Definitions›  
  type_synonym 'a rp_ass = "'a literal ⇒ bool"
  
  abbreviation (input) rpa_empty :: "'a rp_ass" where "rpa_empty ≡ λ_. False"
  
  
  definition is_true :: "'a rp_ass ⇒ 'a literal ⇒ bool" where "is_true A l ≡ A l"
  abbreviation "is_false A l ≡ is_true A (neg_lit l)"
  
  definition assign_lits :: "'a rp_ass ⇒ 'a literal set ⇒ 'a rp_ass" where
    "assign_lits A ls l ≡ if l∈ls then True else A l" 
    
  context 
    notes [simp] = assign_lits_def fun_eq_iff is_true_def
  begin  
    lemma assign_lits_empty[simp]: "assign_lits A {} = A" by auto
    lemma assign_lits_insert[simp]: "assign_lits A (insert l ls) = (assign_lits A ls)(l:=True)" by auto

    lemma assign_lits_union[simp]: "assign_lits A (ls⇩1 ∪ ls⇩2) = assign_lits (assign_lits A ls⇩2) ls⇩1" by auto
            
    lemma is_true_upd[simp]: "is_true (A(l:=True)) l' ⟷ l'=l ∨ is_true A l'" by auto
    
    lemma is_true_assign[simp]: "is_true (assign_lits A ls) l ⟷ l∈ls ∨ is_true A l" by auto
    
    lemma is_true_empty[simp]: "¬is_true rpa_empty l" by auto
    
  end  

  subsection ‹Refinement to Partial Assignment›        

  definition "rpa_consistent A ≡ ∀l. ¬(is_true A l ∧ is_false A l)"
  definition "rpa_α A ≡ λv. if is_true A (Pos v) then Some True else if is_false A (Pos v) then Some False else None"  
  
  (* For Paper *)
  lemma "rpa_consistent A ⟷ (∀l. ¬ (A l ∧ A (neg_lit l)))"
    unfolding rpa_consistent_def is_true_def
    by auto
  
    
  lemma rpa_empty_refine[simp]: 
    "rpa_consistent rpa_empty" 
    "rpa_α rpa_empty = Map.empty"
    unfolding rpa_consistent_def rpa_α_def by auto

  lemma rpa_is_true_refine[simp]: 
    assumes "rpa_consistent A" 
    shows "is_true A l ⟷ sem_lit' l (rpa_α A) = Some True"  
    using assms
    unfolding rpa_consistent_def rpa_α_def
    apply (cases l)
    by auto
    
  lemma rpa_set_α[simp]:
    assumes "rpa_consistent A"
    assumes "sem_lit' l (rpa_α A) ≠ Some False"
    shows
      "rpa_consistent (A(l := True))" 
      "rpa_α (A(l:=True)) = assign_lit (rpa_α A) l" 
    subgoal 
      using assms rpa_consistent_def by fastforce
    subgoal
      using assms 
      unfolding rpa_α_def
      by (cases l; auto 0 4) 
    done  
  
      
  lemma rpa_consistent_taut: "¬is_syn_taut C ⟹ rpa_consistent (assign_lits rpa_empty C)"
    unfolding rpa_consistent_def is_syn_taut_conv
    by auto
    
  lemma rpa_consistent_upd: "⟦ rpa_consistent A; ¬is_false A l ⟧ ⟹ rpa_consistent (A(l:=True))"
    unfolding rpa_consistent_def
    by auto

  definition "rpa_and_not_C A C ≡ assign_lits A (neg_lit`C)"
  lemma is_true_rpa_and_not_C: "is_true (rpa_and_not_C A C) l ⟷ neg_lit l∈C ∨ is_true A l"
    by (cases l; auto simp: rpa_and_not_C_def)

  definition "rpa_is_blocked A C ≡ (∃l∈C. is_true A l) ∨ is_syn_taut C"
  
  lemma rpa_is_blocked_refine[simp]: "rpa_consistent A ⟹ rpa_is_blocked A C ⟷ is_blocked (rpa_α A) C"
    unfolding is_blocked_def rpa_is_blocked_def sem_clause'_def
    by (auto simp: split: if_splits)
    
  lemma rpa_and_not_C_consistent:
    assumes "rpa_consistent A"
    assumes "¬ rpa_is_blocked A C"
    shows "rpa_consistent (rpa_and_not_C A C)"
    using assms unfolding rpa_consistent_def rpa_and_not_C_def is_syn_taut_conv rpa_is_blocked_def
    by auto
    
  lemma rpa_and_not_C_refine'[simp]: 
    assumes C: "rpa_consistent A"
    assumes NB: "¬is_blocked (rpa_α A) C"
    shows "rpa_consistent (rpa_and_not_C A C)"
      and "rpa_α (rpa_and_not_C A C) = and_not_C (rpa_α A) C"
  proof -
    
    from C NB show [simp]: "rpa_consistent (rpa_and_not_C A C)" 
      using rpa_and_not_C_consistent by force

    from NB have NTAUT: "Pos x ∈ C ⟹ Neg x ∉ C" for x
      unfolding is_blocked_def is_syn_taut_conv by auto   
      
    from NB have NTRUE: "l ∈ C ⟹ sem_lit' l (rpa_α A) ≠ Some True" for l
      unfolding is_blocked_def sem_clause'_def by metis
        
    show "rpa_α (rpa_and_not_C A C) = and_not_C (rpa_α A) C"
      unfolding rpa_α_def rpa_and_not_C_def and_not_C_def
      by (auto simp: fun_eq_iff C dest: NTAUT NTRUE)
  qed    
    
    
  definition "rpa_is_conflict_clause A C ≡ (∀l∈C. is_false A l)"  

  (* For paper *)
  lemma "rpa_is_conflict_clause A C = (∀l∈C. A (neg_lit l))"  
    unfolding is_true_def rpa_is_conflict_clause_def ..
  
  
  lemma rpa_is_conflict_clause_refine'[simp]:
    assumes "rpa_consistent A"
    shows "rpa_is_conflict_clause A C ⟷ is_conflict_clause (rpa_α A) C"
    using assms
    unfolding rpa_is_conflict_clause_def sem_clause'_def
    by (auto simp add: boolopt_neq_simps)
    

  subsection ‹Unit or True Literal›    
  text ‹When doing a RUP proof, it does not matter if the clause is unit, 
    or if the found literal is just already assigned to true›
  
  definition "is_uot_lit A C l 
    ≡ l∈C ∧ sem_lit' l A ≠ Some False ∧ (sem_clause' (C-{l}) A = Some False)"
  definition "is_uot_clause A C ≡ ∃l. is_uot_lit A C l"
  definition "the_uot_lit A C ≡ THE l. is_uot_lit A C l"

  lemma is_uot_lit_inj: "is_uot_lit A C l ⟹ is_uot_lit A C l' ⟹ l=l'"
    unfolding is_uot_lit_def 
    by (force simp: sem_clause'_def split!: if_splits)
    
  lemma is_uot_clause_alt: "is_uot_clause A C ⟷ is_uot_lit A C (the_uot_lit A C)"
    by (metis is_uot_clause_def is_uot_lit_inj theI the_uot_lit_def)
  
  
  lemma is_uot_cases:
    assumes "is_uot_lit A C l"
    obtains 
      "l∈C" "sem_lit' l A = Some True"  
    | "is_unit_lit A C l"
    using assms unfolding is_uot_lit_def is_unit_lit_def
    by force
    
  lemma uot_propagation: "⟦C∈F; is_uot_lit A C l⟧ ⟹ equiv' F A (assign_lit A l)"
    by (auto elim!: is_uot_cases simp: unit_propagation)


  subsubsection ‹Refinement›    
  definition "rpa_is_uot_lit A C l ≡ l∈C ∧ ¬is_false A l ∧ (∀l'∈C-{l}. is_false A l')"
  (* For paper *)
  lemma "rpa_is_uot_lit A C l ⟷ l∈C ∧ ¬A(neg_lit l) ∧ (∀l'∈C-{l}. A(neg_lit l'))"
    unfolding rpa_is_uot_lit_def is_true_def by blast

  lemma rpa_is_uot_lit_inj: "rpa_is_uot_lit A C l ⟹ rpa_is_uot_lit A C l' ⟹ l=l'"
    unfolding rpa_is_uot_lit_def
    by auto

  definition "rpa_is_uot_clause A C ≡ ∃l. rpa_is_uot_lit A C l"    
  definition "rpa_the_uot_lit A C ≡ THE l. rpa_is_uot_lit A C l"
  
  lemma rpa_is_uot_lit: "rpa_is_uot_clause A C ⟹ rpa_is_uot_lit A C (rpa_the_uot_lit A C)"
    unfolding rpa_is_uot_clause_def rpa_the_uot_lit_def using rpa_is_uot_lit_inj
    by (metis theI)
  
  lemma rpa_is_uot_lit_refine[simp]:
    assumes "rpa_consistent A"
    shows "rpa_is_uot_lit A C l = is_uot_lit (rpa_α A) C l"
    using assms
    unfolding rpa_is_uot_lit_def is_uot_lit_def
    by (auto 2 3 simp: sem_clause'_def)

  lemma rpa_is_uot_clause_refine[simp]:  
    assumes "rpa_consistent A" 
    shows "rpa_is_uot_clause A C ⟷ is_uot_clause (rpa_α A) C"
    by (simp add: assms is_uot_clause_def rpa_is_uot_clause_def)
    
  lemma rpa_the_uot_lit_refine[simp]:  
    assumes "rpa_consistent A" "is_uot_clause (rpa_α A) C"
    shows "rpa_the_uot_lit A C = the_uot_lit (rpa_α A) C"
    using assms is_uot_clause_alt rpa_is_uot_clause_refine rpa_is_uot_lit rpa_is_uot_lit_inj rpa_is_uot_lit_refine by blast

  lemma is_uot_lit_not_False[simp]: "is_uot_lit A C l ⟹ sem_lit' l A ≠ Some False"
    using is_uot_lit_def by blast
    
    
    
  subsection ‹Abstract LRUP Checker›        
    
  datatype 'a checker_state = 
      CNF "'a cnf" 
    | PREP_LEMMA "'a cnf" "'a clause" "'a rp_ass"  
    | PROOF "'a cnf" "'a clause" "'a rp_ass"
    | PROOF_DONE "'a cnf" "'a clause"
    | UNSAT
    | FAIL 

    
  inductive checker_trans :: "'a checker_state ⇒ 'a checker_state ⇒ bool" where
    ct_start_lemma: "checker_trans (CNF F) (PREP_LEMMA F {} rpa_empty)"
  | ct_add_lit: "checker_trans (PREP_LEMMA F C A) (PREP_LEMMA F (insert l C) (A(neg_lit l:=True)))"  
  | ct_start_proof: "checker_trans (PREP_LEMMA F C A) (PROOF F C A)"
  | ct_add_unit: "⟦ uC∈F; rpa_is_uot_lit A uC ul ⟧ ⟹ checker_trans (PROOF F C A) (PROOF F C (A(ul:=True)))"
  | ct_add_conflict: "⟦ uC∈F; rpa_is_conflict_clause A uC ⟧ ⟹ checker_trans (PROOF F C A) (PROOF_DONE F C)"
  | ct_del_clauses: "⟦ F' ⊆ F ⟧ ⟹ checker_trans (CNF F) (CNF F')" 
  | ct_finish_proof: "C≠{} ⟹ checker_trans (PROOF_DONE F C) (CNF (insert C F))"
  | ct_finish_proof_unsat: "checker_trans (PROOF_DONE F {}) (UNSAT)"
  | ct_fail: "checker_trans s FAIL"
  | ct_refl: "checker_trans s s"   


  fun checker_invar :: "'a cnf ⇒ 'a checker_state ⇒ bool" where
    "checker_invar F⇩0 (CNF F) ⟷ (sat F⇩0 ⟶ sat F)"
  | "checker_invar F⇩0 (PREP_LEMMA F C A) ⟷ 
        (sat F⇩0 ⟶ sat F) 
      ∧ (is_syn_taut C ∨ rpa_consistent A ∧ rpa_α A = and_not_C (λ_. None) C)"  
(*  | "checker_invar F⇩0 (PROOF F C A) ⟷ 
        (sat F⇩0 ⟶ sat F) 
      ∧ ( is_syn_taut C ∨ 
          (rpa_consistent A ∧ equiv' F (and_not_C (λ_. None) C) (rpa_α A)) )"  
*)          
  | "checker_invar F⇩0 (PROOF F C A) ⟷ 
        (sat F⇩0 ⟶ sat F) 
      ∧ ( is_syn_taut C ∨ 
          (rpa_consistent A ∧ sat' F (and_not_C (λ_. None) C) = sat' F (rpa_α A)) )"  
  | "checker_invar F⇩0 (PROOF_DONE F C) ⟷ (sat F⇩0 ⟶ sat (insert C F))"        
  | "checker_invar F⇩0 (UNSAT) ⟷ ¬sat F⇩0"
  | "checker_invar _ FAIL ⟷ True"  

  
  (* For Paper *)
  experiment
  begin

    lemma rpa_α_emp_and_not_C: "⟦ ¬is_syn_taut C ⟧ ⟹ rpa_α (λl. neg_lit l ∈ C) = and_not_C (λ_. None) C"
      unfolding is_syn_taut_def
      by (auto simp: fun_eq_iff rpa_α_def is_true_def and_not_C_def)
    
    lemma rpa_α_eq_alt: "⟦¬is_syn_taut C; rpa_consistent A⟧ ⟹ rpa_α A = and_not_C (λ_. None) C ⟷ A = (λl. neg_lit l∈C)"
      unfolding is_syn_taut_def rpa_consistent_def
      apply (rule iffI; rule ext)
      subgoal for l
        apply (drule fun_cong[where x="var_of_lit l"])
        apply (cases l)
        by (auto simp: rpa_α_def and_not_C_def is_true_def split: if_splits)
      subgoal for v
        unfolding rpa_α_def and_not_C_def is_true_def by auto
      done
      
    lemma checker_invar_PREP_LEMMA_alt:
      "checker_invar F⇩0 (PREP_LEMMA F C A) ⟷ 
          (sat F⇩0 ⟶ sat F) 
        ∧ (is_syn_taut C ∨ rpa_consistent A ∧ A = (λl. neg_lit l∈C))"    
        by (auto simp: rpa_α_eq_alt)
  
    definition rpa_is_completion :: "'a rp_ass ⇒ ('a ⇒ bool) ⇒ bool" 
      where "rpa_is_completion A σ ≡ ∀x. (A (Pos x) ⟶ σ x) ∧ (A (Neg x) ⟶ ¬σ x)"
        
    lemma rpa_completion_implies_consistent: "rpa_is_completion A σ ⟹ rpa_consistent A"  
      unfolding rpa_is_completion_def rpa_consistent_def is_true_def 
      by (metis neg_lit_neq(1) var_of_lit.elims var_of_lit_neg_eq)
      
    thm sat'_def  
      
      
    definition "rpa_models' F A ≡ { σ. rpa_is_completion A σ ∧ sem_cnf F σ}"
        
    lemma rpa_models_α: "rpa_consistent A ⟹ rpa_models' F A = models' F (rpa_α A)"
      unfolding rpa_consistent_def rpa_models'_def models'_def rpa_is_completion_def compat_assignment_def rpa_α_def is_true_def
      by clarsimp fastforce
    
    definition "rpa_sat' F A ≡ rpa_models' F A ≠ {}"  
    
    lemma rpa_sat'_α: "rpa_consistent A ⟹ rpa_sat' F A = sat' F (rpa_α A) "
      unfolding rpa_sat'_def sat'_def by (simp add: rpa_models_α)
      
    lemma "rpa_sat' F A ⟷ (∃σ. sem_cnf F σ ∧ (∀l. A l ⟶ sem_lit l σ))"
      unfolding rpa_models'_def rpa_sat'_def rpa_is_completion_def
      apply (safe; clarsimp)
      subgoal by (metis sem_lit.elims(3))
      subgoal by (metis sem_lit.simps(1) sem_lit.simps(2))
      done
    
    definition "rpa_equiv' F A A' ≡ rpa_models' F A = rpa_models' F A'"
        
    lemma "rpa_equiv' F A A' ⟷ (∀σ. sem_cnf F σ ⟶ (rpa_is_completion A σ ⟷ rpa_is_completion A' σ))"
      unfolding rpa_equiv'_def rpa_models'_def by blast
    
    lemma rpa_emp_and_not_C_consistent: "rpa_consistent (λl. neg_lit l∈C) ⟷ ¬is_syn_taut C"
      unfolding is_true_def rpa_consistent_def is_syn_taut_conv neg_neg_lit
      by blast
    
    lemma equiv'_and_not_C_rpa_conv: "⟦ ¬is_syn_taut C; rpa_consistent A ⟧ ⟹ equiv' F (and_not_C (λ_. None) C) (rpa_α A) ⟷ rpa_equiv' F (λl. neg_lit l∈C) A"    
      unfolding rpa_equiv'_def equiv'_def 
      by (simp add: rpa_models_α rpa_emp_and_not_C_consistent rpa_α_emp_and_not_C)
  
    lemma checker_invar_PROOF_alt: "checker_invar F⇩0 (PROOF F C A) ⟷ 
        (sat F⇩0 ⟶ sat F) 
      ∧ ( is_syn_taut C ∨ 
          (rpa_consistent A ∧ rpa_sat' F (λl. neg_lit l∈C) = rpa_sat' F A))"  
      by (auto simp: rpa_sat'_α rpa_emp_and_not_C_consistent rpa_α_emp_and_not_C)
    
      
    lemma and_not_C_pres_models:
      assumes "models (F ∪ { {neg_lit l} | l. l∈C }) = {}"
      shows "models (insert C F) = models F"  
      using assms unfolding models_def sem_cnf_def sem_clause_def
      by fastforce
        
    lemma rup_step_correct:
      assumes "rpa_equiv' F (λl. neg_lit l∈C) A" "E∈F" "∀l∈E. A (neg_lit l)"
      assumes "sat F"
      shows "sat (insert C F)"
    proof -
      
      have "models (F ∪ { {neg_lit l} | l. l∈C }) = rpa_models' F (λl. neg_lit l∈C)"
        unfolding rpa_models'_def  models_def rpa_is_completion_def
        unfolding sem_cnf_def sem_clause_def
        apply safe
        apply simp
        apply (metis (mono_tags, lifting) Un_iff mem_Collect_eq sem_lit.simps(2) sem_neg_lit singletonD)
        apply simp
        apply (metis (mono_tags, lifting) Un_iff mem_Collect_eq sem_lit.simps(1) sem_neg_lit singletonD)
        apply simp
        apply auto []
        apply auto [] 
        apply (metis sem_lit.elims(2))
        done
      
      moreover have "rpa_models' F A = {}" using ‹E∈F› ‹∀l∈E. A (neg_lit l)›
        unfolding rpa_models'_def rpa_is_completion_def sem_cnf_def sem_clause_def
        apply clarsimp
        by (metis neg_lit.simps(1) neg_lit.simps(2) sem_lit.elims(2))
        
      ultimately show ?thesis 
        using assms(1) ‹sat F› and_not_C_pres_models[of F C]
        unfolding rpa_equiv'_def sat_iff_has_models  
        by simp
    qed    
      
    
    lemma rpa_uot_propagation:
      assumes "rpa_consistent A" "rpa_is_uot_lit A uC ul" "uC∈F" 
      shows "rpa_consistent (A(ul := True))" (is ?G1) 
        and "rpa_equiv' F A (A(ul := True))" (is ?G2)
    proof -  
      from assms show G1: "?G1" by auto
      
      from assms show "?G2"
        by (metis (no_types, lifting) G1 equiv'_def is_uot_lit_def rpa_equiv'_def 
          rpa_is_uot_lit_refine rpa_models_α rpa_set_α(2) uot_propagation)
          
    qed      


    lemma rpa_empty_sat: "rpa_sat' F (λ_. False) = sat F"
      by (simp add: rpa_sat'_α)
        
    lemma "¬is_syn_taut C ⟹ rpa_sat' F (rpa_and_not_C (λ_. False) C) = sat (F ∪ neg_clause C)" 
      by (simp add: rpa_sat'_α rpa_and_not_C_consistent is_blocked_empy_taut sat'_and_not_C_conv)
      
    lemma rpa_uot_pres_sat:
      assumes "rpa_consistent A" "rpa_is_uot_lit A uC ul" "uC∈F" 
      shows "rpa_consistent (A(ul := True))" (is ?G1) 
        and "rpa_sat' F A = rpa_sat' F (A(ul := True))" (is ?G2)
    proof -  
      from assms show G1: "?G1" by auto
      
      from assms show "?G2"
        apply (simp add: rpa_sat'_α)
        by (simp add: sat'_equiv uot_propagation)
          
    qed      
    
    lemma rpa_conflict_unsat:
      assumes "rpa_consistent A" "rpa_is_conflict_clause A cC" "cC∈F"
      shows "¬rpa_sat' F A"
      using assms
      apply (simp add: rpa_sat'_α)
      by (simp add: conflict_clause_imp_no_models sat'_def)

    (* The consistency assumption is actually not needed here *)  
    lemma 
      assumes  "rpa_is_conflict_clause A cC" "cC∈F"
      shows "¬rpa_sat' F A"
      using assms
      by (metis (no_types, lifting) Collect_empty_eq conflict_clause_imp_no_models 
        rpa_completion_implies_consistent rpa_is_conflict_clause_refine' rpa_models'_def rpa_sat'_α 
        rpa_sat'_def sat'_def)
      
      
          
          
  end
  
  
    
    
    
    
      
    
  lemma checker_invar_init[simp]: "checker_invar F (CNF F)" by auto  

  (* TODO: Move *)
  lemma is_syn_taut_insert[simp]: "is_syn_taut (insert l C) ⟷ is_syn_taut C ∨ neg_lit l∈C"
    unfolding is_syn_taut_def by auto
  
    
    
  lemma sem_and_Not_C_conv: "¬is_syn_taut C 
    ⟹ sem_lit' l (and_not_C Map.empty C) 
      = (if l∈C then Some False else if neg_lit l∈C then Some True else None)"  
    unfolding is_syn_taut_def and_not_C_def
    apply (cases l) by auto
  
    
  lemma and_not_C_insert: "⟦¬is_syn_taut C; neg_lit l ∉ C⟧ 
    ⟹ and_not_C Map.empty (insert l C) = assign_lit (and_not_C Map.empty C) (neg_lit l)"  
    unfolding and_not_C_def assign_lit_def is_syn_taut_def
    by (cases l; auto simp: fun_eq_iff split!: if_splits)
    
  lemma checker_trans_pres_invar:
    assumes "checker_invar F⇩0 cs"
    assumes "checker_trans cs cs'"
    shows "checker_invar F⇩0 cs'"
    using assms(2,1)
    apply cases
    apply simp_all
    subgoal by (auto simp: sem_and_Not_C_conv and_not_C_insert) 
    subgoal using is_blocked_empy_taut by fastforce 
    subgoal by (metis is_uot_lit_def rpa_consistent_upd rpa_is_uot_lit_def rpa_is_uot_lit_refine rpa_set_α(2) sat'_equiv uot_propagation)
    subgoal for uC F A C
      apply (cases "is_syn_taut C"; simp)
      apply safe
      subgoal by (simp add: conflict_clause_imp_no_models sat'_def)
      subgoal by (auto simp add: sat'_and_not_C_conv dest: pres_sat_by_conj_negated)
      done  
    subgoal using sat_antimono by blast 
    subgoal by (simp add: unsat_empty_clause)
    done
    
  lemmas [simp del] = checker_invar.simps

  (* For paper *)
  
  theorem checker_trans_rtrancl_unsatI: "checker_trans⇧*⇧* (CNF F) UNSAT ⟹ ¬sat F"
    by (smt (verit, best) checker_invar.simps(1) checker_invar.simps(5) checker_trans_pres_invar rtranclp_induct)
  
      
  (*
  datatype 'a fbuilder_state = 
    FB_CNF "'a cnf"
  | FB_PREP_CLAUSE "'a cnf" "'a clause"  
  *)



end