我正在尝试将VDM模型转换为Isabelle,但出于某种原因,我所做的,不起作用
以下示例是我的模型的VDM功能
Dot_Move_invariant: Dot * Dot -> bool
Dot_Move_invariant(d1, d2) ==
d1 < d2 and
let coordinate_1 = Dot_Coord(d1) in
let coordinate_2 = Dot_Coord(d2) in
moving_coordinates_invariant(coordinate_1, coordinate_2);
以下示例代表我尝试翻译它
definition
Dot_Move_invariant:: "Dot⇒Dot⇒𝔹"
where "Dot_Move_invariant d1 d2 ≡ d1 < d2 ∧ let x = (SOME y. y ∈ Dot_Coord d1) in x ∧ let y = (SOME x. x ∈ Dot_Coord d2 ) "
我得到的错误是:内部语法错误⌂无法解析道具
它可能如下:
"Dot_Move_invariant d1 d2 ≡ d1 < d2 ∧ let x = (SOME y. y ∈ Dot_Coord d1) in x ∧ let y = (SOME x. x ∈ Dot_Coord d2 ) in y"