src/HOL/Nominal/nominal_package.ML
author berghofe
Mon Oct 17 17:42:24 2005 +0200 (2005-10-17)
changeset 17872 f08fc98a164a
parent 17870 c35381811d5c
child 17873 09236f6a6a19
permissions -rw-r--r--
Implemented proofs for support and freshness theorems.
     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, prove_goalw_cterm [] (cterm_of (sign_of 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, prove_goalw_cterm [] (cterm_of (sign_of 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, prove_goalw_cterm [] (cterm_of (sign_of 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 _ => [auto_tac (claset(),simp_s), rtac cp1 1];
   341 	   in
   342 	     thy' |> PureThy.add_thms 
   343                     [((name, prove_goalw_cterm [] (cterm_of (sign_of 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, prove_goalw_cterm [] (cterm_of (sign_of 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 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
   924 
   925 fun read_typ sign ((Ts, sorts), str) =
   926   let
   927     val T = Type.no_tvars (Sign.read_typ (sign, (AList.lookup op =)
   928       (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
   929   in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
   930 
   931 (** taken from HOL/Tools/datatype_aux.ML **)
   932 
   933 fun indtac indrule indnames i st =
   934   let
   935     val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
   936     val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop
   937       (Logic.strip_imp_concl (List.nth (prems_of st, i - 1))));
   938     val getP = if can HOLogic.dest_imp (hd ts) then
   939       (apfst SOME) o HOLogic.dest_imp else pair NONE;
   940     fun abstr (t1, t2) = (case t1 of
   941         NONE => (case filter (fn Free (s, _) => s mem indnames | _ => false)
   942               (term_frees t2) of
   943             [Free (s, T)] => absfree (s, T, t2)
   944           | _ => sys_error "indtac")
   945       | SOME (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2)))
   946     val cert = cterm_of (Thm.sign_of_thm st);
   947     val Ps = map (cert o head_of o snd o getP) ts;
   948     val indrule' = cterm_instantiate (Ps ~~
   949       (map (cert o abstr o getP) ts')) indrule
   950   in
   951     rtac indrule' i st
   952   end;
   953 
   954 fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
   955   let
   956     (* this theory is used just for parsing *)
   957   
   958     val tmp_thy = thy |>
   959       Theory.copy |>
   960       Theory.add_types (map (fn (tvs, tname, mx, _) =>
   961         (tname, length tvs, mx)) dts);
   962 
   963     val sign = Theory.sign_of tmp_thy;
   964 
   965     val atoms = atoms_of thy;
   966     val classes = map (NameSpace.map_base (fn s => "pt_" ^ s)) atoms;
   967     val cp_classes = List.concat (map (fn atom1 => map (fn atom2 =>
   968       Sign.intern_class thy ("cp_" ^ Sign.base_name atom1 ^ "_" ^
   969         Sign.base_name atom2)) atoms) atoms);
   970     fun augment_sort S = S union classes;
   971     val augment_sort_typ = map_type_tfree (fn (s, S) => TFree (s, augment_sort S));
   972 
   973     fun prep_constr ((constrs, sorts), (cname, cargs, mx)) =
   974       let val (cargs', sorts') = Library.foldl (prep_typ sign) (([], sorts), cargs)
   975       in (constrs @ [(cname, cargs', mx)], sorts') end
   976 
   977     fun prep_dt_spec ((dts, sorts), (tvs, tname, mx, constrs)) =
   978       let val (constrs', sorts') = Library.foldl prep_constr (([], sorts), constrs)
   979       in (dts @ [(tvs, tname, mx, constrs')], sorts') end
   980 
   981     val (dts', sorts) = Library.foldl prep_dt_spec (([], []), dts);
   982     val sorts' = map (apsnd augment_sort) sorts;
   983     val tyvars = map #1 dts';
   984 
   985     val types_syntax = map (fn (tvs, tname, mx, constrs) => (tname, mx)) dts';
   986     val constr_syntax = map (fn (tvs, tname, mx, constrs) =>
   987       map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts';
   988 
   989     val ps = map (fn (_, n, _, _) =>
   990       (Sign.full_name sign n, Sign.full_name sign (n ^ "_Rep"))) dts;
   991     val rps = map Library.swap ps;
   992 
   993     fun replace_types (Type ("nominal.ABS", [T, U])) = 
   994           Type ("fun", [T, Type ("nominal.nOption", [replace_types U])])
   995       | replace_types (Type (s, Ts)) =
   996           Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
   997       | replace_types T = T;
   998 
   999     fun replace_types' (Type (s, Ts)) =
  1000           Type (getOpt (AList.lookup op = rps s, s), map replace_types' Ts)
  1001       | replace_types' T = T;
  1002 
  1003     val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, tname ^ "_Rep", NoSyn,
  1004       map (fn (cname, cargs, mx) => (cname,
  1005         map (augment_sort_typ o replace_types) cargs, NoSyn)) constrs)) dts';
  1006 
  1007     val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
  1008     val full_new_type_names' = map (Sign.full_name (sign_of thy)) new_type_names';
  1009 
  1010     val (thy1, {induction, ...}) =
  1011       DatatypePackage.add_datatype_i err flat_names new_type_names' dts'' thy;
  1012 
  1013     val SOME {descr, ...} = Symtab.lookup
  1014       (DatatypePackage.get_datatypes thy1) (hd full_new_type_names');
  1015     val typ_of_dtyp = typ_of_dtyp descr sorts';
  1016     fun nth_dtyp i = typ_of_dtyp (DtRec i);
  1017 
  1018     (**** define permutation functions ****)
  1019 
  1020     val permT = mk_permT (TFree ("'x", HOLogic.typeS));
  1021     val pi = Free ("pi", permT);
  1022     val perm_types = map (fn (i, _) =>
  1023       let val T = nth_dtyp i
  1024       in permT --> T --> T end) descr;
  1025     val perm_names = replicate (length new_type_names) "nominal.perm" @
  1026       DatatypeProp.indexify_names (map (fn i => Sign.full_name (sign_of thy1)
  1027         ("perm_" ^ name_of_typ (nth_dtyp i)))
  1028           (length new_type_names upto length descr - 1));
  1029     val perm_names_types = perm_names ~~ perm_types;
  1030 
  1031     val perm_eqs = List.concat (map (fn (i, (_, _, constrs)) =>
  1032       let val T = nth_dtyp i
  1033       in map (fn (cname, dts) => 
  1034         let
  1035           val Ts = map typ_of_dtyp dts;
  1036           val names = DatatypeProp.make_tnames Ts;
  1037           val args = map Free (names ~~ Ts);
  1038           val c = Const (cname, Ts ---> T);
  1039           fun perm_arg (dt, x) =
  1040             let val T = type_of x
  1041             in if is_rec_type dt then
  1042                 let val (Us, _) = strip_type T
  1043                 in list_abs (map (pair "x") Us,
  1044                   Const (List.nth (perm_names_types, body_index dt)) $ pi $
  1045                     list_comb (x, map (fn (i, U) =>
  1046                       Const ("nominal.perm", permT --> U --> U) $
  1047                         (Const ("List.rev", permT --> permT) $ pi) $
  1048                         Bound i) ((length Us - 1 downto 0) ~~ Us)))
  1049                 end
  1050               else Const ("nominal.perm", permT --> T --> T) $ pi $ x
  1051             end;  
  1052         in
  1053           (("", HOLogic.mk_Trueprop (HOLogic.mk_eq
  1054             (Const (List.nth (perm_names_types, i)) $
  1055                Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
  1056                list_comb (c, args),
  1057              list_comb (c, map perm_arg (dts ~~ args))))), [])
  1058         end) constrs
  1059       end) descr);
  1060 
  1061     val (thy2, perm_simps) = thy1 |>
  1062       Theory.add_consts_i (map (fn (s, T) => (Sign.base_name s, T, NoSyn))
  1063         (List.drop (perm_names_types, length new_type_names))) |>
  1064       PrimrecPackage.add_primrec_i "" perm_eqs;
  1065 
  1066     (**** prove that permutation functions introduced by unfolding are ****)
  1067     (**** equivalent to already existing permutation functions         ****)
  1068 
  1069     val _ = warning ("length descr: " ^ string_of_int (length descr));
  1070     val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
  1071 
  1072     val perm_indnames = DatatypeProp.make_tnames (map body_type perm_types);
  1073     val perm_fun_def = PureThy.get_thm thy2 (Name "perm_fun_def");
  1074 
  1075     val unfolded_perm_eq_thms =
  1076       if length descr = length new_type_names then []
  1077       else map standard (List.drop (split_conj_thm
  1078         (prove_goalw_cterm [] (cterm_of thy2 
  1079           (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1080             (map (fn (c as (s, T), x) =>
  1081                let val [T1, T2] = binder_types T
  1082                in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
  1083                  Const ("nominal.perm", T) $ pi $ Free (x, T2))
  1084                end)
  1085              (perm_names_types ~~ perm_indnames)))))
  1086           (fn _ => [indtac induction perm_indnames 1,
  1087             ALLGOALS (asm_full_simp_tac
  1088               (simpset_of thy2 addsimps [perm_fun_def]))])),
  1089         length new_type_names));
  1090 
  1091     (**** prove [] \<bullet> t = t ****)
  1092 
  1093     val _ = warning "perm_empty_thms";
  1094 
  1095     val perm_empty_thms = List.concat (map (fn a =>
  1096       let val permT = mk_permT (Type (a, []))
  1097       in map standard (List.take (split_conj_thm
  1098         (prove_goalw_cterm [] (cterm_of thy2
  1099           (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1100             (map (fn ((s, T), x) => HOLogic.mk_eq
  1101                 (Const (s, permT --> T --> T) $
  1102                    Const ("List.list.Nil", permT) $ Free (x, T),
  1103                  Free (x, T)))
  1104              (perm_names ~~
  1105               map body_type perm_types ~~ perm_indnames)))))
  1106           (fn _ => [indtac induction perm_indnames 1,
  1107             ALLGOALS (asm_full_simp_tac (simpset_of thy2))])),
  1108         length new_type_names))
  1109       end)
  1110       atoms);
  1111 
  1112     (**** prove (pi1 @ pi2) \<bullet> t = pi1 \<bullet> (pi2 \<bullet> t) ****)
  1113 
  1114     val _ = warning "perm_append_thms";
  1115 
  1116     (*FIXME: these should be looked up statically*)
  1117     val at_pt_inst = PureThy.get_thm thy2 (Name "at_pt_inst");
  1118     val pt2 = PureThy.get_thm thy2 (Name "pt2");
  1119 
  1120     val perm_append_thms = List.concat (map (fn a =>
  1121       let
  1122         val permT = mk_permT (Type (a, []));
  1123         val pi1 = Free ("pi1", permT);
  1124         val pi2 = Free ("pi2", permT);
  1125         val pt_inst = PureThy.get_thm thy2 (Name ("pt_" ^ Sign.base_name a ^ "_inst"));
  1126         val pt2' = pt_inst RS pt2;
  1127         val pt2_ax = PureThy.get_thm thy2
  1128           (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a));
  1129       in List.take (map standard (split_conj_thm
  1130         (prove_goalw_cterm [] (cterm_of thy2
  1131              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1132                 (map (fn ((s, T), x) =>
  1133                     let val perm = Const (s, permT --> T --> T)
  1134                     in HOLogic.mk_eq
  1135                       (perm $ (Const ("List.op @", permT --> permT --> permT) $
  1136                          pi1 $ pi2) $ Free (x, T),
  1137                        perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
  1138                     end)
  1139                   (perm_names ~~
  1140                    map body_type perm_types ~~ perm_indnames)))))
  1141            (fn _ => [indtac induction perm_indnames 1,
  1142               ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
  1143          length new_type_names)
  1144       end) atoms);
  1145 
  1146     (**** prove pi1 ~ pi2 ==> pi1 \<bullet> t = pi2 \<bullet> t ****)
  1147 
  1148     val _ = warning "perm_eq_thms";
  1149 
  1150     val pt3 = PureThy.get_thm thy2 (Name "pt3");
  1151     val pt3_rev = PureThy.get_thm thy2 (Name "pt3_rev");
  1152 
  1153     val perm_eq_thms = List.concat (map (fn a =>
  1154       let
  1155         val permT = mk_permT (Type (a, []));
  1156         val pi1 = Free ("pi1", permT);
  1157         val pi2 = Free ("pi2", permT);
  1158         (*FIXME: not robust - better access these theorems using NominalData?*)
  1159         val at_inst = PureThy.get_thm thy2 (Name ("at_" ^ Sign.base_name a ^ "_inst"));
  1160         val pt_inst = PureThy.get_thm thy2 (Name ("pt_" ^ Sign.base_name a ^ "_inst"));
  1161         val pt3' = pt_inst RS pt3;
  1162         val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
  1163         val pt3_ax = PureThy.get_thm thy2
  1164           (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a));
  1165       in List.take (map standard (split_conj_thm
  1166         (prove_goalw_cterm [] (cterm_of thy2 (Logic.mk_implies
  1167              (HOLogic.mk_Trueprop (Const ("nominal.prm_eq",
  1168                 permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
  1169               HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1170                 (map (fn ((s, T), x) =>
  1171                     let val perm = Const (s, permT --> T --> T)
  1172                     in HOLogic.mk_eq
  1173                       (perm $ pi1 $ Free (x, T),
  1174                        perm $ pi2 $ Free (x, T))
  1175                     end)
  1176                   (perm_names ~~
  1177                    map body_type perm_types ~~ perm_indnames))))))
  1178            (fn hyps => [cut_facts_tac hyps 1, indtac induction perm_indnames 1,
  1179               ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
  1180          length new_type_names)
  1181       end) atoms);
  1182 
  1183     (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
  1184 
  1185     val cp1 = PureThy.get_thm thy2 (Name "cp1");
  1186     val dj_cp = PureThy.get_thm thy2 (Name "dj_cp");
  1187     val pt_perm_compose = PureThy.get_thm thy2 (Name "pt_perm_compose");
  1188     val pt_perm_compose_rev = PureThy.get_thm thy2 (Name "pt_perm_compose_rev");
  1189     val dj_perm_perm_forget = PureThy.get_thm thy2 (Name "dj_perm_perm_forget");
  1190 
  1191     fun composition_instance name1 name2 thy =
  1192       let
  1193         val name1' = Sign.base_name name1;
  1194         val name2' = Sign.base_name name2;
  1195         val cp_class = Sign.intern_class thy ("cp_" ^ name1' ^ "_" ^ name2');
  1196         val permT1 = mk_permT (Type (name1, []));
  1197         val permT2 = mk_permT (Type (name2, []));
  1198         val augment = map_type_tfree
  1199           (fn (x, S) => TFree (x, cp_class :: S));
  1200         val Ts = map (augment o body_type) perm_types;
  1201         val cp_inst = PureThy.get_thm thy
  1202           (Name ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst"));
  1203         val simps = simpset_of thy addsimps (perm_fun_def ::
  1204           (if name1 <> name2 then
  1205              let val dj = PureThy.get_thm thy (Name ("dj_" ^ name2' ^ "_" ^ name1'))
  1206              in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
  1207            else
  1208              let
  1209                val at_inst = PureThy.get_thm thy (Name ("at_" ^ name1' ^ "_inst"));
  1210                val pt_inst = PureThy.get_thm thy (Name ("pt_" ^ name1' ^ "_inst"))
  1211              in
  1212                [cp_inst RS cp1 RS sym,
  1213                 at_inst RS (pt_inst RS pt_perm_compose) RS sym,
  1214                 at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
  1215             end))
  1216         val thms = split_conj_thm (prove_goalw_cterm [] (cterm_of thy
  1217             (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1218               (map (fn ((s, T), x) =>
  1219                   let
  1220                     val pi1 = Free ("pi1", permT1);
  1221                     val pi2 = Free ("pi2", permT2);
  1222                     val perm1 = Const (s, permT1 --> T --> T);
  1223                     val perm2 = Const (s, permT2 --> T --> T);
  1224                     val perm3 = Const ("nominal.perm", permT1 --> permT2 --> permT2)
  1225                   in HOLogic.mk_eq
  1226                     (perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
  1227                      perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
  1228                   end)
  1229                 (perm_names ~~ Ts ~~ perm_indnames)))))
  1230           (fn _ => [indtac induction perm_indnames 1,
  1231              ALLGOALS (asm_full_simp_tac simps)]))
  1232       in
  1233         foldl (fn ((s, tvs), thy) => AxClass.add_inst_arity_i
  1234             (s, replicate (length tvs) (cp_class :: classes), [cp_class])
  1235             (AxClass.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
  1236           thy (full_new_type_names' ~~ tyvars)
  1237       end;
  1238 
  1239     val (thy3, perm_thmss) = thy2 |>
  1240       fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
  1241       curry (Library.foldr (fn ((i, (tyname, args, _)), thy) =>
  1242         AxClass.add_inst_arity_i (tyname, replicate (length args) classes, classes)
  1243         (AxClass.intro_classes_tac [] THEN REPEAT (EVERY
  1244            [resolve_tac perm_empty_thms 1,
  1245             resolve_tac perm_append_thms 1,
  1246             resolve_tac perm_eq_thms 1, assume_tac 1])) thy))
  1247         (List.take (descr, length new_type_names)) |>
  1248       PureThy.add_thmss
  1249         [((space_implode "_" new_type_names ^ "_unfolded_perm_eq",
  1250           unfolded_perm_eq_thms), [Simplifier.simp_add_global]),
  1251          ((space_implode "_" new_type_names ^ "_perm_empty",
  1252           perm_empty_thms), [Simplifier.simp_add_global]),
  1253          ((space_implode "_" new_type_names ^ "_perm_append",
  1254           perm_append_thms), [Simplifier.simp_add_global]),
  1255          ((space_implode "_" new_type_names ^ "_perm_eq",
  1256           perm_eq_thms), [Simplifier.simp_add_global])];
  1257   
  1258     (**** Define representing sets ****)
  1259 
  1260     val _ = warning "representing sets";
  1261 
  1262     val rep_set_names = map (Sign.full_name thy3) (DatatypeProp.indexify_names
  1263       (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr));
  1264     val big_rep_name =
  1265       space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
  1266         (fn (i, ("nominal.nOption", _, _)) => NONE
  1267           | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
  1268     val _ = warning ("big_rep_name: " ^ big_rep_name);
  1269 
  1270     fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
  1271           (case AList.lookup op = descr i of
  1272              SOME ("nominal.nOption", _, [(_, [dt']), _]) =>
  1273                apfst (cons dt) (strip_option dt')
  1274            | _ => ([], dtf))
  1275       | strip_option dt = ([], dt);
  1276 
  1277     fun make_intr s T (cname, cargs) =
  1278       let
  1279         fun mk_prem (dt, (j, j', prems, ts)) = 
  1280           let
  1281             val (dts, dt') = strip_option dt;
  1282             val (dts', dt'') = strip_dtyp dt';
  1283             val Ts = map typ_of_dtyp dts;
  1284             val Us = map typ_of_dtyp dts';
  1285             val T = typ_of_dtyp dt'';
  1286             val free = mk_Free "x" (Us ---> T) j;
  1287             val free' = app_bnds free (length Us);
  1288             fun mk_abs_fun (T, (i, t)) =
  1289               let val U = fastype_of t
  1290               in (i + 1, Const ("nominal.abs_fun", [T, U, T] --->
  1291                 Type ("nominal.nOption", [U])) $ mk_Free "y" T i $ t)
  1292               end
  1293           in (j + 1, j' + length Ts,
  1294             case dt'' of
  1295                 DtRec k => list_all (map (pair "x") Us,
  1296                   HOLogic.mk_Trueprop (HOLogic.mk_mem (free',
  1297                     Const (List.nth (rep_set_names, k),
  1298                       HOLogic.mk_setT T)))) :: prems
  1299               | _ => prems,
  1300             snd (foldr mk_abs_fun (j', free) Ts) :: ts)
  1301           end;
  1302 
  1303         val (_, _, prems, ts) = foldr mk_prem (1, 1, [], []) cargs;
  1304         val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
  1305           (list_comb (Const (cname, map fastype_of ts ---> T), ts),
  1306            Const (s, HOLogic.mk_setT T)))
  1307       in Logic.list_implies (prems, concl)
  1308       end;
  1309 
  1310     val (intr_ts, ind_consts) =
  1311       apfst List.concat (ListPair.unzip (List.mapPartial
  1312         (fn ((_, ("nominal.nOption", _, _)), _) => NONE
  1313           | ((i, (_, _, constrs)), rep_set_name) =>
  1314               let val T = nth_dtyp i
  1315               in SOME (map (make_intr rep_set_name T) constrs,
  1316                 Const (rep_set_name, HOLogic.mk_setT T))
  1317               end)
  1318                 (descr ~~ rep_set_names)));
  1319 
  1320     val (thy4, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
  1321       setmp InductivePackage.quiet_mode false
  1322         (InductivePackage.add_inductive_i false true big_rep_name false true false
  1323            ind_consts (map (fn x => (("", x), [])) intr_ts) []) thy3;
  1324 
  1325     (**** Prove that representing set is closed under permutation ****)
  1326 
  1327     val _ = warning "proving closure under permutation...";
  1328 
  1329     val perm_indnames' = List.mapPartial
  1330       (fn (x, (_, ("nominal.nOption", _, _))) => NONE | (x, _) => SOME x)
  1331       (perm_indnames ~~ descr);
  1332 
  1333     fun mk_perm_closed name = map (fn th => standard (th RS mp))
  1334       (List.take (split_conj_thm (prove_goalw_cterm [] (cterm_of thy4 
  1335         (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
  1336            (fn (S, x) =>
  1337               let
  1338                 val S = map_term_types (map_type_tfree
  1339                   (fn (s, cs) => TFree (s, cs union cp_classes))) S;
  1340                 val T = HOLogic.dest_setT (fastype_of S);
  1341                 val permT = mk_permT (Type (name, []))
  1342               in HOLogic.mk_imp (HOLogic.mk_mem (Free (x, T), S),
  1343                 HOLogic.mk_mem (Const ("nominal.perm", permT --> T --> T) $
  1344                   Free ("pi", permT) $ Free (x, T), S))
  1345               end) (ind_consts ~~ perm_indnames')))))
  1346         (fn _ =>  (* CU: added perm_fun_def in the final tactic in order to deal with funs *)
  1347            [indtac rep_induct [] 1,
  1348             ALLGOALS (simp_tac (simpset_of thy4 addsimps
  1349               (symmetric perm_fun_def :: PureThy.get_thms thy4 (Name ("abs_perm"))))),
  1350             ALLGOALS (resolve_tac rep_intrs 
  1351                THEN_ALL_NEW (asm_full_simp_tac (simpset_of thy4 addsimps [perm_fun_def])))])),
  1352         length new_type_names));
  1353 
  1354     (* FIXME: theorems are stored in database for testing only *)
  1355     val perm_closed_thmss = map mk_perm_closed atoms;
  1356     val (thy5, _) = PureThy.add_thmss [(("perm_closed",
  1357       List.concat perm_closed_thmss), [])] thy4;
  1358 
  1359     (**** typedef ****)
  1360 
  1361     val _ = warning "defining type...";
  1362 
  1363     val (thy6, typedefs) =
  1364       foldl_map (fn (thy, ((((name, mx), tvs), c), name')) =>
  1365         setmp TypedefPackage.quiet_mode true
  1366           (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE
  1367             (rtac exI 1 THEN
  1368               QUIET_BREADTH_FIRST (has_fewer_prems 1)
  1369               (resolve_tac rep_intrs 1))) thy |> (fn (thy, r) =>
  1370         let
  1371           val permT = mk_permT (TFree (variant tvs "'a", HOLogic.typeS));
  1372           val pi = Free ("pi", permT);
  1373           val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs;
  1374           val T = Type (Sign.intern_type thy name, tvs');
  1375           val Const (_, Type (_, [U])) = c
  1376         in apsnd (pair r o hd)
  1377           (PureThy.add_defs_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
  1378             (Const ("nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
  1379              Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
  1380                (Const ("nominal.perm", permT --> U --> U) $ pi $
  1381                  (Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $
  1382                    Free ("x", T))))), [])] thy)
  1383         end))
  1384           (thy5, types_syntax ~~ tyvars ~~
  1385             (List.take (ind_consts, length new_type_names)) ~~ new_type_names);
  1386 
  1387     val perm_defs = map snd typedefs;
  1388     val Abs_inverse_thms = map (#Abs_inverse o fst) typedefs;
  1389     val Rep_thms = map (#Rep o fst) typedefs;
  1390 
  1391     (** prove that new types are in class pt_<name> **)
  1392 
  1393     val _ = warning "prove that new types are in class pt_<name> ...";
  1394 
  1395     fun pt_instance ((class, atom), perm_closed_thms) =
  1396       fold (fn (((({Abs_inverse, Rep_inverse, Rep, ...},
  1397         perm_def), name), tvs), perm_closed) => fn thy =>
  1398           AxClass.add_inst_arity_i
  1399             (Sign.intern_type thy name,
  1400               replicate (length tvs) (classes @ cp_classes), [class])
  1401             (EVERY [AxClass.intro_classes_tac [],
  1402               rewrite_goals_tac [perm_def],
  1403               asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
  1404               asm_full_simp_tac (simpset_of thy addsimps
  1405                 [Rep RS perm_closed RS Abs_inverse]) 1,
  1406               asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
  1407                 (Name ("pt_" ^ Sign.base_name atom ^ "3"))]) 1]) thy)
  1408         (typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms);
  1409 
  1410 
  1411     (** prove that new types are in class cp_<name1>_<name2> **)
  1412 
  1413     val _ = warning "prove that new types are in class cp_<name1>_<name2> ...";
  1414 
  1415     fun cp_instance (atom1, perm_closed_thms1) (atom2, perm_closed_thms2) thy =
  1416       let
  1417         val name = "cp_" ^ Sign.base_name atom1 ^ "_" ^ Sign.base_name atom2;
  1418         val class = Sign.intern_class thy name;
  1419         val cp1' = PureThy.get_thm thy (Name (name ^ "_inst")) RS cp1
  1420       in fold (fn ((((({Abs_inverse, Rep_inverse, Rep, ...},
  1421         perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
  1422           AxClass.add_inst_arity_i
  1423             (Sign.intern_type thy name,
  1424               replicate (length tvs) (classes @ cp_classes), [class])
  1425             (EVERY [AxClass.intro_classes_tac [],
  1426               rewrite_goals_tac [perm_def],
  1427               asm_full_simp_tac (simpset_of thy addsimps
  1428                 ((Rep RS perm_closed1 RS Abs_inverse) ::
  1429                  (if atom1 = atom2 then []
  1430                   else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
  1431               DatatypeAux.cong_tac 1,
  1432               rtac refl 1,
  1433               rtac cp1' 1]) thy)
  1434         (typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms1 ~~
  1435           perm_closed_thms2) thy
  1436       end;
  1437 
  1438     val thy7 = fold (fn x => fn thy => thy |>
  1439       pt_instance x |>
  1440       fold (cp_instance (apfst snd x)) (atoms ~~ perm_closed_thmss))
  1441         (classes ~~ atoms ~~ perm_closed_thmss) thy6;
  1442 
  1443     (**** constructors ****)
  1444 
  1445     fun mk_abs_fun (x, t) =
  1446       let
  1447         val T = fastype_of x;
  1448         val U = fastype_of t
  1449       in
  1450         Const ("nominal.abs_fun", T --> U --> T -->
  1451           Type ("nominal.nOption", [U])) $ x $ t
  1452       end;
  1453 
  1454     val typ_of_dtyp' = replace_types' o typ_of_dtyp;
  1455 
  1456     val rep_names = map (fn s =>
  1457       Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
  1458     val abs_names = map (fn s =>
  1459       Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
  1460 
  1461     val recTs = get_rec_types descr sorts;
  1462     val newTs' = Library.take (length new_type_names, recTs);
  1463     val newTs = map replace_types' newTs';
  1464 
  1465     val full_new_type_names = map (Sign.full_name (sign_of thy)) new_type_names;
  1466 
  1467     fun make_constr_def tname T T' ((thy, defs, eqns), ((cname, cargs), (cname', mx))) =
  1468       let
  1469         fun constr_arg (dt, (j, l_args, r_args)) =
  1470           let
  1471             val x' = mk_Free "x" (typ_of_dtyp' dt) j;
  1472             val (dts, dt') = strip_option dt;
  1473             val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp' dt) i)
  1474               (dts ~~ (j upto j + length dts - 1))
  1475             val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts)
  1476             val (dts', dt'') = strip_dtyp dt'
  1477           in case dt'' of
  1478               DtRec k => if k < length new_type_names then
  1479                   (j + length dts + 1,
  1480                    xs @ x :: l_args,
  1481                    foldr mk_abs_fun
  1482                      (list_abs (map (pair "z" o typ_of_dtyp') dts',
  1483                        Const (List.nth (rep_names, k), typ_of_dtyp' dt'' -->
  1484                          typ_of_dtyp dt'') $ app_bnds x (length dts')))
  1485                      xs :: r_args)
  1486                 else error "nested recursion not (yet) supported"
  1487             | _ => (j + 1, x' :: l_args, x' :: r_args)
  1488           end
  1489 
  1490         val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs;
  1491         val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname);
  1492         val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname);
  1493         val constrT = map fastype_of l_args ---> T;
  1494         val lhs = list_comb (Const (Sign.full_name thy (Sign.base_name cname),
  1495           constrT), l_args);
  1496         val rhs = list_comb (Const (cname, map fastype_of r_args ---> T'), r_args);
  1497         val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs);
  1498         val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
  1499           (Const (rep_name, T --> T') $ lhs, rhs));
  1500         val def_name = (Sign.base_name cname) ^ "_def";
  1501         val (thy', [def_thm]) = thy |>
  1502           Theory.add_consts_i [(cname', constrT, mx)] |>
  1503           (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]
  1504       in (thy', defs @ [def_thm], eqns @ [eqn]) end;
  1505 
  1506     fun dt_constr_defs ((thy, defs, eqns, dist_lemmas),
  1507         (((((_, (_, _, constrs)), tname), T), T'), constr_syntax)) =
  1508       let
  1509         val rep_const = cterm_of thy
  1510           (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
  1511         val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
  1512         val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
  1513           ((Theory.add_path tname thy, defs, []), constrs ~~ constr_syntax)
  1514       in
  1515         (parent_path flat_names thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
  1516       end;
  1517 
  1518     val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs
  1519       ((thy7, [], [], []), List.take (descr, length new_type_names) ~~
  1520         new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax);
  1521 
  1522     val abs_inject_thms = map (fn tname =>
  1523       PureThy.get_thm thy8 (Name ("Abs_" ^ tname ^ "_inject"))) new_type_names;
  1524 
  1525     val rep_inject_thms = map (fn tname =>
  1526       PureThy.get_thm thy8 (Name ("Rep_" ^ tname ^ "_inject"))) new_type_names;
  1527 
  1528     val rep_thms = map (fn tname =>
  1529       PureThy.get_thm thy8 (Name ("Rep_" ^ tname))) new_type_names;
  1530 
  1531     val rep_inverse_thms = map (fn tname =>
  1532       PureThy.get_thm thy8 (Name ("Rep_" ^ tname ^ "_inverse"))) new_type_names;
  1533 
  1534     (* prove theorem  Rep_i (Constr_j ...) = Constr'_j ...  *)
  1535     
  1536     fun prove_constr_rep_thm eqn =
  1537       let
  1538         val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
  1539         val rewrites = constr_defs @ map mk_meta_eq rep_inverse_thms
  1540       in prove_goalw_cterm [] (cterm_of thy8 eqn) (fn _ =>
  1541         [resolve_tac inj_thms 1,
  1542          rewrite_goals_tac rewrites,
  1543          rtac refl 3,
  1544          resolve_tac rep_intrs 2,
  1545          REPEAT (resolve_tac rep_thms 1)])
  1546       end;
  1547 
  1548     val constr_rep_thmss = map (map prove_constr_rep_thm) constr_rep_eqns;
  1549 
  1550     (* prove theorem  pi \<bullet> Rep_i x = Rep_i (pi \<bullet> x) *)
  1551 
  1552     fun prove_perm_rep_perm (atom, perm_closed_thms) = map (fn th =>
  1553       let
  1554         val _ $ (_ $ (Rep $ x) $ _) = Logic.unvarify (prop_of th);
  1555         val Type ("fun", [T, U]) = fastype_of Rep;
  1556         val permT = mk_permT (Type (atom, []));
  1557         val pi = Free ("pi", permT);
  1558       in
  1559         prove_goalw_cterm [] (cterm_of thy8 (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1560             (Const ("nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
  1561              Rep $ (Const ("nominal.perm", permT --> T --> T) $ pi $ x)))))
  1562           (fn _ => [simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @
  1563             perm_closed_thms @ Rep_thms)) 1])
  1564       end) Rep_thms;
  1565 
  1566     val perm_rep_perm_thms = List.concat (map prove_perm_rep_perm
  1567       (atoms ~~ perm_closed_thmss));
  1568 
  1569     (* prove distinctness theorems *)
  1570 
  1571     fun make_distincts_1 _ [] = []
  1572       | make_distincts_1 tname ((cname, cargs)::constrs) =
  1573           let
  1574             val cname = Sign.intern_const thy8
  1575               (NameSpace.append tname (Sign.base_name cname));
  1576             val (Ts, T) = strip_type (the (Sign.const_type thy8 cname));
  1577             val frees = map Free ((DatatypeProp.make_tnames Ts) ~~ Ts);
  1578             val t = list_comb (Const (cname, Ts ---> T), frees);
  1579 
  1580             fun make_distincts' [] = []
  1581               | make_distincts' ((cname', cargs')::constrs') =
  1582                   let
  1583                     val cname' = Sign.intern_const thy8
  1584                       (NameSpace.append tname (Sign.base_name cname'));
  1585                     val Ts' = binder_types (the (Sign.const_type thy8 cname'));
  1586                     val frees' = map Free ((map ((op ^) o (rpair "'"))
  1587                       (DatatypeProp.make_tnames Ts')) ~~ Ts');
  1588                     val t' = list_comb (Const (cname', Ts' ---> T), frees')
  1589                   in
  1590                     (HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t')))::
  1591                       (make_distincts' constrs')
  1592                   end
  1593 
  1594           in (make_distincts' constrs) @ (make_distincts_1 tname constrs)
  1595           end;
  1596 
  1597     val distinct_props = map (fn ((_, (_, _, constrs)), tname) =>
  1598         make_distincts_1 tname constrs)
  1599       (List.take (descr, length new_type_names) ~~ new_type_names);
  1600 
  1601     val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
  1602       dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
  1603         (constr_rep_thmss ~~ dist_lemmas);
  1604 
  1605     fun prove_distinct_thms (_, []) = []
  1606       | prove_distinct_thms (p as (rep_thms, dist_lemma), t::ts) =
  1607           let
  1608             val dist_thm = prove_goalw_cterm [] (cterm_of thy8 t) (fn _ =>
  1609               [simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1])
  1610           in dist_thm::(standard (dist_thm RS not_sym))::
  1611             (prove_distinct_thms (p, ts))
  1612           end;
  1613 
  1614     val distinct_thms = map prove_distinct_thms
  1615       (constr_rep_thmss ~~ dist_lemmas ~~ distinct_props);
  1616 
  1617     (** prove equations for permutation functions **)
  1618 
  1619     val abs_perm = PureThy.get_thms thy8 (Name "abs_perm"); (* FIXME *)
  1620 
  1621     val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
  1622       let val T = replace_types' (nth_dtyp i)
  1623       in List.concat (map (fn (atom, perm_closed_thms) =>
  1624           map (fn ((cname, dts), constr_rep_thm) => 
  1625         let
  1626           val cname = Sign.intern_const thy8
  1627             (NameSpace.append tname (Sign.base_name cname));
  1628           val permT = mk_permT (Type (atom, []));
  1629           val pi = Free ("pi", permT);
  1630 
  1631           fun perm t =
  1632             let val T = fastype_of t
  1633             in Const ("nominal.perm", permT --> T --> T) $ pi $ t end;
  1634 
  1635           fun constr_arg (dt, (j, l_args, r_args)) =
  1636             let
  1637               val x' = mk_Free "x" (typ_of_dtyp' dt) j;
  1638               val (dts, dt') = strip_option dt;
  1639               val Ts = map typ_of_dtyp' dts;
  1640               val xs = map (fn (T, i) => mk_Free "x" T i)
  1641                 (Ts ~~ (j upto j + length dts - 1))
  1642               val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
  1643               val (dts', dt'') = strip_dtyp dt';
  1644             in case dt'' of
  1645                 DtRec k => if k < length new_type_names then
  1646                     (j + length dts + 1,
  1647                      xs @ x :: l_args,
  1648                      map perm (xs @ [x]) @ r_args)
  1649                   else error "nested recursion not (yet) supported"
  1650               | _ => (j + 1, x' :: l_args, perm x' :: r_args)
  1651             end
  1652 
  1653           val (_, l_args, r_args) = foldr constr_arg (1, [], []) dts;
  1654           val c = Const (cname, map fastype_of l_args ---> T)
  1655         in
  1656           prove_goalw_cterm [] (cterm_of thy8
  1657             (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1658               (perm (list_comb (c, l_args)), list_comb (c, r_args)))))
  1659             (fn _ =>
  1660               [simp_tac (simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1,
  1661                simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @
  1662                  constr_defs @ perm_closed_thms)) 1,
  1663                TRY (simp_tac (HOL_basic_ss addsimps
  1664                  (symmetric perm_fun_def :: abs_perm)) 1),
  1665                TRY (simp_tac (HOL_basic_ss addsimps
  1666                  (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
  1667                     perm_closed_thms)) 1)])
  1668         end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss))
  1669       end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
  1670 
  1671     (** prove injectivity of constructors **)
  1672 
  1673     val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
  1674     val alpha = PureThy.get_thms thy8 (Name "alpha");
  1675     val abs_fresh = PureThy.get_thms thy8 (Name "abs_fresh");
  1676     val fresh_def = PureThy.get_thm thy8 (Name "fresh_def");
  1677     val supp_def = PureThy.get_thm thy8 (Name "supp_def");
  1678 
  1679     val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
  1680       let val T = replace_types' (nth_dtyp i)
  1681       in List.mapPartial (fn ((cname, dts), constr_rep_thm) =>
  1682         if null dts then NONE else SOME
  1683         let
  1684           val cname = Sign.intern_const thy8
  1685             (NameSpace.append tname (Sign.base_name cname));
  1686 
  1687           fun make_inj (dt, (j, args1, args2, eqs)) =
  1688             let
  1689               val x' = mk_Free "x" (typ_of_dtyp' dt) j;
  1690               val y' = mk_Free "y" (typ_of_dtyp' dt) j;
  1691               val (dts, dt') = strip_option dt;
  1692               val Ts_idx = map typ_of_dtyp' dts ~~ (j upto j + length dts - 1);
  1693               val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
  1694               val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx;
  1695               val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
  1696               val y = mk_Free "y" (typ_of_dtyp' dt') (j + length dts);
  1697               val (dts', dt'') = strip_dtyp dt';
  1698             in case dt'' of
  1699                 DtRec k => if k < length new_type_names then
  1700                     (j + length dts + 1,
  1701                      xs @ (x :: args1), ys @ (y :: args2),
  1702                      HOLogic.mk_eq
  1703                        (foldr mk_abs_fun x xs, foldr mk_abs_fun y ys) :: eqs)
  1704                   else error "nested recursion not (yet) supported"
  1705               | _ => (j + 1, x' :: args1, y' :: args2, HOLogic.mk_eq (x', y') :: eqs)
  1706             end;
  1707 
  1708           val (_, args1, args2, eqs) = foldr make_inj (1, [], [], []) dts;
  1709           val Ts = map fastype_of args1;
  1710           val c = Const (cname, Ts ---> T)
  1711         in
  1712           prove_goalw_cterm [] (cterm_of thy8 (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1713               (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)),
  1714                foldr1 HOLogic.mk_conj eqs))))
  1715             (fn _ =>
  1716                [asm_full_simp_tac (simpset_of thy8 addsimps (constr_rep_thm ::
  1717                   rep_inject_thms')) 1,
  1718                 TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def ::
  1719                   alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
  1720                   perm_rep_perm_thms)) 1)])
  1721         end) (constrs ~~ constr_rep_thms)
  1722       end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
  1723 
  1724     (** equations for support and freshness **)
  1725 
  1726     val Un_assoc = PureThy.get_thm thy8 (Name "Un_assoc");
  1727     val de_Morgan_conj = PureThy.get_thm thy8 (Name "de_Morgan_conj");
  1728     val Collect_disj_eq = PureThy.get_thm thy8 (Name "Collect_disj_eq");
  1729     val finite_Un = PureThy.get_thm thy8 (Name "finite_Un");
  1730 
  1731     val (supp_thms, fresh_thms) = ListPair.unzip (map ListPair.unzip
  1732       (map (fn ((((i, (_, _, constrs)), tname), inject_thms'), perm_thms') =>
  1733       let val T = replace_types' (nth_dtyp i)
  1734       in List.concat (map (fn (cname, dts) => map (fn atom =>
  1735         let
  1736           val cname = Sign.intern_const thy8
  1737             (NameSpace.append tname (Sign.base_name cname));
  1738           val atomT = Type (atom, []);
  1739 
  1740           fun process_constr (dt, (j, args1, args2)) =
  1741             let
  1742               val x' = mk_Free "x" (typ_of_dtyp' dt) j;
  1743               val (dts, dt') = strip_option dt;
  1744               val Ts_idx = map typ_of_dtyp' dts ~~ (j upto j + length dts - 1);
  1745               val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
  1746               val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
  1747               val (dts', dt'') = strip_dtyp dt';
  1748             in case dt'' of
  1749                 DtRec k => if k < length new_type_names then
  1750                     (j + length dts + 1,
  1751                      xs @ (x :: args1), foldr mk_abs_fun x xs :: args2)
  1752                   else error "nested recursion not (yet) supported"
  1753               | _ => (j + 1, x' :: args1, x' :: args2)
  1754             end;
  1755 
  1756           val (_, args1, args2) = foldr process_constr (1, [], []) dts;
  1757           val Ts = map fastype_of args1;
  1758           val c = list_comb (Const (cname, Ts ---> T), args1);
  1759           fun supp t =
  1760             Const ("nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
  1761           fun fresh t =
  1762             Const ("nominal.fresh", atomT --> fastype_of t --> HOLogic.boolT) $
  1763               Free ("a", atomT) $ t;
  1764           val supp_thm = prove_goalw_cterm [] (cterm_of thy8
  1765               (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1766                 (supp c,
  1767                  if null dts then Const ("{}", HOLogic.mk_setT atomT)
  1768                  else foldr1 (HOLogic.mk_binop "op Un") (map supp args2)))))
  1769             (fn _ =>
  1770               [simp_tac (HOL_basic_ss addsimps (supp_def ::
  1771                  Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
  1772                  abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1])
  1773         in
  1774           (supp_thm,
  1775            prove_goalw_cterm [] (cterm_of thy8 (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1776               (fresh c,
  1777                if null dts then HOLogic.true_const
  1778                else foldr1 HOLogic.mk_conj (map fresh args2)))))
  1779              (fn _ =>
  1780                [simp_tac (simpset_of thy8 addsimps [fresh_def, supp_thm]) 1]))
  1781         end) atoms) constrs)
  1782       end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
  1783 
  1784     val (thy9, _) = thy8 |>
  1785       DatatypeAux.store_thmss "distinct" new_type_names distinct_thms |>>>
  1786       DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss |>>>
  1787       DatatypeAux.store_thmss "perm" new_type_names perm_simps' |>>>
  1788       DatatypeAux.store_thmss "inject" new_type_names inject_thms |>>>
  1789       DatatypeAux.store_thmss "supp" new_type_names supp_thms |>>>
  1790       DatatypeAux.store_thmss "fresh" new_type_names fresh_thms;
  1791 
  1792   in
  1793     (thy9, perm_eq_thms)
  1794   end;
  1795 
  1796 val add_nominal_datatype = gen_add_nominal_datatype read_typ true;
  1797 
  1798 
  1799 (* FIXME: The following stuff should be exported by DatatypePackage *)
  1800 
  1801 local structure P = OuterParse and K = OuterKeyword in
  1802 
  1803 val datatype_decl =
  1804   Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
  1805     (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
  1806 
  1807 fun mk_datatype args =
  1808   let
  1809     val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
  1810     val specs = map (fn ((((_, vs), t), mx), cons) =>
  1811       (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
  1812   in #1 o add_nominal_datatype false names specs end;
  1813 
  1814 val nominal_datatypeP =
  1815   OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
  1816     (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
  1817 
  1818 val _ = OuterSyntax.add_parsers [nominal_datatypeP];
  1819 
  1820 end;
  1821 
  1822 end