Stage work on the lambda example (BT_subterm_thm, etc.)

[binghe]

Hi,

This PR contains some stage progress for the lambda calculus example, in particular, the relationship between the two accessors (ltree_el and ltree_lookup) of BT (Böhm tree), and subterms. This is basically the first time we actually deal with Böhm trees (previously the focus was mainly on subterms).

In the ltreeTheory, the relationship between ltree_el (returns only the tree node at the end of certain path) and ltree_lookup (returns the entire subtree after passing certain path) is now established with help of monad syntax:

   [ltree_el_alt_ltree_lookup]  Theorem (ltreeTheory)      
      ⊢ ∀p t.
          p ∈ ltree_paths t ⇒
          ltree_el t p =
          do
            t' <- ltree_lookup t p;
            SOME (ltree_node t',LLENGTH (ltree_children t'))
          od

Recall that, a "subterm X M p" is the children term of the generation process of Böhm tree (after passing the path p) at the head normal form LAMl vs (VAR y) @* args (EL n args is the subterm, assuming the last number in the list p is n). Previously, the relationship between subterm and ltree_lookup has been established by the following (renamed) lemma: (i.e. the BT of subterm is the subtree of BT of the original term)

[BT_subterm_lemma] (boehmTheory)
⊢ ∀p X M.
    FINITE X ∧ subterm X M p ≠ NONE ⇒
    BT (THE (subterm X M p)) = THE (ltree_lookup (BTe X M) p)

Now, with help of the above [ltree_el_alt_ltree_lookup], I can directly prove the following (dirty) connecting theorem (between ltree_el and subterm) without doing induction:

BT_subterm_thm
⊢ ∀p X M.
    FINITE X ∧ subterm X M p ≠ NONE ∧ solvable (subterm' X M p) ⇒
    do
      (t,m) <- ltree_el (BTe X M) p;
      (Z,N) <- subterm X M p;
      (xs,y) <- t;
      M0 <<- principle_hnf N;
      n <<- LAMl_size M0;
      vs <<- NEWS n (Z ∪ FV M0);
      M1 <<- principle_hnf (M0 ·· MAP VAR vs);
      SOME (vs = xs ∧ hnf_headvar M1 = y ∧ hnf_children_size M1 = THE m)
    od = SOME T

The above theorem will play a key role in proving the following "agree_upto" lemma (still in progress):

agree_upto_lemma (in progress, not contained in this PR)
⊢ ∀X Ms p.
    FINITE X ∧ p ≠ [] ∧ EVERY (λe. subterm X e p ≠ NONE) Ms ∧ agree_upto p Ms ⇒
    ∃pi.
      Boehm_transform pi ∧ EVERY is_ready (MAP (apply pi) Ms) ∧
      agree_upto p (MAP (apply pi) Ms)

This PR contains also some more properties about the lambda permutator for their head reductions in different situations, used by the in-progress proofs.

The head_reductionScript.sml was cleaned up and updated with loose equality removed. Since the total changes involve many files, I think it's better to get the current stage work reviewed before the next major stage.

--Chun

[binghe]

Oh, I forgot the mention that, the previously added script under examples/lambda/completeness is no more useful (thus deleted), since it's now clear that de Bruijn encodings won't be used in this work.

[mn200]

Thanks for this!