Theory Watched_Literals_Transition_System_Simp

theory Watched_Literals_Transition_System_Simp
imports
  Watched_Literals_Transition_System_Reduce
  Watched_Literals_Transition_System_Restart
begin


context twl_restart
begin

theorem wf_cdcl_twl_stgy_restart:
  ‹wf {(T, S :: 'v twl_st_restart). twl_restart_inv S ∧ cdcl_twl_stgy_restart S T}› (is ‹wf ?S›)
proof -
  have ‹?S ⊆
    {((S', T', U', m', n', g'), (S, T, U, m, n, g)).
        pcdcl_stgy_restart_inv (pstateW_of S, pstateW_of T, pstateW_of U, m, n, g) ∧
        pcdcl_stgy_restart (pstateW_of S, pstateW_of T, pstateW_of U, m, n, g)
           (pstateW_of S', pstateW_of T', pstateW_of U', m', n', g')} ∪
    {((S', T', U', m', n', g'), (S, T, U, m, n, g)).
        pcdcl_stgy_restart_inv (pstateW_of S, pstateW_of T, pstateW_of U, m, n, g) ∧
        S = S' ∧ T = T' ∧ m = m' ∧ n = n' ∧ g = g' ∧
      pstateW_of U = pstateW_of U' ∧ (literals_to_update_measure U', literals_to_update_measure U)
      ∈ lexn less_than 2}› (is ‹_ ⊆ ?A ∪ ?B›)
    by (auto dest!: cdcl_twl_stgy_cdclW_stgy_restart2 simp: twl_restart_inv_def)
  moreover have ‹wf (?A ∪ ?B)›
    apply (rule wf_union_compatible)
    subgoal
      by (rule wf_subset[OF wf_if_measure_f[OF wf_pcdcl_twl_stgy_restart],
        of _ ‹λ(S, T, U, m, g). (pstateW_of S, pstateW_of T, pstateW_of U, m, g)›]) auto
    subgoal
      by (rule wf_subset[OF wf_if_measure_f[OF ],
        of ‹(lexn less_than 2)›  _ ‹λ(S, T, U, m, g). literals_to_update_measure (U)›])
        (auto intro!: wf_lexn)
    subgoal
      by auto
    done
  ultimately show ?thesis
    by (blast intro: wf_subset)
qed

end


context twl_restart_ops
begin

lemma cdcl_twl_stgy_size_get_all_learned:
  ‹cdcl_twl_stgy S T ⟹ size (get_all_learned_clss S) ≤ size (get_all_learned_clss T)›
  by (induction rule: cdcl_twl_stgy.induct)
   (auto simp: cdcl_twl_cp.simps cdcl_twl_o.simps update_clauses.simps
    dest: multi_member_split)

lemma rtranclp_cdcl_twl_stgy_size_get_all_learned:
  ‹cdcl_twl_stgy** S T ⟹ size (get_all_learned_clss S) ≤ size (get_all_learned_clss T)›
  by (induction rule: rtranclp_induct)
    (auto dest!: cdcl_twl_stgy_size_get_all_learned)

(*TODO Move*)
lemma (in -) wf_trancl_iff: ‹wf (r+) ⟷ wf r›
  by (auto intro!: wf_subset[of ‹r+› r] simp: wf_trancl)

lemma (in -) tranclp_inv_tranclp:
  assumes ‹⋀S T. R S T ⟹ P S ⟹ P T›
  shows
    ‹{(T, S). R S T ∧ P S}+ = {(T, S). R++ S T ∧ P S}›
proof -
  have H: ‹R++ S T ⟹ P S ⟹ P T› for S T
    by (induction rule: tranclp_induct)
      (auto dest: assms)
  show ?thesis
    apply (rule; rule; clarify)
    unfolding mem_Collect_eq in_pair_collect_simp
    subgoal for a b
      by (induction rule: trancl_induct) auto
    subgoal for b x
      apply (induction rule: tranclp_induct)
      subgoal for b
        by auto
      subgoal for e f
        by (rule trancl_into_trancl2[of f e])
          (use H[of x e] in auto)
      done
    done
qed

definition partial_conclusive_TWL_run :: ‹'v twl_st ⇒ (bool × 'v twl_st) nres› where
  ‹partial_conclusive_TWL_run S = SPEC(λ(b, T). ∃R1 R2 m m0 n0.
       cdcl_twl_stgy_restart** (S, S, S, m0, n0, True) (R1, R2, T, m) ∧ (¬b ⟶ final_twl_state T))›

definition partial_conclusive_TWL_run2
  :: ‹nat ⇒ nat ⇒ 'v twl_st ⇒ 'v twl_st ⇒ 'v twl_st ⇒ (bool × 'v twl_st) nres›
where
  ‹partial_conclusive_TWL_run2  m0 n0 S0 T0 U0 = SPEC(λ(b, T). ∃R1 R2 m.
       cdcl_twl_stgy_restart** (S0, T0, U0, m0, n0, True) (R1, R2, T, m) ∧ (¬b ⟶ final_twl_state T))›

definition conclusive_TWL_run :: ‹'v twl_st ⇒ 'v twl_st nres› where
  ‹conclusive_TWL_run S = SPEC(λT. (∃R1 R2 m m0 n0.
       cdcl_twl_stgy_restart** (S, S, S, m0, n0, True) (R1, R2, T, m) ∧ final_twl_state T))›

definition conclusive_TWL_run2 :: ‹nat ⇒ nat ⇒ 'v twl_st ⇒ 'v twl_st ⇒ 'v twl_st ⇒ 'v twl_st nres› where
  ‹conclusive_TWL_run2 m0 n0 S0 T0 U0 = SPEC(λT. (∃R1 R2 m.
       cdcl_twl_stgy_restart** (S0, T0, U0, m0, n0, True) (R1, R2, T, m) ∧ final_twl_state T))›
end

end