# Re: [isabelle] Question about drule_tac

• To: Manfred Kerber <M.Kerber at cs.bham.ac.uk>
• Subject: Re: [isabelle] Question about drule_tac
• From: Tobias Nipkow <nipkow at in.tum.de>
• Date: Fri, 04 Feb 2011 09:25:53 +0100
• Cc: isabelle-users at cl.cam.ac.uk
• References: <20110204081358.3B369E9DF1@maildmz1.informatik.tu-muenchen.de>
• User-agent: Thunderbird 2.0.0.24 (Macintosh/20100228)

```Hi Manfred,

The "in allE" really means that you instantiate variables in "allE", not
in the proof state. The variable in allE is called "x" (more precisely
"?x", but no need to write the "?").

Best
Tobias

Manfred Kerber schrieb:
> Dear All,
>
> Being new to Isabelle I have a question about drule_tac:
>
> I have the following proof state:
>
> --------------------------------------------------------------------------------
> proof (prove): step 9
>
> goal (1 subgoal):
>  1. !!x. [| ALL sigma.
>                perm_on sigma (I n) &
>                (ALL i.
>                    leqv (i : ?C6 x) (sigma i : ?C2.8 x) &
>                    ?x1.10 x i = ?x2.12 x (sigma i)) -->
>                pi (?C6 x) (?x1.10 x) = pi (?C2.8 x) (?x2.12 x);
>             !!n. perm_on (%x. if x = 1 then 2 else if x = 2 then 1 else x)
>                   (I n) |]
>          ==> pi {1} x =
>              pi {2} (%m. x (if m = 1 then 2 else if m = 2 then 1 else m))
> --------------------------------------------------------------------------------
>
> and want apply drule_tac as follows:
> apply(drule_tac sigma = "% y. if y = 1 then 2 else (if y = 2 then 1 else y)"
>        in allE)
>
> in order to instantiate the universally quantified variable sigma with the
> lambda expression %y ...., but get the error:
>
> --------------------------------------------------------------------------------
> *** No such variable in theorem: ?sigma
> *** At command "apply".
> --------------------------------------------------------------------------------
> However when I do a similar thing with the toy example
>
> --------------------------------------------------------------------------------
> theory ToyList
> imports Datatype
> begin
>
> lemma example:
> "(ALL x. P x) & (P a --> Q b) --> Q b"
>
>
> apply(rule impI)
> apply(erule conjE)
> apply(drule_tac x = "a" in allE)
> by auto
> end
> --------------------------------------------------------------------------------
>
> everything works as I except. What do I do wrong? Where can I find
>
> Many thanks
> Manfred
>
> +---------------------------------------------------------------+
> | Manfred Kerber                 URL:    www.cs.bham.ac.uk/~mmk |
> | School of Computer Science     e-mail: M.Kerber at cs.bham.ac.uk |
> | The University of Birmingham   Tel.:   (+44)-121-414-4787     |
> | Birmingham, B15 2TT, England   Fax.:   (+44)-121-414-4281     |
> +---------------------------------------------------------------+

```

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