[rich_list] Added IS_PREFIX_FINITE, etc. (The set of prefixes is finite)

[binghe]

Hi,

Today I was in the need of the following theorem stating that "the set of all prefixes of a given list, is finite":

   [IS_PREFIX_FINITE]  Theorem   
      ⊢ ∀l. FINITE {l1 | l1 ≼ l}

My idea of the proof is based on rewriting IS_PREFIX to TAKE (and then use IMAGE_FINITE to finish the proof):

   [IS_PREFIX_EQ_TAKE]  Theorem
      ⊢ ∀l l1. l1 ≼ l ⇔ ∃n. n ≤ LENGTH l ∧ l1 = TAKE n l

   [IS_PREFIX_EQ_TAKE']  Theorem
      ⊢ ∀l l1. l1 ≼ l ⇔ ∃n. l1 = TAKE n l

The above theorems are to be added into rich_listTheory.

But then this makes me wonder how to prove that "the set of all sublists of a list is finite", i.e. ∀l. FINITE {l1 | IS_SUBLIST l l1}? (I can imagine that a sublist may be obtained by first do a TAKE and then a DROP, or in reversed order, thus leads to finite number of possibilities, but this proof seems not easy)

This will subsume the above IS_PREFIX_FINITE, since we have:

   [IS_PREFIX_IS_SUBLIST]  Theorem      
      ⊢ ∀l1 l2. l2 ≼ l1 ⇒ IS_SUBLIST l1 l2

Furthermore, IS_SUFFIX_FINITE can be easily proved too, if we know "the set of all subsets of a list is finite", before suffix is also a sublist:

   [IS_SUFFIX_IS_SUBLIST]  Theorem      
      ⊢ ∀l1 l2. IS_SUFFIX l1 l2 ⇒ IS_SUBLIST l1 l2

[mn200]

That theorem is already present in rich_listTheory under name FINITE_prefix, but the characterisations of prefix in terms of TAKE might still be useful.

[binghe]

Ah, thanks, I didn't see FINITE_prefix. After your addition of FINITE_BOUNDED_LISTS, I think all similar results (for suffix and sublists) are now quite obvious. I have deleted IS_PREFIX_FINITE and only kept the IS_PREFIX_EQ_TAKE and IS_PREFIX_EQ_TAKE' in the code changes.

[mn200]

Thanks!