Re: [isabelle] Question about drule_tac



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