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

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



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