Improved support of mutually (recursive) nominal datatypes

[binghe]

This PR fixes #1418 (@mn200's own work).

In case multiple mutually recursive nominal types are being defined, the newly added "witnesses" argument of the API function new_type_step1 provides a list of genind_exists theorems generated from previous calls to the same function, otherwise the proof of term_exists may not succeed.

As a sample application of the improve nomdatatype package, I added the initial theory of my ongoing pi-calculus work, in examples/formal-languages/pi-calculus. There are totally 3 nominal types (mutual but not recursive), expressed in future API Nominal_datatype:

   Nominal_datatype :

           name = Name string

           pi   = Nil                      (* 0 *)
                | Tau pi                   (* tau.P *)
                | Input name ''name pi     (* a(x).P *)
                | Output name name pi      (* {a}b.P *)
                | Match name name pi       (* [a == b] P *)
                | Mismatch name name pi    (* [a <> b] P *)
                | Sum pi pi                (* P + Q *)
                | Par pi pi                (* P | Q *)
                | Res ''name pi            (* nu x. P *)

       residual = TauR pi
                | InputR name ''name pi      (* (Bound) input *)
                | BoundOutput name ''name pi (* Bound output *)
                | FreeOutput name name pi    (* Free output *)
   End

Below are the basic tpm and induction theorems for the :pi type and the FV function for getting free variables:

tpm_thm
⊢ (∀pi. tpm pi Nil = Nil) ∧ (∀pi P. tpm pi (Tau P) = Tau (tpm pi P)) ∧
  (∀x pi a P.
     tpm pi (Input a x P) = Input (npm pi a) (lswapstr pi x) (tpm pi P)) ∧
  (∀pi b a P. tpm pi (Output a b P) = Output (npm pi a) (npm pi b) (tpm pi P)) ∧
  (∀pi b a P. tpm pi (Match a b P) = Match (npm pi a) (npm pi b) (tpm pi P)) ∧
  (∀pi b a P.
     tpm pi (Mismatch a b P) = Mismatch (npm pi a) (npm pi b) (tpm pi P)) ∧
  (∀pi Q P. tpm pi (Sum P Q) = Sum (tpm pi P) (tpm pi Q)) ∧
  (∀pi Q P. tpm pi (Par P Q) = Par (tpm pi P) (tpm pi Q)) ∧
  ∀v pi P. tpm pi (Res v P) = Res (lswapstr pi v) (tpm pi P)

FV_thm
⊢ FV Nil = ∅ ∧ (∀P. FV (Tau P) = FV P) ∧
  (∀x a P. FV (Input a x P) = FV P DELETE x ∪ FV a) ∧
  (∀b a P. FV (Output a b P) = FV a ∪ (FV b ∪ FV P)) ∧
  (∀b a P. FV (Match a b P) = FV a ∪ (FV b ∪ FV P)) ∧
  (∀b a P. FV (Mismatch a b P) = FV a ∪ (FV b ∪ FV P)) ∧
  (∀Q P. FV (Sum P Q) = FV P ∪ FV Q) ∧ (∀Q P. FV (Par P Q) = FV P ∪ FV Q) ∧
  ∀v P. FV (Res v P) = FV P DELETE v

nc_INDUCTION2
⊢ ∀P X.
    P Nil ∧ (∀E. P E ⇒ P (Tau E)) ∧
    (∀a x E. P E ∧ x ∉ X ∧ x # a ⇒ P (Input a x E)) ∧
    (∀a b E. P E ⇒ P (Output a b E)) ∧ (∀a b E. P E ⇒ P (Match a b E)) ∧
    (∀a b E. P E ⇒ P (Mismatch a b E)) ∧ (∀E E'. P E ∧ P E' ⇒ P (Sum E E')) ∧
    (∀E E'. P E ∧ P E' ⇒ P (Par E E')) ∧ (∀y E. P E ∧ y ∉ X ⇒ P (Res y E)) ∧
    FINITE X ⇒
    ∀E. P E

The following theorems show the (correct) built-in alpha conversion of the Input and Res constructors:

Input_eq_thm
⊢ ∀a b x y t1 t2.
    Input a x t1 = Input b y t2 ⇔
    x = y ∧ t1 = t2 ∧ a = b ∨ x ≠ y ∧ x # t2 ∧ t1 = tpm [(x,y)] t2 ∧ a = b

Input_tpm_ALPHA
⊢ v # u ⇒ Input a x u = Input a v (tpm [(v,x)] u)

Res_eq_thm
⊢ ∀u v t1 t2.
    Res u t1 = Res v t2 ⇔
    u = v ∧ t1 = t2 ∨ u ≠ v ∧ u # t2 ∧ t1 = tpm [(u,v)] t2

Res_tpm_ALPHA
⊢ v # u ⇒ Res x u = Res v (tpm [(v,x)] u)

[binghe]

The CI tests may fail if there are other nomdatatype uses beside examples/lambda and examples/CCS. Let's see...

[mn200]

Calls to the changed function in selftest.sml. I assume this should be an easy fix.

[binghe]

Calls to the changed function in selftest.sml. I assume this should be an easy fix.

Should be fixed now.