another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
Function definitions+ −
+ −
- nominal_datatype should export proofs about alpha_bn: reflexivity, induction, ...?+ −
+ −
- nominal_datatype should declare xxx.fv_bn_eqvt as [eqvt]+ −
+ −
- equations that talk about True/False, for example+ −
| "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)"+ −
do not work (since 'function' does not work)+ −
+ −
- equivariance for functions can be derived automatically (knowing termination and+ −
equivariance of the graph).+ −
+ −
- for multiple simultanously defined functions, compatibility cases should fold the+ −
definition and derive eqvt_at for the folded one+ −
+ −
- equivariance of the graph for multiple functions does not use equivariance+ −
infrastructure+ −
+ −
Nominal_Datatype 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:+ −
+ −
- maybe <t1_t2>.perm_simps should be called permute_<type>.simps;+ −
that would conform with the terminology in Nominal2+ −
+ −
- nominal_induct does not work without an induction rule+ −
+ −
- nominal_induct throws strange "THM" exceptions if not enough+ −
variables are given+ −
+ −
- nominal_induct cannot avoid a term (for example function applied+ −
to an argument).+ −
+ −
- .induct and .exhaust could be the default methods for induction/cases+ −
on nominal datatypes+ −
+ −
Other:+ −
+ −
- nested recursion, like types "trm list" in a constructor+ −
+ −
- store information about defined nominal datatypes, so that+ −
it can be used to define new types that depend on these+ −
+ −