[isabelle] Question about drule_tac



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
more info on tactics such as drule_tac?

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.