src/HOL/Nominal/nominal_package.ML
changeset 26343 0dd2eab7b296
parent 26337 44473c957672
child 26359 6d437bde2f1d
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Mar 19 22:50:42 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Mar 20 00:20:44 2008 +0100
     1.3 @@ -140,8 +140,8 @@
     1.4            let
     1.5              val a' = Sign.base_name a;
     1.6              val b' = Sign.base_name b;
     1.7 -            val cp = dynamic_thm thy ("cp_" ^ a' ^ "_" ^ b' ^ "_inst");
     1.8 -            val dj = dynamic_thm thy ("dj_" ^ b' ^ "_" ^ a');
     1.9 +            val cp = PureThy.get_thm thy ("cp_" ^ a' ^ "_" ^ b' ^ "_inst");
    1.10 +            val dj = PureThy.get_thm thy ("dj_" ^ b' ^ "_" ^ a');
    1.11              val dj_cp' = [cp, dj] MRS dj_cp;
    1.12              val cert = SOME o cterm_of thy
    1.13            in
    1.14 @@ -309,7 +309,7 @@
    1.15      val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
    1.16  
    1.17      val perm_indnames = DatatypeProp.make_tnames (map body_type perm_types);
    1.18 -    val perm_fun_def = dynamic_thm thy2 "perm_fun_def";
    1.19 +    val perm_fun_def = PureThy.get_thm thy2 "perm_fun_def";
    1.20  
    1.21      val unfolded_perm_eq_thms =
    1.22        if length descr = length new_type_names then []
    1.23 @@ -353,17 +353,17 @@
    1.24      val _ = warning "perm_append_thms";
    1.25  
    1.26      (*FIXME: these should be looked up statically*)
    1.27 -    val at_pt_inst = dynamic_thm thy2 "at_pt_inst";
    1.28 -    val pt2 = dynamic_thm thy2 "pt2";
    1.29 +    val at_pt_inst = PureThy.get_thm thy2 "at_pt_inst";
    1.30 +    val pt2 = PureThy.get_thm thy2 "pt2";
    1.31  
    1.32      val perm_append_thms = List.concat (map (fn a =>
    1.33        let
    1.34          val permT = mk_permT (Type (a, []));
    1.35          val pi1 = Free ("pi1", permT);
    1.36          val pi2 = Free ("pi2", permT);
    1.37 -        val pt_inst = dynamic_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
    1.38 +        val pt_inst = PureThy.get_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
    1.39          val pt2' = pt_inst RS pt2;
    1.40 -        val pt2_ax = dynamic_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a);
    1.41 +        val pt2_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a);
    1.42        in List.take (map standard (split_conj_thm
    1.43          (Goal.prove_global thy2 [] []
    1.44               (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.45 @@ -385,8 +385,8 @@
    1.46  
    1.47      val _ = warning "perm_eq_thms";
    1.48  
    1.49 -    val pt3 = dynamic_thm thy2 "pt3";
    1.50 -    val pt3_rev = dynamic_thm thy2 "pt3_rev";
    1.51 +    val pt3 = PureThy.get_thm thy2 "pt3";
    1.52 +    val pt3_rev = PureThy.get_thm thy2 "pt3_rev";
    1.53  
    1.54      val perm_eq_thms = List.concat (map (fn a =>
    1.55        let
    1.56 @@ -394,11 +394,11 @@
    1.57          val pi1 = Free ("pi1", permT);
    1.58          val pi2 = Free ("pi2", permT);
    1.59          (*FIXME: not robust - better access these theorems using NominalData?*)
    1.60 -        val at_inst = dynamic_thm thy2 ("at_" ^ Sign.base_name a ^ "_inst");
    1.61 -        val pt_inst = dynamic_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
    1.62 +        val at_inst = PureThy.get_thm thy2 ("at_" ^ Sign.base_name a ^ "_inst");
    1.63 +        val pt_inst = PureThy.get_thm thy2 ("pt_" ^ Sign.base_name a ^ "_inst");
    1.64          val pt3' = pt_inst RS pt3;
    1.65          val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
    1.66 -        val pt3_ax = dynamic_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a);
    1.67 +        val pt3_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a);
    1.68        in List.take (map standard (split_conj_thm
    1.69          (Goal.prove_global thy2 [] [] (Logic.mk_implies
    1.70               (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
    1.71 @@ -419,11 +419,11 @@
    1.72  
    1.73      (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
    1.74  
    1.75 -    val cp1 = dynamic_thm thy2 "cp1";
    1.76 -    val dj_cp = dynamic_thm thy2 "dj_cp";
    1.77 -    val pt_perm_compose = dynamic_thm thy2 "pt_perm_compose";
    1.78 -    val pt_perm_compose_rev = dynamic_thm thy2 "pt_perm_compose_rev";
    1.79 -    val dj_perm_perm_forget = dynamic_thm thy2 "dj_perm_perm_forget";
    1.80 +    val cp1 = PureThy.get_thm thy2 "cp1";
    1.81 +    val dj_cp = PureThy.get_thm thy2 "dj_cp";
    1.82 +    val pt_perm_compose = PureThy.get_thm thy2 "pt_perm_compose";
    1.83 +    val pt_perm_compose_rev = PureThy.get_thm thy2 "pt_perm_compose_rev";
    1.84 +    val dj_perm_perm_forget = PureThy.get_thm thy2 "dj_perm_perm_forget";
    1.85  
    1.86      fun composition_instance name1 name2 thy =
    1.87        let
    1.88 @@ -435,15 +435,15 @@
    1.89          val augment = map_type_tfree
    1.90            (fn (x, S) => TFree (x, cp_class :: S));
    1.91          val Ts = map (augment o body_type) perm_types;
    1.92 -        val cp_inst = dynamic_thm thy ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst");
    1.93 +        val cp_inst = PureThy.get_thm thy ("cp_" ^ name1' ^ "_" ^ name2' ^ "_inst");
    1.94          val simps = simpset_of thy addsimps (perm_fun_def ::
    1.95            (if name1 <> name2 then
    1.96 -             let val dj = dynamic_thm thy ("dj_" ^ name2' ^ "_" ^ name1')
    1.97 +             let val dj = PureThy.get_thm thy ("dj_" ^ name2' ^ "_" ^ name1')
    1.98               in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
    1.99             else
   1.100               let
   1.101 -               val at_inst = dynamic_thm thy ("at_" ^ name1' ^ "_inst");
   1.102 -               val pt_inst = dynamic_thm thy ("pt_" ^ name1' ^ "_inst");
   1.103 +               val at_inst = PureThy.get_thm thy ("at_" ^ name1' ^ "_inst");
   1.104 +               val pt_inst = PureThy.get_thm thy ("pt_" ^ name1' ^ "_inst");
   1.105               in
   1.106                 [cp_inst RS cp1 RS sym,
   1.107                  at_inst RS (pt_inst RS pt_perm_compose) RS sym,
   1.108 @@ -571,7 +571,7 @@
   1.109  
   1.110      val _ = warning "proving closure under permutation...";
   1.111  
   1.112 -    val abs_perm = dynamic_thms thy4 "abs_perm";
   1.113 +    val abs_perm = PureThy.get_thms thy4 "abs_perm";
   1.114  
   1.115      val perm_indnames' = List.mapPartial
   1.116        (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
   1.117 @@ -656,7 +656,7 @@
   1.118                asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
   1.119                asm_full_simp_tac (simpset_of thy addsimps
   1.120                  [Rep RS perm_closed RS Abs_inverse]) 1,
   1.121 -              asm_full_simp_tac (HOL_basic_ss addsimps [dynamic_thm thy
   1.122 +              asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
   1.123                  ("pt_" ^ Sign.base_name atom ^ "3")]) 1]) thy)
   1.124          (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
   1.125             new_type_names ~~ tyvars ~~ perm_closed_thms);
   1.126 @@ -670,7 +670,7 @@
   1.127        let
   1.128          val name = "cp_" ^ Sign.base_name atom1 ^ "_" ^ Sign.base_name atom2;
   1.129          val class = Sign.intern_class thy name;
   1.130 -        val cp1' = dynamic_thm thy (name ^ "_inst") RS cp1
   1.131 +        val cp1' = PureThy.get_thm thy (name ^ "_inst") RS cp1
   1.132        in fold (fn ((((((Abs_inverse, Rep),
   1.133          perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
   1.134            AxClass.prove_arity
   1.135 @@ -920,8 +920,8 @@
   1.136      (** prove injectivity of constructors **)
   1.137  
   1.138      val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
   1.139 -    val alpha = dynamic_thms thy8 "alpha";
   1.140 -    val abs_fresh = dynamic_thms thy8 "abs_fresh";
   1.141 +    val alpha = PureThy.get_thms thy8 "alpha";
   1.142 +    val abs_fresh = PureThy.get_thms thy8 "abs_fresh";
   1.143  
   1.144      val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
   1.145        let val T = nth_dtyp' i
   1.146 @@ -1066,8 +1066,8 @@
   1.147  
   1.148      val indnames = DatatypeProp.make_tnames recTs;
   1.149  
   1.150 -    val abs_supp = dynamic_thms thy8 "abs_supp";
   1.151 -    val supp_atm = dynamic_thms thy8 "supp_atm";
   1.152 +    val abs_supp = PureThy.get_thms thy8 "abs_supp";
   1.153 +    val supp_atm = PureThy.get_thms thy8 "supp_atm";
   1.154  
   1.155      val finite_supp_thms = map (fn atom =>
   1.156        let val atomT = Type (atom, [])
   1.157 @@ -1080,7 +1080,7 @@
   1.158             (fn _ => indtac dt_induct indnames 1 THEN
   1.159              ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
   1.160                (abs_supp @ supp_atm @
   1.161 -               dynamic_thms thy8 ("fs_" ^ Sign.base_name atom ^ "1") @
   1.162 +               PureThy.get_thms thy8 ("fs_" ^ Sign.base_name atom ^ "1") @
   1.163                 List.concat supp_thms))))),
   1.164           length new_type_names))
   1.165        end) atoms;
   1.166 @@ -1207,23 +1207,23 @@
   1.167          (descr'' ~~ recTs ~~ tnames)));
   1.168  
   1.169      val fin_set_supp = map (fn Type (s, _) =>
   1.170 -      dynamic_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
   1.171 +      PureThy.get_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
   1.172          at_fin_set_supp) dt_atomTs;
   1.173      val fin_set_fresh = map (fn Type (s, _) =>
   1.174 -      dynamic_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
   1.175 +      PureThy.get_thm thy9 ("at_" ^ Sign.base_name s ^ "_inst") RS
   1.176          at_fin_set_fresh) dt_atomTs;
   1.177      val pt1_atoms = map (fn Type (s, _) =>
   1.178 -      dynamic_thm thy9 ("pt_" ^ Sign.base_name s ^ "1")) dt_atomTs;
   1.179 +      PureThy.get_thm thy9 ("pt_" ^ Sign.base_name s ^ "1")) dt_atomTs;
   1.180      val pt2_atoms = map (fn Type (s, _) =>
   1.181 -      dynamic_thm thy9 ("pt_" ^ Sign.base_name s ^ "2") RS sym) dt_atomTs;
   1.182 -    val exists_fresh' = dynamic_thms thy9 "exists_fresh'";
   1.183 -    val fs_atoms = dynamic_thms thy9 "fin_supp";
   1.184 -    val abs_supp = dynamic_thms thy9 "abs_supp";
   1.185 -    val perm_fresh_fresh = dynamic_thms thy9 "perm_fresh_fresh";
   1.186 -    val calc_atm = dynamic_thms thy9 "calc_atm";
   1.187 -    val fresh_atm = dynamic_thms thy9 "fresh_atm";
   1.188 -    val fresh_left = dynamic_thms thy9 "fresh_left";
   1.189 -    val perm_swap = dynamic_thms thy9 "perm_swap";
   1.190 +      PureThy.get_thm thy9 ("pt_" ^ Sign.base_name s ^ "2") RS sym) dt_atomTs;
   1.191 +    val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'";
   1.192 +    val fs_atoms = PureThy.get_thms thy9 "fin_supp";
   1.193 +    val abs_supp = PureThy.get_thms thy9 "abs_supp";
   1.194 +    val perm_fresh_fresh = PureThy.get_thms thy9 "perm_fresh_fresh";
   1.195 +    val calc_atm = PureThy.get_thms thy9 "calc_atm";
   1.196 +    val fresh_atm = PureThy.get_thms thy9 "fresh_atm";
   1.197 +    val fresh_left = PureThy.get_thms thy9 "fresh_left";
   1.198 +    val perm_swap = PureThy.get_thms thy9 "perm_swap";
   1.199  
   1.200      fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) =
   1.201        let
   1.202 @@ -1496,8 +1496,8 @@
   1.203  
   1.204      (** equivariance **)
   1.205  
   1.206 -    val fresh_bij = dynamic_thms thy11 "fresh_bij";
   1.207 -    val perm_bij = dynamic_thms thy11 "perm_bij";
   1.208 +    val fresh_bij = PureThy.get_thms thy11 "fresh_bij";
   1.209 +    val perm_bij = PureThy.get_thms thy11 "perm_bij";
   1.210  
   1.211      val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT =>
   1.212        let
   1.213 @@ -1535,7 +1535,7 @@
   1.214      val rec_fin_supp_thms = map (fn aT =>
   1.215        let
   1.216          val name = Sign.base_name (fst (dest_Type aT));
   1.217 -        val fs_name = dynamic_thm thy11 ("fs_" ^ name ^ "1");
   1.218 +        val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
   1.219          val aset = HOLogic.mk_setT aT;
   1.220          val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
   1.221          val fins = map (fn (f, T) => HOLogic.mk_Trueprop
   1.222 @@ -1568,7 +1568,7 @@
   1.223      val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
   1.224        let
   1.225          val name = Sign.base_name (fst (dest_Type aT));
   1.226 -        val fs_name = dynamic_thm thy11 ("fs_" ^ name ^ "1");
   1.227 +        val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
   1.228          val a = Free ("a", aT);
   1.229          val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
   1.230            (fresh_const aT fT $ a $ f)) (rec_fns ~~ rec_fn_Ts)