Extract "Boehm_construction" from the proof of subtree_equiv_lemma

[binghe]

Hi,

This follows #1378. With a little more efforts, the construction of the Böhm transformation in the big proof of [subtree_equiv_lemma] can be extracted as the following definition:

Boehm_construction_def
⊢ ∀X Ms p.
    Boehm_construction X Ms p =
    (let
       n_max = MAX_LIST (MAP (λe. subterm_length e p) Ms);
       d_max = MAX_LIST (MAP (λe. subterm_width e p) Ms) + n_max;
       k = LENGTH Ms;
       Y = BIGUNION (IMAGE FV (set Ms));
       vs0 = NEWS (n_max + SUC d_max + k) (X ∪ Y);
       vs = TAKE n_max vs0;
       xs = DROP n_max vs0;
       M i = EL i Ms;
       M0 i = principle_hnf (M i);
       M1 i = principle_hnf (M0 i ·· MAP VAR vs);
       y i = hnf_headvar (M1 i);
       P i = permutator (d_max + i);
       p1 = MAP rightctxt (REVERSE (MAP VAR vs));
       p2 = REVERSE (GENLIST (λi. [P i/y i]) k);
       p3 = MAP rightctxt (REVERSE (MAP VAR xs))
     in
       p3 ++ p2 ++ p1)

And we can obtain an "explicit" form of that lemma in the following form without existential quantifier:

[subtree_equiv_lemma_explicit]
⊢ ∀X Ms p r.
    FINITE X ∧ p ≠ [] ∧ 0 < r ∧ Ms ≠ [] ∧
    BIGUNION (IMAGE FV (set Ms)) ⊆ X ∪ RANK r ∧
    EVERY (λM. subterm X M p r ≠ NONE) Ms ⇒
    (let
       pi = Boehm_construction X Ms p
     in
       Boehm_transform pi ∧ EVERY is_ready' (MAP (apply pi) Ms) ∧
       EVERY (λM. p ∈ ltree_paths (BT' X M r)) (MAP (apply pi) Ms) ∧
       ∀M N q.
         MEM M Ms ∧ MEM N Ms ∧ q ≼ p ⇒
         (subtree_equiv X M N q r ⇔
          subtree_equiv X (apply pi M) (apply pi N) q r))

The previous [subtree_equiv_lemma], of course, can be easily derived from it as a corollary. The definition Boehm_construction is not useful in proving the completeness theorem but can be seen as part of the actual "algorithm" which can separate any two λ-terms, if being further implemented as a library.

--Chun