separated general nominal theory into separate folder
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 bindingsSmaller 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 datatypesBigger things:- 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)- 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'.