src/HOL/Nominal/nominal_package.ML
author urbanc
Wed Nov 02 11:02:29 2005 +0100 (2005-11-02)
changeset 18054 2493cb9f5ede
parent 18045 6d69a4190eb2
child 18066 d1e47ee13070
permissions -rw-r--r--
added the collection of lemmas "supp_at"
     1 (* $Id$ *)
     2 
     3 signature NOMINAL_PACKAGE =
     4 sig
     5   val create_nom_typedecls : string list -> theory -> theory
     6   val add_nominal_datatype : bool -> string list -> (string list * bstring * mixfix *
     7     (bstring * string list * mixfix) list) list -> theory -> theory *
     8       {distinct : thm list list,
     9        inject : thm list list,
    10        exhaustion : thm list,
    11        rec_thms : thm list,
    12        case_thms : thm list list,
    13        split_thms : (thm * thm) list,
    14        induction : thm,
    15        size : thm list,
    16        simps : thm list}
    17   val setup : (theory -> theory) list
    18 end
    19 
    20 structure NominalPackage (*: NOMINAL_PACKAGE *) =
    21 struct
    22 
    23 open DatatypeAux;
    24 
    25 (* data kind 'HOL/nominal' *)
    26 
    27 structure NominalArgs =
    28 struct
    29   val name = "HOL/nominal";
    30   type T = unit Symtab.table;
    31 
    32   val empty = Symtab.empty;
    33   val copy = I;
    34   val extend = I;
    35   fun merge _ x = Symtab.merge (K true) x;
    36 
    37   fun print sg tab = ();
    38 end;
    39 
    40 structure NominalData = TheoryDataFun(NominalArgs);
    41 
    42 fun atoms_of thy = map fst (Symtab.dest (NominalData.get thy));
    43 
    44 (* FIXME: add to hologic.ML ? *)
    45 fun mk_listT T = Type ("List.list", [T]);
    46 fun mk_permT T = mk_listT (HOLogic.mk_prodT (T, T));
    47 
    48 fun mk_Cons x xs =
    49   let val T = fastype_of x
    50   in Const ("List.list.Cons", T --> mk_listT T --> mk_listT T) $ x $ xs end;
    51 
    52 
    53 (* this function sets up all matters related to atom-  *)
    54 (* kinds; the user specifies a list of atom-kind names *)
    55 (* atom_decl <ak1> ... <akn>                           *)
    56 fun create_nom_typedecls ak_names thy =
    57   let
    58     (* declares a type-decl for every atom-kind: *) 
    59     (* that is typedecl <ak>                     *)
    60     val thy1 = TypedefPackage.add_typedecls (map (fn x => (x,[],NoSyn)) ak_names) thy;
    61     
    62     (* produces a list consisting of pairs:         *)
    63     (*  fst component is the atom-kind name         *)
    64     (*  snd component is its type                   *)
    65     val full_ak_names = map (Sign.intern_type (sign_of thy1)) ak_names;
    66     val ak_names_types = ak_names ~~ map (Type o rpair []) full_ak_names;
    67      
    68     (* adds for every atom-kind an axiom             *)
    69     (* <ak>_infinite: infinite (UNIV::<ak_type> set) *)
    70     val (thy2,inf_axs) = PureThy.add_axioms_i (map (fn (ak_name, T) =>
    71       let 
    72 	val name = ak_name ^ "_infinite"
    73         val axiom = HOLogic.mk_Trueprop (HOLogic.mk_not
    74                     (HOLogic.mk_mem (HOLogic.mk_UNIV T,
    75                      Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T)))))
    76       in
    77 	((name, axiom), []) 
    78       end) ak_names_types) thy1;
    79     
    80     (* declares a swapping function for every atom-kind, it is         *)
    81     (* const swap_<ak> :: <akT> * <akT> => <akT> => <akT>              *)
    82     (* swap_<ak> (a,b) c = (if a=c then b (else if b=c then a else c)) *)
    83     (* overloades then the general swap-function                       *) 
    84     val (thy3, swap_eqs) = foldl_map (fn (thy, (ak_name, T)) =>
    85       let
    86         val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
    87         val swap_name = Sign.full_name (sign_of thy) ("swap_" ^ ak_name);
    88         val a = Free ("a", T);
    89         val b = Free ("b", T);
    90         val c = Free ("c", T);
    91         val ab = Free ("ab", HOLogic.mk_prodT (T, T))
    92         val cif = Const ("HOL.If", HOLogic.boolT --> T --> T --> T);
    93         val cswap_akname = Const (swap_name, swapT);
    94         val cswap = Const ("nominal.swap", swapT)
    95 
    96         val name = "swap_"^ak_name^"_def";
    97         val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
    98 		   (cswap_akname $ HOLogic.mk_prod (a,b) $ c,
    99                     cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))
   100         val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
   101       in
   102         thy |> Theory.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
   103             |> (#1 o PureThy.add_defs_i true [((name, def2),[])])
   104             |> PrimrecPackage.add_primrec_i "" [(("", def1),[])]            
   105       end) (thy2, ak_names_types);
   106     
   107     (* declares a permutation function for every atom-kind acting  *)
   108     (* on such atoms                                               *)
   109     (* const <ak>_prm_<ak> :: (<akT> * <akT>)list => akT => akT    *)
   110     (* <ak>_prm_<ak> []     a = a                                  *)
   111     (* <ak>_prm_<ak> (x#xs) a = swap_<ak> x (perm xs a)            *)
   112     val (thy4, prm_eqs) = foldl_map (fn (thy, (ak_name, T)) =>
   113       let
   114         val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
   115         val swap_name = Sign.full_name (sign_of thy) ("swap_" ^ ak_name)
   116         val prmT = mk_permT T --> T --> T;
   117         val prm_name = ak_name ^ "_prm_" ^ ak_name;
   118         val qu_prm_name = Sign.full_name (sign_of thy) prm_name;
   119         val x  = Free ("x", HOLogic.mk_prodT (T, T));
   120         val xs = Free ("xs", mk_permT T);
   121         val a  = Free ("a", T) ;
   122 
   123         val cnil  = Const ("List.list.Nil", mk_permT T);
   124         
   125         val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (qu_prm_name, prmT) $ cnil $ a, a));
   126 
   127         val def2 = HOLogic.mk_Trueprop (HOLogic.mk_eq
   128                    (Const (qu_prm_name, prmT) $ mk_Cons x xs $ a,
   129                     Const (swap_name, swapT) $ x $ (Const (qu_prm_name, prmT) $ xs $ a)));
   130       in
   131         thy |> Theory.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)] 
   132             |> PrimrecPackage.add_primrec_i "" [(("", def1), []),(("", def2), [])]
   133       end) (thy3, ak_names_types);
   134     
   135     (* defines permutation functions for all combinations of atom-kinds; *)
   136     (* there are a trivial cases and non-trivial cases                   *)
   137     (* non-trivial case:                                                 *)
   138     (* <ak>_prm_<ak>_def:  perm pi a == <ak>_prm_<ak> pi a               *)
   139     (* trivial case with <ak> != <ak'>                                   *)
   140     (* <ak>_prm<ak'>_def[simp]:  perm pi a == a                          *)
   141     (*                                                                   *)
   142     (* the trivial cases are added to the simplifier, while the non-     *)
   143     (* have their own rules proved below                                 *)  
   144     val (thy5, perm_defs) = foldl_map (fn (thy, (ak_name, T)) =>
   145       foldl_map (fn (thy', (ak_name', T')) =>
   146         let
   147           val perm_def_name = ak_name ^ "_prm_" ^ ak_name';
   148           val pi = Free ("pi", mk_permT T);
   149           val a  = Free ("a", T');
   150           val cperm = Const ("nominal.perm", mk_permT T --> T' --> T');
   151           val cperm_def = Const (Sign.full_name (sign_of thy') perm_def_name, mk_permT T --> T' --> T');
   152 
   153           val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def";
   154           val def = Logic.mk_equals
   155                     (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)
   156         in
   157           thy' |> PureThy.add_defs_i true [((name, def),[])] 
   158         end) (thy, ak_names_types)) (thy4, ak_names_types);
   159     
   160     (* proves that every atom-kind is an instance of at *)
   161     (* lemma at_<ak>_inst:                              *)
   162     (* at TYPE(<ak>)                                    *)
   163     val (thy6, prm_cons_thms) = 
   164       thy5 |> PureThy.add_thms (map (fn (ak_name, T) =>
   165       let
   166         val ak_name_qu = Sign.full_name (sign_of thy5) (ak_name);
   167         val i_type = Type(ak_name_qu,[]);
   168 	val cat = Const ("nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
   169         val at_type = Logic.mk_type i_type;
   170         val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy5
   171                                   [Name "at_def",
   172                                    Name (ak_name ^ "_prm_" ^ ak_name ^ "_def"),
   173                                    Name (ak_name ^ "_prm_" ^ ak_name ^ ".simps"),
   174                                    Name ("swap_" ^ ak_name ^ "_def"),
   175                                    Name ("swap_" ^ ak_name ^ ".simps"),
   176                                    Name (ak_name ^ "_infinite")]
   177 	    
   178 	val name = "at_"^ak_name^ "_inst";
   179         val statement = HOLogic.mk_Trueprop (cat $ at_type);
   180 
   181         val proof = fn _ => auto_tac (claset(),simp_s);
   182 
   183       in 
   184         ((name, standard (Goal.prove thy5 [] [] statement proof)), []) 
   185       end) ak_names_types);
   186 
   187     (* declares a perm-axclass for every atom-kind               *)
   188     (* axclass pt_<ak>                                           *)
   189     (* pt_<ak>1[simp]: perm [] x = x                             *)
   190     (* pt_<ak>2:       perm (pi1@pi2) x = perm pi1 (perm pi2 x)  *)
   191     (* pt_<ak>3:       pi1 ~ pi2 ==> perm pi1 x = perm pi2 x     *)
   192      val (thy7, pt_ax_classes) =  foldl_map (fn (thy, (ak_name, T)) =>
   193       let 
   194 	  val cl_name = "pt_"^ak_name;
   195           val ty = TFree("'a",["HOL.type"]);
   196           val x   = Free ("x", ty);
   197           val pi1 = Free ("pi1", mk_permT T);
   198           val pi2 = Free ("pi2", mk_permT T);
   199           val cperm = Const ("nominal.perm", mk_permT T --> ty --> ty);
   200           val cnil  = Const ("List.list.Nil", mk_permT T);
   201           val cappend = Const ("List.op @",mk_permT T --> mk_permT T --> mk_permT T);
   202           val cprm_eq = Const ("nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
   203           (* nil axiom *)
   204           val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq 
   205                        (cperm $ cnil $ x, x));
   206           (* append axiom *)
   207           val axiom2 = HOLogic.mk_Trueprop (HOLogic.mk_eq
   208                        (cperm $ (cappend $ pi1 $ pi2) $ x, cperm $ pi1 $ (cperm $ pi2 $ x)));
   209           (* perm-eq axiom *)
   210           val axiom3 = Logic.mk_implies
   211                        (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
   212                         HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
   213       in
   214         thy |> AxClass.add_axclass_i (cl_name, ["HOL.type"])
   215                 [((cl_name^"1", axiom1),[Simplifier.simp_add_global]), 
   216                  ((cl_name^"2", axiom2),[]),                           
   217                  ((cl_name^"3", axiom3),[])]                          
   218       end) (thy6,ak_names_types);
   219 
   220     (* proves that every pt_<ak>-type together with <ak>-type *)
   221     (* instance of pt                                         *)
   222     (* lemma pt_<ak>_inst:                                    *)
   223     (* pt TYPE('x::pt_<ak>) TYPE(<ak>)                        *)
   224     val (thy8, prm_inst_thms) = 
   225       thy7 |> PureThy.add_thms (map (fn (ak_name, T) =>
   226       let
   227         val ak_name_qu = Sign.full_name (sign_of thy7) (ak_name);
   228         val pt_name_qu = Sign.full_name (sign_of thy7) ("pt_"^ak_name);
   229         val i_type1 = TFree("'x",[pt_name_qu]);
   230         val i_type2 = Type(ak_name_qu,[]);
   231 	val cpt = Const ("nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
   232         val pt_type = Logic.mk_type i_type1;
   233         val at_type = Logic.mk_type i_type2;
   234         val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy7
   235                                   [Name "pt_def",
   236                                    Name ("pt_" ^ ak_name ^ "1"),
   237                                    Name ("pt_" ^ ak_name ^ "2"),
   238                                    Name ("pt_" ^ ak_name ^ "3")];
   239 
   240 	val name = "pt_"^ak_name^ "_inst";
   241         val statement = HOLogic.mk_Trueprop (cpt $ pt_type $ at_type);
   242 
   243         val proof = fn _ => auto_tac (claset(),simp_s);
   244       in 
   245         ((name, standard (Goal.prove thy7 [] [] statement proof)), []) 
   246       end) ak_names_types);
   247 
   248      (* declares an fs-axclass for every atom-kind       *)
   249      (* axclass fs_<ak>                                  *)
   250      (* fs_<ak>1: finite ((supp x)::<ak> set)            *)
   251      val (thy11, fs_ax_classes) =  foldl_map (fn (thy, (ak_name, T)) =>
   252        let 
   253 	  val cl_name = "fs_"^ak_name;
   254 	  val pt_name = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   255           val ty = TFree("'a",["HOL.type"]);
   256           val x   = Free ("x", ty);
   257           val csupp    = Const ("nominal.supp", ty --> HOLogic.mk_setT T);
   258           val cfinites = Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T))
   259           
   260           val axiom1   = HOLogic.mk_Trueprop (HOLogic.mk_mem (csupp $ x, cfinites));
   261 
   262        in  
   263         thy |> AxClass.add_axclass_i (cl_name, [pt_name]) [((cl_name^"1", axiom1),[])]            
   264        end) (thy8,ak_names_types); 
   265 
   266      (* proves that every fs_<ak>-type together with <ak>-type   *)
   267      (* instance of fs-type                                      *)
   268      (* lemma abst_<ak>_inst:                                    *)
   269      (* fs TYPE('x::pt_<ak>) TYPE (<ak>)                         *)
   270      val (thy12, fs_inst_thms) = 
   271        thy11 |> PureThy.add_thms (map (fn (ak_name, T) =>
   272        let
   273          val ak_name_qu = Sign.full_name (sign_of thy11) (ak_name);
   274          val fs_name_qu = Sign.full_name (sign_of thy11) ("fs_"^ak_name);
   275          val i_type1 = TFree("'x",[fs_name_qu]);
   276          val i_type2 = Type(ak_name_qu,[]);
   277  	 val cfs = Const ("nominal.fs", 
   278                                  (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
   279          val fs_type = Logic.mk_type i_type1;
   280          val at_type = Logic.mk_type i_type2;
   281 	 val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy11
   282                                    [Name "fs_def",
   283                                     Name ("fs_" ^ ak_name ^ "1")];
   284     
   285 	 val name = "fs_"^ak_name^ "_inst";
   286          val statement = HOLogic.mk_Trueprop (cfs $ fs_type $ at_type);
   287 
   288          val proof = fn _ => auto_tac (claset(),simp_s);
   289        in 
   290          ((name, standard (Goal.prove thy11 [] [] statement proof)), []) 
   291        end) ak_names_types);
   292 
   293        (* declares for every atom-kind combination an axclass            *)
   294        (* cp_<ak1>_<ak2> giving a composition property                   *)
   295        (* cp_<ak1>_<ak2>1: pi1 o pi2 o x = (pi1 o pi2) o (pi1 o x)       *)
   296         val (thy12b,_) = foldl_map (fn (thy, (ak_name, T)) =>
   297 	 foldl_map (fn (thy', (ak_name', T')) =>
   298 	     let
   299 	       val cl_name = "cp_"^ak_name^"_"^ak_name';
   300 	       val ty = TFree("'a",["HOL.type"]);
   301                val x   = Free ("x", ty);
   302                val pi1 = Free ("pi1", mk_permT T);
   303 	       val pi2 = Free ("pi2", mk_permT T');                  
   304 	       val cperm1 = Const ("nominal.perm", mk_permT T  --> ty --> ty);
   305                val cperm2 = Const ("nominal.perm", mk_permT T' --> ty --> ty);
   306                val cperm3 = Const ("nominal.perm", mk_permT T  --> mk_permT T' --> mk_permT T');
   307 
   308                val ax1   = HOLogic.mk_Trueprop 
   309 			   (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
   310                                            cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
   311 	       in  
   312 	       (fst (AxClass.add_axclass_i (cl_name, ["HOL.type"]) [((cl_name^"1", ax1),[])] thy'),())  
   313 	       end) 
   314 	   (thy, ak_names_types)) (thy12, ak_names_types)
   315 
   316         (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem;     *)
   317         (* lemma cp_<ak1>_<ak2>_inst:                                           *)
   318         (* cp TYPE('a::cp_<ak1>_<ak2>) TYPE(<ak1>) TYPE(<ak2>)                  *)
   319         val (thy12c, cp_thms) = foldl_map (fn (thy, (ak_name, T)) =>
   320 	 foldl_map (fn (thy', (ak_name', T')) =>
   321            let
   322              val ak_name_qu  = Sign.full_name (sign_of thy') (ak_name);
   323 	     val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');
   324              val cp_name_qu  = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   325              val i_type0 = TFree("'a",[cp_name_qu]);
   326              val i_type1 = Type(ak_name_qu,[]);
   327              val i_type2 = Type(ak_name_qu',[]);
   328 	     val ccp = Const ("nominal.cp",
   329                              (Term.itselfT i_type0)-->(Term.itselfT i_type1)-->
   330                                                       (Term.itselfT i_type2)-->HOLogic.boolT);
   331              val at_type  = Logic.mk_type i_type1;
   332              val at_type' = Logic.mk_type i_type2;
   333 	     val cp_type  = Logic.mk_type i_type0;
   334              val simp_s   = HOL_basic_ss addsimps PureThy.get_thmss thy' [(Name "cp_def")];
   335 	     val cp1      = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"1"));
   336 
   337 	     val name = "cp_"^ak_name^ "_"^ak_name'^"_inst";
   338              val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type');
   339 
   340              val proof = fn _ => EVERY [auto_tac (claset(),simp_s), rtac cp1 1];
   341 	   in
   342 	     thy' |> PureThy.add_thms 
   343                     [((name, standard (Goal.prove thy' [] [] statement proof)), [])]
   344 	   end) 
   345 	   (thy, ak_names_types)) (thy12b, ak_names_types);
   346        
   347         (* proves for every non-trivial <ak>-combination a disjointness   *)
   348         (* theorem; i.e. <ak1> != <ak2>                                   *)
   349         (* lemma ds_<ak1>_<ak2>:                                          *)
   350         (* dj TYPE(<ak1>) TYPE(<ak2>)                                     *)
   351         val (thy12d, dj_thms) = foldl_map (fn (thy, (ak_name, T)) =>
   352 	  foldl_map (fn (thy', (ak_name', T')) =>
   353           (if not (ak_name = ak_name') 
   354            then 
   355 	       let
   356 		 val ak_name_qu  = Sign.full_name (sign_of thy') (ak_name);
   357 	         val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');
   358                  val i_type1 = Type(ak_name_qu,[]);
   359                  val i_type2 = Type(ak_name_qu',[]);
   360 	         val cdj = Const ("nominal.disjoint",
   361                            (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
   362                  val at_type  = Logic.mk_type i_type1;
   363                  val at_type' = Logic.mk_type i_type2;
   364                  val simp_s = HOL_basic_ss addsimps PureThy.get_thmss thy' 
   365 					   [Name "disjoint_def",
   366                                             Name (ak_name^"_prm_"^ak_name'^"_def"),
   367                                             Name (ak_name'^"_prm_"^ak_name^"_def")];
   368 
   369 	         val name = "dj_"^ak_name^"_"^ak_name';
   370                  val statement = HOLogic.mk_Trueprop (cdj $ at_type $ at_type');
   371 
   372                  val proof = fn _ => auto_tac (claset(),simp_s);
   373 	       in
   374 		   thy' |> PureThy.add_thms 
   375                         [((name, standard (Goal.prove thy' [] [] statement proof)), []) ]
   376 	       end
   377            else 
   378             (thy',[])))  (* do nothing branch, if ak_name = ak_name' *) 
   379 	   (thy, ak_names_types)) (thy12c, ak_names_types);
   380 
   381      (*<<<<<<<  pt_<ak> class instances  >>>>>>>*)
   382      (*=========================================*)
   383      
   384      (* some frequently used theorems *)
   385       val pt1 = PureThy.get_thm thy12c (Name "pt1");
   386       val pt2 = PureThy.get_thm thy12c (Name "pt2");
   387       val pt3 = PureThy.get_thm thy12c (Name "pt3");
   388       val at_pt_inst    = PureThy.get_thm thy12c (Name "at_pt_inst");
   389       val pt_bool_inst  = PureThy.get_thm thy12c (Name "pt_bool_inst");
   390       val pt_set_inst   = PureThy.get_thm thy12c (Name "pt_set_inst"); 
   391       val pt_unit_inst  = PureThy.get_thm thy12c (Name "pt_unit_inst");
   392       val pt_prod_inst  = PureThy.get_thm thy12c (Name "pt_prod_inst"); 
   393       val pt_list_inst  = PureThy.get_thm thy12c (Name "pt_list_inst");   
   394       val pt_optn_inst  = PureThy.get_thm thy12c (Name "pt_option_inst");   
   395       val pt_noptn_inst = PureThy.get_thm thy12c (Name "pt_noption_inst");   
   396       val pt_fun_inst   = PureThy.get_thm thy12c (Name "pt_fun_inst");     
   397 
   398      (* for all atom-kind combination shows that         *)
   399      (* every <ak> is an instance of pt_<ai>             *)
   400      val (thy13,_) = foldl_map (fn (thy, (ak_name, T)) =>
   401 	 foldl_map (fn (thy', (ak_name', T')) =>
   402           (if ak_name = ak_name'
   403 	   then
   404 	     let
   405 	      val qu_name =  Sign.full_name (sign_of thy') ak_name;
   406               val qu_class = Sign.full_name (sign_of thy') ("pt_"^ak_name);
   407               val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name ^"_inst"));
   408               val proof = EVERY [AxClass.intro_classes_tac [],
   409                                  rtac ((at_inst RS at_pt_inst) RS pt1) 1,
   410                                  rtac ((at_inst RS at_pt_inst) RS pt2) 1,
   411                                  rtac ((at_inst RS at_pt_inst) RS pt3) 1,
   412                                  atac 1];
   413              in 
   414 	      (AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy',()) 
   415              end
   416            else 
   417              let
   418 	      val qu_name' = Sign.full_name (sign_of thy') ak_name';
   419               val qu_class = Sign.full_name (sign_of thy') ("pt_"^ak_name);
   420               val simp_s = HOL_basic_ss addsimps 
   421                            PureThy.get_thmss thy' [Name (ak_name^"_prm_"^ak_name'^"_def")];  
   422               val proof = EVERY [AxClass.intro_classes_tac [], auto_tac (claset(),simp_s)];
   423              in 
   424 	      (AxClass.add_inst_arity_i (qu_name',[],[qu_class]) proof thy',()) 
   425              end)) 
   426 	     (thy, ak_names_types)) (thy12c, ak_names_types);
   427 
   428      (* shows that bool is an instance of pt_<ak>     *)
   429      (* uses the theorem pt_bool_inst                 *)
   430      val (thy14,_) = foldl_map (fn (thy, (ak_name, T)) =>
   431        let
   432           val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   433           val proof = EVERY [AxClass.intro_classes_tac [],
   434                              rtac (pt_bool_inst RS pt1) 1,
   435                              rtac (pt_bool_inst RS pt2) 1,
   436                              rtac (pt_bool_inst RS pt3) 1,
   437                              atac 1];
   438        in 
   439 	 (AxClass.add_inst_arity_i ("bool",[],[qu_class]) proof thy,()) 
   440        end) (thy13,ak_names_types); 
   441 
   442      (* shows that set(pt_<ak>) is an instance of pt_<ak>          *)
   443      (* unfolds the permutation definition and applies pt_<ak>i    *)
   444      val (thy15,_) = foldl_map (fn (thy, (ak_name, T)) =>
   445        let
   446           val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   447           val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));  
   448           val proof = EVERY [AxClass.intro_classes_tac [],
   449                              rtac ((pt_inst RS pt_set_inst) RS pt1) 1,
   450                              rtac ((pt_inst RS pt_set_inst) RS pt2) 1,
   451                              rtac ((pt_inst RS pt_set_inst) RS pt3) 1,
   452                              atac 1];
   453        in 
   454 	 (AxClass.add_inst_arity_i ("set",[[qu_class]],[qu_class]) proof thy,()) 
   455        end) (thy14,ak_names_types); 
   456 
   457      (* shows that unit is an instance of pt_<ak>          *)
   458      val (thy16,_) = foldl_map (fn (thy, (ak_name, T)) =>
   459        let
   460           val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   461           val proof = EVERY [AxClass.intro_classes_tac [],
   462                              rtac (pt_unit_inst RS pt1) 1,
   463                              rtac (pt_unit_inst RS pt2) 1,
   464                              rtac (pt_unit_inst RS pt3) 1,
   465                              atac 1];
   466        in 
   467 	 (AxClass.add_inst_arity_i ("Product_Type.unit",[],[qu_class]) proof thy,()) 
   468        end) (thy15,ak_names_types); 
   469 
   470      (* shows that *(pt_<ak>,pt_<ak>) is an instance of pt_<ak> *)
   471      (* uses the theorem pt_prod_inst and pt_<ak>_inst          *)
   472      val (thy17,_) = foldl_map (fn (thy, (ak_name, T)) =>
   473        let
   474           val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   475           val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));  
   476           val proof = EVERY [AxClass.intro_classes_tac [],
   477                              rtac ((pt_inst RS (pt_inst RS pt_prod_inst)) RS pt1) 1,
   478                              rtac ((pt_inst RS (pt_inst RS pt_prod_inst)) RS pt2) 1,
   479                              rtac ((pt_inst RS (pt_inst RS pt_prod_inst)) RS pt3) 1,
   480                              atac 1];
   481        in 
   482           (AxClass.add_inst_arity_i ("*",[[qu_class],[qu_class]],[qu_class]) proof thy,()) 
   483        end) (thy16,ak_names_types); 
   484 
   485      (* shows that list(pt_<ak>) is an instance of pt_<ak>     *)
   486      (* uses the theorem pt_list_inst and pt_<ak>_inst         *)
   487      val (thy18,_) = foldl_map (fn (thy, (ak_name, T)) =>
   488        let
   489           val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   490           val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
   491           val proof = EVERY [AxClass.intro_classes_tac [],
   492                              rtac ((pt_inst RS pt_list_inst) RS pt1) 1,
   493                              rtac ((pt_inst RS pt_list_inst) RS pt2) 1,
   494                              rtac ((pt_inst RS pt_list_inst) RS pt3) 1,
   495                              atac 1];      
   496        in 
   497 	 (AxClass.add_inst_arity_i ("List.list",[[qu_class]],[qu_class]) proof thy,()) 
   498        end) (thy17,ak_names_types); 
   499 
   500      (* shows that option(pt_<ak>) is an instance of pt_<ak>   *)
   501      (* uses the theorem pt_option_inst and pt_<ak>_inst       *)
   502      val (thy18a,_) = foldl_map (fn (thy, (ak_name, T)) =>
   503        let
   504           val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   505           val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
   506           val proof = EVERY [AxClass.intro_classes_tac [],
   507                              rtac ((pt_inst RS pt_optn_inst) RS pt1) 1,
   508                              rtac ((pt_inst RS pt_optn_inst) RS pt2) 1,
   509                              rtac ((pt_inst RS pt_optn_inst) RS pt3) 1,
   510                              atac 1];      
   511        in 
   512 	 (AxClass.add_inst_arity_i ("Datatype.option",[[qu_class]],[qu_class]) proof thy,()) 
   513        end) (thy18,ak_names_types); 
   514 
   515      (* shows that nOption(pt_<ak>) is an instance of pt_<ak>   *)
   516      (* uses the theorem pt_option_inst and pt_<ak>_inst       *)
   517      val (thy18b,_) = foldl_map (fn (thy, (ak_name, T)) =>
   518        let
   519           val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   520           val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
   521           val proof = EVERY [AxClass.intro_classes_tac [],
   522                              rtac ((pt_inst RS pt_noptn_inst) RS pt1) 1,
   523                              rtac ((pt_inst RS pt_noptn_inst) RS pt2) 1,
   524                              rtac ((pt_inst RS pt_noptn_inst) RS pt3) 1,
   525                              atac 1];      
   526        in 
   527 	 (AxClass.add_inst_arity_i ("nominal.nOption",[[qu_class]],[qu_class]) proof thy,()) 
   528        end) (thy18a,ak_names_types); 
   529 
   530 
   531      (* shows that fun(pt_<ak>,pt_<ak>) is an instance of pt_<ak>     *)
   532      (* uses the theorem pt_list_inst and pt_<ak>_inst                *)
   533      val (thy19,_) = foldl_map (fn (thy, (ak_name, T)) =>
   534        let
   535           val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   536           val at_thm   = PureThy.get_thm thy (Name ("at_"^ak_name^"_inst"));
   537           val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
   538           val proof = EVERY [AxClass.intro_classes_tac [],
   539                              rtac ((at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst))) RS pt1) 1,
   540                              rtac ((at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst))) RS pt2) 1,
   541                              rtac ((at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst))) RS pt3) 1,
   542                              atac 1];      
   543        in 
   544 	 (AxClass.add_inst_arity_i ("fun",[[qu_class],[qu_class]],[qu_class]) proof thy,()) 
   545        end) (thy18b,ak_names_types);
   546 
   547        (*<<<<<<<  fs_<ak> class instances  >>>>>>>*)
   548        (*=========================================*)
   549        val fs1          = PureThy.get_thm thy19 (Name "fs1");
   550        val fs_at_inst   = PureThy.get_thm thy19 (Name "fs_at_inst");
   551        val fs_unit_inst = PureThy.get_thm thy19 (Name "fs_unit_inst");
   552        val fs_bool_inst = PureThy.get_thm thy19 (Name "fs_bool_inst");
   553        val fs_prod_inst = PureThy.get_thm thy19 (Name "fs_prod_inst");
   554        val fs_list_inst = PureThy.get_thm thy19 (Name "fs_list_inst");
   555 
   556        (* shows that <ak> is an instance of fs_<ak>     *)
   557        (* uses the theorem at_<ak>_inst                 *)
   558        val (thy20,_) = foldl_map (fn (thy, (ak_name, T)) =>
   559        let
   560           val qu_name =  Sign.full_name (sign_of thy) ak_name;
   561           val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
   562           val at_thm   = PureThy.get_thm thy (Name ("at_"^ak_name^"_inst"));
   563           val proof = EVERY [AxClass.intro_classes_tac [],
   564                              rtac ((at_thm RS fs_at_inst) RS fs1) 1];      
   565        in 
   566 	 (AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy,()) 
   567        end) (thy19,ak_names_types);  
   568 
   569        (* shows that unit is an instance of fs_<ak>     *)
   570        (* uses the theorem fs_unit_inst                 *)
   571        val (thy21,_) = foldl_map (fn (thy, (ak_name, T)) =>
   572        let
   573           val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
   574           val proof = EVERY [AxClass.intro_classes_tac [],
   575                              rtac (fs_unit_inst RS fs1) 1];      
   576        in 
   577 	 (AxClass.add_inst_arity_i ("Product_Type.unit",[],[qu_class]) proof thy,()) 
   578        end) (thy20,ak_names_types);  
   579 
   580        (* shows that bool is an instance of fs_<ak>     *)
   581        (* uses the theorem fs_bool_inst                 *)
   582        val (thy22,_) = foldl_map (fn (thy, (ak_name, T)) =>
   583        let
   584           val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
   585           val proof = EVERY [AxClass.intro_classes_tac [],
   586                              rtac (fs_bool_inst RS fs1) 1];      
   587        in 
   588 	 (AxClass.add_inst_arity_i ("bool",[],[qu_class]) proof thy,()) 
   589        end) (thy21,ak_names_types);  
   590 
   591        (* shows that *(fs_<ak>,fs_<ak>) is an instance of fs_<ak>     *)
   592        (* uses the theorem fs_prod_inst                               *)
   593        val (thy23,_) = foldl_map (fn (thy, (ak_name, T)) =>
   594        let
   595           val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
   596           val fs_inst  = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
   597           val proof = EVERY [AxClass.intro_classes_tac [],
   598                              rtac ((fs_inst RS (fs_inst RS fs_prod_inst)) RS fs1) 1];      
   599        in 
   600 	 (AxClass.add_inst_arity_i ("*",[[qu_class],[qu_class]],[qu_class]) proof thy,()) 
   601        end) (thy22,ak_names_types);  
   602 
   603        (* shows that list(fs_<ak>) is an instance of fs_<ak>     *)
   604        (* uses the theorem fs_list_inst                          *)
   605        val (thy24,_) = foldl_map (fn (thy, (ak_name, T)) =>
   606        let
   607           val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
   608           val fs_inst  = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
   609           val proof = EVERY [AxClass.intro_classes_tac [],
   610                               rtac ((fs_inst RS fs_list_inst) RS fs1) 1];      
   611        in 
   612 	 (AxClass.add_inst_arity_i ("List.list",[[qu_class]],[qu_class]) proof thy,()) 
   613        end) (thy23,ak_names_types);  
   614 	   
   615        (*<<<<<<<  cp_<ak>_<ai> class instances  >>>>>>>*)
   616        (*==============================================*)
   617        val cp1             = PureThy.get_thm thy24 (Name "cp1");
   618        val cp_unit_inst    = PureThy.get_thm thy24 (Name "cp_unit_inst");
   619        val cp_bool_inst    = PureThy.get_thm thy24 (Name "cp_bool_inst");
   620        val cp_prod_inst    = PureThy.get_thm thy24 (Name "cp_prod_inst");
   621        val cp_list_inst    = PureThy.get_thm thy24 (Name "cp_list_inst");
   622        val cp_fun_inst     = PureThy.get_thm thy24 (Name "cp_fun_inst");
   623        val cp_option_inst  = PureThy.get_thm thy24 (Name "cp_option_inst");
   624        val cp_noption_inst = PureThy.get_thm thy24 (Name "cp_noption_inst");
   625        val pt_perm_compose = PureThy.get_thm thy24 (Name "pt_perm_compose");
   626        val dj_pp_forget    = PureThy.get_thm thy24 (Name "dj_perm_perm_forget");
   627 
   628        (* shows that <aj> is an instance of cp_<ak>_<ai>  *)
   629        (* that needs a three-nested loop *)
   630        val (thy25,_) = foldl_map (fn (thy, (ak_name, T)) =>
   631 	 foldl_map (fn (thy', (ak_name', T')) =>
   632           foldl_map (fn (thy'', (ak_name'', T'')) =>
   633             let
   634               val qu_name =  Sign.full_name (sign_of thy'') ak_name;
   635               val qu_class = Sign.full_name (sign_of thy'') ("cp_"^ak_name'^"_"^ak_name'');
   636               val proof =
   637                 (if (ak_name'=ak_name'') then 
   638 		  (let
   639                     val pt_inst  = PureThy.get_thm thy'' (Name ("pt_"^ak_name''^"_inst"));
   640 		    val at_inst  = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst"));
   641                   in 
   642 		   EVERY [AxClass.intro_classes_tac [], 
   643                           rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]
   644                   end)
   645 		else
   646 		  (let 
   647                      val dj_inst  = PureThy.get_thm thy'' (Name ("dj_"^ak_name''^"_"^ak_name'));
   648 		     val simp_s = HOL_basic_ss addsimps 
   649                                         ((dj_inst RS dj_pp_forget)::
   650                                          (PureThy.get_thmss thy'' 
   651 					   [Name (ak_name' ^"_prm_"^ak_name^"_def"),
   652                                             Name (ak_name''^"_prm_"^ak_name^"_def")]));  
   653 		  in 
   654                     EVERY [AxClass.intro_classes_tac [], simp_tac simp_s 1]
   655                   end))
   656 	      in
   657                 (AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy'',())
   658 	      end)
   659 	   (thy', ak_names_types)) (thy, ak_names_types)) (thy24, ak_names_types);
   660       
   661        (* shows that unit is an instance of cp_<ak>_<ai>     *)
   662        (* for every <ak>-combination                         *)
   663        val (thy26,_) = foldl_map (fn (thy, (ak_name, T)) =>
   664 	 foldl_map (fn (thy', (ak_name', T')) =>
   665           let
   666             val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   667             val proof = EVERY [AxClass.intro_classes_tac [],rtac (cp_unit_inst RS cp1) 1];     
   668 	  in
   669             (AxClass.add_inst_arity_i ("Product_Type.unit",[],[qu_class]) proof thy',())
   670 	  end) 
   671 	   (thy, ak_names_types)) (thy25, ak_names_types);
   672        
   673        (* shows that bool is an instance of cp_<ak>_<ai>     *)
   674        (* for every <ak>-combination                         *)
   675        val (thy27,_) = foldl_map (fn (thy, (ak_name, T)) =>
   676 	 foldl_map (fn (thy', (ak_name', T')) =>
   677            let
   678 	     val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   679              val proof = EVERY [AxClass.intro_classes_tac [], rtac (cp_bool_inst RS cp1) 1];     
   680 	   in
   681              (AxClass.add_inst_arity_i ("bool",[],[qu_class]) proof thy',())
   682 	   end) 
   683 	   (thy, ak_names_types)) (thy26, ak_names_types);
   684 
   685        (* shows that prod is an instance of cp_<ak>_<ai>     *)
   686        (* for every <ak>-combination                         *)
   687        val (thy28,_) = foldl_map (fn (thy, (ak_name, T)) =>
   688 	 foldl_map (fn (thy', (ak_name', T')) =>
   689           let
   690 	    val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   691             val cp_inst  = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   692             val proof = EVERY [AxClass.intro_classes_tac [],
   693                                rtac ((cp_inst RS (cp_inst RS cp_prod_inst)) RS cp1) 1];     
   694 	  in
   695             (AxClass.add_inst_arity_i ("*",[[qu_class],[qu_class]],[qu_class]) proof thy',())
   696 	  end)  
   697 	  (thy, ak_names_types)) (thy27, ak_names_types);
   698 
   699        (* shows that list is an instance of cp_<ak>_<ai>     *)
   700        (* for every <ak>-combination                         *)
   701        val (thy29,_) = foldl_map (fn (thy, (ak_name, T)) =>
   702 	 foldl_map (fn (thy', (ak_name', T')) =>
   703            let
   704 	     val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   705              val cp_inst  = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   706              val proof = EVERY [AxClass.intro_classes_tac [],
   707                                 rtac ((cp_inst RS cp_list_inst) RS cp1) 1];     
   708 	   in
   709             (AxClass.add_inst_arity_i ("List.list",[[qu_class]],[qu_class]) proof thy',())
   710 	   end) 
   711 	   (thy, ak_names_types)) (thy28, ak_names_types);
   712 
   713        (* shows that function is an instance of cp_<ak>_<ai>     *)
   714        (* for every <ak>-combination                             *)
   715        val (thy30,_) = foldl_map (fn (thy, (ak_name, T)) =>
   716 	 foldl_map (fn (thy', (ak_name', T')) =>
   717           let
   718 	    val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   719             val cp_inst  = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   720             val pt_inst  = PureThy.get_thm thy' (Name ("pt_"^ak_name^"_inst"));
   721             val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
   722             val proof = EVERY [AxClass.intro_classes_tac [],
   723                     rtac ((at_inst RS (pt_inst RS (cp_inst RS (cp_inst RS cp_fun_inst)))) RS cp1) 1];  
   724 	  in
   725             (AxClass.add_inst_arity_i ("fun",[[qu_class],[qu_class]],[qu_class]) proof thy',())
   726 	  end) 
   727 	  (thy, ak_names_types)) (thy29, ak_names_types);
   728 
   729        (* shows that option is an instance of cp_<ak>_<ai>     *)
   730        (* for every <ak>-combination                           *)
   731        val (thy31,_) = foldl_map (fn (thy, (ak_name, T)) =>
   732 	 foldl_map (fn (thy', (ak_name', T')) =>
   733           let
   734 	    val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   735             val cp_inst  = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   736             val proof = EVERY [AxClass.intro_classes_tac [],
   737                                rtac ((cp_inst RS cp_option_inst) RS cp1) 1];     
   738 	  in
   739             (AxClass.add_inst_arity_i ("Datatype.option",[[qu_class]],[qu_class]) proof thy',())
   740 	  end) 
   741 	  (thy, ak_names_types)) (thy30, ak_names_types);
   742 
   743        (* shows that nOption is an instance of cp_<ak>_<ai>     *)
   744        (* for every <ak>-combination                            *)
   745        val (thy32,_) = foldl_map (fn (thy, (ak_name, T)) =>
   746 	 foldl_map (fn (thy', (ak_name', T')) =>
   747           let
   748 	    val qu_class = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
   749             val cp_inst  = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   750             val proof = EVERY [AxClass.intro_classes_tac [],
   751                                rtac ((cp_inst RS cp_noption_inst) RS cp1) 1];     
   752 	  in
   753            (AxClass.add_inst_arity_i ("nominal.nOption",[[qu_class]],[qu_class]) proof thy',())
   754 	  end) 
   755 	  (thy, ak_names_types)) (thy31, ak_names_types);
   756 
   757        (* abbreviations for some collection of rules *)
   758        (*============================================*)
   759        val abs_fun_pi        = PureThy.get_thm thy32 (Name ("nominal.abs_fun_pi"));
   760        val abs_fun_pi_ineq   = PureThy.get_thm thy32 (Name ("nominal.abs_fun_pi_ineq"));
   761        val abs_fun_eq        = PureThy.get_thm thy32 (Name ("nominal.abs_fun_eq"));
   762        val dj_perm_forget    = PureThy.get_thm thy32 (Name ("nominal.dj_perm_forget"));
   763        val dj_pp_forget      = PureThy.get_thm thy32 (Name ("nominal.dj_perm_perm_forget"));
   764        val fresh_iff         = PureThy.get_thm thy32 (Name ("nominal.fresh_abs_fun_iff"));
   765        val fresh_iff_ineq    = PureThy.get_thm thy32 (Name ("nominal.fresh_abs_fun_iff_ineq"));
   766        val abs_fun_supp      = PureThy.get_thm thy32 (Name ("nominal.abs_fun_supp"));
   767        val abs_fun_supp_ineq = PureThy.get_thm thy32 (Name ("nominal.abs_fun_supp_ineq"));
   768        val pt_swap_bij       = PureThy.get_thm thy32 (Name ("nominal.pt_swap_bij"));
   769        val pt_fresh_fresh    = PureThy.get_thm thy32 (Name ("nominal.pt_fresh_fresh"));
   770        val pt_bij            = PureThy.get_thm thy32 (Name ("nominal.pt_bij"));
   771        val pt_perm_compose   = PureThy.get_thm thy32 (Name ("nominal.pt_perm_compose"));
   772        val perm_eq_app       = PureThy.get_thm thy32 (Name ("nominal.perm_eq_app"));
   773        val at_fresh          = PureThy.get_thm thy32 (Name ("nominal.at_fresh"));
   774        (*val at_calc           = PureThy.get_thms thy32 (Name ("nominal.at_calc"));*)
   775        val at_supp           = PureThy.get_thm thy32 (Name ("nominal.at_supp"));
   776        val dj_supp           = PureThy.get_thm thy32 (Name ("nominal.at_supp"));
   777 
   778        (* abs_perm collects all lemmas for simplifying a permutation *)
   779        (* in front of an abs_fun                                     *)
   780        val (thy33,_) = 
   781 	   let 
   782 	     val name = "abs_perm"
   783              val thm_list = Library.flat (map (fn (ak_name, T) =>
   784 	        let	
   785 		  val at_inst = PureThy.get_thm thy32 (Name ("at_"^ak_name^"_inst"));
   786 		  val pt_inst = PureThy.get_thm thy32 (Name ("pt_"^ak_name^"_inst"));	      
   787 	          val thm = [pt_inst, at_inst] MRS abs_fun_pi
   788                   val thm_list = map (fn (ak_name', T') =>
   789                      let
   790                       val cp_inst = PureThy.get_thm thy32 (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   791 	             in
   792                      [pt_inst, pt_inst, at_inst, cp_inst] MRS abs_fun_pi_ineq
   793 	             end) ak_names_types;
   794                  in thm::thm_list end) (ak_names_types))
   795            in
   796              (PureThy.add_thmss [((name, thm_list),[])] thy32)
   797            end;
   798 
   799        val (thy34,_) = 
   800 	   let 
   801 	       fun inst_pt_at thm ak_name =
   802 		 let	
   803 		   val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
   804 		   val pt_inst = PureThy.get_thm thy33 (Name ("pt_"^ak_name^"_inst"));	      
   805 	         in
   806                      [pt_inst, at_inst] MRS thm
   807 	         end	
   808                fun inst_at thm ak_name =
   809 		 let	
   810 		   val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
   811                  in
   812                      at_inst RS thm
   813 	         end
   814 
   815            in
   816             thy33 
   817 	    |> PureThy.add_thmss   [(("alpha", map (inst_pt_at abs_fun_eq) ak_names),[])]
   818             |>>> PureThy.add_thmss [(("perm_swap", map (inst_pt_at pt_swap_bij) ak_names),[])]
   819             |>>> PureThy.add_thmss [(("perm_fresh_fresh", map (inst_pt_at pt_fresh_fresh) ak_names),[])]
   820             |>>> PureThy.add_thmss [(("perm_bij", map (inst_pt_at pt_bij) ak_names),[])]
   821             |>>> PureThy.add_thmss [(("perm_compose", map (inst_pt_at pt_perm_compose) ak_names),[])]
   822             |>>> PureThy.add_thmss [(("perm_app_eq", map (inst_pt_at perm_eq_app) ak_names),[])]
   823             |>>> PureThy.add_thmss [(("supp_at", map (inst_at at_supp) ak_names),[])]
   824             (*|>>> PureThy.add_thmss [(("fresh_at", map (inst_at at_fresh) ak_names),
   825                                     [Simplifier.simp_add_global])]*)
   826             (*|>>> PureThy.add_thmss [(("calc_at", map (inst_at at_calc) ak_names),
   827                                     [Simplifier.simp_add_global])]*)
   828 	   end;
   829 
   830          (* perm_dj collects all lemmas that forget an permutation *)
   831          (* when it acts on an atom of different type              *)
   832          val (thy35,_) = 
   833 	   let 
   834 	     val name = "perm_dj"
   835              val thm_list = Library.flat (map (fn (ak_name, T) =>
   836 	        Library.flat (map (fn (ak_name', T') => 
   837                  if not (ak_name = ak_name') 
   838                  then 
   839 		    let
   840                       val dj_inst = PureThy.get_thm thy34 (Name ("dj_"^ak_name^"_"^ak_name'));
   841                     in
   842                       [dj_inst RS dj_perm_forget, dj_inst RS dj_pp_forget]
   843                     end 
   844                  else []) ak_names_types)) ak_names_types)
   845            in
   846              (PureThy.add_thmss [((name, thm_list),[])] thy34)
   847            end;
   848 
   849          (* abs_fresh collects all lemmas for simplifying a freshness *)
   850          (* proposition involving an abs_fun                          *)
   851 
   852          val (thy36,_) = 
   853 	   let 
   854 	     val name = "abs_fresh"
   855              val thm_list = Library.flat (map (fn (ak_name, T) =>
   856 	        let	
   857 		  val at_inst = PureThy.get_thm thy35 (Name ("at_"^ak_name^"_inst"));
   858 		  val pt_inst = PureThy.get_thm thy35 (Name ("pt_"^ak_name^"_inst"));
   859                   val fs_inst = PureThy.get_thm thy35 (Name ("fs_"^ak_name^"_inst"));	      
   860 	          val thm = [pt_inst, at_inst, (fs_inst RS fs1)] MRS fresh_iff
   861                   val thm_list = Library.flat (map (fn (ak_name', T') =>
   862                      (if (not (ak_name = ak_name')) 
   863                      then
   864                        let
   865                         val cp_inst = PureThy.get_thm thy35 (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   866 	                val dj_inst = PureThy.get_thm thy35 (Name ("dj_"^ak_name'^"_"^ak_name));
   867                        in
   868                         [[pt_inst, pt_inst, at_inst, cp_inst, dj_inst] MRS fresh_iff_ineq]
   869 	               end
   870                      else [])) ak_names_types);
   871                  in thm::thm_list end) (ak_names_types))
   872            in
   873              (PureThy.add_thmss [((name, thm_list),[])] thy35)
   874            end;
   875 
   876          (* abs_supp collects all lemmas for simplifying  *)
   877          (* support proposition involving an abs_fun      *)
   878 
   879          val (thy37,_) = 
   880 	   let 
   881 	     val name = "abs_supp"
   882              val thm_list = Library.flat (map (fn (ak_name, T) =>
   883 	        let	
   884 		  val at_inst = PureThy.get_thm thy36 (Name ("at_"^ak_name^"_inst"));
   885 		  val pt_inst = PureThy.get_thm thy36 (Name ("pt_"^ak_name^"_inst"));
   886                   val fs_inst = PureThy.get_thm thy36 (Name ("fs_"^ak_name^"_inst"));	      
   887 	          val thm1 = [pt_inst, at_inst, (fs_inst RS fs1)] MRS abs_fun_supp
   888                   val thm2 = [pt_inst, at_inst] MRS abs_fun_supp
   889                   val thm_list = Library.flat (map (fn (ak_name', T') =>
   890                      (if (not (ak_name = ak_name')) 
   891                      then
   892                        let
   893                         val cp_inst = PureThy.get_thm thy36 (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   894 	                val dj_inst = PureThy.get_thm thy36 (Name ("dj_"^ak_name'^"_"^ak_name));
   895                        in
   896                         [[pt_inst, pt_inst, at_inst, cp_inst, dj_inst] MRS abs_fun_supp_ineq]
   897 	               end
   898                      else [])) ak_names_types);
   899                  in thm1::thm2::thm_list end) (ak_names_types))
   900            in
   901              (PureThy.add_thmss [((name, thm_list),[])] thy36)
   902            end;
   903 
   904     in NominalData.put (fold Symtab.update (map (rpair ()) full_ak_names)
   905       (NominalData.get thy11)) thy37
   906     end;
   907 
   908 
   909 (* syntax und parsing *)
   910 structure P = OuterParse and K = OuterKeyword;
   911 
   912 val atom_declP =
   913   OuterSyntax.command "atom_decl" "Declare new kinds of atoms" K.thy_decl
   914     (Scan.repeat1 P.name >> (Toplevel.theory o create_nom_typedecls));
   915 
   916 val _ = OuterSyntax.add_parsers [atom_declP];
   917 
   918 val setup = [NominalData.init];
   919 
   920 (*=======================================================================*)
   921 
   922 (** FIXME: DatatypePackage should export this function **)
   923 
   924 local
   925 
   926 fun dt_recs (DtTFree _) = []
   927   | dt_recs (DtType (_, dts)) = List.concat (map dt_recs dts)
   928   | dt_recs (DtRec i) = [i];
   929 
   930 fun dt_cases (descr: descr) (_, args, constrs) =
   931   let
   932     fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
   933     val bnames = map the_bname (distinct (List.concat (map dt_recs args)));
   934   in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
   935 
   936 
   937 fun induct_cases descr =
   938   DatatypeProp.indexify_names (List.concat (map (dt_cases descr) (map #2 descr)));
   939 
   940 fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
   941 
   942 in
   943 
   944 fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
   945 
   946 fun mk_case_names_exhausts descr new =
   947   map (RuleCases.case_names o exhaust_cases descr o #1)
   948     (List.filter (fn ((_, (name, _, _))) => name mem_string new) descr);
   949 
   950 end;
   951 
   952 (*******************************)
   953 
   954 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
   955 
   956 fun read_typ sign ((Ts, sorts), str) =
   957   let
   958     val T = Type.no_tvars (Sign.read_typ (sign, (AList.lookup op =)
   959       (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
   960   in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
   961 
   962 (** taken from HOL/Tools/datatype_aux.ML **)
   963 
   964 fun indtac indrule indnames i st =
   965   let
   966     val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
   967     val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop
   968       (Logic.strip_imp_concl (List.nth (prems_of st, i - 1))));
   969     val getP = if can HOLogic.dest_imp (hd ts) then
   970       (apfst SOME) o HOLogic.dest_imp else pair NONE;
   971     fun abstr (t1, t2) = (case t1 of
   972         NONE => (case filter (fn Free (s, _) => s mem indnames | _ => false)
   973               (term_frees t2) of
   974             [Free (s, T)] => absfree (s, T, t2)
   975           | _ => sys_error "indtac")
   976       | SOME (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2)))
   977     val cert = cterm_of (Thm.sign_of_thm st);
   978     val Ps = map (cert o head_of o snd o getP) ts;
   979     val indrule' = cterm_instantiate (Ps ~~
   980       (map (cert o abstr o getP) ts')) indrule
   981   in
   982     rtac indrule' i st
   983   end;
   984 
   985 fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
   986   let
   987     (* this theory is used just for parsing *)
   988   
   989     val tmp_thy = thy |>
   990       Theory.copy |>
   991       Theory.add_types (map (fn (tvs, tname, mx, _) =>
   992         (tname, length tvs, mx)) dts);
   993 
   994     val sign = Theory.sign_of tmp_thy;
   995 
   996     val atoms = atoms_of thy;
   997     val classes = map (NameSpace.map_base (fn s => "pt_" ^ s)) atoms;
   998     val cp_classes = List.concat (map (fn atom1 => map (fn atom2 =>
   999       Sign.intern_class thy ("cp_" ^ Sign.base_name atom1 ^ "_" ^
  1000         Sign.base_name atom2)) atoms) atoms);
  1001     fun augment_sort S = S union classes;
  1002     val augment_sort_typ = map_type_tfree (fn (s, S) => TFree (s, augment_sort S));
  1003 
  1004     fun prep_constr ((constrs, sorts), (cname, cargs, mx)) =
  1005       let val (cargs', sorts') = Library.foldl (prep_typ sign) (([], sorts), cargs)
  1006       in (constrs @ [(cname, cargs', mx)], sorts') end
  1007 
  1008     fun prep_dt_spec ((dts, sorts), (tvs, tname, mx, constrs)) =
  1009       let val (constrs', sorts') = Library.foldl prep_constr (([], sorts), constrs)
  1010       in (dts @ [(tvs, tname, mx, constrs')], sorts') end
  1011 
  1012     val (dts', sorts) = Library.foldl prep_dt_spec (([], []), dts);
  1013     val sorts' = map (apsnd augment_sort) sorts;
  1014     val tyvars = map #1 dts';
  1015 
  1016     val types_syntax = map (fn (tvs, tname, mx, constrs) => (tname, mx)) dts';
  1017     val constr_syntax = map (fn (tvs, tname, mx, constrs) =>
  1018       map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts';
  1019 
  1020     val ps = map (fn (_, n, _, _) =>
  1021       (Sign.full_name sign n, Sign.full_name sign (n ^ "_Rep"))) dts;
  1022     val rps = map Library.swap ps;
  1023 
  1024     fun replace_types (Type ("nominal.ABS", [T, U])) = 
  1025           Type ("fun", [T, Type ("nominal.nOption", [replace_types U])])
  1026       | replace_types (Type (s, Ts)) =
  1027           Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
  1028       | replace_types T = T;
  1029 
  1030     fun replace_types' (Type (s, Ts)) =
  1031           Type (getOpt (AList.lookup op = rps s, s), map replace_types' Ts)
  1032       | replace_types' T = T;
  1033 
  1034     val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, tname ^ "_Rep", NoSyn,
  1035       map (fn (cname, cargs, mx) => (cname,
  1036         map (augment_sort_typ o replace_types) cargs, NoSyn)) constrs)) dts';
  1037 
  1038     val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
  1039     val full_new_type_names' = map (Sign.full_name (sign_of thy)) new_type_names';
  1040 
  1041     val ({induction, ...},thy1) =
  1042       DatatypePackage.add_datatype_i err flat_names new_type_names' dts'' thy;
  1043 
  1044     val SOME {descr, ...} = Symtab.lookup
  1045       (DatatypePackage.get_datatypes thy1) (hd full_new_type_names');
  1046     val typ_of_dtyp = typ_of_dtyp descr sorts';
  1047     fun nth_dtyp i = typ_of_dtyp (DtRec i);
  1048 
  1049     (**** define permutation functions ****)
  1050 
  1051     val permT = mk_permT (TFree ("'x", HOLogic.typeS));
  1052     val pi = Free ("pi", permT);
  1053     val perm_types = map (fn (i, _) =>
  1054       let val T = nth_dtyp i
  1055       in permT --> T --> T end) descr;
  1056     val perm_names = replicate (length new_type_names) "nominal.perm" @
  1057       DatatypeProp.indexify_names (map (fn i => Sign.full_name (sign_of thy1)
  1058         ("perm_" ^ name_of_typ (nth_dtyp i)))
  1059           (length new_type_names upto length descr - 1));
  1060     val perm_names_types = perm_names ~~ perm_types;
  1061 
  1062     val perm_eqs = List.concat (map (fn (i, (_, _, constrs)) =>
  1063       let val T = nth_dtyp i
  1064       in map (fn (cname, dts) => 
  1065         let
  1066           val Ts = map typ_of_dtyp dts;
  1067           val names = DatatypeProp.make_tnames Ts;
  1068           val args = map Free (names ~~ Ts);
  1069           val c = Const (cname, Ts ---> T);
  1070           fun perm_arg (dt, x) =
  1071             let val T = type_of x
  1072             in if is_rec_type dt then
  1073                 let val (Us, _) = strip_type T
  1074                 in list_abs (map (pair "x") Us,
  1075                   Const (List.nth (perm_names_types, body_index dt)) $ pi $
  1076                     list_comb (x, map (fn (i, U) =>
  1077                       Const ("nominal.perm", permT --> U --> U) $
  1078                         (Const ("List.rev", permT --> permT) $ pi) $
  1079                         Bound i) ((length Us - 1 downto 0) ~~ Us)))
  1080                 end
  1081               else Const ("nominal.perm", permT --> T --> T) $ pi $ x
  1082             end;  
  1083         in
  1084           (("", HOLogic.mk_Trueprop (HOLogic.mk_eq
  1085             (Const (List.nth (perm_names_types, i)) $
  1086                Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
  1087                list_comb (c, args),
  1088              list_comb (c, map perm_arg (dts ~~ args))))), [])
  1089         end) constrs
  1090       end) descr);
  1091 
  1092     val (thy2, perm_simps) = thy1 |>
  1093       Theory.add_consts_i (map (fn (s, T) => (Sign.base_name s, T, NoSyn))
  1094         (List.drop (perm_names_types, length new_type_names))) |>
  1095       PrimrecPackage.add_primrec_i "" perm_eqs;
  1096 
  1097     (**** prove that permutation functions introduced by unfolding are ****)
  1098     (**** equivalent to already existing permutation functions         ****)
  1099 
  1100     val _ = warning ("length descr: " ^ string_of_int (length descr));
  1101     val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
  1102 
  1103     val perm_indnames = DatatypeProp.make_tnames (map body_type perm_types);
  1104     val perm_fun_def = PureThy.get_thm thy2 (Name "perm_fun_def");
  1105 
  1106     val unfolded_perm_eq_thms =
  1107       if length descr = length new_type_names then []
  1108       else map standard (List.drop (split_conj_thm
  1109         (Goal.prove thy2 [] []
  1110           (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1111             (map (fn (c as (s, T), x) =>
  1112                let val [T1, T2] = binder_types T
  1113                in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
  1114                  Const ("nominal.perm", T) $ pi $ Free (x, T2))
  1115                end)
  1116              (perm_names_types ~~ perm_indnames))))
  1117           (fn _ => EVERY [indtac induction perm_indnames 1,
  1118             ALLGOALS (asm_full_simp_tac
  1119               (simpset_of thy2 addsimps [perm_fun_def]))])),
  1120         length new_type_names));
  1121 
  1122     (**** prove [] \<bullet> t = t ****)
  1123 
  1124     val _ = warning "perm_empty_thms";
  1125 
  1126     val perm_empty_thms = List.concat (map (fn a =>
  1127       let val permT = mk_permT (Type (a, []))
  1128       in map standard (List.take (split_conj_thm
  1129         (Goal.prove thy2 [] []
  1130           (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1131             (map (fn ((s, T), x) => HOLogic.mk_eq
  1132                 (Const (s, permT --> T --> T) $
  1133                    Const ("List.list.Nil", permT) $ Free (x, T),
  1134                  Free (x, T)))
  1135              (perm_names ~~
  1136               map body_type perm_types ~~ perm_indnames))))
  1137           (fn _ => EVERY [indtac induction perm_indnames 1,
  1138             ALLGOALS (asm_full_simp_tac (simpset_of thy2))])),
  1139         length new_type_names))
  1140       end)
  1141       atoms);
  1142 
  1143     (**** prove (pi1 @ pi2) \<bullet> t = pi1 \<bullet> (pi2 \<bullet> t) ****)
  1144 
  1145     val _ = warning "perm_append_thms";
  1146 
  1147     (*FIXME: these should be looked up statically*)
  1148     val at_pt_inst = PureThy.get_thm thy2 (Name "at_pt_inst");
  1149     val pt2 = PureThy.get_thm thy2 (Name "pt2");
  1150 
  1151     val perm_append_thms = List.concat (map (fn a =>
  1152       let
  1153         val permT = mk_permT (Type (a, []));
  1154         val pi1 = Free ("pi1", permT);
  1155         val pi2 = Free ("pi2", permT);
  1156         val pt_inst = PureThy.get_thm thy2 (Name ("pt_" ^ Sign.base_name a ^ "_inst"));
  1157         val pt2' = pt_inst RS pt2;
  1158         val pt2_ax = PureThy.get_thm thy2
  1159           (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a));
  1160       in List.take (map standard (split_conj_thm
  1161         (Goal.prove thy2 [] []
  1162              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1163                 (map (fn ((s, T), x) =>
  1164                     let val perm = Const (s, permT --> T --> T)
  1165                     in HOLogic.mk_eq
  1166                       (perm $ (Const ("List.op @", permT --> permT --> permT) $
  1167                          pi1 $ pi2) $ Free (x, T),
  1168                        perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
  1169                     end)
  1170                   (perm_names ~~
  1171                    map body_type perm_types ~~ perm_indnames))))
  1172            (fn _ => EVERY [indtac induction perm_indnames 1,
  1173               ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
  1174          length new_type_names)
  1175       end) atoms);
  1176 
  1177     (**** prove pi1 ~ pi2 ==> pi1 \<bullet> t = pi2 \<bullet> t ****)
  1178 
  1179     val _ = warning "perm_eq_thms";
  1180 
  1181     val pt3 = PureThy.get_thm thy2 (Name "pt3");
  1182     val pt3_rev = PureThy.get_thm thy2 (Name "pt3_rev");
  1183 
  1184     val perm_eq_thms = List.concat (map (fn a =>
  1185       let
  1186         val permT = mk_permT (Type (a, []));
  1187         val pi1 = Free ("pi1", permT);
  1188         val pi2 = Free ("pi2", permT);
  1189         (*FIXME: not robust - better access these theorems using NominalData?*)
  1190         val at_inst = PureThy.get_thm thy2 (Name ("at_" ^ Sign.base_name a ^ "_inst"));
  1191         val pt_inst = PureThy.get_thm thy2 (Name ("pt_" ^ Sign.base_name a ^ "_inst"));
  1192         val pt3' = pt_inst RS pt3;
  1193         val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
  1194         val pt3_ax = PureThy.get_thm thy2
  1195           (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a));
  1196       in List.take (map standard (split_conj_thm
  1197         (Goal.prove thy2 [] [] (Logic.mk_implies
  1198              (HOLogic.mk_Trueprop (Const ("nominal.prm_eq",
  1199                 permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
  1200               HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1201                 (map (fn ((s, T), x) =>
  1202                     let val perm = Const (s, permT --> T --> T)
  1203                     in HOLogic.mk_eq
  1204                       (perm $ pi1 $ Free (x, T),
  1205                        perm $ pi2 $ Free (x, T))
  1206                     end)
  1207                   (perm_names ~~
  1208                    map body_type perm_types ~~ perm_indnames)))))
  1209            (fn _ => EVERY [indtac induction perm_indnames 1,
  1210               ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
  1211          length new_type_names)
  1212       end) atoms);
  1213 
  1214     (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
  1215 
  1216     val cp1 = PureThy.get_thm thy2 (Name "cp1");
  1217     val dj_cp = PureThy.get_thm thy2 (Name "dj_cp");
  1218     val pt_perm_compose = PureThy.get_thm thy2 (Name "pt_perm_compose");
  1219     val pt_perm_compose_rev = PureThy.get_thm thy2 (Name "pt_perm_compose_rev");
  1220     val dj_perm_perm_forget = PureThy.get_thm thy2 (Name "dj_perm_perm_forget");
  1221 
  1222     fun composition_instance name1 name2 thy =
  1223       let
  1224         val name1' = Sign.base_name name1;
  1225         val name2' = Sign.base_name name2;
  1226         val cp_class = Sign.intern_class thy ("cp_" ^ name1' ^ "_" ^ name2');
  1227         val permT1 = mk_permT (Type (name1, []));
  1228         val permT2 = mk_permT (Type (name2, []));
  1229         val augment = map_type_tfree
  1230           (fn (x, S) => TFree (x, cp_class :: S));
  1231         val Ts = map (augment o body_type) perm_types;
  1232         val cp_inst = PureThy.get_thm thy
  1233           (Name ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst"));
  1234         val simps = simpset_of thy addsimps (perm_fun_def ::
  1235           (if name1 <> name2 then
  1236              let val dj = PureThy.get_thm thy (Name ("dj_" ^ name2' ^ "_" ^ name1'))
  1237              in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
  1238            else
  1239              let
  1240                val at_inst = PureThy.get_thm thy (Name ("at_" ^ name1' ^ "_inst"));
  1241                val pt_inst = PureThy.get_thm thy (Name ("pt_" ^ name1' ^ "_inst"))
  1242              in
  1243                [cp_inst RS cp1 RS sym,
  1244                 at_inst RS (pt_inst RS pt_perm_compose) RS sym,
  1245                 at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
  1246             end))
  1247         val thms = split_conj_thm (standard (Goal.prove thy [] []
  1248             (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1249               (map (fn ((s, T), x) =>
  1250                   let
  1251                     val pi1 = Free ("pi1", permT1);
  1252                     val pi2 = Free ("pi2", permT2);
  1253                     val perm1 = Const (s, permT1 --> T --> T);
  1254                     val perm2 = Const (s, permT2 --> T --> T);
  1255                     val perm3 = Const ("nominal.perm", permT1 --> permT2 --> permT2)
  1256                   in HOLogic.mk_eq
  1257                     (perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
  1258                      perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
  1259                   end)
  1260                 (perm_names ~~ Ts ~~ perm_indnames))))
  1261           (fn _ => EVERY [indtac induction perm_indnames 1,
  1262              ALLGOALS (asm_full_simp_tac simps)])))
  1263       in
  1264         foldl (fn ((s, tvs), thy) => AxClass.add_inst_arity_i
  1265             (s, replicate (length tvs) (cp_class :: classes), [cp_class])
  1266             (AxClass.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
  1267           thy (full_new_type_names' ~~ tyvars)
  1268       end;
  1269 
  1270     val (thy3, perm_thmss) = thy2 |>
  1271       fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
  1272       curry (Library.foldr (fn ((i, (tyname, args, _)), thy) =>
  1273         AxClass.add_inst_arity_i (tyname, replicate (length args) classes, classes)
  1274         (AxClass.intro_classes_tac [] THEN REPEAT (EVERY
  1275            [resolve_tac perm_empty_thms 1,
  1276             resolve_tac perm_append_thms 1,
  1277             resolve_tac perm_eq_thms 1, assume_tac 1])) thy))
  1278         (List.take (descr, length new_type_names)) |>
  1279       PureThy.add_thmss
  1280         [((space_implode "_" new_type_names ^ "_unfolded_perm_eq",
  1281           unfolded_perm_eq_thms), [Simplifier.simp_add_global]),
  1282          ((space_implode "_" new_type_names ^ "_perm_empty",
  1283           perm_empty_thms), [Simplifier.simp_add_global]),
  1284          ((space_implode "_" new_type_names ^ "_perm_append",
  1285           perm_append_thms), [Simplifier.simp_add_global]),
  1286          ((space_implode "_" new_type_names ^ "_perm_eq",
  1287           perm_eq_thms), [Simplifier.simp_add_global])];
  1288   
  1289     (**** Define representing sets ****)
  1290 
  1291     val _ = warning "representing sets";
  1292 
  1293     val rep_set_names = map (Sign.full_name thy3) (DatatypeProp.indexify_names
  1294       (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr));
  1295     val big_rep_name =
  1296       space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
  1297         (fn (i, ("nominal.nOption", _, _)) => NONE
  1298           | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
  1299     val _ = warning ("big_rep_name: " ^ big_rep_name);
  1300 
  1301     fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
  1302           (case AList.lookup op = descr i of
  1303              SOME ("nominal.nOption", _, [(_, [dt']), _]) =>
  1304                apfst (cons dt) (strip_option dt')
  1305            | _ => ([], dtf))
  1306       | strip_option dt = ([], dt);
  1307 
  1308     fun make_intr s T (cname, cargs) =
  1309       let
  1310         fun mk_prem (dt, (j, j', prems, ts)) = 
  1311           let
  1312             val (dts, dt') = strip_option dt;
  1313             val (dts', dt'') = strip_dtyp dt';
  1314             val Ts = map typ_of_dtyp dts;
  1315             val Us = map typ_of_dtyp dts';
  1316             val T = typ_of_dtyp dt'';
  1317             val free = mk_Free "x" (Us ---> T) j;
  1318             val free' = app_bnds free (length Us);
  1319             fun mk_abs_fun (T, (i, t)) =
  1320               let val U = fastype_of t
  1321               in (i + 1, Const ("nominal.abs_fun", [T, U, T] --->
  1322                 Type ("nominal.nOption", [U])) $ mk_Free "y" T i $ t)
  1323               end
  1324           in (j + 1, j' + length Ts,
  1325             case dt'' of
  1326                 DtRec k => list_all (map (pair "x") Us,
  1327                   HOLogic.mk_Trueprop (HOLogic.mk_mem (free',
  1328                     Const (List.nth (rep_set_names, k),
  1329                       HOLogic.mk_setT T)))) :: prems
  1330               | _ => prems,
  1331             snd (foldr mk_abs_fun (j', free) Ts) :: ts)
  1332           end;
  1333 
  1334         val (_, _, prems, ts) = foldr mk_prem (1, 1, [], []) cargs;
  1335         val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
  1336           (list_comb (Const (cname, map fastype_of ts ---> T), ts),
  1337            Const (s, HOLogic.mk_setT T)))
  1338       in Logic.list_implies (prems, concl)
  1339       end;
  1340 
  1341     val (intr_ts, ind_consts) =
  1342       apfst List.concat (ListPair.unzip (List.mapPartial
  1343         (fn ((_, ("nominal.nOption", _, _)), _) => NONE
  1344           | ((i, (_, _, constrs)), rep_set_name) =>
  1345               let val T = nth_dtyp i
  1346               in SOME (map (make_intr rep_set_name T) constrs,
  1347                 Const (rep_set_name, HOLogic.mk_setT T))
  1348               end)
  1349                 (descr ~~ rep_set_names)));
  1350 
  1351     val (thy4, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
  1352       setmp InductivePackage.quiet_mode false
  1353         (InductivePackage.add_inductive_i false true big_rep_name false true false
  1354            ind_consts (map (fn x => (("", x), [])) intr_ts) []) thy3;
  1355 
  1356     (**** Prove that representing set is closed under permutation ****)
  1357 
  1358     val _ = warning "proving closure under permutation...";
  1359 
  1360     val perm_indnames' = List.mapPartial
  1361       (fn (x, (_, ("nominal.nOption", _, _))) => NONE | (x, _) => SOME x)
  1362       (perm_indnames ~~ descr);
  1363 
  1364     fun mk_perm_closed name = map (fn th => standard (th RS mp))
  1365       (List.take (split_conj_thm (Goal.prove thy4 [] []
  1366         (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
  1367            (fn (S, x) =>
  1368               let
  1369                 val S = map_term_types (map_type_tfree
  1370                   (fn (s, cs) => TFree (s, cs union cp_classes))) S;
  1371                 val T = HOLogic.dest_setT (fastype_of S);
  1372                 val permT = mk_permT (Type (name, []))
  1373               in HOLogic.mk_imp (HOLogic.mk_mem (Free (x, T), S),
  1374                 HOLogic.mk_mem (Const ("nominal.perm", permT --> T --> T) $
  1375                   Free ("pi", permT) $ Free (x, T), S))
  1376               end) (ind_consts ~~ perm_indnames'))))
  1377         (fn _ => EVERY (* CU: added perm_fun_def in the final tactic in order to deal with funs *)
  1378            [indtac rep_induct [] 1,
  1379             ALLGOALS (simp_tac (simpset_of thy4 addsimps
  1380               (symmetric perm_fun_def :: PureThy.get_thms thy4 (Name ("abs_perm"))))),
  1381             ALLGOALS (resolve_tac rep_intrs 
  1382                THEN_ALL_NEW (asm_full_simp_tac (simpset_of thy4 addsimps [perm_fun_def])))])),
  1383         length new_type_names));
  1384 
  1385     (* FIXME: theorems are stored in database for testing only *)
  1386     val perm_closed_thmss = map mk_perm_closed atoms;
  1387     val (thy5, _) = PureThy.add_thmss [(("perm_closed",
  1388       List.concat perm_closed_thmss), [])] thy4;
  1389 
  1390     (**** typedef ****)
  1391 
  1392     val _ = warning "defining type...";
  1393 
  1394     val (thy6, typedefs) =
  1395       foldl_map (fn (thy, ((((name, mx), tvs), c), name')) =>
  1396         setmp TypedefPackage.quiet_mode true
  1397           (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE
  1398             (rtac exI 1 THEN
  1399               QUIET_BREADTH_FIRST (has_fewer_prems 1)
  1400               (resolve_tac rep_intrs 1))) thy |> (fn (thy, r) =>
  1401         let
  1402           val permT = mk_permT (TFree (variant tvs "'a", HOLogic.typeS));
  1403           val pi = Free ("pi", permT);
  1404           val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs;
  1405           val T = Type (Sign.intern_type thy name, tvs');
  1406           val Const (_, Type (_, [U])) = c
  1407         in apsnd (pair r o hd)
  1408           (PureThy.add_defs_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
  1409             (Const ("nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
  1410              Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
  1411                (Const ("nominal.perm", permT --> U --> U) $ pi $
  1412                  (Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $
  1413                    Free ("x", T))))), [])] thy)
  1414         end))
  1415           (thy5, types_syntax ~~ tyvars ~~
  1416             (List.take (ind_consts, length new_type_names)) ~~ new_type_names);
  1417 
  1418     val perm_defs = map snd typedefs;
  1419     val Abs_inverse_thms = map (#Abs_inverse o fst) typedefs;
  1420     val Rep_inverse_thms = map (#Rep_inverse o fst) typedefs;
  1421     val Rep_thms = map (#Rep o fst) typedefs;
  1422 
  1423     val big_name = space_implode "_" new_type_names;
  1424 
  1425 
  1426     (** prove that new types are in class pt_<name> **)
  1427 
  1428     val _ = warning "prove that new types are in class pt_<name> ...";
  1429 
  1430     fun pt_instance ((class, atom), perm_closed_thms) =
  1431       fold (fn (((({Abs_inverse, Rep_inverse, Rep, ...},
  1432         perm_def), name), tvs), perm_closed) => fn thy =>
  1433           AxClass.add_inst_arity_i
  1434             (Sign.intern_type thy name,
  1435               replicate (length tvs) (classes @ cp_classes), [class])
  1436             (EVERY [AxClass.intro_classes_tac [],
  1437               rewrite_goals_tac [perm_def],
  1438               asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
  1439               asm_full_simp_tac (simpset_of thy addsimps
  1440                 [Rep RS perm_closed RS Abs_inverse]) 1,
  1441               asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
  1442                 (Name ("pt_" ^ Sign.base_name atom ^ "3"))]) 1]) thy)
  1443         (typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms);
  1444 
  1445 
  1446     (** prove that new types are in class cp_<name1>_<name2> **)
  1447 
  1448     val _ = warning "prove that new types are in class cp_<name1>_<name2> ...";
  1449 
  1450     fun cp_instance (atom1, perm_closed_thms1) (atom2, perm_closed_thms2) thy =
  1451       let
  1452         val name = "cp_" ^ Sign.base_name atom1 ^ "_" ^ Sign.base_name atom2;
  1453         val class = Sign.intern_class thy name;
  1454         val cp1' = PureThy.get_thm thy (Name (name ^ "_inst")) RS cp1
  1455       in fold (fn ((((({Abs_inverse, Rep_inverse, Rep, ...},
  1456         perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
  1457           AxClass.add_inst_arity_i
  1458             (Sign.intern_type thy name,
  1459               replicate (length tvs) (classes @ cp_classes), [class])
  1460             (EVERY [AxClass.intro_classes_tac [],
  1461               rewrite_goals_tac [perm_def],
  1462               asm_full_simp_tac (simpset_of thy addsimps
  1463                 ((Rep RS perm_closed1 RS Abs_inverse) ::
  1464                  (if atom1 = atom2 then []
  1465                   else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
  1466               cong_tac 1,
  1467               rtac refl 1,
  1468               rtac cp1' 1]) thy)
  1469         (typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms1 ~~
  1470           perm_closed_thms2) thy
  1471       end;
  1472 
  1473     val thy7 = fold (fn x => fn thy => thy |>
  1474       pt_instance x |>
  1475       fold (cp_instance (apfst snd x)) (atoms ~~ perm_closed_thmss))
  1476         (classes ~~ atoms ~~ perm_closed_thmss) thy6;
  1477 
  1478     (**** constructors ****)
  1479 
  1480     fun mk_abs_fun (x, t) =
  1481       let
  1482         val T = fastype_of x;
  1483         val U = fastype_of t
  1484       in
  1485         Const ("nominal.abs_fun", T --> U --> T -->
  1486           Type ("nominal.nOption", [U])) $ x $ t
  1487       end;
  1488 
  1489     val (ty_idxs, _) = foldl
  1490       (fn ((i, ("nominal.nOption", _, _)), p) => p
  1491         | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
  1492 
  1493     fun reindex (DtType (s, dts)) = DtType (s, map reindex dts)
  1494       | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i))
  1495       | reindex dt = dt;
  1496 
  1497     fun strip_suffix i s = implode (List.take (explode s, size s - i));
  1498 
  1499     (** strips the "_Rep" in type names *)
  1500     fun strip_nth_name i s = 
  1501       let val xs = NameSpace.unpack s; 
  1502       in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
  1503 
  1504     val descr'' = List.mapPartial
  1505       (fn (i, ("nominal.nOption", _, _)) => NONE
  1506         | (i, (s, dts, constrs)) => SOME (the (AList.lookup op = ty_idxs i),
  1507             (strip_nth_name 1 s,  map reindex dts,
  1508              map (fn (cname, cargs) =>
  1509                (strip_nth_name 2 cname,
  1510                 foldl (fn (dt, dts) =>
  1511                   let val (dts', dt') = strip_option dt
  1512                   in (dts @ dts' @ [reindex dt']) end) [] cargs)) constrs))) descr;
  1513 
  1514     val (descr1, descr2) = splitAt (length new_type_names, descr'');
  1515     val descr' = [descr1, descr2];
  1516 
  1517     val typ_of_dtyp' = replace_types' o typ_of_dtyp;
  1518 
  1519     val rep_names = map (fn s =>
  1520       Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
  1521     val abs_names = map (fn s =>
  1522       Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
  1523 
  1524     val recTs' = List.mapPartial
  1525       (fn ((_, ("nominal.nOption", _, _)), T) => NONE
  1526         | (_, T) => SOME T) (descr ~~ get_rec_types descr sorts');
  1527     val recTs = get_rec_types (List.concat descr') sorts';
  1528     val newTs' = Library.take (length new_type_names, recTs');
  1529     val newTs = Library.take (length new_type_names, recTs);
  1530 
  1531     val full_new_type_names = map (Sign.full_name (sign_of thy)) new_type_names;
  1532 
  1533     fun make_constr_def tname T T' ((thy, defs, eqns), ((cname, cargs), (cname', mx))) =
  1534       let
  1535         fun constr_arg (dt, (j, l_args, r_args)) =
  1536           let
  1537             val x' = mk_Free "x" (typ_of_dtyp' dt) j;
  1538             val (dts, dt') = strip_option dt;
  1539             val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp' dt) i)
  1540               (dts ~~ (j upto j + length dts - 1))
  1541             val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts)
  1542             val (dts', dt'') = strip_dtyp dt'
  1543           in case dt'' of
  1544               DtRec k => if k < length new_type_names then
  1545                   (j + length dts + 1,
  1546                    xs @ x :: l_args,
  1547                    foldr mk_abs_fun
  1548                      (list_abs (map (pair "z" o typ_of_dtyp') dts',
  1549                        Const (List.nth (rep_names, k), typ_of_dtyp' dt'' -->
  1550                          typ_of_dtyp dt'') $ app_bnds x (length dts')))
  1551                      xs :: r_args)
  1552                 else error "nested recursion not (yet) supported"
  1553             | _ => (j + 1, x' :: l_args, x' :: r_args)
  1554           end
  1555 
  1556         val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs;
  1557         val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname);
  1558         val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname);
  1559         val constrT = map fastype_of l_args ---> T;
  1560         val lhs = list_comb (Const (Sign.full_name thy (Sign.base_name cname),
  1561           constrT), l_args);
  1562         val rhs = list_comb (Const (cname, map fastype_of r_args ---> T'), r_args);
  1563         val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs);
  1564         val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
  1565           (Const (rep_name, T --> T') $ lhs, rhs));
  1566         val def_name = (Sign.base_name cname) ^ "_def";
  1567         val (thy', [def_thm]) = thy |>
  1568           Theory.add_consts_i [(cname', constrT, mx)] |>
  1569           (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]
  1570       in (thy', defs @ [def_thm], eqns @ [eqn]) end;
  1571 
  1572     fun dt_constr_defs ((thy, defs, eqns, dist_lemmas),
  1573         (((((_, (_, _, constrs)), tname), T), T'), constr_syntax)) =
  1574       let
  1575         val rep_const = cterm_of thy
  1576           (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
  1577         val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
  1578         val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
  1579           ((Theory.add_path tname thy, defs, []), constrs ~~ constr_syntax)
  1580       in
  1581         (parent_path flat_names thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
  1582       end;
  1583 
  1584     val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs
  1585       ((thy7, [], [], []), List.take (descr, length new_type_names) ~~
  1586         new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax);
  1587 
  1588     val abs_inject_thms = map (fn tname =>
  1589       PureThy.get_thm thy8 (Name ("Abs_" ^ tname ^ "_inject"))) new_type_names;
  1590 
  1591     val rep_inject_thms = map (fn tname =>
  1592       PureThy.get_thm thy8 (Name ("Rep_" ^ tname ^ "_inject"))) new_type_names;
  1593 
  1594     val rep_thms = map (fn tname =>
  1595       PureThy.get_thm thy8 (Name ("Rep_" ^ tname))) new_type_names;
  1596 
  1597     val rep_inverse_thms = map (fn tname =>
  1598       PureThy.get_thm thy8 (Name ("Rep_" ^ tname ^ "_inverse"))) new_type_names;
  1599 
  1600     (* prove theorem  Rep_i (Constr_j ...) = Constr'_j ...  *)
  1601     
  1602     fun prove_constr_rep_thm eqn =
  1603       let
  1604         val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
  1605         val rewrites = constr_defs @ map mk_meta_eq rep_inverse_thms
  1606       in standard (Goal.prove thy8 [] [] eqn (fn _ => EVERY
  1607         [resolve_tac inj_thms 1,
  1608          rewrite_goals_tac rewrites,
  1609          rtac refl 3,
  1610          resolve_tac rep_intrs 2,
  1611          REPEAT (resolve_tac rep_thms 1)]))
  1612       end;
  1613 
  1614     val constr_rep_thmss = map (map prove_constr_rep_thm) constr_rep_eqns;
  1615 
  1616     (* prove theorem  pi \<bullet> Rep_i x = Rep_i (pi \<bullet> x) *)
  1617 
  1618     fun prove_perm_rep_perm (atom, perm_closed_thms) = map (fn th =>
  1619       let
  1620         val _ $ (_ $ (Rep $ x) $ _) = Logic.unvarify (prop_of th);
  1621         val Type ("fun", [T, U]) = fastype_of Rep;
  1622         val permT = mk_permT (Type (atom, []));
  1623         val pi = Free ("pi", permT);
  1624       in
  1625         standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1626             (Const ("nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
  1627              Rep $ (Const ("nominal.perm", permT --> T --> T) $ pi $ x))))
  1628           (fn _ => simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @
  1629             perm_closed_thms @ Rep_thms)) 1))
  1630       end) Rep_thms;
  1631 
  1632     val perm_rep_perm_thms = List.concat (map prove_perm_rep_perm
  1633       (atoms ~~ perm_closed_thmss));
  1634 
  1635     (* prove distinctness theorems *)
  1636 
  1637     val distinct_props = setmp DatatypeProp.dtK 1000
  1638       (DatatypeProp.make_distincts new_type_names descr' sorts') thy8;
  1639 
  1640     val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
  1641       dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
  1642         (constr_rep_thmss ~~ dist_lemmas);
  1643 
  1644     fun prove_distinct_thms (_, []) = []
  1645       | prove_distinct_thms (p as (rep_thms, dist_lemma), t::ts) =
  1646           let
  1647             val dist_thm = standard (Goal.prove thy8 [] [] t (fn _ =>
  1648               simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1))
  1649           in dist_thm::(standard (dist_thm RS not_sym))::
  1650             (prove_distinct_thms (p, ts))
  1651           end;
  1652 
  1653     val distinct_thms = map prove_distinct_thms
  1654       (constr_rep_thmss ~~ dist_lemmas ~~ distinct_props);
  1655 
  1656     (** prove equations for permutation functions **)
  1657 
  1658     val abs_perm = PureThy.get_thms thy8 (Name "abs_perm"); (* FIXME *)
  1659 
  1660     val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
  1661       let val T = replace_types' (nth_dtyp i)
  1662       in List.concat (map (fn (atom, perm_closed_thms) =>
  1663           map (fn ((cname, dts), constr_rep_thm) => 
  1664         let
  1665           val cname = Sign.intern_const thy8
  1666             (NameSpace.append tname (Sign.base_name cname));
  1667           val permT = mk_permT (Type (atom, []));
  1668           val pi = Free ("pi", permT);
  1669 
  1670           fun perm t =
  1671             let val T = fastype_of t
  1672             in Const ("nominal.perm", permT --> T --> T) $ pi $ t end;
  1673 
  1674           fun constr_arg (dt, (j, l_args, r_args)) =
  1675             let
  1676               val x' = mk_Free "x" (typ_of_dtyp' dt) j;
  1677               val (dts, dt') = strip_option dt;
  1678               val Ts = map typ_of_dtyp' dts;
  1679               val xs = map (fn (T, i) => mk_Free "x" T i)
  1680                 (Ts ~~ (j upto j + length dts - 1))
  1681               val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
  1682               val (dts', dt'') = strip_dtyp dt';
  1683             in case dt'' of
  1684                 DtRec k => if k < length new_type_names then
  1685                     (j + length dts + 1,
  1686                      xs @ x :: l_args,
  1687                      map perm (xs @ [x]) @ r_args)
  1688                   else error "nested recursion not (yet) supported"
  1689               | _ => (j + 1, x' :: l_args, perm x' :: r_args)
  1690             end
  1691 
  1692           val (_, l_args, r_args) = foldr constr_arg (1, [], []) dts;
  1693           val c = Const (cname, map fastype_of l_args ---> T)
  1694         in
  1695           standard (Goal.prove thy8 [] []
  1696             (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1697               (perm (list_comb (c, l_args)), list_comb (c, r_args))))
  1698             (fn _ => EVERY
  1699               [simp_tac (simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1,
  1700                simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @
  1701                  constr_defs @ perm_closed_thms)) 1,
  1702                TRY (simp_tac (HOL_basic_ss addsimps
  1703                  (symmetric perm_fun_def :: abs_perm)) 1),
  1704                TRY (simp_tac (HOL_basic_ss addsimps
  1705                  (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
  1706                     perm_closed_thms)) 1)]))
  1707         end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss))
  1708       end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
  1709 
  1710     (** prove injectivity of constructors **)
  1711 
  1712     val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
  1713     val alpha = PureThy.get_thms thy8 (Name "alpha");
  1714     val abs_fresh = PureThy.get_thms thy8 (Name "abs_fresh");
  1715     val fresh_def = PureThy.get_thm thy8 (Name "fresh_def");
  1716     val supp_def = PureThy.get_thm thy8 (Name "supp_def");
  1717 
  1718     val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
  1719       let val T = replace_types' (nth_dtyp i)
  1720       in List.mapPartial (fn ((cname, dts), constr_rep_thm) =>
  1721         if null dts then NONE else SOME
  1722         let
  1723           val cname = Sign.intern_const thy8
  1724             (NameSpace.append tname (Sign.base_name cname));
  1725 
  1726           fun make_inj (dt, (j, args1, args2, eqs)) =
  1727             let
  1728               val x' = mk_Free "x" (typ_of_dtyp' dt) j;
  1729               val y' = mk_Free "y" (typ_of_dtyp' dt) j;
  1730               val (dts, dt') = strip_option dt;
  1731               val Ts_idx = map typ_of_dtyp' dts ~~ (j upto j + length dts - 1);
  1732               val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
  1733               val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx;
  1734               val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
  1735               val y = mk_Free "y" (typ_of_dtyp' dt') (j + length dts);
  1736               val (dts', dt'') = strip_dtyp dt';
  1737             in case dt'' of
  1738                 DtRec k => if k < length new_type_names then
  1739                     (j + length dts + 1,
  1740                      xs @ (x :: args1), ys @ (y :: args2),
  1741                      HOLogic.mk_eq
  1742                        (foldr mk_abs_fun x xs, foldr mk_abs_fun y ys) :: eqs)
  1743                   else error "nested recursion not (yet) supported"
  1744               | _ => (j + 1, x' :: args1, y' :: args2, HOLogic.mk_eq (x', y') :: eqs)
  1745             end;
  1746 
  1747           val (_, args1, args2, eqs) = foldr make_inj (1, [], [], []) dts;
  1748           val Ts = map fastype_of args1;
  1749           val c = Const (cname, Ts ---> T)
  1750         in
  1751           standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1752               (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)),
  1753                foldr1 HOLogic.mk_conj eqs)))
  1754             (fn _ => EVERY
  1755                [asm_full_simp_tac (simpset_of thy8 addsimps (constr_rep_thm ::
  1756                   rep_inject_thms')) 1,
  1757                 TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def ::
  1758                   alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
  1759                   perm_rep_perm_thms)) 1),
  1760                 TRY (asm_full_simp_tac (HOL_basic_ss addsimps (perm_fun_def ::
  1761                   expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)]))
  1762         end) (constrs ~~ constr_rep_thms)
  1763       end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
  1764 
  1765     (** equations for support and freshness **)
  1766 
  1767     val Un_assoc = PureThy.get_thm thy8 (Name "Un_assoc");
  1768     val de_Morgan_conj = PureThy.get_thm thy8 (Name "de_Morgan_conj");
  1769     val Collect_disj_eq = PureThy.get_thm thy8 (Name "Collect_disj_eq");
  1770     val finite_Un = PureThy.get_thm thy8 (Name "finite_Un");
  1771 
  1772     val (supp_thms, fresh_thms) = ListPair.unzip (map ListPair.unzip
  1773       (map (fn ((((i, (_, _, constrs)), tname), inject_thms'), perm_thms') =>
  1774       let val T = replace_types' (nth_dtyp i)
  1775       in List.concat (map (fn (cname, dts) => map (fn atom =>
  1776         let
  1777           val cname = Sign.intern_const thy8
  1778             (NameSpace.append tname (Sign.base_name cname));
  1779           val atomT = Type (atom, []);
  1780 
  1781           fun process_constr (dt, (j, args1, args2)) =
  1782             let
  1783               val x' = mk_Free "x" (typ_of_dtyp' dt) j;
  1784               val (dts, dt') = strip_option dt;
  1785               val Ts_idx = map typ_of_dtyp' dts ~~ (j upto j + length dts - 1);
  1786               val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
  1787               val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
  1788               val (dts', dt'') = strip_dtyp dt';
  1789             in case dt'' of
  1790                 DtRec k => if k < length new_type_names then
  1791                     (j + length dts + 1,
  1792                      xs @ (x :: args1), foldr mk_abs_fun x xs :: args2)
  1793                   else error "nested recursion not (yet) supported"
  1794               | _ => (j + 1, x' :: args1, x' :: args2)
  1795             end;
  1796 
  1797           val (_, args1, args2) = foldr process_constr (1, [], []) dts;
  1798           val Ts = map fastype_of args1;
  1799           val c = list_comb (Const (cname, Ts ---> T), args1);
  1800           fun supp t =
  1801             Const ("nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
  1802           fun fresh t =
  1803             Const ("nominal.fresh", atomT --> fastype_of t --> HOLogic.boolT) $
  1804               Free ("a", atomT) $ t;
  1805           val supp_thm = standard (Goal.prove thy8 [] []
  1806               (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1807                 (supp c,
  1808                  if null dts then Const ("{}", HOLogic.mk_setT atomT)
  1809                  else foldr1 (HOLogic.mk_binop "op Un") (map supp args2))))
  1810             (fn _ =>
  1811               simp_tac (HOL_basic_ss addsimps (supp_def ::
  1812                  Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
  1813                  symmetric empty_def :: Finites.emptyI :: simp_thms @
  1814                  abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1))
  1815         in
  1816           (supp_thm,
  1817            standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1818               (fresh c,
  1819                if null dts then HOLogic.true_const
  1820                else foldr1 HOLogic.mk_conj (map fresh args2))))
  1821              (fn _ =>
  1822                simp_tac (simpset_of thy8 addsimps [fresh_def, supp_thm]) 1)))
  1823         end) atoms) constrs)
  1824       end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
  1825 
  1826     (**** Induction theorem ****)
  1827 
  1828     val arities = get_arities (List.concat descr');
  1829 
  1830     fun mk_funs_inv thm =
  1831       let
  1832         val {sign, prop, ...} = rep_thm thm;
  1833         val _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $
  1834           (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
  1835         val used = add_term_tfree_names (a, []);
  1836 
  1837         fun mk_thm i =
  1838           let
  1839             val Ts = map (TFree o rpair HOLogic.typeS)
  1840               (variantlist (replicate i "'t", used));
  1841             val f = Free ("f", Ts ---> U)
  1842           in standard (Goal.prove sign [] [] (Logic.mk_implies
  1843             (HOLogic.mk_Trueprop (HOLogic.list_all
  1844                (map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))),
  1845              HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
  1846                r $ (a $ app_bnds f i)), f))))
  1847             (fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1]))
  1848           end
  1849       in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
  1850 
  1851     fun mk_indrule_lemma ((prems, concls), (((i, _), T), U)) =
  1852       let
  1853         val Rep_t = Const (List.nth (rep_names, i), T --> U) $
  1854           mk_Free "x" T i;
  1855 
  1856         val Abs_t =  Const (List.nth (abs_names, i), U --> T)
  1857 
  1858       in (prems @ [HOLogic.imp $ HOLogic.mk_mem (Rep_t,
  1859             Const (List.nth (rep_set_names, i), HOLogic.mk_setT U)) $
  1860               (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
  1861           concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
  1862       end;
  1863 
  1864     val (indrule_lemma_prems, indrule_lemma_concls) =
  1865       Library.foldl mk_indrule_lemma (([], []), (List.concat descr' ~~ recTs ~~ recTs'));
  1866 
  1867     val indrule_lemma = standard (Goal.prove thy8 [] []
  1868       (Logic.mk_implies
  1869         (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
  1870          HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
  1871            [REPEAT (etac conjE 1),
  1872             REPEAT (EVERY
  1873               [TRY (rtac conjI 1), full_simp_tac (HOL_basic_ss addsimps Rep_inverse_thms) 1,
  1874                etac mp 1, resolve_tac Rep_thms 1])]));
  1875 
  1876     val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
  1877     val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
  1878       map (Free o apfst fst o dest_Var) Ps;
  1879     val indrule_lemma' = cterm_instantiate
  1880       (map (cterm_of thy8) Ps ~~ map (cterm_of thy8) frees) indrule_lemma;
  1881 
  1882     val Abs_inverse_thms' = List.concat (map mk_funs_inv Abs_inverse_thms);
  1883 
  1884     val dt_induct_prop = DatatypeProp.make_ind descr' sorts';
  1885     val dt_induct = standard (Goal.prove thy8 []
  1886       (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
  1887       (fn prems => EVERY
  1888         [rtac indrule_lemma' 1,
  1889          (DatatypeAux.indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
  1890          EVERY (map (fn (prem, r) => (EVERY
  1891            [REPEAT (eresolve_tac Abs_inverse_thms' 1),
  1892             simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
  1893             DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
  1894                 (prems ~~ constr_defs))]));
  1895 
  1896     val case_names_induct = mk_case_names_induct (List.concat descr');
  1897 
  1898     val (thy9, _) = thy8 |>
  1899       Theory.add_path big_name |>
  1900       PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] |>>
  1901       Theory.parent_path |>>>
  1902       DatatypeAux.store_thmss "distinct" new_type_names distinct_thms |>>>
  1903       DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss |>>>
  1904       DatatypeAux.store_thmss "perm" new_type_names perm_simps' |>>>
  1905       DatatypeAux.store_thmss "inject" new_type_names inject_thms |>>>
  1906       DatatypeAux.store_thmss "supp" new_type_names supp_thms |>>>
  1907       DatatypeAux.store_thmss "fresh" new_type_names fresh_thms;
  1908 
  1909   in
  1910     (thy9, perm_eq_thms)
  1911   end;
  1912 
  1913 val add_nominal_datatype = gen_add_nominal_datatype read_typ true;
  1914 
  1915 
  1916 (* FIXME: The following stuff should be exported by DatatypePackage *)
  1917 
  1918 local structure P = OuterParse and K = OuterKeyword in
  1919 
  1920 val datatype_decl =
  1921   Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
  1922     (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
  1923 
  1924 fun mk_datatype args =
  1925   let
  1926     val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
  1927     val specs = map (fn ((((_, vs), t), mx), cons) =>
  1928       (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
  1929   in #1 o add_nominal_datatype false names specs end;
  1930 
  1931 val nominal_datatypeP =
  1932   OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
  1933     (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
  1934 
  1935 val _ = OuterSyntax.add_parsers [nominal_datatypeP];
  1936 
  1937 end;
  1938 
  1939 end