[lambda] Boehm_transform_exists_lemma (Lemma 10.3.6 (ii) [1, p.247])

[binghe]

Hi,

The single purpose of all code changes in this PR, is to prove the surprisingly hard Lemma 10.3.6 (ii) of [Barendregt 1984, p.247]), part of Chapter 10.3 (The Böhm out technology):

After repeated experiments and many rounds of statement changes, the current best proved form is the following: (a better form has been replaced here, the asserted Z is now unique, ISUB has been changed to a single closed substitution, which may well escape from a outer tpm)

[Boehm_transform_exists_lemma] (boehmTheory)
⊢ ∀X M p.
    FINITE X ∧ p ≠ [] ∧ p ∈ ltree_paths (BTe X M) ∧ subterm X M p ≠ NONE ⇒
    ∃pi.
      Boehm_transform pi ∧ solvable (apply pi M) ∧ is_ready (apply pi M) ∧
      ∃Z v N.
        Z = X ∪ FV M ∧ closed N ∧ subterm Z (apply pi M) p ≠ NONE ∧
        tpm_rel (subterm' Z (apply pi M) p) ([N/v] (subterm' Z M p))

where tpm_rel is a new (equivalence) relation on lambda terms, based on tpm:

[tpm_rel_def]
⊢ ∀M N. tpm_rel M N ⇔ ∃pi. tpm pi M = N

[equivalence_tpm_rel]
⊢ equivalence tpm_rel

There are a huge number of new intermediate lemmas added to server the proof of the above lemma. In particular, the facility for generating fresh list of variables, now is called NEWS, has to be updated, and now is put into basic_swapTheory. Its new property (NEWS_prefix) is the key to complete the above lemma.

[NEWS]
⊢ (∀s. NEWS 0 s = []) ∧ ∀n s. NEWS (SUC n) s = NEW s::NEWS n (NEW s INSERT s)

[NEWS_prefix]
⊢ ∀m n s. FINITE s ∧ m ≤ n ⇒ NEWS m s ≼ NEWS n s

In rich_listTheory, I added one more theorem about IS_PREFIX: (with my previous added theorem [IS_PREFIX_EQ_TAKE], the proof is surprisingly straightforward)

[IS_PREFIX_FRONT_MONO]  Theorem (rich_listTheory)
⊢ ∀l1 l2. l1 ≠ [] ∧ l2 ≠ [] ∧ l1 ≼ l2 ⇒ FRONT l1 ≼ FRONT l2

Chun

[1] Barendregt, H.P.: The lambda calculus, its syntax and semantics. College Publications, London (1984).

[binghe]

In boehmTheory the following new addition (canonical_vars) is actually for the new unfinished theorem:

[canonical_vars_def]
⊢ ∀X M.
    canonical_vars X M =
    (let M0 = principle_hnf M; n = LAMl_size M0 in NEWS n (X ∪ FV M0))

[mn200]

Thanks!