2

コード生成の非常に単純な定義があるとします。特定のケースに対してのみ定義され、それ以外の場合は実行時例外をスローします。

definition "blubb a = (if P a then True else undefined)"

blubb今、私は正しいことを示したいと思います。例外がスローされるケースは無視する必要があります (数学的な観点ではなく、私の観点から)。Xただし、任意の値がであると仮定するサブゴールになってしまいますundefined。次の補題はサブゴールとほぼ同等です。False例外がスローされる (つまり、undefined返される)ケースを無視したいので、表示したいと思います。

lemma "X = undefined ⟹ False"

これは証明できません。

  try

Nitpick found a counterexample for card 'a = 1:
 Free variable:
  X = a1

例外をスローしたり処理したりする可能性のある関数の正確性を示す最良の方法は何undefinedですか? これはこの質問に関連しています。

4

1 に答える 1

2

undefinedあなたが何も知らないIsabelleの定数です。特に、一般に を証明することはできませんX ≠ undefined。

特定の入力に対してのみ有効な関数を作成する場合は'a option、次のように型を使用することを検討してください。

definition "blubb a ≡ (if P a then Some True else None)"

そして、あなたの証明では、それblubb aが次のように定義されていると仮定します:

lemma "∃x. blubb a = Some x ⟹ Q (blubb a)"
  ...

または単に：

lemma "a ∈ dom blubb ⟹ Q (blubb a)"
  ...

の値は、blubb aを使用して抽出できますthe (blubb a)。

于 2013-03-20T01:27:18.363 に答える