1

我正在尝试编写一个谓词，“如果某个常数为真”（在这种情况下，如果 'sec=ok'）那么谓词将评估为 False，因为我已经在那个特定的结果中编写了一个表达式与谓词其他地方的另一个表达式相矛盾的暗示。(f%^x ≠ g%^x) ∧ (f%^ci = g%^ci) 应该是矛盾的，因为 x 和 ci 都是普遍量化的并且具有相同的类型。

但是，Nitpick 产生了一个我无法理解的反例。我希望是否有人可以检查这个引理，看看是否可以证明矛盾。或者让我知道我哪里出错了。所以简要说明如下；

  • f 和 g 是从任意类型 'a 到 'b 的两个偏函数。

  • '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 )  "

我还看到了两个 Z 数学工具包之间关于函数应用的“细微”差异。我都试过了，但问题仍然存在。

    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)"
4

0 回答 0