README
1basic_swapScript.sml
2 Very basic theory of swaps over strings (the swapstr constant), and
3 permutations (which take a list of pairs of strings to swap). Also
4 defines the NEW constant, which is used everywhere (including in
5 the dB and nc developments above).
6
7nomsetScript.sml
8 A more involved theory of permutations and their actions on
9 arbitrary types (the "nominal sets"). Includes the notion of
10 support.
11
12NEWLib.{sig,sml}
13 simple tactics to use with the NEW constant.
14
15binderLib.{sig,sml}
16 Tools for doing proofs with terms that include binders, including
17 function definition and facilities from NEWLib.
18
19pretermScript.sml termScript.sml
20 Using a quotient over raw syntax from pretermTheory, establishes a
21 type of lambda calculus terms, and defines substitution, the notion
22 of free variable and permutations over that type. Proves some
23 simple lemmas about substitution. For example,
24
25 lemma14a: |- [VAR x/x] t = t
26
27