Initial boehm_treeTheory (up to dhnf_cases)

[binghe]

Hi,

This PR continues previous work under examples/lambda. It intends to start the theory of Böhm trees but so far I only committed code up to the proof of dhnf_cases (dB version of hnf_cases, explicit form of head normal forms):

dhnf_cases
⊢ ∀M. dhnf M ⇒ ∃n y Ms. M = dABSi n (dV y ·· Ms)

where dhnf is now just an overload to hnf o toTerm. This proof (indirectly) requires a lot of new lemmas about dB versions of LAMl (now renamed to dLAMl for dB terms) and @* (appstar), which is now defined in pure_dBTheory. A key (direct) lemma is the following "transition" lemma from dLAMl to dABSi, FUNPOW of the primitive dABS:

dLAMl_to_dABSi
⊢ ∀vs.
    ALL_DISTINCT vs ⇒
    (let
       n = LENGTH vs;
       body = FOLDL lift t (GENLIST I n);
       phi = ZIP (GENLIST dV n,MAP (λi. i + n) (REVERSE vs))
     in
       dLAMl vs t = dABSi n (body ISUB phi))

Since I also moved some useful theorems upwards, the entire code changes involve many files, and seem already large enough as a stage work for code review. This is also to prevent merge conflicts with potential parallel work.

--Chun

[mn200]

If you cause HTML files to be generated as part of script-file running, can you also clean them up by adding the relevant names to an EXTRA_CLEANS line in the directory's Holmakefile please?

[binghe]

I just modified that EXTRA_CLEANS. I've already done such changes in Holmakefiles in sub-directories of examples/lambda.

[mn200]

I'm confused by

LAMl vs t = dABSi n (body ISUB phi)

This looks as if dABSi is generating a value of type :term. But then I see from looking at the sources that you've overloaded LAMl in pure_dbTheory to be a pure_db-constructing function. Can you make that name dLAMl instead please?

[binghe]

I'm confused by

LAMl vs t = dABSi n (body ISUB phi)

This looks as if dABSi is generating a value of type :term. But then I see from looking at the sources that you've overloaded LAMl in pure_dbTheory to be a pure_db-constructing function. Can you make that name dLAMl instead please?

OK. But what about the "appstar" (@*) that I also overload to the same symbol for :term? I guess this one is not too much confusing thus can be kept?

[mn200]

... [@* for dB terms] ...

I agree this one is an interesting case. Being symbolic I don't see it as confusing as LAMl. I also can't see what the "dB" version of @* would be. In the Unicode syntax, there is a superscript ‘d’ available, so that it might become

  dV i ··ᵈ Ms

but that just seems excessive. And in contexts like the above where the leading token is already dV, I think there's a good chance the reader won't get confused. (Contrast LAMl which is the first thing you see when reading form the left.)

[binghe]

... [@* for dB terms] ...

I agree this one is an interesting case. Being symbolic I don't see it as confusing as LAMl. I also can't see what the "dB" version of @* would be. In the Unicode syntax, there is a superscript ‘d’ available, so that it might become

  dV i ··ᵈ Ms

but that just seems excessive. And in contexts like the above where the leading token is already dV, I think there's a good chance the reader won't get confused. (Contrast LAMl which is the first thing you see when reading form the left.)

Fair enough. Currently we just have no case in which @* (for dB terms) occurs in a confusing way, but let's see what will happen in the future, and your suggestion of putting a d-superscript may be put in use.