Theory IsaSAT_Other

theory IsaSAT_Other
  imports IsaSAT_Conflict_Analysis IsaSAT_Backtrack IsaSAT_Decide
    IsaSAT_Other_Defs
begin
chapter ‹Combining Together: the Other Rules›

lemma cdcl_twl_o_prog_wl_D_heur_cdcl_twl_o_prog_wl_D:
  ‹(cdcl_twl_o_prog_wl_D_heur, cdcl_twl_o_prog_wl) ∈
   {(S, T). (S, T) ∈ twl_st_heur ∧ length (get_clauses_wl_heur S) = r ∧ learned_clss_count S = u} →⇩f
     ⟨bool_rel ×⇩f {(S, T). (S, T) ∈ twl_st_heur ∧
        length (get_clauses_wl_heur S) ≤ r + MAX_HEADER_SIZE+1 + unat32_max div 2  ∧ 
           learned_clss_count S ≤ Suc u}⟩nres_rel›
proof -
  have H: ‹(x, y) ∈ {(S, T).
               (S, T) ∈ twl_st_heur ∧
               length (get_clauses_wl_heur S) =
               length (get_clauses_wl_heur x)} ⟹
           (x, y)
           ∈ {(S, T).
               (S, T) ∈ twl_st_heur_conflict_ana ∧
               length (get_clauses_wl_heur S) =
               length (get_clauses_wl_heur x)}› for x y
    by (auto simp: twl_st_heur_state_simp twl_st_heur_twl_st_heur_conflict_ana)
   have H2: ‹(x, y) ∈ {(S, T).
     (S, T) ∈ twl_st_heur ∧
     length (get_clauses_wl_heur S) = r ∧ learned_clss_count S = u} ⟹
          (x, y) ∈ twl_st_heur_conflict_ana' r (get_learned_count x)› for x y
     by (auto simp: twl_st_heur_state_simp twl_st_heur_twl_st_heur_conflict_ana)
   have H3: ‹(x, y)
     ∈ {(S, T).
     (S, T) ∈ twl_st_heur ∧
     length (get_clauses_wl_heur S) = r ∧ learned_clss_count S = u} ⟹
     (x, y) ∈ {(S, T). (S, T) ∈ twl_st_heur''' r ∧ learned_clss_count S = u}› for x y
     by auto
 have UUa: ‹(U, Ua)
       ∈ {(S, T).
          (S, T) ∈ twl_st_heur ∧
          length (get_clauses_wl_heur S) ≤ 3 + 1 + r + unat32_max div 2 ∧
          learned_clss_count S ≤ Suc u} ⟹
       (U,  Ua)
       ∈ {(S, Tb).
          (S, Tb) ∈ twl_st_heur ∧
     length (get_clauses_wl_heur S) ≤ 3 + 1 + r + unat32_max div 2 ∧ learned_clss_count S ≤ Suc u}› for U Ua
   by auto
  show ?thesis
    unfolding cdcl_twl_o_prog_wl_D_heur_def cdcl_twl_o_prog_wl_def
      get_conflict_wl_is_None
    apply (intro frefI nres_relI)
    apply (refine_vcg
        decide_wl_or_skip_D_heur_decide_wl_or_skip_D[where r=r and u=u, THEN fref_to_Down, THEN order_trans]
        skip_and_resolve_loop_wl_D_heur_skip_and_resolve_loop_wl_D[where r=r, THEN fref_to_Down]
        backtrack_wl_D_nlit_backtrack_wl_D[where r=r and u=u, THEN fref_to_Down]
        isasat_current_status_id[THEN fref_to_Down, THEN order_trans])
    subgoal
      by (auto simp: twl_st_heur_state_simp
          get_conflict_wl_is_None_heur_get_conflict_wl_is_None[THEN fref_to_Down_unRET_Id])
    apply (rule H3; assumption)
    subgoal by (rule conc_fun_R_mono) auto
    subgoal by (auto simp: twl_st_heur_state_simp twl_st_heur_count_decided_st_alt_def)
    apply (rule H2; assumption)
    subgoal by (auto simp: twl_st_heur_state_simp twl_st_heur_twl_st_heur_conflict_ana)
    subgoal by (auto simp: twl_st_heur_state_simp)
    subgoal by (auto simp: twl_st_heur_state_simp dest!: get_learned_count_learned_clss_countD2)
    apply (rule UUa; assumption)
    subgoal by (auto simp: conc_fun_RES RETURN_def learned_clss_count_def)
    subgoal by (auto simp: twl_st_heur_state_simp)
    done
qed

lemma cdcl_twl_o_prog_wl_D_heur_cdcl_twl_o_prog_wl_D2:
  ‹(cdcl_twl_o_prog_wl_D_heur, cdcl_twl_o_prog_wl) ∈
   {(S, T). (S, T) ∈ twl_st_heur} →⇩f
     ⟨bool_rel ×⇩f {(S, T). (S, T) ∈ twl_st_heur}⟩nres_rel›
  apply (intro frefI nres_relI)
  apply (rule cdcl_twl_o_prog_wl_D_heur_cdcl_twl_o_prog_wl_D[THEN fref_to_Down, THEN order_trans])
  apply (auto intro!: conc_fun_R_mono)
  done

end