[isabelle] Polymorphic predicate closed under composition
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
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and