[isabelle] Splitting if-then-else in assumptions?



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 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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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