Re: [isabelle] Parametricity for records
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