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.