# [isabelle] Interpretation of Partial Functions from Z to Isabelle/HOL

```I am trying to write a predicate such that, "if a certain constant is
true"(in this case if 'sec=ok') then the predicate will evaluate to False,
because I've written an expression in the consequent of that particular
implication that contradicts with another expression elsewhere in the
predicate. (f%^x â g%^x) â (f%^ci = g%^ci) should contradict, given the
fact that both x and ci are universally quantified and have the same type.

However, Nitpick produces a counter example(
http://i58.tinypic.com/316te1t.png) that I am not able to understand. I was
hoping if someone could kindly check this lemma and see whether a
contradiction can be proved. Or else let me know where I'm going wrong. So
a brief description is as follows;

- f and g are two partial functions from arbitrary types 'a to 'b.
-

'sec' is a constant with values 'ok' and '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 )  "

I've also seen a 'suttle' difference between two Z Math toolkits regarding
Function Application. I've tried both but the problem remains.

In HIVE Z Math toolkit :  "R %^ x      == The(Îy. (x,y) : R )  "
In HOL-Z Math Toolkit :   "R %^ x      == (@y. (x,y) : R)"

NOTE: For reference, please find the definition of partial function I'm
using currently from 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)"

rgrds
Ibrahim

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.