The following data types are defined in HOL4.
val _ = Datatype ` coordinate = <|
x_axis: real;
y_axis: real; z_axis: real
|> `; val _ = Datatype `
chromosome = <| r: num;
b: num; distance:
real; rx: coordinate;
path: coordinate list; bx:
coordinate |> `;
val ch = ``ch: chromosome``;
val pop = ``pop: chromosome list``;
val get_def = Define `
get pop = !ch if (Certain condition) then (ch with <| distance :=
ch.distance + 1000 |>)
else (ch with <| distance := ch.distance |>)`;
Given a pop(:chromosome list),ch is an element in pop. For any ch, if a
certain condition is met, the value of distance in ch is increased by 1000 on
the basis of the original value, otherwise it is unchanged. How to achieve this?
How to write an program in SML (or Haskell, or OCaml) first,then
formalising it in HOL? Can you give a simple example?_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
