Re: [isabelle] tactical combinators

It sounds like you need THEN_ALL_NEW, which is generally pretty useful.

So you can write your tactic a bit like this. I'm referring to your stage (1) as tac2.

fun tac arg n =
  (etac erule_thm n
  THEN (tac2 THEN_ALL_NEW tac 1) (n + 2)
  THEN (tac2 THEN_ALL_NEW tac 2) (n + 1)
  THEN (tac2 THEN_ALL_NEW tac 3) n

That's a bit ugly, obviously, you could clean up the repetition with some kind of EVERY.

BTW, passing different parameters to tac positionally can work well, but always consider whether it's possible to figure out what to do by inspecting the goal state with SUBGOAL or similar, giving you tactics that are easier to compose.


From: cl-isabelle-users-bounces at [cl-isabelle-users-bounces at] On Behalf Of Abderrahmane FELIACHI [Abderrahmane.Feliachi at]
Sent: Sunday, June 05, 2011 8:41 AM
To: cl-isabelle-users at
Subject: [isabelle] tactical combinators

Hi all,

I'm trying to write the (recursive) tactic described as below:

A    - apply some elimination rule to the subgoal n producing 3 subgoals
(n, n+1, n+2), then :
       1  - simultaneously apply some elimination rules to the 3
subgoals. then
       2  - apply the same tactic to the 3 subgoals (with different
parameters for each case).

My problem is that when applying the elimination rules in 1, this can
lead to 0 or more subgoals,
so I cannot apply the tactics in 2 to the subgoals (n, n+1, n+2).

My question is: Wich combinator should I use in step 1 and 2 in order to
apply (locally) these steps with rules (n, n+1, n+2) whatever the result
of applying the rule 1.

Thanks a lot,


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.