Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Instantiation problem

Email Gateway (Aug 18 2022 at 10:00):

From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
Hello everybody,
during a proof I have obtained:
(getPc (stof (snd s)) ! (cinc i) = S) /\ getDir (stof (snd s)) ! (cinc i) =
right /\ getPc (stof (snd s)) ! i = ER
where (cinc i)::nat.

Now I want demonstrate the goal:
EX i::nat. ((getPc (stof (snd s)) ! i = S) /\ getDir (stof (snd s)) ! i =
right /\ getPc (stof (snd s)) ! cdec i = ER)

It follow from a simple instantiation ( i <-- (cinc i) ) but I don't find
how to help Isabelle to execute it and using normal proof methods Isabelle
don't find the solution.

Can you help me?

Sorry, I know that this is a very trivial problem but I don't understand it.

Thanks

Gabriele

Email Gateway (Aug 18 2022 at 10:01):

From: Farhad Mehta <fmehta@inf.ethz.ch>
Hi,

try the following :

apply (rule_tac x="cinc i" in exI)

The x comes from the name of the free variable in the rule exI

thm exI

For more details, see section 5.9.6 of the Isabelle tutorial.

Farhad

Last updated: May 03 2024 at 04:19 UTC