src/HOL/Nominal/nominal_atoms.ML
changeset 26337 44473c957672
parent 26090 ec111fa4f8c5
child 26343 0dd2eab7b296
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Mar 19 22:27:57 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Mar 19 22:28:08 2008 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Nominal/nominal_atoms.ML
     1.5 +(*  title:      HOL/Nominal/nominal_atoms.ML
     1.6      ID:         $Id$
     1.7      Author:     Christian Urban and Stefan Berghofer, TU Muenchen
     1.8  
     1.9 @@ -230,17 +230,17 @@
    1.10        let
    1.11          val ak_name_qu = Sign.full_name thy5 (ak_name);
    1.12          val i_type = Type(ak_name_qu,[]);
    1.13 -	val cat = Const ("Nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
    1.14 +        val cat = Const ("Nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
    1.15          val at_type = Logic.mk_type i_type;
    1.16 -        val simp_s = HOL_ss addsimps PureThy.get_thmss thy5
    1.17 -                                  [Name "at_def",
    1.18 -                                   Name (ak_name ^ "_prm_" ^ ak_name ^ "_def"),
    1.19 -                                   Name (ak_name ^ "_prm_" ^ ak_name ^ ".simps"),
    1.20 -                                   Name ("swap_" ^ ak_name ^ "_def"),
    1.21 -                                   Name ("swap_" ^ ak_name ^ ".simps"),
    1.22 -                                   Name (ak_name ^ "_infinite")]
    1.23 -	    
    1.24 -	val name = "at_"^ak_name^ "_inst";
    1.25 +        val simp_s = HOL_ss addsimps maps (dynamic_thms thy5)
    1.26 +                                  ["at_def",
    1.27 +                                   ak_name ^ "_prm_" ^ ak_name ^ "_def",
    1.28 +                                   ak_name ^ "_prm_" ^ ak_name ^ ".simps",
    1.29 +                                   "swap_" ^ ak_name ^ "_def",
    1.30 +                                   "swap_" ^ ak_name ^ ".simps",
    1.31 +                                   ak_name ^ "_infinite"]
    1.32 +            
    1.33 +        val name = "at_"^ak_name^ "_inst";
    1.34          val statement = HOLogic.mk_Trueprop (cat $ at_type);
    1.35  
    1.36          val proof = fn _ => simp_tac simp_s 1
    1.37 @@ -256,7 +256,7 @@
    1.38      (* pt_<ak>3:       pi1 ~ pi2 ==> perm pi1 x = perm pi2 x     *)
    1.39       val (pt_ax_classes,thy7) =  fold_map (fn (ak_name, T) => fn thy =>
    1.40        let 
    1.41 -	  val cl_name = "pt_"^ak_name;
    1.42 +          val cl_name = "pt_"^ak_name;
    1.43            val ty = TFree("'a",["HOL.type"]);
    1.44            val x   = Free ("x", ty);
    1.45            val pi1 = Free ("pi1", mk_permT T);
    1.46 @@ -293,16 +293,16 @@
    1.47          val pt_name_qu = Sign.full_name thy7 ("pt_"^ak_name);
    1.48          val i_type1 = TFree("'x",[pt_name_qu]);
    1.49          val i_type2 = Type(ak_name_qu,[]);
    1.50 -	val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    1.51 +        val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    1.52          val pt_type = Logic.mk_type i_type1;
    1.53          val at_type = Logic.mk_type i_type2;
    1.54 -        val simp_s = HOL_ss addsimps PureThy.get_thmss thy7
    1.55 -                                  [Name "pt_def",
    1.56 -                                   Name ("pt_" ^ ak_name ^ "1"),
    1.57 -                                   Name ("pt_" ^ ak_name ^ "2"),
    1.58 -                                   Name ("pt_" ^ ak_name ^ "3")];
    1.59 +        val simp_s = HOL_ss addsimps maps (dynamic_thms thy7)
    1.60 +                                  ["pt_def",
    1.61 +                                   "pt_" ^ ak_name ^ "1",
    1.62 +                                   "pt_" ^ ak_name ^ "2",
    1.63 +                                   "pt_" ^ ak_name ^ "3"];
    1.64  
    1.65 -	val name = "pt_"^ak_name^ "_inst";
    1.66 +        val name = "pt_"^ak_name^ "_inst";
    1.67          val statement = HOLogic.mk_Trueprop (cpt $ pt_type $ at_type);
    1.68  
    1.69          val proof = fn _ => simp_tac simp_s 1;
    1.70 @@ -315,8 +315,8 @@
    1.71       (* fs_<ak>1: finite ((supp x)::<ak> set)            *)
    1.72       val (fs_ax_classes,thy11) =  fold_map (fn (ak_name, T) => fn thy =>
    1.73         let 
    1.74 -	  val cl_name = "fs_"^ak_name;
    1.75 -	  val pt_name = Sign.full_name thy ("pt_"^ak_name);
    1.76 +          val cl_name = "fs_"^ak_name;
    1.77 +          val pt_name = Sign.full_name thy ("pt_"^ak_name);
    1.78            val ty = TFree("'a",["HOL.type"]);
    1.79            val x   = Free ("x", ty);
    1.80            val csupp    = Const ("Nominal.supp", ty --> HOLogic.mk_setT T);
    1.81 @@ -327,7 +327,7 @@
    1.82         in  
    1.83          AxClass.define_class (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy            
    1.84         end) ak_names_types thy8; 
    1.85 -	 
    1.86 +         
    1.87       (* proves that every fs_<ak>-type together with <ak>-type   *)
    1.88       (* instance of fs-type                                      *)
    1.89       (* lemma abst_<ak>_inst:                                    *)
    1.90 @@ -339,15 +339,15 @@
    1.91           val fs_name_qu = Sign.full_name thy11 ("fs_"^ak_name);
    1.92           val i_type1 = TFree("'x",[fs_name_qu]);
    1.93           val i_type2 = Type(ak_name_qu,[]);
    1.94 - 	 val cfs = Const ("Nominal.fs", 
    1.95 +         val cfs = Const ("Nominal.fs", 
    1.96                                   (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    1.97           val fs_type = Logic.mk_type i_type1;
    1.98           val at_type = Logic.mk_type i_type2;
    1.99 -	 val simp_s = HOL_ss addsimps PureThy.get_thmss thy11
   1.100 -                                   [Name "fs_def",
   1.101 -                                    Name ("fs_" ^ ak_name ^ "1")];
   1.102 +         val simp_s = HOL_ss addsimps maps (dynamic_thms thy11)
   1.103 +                                   ["fs_def",
   1.104 +                                    "fs_" ^ ak_name ^ "1"];
   1.105      
   1.106 -	 val name = "fs_"^ak_name^ "_inst";
   1.107 +         val name = "fs_"^ak_name^ "_inst";
   1.108           val statement = HOLogic.mk_Trueprop (cfs $ fs_type $ at_type);
   1.109  
   1.110           val proof = fn _ => simp_tac simp_s 1;
   1.111 @@ -359,54 +359,54 @@
   1.112         (* cp_<ak1>_<ak2> giving a composition property                   *)
   1.113         (* cp_<ak1>_<ak2>1: pi1 o pi2 o x = (pi1 o pi2) o (pi1 o x)       *)
   1.114          val (cp_ax_classes,thy12b) = fold_map (fn (ak_name, T) => fn thy =>
   1.115 -	 fold_map (fn (ak_name', T') => fn thy' =>
   1.116 -	     let
   1.117 -	       val cl_name = "cp_"^ak_name^"_"^ak_name';
   1.118 -	       val ty = TFree("'a",["HOL.type"]);
   1.119 +         fold_map (fn (ak_name', T') => fn thy' =>
   1.120 +             let
   1.121 +               val cl_name = "cp_"^ak_name^"_"^ak_name';
   1.122 +               val ty = TFree("'a",["HOL.type"]);
   1.123                 val x   = Free ("x", ty);
   1.124                 val pi1 = Free ("pi1", mk_permT T);
   1.125 -	       val pi2 = Free ("pi2", mk_permT T');                  
   1.126 -	       val cperm1 = Const ("Nominal.perm", mk_permT T  --> ty --> ty);
   1.127 +               val pi2 = Free ("pi2", mk_permT T');                  
   1.128 +               val cperm1 = Const ("Nominal.perm", mk_permT T  --> ty --> ty);
   1.129                 val cperm2 = Const ("Nominal.perm", mk_permT T' --> ty --> ty);
   1.130                 val cperm3 = Const ("Nominal.perm", mk_permT T  --> mk_permT T' --> mk_permT T');
   1.131  
   1.132                 val ax1   = HOLogic.mk_Trueprop 
   1.133 -			   (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
   1.134 +                           (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
   1.135                                             cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
   1.136 -	       in  
   1.137 -		 AxClass.define_class (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy'  
   1.138 -	       end) ak_names_types thy) ak_names_types thy12;
   1.139 +               in  
   1.140 +                 AxClass.define_class (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy'  
   1.141 +               end) ak_names_types thy) ak_names_types thy12;
   1.142  
   1.143          (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem;     *)
   1.144          (* lemma cp_<ak1>_<ak2>_inst:                                           *)
   1.145          (* cp TYPE('a::cp_<ak1>_<ak2>) TYPE(<ak1>) TYPE(<ak2>)                  *)
   1.146          val (cp_thms,thy12c) = fold_map (fn (ak_name, T) => fn thy =>
   1.147 -	 fold_map (fn (ak_name', T') => fn thy' =>
   1.148 +         fold_map (fn (ak_name', T') => fn thy' =>
   1.149             let
   1.150               val ak_name_qu  = Sign.full_name thy' (ak_name);
   1.151 -	     val ak_name_qu' = Sign.full_name thy' (ak_name');
   1.152 +             val ak_name_qu' = Sign.full_name thy' (ak_name');
   1.153               val cp_name_qu  = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name');
   1.154               val i_type0 = TFree("'a",[cp_name_qu]);
   1.155               val i_type1 = Type(ak_name_qu,[]);
   1.156               val i_type2 = Type(ak_name_qu',[]);
   1.157 -	     val ccp = Const ("Nominal.cp",
   1.158 +             val ccp = Const ("Nominal.cp",
   1.159                               (Term.itselfT i_type0)-->(Term.itselfT i_type1)-->
   1.160                                                        (Term.itselfT i_type2)-->HOLogic.boolT);
   1.161               val at_type  = Logic.mk_type i_type1;
   1.162               val at_type' = Logic.mk_type i_type2;
   1.163 -	     val cp_type  = Logic.mk_type i_type0;
   1.164 -             val simp_s   = HOL_basic_ss addsimps PureThy.get_thmss thy' [(Name "cp_def")];
   1.165 -	     val cp1      = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"1"));
   1.166 +             val cp_type  = Logic.mk_type i_type0;
   1.167 +             val simp_s   = HOL_basic_ss addsimps maps (dynamic_thms thy') ["cp_def"];
   1.168 +             val cp1      = dynamic_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1");
   1.169  
   1.170 -	     val name = "cp_"^ak_name^ "_"^ak_name'^"_inst";
   1.171 +             val name = "cp_"^ak_name^ "_"^ak_name'^"_inst";
   1.172               val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type');
   1.173  
   1.174               val proof = fn _ => EVERY [simp_tac simp_s 1, 
   1.175                                          rtac allI 1, rtac allI 1, rtac allI 1,
   1.176                                          rtac cp1 1];
   1.177 -	   in
   1.178 -	     PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
   1.179 -	   end) 
   1.180 +           in
   1.181 +             PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
   1.182 +           end) 
   1.183             ak_names_types thy) ak_names_types thy12b;
   1.184         
   1.185          (* proves for every non-trivial <ak>-combination a disjointness   *)
   1.186 @@ -414,33 +414,33 @@
   1.187          (* lemma ds_<ak1>_<ak2>:                                          *)
   1.188          (* dj TYPE(<ak1>) TYPE(<ak2>)                                     *)
   1.189          val (dj_thms, thy12d) = fold_map (fn (ak_name,T) => fn thy =>
   1.190 -	  fold_map (fn (ak_name',T') => fn thy' =>
   1.191 +          fold_map (fn (ak_name',T') => fn thy' =>
   1.192            (if not (ak_name = ak_name') 
   1.193             then 
   1.194 -	       let
   1.195 -		 val ak_name_qu  = Sign.full_name thy' ak_name;
   1.196 -	         val ak_name_qu' = Sign.full_name thy' ak_name';
   1.197 +               let
   1.198 +                 val ak_name_qu  = Sign.full_name thy' ak_name;
   1.199 +                 val ak_name_qu' = Sign.full_name thy' ak_name';
   1.200                   val i_type1 = Type(ak_name_qu,[]);
   1.201                   val i_type2 = Type(ak_name_qu',[]);
   1.202 -	         val cdj = Const ("Nominal.disjoint",
   1.203 +                 val cdj = Const ("Nominal.disjoint",
   1.204                             (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
   1.205                   val at_type  = Logic.mk_type i_type1;
   1.206                   val at_type' = Logic.mk_type i_type2;
   1.207 -                 val simp_s = HOL_ss addsimps PureThy.get_thmss thy' 
   1.208 -					   [Name "disjoint_def",
   1.209 -                                            Name (ak_name^"_prm_"^ak_name'^"_def"),
   1.210 -                                            Name (ak_name'^"_prm_"^ak_name^"_def")];
   1.211 +                 val simp_s = HOL_ss addsimps maps (dynamic_thms thy')
   1.212 +                                           ["disjoint_def",
   1.213 +                                            ak_name ^ "_prm_" ^ ak_name' ^ "_def",
   1.214 +                                            ak_name' ^ "_prm_" ^ ak_name ^ "_def"];
   1.215  
   1.216 -	         val name = "dj_"^ak_name^"_"^ak_name';
   1.217 +                 val name = "dj_"^ak_name^"_"^ak_name';
   1.218                   val statement = HOLogic.mk_Trueprop (cdj $ at_type $ at_type');
   1.219  
   1.220                   val proof = fn _ => simp_tac simp_s 1;
   1.221 -	       in
   1.222 -		PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
   1.223 -	       end
   1.224 +               in
   1.225 +                PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
   1.226 +               end
   1.227             else 
   1.228              ([],thy')))  (* do nothing branch, if ak_name = ak_name' *) 
   1.229 -	    ak_names_types thy) ak_names_types thy12c;
   1.230 +            ak_names_types thy) ak_names_types thy12c;
   1.231  
   1.232       (********  pt_<ak> class instances  ********)
   1.233       (*=========================================*)
   1.234 @@ -462,11 +462,11 @@
   1.235       (* every <ak> is an instance of pt_<ak'>; the proof for       *)
   1.236       (* ak!=ak' is by definition; the case ak=ak' uses at_pt_inst. *)
   1.237       val thy13 = fold (fn ak_name => fn thy =>
   1.238 -	fold (fn ak_name' => fn thy' =>
   1.239 +        fold (fn ak_name' => fn thy' =>
   1.240           let
   1.241             val qu_name =  Sign.full_name thy' ak_name';
   1.242             val cls_name = Sign.full_name thy' ("pt_"^ak_name);
   1.243 -           val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name'^"_inst")); 
   1.244 +           val at_inst  = dynamic_thm thy' ("at_" ^ ak_name' ^ "_inst");
   1.245  
   1.246             val proof1 = EVERY [Class.intro_classes_tac [],
   1.247                                   rtac ((at_inst RS at_pt_inst) RS pt1) 1,
   1.248 @@ -474,7 +474,7 @@
   1.249                                   rtac ((at_inst RS at_pt_inst) RS pt3) 1,
   1.250                                   atac 1];
   1.251             val simp_s = HOL_basic_ss addsimps 
   1.252 -                        PureThy.get_thmss thy' [Name (ak_name^"_prm_"^ak_name'^"_def")];  
   1.253 +                        maps (dynamic_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"];  
   1.254             val proof2 = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
   1.255  
   1.256           in
   1.257 @@ -496,8 +496,8 @@
   1.258       val thy18 = fold (fn ak_name => fn thy =>
   1.259         let
   1.260            val cls_name = Sign.full_name thy ("pt_"^ak_name);
   1.261 -          val at_thm   = PureThy.get_thm thy (Name ("at_"^ak_name^"_inst"));
   1.262 -          val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
   1.263 +          val at_thm   = dynamic_thm thy ("at_"^ak_name^"_inst");
   1.264 +          val pt_inst  = dynamic_thm thy ("pt_"^ak_name^"_inst");
   1.265  
   1.266            fun pt_proof thm = 
   1.267                EVERY [Class.intro_classes_tac [],
   1.268 @@ -546,11 +546,11 @@
   1.269             val proof =
   1.270                 (if ak_name = ak_name'
   1.271                  then
   1.272 -                  let val at_thm = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
   1.273 +                  let val at_thm = dynamic_thm thy' ("at_"^ak_name^"_inst");
   1.274                    in  EVERY [Class.intro_classes_tac [],
   1.275                               rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
   1.276                  else
   1.277 -                  let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name));
   1.278 +                  let val dj_inst = dynamic_thm thy' ("dj_"^ak_name'^"_"^ak_name);
   1.279                        val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI];
   1.280                    in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end)
   1.281          in
   1.282 @@ -568,7 +568,7 @@
   1.283         val thy24 = fold (fn ak_name => fn thy => 
   1.284          let
   1.285            val cls_name = Sign.full_name thy ("fs_"^ak_name);
   1.286 -          val fs_inst  = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
   1.287 +          val fs_inst  = dynamic_thm thy ("fs_"^ak_name^"_inst");
   1.288            fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1];
   1.289  
   1.290            val fs_thm_unit  = fs_unit_inst;
   1.291 @@ -613,20 +613,20 @@
   1.292                val proof =
   1.293                  (if (ak_name'=ak_name'') then 
   1.294                    (let
   1.295 -                    val pt_inst  = PureThy.get_thm thy'' (Name ("pt_"^ak_name''^"_inst"));
   1.296 -                    val at_inst  = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst"));
   1.297 +                    val pt_inst  = dynamic_thm thy'' ("pt_"^ak_name''^"_inst");
   1.298 +                    val at_inst  = dynamic_thm thy'' ("at_"^ak_name''^"_inst");
   1.299                    in
   1.300 -		   EVERY [Class.intro_classes_tac [],
   1.301 +                   EVERY [Class.intro_classes_tac [],
   1.302                            rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]
   1.303                    end)
   1.304 -		else
   1.305 -		  (let
   1.306 -                     val dj_inst  = PureThy.get_thm thy'' (Name ("dj_"^ak_name''^"_"^ak_name'));
   1.307 -		     val simp_s = HOL_basic_ss addsimps
   1.308 +                else
   1.309 +                  (let
   1.310 +                     val dj_inst  = dynamic_thm thy'' ("dj_"^ak_name''^"_"^ak_name');
   1.311 +                     val simp_s = HOL_basic_ss addsimps
   1.312                                          ((dj_inst RS dj_pp_forget)::
   1.313 -                                         (PureThy.get_thmss thy''
   1.314 -                                           [Name (ak_name' ^"_prm_"^ak_name^"_def"),
   1.315 -                                            Name (ak_name''^"_prm_"^ak_name^"_def")]));
   1.316 +                                         (maps (dynamic_thms thy'')
   1.317 +                                           [ak_name' ^"_prm_"^ak_name^"_def",
   1.318 +                                            ak_name''^"_prm_"^ak_name^"_def"]));
   1.319                    in
   1.320                      EVERY [Class.intro_classes_tac [], simp_tac simp_s 1]
   1.321                    end))
   1.322 @@ -644,15 +644,15 @@
   1.323         (*      sets                                                     *)
   1.324         (* are instances of cp_<ak>_<ai> for every <ak>/<ai>-combination *)
   1.325         val thy26 = fold (fn ak_name => fn thy =>
   1.326 -	fold (fn ak_name' => fn thy' =>
   1.327 +        fold (fn ak_name' => fn thy' =>
   1.328          let
   1.329              val cls_name = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name');
   1.330 -            val cp_inst  = PureThy.get_thm thy' (Name ("cp_"^ak_name^"_"^ak_name'^"_inst"));
   1.331 -            val pt_inst  = PureThy.get_thm thy' (Name ("pt_"^ak_name^"_inst"));
   1.332 -            val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
   1.333 +            val cp_inst  = dynamic_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst");
   1.334 +            val pt_inst  = dynamic_thm thy' ("pt_"^ak_name^"_inst");
   1.335 +            val at_inst  = dynamic_thm thy' ("at_"^ak_name^"_inst");
   1.336  
   1.337              fun cp_proof thm  = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1];
   1.338 -	  
   1.339 +          
   1.340              val cp_thm_unit = cp_unit_inst;
   1.341              val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst);
   1.342              val cp_thm_list = cp_inst RS cp_list_inst;
   1.343 @@ -663,7 +663,7 @@
   1.344          in
   1.345           thy'
   1.346           |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
   1.347 -	 |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
   1.348 +         |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
   1.349           |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
   1.350           |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
   1.351           |> AxClass.prove_arity ("Datatype.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
   1.352 @@ -677,36 +677,36 @@
   1.353       (* which renders the proofs to be simple "simp_all"-proofs.             *)
   1.354       val thy32 =
   1.355          let
   1.356 -	  fun discrete_pt_inst discrete_ty defn =
   1.357 -	     fold (fn ak_name => fn thy =>
   1.358 -	     let
   1.359 -	       val qu_class = Sign.full_name thy ("pt_"^ak_name);
   1.360 -	       val simp_s = HOL_basic_ss addsimps [defn];
   1.361 +          fun discrete_pt_inst discrete_ty defn =
   1.362 +             fold (fn ak_name => fn thy =>
   1.363 +             let
   1.364 +               val qu_class = Sign.full_name thy ("pt_"^ak_name);
   1.365 +               val simp_s = HOL_basic_ss addsimps [defn];
   1.366                 val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
   1.367               in 
   1.368 -	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
   1.369 +               AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
   1.370               end) ak_names;
   1.371  
   1.372            fun discrete_fs_inst discrete_ty defn = 
   1.373 -	     fold (fn ak_name => fn thy =>
   1.374 -	     let
   1.375 -	       val qu_class = Sign.full_name thy ("fs_"^ak_name);
   1.376 -	       val supp_def = @{thm "Nominal.supp_def"};
   1.377 +             fold (fn ak_name => fn thy =>
   1.378 +             let
   1.379 +               val qu_class = Sign.full_name thy ("fs_"^ak_name);
   1.380 +               val supp_def = @{thm "Nominal.supp_def"};
   1.381                 val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn];
   1.382                 val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
   1.383               in 
   1.384 -	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
   1.385 +               AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
   1.386               end) ak_names;
   1.387  
   1.388            fun discrete_cp_inst discrete_ty defn = 
   1.389 -	     fold (fn ak_name' => (fold (fn ak_name => fn thy =>
   1.390 -	     let
   1.391 -	       val qu_class = Sign.full_name thy ("cp_"^ak_name^"_"^ak_name');
   1.392 -	       val supp_def = @{thm "Nominal.supp_def"};
   1.393 +             fold (fn ak_name' => (fold (fn ak_name => fn thy =>
   1.394 +             let
   1.395 +               val qu_class = Sign.full_name thy ("cp_"^ak_name^"_"^ak_name');
   1.396 +               val supp_def = @{thm "Nominal.supp_def"};
   1.397                 val simp_s = HOL_ss addsimps [defn];
   1.398                 val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
   1.399               in
   1.400 -	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
   1.401 +               AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
   1.402               end) ak_names)) ak_names;
   1.403  
   1.404          in
   1.405 @@ -771,7 +771,7 @@
   1.406         val at_exists_fresh     = @{thm "Nominal.at_exists_fresh"};
   1.407         val at_exists_fresh'    = @{thm "Nominal.at_exists_fresh'"};
   1.408         val fresh_perm_app_ineq = @{thm "Nominal.pt_fresh_perm_app_ineq"};
   1.409 -       val fresh_perm_app      = @{thm "Nominal.pt_fresh_perm_app"};	
   1.410 +       val fresh_perm_app      = @{thm "Nominal.pt_fresh_perm_app"};    
   1.411         val fresh_aux           = @{thm "Nominal.pt_fresh_aux"};  
   1.412         val pt_perm_supp_ineq   = @{thm "Nominal.pt_perm_supp_ineq"};
   1.413         val pt_perm_supp        = @{thm "Nominal.pt_perm_supp"};
   1.414 @@ -804,58 +804,58 @@
   1.415  
   1.416               
   1.417               (* list of all at_inst-theorems *)
   1.418 -             val ats = map (fn ak => PureThy.get_thm thy32 (Name ("at_"^ak^"_inst"))) ak_names
   1.419 +             val ats = map (fn ak => dynamic_thm thy32 ("at_"^ak^"_inst")) ak_names
   1.420               (* list of all pt_inst-theorems *)
   1.421 -             val pts = map (fn ak => PureThy.get_thm thy32 (Name ("pt_"^ak^"_inst"))) ak_names
   1.422 +             val pts = map (fn ak => dynamic_thm thy32 ("pt_"^ak^"_inst")) ak_names
   1.423               (* list of all cp_inst-theorems as a collection of lists*)
   1.424               val cps = 
   1.425 -		 let fun cps_fun ak1 ak2 = PureThy.get_thm thy32 (Name ("cp_"^ak1^"_"^ak2^"_inst"))
   1.426 -		 in map (fn aki => (map (cps_fun aki) ak_names)) ak_names end; 
   1.427 +                 let fun cps_fun ak1 ak2 =  dynamic_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")
   1.428 +                 in map (fn aki => (map (cps_fun aki) ak_names)) ak_names end; 
   1.429               (* list of all cp_inst-theorems that have different atom types *)
   1.430               val cps' = 
   1.431 -		let fun cps'_fun ak1 ak2 = 
   1.432 -		if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 (Name ("cp_"^ak1^"_"^ak2^"_inst")))
   1.433 -		in map (fn aki => (List.mapPartial I (map (cps'_fun aki) ak_names))) ak_names end;
   1.434 +                let fun cps'_fun ak1 ak2 = 
   1.435 +                if ak1=ak2 then NONE else SOME (dynamic_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst"))
   1.436 +                in map (fn aki => (List.mapPartial I (map (cps'_fun aki) ak_names))) ak_names end;
   1.437               (* list of all dj_inst-theorems *)
   1.438               val djs = 
   1.439 -	       let fun djs_fun ak1 ak2 = 
   1.440 -		     if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 (Name ("dj_"^ak2^"_"^ak1)))
   1.441 -	       in map_filter I (map_product djs_fun ak_names ak_names) end;
   1.442 +               let fun djs_fun ak1 ak2 = 
   1.443 +                     if ak1=ak2 then NONE else SOME(dynamic_thm thy32 ("dj_"^ak2^"_"^ak1))
   1.444 +               in map_filter I (map_product djs_fun ak_names ak_names) end;
   1.445               (* list of all fs_inst-theorems *)
   1.446 -             val fss = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"_inst"))) ak_names
   1.447 +             val fss = map (fn ak => dynamic_thm thy32 ("fs_"^ak^"_inst")) ak_names
   1.448               (* list of all at_inst-theorems *)
   1.449 -             val fs_axs = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"1"))) ak_names
   1.450 +             val fs_axs = map (fn ak => dynamic_thm thy32 ("fs_"^ak^"1")) ak_names
   1.451  
   1.452               fun inst_pt thms = maps (fn ti => instR ti pts) thms;
   1.453               fun inst_at thms = maps (fn ti => instR ti ats) thms;
   1.454               fun inst_fs thms = maps (fn ti => instR ti fss) thms;
   1.455               fun inst_cp thms cps = flat (inst_mult thms cps);
   1.456 -	     fun inst_pt_at thms = inst_zip ats (inst_pt thms);
   1.457 +             fun inst_pt_at thms = inst_zip ats (inst_pt thms);
   1.458               fun inst_dj thms = maps (fn ti => instR ti djs) thms;
   1.459 -	     fun inst_pt_pt_at_cp thms = inst_cp (inst_zip ats (inst_zip pts (inst_pt thms))) cps;
   1.460 +             fun inst_pt_pt_at_cp thms = inst_cp (inst_zip ats (inst_zip pts (inst_pt thms))) cps;
   1.461               fun inst_pt_at_fs thms = inst_zip (inst_fs [fs1]) (inst_zip ats (inst_pt thms));
   1.462 -	     fun inst_pt_pt_at_cp thms =
   1.463 -		 let val i_pt_pt_at = inst_zip ats (inst_zip pts (inst_pt thms));
   1.464 +             fun inst_pt_pt_at_cp thms =
   1.465 +                 let val i_pt_pt_at = inst_zip ats (inst_zip pts (inst_pt thms));
   1.466                       val i_pt_pt_at_cp = inst_cp i_pt_pt_at cps';
   1.467 -		 in i_pt_pt_at_cp end;
   1.468 +                 in i_pt_pt_at_cp end;
   1.469               fun inst_pt_pt_at_cp_dj thms = inst_zip djs (inst_pt_pt_at_cp thms);
   1.470             in
   1.471              thy32 
   1.472 -	    |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
   1.473 +            |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
   1.474              ||>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])]
   1.475              ||>> PureThy.add_thmss [(("alpha_fresh", inst_pt_at [abs_fun_fresh]),[])]
   1.476              ||>> PureThy.add_thmss [(("alpha_fresh'", inst_pt_at [abs_fun_fresh']),[])]
   1.477              ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])]
   1.478 -            ||>> PureThy.add_thmss [(("swap_simps", inst_at at_swap_simps),[])]	 
   1.479 +            ||>> PureThy.add_thmss [(("swap_simps", inst_at at_swap_simps),[])]  
   1.480              ||>> PureThy.add_thmss 
   1.481 -	      let val thms1 = inst_pt_at [pt_pi_rev];
   1.482 -		  val thms2 = inst_pt_at [pt_rev_pi];
   1.483 +              let val thms1 = inst_pt_at [pt_pi_rev];
   1.484 +                  val thms2 = inst_pt_at [pt_rev_pi];
   1.485                in [(("perm_pi_simp",thms1 @ thms2),[])] end
   1.486              ||>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])]
   1.487              ||>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])]
   1.488              ||>> PureThy.add_thmss 
   1.489 -	      let val thms1 = inst_pt_at [pt_perm_compose];
   1.490 -		  val thms2 = instR cp1 (Library.flat cps');
   1.491 +              let val thms1 = inst_pt_at [pt_perm_compose];
   1.492 +                  val thms2 = instR cp1 (Library.flat cps');
   1.493                in [(("perm_compose",thms1 @ thms2),[])] end
   1.494              ||>> PureThy.add_thmss [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])] 
   1.495              ||>> PureThy.add_thmss [(("perm_app", inst_pt_at [perm_app]),[])]
   1.496 @@ -871,74 +871,74 @@
   1.497                end
   1.498              ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])]
   1.499              ||>> PureThy.add_thmss 
   1.500 -	      let val thms1 = inst_at [at_fresh]
   1.501 -		  val thms2 = inst_dj [at_fresh_ineq]
   1.502 -	      in [(("fresh_atm", thms1 @ thms2),[])] end
   1.503 +              let val thms1 = inst_at [at_fresh]
   1.504 +                  val thms2 = inst_dj [at_fresh_ineq]
   1.505 +              in [(("fresh_atm", thms1 @ thms2),[])] end
   1.506              ||>> PureThy.add_thmss
   1.507 -	      let val thms1 = filter
   1.508 +              let val thms1 = filter
   1.509                  (fn th => case prop_of th of _ $ _ $ Var _ => true | _ => false)
   1.510                  (List.concat (List.concat perm_defs))
   1.511                in [(("calc_atm", (inst_at at_calc) @ thms1),[])] end
   1.512              ||>> PureThy.add_thmss
   1.513 -	      let val thms1 = inst_pt_at [abs_fun_pi]
   1.514 -		  and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq]
   1.515 -	      in [(("abs_perm", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end
   1.516 +              let val thms1 = inst_pt_at [abs_fun_pi]
   1.517 +                  and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq]
   1.518 +              in [(("abs_perm", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end
   1.519              ||>> PureThy.add_thmss
   1.520 -	      let val thms1 = inst_dj [dj_perm_forget]
   1.521 -		  and thms2 = inst_dj [dj_pp_forget]
   1.522 +              let val thms1 = inst_dj [dj_perm_forget]
   1.523 +                  and thms2 = inst_dj [dj_pp_forget]
   1.524                in [(("perm_dj", thms1 @ thms2),[])] end
   1.525              ||>> PureThy.add_thmss
   1.526 -	      let val thms1 = inst_pt_at_fs [fresh_iff]
   1.527 +              let val thms1 = inst_pt_at_fs [fresh_iff]
   1.528                    and thms2 = inst_pt_at [fresh_iff]
   1.529 -		  and thms3 = inst_pt_pt_at_cp_dj [fresh_iff_ineq]
   1.530 -	    in [(("abs_fresh", thms1 @ thms2 @ thms3),[])] end
   1.531 -	    ||>> PureThy.add_thmss
   1.532 -	      let val thms1 = inst_pt_at [abs_fun_supp]
   1.533 -		  and thms2 = inst_pt_at_fs [abs_fun_supp]
   1.534 -		  and thms3 = inst_pt_pt_at_cp_dj [abs_fun_supp_ineq]
   1.535 -	      in [(("abs_supp", thms1 @ thms2 @ thms3),[])] end
   1.536 +                  and thms3 = inst_pt_pt_at_cp_dj [fresh_iff_ineq]
   1.537 +            in [(("abs_fresh", thms1 @ thms2 @ thms3),[])] end
   1.538 +            ||>> PureThy.add_thmss
   1.539 +              let val thms1 = inst_pt_at [abs_fun_supp]
   1.540 +                  and thms2 = inst_pt_at_fs [abs_fun_supp]
   1.541 +                  and thms3 = inst_pt_pt_at_cp_dj [abs_fun_supp_ineq]
   1.542 +              in [(("abs_supp", thms1 @ thms2 @ thms3),[])] end
   1.543              ||>> PureThy.add_thmss
   1.544 -	      let val thms1 = inst_pt_at [fresh_left]
   1.545 -		  and thms2 = inst_pt_pt_at_cp [fresh_left_ineq]
   1.546 -	      in [(("fresh_left", thms1 @ thms2),[])] end
   1.547 +              let val thms1 = inst_pt_at [fresh_left]
   1.548 +                  and thms2 = inst_pt_pt_at_cp [fresh_left_ineq]
   1.549 +              in [(("fresh_left", thms1 @ thms2),[])] end
   1.550              ||>> PureThy.add_thmss
   1.551 -	      let val thms1 = inst_pt_at [fresh_right]
   1.552 -		  and thms2 = inst_pt_pt_at_cp [fresh_right_ineq]
   1.553 -	      in [(("fresh_right", thms1 @ thms2),[])] end
   1.554 +              let val thms1 = inst_pt_at [fresh_right]
   1.555 +                  and thms2 = inst_pt_pt_at_cp [fresh_right_ineq]
   1.556 +              in [(("fresh_right", thms1 @ thms2),[])] end
   1.557              ||>> PureThy.add_thmss
   1.558 -	      let val thms1 = inst_pt_at [fresh_bij]
   1.559 - 		  and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq]
   1.560 -	      in [(("fresh_bij", thms1 @ thms2),[])] end
   1.561 +              let val thms1 = inst_pt_at [fresh_bij]
   1.562 +                  and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq]
   1.563 +              in [(("fresh_bij", thms1 @ thms2),[])] end
   1.564              ||>> PureThy.add_thmss
   1.565 -	      let val thms1 = inst_pt_at [fresh_eqvt]
   1.566 +              let val thms1 = inst_pt_at [fresh_eqvt]
   1.567                    and thms2 = inst_pt_pt_at_cp_dj [fresh_eqvt_ineq]
   1.568 -	      in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end
   1.569 +              in [(("fresh_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end
   1.570              ||>> PureThy.add_thmss
   1.571 -	      let val thms1 = inst_pt_at [in_eqvt]
   1.572 -	      in [(("in_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   1.573 -  	    ||>> PureThy.add_thmss
   1.574 -	      let val thms1 = inst_pt_at [eq_eqvt]
   1.575 -	      in [(("eq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   1.576 -	    ||>> PureThy.add_thmss
   1.577 -	      let val thms1 = inst_pt_at [set_diff_eqvt]
   1.578 -	      in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   1.579 +              let val thms1 = inst_pt_at [in_eqvt]
   1.580 +              in [(("in_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   1.581 +            ||>> PureThy.add_thmss
   1.582 +              let val thms1 = inst_pt_at [eq_eqvt]
   1.583 +              in [(("eq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   1.584              ||>> PureThy.add_thmss
   1.585 -	      let val thms1 = inst_pt_at [subseteq_eqvt]
   1.586 -	      in [(("subseteq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   1.587 +              let val thms1 = inst_pt_at [set_diff_eqvt]
   1.588 +              in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   1.589 +            ||>> PureThy.add_thmss
   1.590 +              let val thms1 = inst_pt_at [subseteq_eqvt]
   1.591 +              in [(("subseteq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
   1.592              ||>> PureThy.add_thmss
   1.593 -	      let val thms1 = inst_pt_at [fresh_aux]
   1.594 -		  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
   1.595 -	      in  [(("fresh_aux", thms1 @ thms2),[])] end  
   1.596 +              let val thms1 = inst_pt_at [fresh_aux]
   1.597 +                  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
   1.598 +              in  [(("fresh_aux", thms1 @ thms2),[])] end  
   1.599              ||>> PureThy.add_thmss
   1.600 -	      let val thms1 = inst_pt_at [fresh_perm_app]
   1.601 -		  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
   1.602 -	      in  [(("fresh_perm_app", thms1 @ thms2),[])] end 
   1.603 +              let val thms1 = inst_pt_at [fresh_perm_app]
   1.604 +                  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
   1.605 +              in  [(("fresh_perm_app", thms1 @ thms2),[])] end 
   1.606              ||>> PureThy.add_thmss
   1.607 -	      let val thms1 = inst_pt_at [pt_perm_supp]
   1.608 -		  and thms2 = inst_pt_pt_at_cp [pt_perm_supp_ineq] 
   1.609 -	      in  [(("supp_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end  
   1.610 +              let val thms1 = inst_pt_at [pt_perm_supp]
   1.611 +                  and thms2 = inst_pt_pt_at_cp [pt_perm_supp_ineq] 
   1.612 +              in  [(("supp_eqvt", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end  
   1.613              ||>> PureThy.add_thmss [(("fin_supp",fs_axs),[])]
   1.614 -	   end;
   1.615 +           end;
   1.616  
   1.617      in 
   1.618        NominalData.map (fold Symtab.update (full_ak_names ~~ map make_atom_info