[isabelle-dev] sets and code generation

[Florian Haftmann]

Hi Christian,

> since set is a proper type some code equations that used to work, no
> longer do, e.g.,
> 
> "op |> = {(x, y). supt_impl x y}"

there is a couple of issues you are hitting at here.

A. The (re-)introduction of the set type constructor

See
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg01736.html
for one possible entry into the motivation and discussion concerning that.

B. The default code generation for setup

You can always turn back to sets-as-predicates by

	code_datatype Collect

and then proving appropriate theorems for the set operation etc. – this
would fir best into a library theory which could then be part of the
distribution.  But I guess your issue is mainly with…

C. Relations

Both kinds of relations 'a => 'a => bool and ('a * 'a) set are present
in their own right, but with disjoint developments in the HOL theoris.
Note that you can convert between both using pred/set conversions, the
same infrastructure as inductive_set is using.

So, if you want predicate relations, it seems to be best to convert your
stuff to them, filling existing gaps in the HOL theories by additional
definitions and suitable pred/set conversion declarations.

See theory "Relation" for examples for making use of pred/set
conversions by means of attributes "to_set" and "to_pred"; and
declarations of pred/set conversions by means of attribute "pred_set_conv".

Unfortunately, there is no reference for them in the Isabelle Reference
Manual.  Maybe one day this is subsumed by an emerging generic »lifting«
infrastructure.

Hope this helps,
	Florian

-- 

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120321/169e6a1f/attachment.sig>