Initial work on the theory of solvable terms

[binghe]

Hi,

this PR continues your existing work in examples/lambda, by an initial part of the theory of "solvable" terms (Chapter 8.3 of Barendregt 1984 [1]).

First of all, a (lambda) term is closed if its free variable set (FV) is empty. Since sometimes there's a need of expressing a list of (lambda) terms are all closed. Now I have added the following definition closed_def into termTheory (so that HOL terms like EVERY closed Ns can be used when needed):

[closed_def] (termTheory)
    ⊢ ∀M. closed M ⇔ FV M = ∅

Given any (lambda) term, we can "close" it by wrapping some LAMs with all its free variables, so that the overall FV becomes empty. Due to different order of these free variables, we can only define this the concept of "closure" as a set of terms:

[closures_def] (solvableTheory)
    ⊢ ∀M. closures M = {LAMl vs M | vs | ALL_DISTINCT vs ∧ set vs = FV M}

When the order of free variables is irrelevant, we can arbitrarily choose one from closures M by using the HOL term CHOICE (closures M) (NOTE: this choice is always possible because |- closures M <> EMPTY can be proved), which is overloaded to closure M. In two cases, the set closures M is singleton, as shown in the following two theorems:

[closures_of_closed]
    ⊢ ∀M. closed M ⇒ closures M = {M}
[closures_of_open_sing]
    ⊢ ∀M v. FV M = {v} ⇒ closures M = {LAM v M}

Now, a term is solvable if its closure (any of it), after applying a list of other terms, becomes the "I" combinator (Definition 8.3.1 of [1, p.171]):

[solvable_def]
⊢ ∀M. solvable M ⇔ ∃M' Ns. M' ∈ closures M ∧ M' ·· Ns == I

In particular, for already closed terms, the definition of "solvable" can be simplified without using `closures": (as a theorem)

[solvable_alt_closed]
    ⊢ ∀M. closed M ⇒ (solvable M ⇔ ∃Ns. M ·· Ns == I)

With above definitions, we can prove some common combinators and terms (defined in chap2Theory) are indeed solvable:

[solvable_K]
    ⊢ solvable K
[solvable_Y]
    ⊢ solvable Y
[solvable_xIO]
    ⊢ solvable (VAR x @@ I @@ Ω)

Then we focus on various equivalent alternative definitions of solvable terms. Note that, in the above definitions the list of terms Ns are not required to be closed, but they can be closed when needed in some proofs:

[solvable_alt_closed_every]
    ⊢ ∀M. closed M ⇒ (solvable M ⇔ ∃Ns. M ·· Ns == I ∧ EVERY closed Ns)
[solvable_alt]
    ⊢ ∀M. solvable M ⇔ ∃M' Ns. M' ∈ closures M ∧ M' ·· Ns == I ∧ EVERY closed Ns

Also note that, the existential quantifier ∃Ns used in solvable_def (and all above theorems) can be actually upgraded to universal quantifiers. This result is extremely useful when specific order of free variables is required in certain (future) proofs, and is so far the hardest proof in this PR:

[solvable_alt_universal]
    ⊢ ∀M. solvable M ⇔ ∀M'. M' ∈ closures M ⇒ ∃Ns. M' ·· Ns == I ∧ EVERY closed Ns

Now comes to the Lemma 8.3.3 (i) (M is solvable iff there exists a (closed) substitution instance M' of M and closed terms Ns such that M' @* Ns == I). Closed substitution instance is now defined on top of your ssub (simultaneous substitution based on finite maps):

[closed_substitution_instances_def]
    ⊢ ∀M. closed_substitution_instances M =
      {fm ' M | fm | FDOM fm = FV M ∧ ∀v. v ∈ FDOM fm ⇒ closed (fm ' v)}

Now Lemma 8.3.3 (i) itself is proved:

[solvable_alt_closed_substitution_instance]
    ⊢ ∀M. solvable M ⇔
      ∃M' Ns.
        M' ∈ closed_substitution_instances M ∧ M' ·· Ns == I ∧ EVERY closed Ns

Many new supporting lemmas (for LAMl and ssup) are need, and I have added them into their original theories. The following lemma is hard but very useful, which connects LAMl, appstar and ssub once together:

[LAMl_appstar] (standardisationTheory)
    ⊢ ∀vs M Ns.
    ALL_DISTINCT vs ∧ (LENGTH vs = LENGTH Ns) ∧ EVERY closed Ns ⇒
    LAMl vs M ·· Ns == (FEMPTY |++ ZIP (vs,Ns)) ' M

Besides, in core theory finite_mapTheory, I added the following new lemma for FUN_FMAP:

   [FUN_FMAP_INSERT]  Theorem      
      ⊢ ∀f e s.
          FINITE s ∧ e ∉ s ⇒
          FUN_FMAP f (e INSERT s) = FUN_FMAP f s |+ (e,f e)

And in listTheory, I added "LIST_TO_SET_SING" in addition to "SET_TO_LIST_SING" as the other side of it:

   [LIST_TO_SET_SING]  Theorem      
      ⊢ ∀vs x. ALL_DISTINCT vs ∧ set vs = {x} ⇔ vs = [x]

[1] Barendregt, H.P.: The Lambda Calculus, Its Syntax and Semantics. College Publications, London (1984).

[binghe]

Lemma 8.3.3 (ii) is also done as an additional commit:

[solvable_iff_solvable_LAM]
    ⊢ ∀M x. solvable M ⇔ solvable (LAM x M)

[mn200]

The latter would be better the other way round and made an automatic rewrite with a [simp] annotation.

[binghe]

The latter would be better the other way round and made an automatic rewrite with a [simp] annotation.

Done.

[solvable_iff_solvable_LAM]
    ⊢ ∀M x. solvable (LAM x M) ⇔ solvable M

[mn200]

Thanks!

[binghe]

Also note that now I have added a toplevel examples/lambda/Holmakefile with the following contents: (maybe the build sequence can be slightly simplified)

INCLUDES = barendregt basics other-models typing wcbv-reasonable

The above mentioned sub-directories are those can actually be built, while the others 3 sub-directories (cl, examples, and fsub) are currently broken (no idea how to fix...)