Re: [isabelle] op =simp=> in congruence rules



On 12.08.2014 14:30, Jasmin Christian Blanchette wrote:
Hi Andreas,

Thanks for your thorough investigation.

In conclusion, =simp=> does not break anything in the tested theories when map_cong is used as a congruence rule. Since [fundef_cong] does not handle =simp=> and map_cong seems to be useful in some cases (2a,b), we should keep the version with ==>. Possibly, BNF could also generate the congruence rule list.strong_map_cong with =simp=>. The name follow the existing naming convention for ball, bex, SUP, INF, ... (Although I would prefer map_cong_strong because the main operator does not hide somewhere in the middle of the theorem name.)
Good idea. I would also prefer "_strong" as a suffix, for consistency with other "_strong"ly-suffixed properties in BNF. We'll add it to our list. If nobody objects, I could also rename "strong_ball_cong" etc. to "ball_cong_strong" etc. (once Isabelle2014 is out).
I would even argue that there is nothing "strong" about those rules (since op =simp=> = op ==>). So if renaming anyway, maybe ball_cong_simp or even ball_cong_simp_implies is a better name?

Dmitriy




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