Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Delving into Isabelle.


view this post on Zulip 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.

view this post on Zulip 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: Mar 28 2024 at 20:16 UTC