Re: [isabelle] Polymorphic predicate closed under composition
it sounds ok, in the sense that it will not introduce inconsistencies.
What I'm not sure about is how you plan to further work with your
predicate---do you need to integrate it with some other theories or is
(ALL x. P x --> foo x) ==> P something ==> P something_more_complicated
really the final theorem you are after?
On 15.05.2015 08:52, Andreas Lochbihler wrote:
Thanks for the confirmation that there is no easy solution. Several
monomorphic copies probably do not scale, because my reasoning will
involve various instances of the types. So even in simple cases, I
need at least 10 copies and I'd have to figure out in each case which
copy I need.
What do you think of my axiomatic suggestion?
On 14/05/15 20:04, Dmitriy Traytel wrote:
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).
On 13.05.2015 17:41, Andreas Lochbihler wrote:
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
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
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
In my understanding, this should ensure that the axioms do not
anywhere. Still, as the theorem is proven in a scope where P is only
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