297 (* nominal_datatype2 does the following things in order:

   298   1) define the raw datatype

   299   2) define the raw binding functions

   300   3) define permutations of the raw datatype and show that raw type is in the pt typeclass

   301   4) define fv and fb_bn

   302   5) define alpha and alpha_bn

   303   6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...)             (Proof by cases; simp)

   304   6) prove alpha_eq_iff    (C1 x = C2 y \<leftrightarrow> P x y ...)

   305      (left-to-right by intro rule, right-to-left by cases; simp)

   306   7) prove bn_eqvt (common induction on the raw datatype)

   307   8) prove fv_eqvt (common induction on the raw datatype with help of above)

   308   9) prove alpha_eqvt and alpha_bn_eqvt

   309      (common alpha-induction, unfolding alpha_gen, permute of #* and =)

   310  10) prove that alpha and alpha_bn are equivalence relations

   311      (common induction and application of 'compose' lemmas)

   312  11) define quotient types

   313  12) prove bn respects     (common induction and simp with alpha_gen)

   314  13) prove fv respects     (common induction and simp with alpha_gen)

   315  14) prove permute respects    (unfolds to alpha_eqvt)

   316  15) prove alpha_bn respects

   317      (alpha_induct then cases then sym and trans of the relations)

   318  16) show that alpha implies alpha_bn (by unduction, needed in following step)

   319  17) prove respects for all datatype constructors

   320      (unfold eq_iff and alpha_gen; introduce zero permutations; simp)

   321  18) define lifted constructors, fv, bn, alpha_bn, permutations

   322  19) lift permutation zero and add properties to show that quotient type is in the pt typeclass

   323  20) lift permutation simplifications

   324  21) lift induction

   325  22) lift fv

   326  23) lift bn

   327  24) lift eq_iff

   328  25) lift alpha_distincts

   329  26) lift fv and bn eqvts

   330  27) prove that union of arguments supports constructors

   331  28) show that the lifted type is in fs typeclass     (* by q_induct, supports *)

   332  29) prove supp = fv

   333 *)