A lemma about substitution in TypeSchemes.
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.+ −
+ −
- 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 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'.+ −