Ошибка проверки Isabelle при вызове операций последовательной записи

Question

Я очень новичок в Isabelle и доказал свои обязательства, и в настоящее время я переводил модель VDM, которую я сделал из игры «Dots and Boxes» (основные переводы VDM были предоставлены для нас).

До сих пор у меня есть два типа записей, а Dot:

record Dot = 
    pos_x :: VDMNat1 
    pos_y :: VDMNat1 

..и в Move (состоящий из двух Dot 'ы):

record Move = 
    dot_a :: Dot 
    dot_b :: Dot 

..но теперь я m пытается перевести последовательность из этих Move и испытывает странную ошибку с инвариантом:

type_synonym Moves = "Move VDMSet" 

definition inv_Moves :: "Moves ⇒ " 
    where "inv_Moves ms ≡ 
     int (card ms) ≤ MAX_MOVES ∧ 
     (∀ m . m ∈ ms ⟶ 
      inv_Move m ∧ 
      pos_x dot_a m > 0 ∧ 
      pos_y dot_a m > 0 ∧ 
      pos_x dot_b m > 0 ∧ 
      pos_y dot_b m > 0 ∧ 
      pos_x dot_a m ≤ BOARD_WIDTH ∧ 
      pos_y dot_a m ≤ BOARD_HEIGHT ∧ 
      pos_x dot_b m ≤ BOARD_WIDTH ∧ 
      pos_y dot_b m ≤ BOARD_HEIGHT ∧ 
      inverse_move m ∉ ms)" 

Я знаю, что инвариант, вероятно, хуже, чем просто эту ошибку, но, насколько я могу сказать от ошибки это имеющей проблемы с несколькими вызовами к полей записи; то есть пропускают dot_a до pos_x вместо результата dot_a m. Единственное решение, о котором я могу думать, - манипулировать порядком операций, но я не уверен, как это сделать как pos_x dot_a m = pos_x (dot_a m).

Любая помощь была бы высоко оценена!

Answer 1

Ассоциативность применения функций - это наоборот: pos_x dot_a m = (pos_x dot_a) m. Попробуйте pos_x (dot_a m).