伊莎貝爾基數

我有一個比較簡單的問題，它在伊莎貝爾引起了一些問題。伊莎貝爾基數

我試着去證明如下：

∃ 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

回答