[lambda] ltree_finite_BT_bnf (by ltree_finite_by_unfolding)

[binghe]

Hi,

This PR adds some more useful lemmas into ltreeTheory and further pushed the lambda example.

If an ltree is generated by unfolding (ltree_unfold), and the unfolding seeds have a decreasing "measure", then the resulting ltree must be finite:

   [ltree_finite_by_unfolding']  Theorem (ltreeTheory)
      ⊢ ∀f. (∃m. ∀seed.
               (let
                  (a,seeds) = f seed
                in
                  LFINITE seeds ∧ every (λe. m e < m seed) seeds)) ⇒
            ∀seed. ltree_finite (ltree_unfold f seed)

In a more general version, an extra predicate P is used to restrict the involved seeds:

   [ltree_finite_by_unfolding]  Theorem      
      ⊢ ∀P f.
          (∃m. ∀seed.
             P seed ⇒
             (let
                (a,seeds) = f seed
              in
                LFINITE seeds ∧ every (λe. P e ∧ m e < m seed) seeds)) ⇒
          ∀seed. P seed ⇒ ltree_finite (ltree_unfold f seed)

By the above result, I have proved that Böhm trees of β-normal forms (of λ-terms) are finite:

[ltree_finite_BT_bnf] (examples/lambda/barendregt/lameta_completeTheory)
⊢ ∀X M r. FINITE X ∧ FV M ⊆ X ∪ RANK r ∧ bnf M ⇒ ltree_finite (BT' X M r)

Furthermore, if a λ-term M just has β-normal form, say, M0, then M and M0 are β-equivalent, thus have the same Böhm tree, which is finite:

[ltree_finite_BT_has_bnf]
⊢ ∀X M r. FINITE X ∧ FV M ⊆ X ∪ RANK r ∧ has_bnf M ⇒ ltree_finite (BT' X M r)

The finiteness of Βöhm trees are necessary for their conversion to Rose tree as input of recursive functions (for building the original term from the tree).

P. S. Similar results for λ-terms who are or just have βη-normal forms are not proved yet, but the proof will use the above proven results.

--Chun

[binghe]

Added:

[ltree_finite_BT_benf]
⊢ ∀X M r. FINITE X ∧ FV M ⊆ X ∪ RANK r ∧ benf M ⇒ ltree_finite (BT' X M r)
[ltree_finite_BT_has_benf]
⊢ ∀X M r. FINITE X ∧ FV M ⊆ X ∪ RANK r ∧ has_benf M ⇒ ltree_finite (BT' X M r)

Actually the proof is not as hard as I thought before, given |- has_benf M <=> has_bnf M.

[mn200]

Thanks!