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