Re: [isabelle] Isar-Level cases command



Hi,


Am Dienstag, den 25.11.2014, 11:39 +0100 schrieb Andreas Lochbihler:
> Personally, I do not mind having to state the "show ?case" part, because it makes clear 
> that you really need to do the case distinction to prove the whole case. In fact, I think 
> that your case distinction in the example is not as it should be, because you only need it 
> to for the unfolding of filter.

True, in this sense the example is a bit lacking. And you are rightly
pointing out that fact that for showing an intermediate statement using
case distinction the current scheme is useful. So I would not go as far
to expect that

  cases ("xs")
    case Nil
    have P
  next
    case (Cons x xs')
    have P
  qed

to be equivalent to 

  have P
  proof (cases "xs"))
    case Nil
    have P
  next
    case (Cons x xs')
    have P
  qed

and hence (heh) suggest this feature only for the case (heh) where one
or more actual subgoals are shown (heh) in each case (heh).

(Although I would not dismiss the above if it turns out to be feasible).

Greetings,
Joachim


-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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