Ported remainder of TCP1_auxFns.

Notes:

TCP1_auxFns:

sets and functions to bool not identified?:

  Type error: type mismatch: infix expression
(TCP1_baseTypes.filebflag) -> bool
and
set TCP1_baseTypes.sockbflag
introduced set_of_bool_fn

sf.b is sf.b1

socks \\ sid is DOMSUB socks sid

the following expression is bounded quantification over a fmap
? (sid',s') :: (socks \\ sid)
introduced set_of_fmap

Num is num_of_int

tcp_reass omitted - disambiguation too painful; need to FIXME

andThen infix not in lem version

arguments to functions \ (x:num,y:int). changed to fun ((x:num),(y:int)) ->

assert is a lem reserved word; changed to myassert

choose x :: s. is implemented in HOL as exists x. x IN s && ( )

so we can define mychoose s P as exists x. x IN s && (P x)

does lem have bounded existentials? yes; mychoose s P is exist P s; lem choose is a different thing

there is a clash in field names between TCP1_hostTypes: tcpReassSegment.seq and TCP1_netTypes: tcpSegment.seq; hol can disambiguate using types seemingly, but lem follows ocaml in taking the most recently opened field; tempted to rename the .seq field in tcpReassSegment; Done: renamed tcpReassSegment.seq to tcpReassSegment_seq

n2w is overloaded to operate on word16 and word32; introduced n2w16 for 16bit version

clash in field names between TCP1_hostTypes: host.ts and TCP1_netTypes: tcpSegment.ts; renamed host.ts to host.host_ts

clash in field names between TCP1_netTypes tcpSegment.is1 and TCP1_hostTypes socket.is1; disambiguating by using e.g. TCP1_netTypes.is1 to name fields

FIXME_int used for int - seq32 (don't understand what function this is supposed to be... Ah! this is supposed to be int - int, where the second expression is seq32_diff seq32 seq32 (giving an int))

record update syntax: "r with x updatedby f" replaced by logical equivalent