Structure cooperTheory

signature cooperTheory =
sig
  type thm = Thm.thm
  
  (*  Theorems  *)
    
    val F_and_l : thm
    val F_and_r : thm
    val F_or_l : thm
    val F_or_r : thm
    
    
    val NOT_AND : thm
    
    
    
    val NOT_NOT_P : thm
    val NOT_OR : thm
    val T_and_l : thm
    val T_and_r : thm
    val T_or_l : thm
    val T_or_r : thm
    
    
    
    
    
    
    
    
    val simple_conj_congruence : thm
    val simple_disj_congruence : thm
(*
   [int_arith] Parent theory of "cooper"
   
   [F_and_l]  Theorem
      
      ⊢ ∀t. F ∧ t ⇔ F
   
   [F_and_r]  Theorem
      
      ⊢ ∀t. t ∧ F ⇔ F
   
   [F_or_l]  Theorem
      
      ⊢ ∀t. F ∨ t ⇔ t
   
   [F_or_r]  Theorem
      
      ⊢ ∀t. t ∨ F ⇔ t
   
   [NOT_AND]  Theorem
      
      ⊢ ∀B A. ¬(A ∧ B) ⇔ ¬A ∨ ¬B
   
   [NOT_NOT_P]  Theorem
      
      ⊢ ∀t. ¬¬t ⇔ t
   
   [NOT_OR]  Theorem
      
      ⊢ ∀B A. ¬(A ∨ B) ⇔ ¬A ∧ ¬B
   
   [T_and_l]  Theorem
      
      ⊢ ∀t. T ∧ t ⇔ t
   
   [T_and_r]  Theorem
      
      ⊢ ∀t. t ∧ T ⇔ t
   
   [T_or_l]  Theorem
      
      ⊢ ∀t. T ∨ t ⇔ T
   
   [T_or_r]  Theorem
      
      ⊢ ∀t. t ∨ T ⇔ T
   
   [simple_conj_congruence]  Theorem
      
      ⊢ ∀p q r. (p ⇒ (q ⇔ r)) ⇒ (p ∧ q ⇔ p ∧ r)
   
   [simple_disj_congruence]  Theorem
      
      ⊢ ∀p q r. (¬p ⇒ (q ⇔ r)) ⇒ (p ∨ q ⇔ p ∨ r)
   
   
*)
end

HOL 4, Trindemossen-2