Re: [isabelle] Parametricity for records



Hi Dmitriy,

That's good to hear. I am looking forward to trying this new command. In the meantime, I'll just define the relator myself.

How do you plan to handle the extensibility of records? Do you lift the BNF over the _ext types and use normal composition or do you plan to introduce constants for _scheme, too? This might also affect the selector issue in my other thread
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00109.html

Best,
Andreas


On 20/07/15 18:40, traytel at in.tum.de wrote:
Hi Andreas,

there is a command in the making that will lift BNFs through typedefs (given that the
predicate is closed under map functions). Since records are type copies this will give you
the relator. Proving parametricity of selectors would be then a next step.

Dmitriy

----- Reply message -----
Von: "Andreas Lochbihler" <andreas.lochbihler at inf.ethz.ch>
An: "isabelle-users" <isabelle-users at cl.cam.ac.uk>
Betreff: [isabelle] Parametricity for records
Datum: Mo., Jul. 20, 2015 09:23


Dear all,

I wonder whether there is any support for parametricity for records in Isabelle/HOL. In
particular, suppose I have a record

   record 'a test = test :: "'a => 'a list"

Then, I would like to get a relator

   rel_test_ext ::
"('a => 'b => bool) => ('m1 => 'm2 => bool)
=> ('a, 'm1) test_ext => ('b, 'm2) test => bool"

and appropriate parametricity rules for the constants generated by the record command. For
example,

   test_parametric: "(rel_test_ext A B ==> A ==> list_all2 A) test test"

Do I have to derive the setup manually or is there some tool support available?

Best,
Andreas





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