src/HOL/Nominal/nominal_package.ML
changeset 30364 577edc39b501
parent 30345 76fd85bbf139
child 30450 7655e6533209
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -49,9 +49,9 @@
     1.4  
     1.5  fun dt_cases (descr: descr) (_, args, constrs) =
     1.6    let
     1.7 -    fun the_bname i = NameSpace.base_name (#1 (valOf (AList.lookup (op =) descr i)));
     1.8 +    fun the_bname i = Long_Name.base_name (#1 (valOf (AList.lookup (op =) descr i)));
     1.9      val bnames = map the_bname (distinct op = (List.concat (map dt_recs args)));
    1.10 -  in map (fn (c, _) => space_implode "_" (NameSpace.base_name c :: bnames)) constrs end;
    1.11 +  in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
    1.12  
    1.13  
    1.14  fun induct_cases descr =
    1.15 @@ -364,7 +364,7 @@
    1.16          val pi2 = Free ("pi2", permT);
    1.17          val pt_inst = pt_inst_of thy2 a;
    1.18          val pt2' = pt_inst RS pt2;
    1.19 -        val pt2_ax = PureThy.get_thm thy2 (NameSpace.map_base_name (fn s => "pt_" ^ s ^ "2") a);
    1.20 +        val pt2_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
    1.21        in List.take (map standard (split_conj_thm
    1.22          (Goal.prove_global thy2 [] []
    1.23             (augment_sort thy2 [pt_class_of thy2 a]
    1.24 @@ -399,7 +399,7 @@
    1.25          val pt_inst = pt_inst_of thy2 a;
    1.26          val pt3' = pt_inst RS pt3;
    1.27          val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
    1.28 -        val pt3_ax = PureThy.get_thm thy2 (NameSpace.map_base_name (fn s => "pt_" ^ s ^ "3") a);
    1.29 +        val pt3_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
    1.30        in List.take (map standard (split_conj_thm
    1.31          (Goal.prove_global thy2 [] []
    1.32            (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
    1.33 @@ -665,7 +665,7 @@
    1.34                asm_full_simp_tac (simpset_of thy addsimps
    1.35                  [Rep RS perm_closed RS Abs_inverse]) 1,
    1.36                asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
    1.37 -                ("pt_" ^ NameSpace.base_name atom ^ "3")]) 1]) thy
    1.38 +                ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy
    1.39            end)
    1.40          (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
    1.41             new_type_names ~~ tyvars ~~ perm_closed_thms);
    1.42 @@ -729,8 +729,8 @@
    1.43  
    1.44      (** strips the "_Rep" in type names *)
    1.45      fun strip_nth_name i s =
    1.46 -      let val xs = NameSpace.explode s;
    1.47 -      in NameSpace.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
    1.48 +      let val xs = Long_Name.explode s;
    1.49 +      in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
    1.50  
    1.51      val (descr'', ndescr) = ListPair.unzip (List.mapPartial
    1.52        (fn (i, ("Nominal.noption", _, _)) => NONE
    1.53 @@ -799,7 +799,7 @@
    1.54          val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs);
    1.55          val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.56            (Const (rep_name, T --> T') $ lhs, rhs));
    1.57 -        val def_name = (NameSpace.base_name cname) ^ "_def";
    1.58 +        val def_name = (Long_Name.base_name cname) ^ "_def";
    1.59          val ([def_thm], thy') = thy |>
    1.60            Sign.add_consts_i [(Binding.name cname', constrT, mx)] |>
    1.61            (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
    1.62 @@ -890,7 +890,7 @@
    1.63            map (fn ((cname, dts), constr_rep_thm) =>
    1.64          let
    1.65            val cname = Sign.intern_const thy8
    1.66 -            (NameSpace.append tname (NameSpace.base_name cname));
    1.67 +            (Long_Name.append tname (Long_Name.base_name cname));
    1.68            val permT = mk_permT (Type (atom, []));
    1.69            val pi = Free ("pi", permT);
    1.70  
    1.71 @@ -946,7 +946,7 @@
    1.72          if null dts then NONE else SOME
    1.73          let
    1.74            val cname = Sign.intern_const thy8
    1.75 -            (NameSpace.append tname (NameSpace.base_name cname));
    1.76 +            (Long_Name.append tname (Long_Name.base_name cname));
    1.77  
    1.78            fun make_inj ((dts, dt), (j, args1, args2, eqs)) =
    1.79              let
    1.80 @@ -988,7 +988,7 @@
    1.81        in List.concat (map (fn (cname, dts) => map (fn atom =>
    1.82          let
    1.83            val cname = Sign.intern_const thy8
    1.84 -            (NameSpace.append tname (NameSpace.base_name cname));
    1.85 +            (Long_Name.append tname (Long_Name.base_name cname));
    1.86            val atomT = Type (atom, []);
    1.87  
    1.88            fun process_constr ((dts, dt), (j, args1, args2)) =
    1.89 @@ -1101,7 +1101,7 @@
    1.90             (fn _ => indtac dt_induct indnames 1 THEN
    1.91              ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
    1.92                (abs_supp @ supp_atm @
    1.93 -               PureThy.get_thms thy8 ("fs_" ^ NameSpace.base_name atom ^ "1") @
    1.94 +               PureThy.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
    1.95                 List.concat supp_thms))))),
    1.96           length new_type_names))
    1.97        end) atoms;
    1.98 @@ -1233,9 +1233,9 @@
    1.99      val fin_set_fresh = map (fn s =>
   1.100        at_inst_of thy9 s RS at_fin_set_fresh) dt_atoms;
   1.101      val pt1_atoms = map (fn Type (s, _) =>
   1.102 -      PureThy.get_thm thy9 ("pt_" ^ NameSpace.base_name s ^ "1")) dt_atomTs;
   1.103 +      PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "1")) dt_atomTs;
   1.104      val pt2_atoms = map (fn Type (s, _) =>
   1.105 -      PureThy.get_thm thy9 ("pt_" ^ NameSpace.base_name s ^ "2") RS sym) dt_atomTs;
   1.106 +      PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "2") RS sym) dt_atomTs;
   1.107      val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'";
   1.108      val fs_atoms = PureThy.get_thms thy9 "fin_supp";
   1.109      val abs_supp = PureThy.get_thms thy9 "abs_supp";
   1.110 @@ -1514,7 +1514,7 @@
   1.111            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
   1.112            (map dest_Free rec_fns)
   1.113            (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
   1.114 -      PureThy.hide_fact true (NameSpace.append (Sign.full_bname thy10 big_rec_name) "induct");
   1.115 +      PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct");
   1.116  
   1.117      (** equivariance **)
   1.118  
   1.119 @@ -1560,7 +1560,7 @@
   1.120  
   1.121      val rec_fin_supp_thms = map (fn aT =>
   1.122        let
   1.123 -        val name = NameSpace.base_name (fst (dest_Type aT));
   1.124 +        val name = Long_Name.base_name (fst (dest_Type aT));
   1.125          val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
   1.126          val aset = HOLogic.mk_setT aT;
   1.127          val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
   1.128 @@ -1599,7 +1599,7 @@
   1.129  
   1.130      val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
   1.131        let
   1.132 -        val name = NameSpace.base_name (fst (dest_Type aT));
   1.133 +        val name = Long_Name.base_name (fst (dest_Type aT));
   1.134          val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
   1.135          val a = Free ("a", aT);
   1.136          val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
   1.137 @@ -2013,10 +2013,10 @@
   1.138      val (reccomb_defs, thy12) =
   1.139        thy11
   1.140        |> Sign.add_consts_i (map (fn ((name, T), T') =>
   1.141 -          (Binding.name (NameSpace.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
   1.142 +          (Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
   1.143            (reccomb_names ~~ recTs ~~ rec_result_Ts))
   1.144        |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
   1.145 -          (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
   1.146 +          (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
   1.147             Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
   1.148               set $ Free ("x", T) $ Free ("y", T'))))))
   1.149                 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));