# 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```