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