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 if_split_asm!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 112. - 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 all.Jinja: the 56 occurrences of if_split_asm could be removed, 1 local split del had to be added.
Any views? Tobias
Description: S/MIME Cryptographic Signature