Got rid of alpha_bn_rsp_cheat.
Automatically created functions:+ −
+ −
ty1_tyn.bn[simp] lifted equations for bn funs+ −
ty1_tyn.fv[simp] lifted equations for fv funs+ −
ty1_tyn.perm[simp] lifted permutation equations+ −
ty1_tyn.distinct[simp] lifted distincts+ −
ty1_tyn.eq_iff+ −
ty1_tyn.induct+ −
ty1_tyn.inducts+ −
instance ty1 and tyn :: fs+ −
ty1_tyn.supp empty when for too many bindings+ −
+ −
Smaller things:+ −
+ −
- maybe <type>_perm whould be called permute_<type>.simps;+ −
that would conform with the terminology in Nominal2+ −
+ −
- we also need to lift the size function for nominal+ −
datatypes+ −
+ −
Bigger things:+ −
+ −
- nested recursion, like types "trm list" in a constructor+ −
+ −
- strong induction rules+ −
+ −
- check support equations for more bindings per constructor+ −
+ −
- automate the proofs that are currently proved with sorry:+ −
alpha_equivp+ −
+ −
- store information about defined nominal datatypes, so that+ −
it can be used to define new types that depend on these+ −
+ −
- make parser aware of bn functions that call other bn functions+ −
and reflect it in the datastructure passed to Fv/Alpha generation+ −
+ −
- make parser aware of recursive and of different versions of abs+ −
+ −
Less important:+ −
+ −
- fv_rsp uses 'blast' to show goals of the type:+ −
a u b = c u d ==> a u x u b = c u x u d+ −