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+
−
+
−
Parser should check that:+
−
- types of bindings match types of binding functions+
−
- fsets are not bound in lst bindings+
−
- bound arguments are not datatypes+
−
- binder is referred to by name and not by type+
−
+
−
Smaller things:+
−
+
−
- lam.perm should be called permute_lam.simps (that is +
−
  the convention from Nominal2)+
−
+
−
- 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+
−
+
−
- Abs.thy contains lemmas for equivariance of the alphas;+
−
  they are not yet used anywhere+
−
+
−
Bigger things:+
−
+
−
- Parser adds syntax for raw datatype, but should+
−
  add for lifted datatype.+
−
+
−
- nested recursion, like types "trm list" in a constructor+
−
+
−
- define permute_bn automatically and prove properties of it+
−
+
−
- prove renaming-of-binders lemmas+
−
+
−
- strong induction rules+
−
+
−
- check support equations for more bindings per constructor+
−
+
−
- For binding functions that call other binding functions+
−
  the following are proved with cheat_tac: constr_rsp+
−
+
−
- store information about defined nominal datatypes, so that+
−
  it can be used to define new types that depend on these+
−
+
−
- 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+
−
+
−
When cleaning:+
−
+
−
- remove all 'PolyML.makestring'.+
−