src/HOL/Nominal/nominal_atoms.ML

 
 structure NominalData = TheoryDataFun(NominalArgs);
 
 fun atoms_of thy = map fst (Symtab.dest (NominalData.get thy));
 
-(* FIXME: add to hologic.ML ? *)
-fun mk_listT T = Type ("List.list", [T]);
-fun mk_permT T = mk_listT (HOLogic.mk_prodT (T, T));
+fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
 
 fun mk_Cons x xs =
   let val T = fastype_of x
-  in Const ("List.list.Cons", T --> mk_listT T --> mk_listT T) $ x $ xs end;
+  in Const ("List.list.Cons", T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
 
 
 (* this function sets up all matters related to atom-  *)
 (* kinds; the user specifies a list of atom-kind names *)
 (* atom_decl <ak1> ... <akn>                           *)

 	       end
            else 
             ([],thy')))  (* do nothing branch, if ak_name = ak_name' *) 
 	    ak_names_types thy) ak_names_types thy12c;
 
-     (*<<<<<<<  pt_<ak> class instances  >>>>>>>*)
+     (********  pt_<ak> class instances  ********)
      (*=========================================*)
      (* some abbreviations for theorems *)
       val pt1           = thm "pt1";
       val pt2           = thm "pt2";
       val pt3           = thm "pt3";

      val thy18 = fold (fn ak_name => fn thy =>
        let
           val cls_name = Sign.full_name (sign_of thy) ("pt_"^ak_name);
           val at_thm   = PureThy.get_thm thy (Name ("at_"^ak_name^"_inst"));
           val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
-          
+
           fun pt_proof thm = 
-	      EVERY [ClassPackage.intro_classes_tac [],
+              EVERY [ClassPackage.intro_classes_tac [],
                      rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1];
 
           val pt_thm_fun   = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst));
           val pt_thm_noptn = pt_inst RS pt_noptn_inst; 
           val pt_thm_optn  = pt_inst RS pt_optn_inst; 
           val pt_thm_list  = pt_inst RS pt_list_inst;
           val pt_thm_prod  = pt_inst RS (pt_inst RS pt_prod_inst);
           val pt_thm_nprod = pt_inst RS (pt_inst RS pt_nprod_inst);
           val pt_thm_unit  = pt_unit_inst;
           val pt_thm_set   = pt_inst RS pt_set_inst
-       in 
-	thy
-	|> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
+       in
+        thy
+        |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
         |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
         |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
         |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
         |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
         |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
                                     (pt_proof pt_thm_nprod)
         |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
         |> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
      end) ak_names thy13; 
 
-       (*<<<<<<<  fs_<ak> class instances  >>>>>>>*)
+       (********  fs_<ak> class instances  ********)
        (*=========================================*)
        (* abbreviations for some lemmas *)
        val fs1            = thm "fs1";
        val fs_at_inst     = thm "fs_at_inst";
        val fs_unit_inst   = thm "fs_unit_inst";

        val dj_supp        = thm "dj_supp"
 
        (* shows that <ak> is an instance of fs_<ak>     *)
        (* uses the theorem at_<ak>_inst                 *)
        val thy20 = fold (fn ak_name => fn thy =>
-	fold (fn ak_name' => fn thy' => 
+        fold (fn ak_name' => fn thy' =>
         let
            val qu_name =  Sign.full_name (sign_of thy') ak_name';
            val qu_class = Sign.full_name (sign_of thy') ("fs_"^ak_name);
-           val proof = 
-	       (if ak_name = ak_name'
-	        then
-	          let val at_thm = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
+           val proof =
+               (if ak_name = ak_name'
+                then
+                  let val at_thm = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
                   in  EVERY [ClassPackage.intro_classes_tac [],
                              rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
                 else
-		  let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name));
-                      val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites.emptyI]; 
-                  in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end)      
-        in 
-	 AxClass.prove_arity (qu_name,[],[qu_class]) proof thy' 
+                  let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name));
+                      val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites.emptyI];
+                  in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end)
+        in
+         AxClass.prove_arity (qu_name,[],[qu_class]) proof thy'
         end) ak_names thy) ak_names thy18;
 
        (* shows that                  *)
        (*    unit                     *)
        (*    *(fs_<ak>,fs_<ak>)       *)

 
        val thy24 = fold (fn ak_name => fn thy => 
         let
           val cls_name = Sign.full_name (sign_of thy) ("fs_"^ak_name);
           val fs_inst  = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
-          fun fs_proof thm = EVERY [ClassPackage.intro_classes_tac [], rtac (thm RS fs1) 1];      
+          fun fs_proof thm = EVERY [ClassPackage.intro_classes_tac [], rtac (thm RS fs1) 1];
 
           val fs_thm_unit  = fs_unit_inst;
           val fs_thm_prod  = fs_inst RS (fs_inst RS fs_prod_inst);
           val fs_thm_nprod = fs_inst RS (fs_inst RS fs_nprod_inst);
           val fs_thm_list  = fs_inst RS fs_list_inst;
           val fs_thm_optn  = fs_inst RS fs_option_inst;
         in 
-         thy 
+         thy
          |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
          |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
          |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
                                      (fs_proof fs_thm_nprod) 
          |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
          |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
-        end) ak_names thy20; 
-
-       (*<<<<<<<  cp_<ak>_<ai> class instances  >>>>>>>*)
+        end) ak_names thy20;
+
+       (********  cp_<ak>_<ai> class instances  ********)
        (*==============================================*)
        (* abbreviations for some lemmas *)
        val cp1             = thm "cp1";
        val cp_unit_inst    = thm "cp_unit_inst";
        val cp_bool_inst    = thm "cp_bool_inst";

        val cp_list_inst    = thm "cp_list_inst";
        val cp_fun_inst     = thm "cp_fun_inst";
        val cp_option_inst  = thm "cp_option_inst";
        val cp_noption_inst = thm "cp_noption_inst";
        val pt_perm_compose = thm "pt_perm_compose";
-       
+
        val dj_pp_forget    = thm "dj_perm_perm_forget";
 
        (* shows that <aj> is an instance of cp_<ak>_<ai>  *)
        (* for every  <ak>/<ai>-combination                *)
-       val thy25 = fold (fn ak_name => fn thy => 
-	 fold (fn ak_name' => fn thy' => 
-          fold (fn ak_name'' => fn thy'' => 
+       val thy25 = fold (fn ak_name => fn thy =>
+         fold (fn ak_name' => fn thy' =>
+          fold (fn ak_name'' => fn thy'' =>
             let
               val name =  Sign.full_name (sign_of thy'') ak_name;
               val cls_name = Sign.full_name (sign_of thy'') ("cp_"^ak_name'^"_"^ak_name'');
               val proof =
                 (if (ak_name'=ak_name'') then 
-		  (let
+                  (let
                     val pt_inst  = PureThy.get_thm thy'' (Name ("pt_"^ak_name''^"_inst"));
-		    val at_inst  = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst"));
-                  in 
-		   EVERY [ClassPackage.intro_classes_tac [], 
+                    val at_inst  = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst"));
+                  in
+		   EVERY [ClassPackage.intro_classes_tac [],
                           rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]
                   end)
 		else
-		  (let 
+		  (let
                      val dj_inst  = PureThy.get_thm thy'' (Name ("dj_"^ak_name''^"_"^ak_name'));
-		     val simp_s = HOL_basic_ss addsimps 
+		     val simp_s = HOL_basic_ss addsimps
                                         ((dj_inst RS dj_pp_forget)::
-                                         (PureThy.get_thmss thy'' 
-					   [Name (ak_name' ^"_prm_"^ak_name^"_def"),
-                                            Name (ak_name''^"_prm_"^ak_name^"_def")]));  
-		  in 
+                                         (PureThy.get_thmss thy''
+                                           [Name (ak_name' ^"_prm_"^ak_name^"_def"),
+                                            Name (ak_name''^"_prm_"^ak_name^"_def")]));
+                  in
                     EVERY [ClassPackage.intro_classes_tac [], simp_tac simp_s 1]
                   end))
-	      in
+              in
                 AxClass.prove_arity (name,[],[cls_name]) proof thy''
-	      end) ak_names thy') ak_names thy) ak_names thy24;
-      
+              end) ak_names thy') ak_names thy) ak_names thy24;
+
        (* shows that                                                    *) 
        (*      units                                                    *) 
        (*      products                                                 *)
        (*      lists                                                    *)
        (*      functions                                                *)

             val cls_name = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
             val cp_inst  = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
             val pt_inst  = PureThy.get_thm thy' (Name ("pt_"^ak_name^"_inst"));
             val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
 
-            fun cp_proof thm  = EVERY [ClassPackage.intro_classes_tac [],rtac (thm RS cp1) 1];     
+            fun cp_proof thm  = EVERY [ClassPackage.intro_classes_tac [],rtac (thm RS cp1) 1];
 	  
             val cp_thm_unit = cp_unit_inst;
             val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst);
             val cp_thm_list = cp_inst RS cp_list_inst;
             val cp_thm_fun  = at_inst RS (pt_inst RS (cp_inst RS (cp_inst RS cp_fun_inst)));

          |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
          |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
          |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
          |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
         end) ak_names thy) ak_names thy25;
-       
-     (* show that discrete nominal types are permutation types, finitely     *) 
+
+     (* show that discrete nominal types are permutation types, finitely     *)
      (* supported and have the commutation property                          *)
      (* discrete types have a permutation operation defined as pi o x = x;   *)
-     (* which renders the proofs to be simple "simp_all"-proofs.             *)            
+     (* which renders the proofs to be simple "simp_all"-proofs.             *)
      val thy32 =
-        let 
-	  fun discrete_pt_inst discrete_ty defn = 
+        let
+	  fun discrete_pt_inst discrete_ty defn =
 	     fold (fn ak_name => fn thy =>
 	     let
 	       val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
 	       val simp_s = HOL_basic_ss addsimps [defn];
-               val proof = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];      
-             in  
+               val proof = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
+             in 
 	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
              end) ak_names;
 
           fun discrete_fs_inst discrete_ty defn = 
 	     fold (fn ak_name => fn thy =>
 	     let
 	       val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
 	       val supp_def = thm "Nominal.supp_def";
                val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites.emptyI,defn];
-               val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];      
-             in  
+               val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
+             in 
 	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
-             end) ak_names;  
+             end) ak_names;
 
           fun discrete_cp_inst discrete_ty defn = 
 	     fold (fn ak_name' => (fold (fn ak_name => fn thy =>
 	     let
 	       val qu_class = Sign.full_name (sign_of thy) ("cp_"^ak_name^"_"^ak_name');
 	       val supp_def = thm "Nominal.supp_def";
                val simp_s = HOL_ss addsimps [defn];
-               val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];      
-             in  
+               val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
+             in
 	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
-             end) ak_names)) ak_names;  
-          
+             end) ak_names)) ak_names;
+
         in
          thy26
          |> discrete_pt_inst "nat"  (thm "perm_nat_def")
          |> discrete_fs_inst "nat"  (thm "perm_nat_def") 
          |> discrete_cp_inst "nat"  (thm "perm_nat_def") 

          |> discrete_pt_inst "List.char" (thm "perm_char_def")
          |> discrete_fs_inst "List.char" (thm "perm_char_def")
          |> discrete_cp_inst "List.char" (thm "perm_char_def")
         end;
 
- 
+
        (* abbreviations for some lemmas *)
        (*===============================*)
        val abs_fun_pi          = thm "Nominal.abs_fun_pi";
        val abs_fun_pi_ineq     = thm "Nominal.abs_fun_pi_ineq";
        val abs_fun_eq          = thm "Nominal.abs_fun_eq";

        val fresh_eqvt          = thm "Nominal.pt_fresh_eqvt";
        val all_eqvt            = thm "Nominal.pt_all_eqvt";
        val pt_pi_rev           = thm "Nominal.pt_pi_rev";
        val pt_rev_pi           = thm "Nominal.pt_rev_pi";
        val at_exists_fresh     = thm "Nominal.at_exists_fresh";
-  
+
 
        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
        (* types; this allows for example to use abs_perm (which is a      *)
        (* collection of theorems) instead of thm abs_fun_pi with explicit *)
        (* instantiations.                                                 *)
-       val (_,thy33) = 
-	 let 
-             
+       val (_, thy33) =
+         let
 
              (* takes a theorem thm and a list of theorems [t1,..,tn]            *)
              (* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *) 
              fun instR thm thms = map (fn ti => ti RS thm) thms;
 

 	       let fun djs_fun (ak1,ak2) = 
 		     if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 (Name ("dj_"^ak2^"_"^ak1)))
 	       in List.mapPartial I (map djs_fun (Library.product ak_names ak_names)) end;
              (* list of all fs_inst-theorems *)
              val fss = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"_inst"))) ak_names
-              
-             fun inst_pt thms = Library.flat (map (fn ti => instR ti pts) thms); 
-             fun inst_at thms = Library.flat (map (fn ti => instR ti ats) thms);               
+
+             fun inst_pt thms = Library.flat (map (fn ti => instR ti pts) thms);
+             fun inst_at thms = Library.flat (map (fn ti => instR ti ats) thms);
              fun inst_fs thms = Library.flat (map (fn ti => instR ti fss) thms);
-             fun inst_cp thms cps = Library.flat (inst_mult thms cps); 
-	     fun inst_pt_at thms = inst_zip ats (inst_pt thms);			
-             fun inst_dj thms = Library.flat (map (fn ti => instR ti djs) thms);  
+             fun inst_cp thms cps = Library.flat (inst_mult thms cps);
+	     fun inst_pt_at thms = inst_zip ats (inst_pt thms);
+             fun inst_dj thms = Library.flat (map (fn ti => instR ti djs) thms);
 	     fun inst_pt_pt_at_cp thms = inst_cp (inst_zip ats (inst_zip pts (inst_pt thms))) cps;
              fun inst_pt_at_fs thms = inst_zip (inst_fs [fs1]) (inst_zip ats (inst_pt thms));
-	     fun inst_pt_pt_at_cp thms = 
+	     fun inst_pt_pt_at_cp thms =
 		 let val i_pt_pt_at = inst_zip ats (inst_zip pts (inst_pt thms));
                      val i_pt_pt_at_cp = inst_cp i_pt_pt_at cps';
 		 in i_pt_pt_at_cp end;
              fun inst_pt_pt_at_cp_dj thms = inst_zip djs (inst_pt_pt_at_cp thms);
            in