Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Giving a symbolic name to a tactical

Email Gateway (Aug 18 2022 at 12:23):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,

In my proof, at several positions, there occurs a step like this:
apply (
(intro exI conjI),
(subst (0) m_intro, simp only: m_moves, simp only: m_simps,
(rule compress_u_a[THEN tranclp_into_rtranclp] | rule
elim_use_chain_a[THEN tranclp_into_rtranclp] | erule apply_next_a[THEN
tranclp_into_rtranclp] ))+,
(rule rtranclp.intros),
(subst (0) m_intro, simp only: m_moves, simp only: m_simps,
(rule compress_u_a[THEN tranclp_into_rtranclp] | rule
elim_use_chain_a[THEN tranclp_into_rtranclp] | erule apply_next_a[THEN
tranclp_into_rtranclp] ))+,
(simp add: Un_ac)
)

And I fear this step will even get longer in the future, but it's always
the same step.
Is there a way to give this a symbolic name once, and then refer to the
step via this symbolic name ?

If the only way of doing so should be by converting this to an
ML-tactical [As indicated in Christian Urban's mail of 2007-09-03], then
regard this mail as a feature request:
A nice feature would be:

define my_tactical = tactical_expression

and then use:

apply my_tactical

instead of

apply tactical_expression

Best regards
Peter

Email Gateway (Aug 18 2022 at 12:23):

From: Makarius <makarius@sketis.net>
Just to get the terminology right:

* A tactic is a function that maps a goal state to a lazy sequence of
potential successor state, with ML type tactic = thm -> thm Seq.seq;
tactics with explicit sub-goal addressing are also quite common, and
have type int -> tactic unsurprisingly.

* A tactical is a combinator for tactics, e.g. THEN, ORELSE, REPEAT.

* A proof method (in Isar) is a tactic that refers to an explicit proof
context and a list of immediate facts to be "used" in the goal
refinement.

The ML type is essentially Proof.context -> thm list -> tactic.
Methods handle goal addressing internally. "Methodicals" are limited
to regular expression combinators: ",", "|", "+".

What you descrive above is a way to define your own methods. In
Isabelle/Isar almost everything is "defined" in that sense anyway, and you
can introduce methods on your own. See the 'method_setup' command in the
isar-ref manual or the existing theory sources.

When implementing a method, the implementation body works with ML tactics
and tacticals, wrapped into method syntax.

Makarius

Email Gateway (Aug 18 2022 at 12:24):

From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Peter Lammich wrote:

Hi all,

In my proof, at several positions, there occurs a step like this:
apply (
(intro exI conjI),
(subst (0) m_intro, simp only: m_moves, simp only: m_simps,
(rule compress_u_a[THEN tranclp_into_rtranclp] | rule
elim_use_chain_a[THEN tranclp_into_rtranclp] | erule apply_next_a[THEN
tranclp_into_rtranclp] ))+,
(rule rtranclp.intros),
(subst (0) m_intro, simp only: m_moves, simp only: m_simps,
(rule compress_u_a[THEN tranclp_into_rtranclp] | rule
elim_use_chain_a[THEN tranclp_into_rtranclp] | erule apply_next_a[THEN
tranclp_into_rtranclp] ))+,
(simp add: Un_ac)
)

And I fear this step will even get longer in the future, but it's
always the same step.
Is there a way to give this a symbolic name once, and then refer to
the step via this symbolic name ?

If the only way of doing so should be by converting this to an
ML-tactical [As indicated in Christian Urban's mail of 2007-09-03],
then regard this mail as a feature request:
A nice feature would be:

define my_tactical = tactical_expression

and then use:

apply my_tactical
instead of

apply tactical_expression

Best regards
Peter

Peter,

This is exactly the sort of thing that is readily available in Standard
ML, without requesting any new feature. In fact, ML was originally
conceived to develop proof tactics in the LCF theorem prover (from
which, I gather, HOL and Isabelle originated). In fact, HOL was first
recommended to me, many years ago, on the grounds that it used a "real
language" as its user interface language.

The features designed into ML made it become also a general purpose
functional programming language as well as a user interaction language
for theorem provers.
It remains a highly effective language for combining tactics in various
ways.

Regards,

Jeremy

<http://en.wikipedia.org/wiki/LCF_theorem_prover>
>
>
>
>

Last updated: May 03 2024 at 04:19 UTC