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

Hi Dmitriy,

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 simplify a lot of things in the BNF package. One approach that comes to mind is to use a locale with several monomorphic copies of P (as many as you need to express the propetries). Whether this works without being to painful, depends on what you actually are proving. For BNFs we have used some (trivial) theorems that are preconditioned with something like "M = M1 o M2" which is later instantiated 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 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

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

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

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

- Previous by Date: Re: [isabelle] Document preparation hints
- Next by Date: [isabelle] Deadline Extension: Topics in Theoretical Computer Science (TTCS 2015) -- Tehran, Iran
- 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