More pure functions in the preamble?

[msaaltink]

Several very simple functions ought to be pure in the BPL preamble: $Lt, $Gt, $Le, $Ge, $And, $Or, $Not, $AddBv8_unchecked, $AndBv8, ... various type_inv such as $0_prover_type_inv'u8' (although I am not sure those are used anywhere), $AndInt'u8', ... , $AddU16_unchecked, ..., various $Cast for integers,and bitvectors. As we have seen, Boogie and Z3 perform better with functions than procedures.