src/HOL/Nominal/nominal_package.ML
author berghofe
Fri Oct 28 18:22:26 2005 +0200 (2005-10-28)
changeset 18016 8f3a80033ba4
parent 18010 c885c93a9324
child 18017 f6abeac6dcb5
permissions -rw-r--r--
Implemented proof of weak induction theorem.
     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 
   774        (* abs_perm collects all lemmas for simplifying a permutation *)
   775        (* in front of an abs_fun                                     *)
   776        val (thy33,_) = 
   777 	   let 
   778 	     val name = "abs_perm"
   779              val thm_list = Library.flat (map (fn (ak_name, T) =>
   780 	        let	
   781 		  val at_inst = PureThy.get_thm thy32 (Name ("at_"^ak_name^"_inst"));
   782 		  val pt_inst = PureThy.get_thm thy32 (Name ("pt_"^ak_name^"_inst"));	      
   783 	          val thm = [pt_inst, at_inst] MRS abs_fun_pi
   784                   val thm_list = map (fn (ak_name', T') =>
   785                      let
   786                       val cp_inst = PureThy.get_thm thy32 (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   787 	             in
   788                      [pt_inst, pt_inst, at_inst, cp_inst] MRS abs_fun_pi_ineq
   789 	             end) ak_names_types;
   790                  in thm::thm_list end) (ak_names_types))
   791            in
   792              (PureThy.add_thmss [((name, thm_list),[])] thy32)
   793            end;
   794 
   795         (* alpha collects all lemmas analysing an equation *)
   796         (* between abs_funs                                *)
   797         (*val (thy34,_) = 
   798 	   let 
   799 	     val name = "alpha"
   800              val thm_list = map (fn (ak_name, T) =>
   801 	        let	
   802 		  val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
   803 		  val pt_inst = PureThy.get_thm thy33 (Name ("pt_"^ak_name^"_inst"));	      
   804 	        in
   805                   [pt_inst, at_inst] MRS abs_fun_eq
   806 	        end) ak_names_types
   807            in
   808              (PureThy.add_thmss [((name, thm_list),[])] thy33)
   809            end;*)
   810  
   811           val (thy34,_) = 
   812 	   let 
   813 	     fun inst_pt_at thm ak_name =
   814 		 let	
   815 		   val at_inst = PureThy.get_thm thy33 (Name ("at_"^ak_name^"_inst"));
   816 		   val pt_inst = PureThy.get_thm thy33 (Name ("pt_"^ak_name^"_inst"));	      
   817 	         in
   818                      [pt_inst, at_inst] MRS thm
   819 	         end	 
   820 
   821            in
   822             thy33 
   823 	    |> PureThy.add_thmss   [(("alpha", map (inst_pt_at abs_fun_eq) ak_names),[])]
   824             |>>> PureThy.add_thmss [(("perm_swap", map (inst_pt_at pt_swap_bij) ak_names),[])]
   825             |>>> PureThy.add_thmss [(("perm_fresh_fresh", map (inst_pt_at pt_fresh_fresh) ak_names),[])]
   826             |>>> PureThy.add_thmss [(("perm_bij", map (inst_pt_at pt_bij) ak_names),[])]
   827             |>>> PureThy.add_thmss [(("perm_compose", map (inst_pt_at pt_perm_compose) ak_names),[])]
   828             |>>> PureThy.add_thmss [(("perm_app_eq", map (inst_pt_at perm_eq_app) ak_names),[])]
   829 	   end;
   830 
   831          (* perm_dj collects all lemmas that forget an permutation *)
   832          (* when it acts on an atom of different type              *)
   833          val (thy35,_) = 
   834 	   let 
   835 	     val name = "perm_dj"
   836              val thm_list = Library.flat (map (fn (ak_name, T) =>
   837 	        Library.flat (map (fn (ak_name', T') => 
   838                  if not (ak_name = ak_name') 
   839                  then 
   840 		    let
   841                       val dj_inst = PureThy.get_thm thy34 (Name ("dj_"^ak_name^"_"^ak_name'));
   842                     in
   843                       [dj_inst RS dj_perm_forget, dj_inst RS dj_pp_forget]
   844                     end 
   845                  else []) ak_names_types)) ak_names_types)
   846            in
   847              (PureThy.add_thmss [((name, thm_list),[])] thy34)
   848            end;
   849 
   850          (* abs_fresh collects all lemmas for simplifying a freshness *)
   851          (* proposition involving an abs_fun                          *)
   852 
   853          val (thy36,_) = 
   854 	   let 
   855 	     val name = "abs_fresh"
   856              val thm_list = Library.flat (map (fn (ak_name, T) =>
   857 	        let	
   858 		  val at_inst = PureThy.get_thm thy35 (Name ("at_"^ak_name^"_inst"));
   859 		  val pt_inst = PureThy.get_thm thy35 (Name ("pt_"^ak_name^"_inst"));
   860                   val fs_inst = PureThy.get_thm thy35 (Name ("fs_"^ak_name^"_inst"));	      
   861 	          val thm = [pt_inst, at_inst, (fs_inst RS fs1)] MRS fresh_iff
   862                   val thm_list = Library.flat (map (fn (ak_name', T') =>
   863                      (if (not (ak_name = ak_name')) 
   864                      then
   865                        let
   866                         val cp_inst = PureThy.get_thm thy35 (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   867 	                val dj_inst = PureThy.get_thm thy35 (Name ("dj_"^ak_name'^"_"^ak_name));
   868                        in
   869                         [[pt_inst, pt_inst, at_inst, cp_inst, dj_inst] MRS fresh_iff_ineq]
   870 	               end
   871                      else [])) ak_names_types);
   872                  in thm::thm_list end) (ak_names_types))
   873            in
   874              (PureThy.add_thmss [((name, thm_list),[])] thy35)
   875            end;
   876 
   877          (* abs_supp collects all lemmas for simplifying  *)
   878          (* support proposition involving an abs_fun      *)
   879 
   880          val (thy37,_) = 
   881 	   let 
   882 	     val name = "abs_supp"
   883              val thm_list = Library.flat (map (fn (ak_name, T) =>
   884 	        let	
   885 		  val at_inst = PureThy.get_thm thy36 (Name ("at_"^ak_name^"_inst"));
   886 		  val pt_inst = PureThy.get_thm thy36 (Name ("pt_"^ak_name^"_inst"));
   887                   val fs_inst = PureThy.get_thm thy36 (Name ("fs_"^ak_name^"_inst"));	      
   888 	          val thm1 = [pt_inst, at_inst, (fs_inst RS fs1)] MRS abs_fun_supp
   889                   val thm2 = [pt_inst, at_inst] MRS abs_fun_supp
   890                   val thm_list = Library.flat (map (fn (ak_name', T') =>
   891                      (if (not (ak_name = ak_name')) 
   892                      then
   893                        let
   894                         val cp_inst = PureThy.get_thm thy36 (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   895 	                val dj_inst = PureThy.get_thm thy36 (Name ("dj_"^ak_name'^"_"^ak_name));
   896                        in
   897                         [[pt_inst, pt_inst, at_inst, cp_inst, dj_inst] MRS abs_fun_supp_ineq]
   898 	               end
   899                      else [])) ak_names_types);
   900                  in thm1::thm2::thm_list end) (ak_names_types))
   901            in
   902              (PureThy.add_thmss [((name, thm_list),[])] thy36)
   903            end;
   904 
   905     in NominalData.put (fold Symtab.update (map (rpair ()) full_ak_names)
   906       (NominalData.get thy11)) thy37
   907     end;
   908 
   909 
   910 (* syntax und parsing *)
   911 structure P = OuterParse and K = OuterKeyword;
   912 
   913 val atom_declP =
   914   OuterSyntax.command "atom_decl" "Declare new kinds of atoms" K.thy_decl
   915     (Scan.repeat1 P.name >> (Toplevel.theory o create_nom_typedecls));
   916 
   917 val _ = OuterSyntax.add_parsers [atom_declP];
   918 
   919 val setup = [NominalData.init];
   920 
   921 (*=======================================================================*)
   922 
   923 (** FIXME: DatatypePackage should export this function **)
   924 
   925 local
   926 
   927 fun dt_recs (DtTFree _) = []
   928   | dt_recs (DtType (_, dts)) = List.concat (map dt_recs dts)
   929   | dt_recs (DtRec i) = [i];
   930 
   931 fun dt_cases (descr: descr) (_, args, constrs) =
   932   let
   933     fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
   934     val bnames = map the_bname (distinct (List.concat (map dt_recs args)));
   935   in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
   936 
   937 
   938 fun induct_cases descr =
   939   DatatypeProp.indexify_names (List.concat (map (dt_cases descr) (map #2 descr)));
   940 
   941 fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
   942 
   943 in
   944 
   945 fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
   946 
   947 fun mk_case_names_exhausts descr new =
   948   map (RuleCases.case_names o exhaust_cases descr o #1)
   949     (List.filter (fn ((_, (name, _, _))) => name mem_string new) descr);
   950 
   951 end;
   952 
   953 (*******************************)
   954 
   955 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
   956 
   957 fun read_typ sign ((Ts, sorts), str) =
   958   let
   959     val T = Type.no_tvars (Sign.read_typ (sign, (AList.lookup op =)
   960       (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
   961   in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
   962 
   963 (** taken from HOL/Tools/datatype_aux.ML **)
   964 
   965 fun indtac indrule indnames i st =
   966   let
   967     val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
   968     val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop
   969       (Logic.strip_imp_concl (List.nth (prems_of st, i - 1))));
   970     val getP = if can HOLogic.dest_imp (hd ts) then
   971       (apfst SOME) o HOLogic.dest_imp else pair NONE;
   972     fun abstr (t1, t2) = (case t1 of
   973         NONE => (case filter (fn Free (s, _) => s mem indnames | _ => false)
   974               (term_frees t2) of
   975             [Free (s, T)] => absfree (s, T, t2)
   976           | _ => sys_error "indtac")
   977       | SOME (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2)))
   978     val cert = cterm_of (Thm.sign_of_thm st);
   979     val Ps = map (cert o head_of o snd o getP) ts;
   980     val indrule' = cterm_instantiate (Ps ~~
   981       (map (cert o abstr o getP) ts')) indrule
   982   in
   983     rtac indrule' i st
   984   end;
   985 
   986 fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
   987   let
   988     (* this theory is used just for parsing *)
   989   
   990     val tmp_thy = thy |>
   991       Theory.copy |>
   992       Theory.add_types (map (fn (tvs, tname, mx, _) =>
   993         (tname, length tvs, mx)) dts);
   994 
   995     val sign = Theory.sign_of tmp_thy;
   996 
   997     val atoms = atoms_of thy;
   998     val classes = map (NameSpace.map_base (fn s => "pt_" ^ s)) atoms;
   999     val cp_classes = List.concat (map (fn atom1 => map (fn atom2 =>
  1000       Sign.intern_class thy ("cp_" ^ Sign.base_name atom1 ^ "_" ^
  1001         Sign.base_name atom2)) atoms) atoms);
  1002     fun augment_sort S = S union classes;
  1003     val augment_sort_typ = map_type_tfree (fn (s, S) => TFree (s, augment_sort S));
  1004 
  1005     fun prep_constr ((constrs, sorts), (cname, cargs, mx)) =
  1006       let val (cargs', sorts') = Library.foldl (prep_typ sign) (([], sorts), cargs)
  1007       in (constrs @ [(cname, cargs', mx)], sorts') end
  1008 
  1009     fun prep_dt_spec ((dts, sorts), (tvs, tname, mx, constrs)) =
  1010       let val (constrs', sorts') = Library.foldl prep_constr (([], sorts), constrs)
  1011       in (dts @ [(tvs, tname, mx, constrs')], sorts') end
  1012 
  1013     val (dts', sorts) = Library.foldl prep_dt_spec (([], []), dts);
  1014     val sorts' = map (apsnd augment_sort) sorts;
  1015     val tyvars = map #1 dts';
  1016 
  1017     val types_syntax = map (fn (tvs, tname, mx, constrs) => (tname, mx)) dts';
  1018     val constr_syntax = map (fn (tvs, tname, mx, constrs) =>
  1019       map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts';
  1020 
  1021     val ps = map (fn (_, n, _, _) =>
  1022       (Sign.full_name sign n, Sign.full_name sign (n ^ "_Rep"))) dts;
  1023     val rps = map Library.swap ps;
  1024 
  1025     fun replace_types (Type ("nominal.ABS", [T, U])) = 
  1026           Type ("fun", [T, Type ("nominal.nOption", [replace_types U])])
  1027       | replace_types (Type (s, Ts)) =
  1028           Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
  1029       | replace_types T = T;
  1030 
  1031     fun replace_types' (Type (s, Ts)) =
  1032           Type (getOpt (AList.lookup op = rps s, s), map replace_types' Ts)
  1033       | replace_types' T = T;
  1034 
  1035     val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, tname ^ "_Rep", NoSyn,
  1036       map (fn (cname, cargs, mx) => (cname,
  1037         map (augment_sort_typ o replace_types) cargs, NoSyn)) constrs)) dts';
  1038 
  1039     val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
  1040     val full_new_type_names' = map (Sign.full_name (sign_of thy)) new_type_names';
  1041 
  1042     val (thy1, {induction, ...}) =
  1043       DatatypePackage.add_datatype_i err flat_names new_type_names' dts'' thy;
  1044 
  1045     val SOME {descr, ...} = Symtab.lookup
  1046       (DatatypePackage.get_datatypes thy1) (hd full_new_type_names');
  1047     val typ_of_dtyp = typ_of_dtyp descr sorts';
  1048     fun nth_dtyp i = typ_of_dtyp (DtRec i);
  1049 
  1050     (**** define permutation functions ****)
  1051 
  1052     val permT = mk_permT (TFree ("'x", HOLogic.typeS));
  1053     val pi = Free ("pi", permT);
  1054     val perm_types = map (fn (i, _) =>
  1055       let val T = nth_dtyp i
  1056       in permT --> T --> T end) descr;
  1057     val perm_names = replicate (length new_type_names) "nominal.perm" @
  1058       DatatypeProp.indexify_names (map (fn i => Sign.full_name (sign_of thy1)
  1059         ("perm_" ^ name_of_typ (nth_dtyp i)))
  1060           (length new_type_names upto length descr - 1));
  1061     val perm_names_types = perm_names ~~ perm_types;
  1062 
  1063     val perm_eqs = List.concat (map (fn (i, (_, _, constrs)) =>
  1064       let val T = nth_dtyp i
  1065       in map (fn (cname, dts) => 
  1066         let
  1067           val Ts = map typ_of_dtyp dts;
  1068           val names = DatatypeProp.make_tnames Ts;
  1069           val args = map Free (names ~~ Ts);
  1070           val c = Const (cname, Ts ---> T);
  1071           fun perm_arg (dt, x) =
  1072             let val T = type_of x
  1073             in if is_rec_type dt then
  1074                 let val (Us, _) = strip_type T
  1075                 in list_abs (map (pair "x") Us,
  1076                   Const (List.nth (perm_names_types, body_index dt)) $ pi $
  1077                     list_comb (x, map (fn (i, U) =>
  1078                       Const ("nominal.perm", permT --> U --> U) $
  1079                         (Const ("List.rev", permT --> permT) $ pi) $
  1080                         Bound i) ((length Us - 1 downto 0) ~~ Us)))
  1081                 end
  1082               else Const ("nominal.perm", permT --> T --> T) $ pi $ x
  1083             end;  
  1084         in
  1085           (("", HOLogic.mk_Trueprop (HOLogic.mk_eq
  1086             (Const (List.nth (perm_names_types, i)) $
  1087                Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
  1088                list_comb (c, args),
  1089              list_comb (c, map perm_arg (dts ~~ args))))), [])
  1090         end) constrs
  1091       end) descr);
  1092 
  1093     val (thy2, perm_simps) = thy1 |>
  1094       Theory.add_consts_i (map (fn (s, T) => (Sign.base_name s, T, NoSyn))
  1095         (List.drop (perm_names_types, length new_type_names))) |>
  1096       PrimrecPackage.add_primrec_i "" perm_eqs;
  1097 
  1098     (**** prove that permutation functions introduced by unfolding are ****)
  1099     (**** equivalent to already existing permutation functions         ****)
  1100 
  1101     val _ = warning ("length descr: " ^ string_of_int (length descr));
  1102     val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
  1103 
  1104     val perm_indnames = DatatypeProp.make_tnames (map body_type perm_types);
  1105     val perm_fun_def = PureThy.get_thm thy2 (Name "perm_fun_def");
  1106 
  1107     val unfolded_perm_eq_thms =
  1108       if length descr = length new_type_names then []
  1109       else map standard (List.drop (split_conj_thm
  1110         (Goal.prove thy2 [] []
  1111           (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1112             (map (fn (c as (s, T), x) =>
  1113                let val [T1, T2] = binder_types T
  1114                in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
  1115                  Const ("nominal.perm", T) $ pi $ Free (x, T2))
  1116                end)
  1117              (perm_names_types ~~ perm_indnames))))
  1118           (fn _ => EVERY [indtac induction perm_indnames 1,
  1119             ALLGOALS (asm_full_simp_tac
  1120               (simpset_of thy2 addsimps [perm_fun_def]))])),
  1121         length new_type_names));
  1122 
  1123     (**** prove [] \<bullet> t = t ****)
  1124 
  1125     val _ = warning "perm_empty_thms";
  1126 
  1127     val perm_empty_thms = List.concat (map (fn a =>
  1128       let val permT = mk_permT (Type (a, []))
  1129       in map standard (List.take (split_conj_thm
  1130         (Goal.prove thy2 [] []
  1131           (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1132             (map (fn ((s, T), x) => HOLogic.mk_eq
  1133                 (Const (s, permT --> T --> T) $
  1134                    Const ("List.list.Nil", permT) $ Free (x, T),
  1135                  Free (x, T)))
  1136              (perm_names ~~
  1137               map body_type perm_types ~~ perm_indnames))))
  1138           (fn _ => EVERY [indtac induction perm_indnames 1,
  1139             ALLGOALS (asm_full_simp_tac (simpset_of thy2))])),
  1140         length new_type_names))
  1141       end)
  1142       atoms);
  1143 
  1144     (**** prove (pi1 @ pi2) \<bullet> t = pi1 \<bullet> (pi2 \<bullet> t) ****)
  1145 
  1146     val _ = warning "perm_append_thms";
  1147 
  1148     (*FIXME: these should be looked up statically*)
  1149     val at_pt_inst = PureThy.get_thm thy2 (Name "at_pt_inst");
  1150     val pt2 = PureThy.get_thm thy2 (Name "pt2");
  1151 
  1152     val perm_append_thms = List.concat (map (fn a =>
  1153       let
  1154         val permT = mk_permT (Type (a, []));
  1155         val pi1 = Free ("pi1", permT);
  1156         val pi2 = Free ("pi2", permT);
  1157         val pt_inst = PureThy.get_thm thy2 (Name ("pt_" ^ Sign.base_name a ^ "_inst"));
  1158         val pt2' = pt_inst RS pt2;
  1159         val pt2_ax = PureThy.get_thm thy2
  1160           (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a));
  1161       in List.take (map standard (split_conj_thm
  1162         (Goal.prove thy2 [] []
  1163              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1164                 (map (fn ((s, T), x) =>
  1165                     let val perm = Const (s, permT --> T --> T)
  1166                     in HOLogic.mk_eq
  1167                       (perm $ (Const ("List.op @", permT --> permT --> permT) $
  1168                          pi1 $ pi2) $ Free (x, T),
  1169                        perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
  1170                     end)
  1171                   (perm_names ~~
  1172                    map body_type perm_types ~~ perm_indnames))))
  1173            (fn _ => EVERY [indtac induction perm_indnames 1,
  1174               ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
  1175          length new_type_names)
  1176       end) atoms);
  1177 
  1178     (**** prove pi1 ~ pi2 ==> pi1 \<bullet> t = pi2 \<bullet> t ****)
  1179 
  1180     val _ = warning "perm_eq_thms";
  1181 
  1182     val pt3 = PureThy.get_thm thy2 (Name "pt3");
  1183     val pt3_rev = PureThy.get_thm thy2 (Name "pt3_rev");
  1184 
  1185     val perm_eq_thms = List.concat (map (fn a =>
  1186       let
  1187         val permT = mk_permT (Type (a, []));
  1188         val pi1 = Free ("pi1", permT);
  1189         val pi2 = Free ("pi2", permT);
  1190         (*FIXME: not robust - better access these theorems using NominalData?*)
  1191         val at_inst = PureThy.get_thm thy2 (Name ("at_" ^ Sign.base_name a ^ "_inst"));
  1192         val pt_inst = PureThy.get_thm thy2 (Name ("pt_" ^ Sign.base_name a ^ "_inst"));
  1193         val pt3' = pt_inst RS pt3;
  1194         val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
  1195         val pt3_ax = PureThy.get_thm thy2
  1196           (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a));
  1197       in List.take (map standard (split_conj_thm
  1198         (Goal.prove thy2 [] [] (Logic.mk_implies
  1199              (HOLogic.mk_Trueprop (Const ("nominal.prm_eq",
  1200                 permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
  1201               HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1202                 (map (fn ((s, T), x) =>
  1203                     let val perm = Const (s, permT --> T --> T)
  1204                     in HOLogic.mk_eq
  1205                       (perm $ pi1 $ Free (x, T),
  1206                        perm $ pi2 $ Free (x, T))
  1207                     end)
  1208                   (perm_names ~~
  1209                    map body_type perm_types ~~ perm_indnames)))))
  1210            (fn _ => EVERY [indtac induction perm_indnames 1,
  1211               ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
  1212          length new_type_names)
  1213       end) atoms);
  1214 
  1215     (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
  1216 
  1217     val cp1 = PureThy.get_thm thy2 (Name "cp1");
  1218     val dj_cp = PureThy.get_thm thy2 (Name "dj_cp");
  1219     val pt_perm_compose = PureThy.get_thm thy2 (Name "pt_perm_compose");
  1220     val pt_perm_compose_rev = PureThy.get_thm thy2 (Name "pt_perm_compose_rev");
  1221     val dj_perm_perm_forget = PureThy.get_thm thy2 (Name "dj_perm_perm_forget");
  1222 
  1223     fun composition_instance name1 name2 thy =
  1224       let
  1225         val name1' = Sign.base_name name1;
  1226         val name2' = Sign.base_name name2;
  1227         val cp_class = Sign.intern_class thy ("cp_" ^ name1' ^ "_" ^ name2');
  1228         val permT1 = mk_permT (Type (name1, []));
  1229         val permT2 = mk_permT (Type (name2, []));
  1230         val augment = map_type_tfree
  1231           (fn (x, S) => TFree (x, cp_class :: S));
  1232         val Ts = map (augment o body_type) perm_types;
  1233         val cp_inst = PureThy.get_thm thy
  1234           (Name ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst"));
  1235         val simps = simpset_of thy addsimps (perm_fun_def ::
  1236           (if name1 <> name2 then
  1237              let val dj = PureThy.get_thm thy (Name ("dj_" ^ name2' ^ "_" ^ name1'))
  1238              in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
  1239            else
  1240              let
  1241                val at_inst = PureThy.get_thm thy (Name ("at_" ^ name1' ^ "_inst"));
  1242                val pt_inst = PureThy.get_thm thy (Name ("pt_" ^ name1' ^ "_inst"))
  1243              in
  1244                [cp_inst RS cp1 RS sym,
  1245                 at_inst RS (pt_inst RS pt_perm_compose) RS sym,
  1246                 at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
  1247             end))
  1248         val thms = split_conj_thm (standard (Goal.prove thy [] []
  1249             (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1250               (map (fn ((s, T), x) =>
  1251                   let
  1252                     val pi1 = Free ("pi1", permT1);
  1253                     val pi2 = Free ("pi2", permT2);
  1254                     val perm1 = Const (s, permT1 --> T --> T);
  1255                     val perm2 = Const (s, permT2 --> T --> T);
  1256                     val perm3 = Const ("nominal.perm", permT1 --> permT2 --> permT2)
  1257                   in HOLogic.mk_eq
  1258                     (perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
  1259                      perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
  1260                   end)
  1261                 (perm_names ~~ Ts ~~ perm_indnames))))
  1262           (fn _ => EVERY [indtac induction perm_indnames 1,
  1263              ALLGOALS (asm_full_simp_tac simps)])))
  1264       in
  1265         foldl (fn ((s, tvs), thy) => AxClass.add_inst_arity_i
  1266             (s, replicate (length tvs) (cp_class :: classes), [cp_class])
  1267             (AxClass.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
  1268           thy (full_new_type_names' ~~ tyvars)
  1269       end;
  1270 
  1271     val (thy3, perm_thmss) = thy2 |>
  1272       fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
  1273       curry (Library.foldr (fn ((i, (tyname, args, _)), thy) =>
  1274         AxClass.add_inst_arity_i (tyname, replicate (length args) classes, classes)
  1275         (AxClass.intro_classes_tac [] THEN REPEAT (EVERY
  1276            [resolve_tac perm_empty_thms 1,
  1277             resolve_tac perm_append_thms 1,
  1278             resolve_tac perm_eq_thms 1, assume_tac 1])) thy))
  1279         (List.take (descr, length new_type_names)) |>
  1280       PureThy.add_thmss
  1281         [((space_implode "_" new_type_names ^ "_unfolded_perm_eq",
  1282           unfolded_perm_eq_thms), [Simplifier.simp_add_global]),
  1283          ((space_implode "_" new_type_names ^ "_perm_empty",
  1284           perm_empty_thms), [Simplifier.simp_add_global]),
  1285          ((space_implode "_" new_type_names ^ "_perm_append",
  1286           perm_append_thms), [Simplifier.simp_add_global]),
  1287          ((space_implode "_" new_type_names ^ "_perm_eq",
  1288           perm_eq_thms), [Simplifier.simp_add_global])];
  1289   
  1290     (**** Define representing sets ****)
  1291 
  1292     val _ = warning "representing sets";
  1293 
  1294     val rep_set_names = map (Sign.full_name thy3) (DatatypeProp.indexify_names
  1295       (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr));
  1296     val big_rep_name =
  1297       space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
  1298         (fn (i, ("nominal.nOption", _, _)) => NONE
  1299           | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
  1300     val _ = warning ("big_rep_name: " ^ big_rep_name);
  1301 
  1302     fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
  1303           (case AList.lookup op = descr i of
  1304              SOME ("nominal.nOption", _, [(_, [dt']), _]) =>
  1305                apfst (cons dt) (strip_option dt')
  1306            | _ => ([], dtf))
  1307       | strip_option dt = ([], dt);
  1308 
  1309     fun make_intr s T (cname, cargs) =
  1310       let
  1311         fun mk_prem (dt, (j, j', prems, ts)) = 
  1312           let
  1313             val (dts, dt') = strip_option dt;
  1314             val (dts', dt'') = strip_dtyp dt';
  1315             val Ts = map typ_of_dtyp dts;
  1316             val Us = map typ_of_dtyp dts';
  1317             val T = typ_of_dtyp dt'';
  1318             val free = mk_Free "x" (Us ---> T) j;
  1319             val free' = app_bnds free (length Us);
  1320             fun mk_abs_fun (T, (i, t)) =
  1321               let val U = fastype_of t
  1322               in (i + 1, Const ("nominal.abs_fun", [T, U, T] --->
  1323                 Type ("nominal.nOption", [U])) $ mk_Free "y" T i $ t)
  1324               end
  1325           in (j + 1, j' + length Ts,
  1326             case dt'' of
  1327                 DtRec k => list_all (map (pair "x") Us,
  1328                   HOLogic.mk_Trueprop (HOLogic.mk_mem (free',
  1329                     Const (List.nth (rep_set_names, k),
  1330                       HOLogic.mk_setT T)))) :: prems
  1331               | _ => prems,
  1332             snd (foldr mk_abs_fun (j', free) Ts) :: ts)
  1333           end;
  1334 
  1335         val (_, _, prems, ts) = foldr mk_prem (1, 1, [], []) cargs;
  1336         val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
  1337           (list_comb (Const (cname, map fastype_of ts ---> T), ts),
  1338            Const (s, HOLogic.mk_setT T)))
  1339       in Logic.list_implies (prems, concl)
  1340       end;
  1341 
  1342     val (intr_ts, ind_consts) =
  1343       apfst List.concat (ListPair.unzip (List.mapPartial
  1344         (fn ((_, ("nominal.nOption", _, _)), _) => NONE
  1345           | ((i, (_, _, constrs)), rep_set_name) =>
  1346               let val T = nth_dtyp i
  1347               in SOME (map (make_intr rep_set_name T) constrs,
  1348                 Const (rep_set_name, HOLogic.mk_setT T))
  1349               end)
  1350                 (descr ~~ rep_set_names)));
  1351 
  1352     val (thy4, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
  1353       setmp InductivePackage.quiet_mode false
  1354         (InductivePackage.add_inductive_i false true big_rep_name false true false
  1355            ind_consts (map (fn x => (("", x), [])) intr_ts) []) thy3;
  1356 
  1357     (**** Prove that representing set is closed under permutation ****)
  1358 
  1359     val _ = warning "proving closure under permutation...";
  1360 
  1361     val perm_indnames' = List.mapPartial
  1362       (fn (x, (_, ("nominal.nOption", _, _))) => NONE | (x, _) => SOME x)
  1363       (perm_indnames ~~ descr);
  1364 
  1365     fun mk_perm_closed name = map (fn th => standard (th RS mp))
  1366       (List.take (split_conj_thm (Goal.prove thy4 [] []
  1367         (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
  1368            (fn (S, x) =>
  1369               let
  1370                 val S = map_term_types (map_type_tfree
  1371                   (fn (s, cs) => TFree (s, cs union cp_classes))) S;
  1372                 val T = HOLogic.dest_setT (fastype_of S);
  1373                 val permT = mk_permT (Type (name, []))
  1374               in HOLogic.mk_imp (HOLogic.mk_mem (Free (x, T), S),
  1375                 HOLogic.mk_mem (Const ("nominal.perm", permT --> T --> T) $
  1376                   Free ("pi", permT) $ Free (x, T), S))
  1377               end) (ind_consts ~~ perm_indnames'))))
  1378         (fn _ => EVERY (* CU: added perm_fun_def in the final tactic in order to deal with funs *)
  1379            [indtac rep_induct [] 1,
  1380             ALLGOALS (simp_tac (simpset_of thy4 addsimps
  1381               (symmetric perm_fun_def :: PureThy.get_thms thy4 (Name ("abs_perm"))))),
  1382             ALLGOALS (resolve_tac rep_intrs 
  1383                THEN_ALL_NEW (asm_full_simp_tac (simpset_of thy4 addsimps [perm_fun_def])))])),
  1384         length new_type_names));
  1385 
  1386     (* FIXME: theorems are stored in database for testing only *)
  1387     val perm_closed_thmss = map mk_perm_closed atoms;
  1388     val (thy5, _) = PureThy.add_thmss [(("perm_closed",
  1389       List.concat perm_closed_thmss), [])] thy4;
  1390 
  1391     (**** typedef ****)
  1392 
  1393     val _ = warning "defining type...";
  1394 
  1395     val (thy6, typedefs) =
  1396       foldl_map (fn (thy, ((((name, mx), tvs), c), name')) =>
  1397         setmp TypedefPackage.quiet_mode true
  1398           (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE
  1399             (rtac exI 1 THEN
  1400               QUIET_BREADTH_FIRST (has_fewer_prems 1)
  1401               (resolve_tac rep_intrs 1))) thy |> (fn (thy, r) =>
  1402         let
  1403           val permT = mk_permT (TFree (variant tvs "'a", HOLogic.typeS));
  1404           val pi = Free ("pi", permT);
  1405           val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs;
  1406           val T = Type (Sign.intern_type thy name, tvs');
  1407           val Const (_, Type (_, [U])) = c
  1408         in apsnd (pair r o hd)
  1409           (PureThy.add_defs_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
  1410             (Const ("nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
  1411              Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
  1412                (Const ("nominal.perm", permT --> U --> U) $ pi $
  1413                  (Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $
  1414                    Free ("x", T))))), [])] thy)
  1415         end))
  1416           (thy5, types_syntax ~~ tyvars ~~
  1417             (List.take (ind_consts, length new_type_names)) ~~ new_type_names);
  1418 
  1419     val perm_defs = map snd typedefs;
  1420     val Abs_inverse_thms = map (#Abs_inverse o fst) typedefs;
  1421     val Rep_inverse_thms = map (#Rep_inverse o fst) typedefs;
  1422     val Rep_thms = map (#Rep o fst) typedefs;
  1423 
  1424     val big_name = space_implode "_" new_type_names;
  1425 
  1426 
  1427     (** prove that new types are in class pt_<name> **)
  1428 
  1429     val _ = warning "prove that new types are in class pt_<name> ...";
  1430 
  1431     fun pt_instance ((class, atom), perm_closed_thms) =
  1432       fold (fn (((({Abs_inverse, Rep_inverse, Rep, ...},
  1433         perm_def), name), tvs), perm_closed) => fn thy =>
  1434           AxClass.add_inst_arity_i
  1435             (Sign.intern_type thy name,
  1436               replicate (length tvs) (classes @ cp_classes), [class])
  1437             (EVERY [AxClass.intro_classes_tac [],
  1438               rewrite_goals_tac [perm_def],
  1439               asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
  1440               asm_full_simp_tac (simpset_of thy addsimps
  1441                 [Rep RS perm_closed RS Abs_inverse]) 1,
  1442               asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
  1443                 (Name ("pt_" ^ Sign.base_name atom ^ "3"))]) 1]) thy)
  1444         (typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms);
  1445 
  1446 
  1447     (** prove that new types are in class cp_<name1>_<name2> **)
  1448 
  1449     val _ = warning "prove that new types are in class cp_<name1>_<name2> ...";
  1450 
  1451     fun cp_instance (atom1, perm_closed_thms1) (atom2, perm_closed_thms2) thy =
  1452       let
  1453         val name = "cp_" ^ Sign.base_name atom1 ^ "_" ^ Sign.base_name atom2;
  1454         val class = Sign.intern_class thy name;
  1455         val cp1' = PureThy.get_thm thy (Name (name ^ "_inst")) RS cp1
  1456       in fold (fn ((((({Abs_inverse, Rep_inverse, Rep, ...},
  1457         perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
  1458           AxClass.add_inst_arity_i
  1459             (Sign.intern_type thy name,
  1460               replicate (length tvs) (classes @ cp_classes), [class])
  1461             (EVERY [AxClass.intro_classes_tac [],
  1462               rewrite_goals_tac [perm_def],
  1463               asm_full_simp_tac (simpset_of thy addsimps
  1464                 ((Rep RS perm_closed1 RS Abs_inverse) ::
  1465                  (if atom1 = atom2 then []
  1466                   else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
  1467               cong_tac 1,
  1468               rtac refl 1,
  1469               rtac cp1' 1]) thy)
  1470         (typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms1 ~~
  1471           perm_closed_thms2) thy
  1472       end;
  1473 
  1474     val thy7 = fold (fn x => fn thy => thy |>
  1475       pt_instance x |>
  1476       fold (cp_instance (apfst snd x)) (atoms ~~ perm_closed_thmss))
  1477         (classes ~~ atoms ~~ perm_closed_thmss) thy6;
  1478 
  1479     (**** constructors ****)
  1480 
  1481     fun mk_abs_fun (x, t) =
  1482       let
  1483         val T = fastype_of x;
  1484         val U = fastype_of t
  1485       in
  1486         Const ("nominal.abs_fun", T --> U --> T -->
  1487           Type ("nominal.nOption", [U])) $ x $ t
  1488       end;
  1489 
  1490     val (ty_idxs, _) = foldl
  1491       (fn ((i, ("nominal.nOption", _, _)), p) => p
  1492         | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
  1493 
  1494     fun reindex (DtType (s, dts)) = DtType (s, map reindex dts)
  1495       | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i))
  1496       | reindex dt = dt;
  1497 
  1498     fun strip_suffix i s = implode (List.take (explode s, size s - i));
  1499 
  1500     (** strips the "_Rep" in type names *)
  1501     fun strip_nth_name i s =
  1502       let val xs = NameSpace.unpack s
  1503       in NameSpace.pack (map_nth_elem (length xs - i) (strip_suffix 4) xs) end;
  1504 
  1505     val descr'' = List.mapPartial
  1506       (fn (i, ("nominal.nOption", _, _)) => NONE
  1507         | (i, (s, dts, constrs)) => SOME (the (AList.lookup op = ty_idxs i),
  1508             (strip_nth_name 1 s,  map reindex dts,
  1509              map (fn (cname, cargs) =>
  1510                (strip_nth_name 2 cname,
  1511                 foldl (fn (dt, dts) =>
  1512                   let val (dts', dt') = strip_option dt
  1513                   in (dts @ dts' @ [reindex dt']) end) [] cargs)) constrs))) descr;
  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 descr;
  1897 
  1898     val (thy9, _) = thy8 |>
  1899       Theory.add_path big_name |>
  1900       PureThy.add_thms [(("induct", 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