Adapted to Florian's recent changes to the AxClass package.
authorberghofe
Fri Feb 24 09:00:21 2006 +0100 (2006-02-24)
changeset 191337e84a1a3741c
parent 19132 ff41946e5092
child 19134 47d337aefc21
Adapted to Florian's recent changes to the AxClass package.
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Thu Feb 23 20:56:31 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Feb 24 09:00:21 2006 +0100
     1.3 @@ -390,18 +390,18 @@
     1.4             val cls_name = Sign.full_name (sign_of thy') ("pt_"^ak_name);
     1.5             val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name'^"_inst")); 
     1.6  
     1.7 -           val proof1 = EVERY [AxClass.intro_classes_tac [],
     1.8 +           val proof1 = EVERY [ClassPackage.intro_classes_tac [],
     1.9                                   rtac ((at_inst RS at_pt_inst) RS pt1) 1,
    1.10                                   rtac ((at_inst RS at_pt_inst) RS pt2) 1,
    1.11                                   rtac ((at_inst RS at_pt_inst) RS pt3) 1,
    1.12                                   atac 1];
    1.13             val simp_s = HOL_basic_ss addsimps 
    1.14                          PureThy.get_thmss thy' [Name (ak_name^"_prm_"^ak_name'^"_def")];  
    1.15 -           val proof2 = EVERY [AxClass.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
    1.16 +           val proof2 = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
    1.17  
    1.18           in
    1.19             thy'
    1.20 -           |> AxClass.add_inst_arity_i (qu_name,[],[cls_name])
    1.21 +           |> AxClass.add_inst_arity_i I (qu_name,[],[cls_name])
    1.22                (if ak_name = ak_name' then proof1 else proof2)
    1.23           end) ak_names thy) ak_names thy12c;
    1.24  
    1.25 @@ -422,7 +422,7 @@
    1.26            val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
    1.27            
    1.28            fun pt_proof thm = 
    1.29 -	      EVERY [AxClass.intro_classes_tac [],
    1.30 +	      EVERY [ClassPackage.intro_classes_tac [],
    1.31                       rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1];
    1.32  
    1.33            val pt_thm_fun   = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst));
    1.34 @@ -435,15 +435,15 @@
    1.35            val pt_thm_set   = pt_inst RS pt_set_inst
    1.36         in 
    1.37  	thy
    1.38 -	|> AxClass.add_inst_arity_i ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
    1.39 -        |> AxClass.add_inst_arity_i ("nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
    1.40 -        |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
    1.41 -        |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
    1.42 -        |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
    1.43 -        |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    1.44 +	|> AxClass.add_inst_arity_i I ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
    1.45 +        |> AxClass.add_inst_arity_i I ("nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
    1.46 +        |> AxClass.add_inst_arity_i I ("Datatype.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
    1.47 +        |> AxClass.add_inst_arity_i I ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
    1.48 +        |> AxClass.add_inst_arity_i I ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
    1.49 +        |> AxClass.add_inst_arity_i I ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    1.50                                      (pt_proof pt_thm_nprod)
    1.51 -        |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
    1.52 -        |> AxClass.add_inst_arity_i ("set",[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
    1.53 +        |> AxClass.add_inst_arity_i I ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
    1.54 +        |> AxClass.add_inst_arity_i I ("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 @@ -469,14 +469,14 @@
    1.59  	       (if ak_name = ak_name'
    1.60  	        then
    1.61  	          let val at_thm = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
    1.62 -                  in  EVERY [AxClass.intro_classes_tac [],
    1.63 +                  in  EVERY [ClassPackage.intro_classes_tac [],
    1.64                               rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
    1.65                  else
    1.66  		  let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name));
    1.67                        val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites.emptyI]; 
    1.68 -                  in EVERY [AxClass.intro_classes_tac [], asm_simp_tac simp_s 1] end)      
    1.69 +                  in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end)      
    1.70          in 
    1.71 -	 AxClass.add_inst_arity_i (qu_name,[],[qu_class]) proof thy' 
    1.72 +	 AxClass.add_inst_arity_i I (qu_name,[],[qu_class]) proof thy' 
    1.73          end) ak_names thy) ak_names thy18;
    1.74  
    1.75         (* shows that                  *)
    1.76 @@ -491,7 +491,7 @@
    1.77          let
    1.78            val cls_name = Sign.full_name (sign_of thy) ("fs_"^ak_name);
    1.79            val fs_inst  = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
    1.80 -          fun fs_proof thm = EVERY [AxClass.intro_classes_tac [], rtac (thm RS fs1) 1];      
    1.81 +          fun fs_proof thm = EVERY [ClassPackage.intro_classes_tac [], rtac (thm RS fs1) 1];      
    1.82  
    1.83            val fs_thm_unit  = fs_unit_inst;
    1.84            val fs_thm_prod  = fs_inst RS (fs_inst RS fs_prod_inst);
    1.85 @@ -500,12 +500,12 @@
    1.86            val fs_thm_optn  = fs_inst RS fs_option_inst;
    1.87          in 
    1.88           thy 
    1.89 -         |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
    1.90 -         |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
    1.91 -         |> AxClass.add_inst_arity_i ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    1.92 +         |> AxClass.add_inst_arity_i I ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
    1.93 +         |> AxClass.add_inst_arity_i I ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
    1.94 +         |> AxClass.add_inst_arity_i I ("nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    1.95                                       (fs_proof fs_thm_nprod) 
    1.96 -         |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
    1.97 -         |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
    1.98 +         |> AxClass.add_inst_arity_i I ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
    1.99 +         |> AxClass.add_inst_arity_i I ("Datatype.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
   1.100          end) ak_names thy20; 
   1.101  
   1.102         (*<<<<<<<  cp_<ak>_<ai> class instances  >>>>>>>*)
   1.103 @@ -536,7 +536,7 @@
   1.104                      val pt_inst  = PureThy.get_thm thy'' (Name ("pt_"^ak_name''^"_inst"));
   1.105  		    val at_inst  = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst"));
   1.106                    in 
   1.107 -		   EVERY [AxClass.intro_classes_tac [], 
   1.108 +		   EVERY [ClassPackage.intro_classes_tac [], 
   1.109                            rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]
   1.110                    end)
   1.111  		else
   1.112 @@ -548,10 +548,10 @@
   1.113  					   [Name (ak_name' ^"_prm_"^ak_name^"_def"),
   1.114                                              Name (ak_name''^"_prm_"^ak_name^"_def")]));  
   1.115  		  in 
   1.116 -                    EVERY [AxClass.intro_classes_tac [], simp_tac simp_s 1]
   1.117 +                    EVERY [ClassPackage.intro_classes_tac [], simp_tac simp_s 1]
   1.118                    end))
   1.119  	      in
   1.120 -                AxClass.add_inst_arity_i (name,[],[cls_name]) proof thy''
   1.121 +                AxClass.add_inst_arity_i I (name,[],[cls_name]) proof thy''
   1.122  	      end) ak_names thy') ak_names thy) ak_names thy24;
   1.123        
   1.124         (* shows that                                                    *) 
   1.125 @@ -570,7 +570,7 @@
   1.126              val pt_inst  = PureThy.get_thm thy' (Name ("pt_"^ak_name^"_inst"));
   1.127              val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
   1.128  
   1.129 -            fun cp_proof thm  = EVERY [AxClass.intro_classes_tac [],rtac (thm RS cp1) 1];     
   1.130 +            fun cp_proof thm  = EVERY [ClassPackage.intro_classes_tac [],rtac (thm RS cp1) 1];     
   1.131  	  
   1.132              val cp_thm_unit = cp_unit_inst;
   1.133              val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst);
   1.134 @@ -580,12 +580,12 @@
   1.135              val cp_thm_noptn = cp_inst RS cp_noption_inst;
   1.136          in
   1.137           thy'
   1.138 -         |> AxClass.add_inst_arity_i ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
   1.139 -	 |> AxClass.add_inst_arity_i ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
   1.140 -         |> AxClass.add_inst_arity_i ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
   1.141 -         |> AxClass.add_inst_arity_i ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
   1.142 -         |> AxClass.add_inst_arity_i ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
   1.143 -         |> AxClass.add_inst_arity_i ("nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
   1.144 +         |> AxClass.add_inst_arity_i I ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
   1.145 +	 |> AxClass.add_inst_arity_i I ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
   1.146 +         |> AxClass.add_inst_arity_i I ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
   1.147 +         |> AxClass.add_inst_arity_i I ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
   1.148 +         |> AxClass.add_inst_arity_i I ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
   1.149 +         |> AxClass.add_inst_arity_i I ("nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
   1.150          end) ak_names thy) ak_names thy25;
   1.151         
   1.152       (* show that discrete nominal types are permutation types, finitely     *) 
   1.153 @@ -599,9 +599,9 @@
   1.154  	     let
   1.155  	       val qu_class = Sign.full_name (sign_of thy) ("pt_"^ak_name);
   1.156  	       val simp_s = HOL_basic_ss addsimps [defn];
   1.157 -               val proof = EVERY [AxClass.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];      
   1.158 +               val proof = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];      
   1.159               in  
   1.160 -	       AxClass.add_inst_arity_i (discrete_ty,[],[qu_class]) proof thy
   1.161 +	       AxClass.add_inst_arity_i I (discrete_ty,[],[qu_class]) proof thy
   1.162               end) ak_names;
   1.163  
   1.164            fun discrete_fs_inst discrete_ty defn = 
   1.165 @@ -610,9 +610,9 @@
   1.166  	       val qu_class = Sign.full_name (sign_of thy) ("fs_"^ak_name);
   1.167  	       val supp_def = thm "nominal.supp_def";
   1.168                 val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites.emptyI,defn];
   1.169 -               val proof = EVERY [AxClass.intro_classes_tac [], asm_simp_tac simp_s 1];      
   1.170 +               val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];      
   1.171               in  
   1.172 -	       AxClass.add_inst_arity_i (discrete_ty,[],[qu_class]) proof thy
   1.173 +	       AxClass.add_inst_arity_i I (discrete_ty,[],[qu_class]) proof thy
   1.174               end) ak_names;  
   1.175  
   1.176            fun discrete_cp_inst discrete_ty defn = 
   1.177 @@ -621,9 +621,9 @@
   1.178  	       val qu_class = Sign.full_name (sign_of thy) ("cp_"^ak_name^"_"^ak_name');
   1.179  	       val supp_def = thm "nominal.supp_def";
   1.180                 val simp_s = HOL_ss addsimps [defn];
   1.181 -               val proof = EVERY [AxClass.intro_classes_tac [], asm_simp_tac simp_s 1];      
   1.182 +               val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];      
   1.183               in  
   1.184 -	       AxClass.add_inst_arity_i (discrete_ty,[],[qu_class]) proof thy
   1.185 +	       AxClass.add_inst_arity_i I (discrete_ty,[],[qu_class]) proof thy
   1.186               end) ak_names)) ak_names;  
   1.187            
   1.188          in
     2.1 --- a/src/HOL/Nominal/nominal_package.ML	Thu Feb 23 20:56:31 2006 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_package.ML	Fri Feb 24 09:00:21 2006 +0100
     2.3 @@ -23,7 +23,7 @@
     2.4  fun dt_cases (descr: descr) (_, args, constrs) =
     2.5    let
     2.6      fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
     2.7 -    val bnames = map the_bname (distinct (List.concat (map dt_recs args)));
     2.8 +    val bnames = map the_bname (distinct op = (List.concat (map dt_recs args)));
     2.9    in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
    2.10  
    2.11  
    2.12 @@ -411,17 +411,17 @@
    2.13            (fn _ => EVERY [indtac induction perm_indnames 1,
    2.14               ALLGOALS (asm_full_simp_tac simps)])))
    2.15        in
    2.16 -        foldl (fn ((s, tvs), thy) => AxClass.add_inst_arity_i
    2.17 +        foldl (fn ((s, tvs), thy) => AxClass.add_inst_arity_i I
    2.18              (s, replicate (length tvs) (cp_class :: classes), [cp_class])
    2.19 -            (AxClass.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
    2.20 +            (ClassPackage.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
    2.21            thy (full_new_type_names' ~~ tyvars)
    2.22        end;
    2.23  
    2.24      val (perm_thmss,thy3) = thy2 |>
    2.25        fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
    2.26        curry (Library.foldr (fn ((i, (tyname, args, _)), thy) =>
    2.27 -        AxClass.add_inst_arity_i (tyname, replicate (length args) classes, classes)
    2.28 -        (AxClass.intro_classes_tac [] THEN REPEAT (EVERY
    2.29 +        AxClass.add_inst_arity_i I (tyname, replicate (length args) classes, classes)
    2.30 +        (ClassPackage.intro_classes_tac [] THEN REPEAT (EVERY
    2.31             [resolve_tac perm_empty_thms 1,
    2.32              resolve_tac perm_append_thms 1,
    2.33              resolve_tac perm_eq_thms 1, assume_tac 1])) thy))
    2.34 @@ -457,7 +457,7 @@
    2.35            apfst (cons dt) (strip_option dt')
    2.36        | strip_option dt = ([], dt);
    2.37  
    2.38 -    val dt_atomTs = distinct (map (typ_of_dtyp descr sorts')
    2.39 +    val dt_atomTs = distinct op = (map (typ_of_dtyp descr sorts')
    2.40        (List.concat (map (fn (_, (_, _, cs)) => List.concat
    2.41          (map (List.concat o map (fst o strip_option) o snd) cs)) descr)));
    2.42  
    2.43 @@ -585,10 +585,10 @@
    2.44      fun pt_instance ((class, atom), perm_closed_thms) =
    2.45        fold (fn (((({Abs_inverse, Rep_inverse, Rep, ...},
    2.46          perm_def), name), tvs), perm_closed) => fn thy =>
    2.47 -          AxClass.add_inst_arity_i
    2.48 +          AxClass.add_inst_arity_i I
    2.49              (Sign.intern_type thy name,
    2.50                replicate (length tvs) (classes @ cp_classes), [class])
    2.51 -            (EVERY [AxClass.intro_classes_tac [],
    2.52 +            (EVERY [ClassPackage.intro_classes_tac [],
    2.53                rewrite_goals_tac [perm_def],
    2.54                asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
    2.55                asm_full_simp_tac (simpset_of thy addsimps
    2.56 @@ -609,10 +609,10 @@
    2.57          val cp1' = PureThy.get_thm thy (Name (name ^ "_inst")) RS cp1
    2.58        in fold (fn ((((({Abs_inverse, Rep_inverse, Rep, ...},
    2.59          perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
    2.60 -          AxClass.add_inst_arity_i
    2.61 +          AxClass.add_inst_arity_i I
    2.62              (Sign.intern_type thy name,
    2.63                replicate (length tvs) (classes @ cp_classes), [class])
    2.64 -            (EVERY [AxClass.intro_classes_tac [],
    2.65 +            (EVERY [ClassPackage.intro_classes_tac [],
    2.66                rewrite_goals_tac [perm_def],
    2.67                asm_full_simp_tac (simpset_of thy addsimps
    2.68                  ((Rep RS perm_closed1 RS Abs_inverse) ::
    2.69 @@ -1086,10 +1086,10 @@
    2.70        DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms ||>
    2.71        fold (fn (atom, ths) => fn thy =>
    2.72          let val class = Sign.intern_class thy ("fs_" ^ Sign.base_name atom)
    2.73 -        in fold (fn T => AxClass.add_inst_arity_i
    2.74 +        in fold (fn T => AxClass.add_inst_arity_i I
    2.75              (fst (dest_Type T),
    2.76                replicate (length sorts) [class], [class])
    2.77 -            (AxClass.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
    2.78 +            (ClassPackage.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
    2.79          end) (atoms ~~ finite_supp_thms);
    2.80  
    2.81      (**** strong induction theorem ****)