[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?


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