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.