[isabelle-dev] NEWS

[Lawrence Paulson]

I did quite a few of these conversions. Generally the changes were straightforward, EXCEPT for theories that explicitly treated sets as predicates. In the former case, the strategy is to rigorously confine yourself to set primitives, but in the latter case, you may find yourself with a colossal mess.
Larry

On 4 Jan 2012, at 20:18, Florian Haftmann wrote:

>>> 'set' is now a proper type constructor.  Definitions mem_def and
>>> Collect_def have disappeared.  INCOMPATIBILITY, rephrase sets S used as
>>> predicates by `%x. x : S` and predicates P used as sets by `{x. P x}`.
>>> For typical proofs, it is often sufficent to prune any tinkering with
>>> former theorems mem_def and Collect_def.
>> 
>> The NEWS entry looks a bit too optimistic.  The majority of users after
>> Isabelle2008 will have to change their theories, and need some more
>> explicit instructions how to do it sucessfully (e.g. port forwards by
>> eliminating mem_def/Collect_def before making the actual jump into the
>> new version).
> 
> Good question how such explicit instructions could look like.
> Eliminating mem_def/Collect_def in a first pass is usually not feasible,
> because the set/pred-ignorant versions of Isabelle tended to move back
> and forth between both worlds by their automation setup.  The migration
> strategy had always been to adjust terms to respect the set/pred
> distinction, and then adjust the proofs accordingly.  No trick behind it.
> 
> 	Florian
> 
> -- 
> 
> Home:
> http://www.in.tum.de/~haftmann
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev