(* Author: Carsten Schuermann *)
(* Boolean value and functions *)

(* We are defining our own type of BOOLs.  But everything
   said in this lecture works also for the standard BOOLeans
*)

datatype BOOL			
  = O 
  | I

(* TRUE : BOOL -> BOOL 
   TRUE B = TRUE
*)

fun TRUE O = I
  | TRUE I = I

(* FALSE : BOOL -> BOOL 
   FALSE B = FALSE
*)
fun FALSE O = O
  | FALSE I = O

(* ID : BOOL -> BOOL 
   ID B = ID
*)
fun ID O = O
  | ID I = I

(* NOT : BOOL -> BOOL 
   NOT B = -B
*)
fun NOT O = I
  | NOT I = O

(* AND : BOOL -> BOOL -> BOOL 
   AND B1 B2 = B1 /\ B
*)
fun AND O O = O 
  | AND O I = O
  | AND I O = O
  | AND I I = I

(* OR : BOOL -> BOOL -> BOOL 
   OR B1 B2 = B1 \/ B2
*)
fun OR O O = O 
  | OR O I = I
  | OR I O = I
  | OR I I = I

(* XAND : BOOL -> BOOL -> BOOL 
   XAND B1 B2 = B1 /+\ B2
*)
fun XAND O O = I
  | XAND O I = O
  | XAND I O = O
  | XAND I I = I

(* XOR : BOOL -> BOOL -> BOOL 
   XOR B1 B2 = B1 \+/ B2
*)
fun XOR O O = O
  | XOR O I = I
  | XOR I O = I
  | XOR I I = O


(* IMP : BOOL -> BOOL -> BOOL 
   IMP B1 B2 = B1 => B2
*)
fun IMP O O = O
  | IMP O I = O
  | IMP I O = O
  | IMP I I = I

(* NAND : BOOL -> BOOL -> BOOL 
   NAND B1 B2 = - (B1 /\ B)
*)
fun NAND O O = I
  | NAND O I = I
  | NAND I O = I
  | NAND I I = O

fun nand a b = NOT (AND a b)

(* NOR : BOOL -> BOOL -> BOOL 
   NOR B1 B2 = - (B1 \/ B2)
*)
fun NOR O O = I
  | NOR O I = O
  | NOR I O = O
  | NOR I I = O

fun nor a b = NOT (OR a b)