Lambda term is solvable iff it has hnf (head normal form)

[binghe]

Hi,

This PR continues and connects #1150 and #1155, finally proved Theorem 8.3.14 (Wadsworth) [1, p.175] saying that an λ-term is solvable iff it has hnf (head normal form):

[solvable_iff_has_hnf] (solvableTheory)
⊢ ∀M. solvable M ⇔ has_hnf M

The proof is hard at each lemmas, especially the following one (the case analysis is much more complicated than the textbook version):

[has_hnf_APP_E] (standardisationTheory)
⊢ has_hnf (M @@ N) ⇒ has_hnf M

For easily reasoning of head reduction paths, I have established more lemmas on one-one mapping to list and llist, in the finite and infinite case, resp.:

[infinite_head_reduction_path_to_llist]
⊢ ∀M. infinite (head_reduction_path M) ⇔
      ∃l. ¬LFINITE l ∧ (LNTH 0 l = SOME M) ∧
          ∀i. THE (LNTH i l) -h-> THE (LNTH (SUC i) l)

[finite_head_reduction_path_to_list]
⊢ ∀M. finite (head_reduction_path M) ⇔
      ∃l. l ≠ [] ∧ (HD l = M) ∧ hnf (LAST l) ∧
          ∀i. SUC i < LENGTH l ⇒ EL i l -h-> EL (SUC i) l

[finite_head_reduction_path_to_list_every_has_hnf]
⊢ ∀M. finite (head_reduction_path M) ⇔
      ∃l. l ≠ [] ∧ (HD l = M) ∧ hnf (LAST l) ∧ EVERY has_hnf l ∧
          ∀i. SUC i < LENGTH l ⇒ EL i l -h-> EL (SUC i) l

[finite_head_reduction_path_to_list_last_has_hnf]
⊢ ∀M. finite (head_reduction_path M) ⇔
      ∃l. l ≠ [] ∧ (HD l = M) ∧ has_hnf (LAST l) ∧
          ∀i. SUC i < LENGTH l ⇒ EL i l -h-> EL (SUC i) l

I also added a few new useful lemmas into listTheory and pathTheory, to support some definitions.

--Chun

[1] Barendregt, H.P.: The Lambda Calculus, Its Syntax and Semantics.
College Publications, London (1984).

[mn200]

Thanks for this!