src/HOL/Nominal/nominal_atoms.ML
changeset 19134 47d337aefc21
parent 19133 7e84a1a3741c
child 19139 af69e41eab5d
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Fri Feb 24 09:00:21 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Feb 24 17:48:17 2006 +0100
     1.3 @@ -401,7 +401,7 @@
     1.4  
     1.5           in
     1.6             thy'
     1.7 -           |> AxClass.add_inst_arity_i I (qu_name,[],[cls_name])
     1.8 +           |> AxClass.add_inst_arity_i (qu_name,[],[cls_name])
     1.9                (if ak_name = ak_name' then proof1 else proof2)
    1.10           end) ak_names thy) ak_names thy12c;
    1.11  
    1.12 @@ -435,15 +435,15 @@
    1.13            val pt_thm_set   = pt_inst RS pt_set_inst
    1.14         in 
    1.15  	thy
    1.16 -	|> AxClass.add_inst_arity_i I ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
    1.17 -        |> AxClass.add_inst_arity_i I ("nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
    1.18 -        |> AxClass.add_inst_arity_i I ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
    1.19 -        |> AxClass.add_inst_arity_i I ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
    1.20 -        |> AxClass.add_inst_arity_i I ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
    1.21 -        |> AxClass.add_inst_arity_i I ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    1.22 +	|> AxClass.add_inst_arity_i ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
    1.23 +        |> AxClass.add_inst_arity_i ("nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
    1.24 +        |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
    1.25 +        |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
    1.26 +        |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
    1.27 +        |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    1.28                                      (pt_proof pt_thm_nprod)
    1.29 -        |> AxClass.add_inst_arity_i I ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
    1.30 -        |> AxClass.add_inst_arity_i I ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
    1.31 +        |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
    1.32 +        |> AxClass.add_inst_arity_i ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
    1.33       end) ak_names thy13; 
    1.34  
    1.35         (*<<<<<<<  fs_<ak> class instances  >>>>>>>*)
    1.36 @@ -476,7 +476,7 @@
    1.37                        val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites.emptyI]; 
    1.38                    in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end)      
    1.39          in 
    1.40 -	 AxClass.add_inst_arity_i I (qu_name,[],[qu_class]) proof thy' 
    1.41 +	 AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy' 
    1.42          end) ak_names thy) ak_names thy18;
    1.43  
    1.44         (* shows that                  *)
    1.45 @@ -500,12 +500,12 @@
    1.46            val fs_thm_optn  = fs_inst RS fs_option_inst;
    1.47          in 
    1.48           thy 
    1.49 -         |> AxClass.add_inst_arity_i I ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
    1.50 -         |> AxClass.add_inst_arity_i I ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
    1.51 -         |> AxClass.add_inst_arity_i I ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    1.52 +         |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
    1.53 +         |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
    1.54 +         |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    1.55                                       (fs_proof fs_thm_nprod) 
    1.56 -         |> AxClass.add_inst_arity_i I ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
    1.57 -         |> AxClass.add_inst_arity_i I ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
    1.58 +         |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
    1.59 +         |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
    1.60          end) ak_names thy20; 
    1.61  
    1.62         (*<<<<<<<  cp_<ak>_<ai> class instances  >>>>>>>*)
    1.63 @@ -551,7 +551,7 @@
    1.64                      EVERY [ClassPackage.intro_classes_tac [], simp_tac simp_s 1]
    1.65                    end))
    1.66  	      in
    1.67 -                AxClass.add_inst_arity_i I (name,[],[cls_name]) proof thy''
    1.68 +                AxClass.add_inst_arity_i (name,[],[cls_name]) proof thy''
    1.69  	      end) ak_names thy') ak_names thy) ak_names thy24;
    1.70        
    1.71         (* shows that                                                    *) 
    1.72 @@ -580,12 +580,12 @@
    1.73              val cp_thm_noptn = cp_inst RS cp_noption_inst;
    1.74          in
    1.75           thy'
    1.76 -         |> AxClass.add_inst_arity_i I ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
    1.77 -	 |> AxClass.add_inst_arity_i I ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
    1.78 -         |> AxClass.add_inst_arity_i I ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
    1.79 -         |> AxClass.add_inst_arity_i I ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
    1.80 -         |> AxClass.add_inst_arity_i I ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
    1.81 -         |> AxClass.add_inst_arity_i I ("nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
    1.82 +         |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
    1.83 +	 |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
    1.84 +         |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
    1.85 +         |> AxClass.add_inst_arity_i ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
    1.86 +         |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
    1.87 +         |> AxClass.add_inst_arity_i ("nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
    1.88          end) ak_names thy) ak_names thy25;
    1.89         
    1.90       (* show that discrete nominal types are permutation types, finitely     *) 
    1.91 @@ -601,7 +601,7 @@
    1.92  	       val simp_s = HOL_basic_ss addsimps [defn];
    1.93                 val proof = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];      
    1.94               in  
    1.95 -	       AxClass.add_inst_arity_i I (discrete_ty,[],[qu_class]) proof thy
    1.96 +	       AxClass.add_inst_arity_i (discrete_ty,[],[qu_class]) proof thy
    1.97               end) ak_names;
    1.98  
    1.99            fun discrete_fs_inst discrete_ty defn = 
   1.100 @@ -612,7 +612,7 @@
   1.101                 val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites.emptyI,defn];
   1.102                 val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];      
   1.103               in  
   1.104 -	       AxClass.add_inst_arity_i I (discrete_ty,[],[qu_class]) proof thy
   1.105 +	       AxClass.add_inst_arity_i (discrete_ty,[],[qu_class]) proof thy
   1.106               end) ak_names;  
   1.107  
   1.108            fun discrete_cp_inst discrete_ty defn = 
   1.109 @@ -623,7 +623,7 @@
   1.110                 val simp_s = HOL_ss addsimps [defn];
   1.111                 val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];      
   1.112               in  
   1.113 -	       AxClass.add_inst_arity_i I (discrete_ty,[],[qu_class]) proof thy
   1.114 +	       AxClass.add_inst_arity_i (discrete_ty,[],[qu_class]) proof thy
   1.115               end) ak_names)) ak_names;  
   1.116            
   1.117          in