伊莎贝尔基数

我有一个比较简单的问题，它在伊莎贝尔引起了一些问题。伊莎贝尔基数

我试着去证明如下：

∃ b . inv_Board b

板是一组。船上的不变的是：

card b <= FINISHED

在哪里结束是我用我自己的类型的24 int值，但这样它实际上是一个VDMNat类型，我要投它，像这样：

int (card b) <= FINISHED

大锤不工作，我有1子目标：

∃b. int (card b) ≤ FINISHED

什么想法？

是'B'在你知道不变拥有这方面的具体价值？如果你应用（规则exI [of _b]），会发生什么情况？ –

'b'的类型是什么？如果没有你的特殊输入，即使用'card b <= 24'，如果形成不变量，证明是否工作？ –

如果»FINISHED«是24的整数值，那么应该有一个等式定理‹FINISHED = 24›。

然后你就可以进行大致是

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

2016-01-17 08:00:46

回答