Theory IsaSAT_Restart_Inprocessing

(*TODO Rename to IsaSAT_Inprocessing*)
theory IsaSAT_Restart_Inprocessing
  imports IsaSAT_Setup
   IsaSAT_Simplify_Units
    Watched_Literals.Watched_Literals_Watch_List_Inprocessing
    More_Refinement_Libs.WB_More_Refinement_Loops
    IsaSAT_Restart
    IsaSAT_Simplify_Binaries
    IsaSAT_Simplify_Pure_Literals
    IsaSAT_Simplify_Forward_Subsumption
    IsaSAT_Restart_Inprocessing_Defs
begin

lemma isa_simplify_clauses_with_unit_st2_isa_simplify_clauses_with_unit_wl:
  assumes ‹(S,S') ∈ twl_st_heur_restart_ana' r u›
  shows
    ‹isa_simplify_clauses_with_units_st_wl2 S ≤ ⇓ (twl_st_heur_restart_ana' r u) (simplify_clauses_with_units_st_wl S')›
  apply (rule order_trans)
    defer
  apply (rule ref_two_step')
  apply (rule simplify_clauses_with_units_st_wl2_simplify_clauses_with_units_st_wl[unfolded Down_id_eq, of _ S'])
  subgoal by auto
  subgoal
    apply (rule isa_simplify_clauses_with_units_st2_simplify_clauses_with_units_st2[THEN order_trans, of _ S'])
    apply (rule assms)
    subgoal using assms by auto
    done
  done


lemma incr_purelit_rounds_st_twl_st_heur_restart_ana':
  assumes S⇩0T: ‹(S⇩0, T) ∈ twl_st_heur_restart_ana' r u›
  shows ‹(incr_purelit_rounds_st S⇩0, T) ∈twl_st_heur_restart_ana' r u›
  using assms by (auto simp: incr_purelit_rounds_st_def twl_st_heur_restart_def
    twl_st_heur_restart_ana_def)

lemma isa_pure_literal_elimination_round_wl_pure_literal_elimination_round_wl:
  assumes S⇩0T: ‹(S⇩0, T) ∈ twl_st_heur_restart_ana' r u›
  shows ‹isa_pure_literal_elimination_round_wl S⇩0 ≤⇓{((_, U), V). (U,V)∈twl_st_heur_restart_ana' r u} (pure_literal_elimination_round_wl T)›
proof -
  show ?thesis
    unfolding isa_pure_literal_elimination_round_wl_def pure_literal_elimination_round_wl_def Let_def[of ‹incr_purelit_rounds_st _›]
    apply (refine_rcg isa_pure_literal_deletion_wl_pure_literal_deletion_wl[where r=r and u=‹learned_clss_count S⇩0›]
      isa_pure_literal_count_occs_wl_pure_literal_count_occs_wl[where r=r and u=‹learned_clss_count S⇩0›]
      isa_simplify_clauses_with_unit_st2_isa_simplify_clauses_with_unit_wl[where r=r and u=‹learned_clss_count S⇩0›])
    subgoal using assms unfolding isa_pure_literal_elimination_round_wl_pre_def by fast
    subgoal using assms by (auto simp: twl_st_heur_restart_ana_def)
    subgoal using assms by (auto simp: twl_st_heur_restart_ana_def)
    subgoal using assms by (auto simp: twl_st_heur_restart_ana_def)
    subgoal
      by (subst get_conflict_wl_is_None_heur_get_conflict_wl_is_None_ana[THEN fref_to_Down_unRET_Id])
        (use assms in ‹auto simp: get_conflict_wl_is_None_def›)
    subgoal by auto
    apply (rule order_trans[OF ])
    apply (rule isa_pure_literal_deletion_wl_pure_literal_deletion_wl[where r=r and u=‹learned_clss_count S⇩0›])
    prefer 3
    apply (rule conc_fun_R_mono)
    subgoal using assms by auto
    subgoal by auto
    subgoal by auto
    subgoal using assms by auto
    subgoal using assms by auto
    done
qed


lemma schedule_next_pure_lits_st_twl_st_heur_restart_ana':
  assumes ‹(S,S') ∈ twl_st_heur_restart_ana' r u› ‹u ≤ u'›
  shows ‹(schedule_next_pure_lits_st S, S') ∈ twl_st_heur_restart_ana' r u'›
  using assms by (auto simp: schedule_next_pure_lits_st_def twl_st_heur_restart_ana_def
    twl_st_heur_restart_def)

lemma isa_pure_literal_elimination_wl_pure_literal_elimination_wl:
  assumes ‹(S, S') ∈ twl_st_heur_restart_ana' r u›
  shows ‹isa_pure_literal_elimination_wl S ≤⇓(twl_st_heur_restart_ana' r u) (pure_literal_elimination_wl S')›
proof -
  have [refine]: ‹RETURN (3::nat) ≤ ⇓ {(a,b). a = b} (RES UNIV)›
    ‹RETURN (x1d = 0) ≤ ⇓ bool_rel (RES UNIV)› for x1d
    by (auto simp: RETURN_RES_refine)
  have [refine]: ‹((S, 0, False), S', 0, False) ∈ twl_st_heur_restart_ana' r (learned_clss_count S) ×⇩r Id ×⇩r Id›
    using assms by auto
  show ?thesis
    unfolding isa_pure_literal_elimination_wl_def pure_literal_elimination_wl_def Let_def[of ‹incr_purelit_rounds_st _›]
    apply (refine_vcg isa_pure_literal_elimination_round_wl_pure_literal_elimination_round_wl[where r=r and u=‹learned_clss_count S›]
      schedule_next_pure_lits_st_twl_st_heur_restart_ana'[where r=r and u=‹learned_clss_count S› and u'=u])
    subgoal using assms unfolding isa_pure_literal_elimination_wl_pre_def by fast
    subgoal for max_rounds max_roundsa x x'
      using assms unfolding isa_pure_literal_elimination_wl_inv_def case_prod_beta prod_rel_fst_snd_iff
      by (rule_tac x=S' in exI, rule_tac x=‹fst x'› in exI) auto
    subgoal by auto
    subgoal by auto
    subgoal using assms by (auto simp: twl_st_heur_restart_ana_def)
    subgoal by auto
    subgoal by (rule incr_purelit_rounds_st_twl_st_heur_restart_ana') auto
    subgoal by auto
    subgoal using assms by auto
    subgoal using assms by auto
    done
qed

lemma isa_pure_literal_eliminate:
  assumes ‹(S, S') ∈ twl_st_heur_restart_ana' r u›
  shows ‹isa_pure_literal_eliminate S ≤⇓(twl_st_heur_restart_ana' r u) (pure_literal_eliminate_wl S')›
proof -
  have [refine]: ‹RETURN (should_eliminate_pure_st S)  ≤ ⇓ bool_rel (pure_literal_eliminate_wl_needed S')›
    unfolding pure_literal_eliminate_wl_needed_def by auto
  show ?thesis
    unfolding isa_pure_literal_eliminate_def pure_literal_eliminate_wl_def
    by (refine_vcg isa_pure_literal_elimination_wl_pure_literal_elimination_wl)
     (use assms in auto)
qed

end