Structure bword_bitopTheory

signature bword_bitopTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val WAND_DEF : thm
    val WNOT_DEF : thm
    val WOR_DEF : thm
    val WXOR_DEF : thm
  
  (*  Theorems  *)
    val PBITBOP_WAND : thm
    val PBITBOP_WOR : thm
    val PBITBOP_WXOR : thm
    val PBITOP_WNOT : thm
    val WCAT_WNOT : thm
    val WNOT_WNOT : thm
  
  val bword_bitop_grammars : type_grammar.grammar * term_grammar.grammar
  
  
(*
   [word_bitop] Parent theory of "bword_bitop"
   
   [WAND_DEF]  Definition
      
      |- !l1 l2. WORD l1 WAND WORD l2 = WORD (MAP2 $/\ l1 l2)
   
   [WNOT_DEF]  Definition
      
      |- !l. WNOT (WORD l) = WORD (MAP $~ l)
   
   [WOR_DEF]  Definition
      
      |- !l1 l2. WORD l1 WOR WORD l2 = WORD (MAP2 $\/ l1 l2)
   
   [WXOR_DEF]  Definition
      
      |- !l1 l2. WORD l1 WXOR WORD l2 = WORD (MAP2 (\x y. ~(x = y)) l1 l2)
   
   [PBITBOP_WAND]  Theorem
      
      |- $WAND IN PBITBOP
   
   [PBITBOP_WOR]  Theorem
      
      |- $WOR IN PBITBOP
   
   [PBITBOP_WXOR]  Theorem
      
      |- $WXOR IN PBITBOP
   
   [PBITOP_WNOT]  Theorem
      
      |- WNOT IN PBITOP
   
   [WCAT_WNOT]  Theorem
      
      |- !n1 n2 (w1::PWORDLEN n1) (w2::PWORDLEN n2).
           WCAT (WNOT w1,WNOT w2) = WNOT (WCAT (w1,w2))
   
   [WNOT_WNOT]  Theorem
      
      |- !w. WNOT (WNOT w) = w
   
   
*)
end