EXTENSIONAL and RESTRICTION ported from HOL-Light

[binghe]

Hi,

This PR ports the useful EXTENSIONAL and RESTRICTION from HOL Light. These concepts are to be used by the porting work (in progress) of HOL-Light's ringtheory.sml.

EXTENSIONAL asserts "extensional" functions, mapping to a fixed value ARB outside the domain:

   [EXTENSIONAL_def]  Definition (combinTheory)      
      ⊢ ∀s f. EXTENSIONAL s f ⇔ ∀x. x ∉ s ⇒ f x = ARB

   [EXTENSIONAL]  Theorem (pred_setTheory)
      ⊢ ∀s. EXTENSIONAL s = {f | ∀x. x ∉ s ⇒ f x = ARB}

On the other hand, RESTRICTION does restriction of a function to an EXTENSIONAL one on a subset:

   [RESTRICTION]  Definition (combinTheory)      
      ⊢ ∀s f x. RESTRICTION s f x = if x ∈ s then f x else ARB

These definitions, together with several supporting lemmas, are added in combinTheory. Then. in relationTheory, the definition of RESTRICT for relations, can now be based on the newly added RESTRICTION (and the original definition then becomes a theorem):

   [RESTRICT]  Definition (relationTheory)      
      ⊢ ∀f R x. RESTRICT f R x = RESTRICTION (λy. R y x) f

   [RESTRICT_DEF]  Theorem      
      ⊢ ∀f R x. RESTRICT f R x = (λy. if R y x then f y else ARB)

The main body of supporting theorems are then added in pred_setTheory, e.g.:

   [EXTENSIONAL_UNIV]  Theorem      
      ⊢ ∀f. EXTENSIONAL 𝕌(:α) f

   [RESTRICTION_EXTENSION]  Theorem      
      ⊢ ∀s f g. RESTRICTION s f = RESTRICTION s g ⇔ ∀x. x ∈ s ⇒ f x = g x

   [RESTRICTION_FIXPOINT]  Theorem      
      ⊢ ∀s f. RESTRICTION s f = f ⇔ f ∈ EXTENSIONAL s

   [RESTRICTION_IDEMP]  Theorem      
      ⊢ ∀s f. RESTRICTION s (RESTRICTION s f) = RESTRICTION s f

   [RESTRICTION_IN_EXTENSIONAL]  Theorem      
      ⊢ ∀s f. RESTRICTION s f ∈ EXTENSIONAL s

--Chun

[mn200]

Thanks for these changes!