Email Gateway (Aug 18 2022 at 14:54): Email Gateway (Aug 18 2022 at 14:54):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,
I have the following equivalent definitions
definition
"SetMark ij = (case ij of
(I.init, I.loop) => inf (dem Q1_0) (dem Q2_0) |
(I.loop, I.loop) => inf (dem Q3_0) (dem Q4_0) |
(I.loop, I.final) => dem Q5_0 |
_ => top)";
definition
"SetMark = top(
(I.init, I.loop) := inf (dem Q1_0) (dem Q2_0) ,
(I.loop, I.loop) := inf (dem Q3_0) (dem Q4_0) ,
(I.loop, I.final) := dem Q5_0)
I like the style of the first one, however in proofs when I expand
SetMark with
the second definition everything is expanded and I get to basic cases
which are
discharged automatically, while using the first definition I have to do
case_tac
on both first component and second component until I get the result proved.
Is there a way to split the case term in cases automatically, without
using case_tac?
Best regards,
Viorel Preoteasa
Email Gateway (Aug 18 2022 at 14:54):From: Tobias Nipkow <nipkow@in.tum.de>
You can instruct simp/auto/fastsimp/force to split all case expressions
of some type t by adding the option "split: t.split". See the 3.1.9 in
the Tutorial.
Tobias
Viorel Preoteasa schrieb:
Last updated: Apr 25 2024 at 16:19 UTC