Интерпретация частичных функций от Z до Изабель /HOL

Question

Я пытаюсь написать предикат так, чтобы, "если определенная константа была истинной"(в этом случае, если "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 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)"