# Re: [isabelle] dest versus elim?

> In the example files for Concrete Semantics, I see lemmas
> (for example "SkipE") that are proved with "[elim]", but
> where I think that you do not only want to use them when
> their conclusion unifies with the goal?
Do you mean?
inductive_cases SkipE[elim!]: "(SKIP,s) â t"
thm SkipE
â(SKIP, ?s) â ?t; ?t = ?s â ?Pâ â ?P
This is a standard pattern for case distinction, that you see all over
Isabelle. It is also produced by "obtains".
For SKIP, there is only one case, namely t=s.
The intuition is as follows:
If the premise contains a (SKIP,s) => t, this rule will unify with any
conclusion P, and what remains to proof is "t=s ==> P" ... the SKIP is
gone.
Look, e.g., at
thm list.set_cases
to see examples for more than one case.
Also inductive predicates generate rules in this format, to be applied
with "rule inversion", e.g.
thm big_step.cases
Note that the "proof (cases)" method essentially applies the
corresponding cases rules, and then tries to automatically prove trivial
goals.
--
Peter
>
> A pointer to a relevant book/manual is all I need. And if
> this is too trivial, do not bother the list with this!
>
> Freek
>

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*