Theory Containers_TwoSat_Ex

(* Title:      Containers/Examples/Containers_TwoSat_Ex.thy
   Author:     Andreas Lochbihler, ETH Zurich *)

section ‹Implementation of 2SAT using Containers›

theory Containers_TwoSat_Ex imports
  TwoSat_Ex
  Containers_DFS_Ex
begin

lemma abort_parametric [transfer_rule]: includes lifting_syntax shows (* Move to Isabelle distribution *)
  "((=) ===> ((=) ===> A) ===> A) Code.abort Code.abort"
unfolding Code.abort_def by transfer_prover


instantiation uprod :: (finite_UNIV) finite_UNIV begin
definition finite_UNIV_uprod :: "('a uprod, bool) phantom"
where "finite_UNIV_uprod = Phantom('a uprod) (of_phantom (finite_UNIV :: ('a, bool) phantom))"
instance by standard(auto simp add: finite_UNIV_uprod_def finite_UNIV)
end

instantiation uprod :: (card_UNIV) card_UNIV begin
definition card_UNIV_uprod :: "('a uprod, nat) phantom"
where "card_UNIV_uprod = (let n = of_phantom (card_UNIV :: ('a, nat) phantom) in Phantom('a uprod) (n * (n + 1) div 2))"
instance by standard(auto simp add: card_UNIV_uprod_def card_UNIV Let_def card_UNIV_uprod)
end

text ‹
  To instantiate the @{class ceq} type class for @{typ "'a uprod"}, we must make a small detour.
  As @{typ "'a uprod"}'s type definition uses HOL equality, we cannot implement a new notion of 
  equality that is parametrised by the equality relation. Instead, we define the subtype of all binary
  relations that contains only @{term "(=)"}, and define the parametrised equality relation @{term uprod_ceq}
  on the subtype. Then, the instantiation can pass the equality relation from @{term "CEQ('a :: ceq)"}
  to @{term uprod_ceq} because the type class axioms ensure that the obtained relation is equivalent
  to @{term "(=)"}.
›

typedef 'a equal = "{(=) :: 'a ⇒ 'a ⇒ bool}" by simp

setup_lifting type_definition_equal

lift_definition uprod_eq :: "'a equal ⇒ 'a uprod ⇒ 'a uprod ⇒ bool"
is "λeq (a, b) (c, d). eq a c ∧ eq b d ∨ eq b c ∧ eq a d"
by auto

lemma uprod_eq_simps [simp, code]:
  "uprod_eq eq (Upair a b) (Upair c d) ⟷ 
   Rep_equal eq a c ∧ Rep_equal eq b d ∨ Rep_equal eq b c ∧ Rep_equal eq a d"
  supply Upair.transfer[transfer_rule] by transfer simp


lift_definition (code_dt) ceq_equal :: "'a :: ceq equal option" is "CEQ('a)"
apply(cases "CEQ('a)")
subgoal by(simp)
subgoal by(rule forw_subst[where P="pred_option _"], assumption)(simp (no_asm_use); simp add: ceq)
done

instantiation uprod :: (ceq) ceq begin
definition ceq_uprod
where "ceq_uprod = map_option uprod_eq ceq_equal"
instance
  apply(standard)
  apply(clarsimp simp add: ceq_uprod_def split: option.split_asm)
  apply transfer
  apply(auto simp add: fun_eq_iff)
  done
end

text ‹
  For comparison, we do a similar trick as for @{class ceq}.
›

typedef 'a compare = "{f :: 'a comparator. comparator f}"
proof -
  have "partial_order_on UNIV {(x, y). x = y}"
    by(simp add: partial_order_on_def preorder_on_def refl_on_def trans_def antisym_def)
  then obtain ord :: "('a × 'a) set" where lin: "linear_order ord"
    by(rule porder_extend_to_linorder)
  define f :: "'a comparator" where
    "f x y = (if (x, y) ∈ ord ∧ (y, x) ∈ ord then Eq else if (x, y) ∈ ord then Lt else Gt)" for x y
  have "comparator f"
  proof
    show "invert_order (f x y) = f y x" for x y using lin
      by(cases "x = y")(auto simp add: f_def linear_order_on_def partial_order_on_def preorder_on_def refl_on_def total_on_def)
    show "x = y" if "f x y = Eq" for x y using that lin
      by(auto simp add: f_def linear_order_on_def partial_order_on_def antisym_def split: if_split_asm)
    show "f x z = Lt" if "f x y = Lt" "f y z = Lt" for x y z using that lin
      by(auto simp add: f_def linear_order_on_def partial_order_on_def preorder_on_def split: if_split_asm dest: transD)
  qed
  thus ?thesis by auto
qed

setup_lifting type_definition_compare

lift_definition (code_dt) ccompare_comparator :: "'a :: ccompare compare option"
is "CCOMPARE('a)"
apply(cases "CCOMPARE('a)")
subgoal by simp
subgoal by(rule forw_subst[where P="pred_option _"], assumption)(simp (no_asm_use); simp add: ccompare)
done

lift_definition uprod_compare :: "'a compare ⇒ 'a uprod comparator"
is "λcompare (a, b) (c, d).
  let (x, y) = case compare a b of Lt ⇒ (a, b) | _ ⇒ (b, a);
      (x', y') = case compare c d of Lt ⇒ (c, d) | _ ⇒ (d, c)
  in case compare x x' of Lt ⇒ Lt | Gt ⇒ Gt | Eq ⇒ compare y y'"
subgoal for compare ab ab' cd cd'
  proof(cases ab; cases ab'; cases cd; cases cd'; hypsubst; clarsimp; elim disjE conjE; clarsimp)
    fix a b c d
    assume compare: "comparator compare"
    then interpret comparator compare .
    let ?xy = "case compare a b of Lt ⇒ (a, b) | _ ⇒ (b, a)" 
    let ?xy' = "case compare c d of Lt ⇒ (c, d) | _ ⇒ (d, c)"
    let ?yx = "case compare b a of Lt ⇒ (b, a) | _ ⇒ (a, b)"
    let ?yx' = "case compare d c of Lt ⇒ (d, c) | _ ⇒ (c, d)"
  
    have [simp]: "?xy = ?yx" "?xy' = ?yx'"
      by(auto split: order.split simp add: eq Gt_lt_conv Lt_lt_conv)
    let ?side = "λxy xy'. case xy of (x, y) ⇒ case xy' of (x', y') ⇒ (case compare x x' of Eq ⇒ compare y y' | Lt ⇒ Lt | Gt ⇒ Gt)"
    show "?side ?xy ?xy' = ?side ?xy ?yx'" "?side ?yx ?xy' = ?side ?xy ?xy'" "?side ?yx ?yx' = ?side ?xy ?xy'"
      by simp_all
  qed
done

lemma uprod_compare_simps [simp, code]:
  "uprod_compare compare (Upair a b) (Upair c d) =
   (let (x, y) = case Rep_compare compare a b of Lt ⇒ (a, b) | _ ⇒ (b, a);
        (x', y') = case Rep_compare compare c d of Lt ⇒ (c, d) | _ ⇒ (d, c)
    in case Rep_compare compare x x' of Eq ⇒ Rep_compare compare y y' | Lt ⇒ Lt | Gt ⇒ Gt)"
  for compare supply Upair.transfer[transfer_rule]
  by transfer simp

lemma comparator_uprod_compare: "comparator (uprod_compare compare)" for compare
proof
  show "invert_order (uprod_compare compare x y) = uprod_compare compare y x" for x y
  proof(transfer, goal_cases)
    case (1 compare x y)
    then interpret comparator compare .
    show ?case by(auto split!: order.split prod.split simp add: eq Gt_lt_conv Lt_lt_conv sym dest: order.asym)
  qed
  show "x = y" if "uprod_compare compare x y = Eq" for x y using that
  proof(transfer, goal_cases)
    case (1 compare x y)
    from 1(1) interpret comparator compare .
    show ?case using 1(2) by(clarsimp split: order.split_asm prod.split_asm simp add: eq)
  qed
  show "uprod_compare compare x z = Lt" 
    if "uprod_compare compare x y = Lt" "uprod_compare compare y z = Lt" for x y z using that
  proof(transfer, goal_cases)
    case (1 compare x y z)
    from 1(1) interpret comparator compare .
    show ?case using 1(2-)
      by(auto split!: order.splits prod.split_asm simp add: eq Gt_lt_conv Lt_lt_conv elim: trans)
  qed
qed

instantiation uprod :: (ccompare) ccompare begin
definition ccompare_uprod
where "ccompare_uprod = map_option uprod_compare (ccompare_comparator :: 'a compare option)"
instance by standard(clarsimp simp add: ccompare_uprod_def comparator_uprod_compare)
end

instantiation uprod :: (set_impl) set_impl begin
definition "SET_IMPL('a uprod) = Phantom('a uprod) (of_phantom SET_IMPL('a))"
instance ..
end




(* Graph uses successor representation with function 
  -> let's write a code equation for imp_graph
  -> let's first define the successor operation for an individual vertex.
*)

function succs_of_clause :: "lit ⇒ lit uprod ⇒ lit set ⇒ lit set" where
  "succs_of_clause l (Upair l1 l2) = (if l = negate l1 then insert l2 else if l = negate l2 then insert l1 else id)"
  by(metis surj_pair uprod_exhaust) auto
termination by lexicographic_order

lemma succs_of_clause_split: "P (succs_of_clause l x) ⟷ (∀l1 l2. x = Upair l1 l2 ⟶ P (succs_of_clause l (Upair l1 l2)))"
  by(cases x)(auto simp only:)

context begin

lemma commute_succs_of_clause: "comp_fun_commute (succs_of_clause l)"
  by unfold_locales(auto split: succs_of_clause_split)

interpretation comp_fun_commute "succs_of_clause l" for l by(rule commute_succs_of_clause)

lemma idem_succs_of_clause: "comp_fun_idem (succs_of_clause l)"
  by unfold_locales(auto split: succs_of_clause_split)

interpretation comp_fun_idem "succs_of_clause l" for l by(rule idem_succs_of_clause)

lift_definition succs_loop_body :: "lit ⇒ (lit uprod, lit set) comp_fun_idem" is
  "succs_of_clause" by(rule idem_succs_of_clause)

definition succ_imp_graph :: "cnf ⇒ lit ⇒ lit set"
  where "succ_imp_graph cnf l = set_fold_cfi (succs_loop_body l) {} cnf"

lemma succ_imp_graph_alt_def: 
  "succ_imp_graph cnf l = Finite_Set.fold (succs_of_clause l) {} cnf"
  unfolding succ_imp_graph_def by transfer simp

lemma succ_imp_graph_correct: 
  "finite cnf ⟹ succ_imp_graph cnf l = {l'. (l, l') ∈ imp_graph cnf}"
  by(induction rule: finite_induct)(auto split: succs_of_clause_split simp add: succ_imp_graph_alt_def)

end

lemma imp_graph_code:
  "imp_graph cnf = 
  (if finite cnf then {(l, l'). l' ∈ succ_imp_graph cnf l} 
   else Code.abort (STR ''Infinite or invalid 2CNF formula'') (λ_. imp_graph cnf))"
by(auto simp add: succ_imp_graph_correct)

lift_definition imp_graph_impl :: "cnf ⇒ lit graph" is imp_graph .

lemmas [code] = imp_graph_code[containers_identify]

lemma UNIV_lit: "UNIV = range (λ(x, pos). Lit x pos)"
  apply(auto)
  subgoal for x by(cases x; auto)
  done

instantiation lit :: finite_UNIV begin
definition "finite_UNIV_lit = Phantom(lit) False"
instance by(standard)(auto simp add: finite_UNIV_lit_def UNIV_lit inj_on_def UNIV_Times_UNIV[symmetric] finite_cartesian_product_iff simp del: UNIV_Times_UNIV dest!: finite_imageD)
end

derive (eq) ceq lit
derive (rbt) set_impl lit
derive ccompare lit

export_code imp_graph_impl checking SML

lemma finite_vars_of_cnf: "finite cnf ⟹ finite (vars_of_cnf cnf)"
by(clarsimp simp add: vars_of_cnf_def)

lemma satisfiable_code:
  "satisfiable cnf ⟷ 
  (if finite cnf ∧ is_2sat cnf then 
   let G = imp_graph cnf in ∀x∈vars_of_cnf cnf. ¬ (reachable G (Pos x) (Neg x) ∧ reachable G (Neg x) (Pos x))
   else Code.abort (STR ''Infinite or invalid 2CNF formula'') (λ_. satisfiable cnf))"
by(simp add: reachable_def finite_2sat_iff finite_vars_of_cnf Let_def)

lemmas [code] = satisfiable_code[containers_identify]

export_code satisfiable checking SML

subsection ‹Memoize the implication graph's successor function›

lemma succ_imp_graph_outside: "succ_imp_graph cnf l = {}" if "var l ∉ vars_of_cnf cnf"
proof(cases "finite cnf")
  case True
  interpret comp_fun_idem "succs_of_clause l" by(rule idem_succs_of_clause)
  show ?thesis using True that
    by induction(auto simp add: succ_imp_graph_alt_def vars_of_cnf_def split: if_split_asm succs_of_clause_split)
next
  case False
  then show ?thesis by(simp add: succ_imp_graph_alt_def)
qed

lift_definition tabulate_graph :: "cnf ⇒ (lit, lit set) mapping" is
  "λcnf x. if x ∉ Domain (imp_graph cnf) then None else Some (imp_graph cnf `` {x})" .

primrec insert_mapping :: "'k × 'v ⇒ ('k, 'v set) mapping ⇒ ('k, 'v set) mapping" where
  "insert_mapping (k, v) m = (case Mapping.lookup m k of None ⇒ Mapping.update k {v} m | Some V ⇒ Mapping.update k (insert v V) m)"

lemma comp_fun_idem_insert_mapping: "comp_fun_idem insert_mapping"
  unfolding insert_mapping_def
  by(unfold_locales; transfer; auto simp add: Map_To_Mapping.map_apply_def fun_eq_iff split!: option.split)

context begin
interpretation comp_fun_idem insert_mapping by(rule comp_fun_idem_insert_mapping)

function insert_clause :: "clause ⇒ (lit, lit set) mapping ⇒ (lit, lit set) mapping" where
  "insert_clause (Upair l1 l2) = insert_mapping (negate l1, l2) ∘ insert_mapping (negate l2, l1)"
  by(metis uprod_exhaust)(auto simp add: comp_fun_commute)
termination by lexicographic_order

lemma comp_fun_idem_insert_clause: "comp_fun_idem insert_clause"
  apply(unfold_locales)
  subgoal for x y by(cases x; cases y; simp; metis commute_left_comp comp_fun_commute rewriteL_comp_comp)
  subgoal for x by(cases x; simp; metis (no_types, opaque_lifting) commute_left_comp comp_assoc comp_fun_idem)
  done

lift_definition insert_clause' :: "(clause, (lit, lit set) mapping) comp_fun_idem" is "insert_clause"
  by(rule comp_fun_idem_insert_clause)

lemma tabulate_graph_code [code]:
  "tabulate_graph cnf = 
  (if finite cnf then set_fold_cfi insert_clause' Mapping.empty cnf 
   else Code.abort (STR ''Infinite clause set'') (λ_. tabulate_graph cnf))"
proof -
  interpret comp_fun_idem insert_clause by(rule comp_fun_idem_insert_clause)
  have * [symmetric]: "Finite_Set.fold insert_clause Mapping.empty cnf = tabulate_graph cnf"
    if "finite cnf" using that
  proof(induction)
    case empty
    then show ?case by(simp)(transfer; auto simp add: fun_eq_iff Map_To_Mapping.map_empty_def vars_of_cnf_def)
  next
    case (insert C cnf)
    show ?case by(cases C; simp add: insert; transfer)(auto simp add: fun_eq_iff Map_To_Mapping.map_apply_def split!: option.split)
  qed
  show ?thesis by(clarsimp)(transfer fixing: cnf; rule *)
qed

lemma succ_imp_graph_impl_code [code]:
  "succ_imp_graph cnf =
  (if finite cnf then let m = tabulate_graph cnf
   in (λl. case Mapping.lookup m l of None ⇒ {} | Some succs' ⇒ succs')
   else Code.abort (STR ''Infinite clause set'') (λ_. succ_imp_graph cnf))"
  by transfer(auto simp add: succ_imp_graph_correct fun_eq_iff Map_To_Mapping.map_apply_def dest: succ_imp_graph_outside)
end

derive (rbt) mapping_impl lit

export_code satisfiable checking SML Scala Haskell? OCaml?


end