Translated TCP1_hostLTS to Lem.

Notes (probably incomprehensible):

TCP1_hostLTS:

need to work out what to do with revimp and rule format parsing

updated_by and updated_by ... only_when constructs are irregular - replace with equivalents (although this is a rather tricky replacement to perform automatically)

is updated_by overloaded to take both 'a and 'a -> 'a?

val myrec_def = Hol_datatype `
myrec = <|
  a1: num;
  a2: num
|>
`;

``r with <| a1 := 2 |>``;
``r with <| a1 updated_by 2 |>``; (* doesn't work *)
``r with <| a1 updated_by (\ x. 2) |>``;

Ah! the point is that a updated_by v onlywhen c translates to updated_by (if c then (K v) else ...)

so provided the construct is updated_by v onlyhen c, we expect v to be a value of the same type as the field, and c to be a boolean

translation of updated_by .. onlywhen ... described in TCP1_utils

tcp_seq_flip_sense is overloaded - this is hard to automatically replace; probably most are foreign to local?

the precedence of |+ is not correct in lem; need to bracket eg    fds' = fds |+ (fd', fid') as    fds' = (fds |+ (fd', fid'))

OK overloading from TCP1_baseTypes needs to be manually disambiguated; probably do this upfront

UNION needs changing to union; UNION is an infix op

FAIL is overloaded and needs to be manually disambiguated

manual disambiguation of cases: case x of y -> u = v could be (case x of y -> u) = v or case x of y -> (u = v)

x NOTIN y z manually disambiguated to x NOTIN (y z)

IN' not infix

strings are char lists in hol, but a separate type in lem; introduced string_of_char_list

~bsd_arch h.arch dismabinguated to ~(bsd_arch h.arch)

send_16 is wrong in the original HOL - send2 takes 4 arguments not 3

binding precedences are often wrong

hol type Lh_return of x * y allows currying? or pairs; lem need Lh_return (x*y) to allow pairs (similar to ocaml)

hol allows any syntax to be infix, but lem doesn't

constructors X of  t1 * t1 and X of (t1 * t2) are not the same in hol and ocaml and lem - may have to change pattern matching or type