[isabelle] Parametricity for records



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.