src/HOL/Nominal/nominal_atoms.ML
changeset 26343 0dd2eab7b296
parent 26337 44473c957672
child 26398 fccb74555d9e
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Mar 19 22:50:42 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Mar 20 00:20:44 2008 +0100
     1.3 @@ -232,7 +232,7 @@
     1.4          val i_type = Type(ak_name_qu,[]);
     1.5          val cat = Const ("Nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
     1.6          val at_type = Logic.mk_type i_type;
     1.7 -        val simp_s = HOL_ss addsimps maps (dynamic_thms thy5)
     1.8 +        val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy5)
     1.9                                    ["at_def",
    1.10                                     ak_name ^ "_prm_" ^ ak_name ^ "_def",
    1.11                                     ak_name ^ "_prm_" ^ ak_name ^ ".simps",
    1.12 @@ -296,7 +296,7 @@
    1.13          val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    1.14          val pt_type = Logic.mk_type i_type1;
    1.15          val at_type = Logic.mk_type i_type2;
    1.16 -        val simp_s = HOL_ss addsimps maps (dynamic_thms thy7)
    1.17 +        val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy7)
    1.18                                    ["pt_def",
    1.19                                     "pt_" ^ ak_name ^ "1",
    1.20                                     "pt_" ^ ak_name ^ "2",
    1.21 @@ -343,7 +343,7 @@
    1.22                                   (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    1.23           val fs_type = Logic.mk_type i_type1;
    1.24           val at_type = Logic.mk_type i_type2;
    1.25 -         val simp_s = HOL_ss addsimps maps (dynamic_thms thy11)
    1.26 +         val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy11)
    1.27                                     ["fs_def",
    1.28                                      "fs_" ^ ak_name ^ "1"];
    1.29      
    1.30 @@ -395,8 +395,8 @@
    1.31               val at_type  = Logic.mk_type i_type1;
    1.32               val at_type' = Logic.mk_type i_type2;
    1.33               val cp_type  = Logic.mk_type i_type0;
    1.34 -             val simp_s   = HOL_basic_ss addsimps maps (dynamic_thms thy') ["cp_def"];
    1.35 -             val cp1      = dynamic_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1");
    1.36 +             val simp_s   = HOL_basic_ss addsimps maps (PureThy.get_thms thy') ["cp_def"];
    1.37 +             val cp1      = PureThy.get_thm thy' ("cp_" ^ ak_name ^ "_" ^ ak_name' ^ "1");
    1.38  
    1.39               val name = "cp_"^ak_name^ "_"^ak_name'^"_inst";
    1.40               val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type');
    1.41 @@ -426,7 +426,7 @@
    1.42                             (Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    1.43                   val at_type  = Logic.mk_type i_type1;
    1.44                   val at_type' = Logic.mk_type i_type2;
    1.45 -                 val simp_s = HOL_ss addsimps maps (dynamic_thms thy')
    1.46 +                 val simp_s = HOL_ss addsimps maps (PureThy.get_thms thy')
    1.47                                             ["disjoint_def",
    1.48                                              ak_name ^ "_prm_" ^ ak_name' ^ "_def",
    1.49                                              ak_name' ^ "_prm_" ^ ak_name ^ "_def"];
    1.50 @@ -466,7 +466,7 @@
    1.51           let
    1.52             val qu_name =  Sign.full_name thy' ak_name';
    1.53             val cls_name = Sign.full_name thy' ("pt_"^ak_name);
    1.54 -           val at_inst  = dynamic_thm thy' ("at_" ^ ak_name' ^ "_inst");
    1.55 +           val at_inst  = PureThy.get_thm thy' ("at_" ^ ak_name' ^ "_inst");
    1.56  
    1.57             val proof1 = EVERY [Class.intro_classes_tac [],
    1.58                                   rtac ((at_inst RS at_pt_inst) RS pt1) 1,
    1.59 @@ -474,7 +474,7 @@
    1.60                                   rtac ((at_inst RS at_pt_inst) RS pt3) 1,
    1.61                                   atac 1];
    1.62             val simp_s = HOL_basic_ss addsimps 
    1.63 -                        maps (dynamic_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"];  
    1.64 +                        maps (PureThy.get_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"];  
    1.65             val proof2 = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
    1.66  
    1.67           in
    1.68 @@ -496,8 +496,8 @@
    1.69       val thy18 = fold (fn ak_name => fn thy =>
    1.70         let
    1.71            val cls_name = Sign.full_name thy ("pt_"^ak_name);
    1.72 -          val at_thm   = dynamic_thm thy ("at_"^ak_name^"_inst");
    1.73 -          val pt_inst  = dynamic_thm thy ("pt_"^ak_name^"_inst");
    1.74 +          val at_thm   = PureThy.get_thm thy ("at_"^ak_name^"_inst");
    1.75 +          val pt_inst  = PureThy.get_thm thy ("pt_"^ak_name^"_inst");
    1.76  
    1.77            fun pt_proof thm = 
    1.78                EVERY [Class.intro_classes_tac [],
    1.79 @@ -546,11 +546,11 @@
    1.80             val proof =
    1.81                 (if ak_name = ak_name'
    1.82                  then
    1.83 -                  let val at_thm = dynamic_thm thy' ("at_"^ak_name^"_inst");
    1.84 +                  let val at_thm = PureThy.get_thm thy' ("at_"^ak_name^"_inst");
    1.85                    in  EVERY [Class.intro_classes_tac [],
    1.86                               rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
    1.87                  else
    1.88 -                  let val dj_inst = dynamic_thm thy' ("dj_"^ak_name'^"_"^ak_name);
    1.89 +                  let val dj_inst = PureThy.get_thm thy' ("dj_"^ak_name'^"_"^ak_name);
    1.90                        val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI];
    1.91                    in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end)
    1.92          in
    1.93 @@ -568,7 +568,7 @@
    1.94         val thy24 = fold (fn ak_name => fn thy => 
    1.95          let
    1.96            val cls_name = Sign.full_name thy ("fs_"^ak_name);
    1.97 -          val fs_inst  = dynamic_thm thy ("fs_"^ak_name^"_inst");
    1.98 +          val fs_inst  = PureThy.get_thm thy ("fs_"^ak_name^"_inst");
    1.99            fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1];
   1.100  
   1.101            val fs_thm_unit  = fs_unit_inst;
   1.102 @@ -613,18 +613,18 @@
   1.103                val proof =
   1.104                  (if (ak_name'=ak_name'') then 
   1.105                    (let
   1.106 -                    val pt_inst  = dynamic_thm thy'' ("pt_"^ak_name''^"_inst");
   1.107 -                    val at_inst  = dynamic_thm thy'' ("at_"^ak_name''^"_inst");
   1.108 +                    val pt_inst  = PureThy.get_thm thy'' ("pt_"^ak_name''^"_inst");
   1.109 +                    val at_inst  = PureThy.get_thm thy'' ("at_"^ak_name''^"_inst");
   1.110                    in
   1.111                     EVERY [Class.intro_classes_tac [],
   1.112                            rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]
   1.113                    end)
   1.114                  else
   1.115                    (let
   1.116 -                     val dj_inst  = dynamic_thm thy'' ("dj_"^ak_name''^"_"^ak_name');
   1.117 +                     val dj_inst  = PureThy.get_thm thy'' ("dj_"^ak_name''^"_"^ak_name');
   1.118                       val simp_s = HOL_basic_ss addsimps
   1.119                                          ((dj_inst RS dj_pp_forget)::
   1.120 -                                         (maps (dynamic_thms thy'')
   1.121 +                                         (maps (PureThy.get_thms thy'')
   1.122                                             [ak_name' ^"_prm_"^ak_name^"_def",
   1.123                                              ak_name''^"_prm_"^ak_name^"_def"]));
   1.124                    in
   1.125 @@ -647,9 +647,9 @@
   1.126          fold (fn ak_name' => fn thy' =>
   1.127          let
   1.128              val cls_name = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name');
   1.129 -            val cp_inst  = dynamic_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst");
   1.130 -            val pt_inst  = dynamic_thm thy' ("pt_"^ak_name^"_inst");
   1.131 -            val at_inst  = dynamic_thm thy' ("at_"^ak_name^"_inst");
   1.132 +            val cp_inst  = PureThy.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst");
   1.133 +            val pt_inst  = PureThy.get_thm thy' ("pt_"^ak_name^"_inst");
   1.134 +            val at_inst  = PureThy.get_thm thy' ("at_"^ak_name^"_inst");
   1.135  
   1.136              fun cp_proof thm  = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1];
   1.137            
   1.138 @@ -804,27 +804,27 @@
   1.139  
   1.140               
   1.141               (* list of all at_inst-theorems *)
   1.142 -             val ats = map (fn ak => dynamic_thm thy32 ("at_"^ak^"_inst")) ak_names
   1.143 +             val ats = map (fn ak => PureThy.get_thm thy32 ("at_"^ak^"_inst")) ak_names
   1.144               (* list of all pt_inst-theorems *)
   1.145 -             val pts = map (fn ak => dynamic_thm thy32 ("pt_"^ak^"_inst")) ak_names
   1.146 +             val pts = map (fn ak => PureThy.get_thm thy32 ("pt_"^ak^"_inst")) ak_names
   1.147               (* list of all cp_inst-theorems as a collection of lists*)
   1.148               val cps = 
   1.149 -                 let fun cps_fun ak1 ak2 =  dynamic_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")
   1.150 +                 let fun cps_fun ak1 ak2 =  PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst")
   1.151                   in map (fn aki => (map (cps_fun aki) ak_names)) ak_names end; 
   1.152               (* list of all cp_inst-theorems that have different atom types *)
   1.153               val cps' = 
   1.154                  let fun cps'_fun ak1 ak2 = 
   1.155 -                if ak1=ak2 then NONE else SOME (dynamic_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst"))
   1.156 +                if ak1=ak2 then NONE else SOME (PureThy.get_thm thy32 ("cp_"^ak1^"_"^ak2^"_inst"))
   1.157                  in map (fn aki => (List.mapPartial I (map (cps'_fun aki) ak_names))) ak_names end;
   1.158               (* list of all dj_inst-theorems *)
   1.159               val djs = 
   1.160                 let fun djs_fun ak1 ak2 = 
   1.161 -                     if ak1=ak2 then NONE else SOME(dynamic_thm thy32 ("dj_"^ak2^"_"^ak1))
   1.162 +                     if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 ("dj_"^ak2^"_"^ak1))
   1.163                 in map_filter I (map_product djs_fun ak_names ak_names) end;
   1.164               (* list of all fs_inst-theorems *)
   1.165 -             val fss = map (fn ak => dynamic_thm thy32 ("fs_"^ak^"_inst")) ak_names
   1.166 +             val fss = map (fn ak => PureThy.get_thm thy32 ("fs_"^ak^"_inst")) ak_names
   1.167               (* list of all at_inst-theorems *)
   1.168 -             val fs_axs = map (fn ak => dynamic_thm thy32 ("fs_"^ak^"1")) ak_names
   1.169 +             val fs_axs = map (fn ak => PureThy.get_thm thy32 ("fs_"^ak^"1")) ak_names
   1.170  
   1.171               fun inst_pt thms = maps (fn ti => instR ti pts) thms;
   1.172               fun inst_at thms = maps (fn ti => instR ti ats) thms;