Theory Watched_Literals_Transition_System_Reduce

theory Watched_Literals_Transition_System_Reduce
imports Watched_Literals_Transition_System_Restart
begin

inductive cdcl_twl_inp :: ‹'v twl_st ⇒ 'v twl_st ⇒ bool› where
  ‹cdcl_twl_subsumed S T ⟹ cdcl_twl_inp S T› |
  ‹cdcl_twl_subresolution S T ⟹ cdcl_twl_inp S T› |
  ‹cdcl_twl_unitres S T ⟹ cdcl_twl_inp S T› |
  ‹cdcl_twl_unitres_true S T ⟹ cdcl_twl_inp S T› |
  ‹cdcl_twl_restart S T ⟹ cdcl_twl_inp S T› |
  ‹cdcl_twl_pure_remove S T ⟹ cdcl_twl_inp S T›

lemma true_clss_clss_subset_entailedI:
  ‹UE + UE' = UE'' + ca ⟹ A ⊨ps set_mset UE ⟹ A ⊨ps set_mset UE' ⟹ A ⊨ps set_mset UE''›
  ‹UE + UE' = ca + UE'' ⟹ A ⊨ps set_mset UE ⟹ A ⊨ps set_mset UE' ⟹ A ⊨ps set_mset UE''›
  for UE :: ‹'v clauses›
  by (metis set_mset_union true_clss_clss_union_and)+

lemma cdcl_twl_restart_entailed_init:
  ‹cdcl_twl_restart S T ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of (pstateW_of S)) ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of (pstateW_of T))›
  by (induction rule: cdcl_twl_restart.induct)
   (auto simp: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def
    subset_mset.le_iff_add Un_left_commute image_Un sup_commute
    intro: true_clss_clss_subset_entailedI)

lemma cdcl_twl_inp_invs:
  assumes ‹cdcl_twl_inp S T›
    ‹twl_struct_invs S›
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S)›
  shows
    cdcl_twl_inp_twl_struct_invs: ‹twl_struct_invs T› (is ?A) and
    cdcl_twl_inp_twl_stgy_invs: ‹twl_stgy_invs S ⟹ twl_stgy_invs T› (is ‹_ ⟹ ?B›) and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of T)› (is ?C)
proof -
  show ?A
    using assms(1,2,3)
    by (induction rule: cdcl_twl_inp.induct)
      (blast dest: cdcl_twl_subsumed_struct_invs cdcl_twl_subresolution_twl_struct_invs
      cdcl_twl_unitres_struct_invs cdcl_twl_unitres_true_twl_struct_invs
      cdcl_twl_pure_remove_twl_struct_invs
      cdcl_twl_restart_twl_struct_invs)+
  show ?C
    using assms(1,2,3)
    apply (induction rule: cdcl_twl_inp.induct)
    apply (metis cdcl_subsumed_RI_pcdcl cdcl_subsumed_entailed_by_init cdcl_twl_subsumed_cdcl_subsumed
      rtranclp_pcdcl_entailed_by_init stateW_of_def twl_struct_invs_def)
    unfolding stateW_of_def
    apply (elim cdcl_twl_subresolution_decompE)
    apply (auto elim!: cdcl_twl_subresolution_decompE
      simp: twl_struct_invs_def struct_wf_twl_cls_alt_def twl_st_inv_alt_def; fail)[]
    apply (rule cdcl_subresolutions_entailed_by_init; assumption)
    apply (metis cdcl_flush_unit_unchanged cdcl_subresolution cdcl_subresolutions_entailed_by_init
      pcdcl.intros(1) pcdcl_core.intros(2) pcdcl_entailed_by_init rtranclp_pcdcl_all_struct_invs
      twl_struct_invs_def)
    apply (drule cdcl_twl_unitres_cdcl_unitres, drule cdcl_unitres_learn_subsume)
    apply assumption+
    using rtranclp_pcdcl_entailed_by_init twl_struct_invs_def apply blast
    apply (drule cdcl_twl_unitres_true_cdcl_unitres_true, drule pcdcl.intros)
    using pcdcl_entailed_by_init twl_struct_invs_def apply blast
    apply (solves ‹simp add: cdcl_twl_restart_entailed_init›)
    using cdcl_pure_literal_remove_entailed_by_init cdcl_twl_pure_remove_cdcl_pure_remove
      twl_struct_invs_def by blast
  with assms show ?B if ‹twl_stgy_invs S›
    using that
    apply (induction rule: cdcl_twl_inp.induct)
    apply (metis (no_types, lifting) cdcl_twl_subsumed_stgy_invs)
    using cdcl_twl_subresolution_twl_stgy_invs apply blast
    using cdcl_twl_unitres_twl_stgy_invs apply blast
    apply (metis (no_types, lifting) cdcl_twl_unitres_true_cdcl_unitres_true cdcl_unitres_true_same stateW_of_def twl_stgy_invs_def)
    using cdcl_twl_restart_twl_stgy_invs apply blast
    using cdcl_twl_pure_remove_twl_stgy_invs by blast
qed

lemma rtranclp_cdcl_twl_inp_invs:
  assumes ‹cdcl_twl_inp** S T›
    ‹twl_struct_invs S›
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S)›
  shows
    rtranclp_cdcl_twl_inp_twl_struct_invs: ‹twl_struct_invs T› and
    rtranclp_cdcl_twl_inp_twl_stgy_invs: ‹twl_stgy_invs S ⟹ twl_stgy_invs T› and
    rtranclp_cdcl_twl_inp_entailed_init:
      ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of T)›
  using assms
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal for T U using cdcl_twl_inp_invs[of T U] by auto
  subgoal for T U using cdcl_twl_inp_invs[of T U] by auto
  subgoal for T U using cdcl_twl_inp_invs[of T U] by auto
  done

lemma cdcl_twl_inp_no_new_conflict:
  ‹cdcl_twl_inp S T ⟹ get_conflict T = get_conflict S ∨ get_conflict T ≠ None ∧ count_decided(get_trail T) = 0›
  by (induction rule: cdcl_twl_inp.induct)
   (auto simp: cdcl_twl_subsumed.simps cdcl_twl_subresolution.simps cdcl_twl_unitres.simps
    cdcl_twl_unitres_true.simps cdcl_twl_restart.simps cdcl_twl_pure_remove.simps)

lemma rtranclp_pcdcl_restart_inprocessing: ‹pcdcl** S T ⟹ pcdcl_inprocessing** S T›
  by (induction rule: rtranclp_induct) (auto dest: pcdcl_inprocessing.intros)
 
lemma cdcl_twl_inp_pcdcl:
  ‹cdcl_twl_inp S T ⟹ twl_struct_invs S ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S) ⟹
  pcdcl_inprocessing** (pstateW_of S) (pstateW_of T)›
  apply (induction rule: cdcl_twl_inp.induct)
  subgoal
    by (meson cdcl_subsumed_RI_pcdcl cdcl_twl_subsumed_cdcl_subsumed pcdcl.intros(4) r_into_rtranclp
      rtranclp_pcdcl_restart_inprocessing)
  subgoal
    apply (rule rtranclp_pcdcl_restart_inprocessing, elim cdcl_twl_subresolution_decompE)
    apply (auto elim!: cdcl_twl_subresolution_decompE
      simp: twl_struct_invs_def struct_wf_twl_cls_alt_def twl_st_inv_alt_def; fail)[]
      apply (drule cdcl_subresolution)
    apply (auto elim!: cdcl_twl_subresolution_decompE
      simp: twl_struct_invs_def struct_wf_twl_cls_alt_def twl_st_inv_alt_def; fail)[]
    by (meson cdcl_subresolution pcdcl.intros(1) pcdcl.intros(5) pcdcl_core.intros(2)
      rtranclp.rtrancl_into_rtrancl)
  subgoal
    by (simp add: cdcl_twl_unitres_cdcl_unitres cdcl_unitres_learn_subsume rtranclp_pcdcl_restart_inprocessing)
  subgoal
    by (simp add: cdcl_twl_unitres_true_cdcl_unitres_true pcdcl.intros(8) r_into_rtranclp
      rtranclp_pcdcl_restart_inprocessing)
  subgoal
    using cdcl_twl_restart_pcdcl pcdcl_inprocessing.intros(2) by blast
  subgoal
    by (simp add: cdcl_twl_pure_remove_cdcl_pure_remove pcdcl.intros(10)
      pcdcl_inprocessing.intros(1) r_into_rtranclp)
  done

lemma rtranclp_cdcl_twl_inp_pcdcl:
  ‹cdcl_twl_inp** S T ⟹ twl_struct_invs S ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S) ⟹
  pcdcl_inprocessing** (pstateW_of S) (pstateW_of T)›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using cdcl_twl_inp_pcdcl[of T U] rtranclp_cdcl_twl_inp_invs[of S T]
    by simp
  done



context twl_restart_ops
begin
text ‹
  This is en essence the calculus with restarts we are now using. Compared to the version in my
  thesis, the major difference is that we don't restrict restarts anymore, by requiring only that
  at least one clause has been learned since.

  However, this has a major drawback: The transition do not depend only on the current state, but
  also on the path that was taken. This is annoying for refinement, because the main loop does not
  do one transition anymore, but only a part of transitions. The difference is very small on the
  practical side, but that makes the termination more involved.

  We allow inprocessing, but restrict it a lot. We could allow anything such that the invariants
  are still fulfilled afterwards, but we currently restrict to be some CDCL steps (TODO: generalise
  to also include restarts) and add requirements on the output.

  There is a second termination condition that is not included here, namely UNSAT by inprocessing.
  We decided against including because it breaks the termination argument and makes expressing the
  relation between the elements of the state much more complicated without helping at all. At the
  end, we talk about conclusive states anyway.
›
type_synonym 'v twl_st_restart = ‹'v twl_st × 'v twl_st × 'v twl_st × nat × nat × bool›
inductive cdcl_twl_stgy_restart :: ‹'v twl_st_restart ⇒ 'v twl_st_restart  ⇒ bool› where
step:
 ‹cdcl_twl_stgy_restart (R, S, T, m, n, True) (R, S, U, m, n, True)›
 if
   ‹cdcl_twl_stgy T U› |
restart_step:
  ‹cdcl_twl_stgy_restart (R, S, T, m, n, True) (W, W, W, m, Suc n, True)›
  if
    ‹size (get_all_learned_clss T) - size (get_all_learned_clss R) > f n› and
    ‹cdcl_twl_inp** T U› and
    ‹cdcl_twl_stgy** U W›
    ‹clauses_to_update W = {#}›
    ‹get_conflict W ≠ None ⟶ count_decided (get_trail W) = 0› |
restart_noGC:
  ‹cdcl_twl_stgy_restart (R, S, T, m, n, True) (R, U, U, Suc m, n, True)›
  if
    ‹size (get_all_learned_clss T) > size (get_all_learned_clss S)› and
    ‹cdcl_twl_restart_only T U› |
restart_full:
 ‹cdcl_twl_stgy_restart (R, S, T, m, n, True) (R, S, T, m, n, False)›
 if
   ‹pcdcl_twl_final_state T›


lemma cdcl_twl_stgy_restart_induct[consumes 1, case_names restart_step restart_noGC full]:
  assumes
    ‹cdcl_twl_stgy_restart (R, S, T, m, n, b) (R', S', T', m', n', b')› and
    ‹⋀R S T U. cdcl_twl_stgy T U ⟹ m' = m ⟹ n' = n ⟹ b ⟹ b' ⟹  P R S T m n True R S U m n True› and
    ‹⋀R S T U V W.
      f n < size (get_all_learned_clss T) - size (get_all_learned_clss R) ⟹ cdcl_twl_inp** T U ⟹  cdcl_twl_stgy** U W ⟹
     clauses_to_update W = {#} ⟹ (get_conflict W ≠ None ⟹ count_decided (get_trail W) = 0) ⟹
      m' = m ⟹ n' = Suc n ⟹
      P R S T m n True W W W m (Suc n) True›and
    ‹⋀R S T U.
      size (get_all_learned_clss T) > size (get_all_learned_clss S) ⟹
      cdcl_twl_restart_only T U ⟹ m' = Suc m ⟹ n' = n ⟹
    P R S T m n True R U U (Suc m) n True›
    ‹pcdcl_twl_final_state T ⟹ R' = R ⟹ S' = S ⟹ T' = T ⟹ P R S T m n True R S T m n False›
  shows ‹P R S T m n b R' S' T' m' n' b'›
  using assms(1)
  apply (cases rule: cdcl_twl_stgy_restart.cases)
  subgoal
    using assms(2)[of T T' R S]
    by simp
  subgoal for U
    using assms(3)[of ]
    by simp
  subgoal
    using assms(4)[of ]
    by simp
  subgoal
    using assms(5)[of ]
    by simp
  done


lemma tranclp_cdcl_twl_stgy_cdclW_stgy2:
  ‹cdcl_twl_stgy++ S T ⟹
  twl_struct_invs S ⟹ (pstateW_of S) ≠ (pstateW_of T) ⟹
  pcdcl_tcore_stgy++ (pstateW_of S) (pstateW_of T)›
  using rtranclp_cdcl_twl_stgy_cdclW_stgy[of S T] unfolding rtranclp_unfold
  by auto

lemma tranclp_cdcl_twl_stgy_cdclW_stgy3:
  ‹cdcl_twl_stgy++ S T ⟹
  size (get_all_learned_clss T) > size (get_all_learned_clss S) ⟹
  twl_struct_invs S ⟹
  pcdcl_tcore_stgy++ (pstateW_of S) (pstateW_of T)›
  using rtranclp_cdcl_twl_stgy_cdclW_stgy[of S T] unfolding rtranclp_unfold
  apply auto
  apply (cases T; cases S)
  apply (auto simp: clauses_def dest!: arg_cong[of ‹clauses _› _ size])
  done

lemma [twl_st, simp]:
  ‹pget_all_learned_clss (pstateW_of T) = get_all_learned_clss T›
  ‹pget_conflict (pstateW_of T) = get_conflict T›
  by (cases T; auto; fail)+

lemma pcdcl_twl_final_state_pcdcl:
  ‹pcdcl_twl_final_state S ⟹
  twl_struct_invs S ⟹ pcdcl_final_state (pstateW_of S)›
  using no_step_cdcl_twl_stgy_no_step_cdclW_stgy[of S]
  unfolding pcdcl_twl_final_state_def pcdcl_final_state_def
  by (auto simp add: no_step_pcdcl_core_stgy_pcdcl_coreD)

lemma pcdcl_stgy_restart_stepI:
  ‹pcdcl_tcore_stgy** T T' ⟹ pcdcl_stgy_restart** (R, S, T, m, n, True) (R, S, T', m, n, True)›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for V W
    by (auto dest!: pcdcl_stgy_restart.intros(1)[of _ _ R S m n])
  done

(* TODO deduplicate*)
lemma rtranclp_cdcl_twl_inp_pcdcl_inprocessing:
  ‹cdcl_twl_inp** S T ⟹ twl_struct_invs S ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S) ⟹
  pcdcl_inprocessing** (pstateW_of S) (pstateW_of T)›
  by (drule rtranclp_cdcl_twl_inp_pcdcl; assumption?)

lemma cdcl_twl_stgy_restart_pcdcl:
  ‹cdcl_twl_stgy_restart (R, S :: 'v twl_st, T, m, n, g) (R', S', T', m', n', h) ⟹
  twl_struct_invs R ⟹ twl_struct_invs S ⟹ twl_struct_invs T ⟹ cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of T) ⟹
  pcdcl_stgy_restart** (pstateW_of R, pstateW_of S, pstateW_of T, m, n, g)
      (pstateW_of R', pstateW_of S', pstateW_of T', m', n', h)›
  apply (induction rule: cdcl_twl_stgy_restart_induct)
  subgoal for R S T U
    by (drule cdcl_twl_stgy_cdclW_stgy)
      (simp add: pcdcl_stgy_restart_stepI)+
  subgoal
    apply (rule r_into_rtranclp)
    apply (rule pcdcl_stgy_restart.intros(2))
    apply simp
    apply (rule rtranclp_cdcl_twl_inp_pcdcl_inprocessing; assumption)
    using cdcl_twl_restart_twl_struct_invs rtranclp_cdcl_twl_stgy_cdclW_stgy rtranclp_pcdcl_tcore_stgy_pcdcl_stgy'
    apply (simp_all add: cdcl_twl_restart_twl_struct_invs rtranclp_cdcl_twl_stgy_cdclW_stgy
      rtranclp_pcdcl_tcore_stgy_pcdcl_stgy' rtranclp_cdcl_twl_inp_twl_struct_invs)
    apply (smt cdcl_twl_restart_pcdcl pcdcl_restart_no_smaller_propa' rtranclp_cdcl_twl_inp_twl_struct_invs stateW_of_def twl_struct_invs_def)
    done
  subgoal
    apply (rule r_into_rtranclp)
    apply (rule pcdcl_stgy_restart.intros(3))
    apply simp
    apply (rule cdcl_twl_restart_only_cdcl, assumption)
    done
  subgoal
    apply (rule r_into_rtranclp)
    apply (rule pcdcl_stgy_restart.intros(4))
    by (simp add: twl_restart_ops.pcdcl_twl_final_state_pcdcl)
  done


lemma cdcl_twl_stgy_restart_twl_struct_invs:
  assumes
    ‹cdcl_twl_stgy_restart S T› and
    ‹twl_struct_invs (fst S)› and
    ‹twl_struct_invs (fst (snd S))› and
    ‹twl_struct_invs (fst (snd (snd S)))› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of  (fst (snd (snd S))))›
  shows ‹twl_struct_invs (fst T) ∧ twl_struct_invs (fst (snd T)) ∧ twl_struct_invs (fst (snd (snd T)))›
  using assms
  by (induction rule: cdcl_twl_stgy_restart.induct)
  (auto simp add: full1_def intro: rtranclp_cdcl_twl_stgy_twl_struct_invs
      dest: cdcl_twl_restart_twl_struct_invs rtranclp_cdcl_twl_stgy_twl_stgy_invs
      rtranclp_cdcl_twl_stgy_twl_struct_invs
   cdcl_twl_restart_only_twl_struct_invs
   simp:
     cdcl_twl_restart_twl_struct_invs rtranclp_cdcl_twl_inp_twl_struct_invs
     rtranclp_cdcl_twl_stgy_twl_struct_invs rtranclp_cdcl_twl_inp_twl_struct_invs
   dest!: tranclp_into_rtranclp intro: rtranclp_cdcl_twl_inp_twl_struct_invs)

lemma pcdcl_restart_entailed_by_init:
  assumes ‹pcdcl_restart S T› and
    ‹pcdcl_all_struct_invs S› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S)›
  shows ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of T)›
  using assms
  apply (induction rule: pcdcl_restart.induct)
  subgoal
    by (auto simp: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def
      subset_mset.le_iff_add ac_simps intro: true_clss_clss_subset_entailedI)
  subgoal
    by (auto simp: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def
      subset_mset.le_iff_add ac_simps intro: true_clss_clss_subset_entailedI)
  done

lemma pcdcl_restart_only_entailed_by_init:
  assumes ‹pcdcl_restart_only S T› and
    ‹pcdcl_all_struct_invs S› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S)›
  shows ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of T)›
  using assms
  apply (induction rule: pcdcl_restart_only.induct)
  subgoal
    by (auto simp: cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def
      subset_mset.le_iff_add ac_simps)
  done


lemma cdcl_twl_stgy_restart_entailed_by_init:
  assumes
    ‹cdcl_twl_stgy_restart S T› and
    ‹twl_struct_invs (fst S)› and
    ‹twl_struct_invs (fst (snd S))› and
    ‹twl_struct_invs (fst (snd (snd S)))› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of (fst S))› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of (fst (snd S)))› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of (fst (snd (snd S))))›
  shows ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of (fst T)) ∧
    cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of (fst (snd T))) ∧
    cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of (fst (snd (snd T))))›
  using assms
  apply (induction rule: cdcl_twl_stgy_restart.induct)
  subgoal apply simp
    using cdcl_twl_stgy_cdclW_stgy rtranclp_pcdcl_entailed_by_init rtranclp_pcdcl_stgy_pcdcl
      rtranclp_pcdcl_tcore_stgy_pcdcl_stgy' twl_struct_invs_def by blast
    subgoal apply simp
      by (metis (mono_tags, lifting) cdcl_twl_inp.intros(5) rtranclp.rtrancl_into_rtrancl
        rtranclp_cdcl_twl_stgy_cdclW_stgy rtranclp_cdcl_twl_inp_entailed_init
        rtranclp_cdcl_twl_inp_twl_struct_invs rtranclp_pcdcl_entailed_by_init
        rtranclp_pcdcl_stgy_pcdcl rtranclp_pcdcl_tcore_stgy_pcdcl_stgy' stateW_of_def
        twl_struct_invs_def)
    subgoal apply simp
      using cdcl_twl_restart_only_cdcl twl_restart_ops.pcdcl_restart_only_entailed_by_init
        twl_struct_invs_def by blast
    subgoal
      by simp
    done

lemma rtranclp_cdcl_twl_stgy_restart_twl_struct_invs:
  assumes
    ‹cdcl_twl_stgy_restart** S T› and
    ‹twl_struct_invs (fst S)› and
    ‹twl_struct_invs (fst (snd S))› and
    ‹twl_struct_invs (fst (snd (snd S)))› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of (fst S))› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of (fst (snd S)))› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of (fst (snd (snd S))))›
  shows ‹twl_struct_invs (fst T) ∧ twl_struct_invs (fst (snd T)) ∧ twl_struct_invs (fst (snd (snd T))) ∧
    cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of (fst T)) ∧
    cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of (fst (snd T))) ∧
    cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of (fst (snd (snd T))))›
  using assms
  apply (induction)
  subgoal by auto
  subgoal for T U
    using cdcl_twl_stgy_restart_entailed_by_init[of T U] cdcl_twl_stgy_restart_twl_struct_invs[of T U]
    by simp
  done

lemma rtranclp_cdcl_twl_stgy_restart_pcdcl:
  ‹cdcl_twl_stgy_restart** (R, S :: 'v twl_st, T, m, n, g) (R', S', T', m', n', h) ⟹
  twl_struct_invs R ⟹ twl_struct_invs S ⟹ twl_struct_invs T ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of R) ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S) ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of T) ⟹
  pcdcl_stgy_restart** (pstateW_of R, pstateW_of S, pstateW_of T, m, n, g)
      (pstateW_of R', pstateW_of S', pstateW_of T', m', n', h)›
  apply (induction rule: rtranclp_induct[of r ‹(_, _, _, _, _, _)› ‹(_, _, _, _, _, _)›, split_format(complete), of for r])
  subgoal by auto
  subgoal for R' S' T' m' n' g' R'' S'' T'' m'' n'' g''
    using rtranclp_cdcl_twl_stgy_restart_twl_struct_invs[of ‹(R, S, T, m, n, g)› ‹(R', S', T', m', n', g')›]
    by (auto dest: cdcl_twl_stgy_restart_pcdcl)
  done

lemma cdcl_twl_stgy_cdclW_stgy_restart2:
  assumes ‹cdcl_twl_stgy_restart (S, T, U, m, n, g) (S', T', U', m', n', g')›
    and twl: ‹twl_struct_invs U› and ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of U)›
  shows ‹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 = 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)›
  using assms(1,2,3)
  apply (induction rule: cdcl_twl_stgy_restart_induct)
  subgoal for R S T U
    by (drule  cdcl_twl_stgy_cdclW_stgy2)
      (auto simp add: pcdcl_stgy_restart.step)
  subgoal
    apply (rule disjI1)
    apply (rule pcdcl_stgy_restart.intros(2))
    apply simp
    apply (rule rtranclp_cdcl_twl_inp_pcdcl_inprocessing)
    apply assumption+
    using cdcl_twl_restart_twl_struct_invs rtranclp_cdcl_twl_stgy_cdclW_stgy rtranclp_pcdcl_tcore_stgy_pcdcl_stgy'
    apply (simp_all add: cdcl_twl_restart_twl_struct_invs rtranclp_cdcl_twl_stgy_cdclW_stgy
      rtranclp_pcdcl_tcore_stgy_pcdcl_stgy' rtranclp_cdcl_twl_inp_twl_struct_invs)
    by (smt cdcl_twl_restart_pcdcl pcdcl_restart_no_smaller_propa' rtranclp_cdcl_twl_inp_twl_struct_invs stateW_of_def twl_struct_invs_def)
  subgoal
    apply (rule disjI1)
    apply (rule pcdcl_stgy_restart.intros(3))
    apply simp
    apply (rule cdcl_twl_restart_only_cdcl, assumption)
    done
  subgoal
    apply (rule disjI1)
    apply (rule pcdcl_stgy_restart.intros(4))
    by (simp add: twl_restart_ops.pcdcl_twl_final_state_pcdcl)
  done

abbreviation stateW_of_restart where
  ‹stateW_of_restart ≡ (λ(S, T, U, n, b). (stateW_of S, stateW_of T, stateW_of U, n))›

definition twl_restart_inv :: ‹'v twl_st_restart ⇒ bool› where
  ‹twl_restart_inv = (λ(Q, R, S, m, n). twl_struct_invs Q ∧ twl_struct_invs R ∧ twl_struct_invs S ∧
   cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of Q) ∧
   cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of R) ∧
   cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S) ∧
   pcdcl_stgy_restart_inv (pstateW_of Q, pstateW_of R, pstateW_of S, m, n))›

lemma cdcl_twl_stgy_entailed_by_init:
  ‹cdcl_twl_stgy S T ⟹ twl_struct_invs S ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S) ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of T)›
  apply (induction rule: cdcl_twl_stgy.induct)
  apply (metis cdcl_twl_stgy_cdclW_stgy cp rtranclp_pcdcl_entailed_by_init rtranclp_pcdcl_stgy_pcdcl rtranclp_pcdcl_tcore_stgy_pcdcl_stgy' stateW_of_def twl_struct_invs_def)
  by (metis cdcl_twl_o_cdclW_o_stgy pcdcl_tcore_pcdcl pcdcl_tcore_stgy_pcdcl_tcoreD rtranclp_pcdcl_entailed_by_init stateW_of_def twl_struct_invs_def)

lemma rtranclp_cdcl_twl_stgy_entailed_by_init:
  ‹cdcl_twl_stgy** S T ⟹ twl_struct_invs S ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of S) ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of T)›
  apply (induction rule: rtranclp_induct)
  apply auto[]
  using rtranclp_cdcl_twl_stgy_twl_struct_invs twl_restart_ops.cdcl_twl_stgy_entailed_by_init by blast

lemma cdcl_twl_stgy_restart_twl_restart_inv:
  ‹cdcl_twl_stgy_restart S T ⟹ twl_restart_inv S ⟹ twl_restart_inv T›
  apply (induction rule: cdcl_twl_stgy_restart.induct)
  subgoal for T U R S m n
    using cdcl_twl_stgy_cdclW_stgy_restart2[of R S T m n True R S U m n True]
    unfolding twl_restart_inv_def
    apply (auto intro: cdcl_twl_stgy_twl_struct_invs
      simp: pcdcl_stgy_restart_pcdcl_stgy_restart_inv cdcl_twl_stgy_restart.intros)
    using cdcl_twl_stgy_cdclW_stgy rtranclp_pcdcl_entailed_by_init rtranclp_pcdcl_stgy_pcdcl
      rtranclp_pcdcl_tcore_stgy_pcdcl_stgy' unfolding twl_struct_invs_def by blast
  subgoal for T R n U W S m
    using cdcl_twl_stgy_cdclW_stgy_restart2[of R S T m n True W W W m ‹Suc n› True]
    unfolding twl_restart_inv_def
    apply (auto intro: cdcl_twl_stgy_twl_struct_invs
      simp: pcdcl_stgy_restart_pcdcl_stgy_restart_inv cdcl_twl_stgy_restart.intros
      cdcl_twl_restart_twl_struct_invs rtranclp_cdcl_twl_stgy_twl_struct_invs
      rtranclp_cdcl_twl_inp_twl_struct_invs rtranclp_pcdcl_all_struct_invs
      rtranclp_pcdcl_entailed_by_init pcdcl_restart_entailed_by_init
      intro: pcdcl_restart_entailed_by_init rtranclp_pcdcl_entailed_by_init
      dest: rtranclp_cdcl_twl_inp_pcdcl cdcl_twl_restart_pcdcl)
    apply (metis cdcl_twl_restart_twl_struct_invs cdcl_twl_inp.intros(5)
      cdcl_twl_inp_invs(3) rtranclp_cdcl_twl_inp_entailed_init
      rtranclp_cdcl_twl_inp_twl_struct_invs stateW_of_def
      rtranclp_cdcl_twl_stgy_entailed_by_init)
    by (metis cdcl_twl_restart_twl_struct_invs cdcl_twl_inp.intros(5)
      cdcl_twl_inp_invs(3) rtranclp_cdcl_twl_inp_entailed_init
      rtranclp_cdcl_twl_inp_twl_struct_invs stateW_of_def
      rtranclp_cdcl_twl_stgy_entailed_by_init)
  subgoal for T S U R m n
    using cdcl_twl_stgy_cdclW_stgy_restart2[of R S T m n True R U U ‹Suc m› n True]
    unfolding twl_restart_inv_def
    apply (auto intro: cdcl_twl_stgy_twl_struct_invs
      simp: pcdcl_stgy_restart_pcdcl_stgy_restart_inv cdcl_twl_stgy_restart.intros
      cdcl_twl_restart_only_twl_struct_invs)
      using cdcl_twl_restart_only_cdcl twl_restart_ops.pcdcl_restart_only_entailed_by_init twl_struct_invs_def by blast
  subgoal
    unfolding twl_restart_inv_def pcdcl_stgy_restart_inv_def prod.simps by blast
  done

lemma rtranclp_cdcl_twl_stgy_restart_twl_restart_inv:
  ‹cdcl_twl_stgy_restart** S T ⟹ twl_restart_inv S ⟹ twl_restart_inv T›
  by (induction rule: rtranclp_induct)
    (auto simp: cdcl_twl_stgy_restart_twl_restart_inv)

definition twl_stgy_restart_inv :: ‹'v twl_st_restart ⇒ bool› where
  ‹twl_stgy_restart_inv = (λ(Q, R, S, m, n). twl_stgy_invs Q ∧ twl_stgy_invs R ∧ twl_stgy_invs S)›
lemma cdcl_twl_restart_only_twl_stgy_invs:
  ‹cdcl_twl_restart_only S T ⟹ twl_stgy_invs S ⟹ twl_stgy_invs T›
  by (auto simp: cdcl_twl_restart_only.simps twl_stgy_invs_def
    cdclW_restart_mset.cdclW_stgy_invariant_def cdclW_restart_mset.no_smaller_confl_def
    cdclW_restart_mset.conflict_non_zero_unless_level_0_def
    dest!: get_all_ann_decomposition_exists_prepend)

lemma cdcl_twl_stgy_restart_twl_stgy_invs:
  assumes
    ‹cdcl_twl_stgy_restart S T› and
    ‹twl_restart_inv S› and
    ‹twl_stgy_invs (fst S)› and
    ‹twl_stgy_invs (fst (snd S))› and
    ‹twl_stgy_invs (fst (snd (snd S)))›and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of (fst S))› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of (fst (snd S)))› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (stateW_of (fst (snd (snd S))))›
  shows ‹twl_stgy_invs (fst T) ∧ twl_stgy_invs (fst (snd T)) ∧ twl_stgy_invs (fst (snd (snd T)))›
  using assms
  apply (induction rule: cdcl_twl_stgy_restart.induct)
  subgoal for T U R S m n
    using rtranclp_cdcl_twl_stgy_twl_stgy_invs[of T U]
    by (auto simp: twl_restart_inv_def)
  subgoal for T R n U W S m
    using cdcl_twl_restart_twl_stgy_invs[of U V]
    by (auto simp: twl_restart_inv_def rtranclp_cdcl_twl_inp_twl_stgy_invs
        cdcl_twl_restart_twl_struct_invs rtranclp_cdcl_twl_stgy_twl_stgy_invs
        rtranclp_cdcl_twl_inp_twl_struct_invs
      intro: cdcl_twl_restart_twl_struct_invs rtranclp_cdcl_twl_stgy_twl_stgy_invs)
  subgoal for T S U R m n
    using cdcl_twl_restart_only_twl_stgy_invs[of T U]
    by (auto simp: twl_restart_inv_def)
  subgoal
    by auto
  done

lemma rtranclp_cdcl_twl_stgy_restart_twl_stgy_invs:
  assumes
    ‹cdcl_twl_stgy_restart** S T› and
    ‹twl_restart_inv S› and
    ‹twl_stgy_invs (fst S)› and
    ‹twl_stgy_invs (fst (snd S))› and
    ‹twl_stgy_invs (fst (snd (snd S)))›
  shows ‹twl_stgy_invs (fst T) ∧ twl_stgy_invs (fst (snd T)) ∧ twl_stgy_invs (fst (snd (snd T)))›
  using assms
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using cdcl_twl_stgy_restart_twl_stgy_invs[of T U]
      rtranclp_cdcl_twl_stgy_restart_twl_restart_inv[of S T]
    by (auto dest!: simp: twl_restart_inv_def)
  done

lemma cdcl_twl_stgy_restart_twl_stgy_restart_inv:
  ‹cdcl_twl_stgy_restart S T ⟹ twl_restart_inv S ⟹ twl_stgy_restart_inv S ⟹
  twl_stgy_restart_inv T›
  using cdcl_twl_stgy_restart_twl_stgy_invs[of S T] unfolding twl_stgy_restart_inv_def twl_restart_inv_def
  by auto

lemma rtranclp_cdcl_twl_stgy_restart_twl_stgy_restart_inv:
  ‹cdcl_twl_stgy_restart** S T ⟹ twl_restart_inv S ⟹ twl_stgy_restart_inv S ⟹
  twl_stgy_restart_inv T›
  using rtranclp_cdcl_twl_stgy_restart_twl_stgy_invs[of S T] unfolding twl_stgy_restart_inv_def
  by auto

lemma cdclW_ex_cdclW_stgy:
  ‹cdclW_restart_mset.cdclW S T ⟹ ∃U. cdclW_restart_mset.cdclW_stgy S U›
  by (meson cdclW_restart_mset.cdclW.cases cdclW_restart_mset.cdclW_stgy.simps)

lemma rtranclp_cdclW_cdclW_init_state:
  ‹cdclW_restart_mset.cdclW** (init_state {#}) S ⟷ S = init_state {#}›
  unfolding rtranclp_unfold
  by (subst tranclp_unfold_begin)
    (auto simp: cdclW_stgy_cdclW_init_state_empty_no_step
       cdclW_stgy_cdclW_init_state
      simp del: init_state.simps
       dest: cdclW_restart_mset.cdclW_stgy_cdclW cdclW_ex_cdclW_stgy)

lemma rtranclp_pcdcl_core_is_cdcl:
  ‹pcdcl_core** S T ⟹ cdclW_restart_mset.cdclW** (state_of S) (state_of T)›
  by (induction rule: rtranclp.induct)
    (auto dest: pcdcl_core_is_cdcl)

lemma pcdcl_tcore_is_cdclD:
  ‹pcdcl_tcore T T' ⟹
    cdclW_restart_mset.cdclW_restart** (state_of T) (state_of T')›
  by (induction rule: pcdcl_tcore.induct)
    (auto intro: pcdcl_restart.intros dest!: pcdcl_core_is_cdcl
      cdclW_restart_mset.cdclW_cdclW_restart pcdcl_tcore_stgy_pcdcl_tcoreD
      state_of_cdcl_subsumed cdcl_flush_unit_unchanged
      cdcl_backtrack_unit_is_CDCL_backtrack)

lemma rtranclp_pcdcl_entailed_by_init:
  assumes ‹pcdcl** S T› and
    ‹pcdcl_all_struct_invs S› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S)›
  shows ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of T)›
  using assms
  by (induction rule: rtranclp_induct)
   (auto dest!: pcdcl_entailed_by_init
    intro: rtranclp_pcdcl_all_struct_invs)

lemma pcdcl_inprocessing_entailed_by_init:
  ‹pcdcl_inprocessing S T ⟹ pcdcl_all_struct_invs S ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S) ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of T)›
  apply (induction rule: pcdcl_inprocessing.induct)
  subgoal for S T
    using pcdcl_entailed_by_init[of S T] by auto
  subgoal
    using pcdcl_restart_entailed_by_init by blast
  done

lemma rtranclp_pcdcl_inprocessing_entailed_by_init:
  ‹pcdcl_inprocessing** S T ⟹ pcdcl_all_struct_invs S ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S) ⟹
  cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of T)›
  apply (induction rule: rtranclp_induct)
  subgoal
    by auto
  subgoal for T U
    using pcdcl_inprocessing_entailed_by_init[of T U] rtranclp_pcdcl_inprocessing_pcdcl_all_struct_invs[of S T]
    by blast
  done

lemma pcdcl_stgy_restart_entailed_by_init:
  fixes g g'
  assumes ‹pcdcl_stgy_restart (R1, R2, S, m, n, g) (R1', R2', T, m', n', g')› and
    ‹pcdcl_all_struct_invs S› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S)›
  shows ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of T)›
  using assms
  apply (induction ‹(R1, R2, S, m, n, g)› ‹(R1', R2', T, m', n', g')› rule: pcdcl_stgy_restart.induct)
  subgoal
    using pcdcl_tcore_stgy_pcdcl_stgy' rtranclp_pcdcl_entailed_by_init rtranclp_pcdcl_stgy_pcdcl
    by blast
  subgoal for U
    using pcdcl_restart_entailed_by_init[of U R1'] pcdcl_restart_pcdcl_all_struct_invs[of S U]
      rtranclp_pcdcl_inprocessing_pcdcl_all_struct_invs[of S U]
      rtranclp_pcdcl_inprocessing_entailed_by_init[of S U]
    by (auto dest!: pcdcl_tcore_stgy_pcdcl_stgy' rtranclp_pcdcl_entailed_by_init
      rtranclp_pcdcl_stgy_pcdcl
      dest: pcdcl_restart_pcdcl_all_struct_invs)
  subgoal
    using pcdcl_restart_only_entailed_by_init[of S U]
    by (auto dest!: pcdcl_tcore_stgy_pcdcl_stgy' rtranclp_pcdcl_entailed_by_init
      rtranclp_pcdcl_stgy_pcdcl
      dest: pcdcl_restart_only_entailed_by_init)
  subgoal
    by auto
  done

lemma pcdcl_stgy_restart_pcdcl_all_struct_invs:
  assumes ‹pcdcl_stgy_restart (R1, R2, S, m, n, g) (R1', R2', T, m', n', g')› and
    ‹pcdcl_all_struct_invs S›
  shows ‹pcdcl_all_struct_invs T›
  using assms
  apply (induction ‹(R1, R2, S, m, n, g)› ‹(R1', R2', T, m', n', g')› rule: pcdcl_stgy_restart.induct)
  apply (simp_all add: pcdcl_tcore_stgy_all_struct_invs pcdcl_restart_pcdcl_all_struct_invs
    rtranclp_pcdcl_all_struct_invs rtranclp_pcdcl_stgy_pcdcl)
  using pcdcl_restart_pcdcl_all_struct_invs rtranclp_pcdcl_all_struct_invs rtranclp_pcdcl_stgy_pcdcl
    rtranclp_pcdcl_inprocessing_pcdcl_all_struct_invs apply blast
  using pcdcl_restart_only_pcdcl_all_struct_invs by blast

lemma rtranclp_pcdcl_stgy_restart_pcdcl_all_struct_invs:
  assumes ‹pcdcl_stgy_restart** (R1, R2, S, m, n, g) (R1', R2', T, m', n', g')› and
    ‹pcdcl_all_struct_invs S›
  shows ‹pcdcl_all_struct_invs T›
  using assms
  by (induction rule: rtranclp_induct[of r ‹(_, _, _, _, _, _)› ‹(_, _, _, _, _, _)›, split_format(complete), of for r])
    (auto dest!: pcdcl_stgy_restart_pcdcl_all_struct_invs)

lemma rtranclp_pcdcl_stgy_restart_entailed_by_init:
  assumes ‹pcdcl_stgy_restart** (R1, R2, S, m, n, g) (R1', R2', T, m', n', g')› and
    ‹pcdcl_all_struct_invs S› and
    ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S)›
  shows ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of T)›
  using assms
  by (induction rule: rtranclp_induct[of r ‹(_, _, _, _, _, _)› ‹(_, _, _, _, _, _)›, split_format(complete), of for r])
   (auto dest!: pcdcl_stgy_restart_entailed_by_init rtranclp_pcdcl_stgy_restart_pcdcl_all_struct_invs)

lemma pcdcl_core_entailed_iff:
  ‹pcdcl_core S T ⟹ M ⊨m pget_all_init_clss T ⟷ M ⊨m pget_all_init_clss S›
  by (induction rule: pcdcl_core.induct)
   (auto simp: cdcl_conflict.simps cdcl_propagate.simps cdcl_skip.simps
    cdcl_decide.simps cdcl_resolve.simps cdcl_backtrack.simps)

lemma pcdcl_entailed_iff:
  ‹pcdcl S T ⟹ consistent_interp M ⟹
  total_over_set M (atms_of_mm (pget_all_init_clss T)) ⟹
    cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S) ⟹
    M ⊨m pget_all_init_clss T ⟹ M ⊨m pget_all_init_clss S›
  apply (induction rule: pcdcl.induct)
  subgoal
    by (auto simp: pcdcl_core_entailed_iff)
  subgoal
    by (auto simp: cdcl_learn_clause.simps true_clss_cls_def total_over_m_def
      cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def
      dest: spec[of _ M])
  subgoal
    by (auto simp: cdcl_resolution.simps total_over_m_def consistent_interp_def)
  subgoal
    by (auto simp: cdcl_subsumed.simps)
  subgoal
    by (auto simp: cdcl_flush_unit.simps)
  subgoal
    by (auto simp: cdcl_inp_propagate.simps)
  subgoal
    by (auto simp: cdcl_inp_conflict.simps)
  subgoal
    by (auto simp: cdcl_unitres_true.simps)
  subgoal
    by (auto simp: cdcl_promote_false.simps)
  subgoal
    by (auto simp: cdcl_pure_literal_remove.simps)
  done

lemma cdcl_pure_literal_remove_satisfiable_iff:
  assumes
    ‹cdcl_pure_literal_remove S T› and
    ‹pcdcl_all_struct_invs S› and
    ent_init: ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S)›
  shows
    ‹satisfiable (set_mset (pget_all_init_clss S)) ⟷ satisfiable (set_mset (pget_all_init_clss T))›
  using assms(1)
proof (cases)
  case (cdcl_pure_literal_remove L N NE NS N0 M U UE US U0) note S = this(1) and T = this(2) and
    L = this(3,4) and undef = this(5) and lev0 = this(6)
  have
    ent: ‹entailed_clss_inv S› and
    sub: ‹psubsumed_invs S› and
    clss0: ‹clauses0_inv S› and
    struct_invs: ‹cdclW_restart_mset.cdclW_all_struct_inv (state_of S)›
    using assms(2) unfolding pcdcl_all_struct_invs_def by fast+
  show ?thesis (is ‹?A ⟷ ?B›)
  proof
    assume ?B
    then show ?A
      by (auto simp: S T satisfiable_carac[symmetric])
  next
    assume ?A
    then obtain I where
      cons: ‹consistent_interp I› and
      IS: ‹I ⊨sm pget_all_init_clss S› and
      tot: ‹total_over_m I (set_mset (pget_all_init_clss S))›
      unfolding satisfiable_def by blast
    let ?J = ‹insert L (I - {-L})›
    have cons2: ‹consistent_interp ?J›
      using cons
      by (metis Diff_empty Diff_iff Diff_insert0 consistent_interp_insert_iff insert_Diff singletonI)

    have ‹all_decomposition_implies_m (cdclW_restart_mset.clauses (state_of S))
      (get_all_ann_decomposition (trail (state_of S)))› and
      alien: ‹cdclW_restart_mset.no_strange_atm (state_of S)›
      using struct_invs unfolding cdclW_restart_mset.cdclW_all_struct_inv_def by fast+
    moreover have ‹set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0 ⊨ps
      (set_mset U ∪ set_mset UE ∪ set_mset US ∪ set_mset U0)›
      using ent_init by (auto simp: S cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def)
    ultimately have ‹set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0 ⊨ps unmark_l M›
      using tot lev0 by (auto simp: S clauses_def count_decided_0_iff
        no_decision_get_all_ann_decomposition)
        (metis true_clss_clss_left_right true_clss_clss_union_and)
    moreover have ‹total_over_m I (unmark_l M)›
      using alien tot by (auto simp: cdclW_restart_mset.no_strange_atm_def S
        total_over_m_def total_over_set_def)
    ultimately have ‹I ⊨s unmark_l M›
      using IS tot cons by (auto simp: S true_clss_clss_def)
    then have ‹lits_of_l M ⊆ I›
      by (auto simp: true_clss_def lits_of_def)

    have IN: ‹I ⊨m N› and ‹I ⊨m NS› ‹I ⊨m N0› ‹I ⊨m NE›
      using IS by (auto simp: S)
    have totJ: ‹total_over_m ?J (set_mset (pget_all_init_clss T))›
      using tot apply (auto simp: total_over_m_def S T total_over_set_alt_def
        uminus_lit_swap)
      apply (metis atm_of_uminus literal.sel)+
      done
    have ‹?J ⊨m N›
      using IN L by (clarsimp simp: true_cls_mset_def add_mset_eq_add_mset true_cls_def
        dest!: multi_member_split)
    moreover have ‹?J ⊨m NE›
        using ‹I ⊨m NS› ent ‹I ⊨m N0› ‹I ⊨m NE› totJ L(1) undef ‹lits_of_l M ⊆ I›
        apply (auto simp: entailed_clss_inv_def S true_cls_mset_def T Decided_Propagated_in_iff_in_lits_of_l
          dest!: multi_member_split[of ‹_ :: _ clause›])
       unfolding true_cls_def[of ]
       apply clarsimp
       apply (rule_tac x=La in bexI)
       by auto
    moreover have ‹?J ⊨m N0›
      using ‹I ⊨m NS› ent ‹I ⊨m N0› ‹I ⊨m NE› totJ L undef clss0
      by (auto simp: entailed_clss_inv_def S true_cls_mset_def T Decided_Propagated_in_iff_in_lits_of_l
        clauses0_inv_def
        dest!: multi_member_split)
    moreover have ‹?J ⊨m NS›
      using ‹I ⊨m NS› sub ‹I ⊨m N0› ‹I ⊨m N› totJ calculation
      apply (auto simp: psubsumed_invs_def S true_cls_mset_def T
        dest!: multi_member_split dest: true_cls_mono_leD)
      apply (simp add: tautology_def)
      apply (metis calculation true_cls_mono_leD true_cls_mset_add_mset)+
      done
    ultimately have ‹?J ⊨sm pget_all_init_clss T›
      using ent by (auto simp: S T)
    then show ?B
      using cons2 by auto
  qed
qed

lemma pcdcl_core_same_init_vars:
  ‹pcdcl_core S T ⟹ atms_of_mm (pget_all_init_clss S) = atms_of_mm (pget_all_init_clss T)›
  by (induction rule: pcdcl_core.induct)
   (auto simp: cdcl_conflict.simps cdcl_propagate.simps cdcl_skip.simps
    cdcl_decide.simps cdcl_resolve.simps cdcl_backtrack.simps)

lemma pcdcl_restart_same_init_vars:
  ‹pcdcl_restart S T ⟹ atms_of_mm (pget_all_init_clss S) = atms_of_mm (pget_all_init_clss T)›
  by (induction rule: pcdcl_restart.induct) auto

lemma pcdcl_restart_only_same_init_vars:
  ‹pcdcl_restart_only S T ⟹ atms_of_mm (pget_all_init_clss S) = atms_of_mm (pget_all_init_clss T)›
  by (induction rule: pcdcl_restart_only.induct) auto

lemma pcdcl_satisfiable_iff:
  assumes
    ‹pcdcl S T› and
    ‹pcdcl_all_struct_invs S› and
    ent_init: ‹cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S)›
  shows
    ‹satisfiable (set_mset (pget_all_init_clss S)) ⟷ satisfiable (set_mset (pget_all_init_clss T))›
    (is ‹?A ⟷ ?B›)
  using assms pcdcl_pget_all_init_clss[OF assms(1)]
proof -
  have atms_eq: ‹atms_of_mm (pget_all_init_clss S) = atms_of_mm (pget_all_init_clss T)›
    by (rule pcdcl_pget_all_init_clss[OF assms(1)])
      (use assms(2) in ‹auto simp: pcdcl_all_struct_invs_def›)
  show ?thesis
  proof
    assume ?B
    with assms show ?A
      using atms_eq
      by (induction rule: pcdcl.induct)
        (auto simp: pcdcl_core_entailed_iff  satisfiable_carac[symmetric]
        cdcl_learn_clause.simps cdcl_resolution.simps
        cdcl_subsumed.simps cdcl_flush_unit.simps cdcl_inp_propagate.simps
        cdcl_inp_conflict.simps cdcl_unitres_true.simps cdcl_promote_false.simps
        cdcl_pure_literal_remove.simps)
  next
    assume ?A
    then obtain I where
       ‹I ⊨sm pget_all_init_clss S› and
       I: ‹consistent_interp I›
       ‹total_over_m I (set_mset (pget_all_init_clss S))›
      unfolding satisfiable_def by blast
    with assms have ‹¬cdcl_pure_literal_remove S T ⟹ I ⊨sm pget_all_init_clss T›
      using atms_eq
      apply (induction rule: pcdcl.induct)
      subgoal by (auto simp: pcdcl_core_entailed_iff satisfiable_carac[symmetric])
      subgoal by (auto simp: cdcl_learn_clause.simps true_clss_cls_def total_over_m_def
        cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init_def satisfiable_def)
      subgoal by (auto simp: cdcl_resolution.simps total_over_m_def consistent_interp_def
        satisfiable_carac[symmetric])
      subgoal
        by (auto simp: cdcl_subsumed.simps satisfiable_carac[symmetric])
      subgoal
        by (auto simp: cdcl_flush_unit.simps satisfiable_carac[symmetric])
      subgoal
        by (auto simp: cdcl_inp_propagate.simps satisfiable_carac[symmetric])
      subgoal
        by (auto simp: cdcl_inp_conflict.simps satisfiable_carac[symmetric])
      subgoal
        by (auto simp: cdcl_unitres_true.simps satisfiable_carac[symmetric])
      subgoal
        by (auto simp: cdcl_promote_false.simps satisfiable_carac[symmetric])
      subgoal
        by fast
      done
    then show ?B
      using cdcl_pure_literal_remove_satisfiable_iff[of S T] I atms_eq assms ‹?A›
      by (auto simp: satisfiable_carac[symmetric] intro: exI[of _ I])
  qed
qed

lemma rtranclp_pcdcl_entailed_iff:
  ‹pcdcl** S T ⟹ consistent_interp M ⟹ pcdcl_all_struct_invs S ⟹
    cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S) ⟹
  total_over_set M (atms_of_mm (pget_all_init_clss T)) ⟹ M ⊨m pget_all_init_clss T ⟹ M ⊨m pget_all_init_clss S›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using rtranclp_pcdcl_pget_all_init_clss[of S T] pcdcl_pget_all_init_clss[of T U]
      Pragmatic_CDCL.rtranclp_pcdcl_entailed_by_init[of S T]
      rtranclp_pcdcl_all_struct_invs[of S T]
    by (auto dest!: pcdcl_entailed_iff[of _ _ M] simp del: atms_of_ms_union)
  done


lemma pcdcl_restart_entailed_iff:
  ‹pcdcl_restart S T ⟹ M ⊨m pget_all_init_clss T ⟷ M ⊨m pget_all_init_clss S›
  by (induction rule: pcdcl_restart.induct) (auto)

lemma pcdcl_inprocessing_entailed_iff:
  ‹pcdcl_inprocessing S T ⟹ consistent_interp M ⟹ pcdcl_all_struct_invs S ⟹
    cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S) ⟹
  total_over_set M (atms_of_mm (pget_all_init_clss T)) ⟹ M ⊨m pget_all_init_clss T ⟹ M ⊨m pget_all_init_clss S›
  apply (induction rule: pcdcl_inprocessing.induct)
  using pcdcl_entailed_iff apply blast
  using pcdcl_restart_entailed_iff by blast

lemma pcdcl_restart_satisfiable_iff:
  ‹pcdcl_restart S T ⟹ pcdcl_all_struct_invs S ⟹
    cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S) ⟹
  satisfiable (set_mset (pget_all_init_clss T)) ⟷ satisfiable (set_mset (pget_all_init_clss S))›
  by (induction rule: pcdcl_restart.induct)
   (auto simp: satisfiable_carac[symmetric])

lemma pcdcl_inprocessing_satisfiable_iff:
  ‹pcdcl_inprocessing S T ⟹ pcdcl_all_struct_invs S ⟹
    cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S) ⟹
  satisfiable (set_mset (pget_all_init_clss T)) ⟷ satisfiable (set_mset (pget_all_init_clss S))›
  apply (induction rule: pcdcl_inprocessing.induct)
  subgoal for S T
    using pcdcl_satisfiable_iff[of S T] by blast
  using pcdcl_restart_satisfiable_iff by blast

lemma rtranclp_pcdcl_inprocessing_entailed_iff:
  ‹pcdcl_inprocessing** S T ⟹ consistent_interp M ⟹ pcdcl_all_struct_invs S ⟹
    cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S) ⟹
  total_over_set M (atms_of_mm (pget_all_init_clss T)) ⟹ M ⊨m pget_all_init_clss T ⟹ M ⊨m pget_all_init_clss S›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using
      pcdcl_inprocessing_entailed_iff[of T U M] rtranclp_pcdcl_inprocessing_entailed_by_init[of T U]
      rtranclp_pcdcl_inprocessing_pcdcl_all_struct_invs[of S T]
      rtranclp_pcdcl_inprocessing_pget_all_init_clss[of S T]
      pcdcl_inprocessing_pget_all_init_clss[of T U]
      apply auto
      using rtranclp_pcdcl_inprocessing_entailed_by_init apply blast+
      done
  done


lemma rtranclp_pcdcl_inprocessing_satisfiable_iff:
  ‹pcdcl_inprocessing** S T ⟹ pcdcl_all_struct_invs S ⟹
    cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S) ⟹
  satisfiable (set_mset (pget_all_init_clss T)) ⟷ satisfiable (set_mset (pget_all_init_clss S))›
  apply (induction rule: rtranclp_induct)
  subgoal by auto
  subgoal for T U
    using
      pcdcl_inprocessing_satisfiable_iff[of T U] rtranclp_pcdcl_inprocessing_entailed_by_init[of T U]
      rtranclp_pcdcl_inprocessing_pcdcl_all_struct_invs[of S T]
      rtranclp_pcdcl_inprocessing_pget_all_init_clss[of S T]
      pcdcl_inprocessing_pget_all_init_clss[of T U]
      apply auto
      using rtranclp_pcdcl_inprocessing_entailed_by_init apply blast+
      done
  done

lemma pcdcl_restart_only_entailed_iff:
  ‹pcdcl_restart_only S T ⟹ M ⊨m pget_all_init_clss T ⟷ M ⊨m pget_all_init_clss S›
  by (induction rule: pcdcl_restart_only.induct) (auto)

lemma pcdcl_stgy_restart_same_init_vars:
  ‹pcdcl_stgy_restart  (R1, R2, S, m, n, g) (R1', R2', T, m', n', g') ⟹
  pcdcl_all_struct_invs S ⟹
     atms_of_mm (pget_all_init_clss S) = atms_of_mm (pget_all_init_clss T)›
  apply (induction ‹(R1, R2, S, m, n, g)› ‹(R1', R2', T, m', n', g')› rule: pcdcl_stgy_restart.induct)
  subgoal
    by (auto dest!: pcdcl_restart_only_entailed_iff pcdcl_restart_entailed_iff
      dest!: rtranclp_pcdcl_stgy_pcdcl pcdcl_tcore_stgy_pcdcl_stgy'
      simp: rtranclp_pcdcl_pget_all_init_clss)
  subgoal for U
    apply (auto simp: pcdcl_restart_same_init_vars rtranclp_pcdcl_pget_all_init_clss
      dest!: rtranclp_pcdcl_stgy_pcdcl pcdcl_tcore_stgy_pcdcl_stgy')
    using rtranclp_pcdcl_inprocessing_pcdcl_all_struct_invs rtranclp_pcdcl_inprocessing_pget_all_init_clss rtranclp_pcdcl_pget_all_init_clss apply blast
      by (smt pcdcl_restart_pcdcl_all_struct_invs pcdcl_restart_same_init_vars rtranclp_pcdcl_inprocessing_pcdcl_all_struct_invs rtranclp_pcdcl_inprocessing_pget_all_init_clss rtranclp_pcdcl_pget_all_init_clss)
  subgoal
    by (auto simp: pcdcl_restart_only_same_init_vars)
  subgoal
    by auto
  done

lemma rtranclp_pcdcl_stgy_restart_same_init_vars:
  ‹pcdcl_stgy_restart**  (R1, R2, S, m, n, g) (R1', R2', T, m', n', g') ⟹
  pcdcl_all_struct_invs S ⟹
     atms_of_mm (pget_all_init_clss S) = atms_of_mm (pget_all_init_clss T)›
  apply (induction rule: rtranclp_induct[of r ‹(_, _, _, _, _, _)› ‹(_, _, _, _, _, _)›, split_format(complete), of for r])
  subgoal
    by (auto dest!: pcdcl_restart_only_entailed_iff pcdcl_restart_entailed_iff
      dest!: rtranclp_pcdcl_stgy_pcdcl pcdcl_tcore_stgy_pcdcl_stgy'
      rtranclp_pcdcl_stgy_pcdcl simp: rtranclp_pcdcl_pget_all_init_clss)
  subgoal
    by (auto dest: rtranclp_pcdcl_stgy_restart_pcdcl_all_struct_invs
      pcdcl_stgy_restart_same_init_vars)
  done

lemma pcdcl_stgy_restart_entailed_iff:
  ‹pcdcl_stgy_restart  (R1, R2, S, m, n, g) (R1', R2', T, m', n', g') ⟹
  pcdcl_all_struct_invs S ⟹ cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S) ⟹
  consistent_interp M ⟹ total_over_set M (atms_of_mm (pget_all_init_clss T)) ⟹
  M ⊨m pget_all_init_clss T ⟹ M ⊨m pget_all_init_clss S›
  apply (induction ‹(R1, R2, S, m, n, g)› ‹(R1', R2', T, m', n', g')› rule: pcdcl_stgy_restart.induct)
  apply (auto dest: pcdcl_restart_only_entailed_iff pcdcl_restart_entailed_iff
    dest: rtranclp_pcdcl_stgy_pcdcl pcdcl_tcore_stgy_pcdcl_stgy'
    rtranclp_pcdcl_stgy_pcdcl rtranclp_pcdcl_entailed_iff)[]
  apply (smt pcdcl_restart_entailed_iff pcdcl_restart_pcdcl_all_struct_invs pcdcl_restart_same_init_vars
    rtranclp_pcdcl_entailed_iff rtranclp_pcdcl_inprocessing_entailed_by_init
    rtranclp_pcdcl_inprocessing_entailed_iff rtranclp_pcdcl_inprocessing_pcdcl_all_struct_invs
    rtranclp_pcdcl_stgy_pcdcl rtranclp_pcdcl_stgy_pget_all_init_clss twl_restart_ops.pcdcl_restart_entailed_by_init)
  using pcdcl_restart_only_entailed_iff apply blast
  by simp

lemma rtranclp_pcdcl_restart_entailed_iff:
  ‹pcdcl_stgy_restart**  (R1, R2, S, m, n, g) (R1', R2', T, m', n', g') ⟹
  pcdcl_all_struct_invs S ⟹ cdclW_restart_mset.cdclW_learned_clauses_entailed_by_init (state_of S) ⟹
  consistent_interp M ⟹ total_over_set M (atms_of_mm (pget_all_init_clss T)) ⟹
  M ⊨m pget_all_init_clss T ⟹ M ⊨m pget_all_init_clss S›
  apply (induction rule: rtranclp_induct[of r ‹(_, _, _, _, _, _)› ‹(_, _, _, _, _, _)›, split_format(complete), of for r])
  subgoal by auto
  subgoal for T U
    by (simp add: pcdcl_stgy_restart_entailed_iff pcdcl_stgy_restart_same_init_vars
      rtranclp_pcdcl_stgy_restart_entailed_by_init rtranclp_pcdcl_stgy_restart_pcdcl_all_struct_invs)
  done

lemma [simp]: ‹pget_all_init_clss (pstateW_of S) = (get_all_init_clss S)›
  by (cases S) auto

lemma empty_entails_novars_iff: ‹atms_of_mm S = {} ⟹ {} ⊨ps set_mset S ⟷ S = {#}›
  unfolding true_clss_clss_def
  by (cases S) (auto simp: satisfiable_def total_over_m_def intro: Ex_consistent_interp)
end

end