Theory Lem_bool

chapter ‹Generated by Lem from bool.lem›.›

theory "Lem_bool" 

imports
  Main

begin 

 

― ‹ The type bool is hard-coded, so are true and false ›

― ‹ ----------------------- ›
― ‹ not                     ›
― ‹ ----------------------- ›

― ‹val not : bool -> bool›
― ‹let not b=  match b with
  | true -> false
  | false -> true
end›

― ‹ ----------------------- ›
― ‹ and                     ›
― ‹ ----------------------- ›

― ‹val && [and] : bool -> bool -> bool›
― ‹let && b1 b2=  match (b1, b2) with
  | (true, true) -> true
  | _ -> false
end›


― ‹ ----------------------- ›
― ‹ or                      ›
― ‹ ----------------------- ›

― ‹val || [or] : bool -> bool -> bool›
― ‹let || b1 b2=  match (b1, b2) with
  | (false, false) -> false
  | _ -> true
end›


― ‹ ----------------------- ›
― ‹ implication             ›
― ‹ ----------------------- ›

― ‹val --> [imp] : bool -> bool -> bool›
― ‹let --> b1 b2=  match (b1, b2) with
  | (true, false) -> false
  | _ -> true
end›


― ‹ ----------------------- ›
― ‹ equivalence             ›
― ‹ ----------------------- ›

― ‹val <-> [equiv] : bool -> bool -> bool›
― ‹let <-> b1 b2=  match (b1, b2) with
  | (true, true) -> true
  | (false, false) -> true
  | _ -> false
end›


― ‹ ----------------------- ›
― ‹ xor                     ›
― ‹ ----------------------- ›

― ‹val xor : bool -> bool -> bool›

end