Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Delving into Isabelle.

Email Gateway (Aug 19 2022 at 09:30):

From: Layus <layus.on@gmail.com>
Hi,

I am currently trying to get a grasp at the internals of Isabelle.
I would like to expose some higher order unification within a proof.

I started with some simple theorem.

theorem Isa : "? P. ( P x & P y )"
apply (intro exI)
apply (intro conjI)
using [[simp_trace]]
apply simp
apply eval (* anything solves True *)
done

This behaves as expected, and shows second order unification,
but I cannot see how the simp tactic gets rid of my first subgoal.

To state it in another way :
What is the magic in HOL that is able to simplify "?P x" into a proven
subgoal.

The trace shows nothing except that the second goal changes from "?P x" to
"True",
which means that somehow "P" got unified with "%x . True".

Any pointer would be welcome.

Best regards,
Guillaume.

Email Gateway (Aug 19 2022 at 09:30):

From: Tobias Nipkow <nipkow@in.tum.de>
Am 16/12/2012 02:24, schrieb Layus:

Hi,

I am currently trying to get a grasp at the internals of Isabelle.
I would like to expose some higher order unification within a proof.

I started with some simple theorem.

theorem Isa : "? P. ( P x & P y )"
apply (intro exI)
apply (intro conjI)
using [[simp_trace]]
apply simp
apply eval (* anything solves True *)
done

This behaves as expected, and shows second order unification,
but I cannot see how the simp tactic gets rid of my first subgoal.

To state it in another way :
What is the magic in HOL that is able to simplify "?P x" into a proven subgoal.

At the end of the simplification process, the simplifier tries to solve the goal
by some trivial means, for example by unifying it with True.

Tobias

The trace shows nothing except that the second goal changes from "?P x" to "True",
which means that somehow "P" got unified with "%x . True".

Any pointer would be welcome.

Best regards,
Guillaume.

Last updated: Nov 21 2024 at 12:39 UTC