Re: [isabelle] Isar-Level cases command


Am Dienstag, den 25.11.2014, 10:51 +0100 schrieb Christian Sternagel:
> I think this "use-case" is covered by raw proof blocks. In general I 
> often find that proofs get much more readable when using those (of cause 
> the caveat is that we often have to restate assumptions/their negations, 
> but this can all be handled by tasteful use of "let ?x = ..." before). 
> So here is what I would write:
> lemma "length (filter P xs) ≤ length xs"
> proof (induction xs)
>    case (Cons x xs)
>    { assume "P x"
>      with Cons have "length (filter P (x#xs)) = Suc (length (filter P 
> xs))" by simp
>      also note Cons.IH
>      also have "Suc (length xs) = length (x#xs)" by simp
>      finally have ?case by simp }
>    moreover
>    { assume "¬ P x"
>      with Cons have "length (filter P (x#xs)) = length (filter P xs)" by 
> simp
>      also note Cons.IH
>      also have "length xs ≤ length (x#xs)" by simp
>      finally have ?case . }
>    ultimately show ?case by cases
> qed simp

right. This works ok for boolean cases, but what if my invocation of the
"cases" method is actually a complicate 5-way case distinction on some
expression, or an inductive predicate with multiple variables and lots
of assumptions in each case.

There I really would like to rely on named cases, and that rules out
manual proof blocks.


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

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

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