Re: [isabelle] Parametricity for records
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
On 20/07/15 18:40, traytel at in.tum.de wrote:
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.
----- 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
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
"('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
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and