# [isabelle] Polymorphic predicate closed under composition

Dear readers,

`In Isabelle/HOL, I would like to reason about a polymorphic predicate P which is closed
``under function composition. Since the concrete definition of the predicate is very tedious
``and not relevant for the reasoning, I prefer to work just with the closure properties of
``P. However, I have not found a nice way to accomplish that. Ideas and pointers are welcome.
`

`Here are the details. The predicate P should have type "('a => 'b) => bool" and satisfy
``properties such as the following (type variables may be restricted to some sort if needed):
`
1. P (%x :: 'a. x) for every 'c
2. P f ==> P g ==> P (f o g) for all f :: 'a => 'b and g :: 'c => 'a
3. P (%_ :: 'a. x :: 'b)

`Clearly, I cannot just define a locale l that fixes P as a parameter and assumes the
``properties 1-3, because this does not typecheck as P occurs with different type instances.
``Neither does inductive & friends work (for the same reason).
`

`I could define "P" as "%_. True" and derive properties 1-3 from this. However, my theorem
``is of the form
`
(ALL x. P x --> foo x) ==> P something ==> P something_more_complicated

`where the first assumption is folded in a definition. Unfortunately, foo does not hold for
``all x. Thus, defining "P" as "%_. True" would allow me to derive False from the first
``assumption. So I could circumvent the actual proof of deriving the conclusion from the
``second assumption.
`

`I think of axiomatising properties 1-3 for P declared as a global constant with consts. In
``a separate theory, I could show that "%_. True" satisfies all the properties stated. In my
``understanding, this should ensure that the axioms do not introduce inconsistencies
``anywhere. Still, as the theorem is proven in a scope where P is only axiomatised, I cannot
``derive False from the first assumption in its proof. In fact, the theorem also holds for
``the metamodel of HOL in which P is interpreted as the predicate that I am too lazy to
``define (provided that it exists at all, but that's another issue). Is this argument
``correct? Are there better ways to approach this?
`
Best,
Andreas

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