*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*: Fri, 15 May 2015 11:21:56 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <555597A0.50103@inf.ethz.ch>*References*: <555370B1.5050000@inf.ethz.ch> <5554E3A3.8080607@in.tum.de> <555597A0.50103@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

Hi Andreas,

(ALL x. P x --> foo x) ==> P something ==> P something_more_complicated really the final theorem you are after? Dmitriy On 15.05.2015 08:52, Andreas Lochbihler wrote:

Hi Dmitriy,Thanks for the confirmation that there is no easy solution. Severalmonomorphic copies probably do not scale, because my reasoning willinvolve various instances of the types. So even in simple cases, Ineed at least 10 copies and I'd have to figure out in each case whichcopy I need.What do you think of my axiomatic suggestion? Best, Andreas On 14/05/15 20:04, Dmitriy Traytel wrote:Hi Andreas,if there would be a nice way for doing this in HOL, we could simplifya lot of things inthe BNF package.One approach that comes to mind is to use a locale with severalmonomorphic copies of P(as many as you need to express the propetries). Whether this workswithout being topainful, depends on what you actually are proving. For BNFs we haveused some (trivial)theorems that are preconditioned with something like "M = M1 o M2"which is laterinstantiated with the map_comp theorem (see e.g. src/HOL/BNF_Comp). Best wishes, Dmitriy On 13.05.2015 17:41, Andreas Lochbihler wrote:Dear readers,In Isabelle/HOL, I would like to reason about a polymorphicpredicate P which is closedunder function composition. Since the concrete definition of thepredicate is verytedious and not relevant for the reasoning, I prefer to work justwith the closureproperties of P. However, I have not found a nice way to accomplishthat. Ideas andpointers are welcome.Here are the details. The predicate P should have type "('a => 'b)=> bool" and satisfyproperties such as the following (type variables may be restrictedto 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 theproperties 1-3, because this does not typecheck as P occurs withdifferent typeinstances. Neither does inductive & friends work (for the same reason).I could define "P" as "%_. True" and derive properties 1-3 fromthis. However, mytheorem is of the form(ALL x. P x --> foo x) ==> P something ==> Psomething_more_complicatedwhere the first assumption is folded in a definition. Unfortunately,foo does not holdfor all x. Thus, defining "P" as "%_. True" would allow me to deriveFalse from thefirst assumption. So I could circumvent the actual proof of derivingthe conclusion fromthe second assumption.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 theproperties stated.In my understanding, this should ensure that the axioms do notintroduce inconsistenciesanywhere. Still, as the theorem is proven in a scope where P is onlyaxiomatised, Icannot derive False from the first assumption in its proof. In fact,the theorem alsoholds for the metamodel of HOL in which P is interpreted as thepredicate that I am toolazy to define (provided that it exists at all, but that's anotherissue). 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

**Re: [isabelle] Polymorphic predicate closed under composition***From:*Dmitriy Traytel

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

- Previous by Date: [isabelle] Deadline Extension: Topics in Theoretical Computer Science (TTCS 2015) -- Tehran, Iran
- Next by Date: Re: [isabelle] Polymorphic predicate closed under composition
- Previous by Thread: Re: [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