*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Polymorphic predicate closed under composition*From*: Dmitriy Traytel <traytel at in.tum.de>*Date*: Thu, 14 May 2015 20:04:19 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <555370B1.5050000@inf.ethz.ch>*References*: <555370B1.5050000@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

Hi Andreas,

Best wishes, Dmitriy On 13.05.2015 17:41, Andreas Lochbihler wrote:

Dear readers,In Isabelle/HOL, I would like to reason about a polymorphic predicateP which is closed under function composition. Since the concretedefinition of the predicate is very tedious and not relevant for thereasoning, I prefer to work just with the closure properties of P.However, I have not found a nice way to accomplish that. Ideas andpointers are welcome.Here are the details. The predicate P should have type "('a => 'b) =>bool" and satisfy properties such as the following (type variables maybe 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 parameterand assumes the properties 1-3, because this does not typecheck as Poccurs with different type instances. Neither does inductive & friendswork (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_complicatedwhere the first assumption is folded in a definition. Unfortunately,foo does not hold for all x. Thus, defining "P" as "%_. True" wouldallow me to derive False from the first assumption. So I couldcircumvent the actual proof of deriving the conclusion from the secondassumption.I think of axiomatising properties 1-3 for P declared as a globalconstant with consts. In a separate theory, I could show that "%_.True" satisfies all the properties stated. In my understanding, thisshould ensure that the axioms do not introduce inconsistenciesanywhere. Still, as the theorem is proven in a scope where P is onlyaxiomatised, I cannot derive False from the first assumption in itsproof. In fact, the theorem also holds for the metamodel of HOL inwhich 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 thisargument correct? Are there better ways to approach this?Best, Andreas

**Follow-Ups**:**Re: [isabelle] Polymorphic predicate closed under composition***From:*Andreas Lochbihler

**References**:**[isabelle] Polymorphic predicate closed under composition***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] libisabelle: embedding into application
- Next by Date: Re: [isabelle] Document preparation hints
- Previous by Thread: [isabelle] Polymorphic predicate closed under composition
- Next by Thread: Re: [isabelle] Polymorphic predicate closed under composition
- Cl-isabelle-users May 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list