Stage work on λ-calculus (Böhm transform and head original terms)

[binghe]

Hi,

This is the last piece of (easy) work on λ-calculus mechanisation, before Böhm trees are first involved.

If a head normal form (hnf) is given by M := LAMl vs (VAR y @* Ns) , then:

• It is λ-free if LENGTH vs = 0 (or vs = []), or just ~is_abs M
• It is head original if y is not free in any hnf children term, i.e. !N. MEM N Ns ==> y # N,
• It's ready if it's either unsolvable or has a λ-free and head original hnf.

Due to α-conversions, without using dB encodings the concept head_original has to be defined in the following complicated way, by calling principle_hnf once to remove the potential outer abstractions of input term: (NOTE: hnf_headvar M1 is an overload to THE_VAR (hnf_head M1), where THE_VAR (VAR y) = y is currently put in chap2Theory)

head_original_def
⊢ ∀M0.
    head_original M0 ⇔
    (let
       n = LAMl_size M0;
       vs = FRESH_list n (FV M0);
       M1 = principle_hnf (M0 ·· MAP VAR vs)
     in
       EVERY (λe. hnf_headvar M1 # e) (hnf_children M1))

while the definition is_ready is relatively easy and straightforward:

is_ready_def
⊢ ∀M. is_ready M ⇔
      unsolvable M ∨ ∃N. M == N ∧ hnf N ∧ ¬is_abs N ∧ head_original N

But then, I managed to eliminate head_original and prove the following easier "equivalent definition" of is_ready:

is_ready_alt
⊢ ∀M. is_ready M ⇔
      unsolvable M ∨ ∃y Ns. M == VAR y ·· Ns ∧ EVERY (λe. y # e) Ns

With the above definitions, the following stage lemma (Lemma 10.3.6 (i), page 247 of [Barengredt 1984]) is proved, saying for any λ-term there exists a Böhm transform π such that π(M) is ready.

Boehm_transform_is_ready_exists
⊢ ∀M. ∃pi. Boehm_transform pi ∧ is_ready (apply pi M)

P. S. The next lemma, Lemma 10.3.6 (ii) will show that, for any λ-term M, there exists a Böhm transform π to access any node (at path α) of the Böhm tree BT(M), the resulting term is a substitution instance of the actual tree node, and is ready.

--Chun