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_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 sound_initial_state scl_preserves_sound_state
  by metis+

end