```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.