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

It would improve uniformity.

Tobias




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