# Re: [isabelle] dest versus elim?

Dear Freek,
"inductive_cases" generates a new fact from the given formula which you
can inspect e.g. using "thm".
"thm SkipE" reveales
(SKIP, ?s) â ?t â (?t = ?s â ?P) â ?P
which is in "elim-format" i.e., the conclusion is fully general and
unifies with any subgoal and we have a major premise that is eliminated.
Where did you actually see "(SKIP,s) \<Rightarrow> t \<Longrightarrow> t
= s" ?
cheers,
chris
On 03/10/2016 01:51 PM, Freek Wiedijk wrote:
> Dear Chris,
>
> Thanks for your help!
>
> So I did already roughly understand which rules should have a
> "dest" and which should have an "elim". But:
>
> In example files for the Concrete Semantics book, I find
> the following Isabelle code:
>
> text{* What can we deduce from @{prop "(SKIP,s) \<Rightarrow> t"} ?
> That @{prop "s = t"}. This is how we can automatically prove it: *}
>
> inductive_cases SkipE[elim!]: "(SKIP,s) \<Rightarrow> t"
>
> So what I did not understand is why
>
> "(SKIP,s) \<Rightarrow> t \<Longrightarrow> t = s"
>
> is an elimination rule. I would expect this to be a
> destruction rule (adding "t = s" to the assumptions).
> But it says "[elim!]", not "[dest!]"!
>
> So that prompted my question.
>
> Freek
>

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