Re: [isabelle] Parametricity for records



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.