Re: [isabelle] Splitting if-then-else in assumptions?
A note of caution.
The if_split/split_if rule caused some headaches for us in l4v, and is
globally removed from the split set for a number of the theories (which
causes secondary headaches). It's possible if_split_asm would be the
same, though, as you've probably observed, if statements in assumptions
are probably a lot rarer than in conclusions in any case.
On 04/03/16 21:32, Tobias Nipkow wrote:
Currently simp/auto split if-then-else terms if they occur in the
conclusion by default but not if they occur in the assumptions of a
goal. The motivation was the following: inductive proofs of
propositions involving "if" often go astray if the "if" in the IH is
split. However, this situation is not very frequent (the "if" is
typically hidden in some definition) but I frequently need to modify
my simp/auto calls with
split: if_split_asm (* was named split_if_asm until recently *)
Hence I intend to enable "if_split_asm" by default, just like
"if_split", and would like your feedback on this, if you have any.
Why is this not clear cut? According to my tests, the effect is
largely positive (see below). But there is the following usage aspect:
Realizing that if_split_asm should be added is much easier than
realizing that it should be removed: the presence of "if" in an
assumption is the indicator.
Of course this only applies if the user is aware of the existence of
The empirical side look like this. I have converted all of HOL
(locally) with the following results:
- The number of lines mentioning if_split_asm has dropped from 334 to
- The number of lines deleting if_split_asm has gone up from 18 to 54
- In about 15 theories if_split_asm had to be disabled globally
because it broke too much. Typically these are long apply-style proofs.
- Otherwise local "split del" modifiers did the job.
- In a few places proofs became simpler.
In the AFP I only tested 2 articles.
Launchbury: the 4 occurrences of if_split_asm could be removed, that's
Jinja: the 56 occurrences of if_split_asm could be removed, 1 local
split del had to be added.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
This archive was generated by a fusion of
Pipermail (Mailman edition) and