Я использую математический инструментарий в HOL-Z для выполнения некоторых предикатов Isabelle. в частности, я использую определение частичной функции для определения некоторых отношений в спецификации Z, которые я пишу, где я конвертирую инструкции схемы в спецификацию, чтобы я мог генерировать простые предикаты HOL.нужно определить в Изабель, чтобы показать, что две частичные функции никогда не производят один и тот же вывод
определения из 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 == (@y. (x,y) : R)"
Когда я написать следующее в предиката:
FORALL x. balance %^ x = Bbalance %^ x
, где баланс и Bbalance оба частичные функции (в Z), вида ('a < =>' b) в Изабель, я предполагаю, что он ведет себя хорошо.
Как определить другую функцию, где я говорю, что две частичные функции полностью не пересекаются для всех «х». Я имею в виду, что реляционное приложение того же значения на балансе двух парциальных функций и «Bbalance» никогда не производит одинаковое значение. что-то вроде ...
FORALL x. balance %^ x \noteq Bbalance %^ x
извините за плохое объяснение. мы узнаем через экспертный совет :).
Я просто заметить, скорее всего, Isabelle позволит вам доказательство (е^г) <-> (F = G), и Isabelle также даст вам (! х.x: f = x: g) <-> (f = g). Но я не вижу больших шансов для (! X. (F%^x) = (g%^x)) <-> (f = g). –
Как у бокового узла: более новая версия Isabelle также имеет директиву «partial_function», см. Также здесь: http://stackoverflow.com/questions/25280566/how-to-define-a-partial-function-in-isabelle Но я в настоящее время не знаю основополагающего механизма и будет ли он состоять из еще одной жизнеспособной альтернативы. –