[isabelle-dev] set_comprehension_pointfree simproc

[Dmitriy Traytel]

Am 14.03.2014 13:36, schrieb Makarius:
> What is the status of the set_comprehension_pointfree simproc?
>
> In 31afce809794 Dmitriy says "set_comprehension_pointfree simproc 
> causes to many surprises if enabled by default", and in 4d899933a51a 
> I've tried to reconstruct the missing NEWS entry, since this is cleary 
> a user-relevant change.
>
> Looking around in the sources and the history, e.g. 9979d64b8016 where 
> Lukas Bulwahn is "moving simproc from Finite_Set to more appropriate 
> Product_Type theory" shows that there is a related 
> Set_Comprehension_Pointfree.code_simproc still present today 
> http://isabelle.in.tum.de/repos/isabelle/annotate/9979d64b8016/src/HOL/Product_Type.thy#l1127

When working towards 31afce809794, I also tried deactivating this code 
preprocessor, but it was used in some places outside of HOL-Main for 
code generation (e.g. in HOL-IMP).
>
> Does anybody understand how the tool was initially intended to work?  
> Is it feasible to move it just in one place?  Lets say 
> src/HOL/Library/Set_Comprehension_Pointfree.thy, so that the 
> applications that need it can import just that theory, and main HOL 
> remains clear.
Yes, that's a good idea. The is one usage of the simproc in HOL 
(Relation.thy), but this should be easy to get rid of.

Dmitriy