Manually added some newer keywords from the distribution
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 bindingsParser 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 typeSmaller 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 anywhereBigger things:- Parser adds syntax for raw datatype, but should add for lifted datatype.- the alpha equivalence for Let as::assn t::trm bind "bn as" in t creates as premise EX pi. as ~~bn as' /\ (bn as, t) ~~lst (bn as', t') but I think it should be as ~~bn as' /\ EX pi. (bn as, t) ~~lst (bn as', t') (both are equivalent, but the second seems to be closer to the fv-function)- when there are more than one shallow binder, then alpha equivalence creates more than one permutation. According to the paper, this is incorrect. Example in Classical.thy.- check whether weirdo example in TestMorePerm works with shallow binders- 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 absLess 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 dWhen cleaning:- remove all 'PolyML.makestring'.