Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Automatic case splitting for Isar proofs with ...

Email Gateway (Aug 19 2022 at 11:24):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Benedikt,

"case splitting" is a too general term here, because only tuples of fixed variables are
expanded to their components. You can achieve the same effect by unfolding with
split_paired_all:

lemma "P (while b c (x,y))"
proof(rule while_rule, unfold split_paired_all)

Hope this helps,
Andreas

Last updated: Apr 19 2024 at 12:27 UTC