Theory Invariants

theory Invariants
  imports SCL_FOL
begin

text ‹The following lemma restate existing invariants in a compact, paper-friendly way.›

lemma (in scl_fol_calculus) scl_state_invariants:
  shows
    inv_trail_lits_ground:
      "trail_lits_ground initial_state"
      "scl N β S S' ⟹ trail_lits_ground S ⟹ trail_lits_ground S'" and
    inv_trail_atoms_lt:
      "trail_atoms_lt β initial_state"
      "scl N β S S' ⟹ trail_atoms_lt β S ⟹ trail_atoms_lt β S'" and
    inv_undefined_trail_lits:
      "∀Γ' Ln Γ''. state_trail initial_state = Γ'' @ Ln # Γ' ⟶ ¬ trail_defined_lit Γ' (fst Ln)"
      "scl N β S S' ⟹
        (∀Γ' Ln Γ''. state_trail S = Γ'' @ Ln # Γ' ⟶ ¬ trail_defined_lit Γ' (fst Ln)) ⟹
        (∀Γ' Ln Γ''. state_trail S' = Γ'' @ Ln # Γ' ⟶ ¬ trail_defined_lit Γ' (fst Ln))" and
    inv_ground_closures:
      "ground_closures initial_state"
      "scl N β S S' ⟹ ground_closures S ⟹ ground_closures S'" and
    inv_ground_false_closures:
      "ground_false_closures initial_state"
      "scl N β S S' ⟹ ground_false_closures S ⟹ ground_false_closures S'" and
    inv_trail_propagated_lits_wf:
      "∀𝒦∈set (state_trail initial_state). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ"
      "scl N β S S' ⟹
        (∀𝒦∈set (state_trail S). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ) ⟹
        (∀𝒦∈set (state_trail S'). ∀D K γ. snd 𝒦 = Some (D, K, γ) ⟶ fst 𝒦 = K ⋅l γ)" and
    inv_trail_resolved_lits_pol:
      "trail_resolved_lits_pol initial_state"
      "scl N β S S' ⟹ trail_resolved_lits_pol S ⟹ trail_resolved_lits_pol S'" and
    inv_initial_lits_generalize_learned_trail_conflict:
      "initial_lits_generalize_learned_trail_conflict N initial_state"
      "scl N β S S' ⟹ initial_lits_generalize_learned_trail_conflict N S ⟹ initial_lits_generalize_learned_trail_conflict N S'" and
    inv_trail_lits_from_clauses:
      "trail_lits_from_clauses N initial_state"
      "scl N β S S' ⟹ trail_lits_from_clauses N S ⟹ trail_lits_from_clauses N S'" and
    inv_sound_state:
      "sound_state N β initial_state"
      "scl N β S S' ⟹ sound_state N β S ⟹ sound_state N β S'"
  using trail_lits_ground_initial_state scl_preserves_trail_lits_ground
  using trail_atoms_lt_initial_state scl_preserves_trail_atoms_lt
  using trail_lits_consistent_initial_state[unfolded trail_lits_consistent_def trail_consistent_iff]
    scl_preserves_trail_lits_consistent[unfolded trail_lits_consistent_def trail_consistent_iff]
  using ground_closures_initial_state scl_preserves_ground_closures
  using ground_false_closures_initial_state scl_preserves_ground_false_closures
  using trail_propagated_lit_wf_initial_state scl_preserves_trail_propagated_lit_wf
  using trail_resolved_lits_pol_initial_state scl_preserves_trail_resolved_lits_pol
  using initial_lits_generalize_learned_trail_conflict_initial_state
    scl_preserves_initial_lits_generalize_learned_trail_conflict
  using trail_lits_from_clauses_initial_state scl_preserves_trail_lits_from_clauses
  using sound_initial_state scl_preserves_sound_state
  by metis+

end