Theory Combined_TwoSat

section ‹Formalisation of 2SAT using Autoref with graph tabulation via Containers›

theory Combined_TwoSat
imports Containers.TwoSat_Ex Simple_DFS "Containers.Mapping_Impl"
begin

subsection ‹Representation of Formulas›  

text ‹Tell Autoref that literals are refined by themselves›  
lemma [autoref_rules]: "(Lit,Lit)∈Id→Id→Id" by simp

text ‹We represent formulas as lists of pairs of literals›
type_synonym cnfi = "(lit × lit) list"

text ‹We define the relation between formula implementations and formula via
  an abstraction function and an invariant›
definition cnf_α :: "cnfi ⇒ cnf" where "cnf_α cnfi = (uncurry Upair) ` set cnfi"
definition is_2sati :: "cnfi ⇒ bool" where "is_2sati cnfi ≡ ∀(l1,l2)∈set cnfi. l1≠l2"  
definition "cnfi_rel ≡ br cnf_α is_2sati"

text ‹We show that the concrete invariant matches our abstract invariant @{const is_2sat}›
lemma is_2sati_correct: "is_2sati cnfi ⟷ is_2sat (cnf_α cnfi)"  
  unfolding is_2sati_def is_2sat_def cnf_α_def
  by (auto)

text ‹Setup for Autoref, the conceptual types of formulas›
consts i_cnf :: "interface"
lemmas [autoref_rel_intf] = REL_INTFI[of "cnfi_rel" i_cnf]

subsection ‹Implication Graph›

text ‹We implement the implication graph as a function from nodes to 
  distinct lists of nodes. However, instead of iterating over the whole formula
  each time we query the successors of a node, we tabulate the complete successor
  function in a map. This map will later be implemented using the Containers framework.
  
  The function ‹αsl› abstracts from a mapping to a successor function, 
  interpreting unmapped nodes to have empty successor lists.
›
(* Intentionally restricting the types here: The concept is as general as 
  inserting elements into ‹('a,'b list) mapping›. *)
definition αsl :: "(lit, lit list) mapping ⇒ lit ⇒ lit list"
  where "αsl m ≡ the_default [] o Mapping.lookup m"

text ‹The ‹ins_edge› option inserts a new element ‹v› into the successor list for node ‹k››
definition ins_edge :: "lit ⇒ lit ⇒ ((lit,lit list) mapping) ⇒ ((lit,lit list) mapping)"
  where "ins_edge k v m = (case Mapping.lookup m k of 
    None ⇒ Mapping.update k [v] m | Some l ⇒ Mapping.update k (remdups (v#l)) m)"

text ‹Abstract meaning of the empty map and the ‹ins_edge› operation:›      
lemma sl_abs[simp]: 
  "αsl Mapping.empty = (λ_. [])"
  "αsl (ins_edge k v m) = (αsl m)(k := remdups (v#αsl m k))"  
  unfolding αsl_def ins_edge_def by(transfer; auto split: option.split; fail)+

text ‹Auxiliary lemmas for inductive reasoning about list-representation of formula›  
lemma cnf_α_struct[simp]: 
  "cnf_α [] = {}"
  "cnf_α (cl # cls) = insert (uncurry Upair cl) (cnf_α cls)" for cl cls
  by (auto simp: cnf_α_def)

lemma is_2sati_struct[simp]:
  "is_2sati []" 
  "is_2sati ((l1,l2) # cnfi) ⟷ l1≠l2 ∧ is_2sati cnfi" for l1 l2 cnfi
  by(auto simp add: is_2sati_def)

text ‹Finally, it is straightforward to tabulate the successor graph by folding 
  over the clause list:
›
definition "ins_edges ≡ λ(l⇩1,l⇩2) m. ins_edge (negate l⇩1) l⇩2 (ins_edge (negate l⇩2) l⇩1 m)"
definition "tabulate cnfi = fold ins_edges cnfi Mapping.empty"

text ‹The correctness proof is also straightforward, 
  although the necessary generalization for the induction 
  to go through makes it somewhat technical.
›

lemma tabulate_aux1:
  "E_of_succ (λv. set (αsl (fold ins_edges cnfi M) v)) 
  = imp_graph (cnf_α cnfi) ∪ E_of_succ (set o αsl M)"
proof (induction cnfi arbitrary: M)
  case Nil
  then show ?case by simp
next
  case (Cons a cnfi)
  show ?case 
    by (simp add: Cons.IH)(simp add: E_of_succ_def ins_edges_def split!: prod.splits if_splits)
qed

lemma tabulate_aux2:
  "distinct (αsl M v) ⟹ distinct (αsl (fold ins_edges cnfi M) v)"
  apply (induction cnfi arbitrary: M)
  apply simp
  apply (clarsimp simp: ins_edges_def)
  apply rprems
  apply auto 
  done

lemma tabulate_refines[autoref_rules]: 
  "(λcnfi. αsl (tabulate cnfi), imp_graph) ∈ cnfi_rel → ⟨Id⟩succg_rel"
proof rule
  fix cnfi cnf
  assume "(cnfi,cnf)∈cnfi_rel"
  then show "(αsl (tabulate cnfi), imp_graph cnf) ∈ ⟨Id⟩succg_rel"
    unfolding in_id_succg_rel_iff tabulate_def 
    using tabulate_aux1[of cnfi Mapping.empty] 
    using tabulate_aux2[of Mapping.empty _ cnfi]
    unfolding E_of_succ_def cnfi_rel_def br_def by auto
qed  
  

(* Non-tail-recursive version with simpler proof *)  
fun ig_succm :: "cnfi ⇒ (lit, lit list) mapping" where
  "ig_succm [] = Mapping.empty"
| "ig_succm (cl#cls) = ins_edges cl (ig_succm cls)"  

lemma ig_succm_refines: 
  "(λcnfi. αsl (ig_succm cnfi), imp_graph) ∈ cnfi_rel → ⟨Id⟩succg_rel"
proof
  fix cnfi cnf
  assume "(cnfi,cnf)∈cnfi_rel"
  then show "(αsl (ig_succm cnfi), imp_graph cnf) ∈ ⟨Id⟩succg_rel"
    unfolding in_id_succg_rel_iff
    apply (induction cnfi arbitrary: cnf rule: ig_succm.induct)
    apply (simp add: cnfi_rel_def in_br_conv)
    apply (force simp: cnfi_rel_def in_br_conv ins_edges_def)
    done
qed

subsection ‹Variables of CNF›
text ‹The set of variables of a CNF is implemented by a distinct list›
definition vars_of_cnfi :: "cnfi ⇒ var list"
where "vars_of_cnfi cnfi ≡ remdups (concat (map (λ(l1, l2). [var l1, var l2]) cnfi))"

lemma vars_of_cnfi_refine[autoref_rules]: 
  "(vars_of_cnfi, vars_of_cnf) ∈ cnfi_rel → ⟨Id⟩list_set_rel"
  by (fastforce simp: br_def vars_of_cnfi_def cnfi_rel_def
         vars_of_cnf_def cnf_α_def list_set_rel_def)
  

subsection ‹Implementing Satisfiability Check›

context
  fixes cnfi cnf
  assumes A[autoref_rules]: "(cnfi,cnf)∈cnfi_rel"
begin  
  lemma 
    shows cnfi_finite_reachable[simp]: "finite ((imp_graph cnf)⇧* `` {l})"
      and cnfi_finite_vars: "finite (vars_of_cnf cnf)"
      and cnfi_is_2sat: "is_2sat cnf"
    using A apply -
    apply (auto simp: finite_rtrancl_Image cnfi_rel_def br_def cnf_α_def) [2]
    by (simp add: cnfi_rel_def br_def is_2sati_correct)
  
  lemma sat1_refine: "satisfiable cnf = (let gr = imp_graph cnf in
       ∀x∈vars_of_cnf cnf. ¬ ((Pos x, Neg x) ∈ gr⇧* ∧ (Neg x, Pos x) ∈ gr⇧* ))"
    using finite_2sat_iff[OF cnfi_finite_vars cnfi_is_2sat] by (simp add: Let_def)
    
  schematic_goal sati_refine: "(?f::?'c, satisfiable cnf) ∈ ?R"
    unfolding sat1_refine
    by autoref
    
end

concrete_definition sati uses sati_refine

text ‹Setup of Containers-Framework to handle RBT-maps of literals›
derive ccompare lit   derive (rbt) mapping_impl lit


export_code sati checking SML

export_code sati checking SML OCaml? Haskell? Scala

lemma sati_correct: "is_2sati cnfi ⟹ sati cnfi ⟷ satisfiable (cnf_α cnfi)"
  using sati.refine unfolding cnfi_rel_def br_def 
  by (auto dest: fun_relD)
  
lemma sati_autoref_rl[autoref_rules]: "(sati, satisfiable) ∈ cnfi_rel → bool_rel"
  using sati.refine by auto

end