src/HOL/Nominal/nominal_package.ML
changeset 19494 2e909d5309f4
parent 19489 4441b637871b
child 19635 f7aa7d174343
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Fri Apr 28 15:53:47 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Fri Apr 28 15:54:34 2006 +0200
     1.3 @@ -1,4 +1,9 @@
     1.4 -(* $Id$ *)
     1.5 +(*  Title:      HOL/Nominal/nominal_package.ML
     1.6 +    ID:         $Id$
     1.7 +    Author:     Stefan Berghofer and Christian Urban, TU Muenchen
     1.8 +
     1.9 +Nominal datatype package for Isabelle/HOL.
    1.10 +*)
    1.11  
    1.12  signature NOMINAL_PACKAGE =
    1.13  sig
    1.14 @@ -97,10 +102,10 @@
    1.15  fun dest_permT (Type ("fun", [Type ("List.list", [Type ("*", [T, _])]),
    1.16        Type ("fun", [_, U])])) = (T, U);
    1.17  
    1.18 -fun permTs_of (Const ("nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
    1.19 +fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
    1.20    | permTs_of _ = [];
    1.21  
    1.22 -fun perm_simproc' thy ss (Const ("nominal.perm", T) $ t $ (u as Const ("nominal.perm", U) $ r $ s)) =
    1.23 +fun perm_simproc' thy ss (Const ("Nominal.perm", T) $ t $ (u as Const ("Nominal.perm", U) $ r $ s)) =
    1.24        let
    1.25          val (aT as Type (a, []), S) = dest_permT T;
    1.26          val (bT as Type (b, []), _) = dest_permT U
    1.27 @@ -172,8 +177,8 @@
    1.28        (Sign.full_name sign n, Sign.full_name sign (n ^ "_Rep"))) dts;
    1.29      val rps = map Library.swap ps;
    1.30  
    1.31 -    fun replace_types (Type ("nominal.ABS", [T, U])) = 
    1.32 -          Type ("fun", [T, Type ("nominal.noption", [replace_types U])])
    1.33 +    fun replace_types (Type ("Nominal.ABS", [T, U])) = 
    1.34 +          Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
    1.35        | replace_types (Type (s, Ts)) =
    1.36            Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
    1.37        | replace_types T = T;
    1.38 @@ -203,7 +208,7 @@
    1.39      val perm_types = map (fn (i, _) =>
    1.40        let val T = nth_dtyp i
    1.41        in permT --> T --> T end) descr;
    1.42 -    val perm_names = replicate (length new_type_names) "nominal.perm" @
    1.43 +    val perm_names = replicate (length new_type_names) "Nominal.perm" @
    1.44        DatatypeProp.indexify_names (map (fn i => Sign.full_name (sign_of thy1)
    1.45          ("perm_" ^ name_of_typ (nth_dtyp i)))
    1.46            (length new_type_names upto length descr - 1));
    1.47 @@ -224,11 +229,11 @@
    1.48                  in list_abs (map (pair "x") Us,
    1.49                    Const (List.nth (perm_names_types, body_index dt)) $ pi $
    1.50                      list_comb (x, map (fn (i, U) =>
    1.51 -                      Const ("nominal.perm", permT --> U --> U) $
    1.52 +                      Const ("Nominal.perm", permT --> U --> U) $
    1.53                          (Const ("List.rev", permT --> permT) $ pi) $
    1.54                          Bound i) ((length Us - 1 downto 0) ~~ Us)))
    1.55                  end
    1.56 -              else Const ("nominal.perm", permT --> T --> T) $ pi $ x
    1.57 +              else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
    1.58              end;  
    1.59          in
    1.60            (("", HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.61 @@ -261,7 +266,7 @@
    1.62              (map (fn (c as (s, T), x) =>
    1.63                 let val [T1, T2] = binder_types T
    1.64                 in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
    1.65 -                 Const ("nominal.perm", T) $ pi $ Free (x, T2))
    1.66 +                 Const ("Nominal.perm", T) $ pi $ Free (x, T2))
    1.67                 end)
    1.68               (perm_names_types ~~ perm_indnames))))
    1.69            (fn _ => EVERY [indtac induction perm_indnames 1,
    1.70 @@ -345,7 +350,7 @@
    1.71            (Name (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a));
    1.72        in List.take (map standard (split_conj_thm
    1.73          (Goal.prove thy2 [] [] (Logic.mk_implies
    1.74 -             (HOLogic.mk_Trueprop (Const ("nominal.prm_eq",
    1.75 +             (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
    1.76                  permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
    1.77                HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.78                  (map (fn ((s, T), x) =>
    1.79 @@ -402,7 +407,7 @@
    1.80                      val pi2 = Free ("pi2", permT2);
    1.81                      val perm1 = Const (s, permT1 --> T --> T);
    1.82                      val perm2 = Const (s, permT2 --> T --> T);
    1.83 -                    val perm3 = Const ("nominal.perm", permT1 --> permT2 --> permT2)
    1.84 +                    val perm3 = Const ("Nominal.perm", permT1 --> permT2 --> permT2)
    1.85                    in HOLogic.mk_eq
    1.86                      (perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
    1.87                       perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
    1.88 @@ -444,16 +449,16 @@
    1.89        (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr));
    1.90      val big_rep_name =
    1.91        space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
    1.92 -        (fn (i, ("nominal.noption", _, _)) => NONE
    1.93 +        (fn (i, ("Nominal.noption", _, _)) => NONE
    1.94            | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
    1.95      val _ = warning ("big_rep_name: " ^ big_rep_name);
    1.96  
    1.97      fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
    1.98            (case AList.lookup op = descr i of
    1.99 -             SOME ("nominal.noption", _, [(_, [dt']), _]) =>
   1.100 +             SOME ("Nominal.noption", _, [(_, [dt']), _]) =>
   1.101                 apfst (cons dt) (strip_option dt')
   1.102             | _ => ([], dtf))
   1.103 -      | strip_option (DtType ("fun", [dt, DtType ("nominal.noption", [dt'])])) =
   1.104 +      | strip_option (DtType ("fun", [dt, DtType ("Nominal.noption", [dt'])])) =
   1.105            apfst (cons dt) (strip_option dt')
   1.106        | strip_option dt = ([], dt);
   1.107  
   1.108 @@ -474,8 +479,8 @@
   1.109              val free' = app_bnds free (length Us);
   1.110              fun mk_abs_fun (T, (i, t)) =
   1.111                let val U = fastype_of t
   1.112 -              in (i + 1, Const ("nominal.abs_fun", [T, U, T] --->
   1.113 -                Type ("nominal.noption", [U])) $ mk_Free "y" T i $ t)
   1.114 +              in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
   1.115 +                Type ("Nominal.noption", [U])) $ mk_Free "y" T i $ t)
   1.116                end
   1.117            in (j + 1, j' + length Ts,
   1.118              case dt'' of
   1.119 @@ -496,7 +501,7 @@
   1.120  
   1.121      val (intr_ts, ind_consts) =
   1.122        apfst List.concat (ListPair.unzip (List.mapPartial
   1.123 -        (fn ((_, ("nominal.noption", _, _)), _) => NONE
   1.124 +        (fn ((_, ("Nominal.noption", _, _)), _) => NONE
   1.125            | ((i, (_, _, constrs)), rep_set_name) =>
   1.126                let val T = nth_dtyp i
   1.127                in SOME (map (make_intr rep_set_name T) constrs,
   1.128 @@ -514,7 +519,7 @@
   1.129      val _ = warning "proving closure under permutation...";
   1.130  
   1.131      val perm_indnames' = List.mapPartial
   1.132 -      (fn (x, (_, ("nominal.noption", _, _))) => NONE | (x, _) => SOME x)
   1.133 +      (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
   1.134        (perm_indnames ~~ descr);
   1.135  
   1.136      fun mk_perm_closed name = map (fn th => standard (th RS mp))
   1.137 @@ -527,7 +532,7 @@
   1.138                  val T = HOLogic.dest_setT (fastype_of S);
   1.139                  val permT = mk_permT (Type (name, []))
   1.140                in HOLogic.mk_imp (HOLogic.mk_mem (Free (x, T), S),
   1.141 -                HOLogic.mk_mem (Const ("nominal.perm", permT --> T --> T) $
   1.142 +                HOLogic.mk_mem (Const ("Nominal.perm", permT --> T --> T) $
   1.143                    Free ("pi", permT) $ Free (x, T), S))
   1.144                end) (ind_consts ~~ perm_indnames'))))
   1.145          (fn _ => EVERY (* CU: added perm_fun_def in the final tactic in order to deal with funs *)
   1.146 @@ -561,9 +566,9 @@
   1.147            val Const (_, Type (_, [U])) = c
   1.148          in apfst (pair r o hd)
   1.149            (PureThy.add_defs_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
   1.150 -            (Const ("nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
   1.151 +            (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
   1.152               Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
   1.153 -               (Const ("nominal.perm", permT --> U --> U) $ pi $
   1.154 +               (Const ("Nominal.perm", permT --> U --> U) $ pi $
   1.155                   (Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $
   1.156                     Free ("x", T))))), [])] thy)
   1.157          end))
   1.158 @@ -637,12 +642,12 @@
   1.159          val T = fastype_of x;
   1.160          val U = fastype_of t
   1.161        in
   1.162 -        Const ("nominal.abs_fun", T --> U --> T -->
   1.163 -          Type ("nominal.noption", [U])) $ x $ t
   1.164 +        Const ("Nominal.abs_fun", T --> U --> T -->
   1.165 +          Type ("Nominal.noption", [U])) $ x $ t
   1.166        end;
   1.167  
   1.168      val (ty_idxs, _) = foldl
   1.169 -      (fn ((i, ("nominal.noption", _, _)), p) => p
   1.170 +      (fn ((i, ("Nominal.noption", _, _)), p) => p
   1.171          | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
   1.172  
   1.173      fun reindex (DtType (s, dts)) = DtType (s, map reindex dts)
   1.174 @@ -657,7 +662,7 @@
   1.175        in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
   1.176  
   1.177      val (descr'', ndescr) = ListPair.unzip (List.mapPartial
   1.178 -      (fn (i, ("nominal.noption", _, _)) => NONE
   1.179 +      (fn (i, ("Nominal.noption", _, _)) => NONE
   1.180          | (i, (s, dts, constrs)) =>
   1.181               let
   1.182                 val SOME index = AList.lookup op = ty_idxs i;
   1.183 @@ -682,7 +687,7 @@
   1.184        Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
   1.185  
   1.186      val recTs' = List.mapPartial
   1.187 -      (fn ((_, ("nominal.noption", _, _)), T) => NONE
   1.188 +      (fn ((_, ("Nominal.noption", _, _)), T) => NONE
   1.189          | (_, T) => SOME T) (descr ~~ get_rec_types descr sorts');
   1.190      val recTs = get_rec_types descr'' sorts';
   1.191      val newTs' = Library.take (length new_type_names, recTs');
   1.192 @@ -783,8 +788,8 @@
   1.193          val pi = Free ("pi", permT);
   1.194        in
   1.195          standard (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.196 -            (Const ("nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
   1.197 -             Rep $ (Const ("nominal.perm", permT --> T --> T) $ pi $ x))))
   1.198 +            (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
   1.199 +             Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x))))
   1.200            (fn _ => simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @
   1.201              perm_closed_thms @ Rep_thms)) 1))
   1.202        end) Rep_thms;
   1.203 @@ -829,7 +834,7 @@
   1.204  
   1.205            fun perm t =
   1.206              let val T = fastype_of t
   1.207 -            in Const ("nominal.perm", permT --> T --> T) $ pi $ t end;
   1.208 +            in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
   1.209  
   1.210            fun constr_arg (dt, (j, l_args, r_args)) =
   1.211              let
   1.212 @@ -949,9 +954,9 @@
   1.213            val Ts = map fastype_of args1;
   1.214            val c = list_comb (Const (cname, Ts ---> T), args1);
   1.215            fun supp t =
   1.216 -            Const ("nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
   1.217 +            Const ("Nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
   1.218            fun fresh t =
   1.219 -            Const ("nominal.fresh", atomT --> fastype_of t --> HOLogic.boolT) $
   1.220 +            Const ("Nominal.fresh", atomT --> fastype_of t --> HOLogic.boolT) $
   1.221                Free ("a", atomT) $ t;
   1.222            val supp_thm = standard (Goal.prove thy8 [] []
   1.223                (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.224 @@ -1060,7 +1065,7 @@
   1.225        in map standard (List.take
   1.226          (split_conj_thm (Goal.prove thy8 [] [] (HOLogic.mk_Trueprop
   1.227             (foldr1 HOLogic.mk_conj (map (fn (s, T) => HOLogic.mk_mem
   1.228 -             (Const ("nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T),
   1.229 +             (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T),
   1.230                Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT atomT))))
   1.231                 (indnames ~~ recTs))))
   1.232             (fn _ => indtac dt_induct indnames 1 THEN
   1.233 @@ -1139,7 +1144,7 @@
   1.234  
   1.235      val ind_prems = List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
   1.236        map (make_ind_prem fsT (fn T => fn t => fn u =>
   1.237 -        Const ("nominal.fresh", T --> fsT --> HOLogic.boolT) $ t $ u) i T)
   1.238 +        Const ("Nominal.fresh", T --> fsT --> HOLogic.boolT) $ t $ u) i T)
   1.239            (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
   1.240      val tnames = DatatypeProp.make_tnames recTs;
   1.241      val zs = variantlist (replicate (length descr'') "z", tnames);
   1.242 @@ -1167,7 +1172,7 @@
   1.243        let
   1.244          val T = fastype_of1 (Ts, t);
   1.245          val U = fastype_of1 (Ts, u)
   1.246 -      in Const ("nominal.perm", T --> U --> U) $ t $ u end;
   1.247 +      in Const ("Nominal.perm", T --> U --> U) $ t $ u end;
   1.248  
   1.249      val aux_ind_vars =
   1.250        (DatatypeProp.indexify_names (replicate (length dt_atomTs) "pi") ~~
   1.251 @@ -1213,7 +1218,7 @@
   1.252                (Const ("insert", T --> S --> S) $
   1.253                  (foldr (mk_perm (T :: Ts)) (Bound (n - i - j)) prms) $
   1.254                  (Const ("op Un", S --> S --> S) $ (f $ Bound (n - k - p)) $
   1.255 -                   (Const ("nominal.supp", U --> S) $
   1.256 +                   (Const ("Nominal.supp", U --> S) $
   1.257                       foldr (mk_perm (T :: Ts)) (Bound (n - i')) prms))))))
   1.258        end;
   1.259  
   1.260 @@ -1304,7 +1309,7 @@
   1.261        map (fn (_, f) =>
   1.262          let val f' = Logic.varify f
   1.263          in (cterm_of thy9 f',
   1.264 -          cterm_of thy9 (Const ("nominal.supp", fastype_of f')))
   1.265 +          cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
   1.266          end) fresh_fs) induct_aux;
   1.267  
   1.268      val induct = standard (Goal.prove thy9 [] ind_prems ind_concl
   1.269 @@ -1352,7 +1357,7 @@
   1.270      fun partition_cargs idxs xs = map (fn (i, j) =>
   1.271        (List.take (List.drop (xs, i), j), List.nth (xs, i + j))) idxs;
   1.272  
   1.273 -    fun mk_fresh_fun (a, t) = Const ("nominal.fresh_fun",
   1.274 +    fun mk_fresh_fun (a, t) = Const ("Nominal.fresh_fun",
   1.275        (fastype_of a --> fastype_of t) --> fastype_of t) $ lambda a t;
   1.276  
   1.277      fun make_rec_intr T rec_set ((rec_intr_ts, l), ((cname, cargs), idxs)) =