Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Question about drule_tac

Email Gateway (Aug 18 2022 at 17:11):

From: Manfred Kerber <M.Kerber@cs.bham.ac.uk>
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@cs.bham.ac.uk |
| The University of Birmingham Tel.: (+44)-121-414-4787 |
| Birmingham, B15 2TT, England Fax.: (+44)-121-414-4281 |
+---------------------------------------------------------------+

Email Gateway (Aug 18 2022 at 17:11):

From: Alexander Krauss <krauss@in.tum.de>
The name "sigma" in (drule_tac sigma = ... in allE) refers to the
variable name in the theorem to be instantiated, that is, allE. So it
must be "x" instead of "sigma".

Hope this helps

Alex

Email Gateway (Aug 18 2022 at 17:11):

From: Tobias Nipkow <nipkow@in.tum.de>
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:

Last updated: Apr 24 2024 at 20:16 UTC