# [isabelle] Parametricity for functions which ignore arguments

Dear list,

`Dmitriy and I are struggling with a proof about parametricity of a constant in
``Isabelle/HOL. Suppose we have a natural functor 'a F and a parametric function foo
`
bnf_axiomatization 'a F
consts foo :: "'a F => ('a => 'c G) => 'c G"
axiomatization where
foo_param: "!!A. rel_fun (rel_F A) (rel_fun (rel_fun A (rel_G B)) (rel_G B)) foo foo"

`where 'b G is some type expression for which rel_G is the appropriate relator (G can be a
``BNF, too, if this helps in any way).
`

`Further, we know that for given x :: 'a F and y :: 'b F with "rel_F A x y", the function
``foo ignores its second argument, i.e.,
`
!!f g. foo x f = foo x g
!!f g. foo y f = foo y g

`Can we deduce from all of the above that "rel_G C (foo x f) (foo y g)" for any f and g?
``And if so, how?
`

`Intuitively, the reasoning goes as follows. Parametricity expresses that foo cannot create
``values of type 'c out of nothing. By its type signature, it can only create such values by
``using the second argument. However, for the given arguments x and y, we know that foo x
``and foo y ignore their second arguments, so foo cannot create a value in 'c. That is, foo
``must return a value of type 'c G which does not contain any 'c values at all. Therefore,
``there exist values a and b such that rel_G C a b for any relation C. Hence,
`
rel_fun A (rel_G C) (%_. a) (%_. b)
and therefore foo x f = foo x (%_. a) `rel_G C` foo y (%_. b) = foo y g.

`Is there a flaw in our intuitive reasoning? If not, how could this be formally expressed
``in HOL?
`
Best,
Andreas

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