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"
â(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
Look, e.g., at
to see examples for more than one case.
Also inductive predicates generate rules in this format, to be applied
with "rule inversion", e.g.
Note that the "proof (cases)" method essentially applies the
corresponding cases rules, and then tries to automatically prove trivial
> A pointer to a relevant book/manual is all I need. And if
> this is too trivial, do not bother the list with this!
This archive was generated by a fusion of
Pipermail (Mailman edition) and