1555
|
1 |
Automatically created functions:
|
|
2 |
|
|
3 |
ty1_tyn.bn[simp] lifted equations for bn funs
|
|
4 |
ty1_tyn.fv[simp] lifted equations for fv funs
|
|
5 |
ty1_tyn.perm[simp] lifted permutation equations
|
|
6 |
ty1_tyn.distinct[simp] lifted distincts
|
|
7 |
ty1_tyn.eq_iff
|
|
8 |
ty1_tyn.induct
|
|
9 |
ty1_tyn.inducts
|
|
10 |
instance ty1 and tyn :: fs
|
1573
|
11 |
ty1_tyn.supp empty when for too many bindings
|
1555
|
12 |
|
1501
|
13 |
Smaller things:
|
|
14 |
|
1802
9a32e02cc95b
added small ittems about equivaraince of alpha_gens and name of lam.perm
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
- lam.perm should be called permute_lam.simps (that is
|
9a32e02cc95b
added small ittems about equivaraince of alpha_gens and name of lam.perm
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
the convention from Nominal2)
|
9a32e02cc95b
added small ittems about equivaraince of alpha_gens and name of lam.perm
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
17 |
|
1510
|
18 |
- maybe <type>_perm whould be called permute_<type>.simps;
|
1501
|
19 |
that would conform with the terminology in Nominal2
|
|
20 |
|
1527
|
21 |
- we also need to lift the size function for nominal
|
|
22 |
datatypes
|
1501
|
23 |
|
1802
9a32e02cc95b
added small ittems about equivaraince of alpha_gens and name of lam.perm
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
- Abs.thy contains lemmas for equivariance of the alphas;
|
9a32e02cc95b
added small ittems about equivaraince of alpha_gens and name of lam.perm
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
25 |
they are not yet used anywhere
|
9a32e02cc95b
added small ittems about equivaraince of alpha_gens and name of lam.perm
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
|
1501
|
27 |
Bigger things:
|
|
28 |
|
1808
d7a2c45b447a
added TODO item about parser creating syntax for the wrong type
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
29 |
- Parser adds syntax for raw datatype, but should
|
d7a2c45b447a
added TODO item about parser creating syntax for the wrong type
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
30 |
add for lifted datatype.
|
d7a2c45b447a
added TODO item about parser creating syntax for the wrong type
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
31 |
|
1738
be28f7b4b97b
added an item about alpha-equivalence (the existential should be closer to the abstraction)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
32 |
- the alpha equivalence for
|
be28f7b4b97b
added an item about alpha-equivalence (the existential should be closer to the abstraction)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
33 |
|
be28f7b4b97b
added an item about alpha-equivalence (the existential should be closer to the abstraction)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
34 |
Let as::assn t::trm bind "bn as" in t
|
be28f7b4b97b
added an item about alpha-equivalence (the existential should be closer to the abstraction)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
35 |
|
be28f7b4b97b
added an item about alpha-equivalence (the existential should be closer to the abstraction)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
36 |
creates as premise
|
be28f7b4b97b
added an item about alpha-equivalence (the existential should be closer to the abstraction)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
37 |
|
be28f7b4b97b
added an item about alpha-equivalence (the existential should be closer to the abstraction)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
38 |
EX pi. as ~~bn as' /\ (bn as, t) ~~lst (bn as', t')
|
be28f7b4b97b
added an item about alpha-equivalence (the existential should be closer to the abstraction)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
39 |
|
be28f7b4b97b
added an item about alpha-equivalence (the existential should be closer to the abstraction)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
40 |
but I think it should be
|
be28f7b4b97b
added an item about alpha-equivalence (the existential should be closer to the abstraction)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
41 |
|
be28f7b4b97b
added an item about alpha-equivalence (the existential should be closer to the abstraction)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
42 |
as ~~bn as' /\ EX pi. (bn as, t) ~~lst (bn as', t')
|
be28f7b4b97b
added an item about alpha-equivalence (the existential should be closer to the abstraction)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
43 |
|
be28f7b4b97b
added an item about alpha-equivalence (the existential should be closer to the abstraction)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
44 |
(both are equivalent, but the second seems to be closer to
|
be28f7b4b97b
added an item about alpha-equivalence (the existential should be closer to the abstraction)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
45 |
the fv-function)
|
be28f7b4b97b
added an item about alpha-equivalence (the existential should be closer to the abstraction)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
46 |
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
47 |
- when there are more than one shallow binder, then alpha
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
48 |
equivalence creates more than one permutation. According
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
to the paper, this is incorrect.
|
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
50 |
|
1794
|
51 |
Example in Classical.thy.
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
52 |
|
1794
|
53 |
- check whether weirdo example in TestMorePerm works
|
|
54 |
with shallow binders
|
1792
c29a139410d2
properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
55 |
|
1501
|
56 |
- nested recursion, like types "trm list" in a constructor
|
|
57 |
|
1649
|
58 |
- define permute_bn automatically and prove properties of it
|
|
59 |
|
|
60 |
- prove renaming-of-binders lemmas
|
|
61 |
|
1501
|
62 |
- strong induction rules
|
|
63 |
|
1561
|
64 |
- check support equations for more bindings per constructor
|
1501
|
65 |
|
1649
|
66 |
- For binding functions that call other binding functions
|
1654
|
67 |
the following are proved with cheat_tac: constr_rsp
|
1503
|
68 |
|
|
69 |
- store information about defined nominal datatypes, so that
|
|
70 |
it can be used to define new types that depend on these
|
|
71 |
|
|
72 |
- make parser aware of recursive and of different versions of abs
|
1573
|
73 |
|
|
74 |
Less important:
|
|
75 |
|
|
76 |
- fv_rsp uses 'blast' to show goals of the type:
|
|
77 |
a u b = c u d ==> a u x u b = c u x u d
|
1678
|
78 |
|
|
79 |
When cleaning:
|
|
80 |
|
|
81 |
- remove all 'PolyML.makestring'. |