I recommend learning about the syntax of HOL a bit more. Also, as Michael
suggested (to you or someone else) maybe write the code up first as an SML
program and then translate to HOL. In any case, here are some nonsense
definitions that HOL allows. They should help you get further.
load "realLib";
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 E pop =
case E pop
of SOME ch => (ch with <| distance := ch.distance + 145 |>)
| NONE => (HD pop with <| distance := (HD pop).distance |>)`;
val getA_def =
Define `
getA pop =
case pop
of [] => ARB
| ch::t =>
if ch.r < ch.b
then (ch with <| distance := ch.distance + 145 |>)
else ch`;
On Wed, Dec 19, 2018 at 9:09 PM 幻＠未来 <849678...@qq.com> wrote:
> 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``;
>
>
> Given a pop(:chromosome list), I want to achieve a goal : If if-condition
> is met, the distance value of the ch in the pop is assigned to other values,
> otherwise the distance value of ch is unchanged. How to solve this problem?
> How to define such an operation?
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
