replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
authorwebertj
Tue Jul 11 18:10:47 2006 +0200 (2006-07-11)
changeset 20097be2d96bbf39c
parent 20096 7058714024b3
child 20098 19871ee094b1
replaced mk_listT by HOLogic.listT; trivial whitespace/comment changes
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Jul 11 14:21:08 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Jul 11 18:10:47 2006 +0200
     1.3 @@ -35,13 +35,11 @@
     1.4  
     1.5  fun atoms_of thy = map fst (Symtab.dest (NominalData.get thy));
     1.6  
     1.7 -(* FIXME: add to hologic.ML ? *)
     1.8 -fun mk_listT T = Type ("List.list", [T]);
     1.9 -fun mk_permT T = mk_listT (HOLogic.mk_prodT (T, T));
    1.10 +fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
    1.11  
    1.12  fun mk_Cons x xs =
    1.13    let val T = fastype_of x
    1.14 -  in Const ("List.list.Cons", T --> mk_listT T --> mk_listT T) $ x $ xs end;
    1.15 +  in Const ("List.list.Cons", T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
    1.16  
    1.17  
    1.18  (* this function sets up all matters related to atom-  *)
    1.19 @@ -369,7 +367,7 @@
    1.20              ([],thy')))  (* do nothing branch, if ak_name = ak_name' *) 
    1.21  	    ak_names_types thy) ak_names_types thy12c;
    1.22  
    1.23 -     (*<<<<<<<  pt_<ak> class instances  >>>>>>>*)
    1.24 +     (********  pt_<ak> class instances  ********)
    1.25       (*=========================================*)
    1.26       (* some abbreviations for theorems *)
    1.27        val pt1           = thm "pt1";
    1.28 @@ -425,9 +423,9 @@
    1.29            val cls_name = Sign.full_name (sign_of thy) ("pt_"^ak_name);
    1.30            val at_thm   = PureThy.get_thm thy (Name ("at_"^ak_name^"_inst"));
    1.31            val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
    1.32 -          
    1.33 +
    1.34            fun pt_proof thm = 
    1.35 -	      EVERY [ClassPackage.intro_classes_tac [],
    1.36 +              EVERY [ClassPackage.intro_classes_tac [],
    1.37                       rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1];
    1.38  
    1.39            val pt_thm_fun   = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst));
    1.40 @@ -438,9 +436,9 @@
    1.41            val pt_thm_nprod = pt_inst RS (pt_inst RS pt_nprod_inst);
    1.42            val pt_thm_unit  = pt_unit_inst;
    1.43            val pt_thm_set   = pt_inst RS pt_set_inst
    1.44 -       in 
    1.45 -	thy
    1.46 -	|> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
    1.47 +       in
    1.48 +        thy
    1.49 +        |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
    1.50          |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
    1.51          |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
    1.52          |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
    1.53 @@ -451,7 +449,7 @@
    1.54          |> AxClass.prove_arity ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
    1.55       end) ak_names thy13; 
    1.56  
    1.57 -       (*<<<<<<<  fs_<ak> class instances  >>>>>>>*)
    1.58 +       (********  fs_<ak> class instances  ********)
    1.59         (*=========================================*)
    1.60         (* abbreviations for some lemmas *)
    1.61         val fs1            = thm "fs1";
    1.62 @@ -466,22 +464,22 @@
    1.63         (* shows that <ak> is an instance of fs_<ak>     *)
    1.64         (* uses the theorem at_<ak>_inst                 *)
    1.65         val thy20 = fold (fn ak_name => fn thy =>
    1.66 -	fold (fn ak_name' => fn thy' => 
    1.67 +        fold (fn ak_name' => fn thy' =>
    1.68          let
    1.69             val qu_name =  Sign.full_name (sign_of thy') ak_name';
    1.70             val qu_class = Sign.full_name (sign_of thy') ("fs_"^ak_name);
    1.71 -           val proof = 
    1.72 -	       (if ak_name = ak_name'
    1.73 -	        then
    1.74 -	          let val at_thm = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
    1.75 +           val proof =
    1.76 +               (if ak_name = ak_name'
    1.77 +                then
    1.78 +                  let val at_thm = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
    1.79                    in  EVERY [ClassPackage.intro_classes_tac [],
    1.80                               rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
    1.81                  else
    1.82 -		  let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name));
    1.83 -                      val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites.emptyI]; 
    1.84 -                  in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end)      
    1.85 -        in 
    1.86 -	 AxClass.prove_arity (qu_name,[],[qu_class]) proof thy' 
    1.87 +                  let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name));
    1.88 +                      val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites.emptyI];
    1.89 +                  in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end)
    1.90 +        in
    1.91 +         AxClass.prove_arity (qu_name,[],[qu_class]) proof thy'
    1.92          end) ak_names thy) ak_names thy18;
    1.93  
    1.94         (* shows that                  *)
    1.95 @@ -496,7 +494,7 @@
    1.96          let
    1.97            val cls_name = Sign.full_name (sign_of thy) ("fs_"^ak_name);
    1.98            val fs_inst  = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
    1.99 -          fun fs_proof thm = EVERY [ClassPackage.intro_classes_tac [], rtac (thm RS fs1) 1];      
   1.100 +          fun fs_proof thm = EVERY [ClassPackage.intro_classes_tac [], rtac (thm RS fs1) 1];
   1.101  
   1.102            val fs_thm_unit  = fs_unit_inst;
   1.103            val fs_thm_prod  = fs_inst RS (fs_inst RS fs_prod_inst);
   1.104 @@ -504,16 +502,16 @@
   1.105            val fs_thm_list  = fs_inst RS fs_list_inst;
   1.106            val fs_thm_optn  = fs_inst RS fs_option_inst;
   1.107          in 
   1.108 -         thy 
   1.109 +         thy
   1.110           |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
   1.111           |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
   1.112           |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   1.113                                       (fs_proof fs_thm_nprod) 
   1.114           |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
   1.115           |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
   1.116 -        end) ak_names thy20; 
   1.117 +        end) ak_names thy20;
   1.118  
   1.119 -       (*<<<<<<<  cp_<ak>_<ai> class instances  >>>>>>>*)
   1.120 +       (********  cp_<ak>_<ai> class instances  ********)
   1.121         (*==============================================*)
   1.122         (* abbreviations for some lemmas *)
   1.123         val cp1             = thm "cp1";
   1.124 @@ -525,41 +523,41 @@
   1.125         val cp_option_inst  = thm "cp_option_inst";
   1.126         val cp_noption_inst = thm "cp_noption_inst";
   1.127         val pt_perm_compose = thm "pt_perm_compose";
   1.128 -       
   1.129 +
   1.130         val dj_pp_forget    = thm "dj_perm_perm_forget";
   1.131  
   1.132         (* shows that <aj> is an instance of cp_<ak>_<ai>  *)
   1.133         (* for every  <ak>/<ai>-combination                *)
   1.134 -       val thy25 = fold (fn ak_name => fn thy => 
   1.135 -	 fold (fn ak_name' => fn thy' => 
   1.136 -          fold (fn ak_name'' => fn thy'' => 
   1.137 +       val thy25 = fold (fn ak_name => fn thy =>
   1.138 +         fold (fn ak_name' => fn thy' =>
   1.139 +          fold (fn ak_name'' => fn thy'' =>
   1.140              let
   1.141                val name =  Sign.full_name (sign_of thy'') ak_name;
   1.142                val cls_name = Sign.full_name (sign_of thy'') ("cp_"^ak_name'^"_"^ak_name'');
   1.143                val proof =
   1.144                  (if (ak_name'=ak_name'') then 
   1.145 -		  (let
   1.146 +                  (let
   1.147                      val pt_inst  = PureThy.get_thm thy'' (Name ("pt_"^ak_name''^"_inst"));
   1.148 -		    val at_inst  = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst"));
   1.149 -                  in 
   1.150 -		   EVERY [ClassPackage.intro_classes_tac [], 
   1.151 +                    val at_inst  = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst"));
   1.152 +                  in
   1.153 +		   EVERY [ClassPackage.intro_classes_tac [],
   1.154                            rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]
   1.155                    end)
   1.156  		else
   1.157 -		  (let 
   1.158 +		  (let
   1.159                       val dj_inst  = PureThy.get_thm thy'' (Name ("dj_"^ak_name''^"_"^ak_name'));
   1.160 -		     val simp_s = HOL_basic_ss addsimps 
   1.161 +		     val simp_s = HOL_basic_ss addsimps
   1.162                                          ((dj_inst RS dj_pp_forget)::
   1.163 -                                         (PureThy.get_thmss thy'' 
   1.164 -					   [Name (ak_name' ^"_prm_"^ak_name^"_def"),
   1.165 -                                            Name (ak_name''^"_prm_"^ak_name^"_def")]));  
   1.166 -		  in 
   1.167 +                                         (PureThy.get_thmss thy''
   1.168 +                                           [Name (ak_name' ^"_prm_"^ak_name^"_def"),
   1.169 +                                            Name (ak_name''^"_prm_"^ak_name^"_def")]));
   1.170 +                  in
   1.171                      EVERY [ClassPackage.intro_classes_tac [], simp_tac simp_s 1]
   1.172                    end))
   1.173 -	      in
   1.174 +              in
   1.175                  AxClass.prove_arity (name,[],[cls_name]) proof thy''
   1.176 -	      end) ak_names thy') ak_names thy) ak_names thy24;
   1.177 -      
   1.178 +              end) ak_names thy') ak_names thy) ak_names thy24;
   1.179 +
   1.180         (* shows that                                                    *) 
   1.181         (*      units                                                    *) 
   1.182         (*      products                                                 *)
   1.183 @@ -576,7 +574,7 @@
   1.184              val pt_inst  = PureThy.get_thm thy' (Name ("pt_"^ak_name^"_inst"));
   1.185              val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
   1.186  
   1.187 -            fun cp_proof thm  = EVERY [ClassPackage.intro_classes_tac [],rtac (thm RS cp1) 1];     
   1.188 +            fun cp_proof thm  = EVERY [ClassPackage.intro_classes_tac [],rtac (thm RS cp1) 1];
   1.189  	  
   1.190              val cp_thm_unit = cp_unit_inst;
   1.191              val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst);
   1.192 @@ -593,20 +591,20 @@
   1.193           |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
   1.194           |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
   1.195          end) ak_names thy) ak_names thy25;
   1.196 -       
   1.197 -     (* show that discrete nominal types are permutation types, finitely     *) 
   1.198 +
   1.199 +     (* show that discrete nominal types are permutation types, finitely     *)
   1.200       (* supported and have the commutation property                          *)
   1.201       (* discrete types have a permutation operation defined as pi o x = x;   *)
   1.202 -     (* which renders the proofs to be simple "simp_all"-proofs.             *)            
   1.203 +     (* which renders the proofs to be simple "simp_all"-proofs.             *)
   1.204       val thy32 =
   1.205 -        let 
   1.206 -	  fun discrete_pt_inst discrete_ty defn = 
   1.207 +        let
   1.208 +	  fun discrete_pt_inst discrete_ty defn =
   1.209  	     fold (fn ak_name => fn thy =>
   1.210  	     let
   1.211  	       val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   1.212  	       val simp_s = HOL_basic_ss addsimps [defn];
   1.213 -               val proof = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];      
   1.214 -             in  
   1.215 +               val proof = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
   1.216 +             in 
   1.217  	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
   1.218               end) ak_names;
   1.219  
   1.220 @@ -616,10 +614,10 @@
   1.221  	       val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
   1.222  	       val supp_def = thm "Nominal.supp_def";
   1.223                 val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites.emptyI,defn];
   1.224 -               val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];      
   1.225 -             in  
   1.226 +               val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
   1.227 +             in 
   1.228  	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
   1.229 -             end) ak_names;  
   1.230 +             end) ak_names;
   1.231  
   1.232            fun discrete_cp_inst discrete_ty defn = 
   1.233  	     fold (fn ak_name' => (fold (fn ak_name => fn thy =>
   1.234 @@ -627,11 +625,11 @@
   1.235  	       val qu_class = Sign.full_name (sign_of thy) ("cp_"^ak_name^"_"^ak_name');
   1.236  	       val supp_def = thm "Nominal.supp_def";
   1.237                 val simp_s = HOL_ss addsimps [defn];
   1.238 -               val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];      
   1.239 -             in  
   1.240 +               val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
   1.241 +             in
   1.242  	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
   1.243 -             end) ak_names)) ak_names;  
   1.244 -          
   1.245 +             end) ak_names)) ak_names;
   1.246 +
   1.247          in
   1.248           thy26
   1.249           |> discrete_pt_inst "nat"  (thm "perm_nat_def")
   1.250 @@ -648,7 +646,7 @@
   1.251           |> discrete_cp_inst "List.char" (thm "perm_char_def")
   1.252          end;
   1.253  
   1.254 - 
   1.255 +
   1.256         (* abbreviations for some lemmas *)
   1.257         (*===============================*)
   1.258         val abs_fun_pi          = thm "Nominal.abs_fun_pi";
   1.259 @@ -685,15 +683,14 @@
   1.260         val pt_pi_rev           = thm "Nominal.pt_pi_rev";
   1.261         val pt_rev_pi           = thm "Nominal.pt_rev_pi";
   1.262         val at_exists_fresh     = thm "Nominal.at_exists_fresh";
   1.263 -  
   1.264 +
   1.265  
   1.266         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
   1.267         (* types; this allows for example to use abs_perm (which is a      *)
   1.268         (* collection of theorems) instead of thm abs_fun_pi with explicit *)
   1.269         (* instantiations.                                                 *)
   1.270 -       val (_,thy33) = 
   1.271 -	 let 
   1.272 -             
   1.273 +       val (_, thy33) =
   1.274 +         let
   1.275  
   1.276               (* takes a theorem thm and a list of theorems [t1,..,tn]            *)
   1.277               (* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *) 
   1.278 @@ -733,16 +730,16 @@
   1.279  	       in List.mapPartial I (map djs_fun (Library.product ak_names ak_names)) end;
   1.280               (* list of all fs_inst-theorems *)
   1.281               val fss = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"_inst"))) ak_names
   1.282 -              
   1.283 -             fun inst_pt thms = Library.flat (map (fn ti => instR ti pts) thms); 
   1.284 -             fun inst_at thms = Library.flat (map (fn ti => instR ti ats) thms);               
   1.285 +
   1.286 +             fun inst_pt thms = Library.flat (map (fn ti => instR ti pts) thms);
   1.287 +             fun inst_at thms = Library.flat (map (fn ti => instR ti ats) thms);
   1.288               fun inst_fs thms = Library.flat (map (fn ti => instR ti fss) thms);
   1.289 -             fun inst_cp thms cps = Library.flat (inst_mult thms cps); 
   1.290 -	     fun inst_pt_at thms = inst_zip ats (inst_pt thms);			
   1.291 -             fun inst_dj thms = Library.flat (map (fn ti => instR ti djs) thms);  
   1.292 +             fun inst_cp thms cps = Library.flat (inst_mult thms cps);
   1.293 +	     fun inst_pt_at thms = inst_zip ats (inst_pt thms);
   1.294 +             fun inst_dj thms = Library.flat (map (fn ti => instR ti djs) thms);
   1.295  	     fun inst_pt_pt_at_cp thms = inst_cp (inst_zip ats (inst_zip pts (inst_pt thms))) cps;
   1.296               fun inst_pt_at_fs thms = inst_zip (inst_fs [fs1]) (inst_zip ats (inst_pt thms));
   1.297 -	     fun inst_pt_pt_at_cp thms = 
   1.298 +	     fun inst_pt_pt_at_cp thms =
   1.299  		 let val i_pt_pt_at = inst_zip ats (inst_zip pts (inst_pt thms));
   1.300                       val i_pt_pt_at_cp = inst_cp i_pt_pt_at cps';
   1.301  		 in i_pt_pt_at_cp end;