Изабель мощность

У меня относительно простой вопрос, он вызывает у меня некоторые проблемы с Изабель.

Я пытаюсь доказать следующее:

∃ b . inv_Board b

Доска представляет собой набор. Инвариант на борту:

card b <= FINISHED

Где закончилось значение int 24. Я использую свои собственные типы, поэтому на самом деле это тип VDMNat, и я должен привести его так:

int (card b) <= FINISHED

Кувалда не работает, у меня есть 1 подцель:

∃b. int (card b) ≤ FINISHED

есть идеи?


set cardinality isabelle
person John Setter    schedule 21.12.2015    source источник
comment
Является ли b конкретным значением в том контексте, для которого, как вы знаете, выполняется инвариант? Что произойдет, если вы сделаете apply (rule exI[of _ b])?   -  person Manuel Eberl    schedule 22.12.2015
comment
Какой тип b? Работает ли доказательство, если сформулировать инвариант без вашей специальной типизации, т.е. с card b <= 24?   -  person Ben Keks    schedule 22.12.2015

Ответы (1)


arrow_upward
0
arrow_downward

Если »FINISHED« представляет собой целочисленное значение 24, тогда должна быть теорема об уравнениях ‹FINISHED = 24›.

Затем вы можете действовать примерно так

have "int (card {}) ≤ FINISHED"
  by (simp add: ‹FINISHED = 24›)
then show "∃b. int (card b) ≤ FINISHED"
  ..
person Florian Haftmann    schedule 17.01.2016