Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Printing instantiations

view this post on Zulip Email Gateway (Aug 18 2022 at 15:30):

From: Steve W <s.wong.731@gmail.com>
Hi all,

I was wondering whether it's possible to print out the instantiations
returned by Thm.first_order_match. Since it returns the type (ctyp * ctyp)
list * (cterm * cterm) list, is there a way to convert this type to a
string? I just want to test it to see what the instantiations look like.
Should I actually bother?

Thanks
Steve

view this post on Zulip Email Gateway (Aug 18 2022 at 15:30):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Steve,

for explorative purpose the ML function PolyML.makestring does a good
job. Any serious printing of logical entities requires weaving the
desired appearance on the ML level, e.g.

fn ts => commas (map (Syntax.string_of_term @{context}) ts)

for printing a list of terms as string. In the system those string
conversions are used rarely, more likely output is assembled by means of
pretty printer entities (type Pretty.T).

fn ts => Pretty.commas (map (Syntax.pretty_term @{context}) ts)

See the pretty.ML, library.ML, and syntax.ML modules for available
combinators.

Hope this helps,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 15:30):

From: Steve W <s.wong.731@gmail.com>
Thanks. I have another question which may require working at the ML level:
If some lemma can be proved at the Isar level, are there ways to extract out
the instantiations of each term in the lemma? Does the proof of the lemma
need to be at the ML level as well?

Thanks
Steve

On Tue, Jun 15, 2010 at 9:17 AM, Florian Haftmann <
florian.haftmann@informatik.tu-muenchen.de> wrote:

Hi Steve,

I was wondering whether it's possible to print out the instantiations
returned by Thm.first_order_match. Since it returns the type (ctyp * ctyp)
list * (cterm * cterm) list, is there a way to convert this type to a
string? I just want to test it to see what the instantiations look like.
Should I actually bother?

for explorative purpose the ML function PolyML.makestring does a good
job. Any serious printing of logical entities requires weaving the
desired appearance on the ML level, e.g.

fn ts => commas (map (Syntax.string_of_term @{context}) ts)

for printing a list of terms as string. In the system those string
conversions are used rarely, more likely output is assembled by means of
pretty printer entities (type Pretty.T).

fn ts => Pretty.commas (map (Syntax.pretty_term @{context}) ts)

See the pretty.ML, library.ML, and syntax.ML modules for available
combinators.

Thanks.

Hope this helps,
Florian

--

Home:
http://www.in.tum.de/~haftmann

PGP available:

http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

view this post on Zulip Email Gateway (Aug 18 2022 at 15:30):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Steve,

I am a little bit lost since I don't understand what you want. A lemma
proposition "as it is" is just a term on its own. So what do you mean
exactly by "instantiation of each term in the lemma"? Have you got an
example Isar snippet?

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 15:30):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Steve,

to inspect proofs, you have to use the image "HOL-Proofs" (containing
proof terms) instead of "HOL" and turn proof objects on by selecting
"Full proofs" from the Isabelle settings menu.

Hope this helps,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 15:30):

From: Makarius <makarius@sketis.net>
Actually, in the still official Isabelle2009-1 distribution you only need
to enable "Full proofs", because the HOL image contains full proofs
already.

For the coming Isabelle2009-2 we had to give up that convenience, because
HOL proofs have grown too fat, so there will be the separate HOL-Proofs
image that has to be build manually.

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 15:31):

From: Lawrence Paulson <lp15@cam.ac.uk>
Nothing ever changes. The prohibitive size of proof terms is the reason Robin Milner invented the LCF approach in the first place. The machine he was using had about 1 MB of memory.
Larry

view this post on Zulip Email Gateway (Aug 18 2022 at 15:31):

From: Randy Pollack <rpollack@inf.ed.ac.uk>
There has been much work on reducing the size of proof terms by the
proof carrying code community.

Randy
--
Quoting Lawrence Paulson <lp15@cam.ac.uk>:

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

view this post on Zulip Email Gateway (Aug 18 2022 at 15:31):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Steve,

how automated proof tools actually accomplish the proof is somehow
magic; if you want to specify single proof steps explicitly, restrict
yourself to proper Isar proofs with methods rule, default etc., see also
the tutorial on Isar. For your example, this could read e.g.

definition c :: real where
ax1: "c = 0"

lemma test: "EX x::real. x = 0"
proof -
from ax1 show "EX x::real. x = 0" ..
qed

Note also that auto won't ever use ax1 in your proof: you need a type
constraint on the existential x, otherwise ax1 is not sufficient.

Hope this helps,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 18 2022 at 15:31):

From: Steve W <s.wong.731@gmail.com>
On Fri, Jun 18, 2010 at 8:13 AM, Florian Haftmann <
florian.haftmann@informatik.tu-muenchen.de> wrote:

Hi Steve,

how automated proof tools actually accomplish the proof is somehow
magic; if you want to specify single proof steps explicitly, restrict
yourself to proper Isar proofs with methods rule, default etc., see also
the tutorial on Isar. For your example, this could read e.g.

definition c :: real where
ax1: "c = 0"

lemma test: "EX x::real. x = 0"
proof -
from ax1 show "EX x::real. x = 0" ..
qed

Thanks. Indeed. If I have something slightly less trivial:

consts
f :: "real => real"
d :: real

axioms
ax1: "f d = 0"

lemma test: "EX (F::real=>real) x. F x = 0"
proof -
from ax1 show ?thesis
..

How come the 'default proof' can't try to instantiate 'F' to 'f' and 'x' to
'd'? I presume there are no rules declared in the current context of this
proof and of your proof, so what exactly does '..' or 'by rule' actually
apply here and in your proof?

Note also that auto won't ever use ax1 in your proof: you need a type
constraint on the existential x, otherwise ax1 is not sufficient.

But doesn't Isabelle support polymorphism? If so, types shouldn't need to be
explicitly declared, right?

Thanks again.
Steve

Hope this helps,
Florian

--

Home:
http://www.in.tum.de/~haftmann

PGP available:

http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

view this post on Zulip Email Gateway (Aug 18 2022 at 15:31):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Steve,

How come the 'default proof' can't try to instantiate 'F' to 'f' and 'x' to
'd'? I presume there are no rules declared in the current context of this
proof and of your proof, so what exactly does '..' or 'by rule' actually
apply here and in your proof?

The ".." proof indeed defaults to (rule exI) in the example. But rule
does only perform one resolution step, hence you have to apply it twice.
Here the proof is given by an apply scripts:

axiomatization f :: "real => real" and d :: real where
ax1: "f d = 0"

lemma test1: "EX (F::real=>real) x. F x = 0"
apply (rule exI)
apply (rule exI)
apply (rule ax1)
done

In Isar the matter is a little bit difficult: we cannot write

from EX x. ... have EX y x. ...

since the "EX x. ..." fact would trigger existential elimination. So we
must write it as backward proof:

lemma test2: "EX (F::real=>real) x. F x = 0"
proof -
from ax1 have *: "EX x. f x = 0" by (rule exI)
show ?thesis by (rule exI) (rule *)
qed

This looks not so beautiful but in practice such chained existential
introduction would be accomplished e.g. by blast.

The details can be found in the tutorial, chapter "The rules of the game".

But doesn't Isabelle support polymorphism? If so, types shouldn't need to be
explicitly declared, right?

These are two different things: polymorphism vs. type inference. Type
inference assigns most general types, which may be more general than
actually wanted.

Hope this helps,
Florian

view this post on Zulip Email Gateway (Aug 18 2022 at 15:32):

From: Steve W <s.wong.731@gmail.com>
Hi Florian,

On Mon, Jun 21, 2010 at 7:55 AM, Florian Haftmann <
florian.haftmann@informatik.tu-muenchen.de> wrote:

This looks not so beautiful but in practice such chained existential
introduction would be accomplished e.g. by blast.

The details can be found in the tutorial, chapter "The rules of the game".

Thanks. Your explanation is very helpful.

But doesn't Isabelle support polymorphism? If so, types shouldn't need to
be
explicitly declared, right?

These are two different things: polymorphism vs. type inference. Type
inference assigns most general types, which may be more general than
actually wanted.

I see. Are there other ways to prevent type inference from assigning types
more general than wanted beside explicitly giving F a specific type?
Ideally, I'd like to existentially quantify over the type of F (and x), but
I think Isabelle/HOL doesn't support quantification over types.

Thanks,
Steve

Hope this helps,
Florian

--

Home:
http://www.in.tum.de/~haftmann

PGP available:

http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

view this post on Zulip Email Gateway (Aug 18 2022 at 15:33):

From: Michael Chan <mchan@inf.ed.ac.uk>
On 17/06/10 09:00, Florian Haftmann wrote:

Hi Steve,

lemma test: "EX x. F x< 0"

How can I extract the instantiation of the variable x? I've tried adding
full_prf; after show ?thesis with apply auto, but I keep getting an
error saying 'minimal proof object'. That said, I actually would like to
obtain the internal representation of the instantiation instead. In
essence, I want to find a way to know that 'x' in the lemma is
instantiated to 'c' and obtain the internal representation of it.

to inspect proofs, you have to use the image "HOL-Proofs" (containing
proof terms) instead of "HOL" and turn proof objects on by selecting
"Full proofs" from the Isabelle settings menu.

On a related question, instead of parsing the full proof and take out
the interesting bits, are there ML functions for directly obtaining the
instantiation of a variable in a proof?

Michael

Hope this helps,
Florian

view this post on Zulip Email Gateway (Aug 18 2022 at 15:34):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Michael,

I am uncertain whether I fully understand your question; there is no
way to avoid full proof terms in order to find out instantiations.

Hope this helps,
Florian
signature.asc

Last updated: Apr 26 2024 at 20:16 UTC