「特定の定数が true の場合」(この場合は「sec=ok」の場合) の述語を記述しようとしています。その特定の結果の式を記述したため、述語は False と評価されます。述語の他の場所にある別の式と矛盾する含意。(f%^x ≠ g%^x) ∧ (f%^ci = g%^ci) は、x と ci の両方が普遍的に量化され、同じ型を持つという事実を考えると、矛盾するはずです。
ただし、Nitpick は、私が理解できない反例を生成します。誰かがこの補題を親切にチェックして、矛盾が証明できるかどうかを確認できることを望んでいました. または、どこが間違っているか教えてください。簡単な説明は次のとおりです。
- f と g は、任意の型 'a から 'b までの 2 つの部分関数です。
'sec' は、値が 'ok' と 'notok' の定数です。
f::'a-|->'b g::'a-|->'b lemma simpleExample: shows "∀ (ci::'a ) (a::'a set) (b::'b set) ( f::'a <=> 'b) . f ∈ (a-|-> b) ∧ card f > 0 --> (∃ ( g::'a <=> 'b) . g ∈ (a-|->b) ∧ a=(dom f ∪ dom g) ∧ ( ∀ (x ::'a) . sec=ok --> f%^x ≠ g%^x) ∧ f%^ci = g%^ci ) "
また、Function Application に関して、2 つの Z Math ツールキット間に「微妙な」違いがあることも確認しました。両方を試しましたが、問題は残ります。
In HIVE Z Math toolkit : "R %^ x == The(λy. (x,y) : R ) "
In HOL-Z Math Toolkit : "R %^ x == (@y. (x,y) : R)"
Nitpick エラーはここで見ることができます http://i58.tinypic.com/316te1t.png
注: 参考までに、現在使用している部分関数の定義を HOL-Z から見つけてください。
type_synonym ('a,'b) lts = "('a*'b) set" (infixr "<=>" 20)
prodZ ::"['a set,'b set] => ('a <=> 'b) " ("_ %x _" [81,80] 80)
"a %x b" == "a <*> b"
rel ::"['a set, 'b set] => ('a <=> 'b) set" ("_ <--> _" [54,53] 53)
rel_def : "A <--> B == Pow (A %x B)"
partial_func ::"['a set,'b set] => ('a <=> 'b) set" ("_ -|-> _" [54,53] 53)
partial_func_def : "S -|-> R ==
{f. f:(S <--> R) & (! x y1 y2. (x,y1):f & (x,y2):f --> (y1=y2))}"
rel_appl :: "['a<=>'b,'a] => 'b" ("_ %^ _" [90,91] 90)
rel_appl_def : "R %^ x == The(λy. (x,y) : R)"