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



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

I have no strong opinion about the naming schema itself, but it should
be uniform afterwards.

Also note that the situation with sum and prod and sets is a little
delicate and demands a suffix pattern due to interpretation, e.g.
foo.strong_cong.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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