need a definition in Isabelle to show that two partial functions never produce the same output

Question

I'm using the mathematical toolkit in HOL-Z to discharge some Isabelle predicates. specifically I'm using the partial function definition to define some of the relations in a Z specification that I'm writing, where I convert the schema's to Specification statements so that I can generate simple HOL predicates.

definitions from HOL-Z toolkit

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

When I write the following within a predicate:

FORALL x. balance %^ x = Bbalance %^ x

where balance and Bbalance are both partial functions(in Z), of the form ('a <=> 'b) in Isabelle, I assume it behaves fine.

How can I define another function where I say that the two partial functions are totally disjoint for all 'x' . I mean the relational application of the same value on two partial functions 'balance' and 'Bbalance' NEVER produce the same value. something like...

FORALL x. balance %^ x \noteq Bbalance %^ x

sorry for the poor explanation. we learn through expert advice :).

Unknown Unknown · Accepted Answer · 2015-01-29T23:14:25

Your rel_appl_def rule makes use of the epsilon function. According to the Stanford Encyclopedia of Philosophy (SEP)(*) in his Hamburg lecture in 1921 (1922), Hilbert first presented the idea of using choice functions to deal with the principle of the excluded middle in a formal system for arithmetic.

The governing axiom of the epsilon function reads as follows:

 (A x) --> (A (@ A))

In classical logic, because of ex falso quodlibet, if (A x) fails, (@ A) can take any interpretation. This means that your rel_appl_def rule gives any value when you supply an argument x that is not in the domain dom R.

So probably what you want to use as equality would be the following boolean function (^) on two partial functions:

 f ^ g = (dom f = dom g) & (!x. x : dom f --> f %^ x = g %^ x)

What I cannot understand when SEP writes, the second, of perhaps greater current interest, is the use of the epsilon-operator in the theorem-proving systems HOL and Isabelle, where the expressive power of epsilon-terms yields significant practical advantages.

I have seen a much simpler treatment of partial functions in practice, namely using the option type. So a partial function f belongs simply to a type A => B option. But when you cannot change the types in your project, it is probably wiser to seek the equality that fits your requirements, the above definition could be a candidate.

Bye

(*)
The Epsilon Calculus, Jeremy Avigad and Richard Zach
First published Fri May 3, 2002; substantive revision Wed Nov 27, 2013
http://plato.stanford.edu/entries/epsilon-calculus/

need a definition in Isabelle to show that two partial functions never produce the same output

1 Answers