- Changed naming scheme: names of "internal" constructors now have
authorberghofe
Fri Jun 09 17:30:52 2006 +0200 (2006-06-09)
changeset 198333a3f591c838d
parent 19832 1a09f25410da
child 19834 2290cc06049b
- Changed naming scheme: names of "internal" constructors now have
"_Rep" as suffix - no need to set unique_names to false any longer
- Cleaned up a bit (removed occurrences of strip_option and replace_types')
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Fri Jun 09 16:25:05 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Fri Jun 09 17:30:52 2006 +0200
     1.3 @@ -181,12 +181,8 @@
     1.4            Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
     1.5        | replace_types T = T;
     1.6  
     1.7 -    fun replace_types' (Type (s, Ts)) =
     1.8 -          Type (getOpt (AList.lookup op = rps s, s), map replace_types' Ts)
     1.9 -      | replace_types' T = T;
    1.10 -
    1.11      val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, tname ^ "_Rep", NoSyn,
    1.12 -      map (fn (cname, cargs, mx) => (cname,
    1.13 +      map (fn (cname, cargs, mx) => (cname ^ "_Rep",
    1.14          map (augment_sort_typ o replace_types) cargs, NoSyn)) constrs)) dts';
    1.15  
    1.16      val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
    1.17 @@ -665,7 +661,7 @@
    1.18               let
    1.19                 val SOME index = AList.lookup op = ty_idxs i;
    1.20                 val (constrs1, constrs2) = ListPair.unzip
    1.21 -                 (map (fn (cname, cargs) => apfst (pair (strip_nth_name 2 cname))
    1.22 +                 (map (fn (cname, cargs) => apfst (pair (strip_nth_name 2 (strip_nth_name 1 cname)))
    1.23                     (foldl_map (fn (dts, dt) =>
    1.24                       let val (dts', dt') = strip_option dt
    1.25                       in (dts @ dts' @ [reindex dt'], (length dts, length dts')) end)
    1.26 @@ -680,7 +676,11 @@
    1.27      fun partition_cargs idxs xs = map (fn (i, j) =>
    1.28        (List.take (List.drop (xs, i), j), List.nth (xs, i + j))) idxs;
    1.29  
    1.30 -    val typ_of_dtyp' = replace_types' o typ_of_dtyp descr sorts';
    1.31 +    val pdescr = map (fn ((i, (s, dts, constrs)), (_, idxss)) => (i, (s, dts,
    1.32 +      map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs))
    1.33 +        (constrs ~~ idxss)))) (descr'' ~~ ndescr);
    1.34 +
    1.35 +    fun nth_dtyp' i = typ_of_dtyp descr'' sorts' (DtRec i);
    1.36  
    1.37      val rep_names = map (fn s =>
    1.38        Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
    1.39 @@ -696,25 +696,22 @@
    1.40  
    1.41      val full_new_type_names = map (Sign.full_name (sign_of thy)) new_type_names;
    1.42  
    1.43 -    fun make_constr_def tname T T' ((thy, defs, eqns), ((cname, cargs), (cname', mx))) =
    1.44 +    fun make_constr_def tname T T' ((thy, defs, eqns),
    1.45 +        (((cname_rep, _), (cname, cargs)), (cname', mx))) =
    1.46        let
    1.47 -        fun constr_arg (dt, (j, l_args, r_args)) =
    1.48 +        fun constr_arg ((dts, dt), (j, l_args, r_args)) =
    1.49            let
    1.50 -            val x' = mk_Free "x" (typ_of_dtyp' dt) j;
    1.51 -            val (dts, dt') = strip_option dt;
    1.52 -            val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp' dt) i)
    1.53 +            val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' sorts' dt) i)
    1.54                (dts ~~ (j upto j + length dts - 1))
    1.55 -            val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts)
    1.56 -            val (dts', dt'') = strip_dtyp dt'
    1.57 +            val x = mk_Free "x" (typ_of_dtyp descr'' sorts' dt) (j + length dts)
    1.58            in
    1.59              (j + length dts + 1,
    1.60               xs @ x :: l_args,
    1.61               foldr mk_abs_fun
    1.62 -               (case dt'' of
    1.63 +               (case dt of
    1.64                    DtRec k => if k < length new_type_names then
    1.65 -                      list_abs (map (pair "z" o typ_of_dtyp') dts',
    1.66 -                        Const (List.nth (rep_names, k), typ_of_dtyp' dt'' -->
    1.67 -                          typ_of_dtyp descr sorts' dt'') $ app_bnds x (length dts'))
    1.68 +                      Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts' dt -->
    1.69 +                        typ_of_dtyp descr sorts' dt) $ x
    1.70                      else error "nested recursion not (yet) supported"
    1.71                  | _ => x) xs :: r_args)
    1.72            end
    1.73 @@ -723,9 +720,8 @@
    1.74          val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname);
    1.75          val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname);
    1.76          val constrT = map fastype_of l_args ---> T;
    1.77 -        val lhs = list_comb (Const (Sign.full_name thy (Sign.base_name cname),
    1.78 -          constrT), l_args);
    1.79 -        val rhs = list_comb (Const (cname, map fastype_of r_args ---> T'), r_args);
    1.80 +        val lhs = list_comb (Const (cname, constrT), l_args);
    1.81 +        val rhs = list_comb (Const (cname_rep, map fastype_of r_args ---> T'), r_args);
    1.82          val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs);
    1.83          val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.84            (Const (rep_name, T --> T') $ lhs, rhs));
    1.85 @@ -735,20 +731,21 @@
    1.86            (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]
    1.87        in (thy', defs @ [def_thm], eqns @ [eqn]) end;
    1.88  
    1.89 -    fun dt_constr_defs ((thy, defs, eqns, dist_lemmas),
    1.90 -        (((((_, (_, _, constrs)), tname), T), T'), constr_syntax)) =
    1.91 +    fun dt_constr_defs ((thy, defs, eqns, dist_lemmas), ((((((_, (_, _, constrs)),
    1.92 +        (_, (_, _, constrs'))), tname), T), T'), constr_syntax)) =
    1.93        let
    1.94          val rep_const = cterm_of thy
    1.95            (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
    1.96          val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    1.97          val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
    1.98 -          ((Theory.add_path tname thy, defs, []), constrs ~~ constr_syntax)
    1.99 +          ((Theory.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
   1.100        in
   1.101          (parent_path flat_names thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
   1.102        end;
   1.103  
   1.104      val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs
   1.105        ((thy7, [], [], []), List.take (descr, length new_type_names) ~~
   1.106 +        List.take (pdescr, length new_type_names) ~~
   1.107          new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax);
   1.108  
   1.109      val abs_inject_thms = map (fn tname =>
   1.110 @@ -824,7 +821,7 @@
   1.111      val abs_perm = PureThy.get_thms thy8 (Name "abs_perm"); (* FIXME *)
   1.112  
   1.113      val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
   1.114 -      let val T = replace_types' (nth_dtyp i)
   1.115 +      let val T = nth_dtyp' i
   1.116        in List.concat (map (fn (atom, perm_closed_thms) =>
   1.117            map (fn ((cname, dts), constr_rep_thm) => 
   1.118          let
   1.119 @@ -837,15 +834,12 @@
   1.120              let val T = fastype_of t
   1.121              in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
   1.122  
   1.123 -          fun constr_arg (dt, (j, l_args, r_args)) =
   1.124 +          fun constr_arg ((dts, dt), (j, l_args, r_args)) =
   1.125              let
   1.126 -              val x' = mk_Free "x" (typ_of_dtyp' dt) j;
   1.127 -              val (dts, dt') = strip_option dt;
   1.128 -              val Ts = map typ_of_dtyp' dts;
   1.129 +              val Ts = map (typ_of_dtyp descr'' sorts') dts;
   1.130                val xs = map (fn (T, i) => mk_Free "x" T i)
   1.131                  (Ts ~~ (j upto j + length dts - 1))
   1.132 -              val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
   1.133 -              val (dts', dt'') = strip_dtyp dt';
   1.134 +              val x = mk_Free "x" (typ_of_dtyp descr'' sorts' dt) (j + length dts)
   1.135              in
   1.136                (j + length dts + 1,
   1.137                 xs @ x :: l_args,
   1.138 @@ -868,7 +862,7 @@
   1.139                   (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
   1.140                      perm_closed_thms)) 1)]))
   1.141          end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss))
   1.142 -      end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
   1.143 +      end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
   1.144  
   1.145      (** prove injectivity of constructors **)
   1.146  
   1.147 @@ -879,24 +873,20 @@
   1.148      val supp_def = PureThy.get_thm thy8 (Name "supp_def");
   1.149  
   1.150      val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
   1.151 -      let val T = replace_types' (nth_dtyp i)
   1.152 +      let val T = nth_dtyp' i
   1.153        in List.mapPartial (fn ((cname, dts), constr_rep_thm) =>
   1.154          if null dts then NONE else SOME
   1.155          let
   1.156            val cname = Sign.intern_const thy8
   1.157              (NameSpace.append tname (Sign.base_name cname));
   1.158  
   1.159 -          fun make_inj (dt, (j, args1, args2, eqs)) =
   1.160 +          fun make_inj ((dts, dt), (j, args1, args2, eqs)) =
   1.161              let
   1.162 -              val x' = mk_Free "x" (typ_of_dtyp' dt) j;
   1.163 -              val y' = mk_Free "y" (typ_of_dtyp' dt) j;
   1.164 -              val (dts, dt') = strip_option dt;
   1.165 -              val Ts_idx = map typ_of_dtyp' dts ~~ (j upto j + length dts - 1);
   1.166 +              val Ts_idx = map (typ_of_dtyp descr'' sorts') dts ~~ (j upto j + length dts - 1);
   1.167                val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
   1.168                val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx;
   1.169 -              val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
   1.170 -              val y = mk_Free "y" (typ_of_dtyp' dt') (j + length dts);
   1.171 -              val (dts', dt'') = strip_dtyp dt';
   1.172 +              val x = mk_Free "x" (typ_of_dtyp descr'' sorts' dt) (j + length dts);
   1.173 +              val y = mk_Free "y" (typ_of_dtyp descr'' sorts' dt) (j + length dts)
   1.174              in
   1.175                (j + length dts + 1,
   1.176                 xs @ (x :: args1), ys @ (y :: args2),
   1.177 @@ -920,7 +910,7 @@
   1.178                  TRY (asm_full_simp_tac (HOL_basic_ss addsimps (perm_fun_def ::
   1.179                    expand_fun_eq :: rep_inject_thms @ perm_rep_perm_thms)) 1)]))
   1.180          end) (constrs ~~ constr_rep_thms)
   1.181 -      end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
   1.182 +      end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
   1.183  
   1.184      (** equations for support and freshness **)
   1.185  
   1.186 @@ -931,21 +921,18 @@
   1.187  
   1.188      val (supp_thms, fresh_thms) = ListPair.unzip (map ListPair.unzip
   1.189        (map (fn ((((i, (_, _, constrs)), tname), inject_thms'), perm_thms') =>
   1.190 -      let val T = replace_types' (nth_dtyp i)
   1.191 +      let val T = nth_dtyp' i
   1.192        in List.concat (map (fn (cname, dts) => map (fn atom =>
   1.193          let
   1.194            val cname = Sign.intern_const thy8
   1.195              (NameSpace.append tname (Sign.base_name cname));
   1.196            val atomT = Type (atom, []);
   1.197  
   1.198 -          fun process_constr (dt, (j, args1, args2)) =
   1.199 +          fun process_constr ((dts, dt), (j, args1, args2)) =
   1.200              let
   1.201 -              val x' = mk_Free "x" (typ_of_dtyp' dt) j;
   1.202 -              val (dts, dt') = strip_option dt;
   1.203 -              val Ts_idx = map typ_of_dtyp' dts ~~ (j upto j + length dts - 1);
   1.204 +              val Ts_idx = map (typ_of_dtyp descr'' sorts') dts ~~ (j upto j + length dts - 1);
   1.205                val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
   1.206 -              val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
   1.207 -              val (dts', dt'') = strip_dtyp dt';
   1.208 +              val x = mk_Free "x" (typ_of_dtyp descr'' sorts' dt) (j + length dts)
   1.209              in
   1.210                (j + length dts + 1,
   1.211                 xs @ (x :: args1), foldr mk_abs_fun x xs :: args2)
   1.212 @@ -978,33 +965,10 @@
   1.213               (fn _ =>
   1.214                 simp_tac (simpset_of thy8 addsimps [fresh_def, supp_thm]) 1)))
   1.215          end) atoms) constrs)
   1.216 -      end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
   1.217 +      end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
   1.218  
   1.219      (**** weak induction theorem ****)
   1.220  
   1.221 -    val arities = get_arities descr'';
   1.222 -
   1.223 -    fun mk_funs_inv thm =
   1.224 -      let
   1.225 -        val {sign, prop, ...} = rep_thm thm;
   1.226 -        val _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $
   1.227 -          (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
   1.228 -        val used = add_term_tfree_names (a, []);
   1.229 -
   1.230 -        fun mk_thm i =
   1.231 -          let
   1.232 -            val Ts = map (TFree o rpair HOLogic.typeS)
   1.233 -              (variantlist (replicate i "'t", used));
   1.234 -            val f = Free ("f", Ts ---> U)
   1.235 -          in standard (Goal.prove sign [] [] (Logic.mk_implies
   1.236 -            (HOLogic.mk_Trueprop (HOLogic.list_all
   1.237 -               (map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))),
   1.238 -             HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
   1.239 -               r $ (a $ app_bnds f i)), f))))
   1.240 -            (fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1]))
   1.241 -          end
   1.242 -      in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
   1.243 -
   1.244      fun mk_indrule_lemma ((prems, concls), (((i, _), T), U)) =
   1.245        let
   1.246          val Rep_t = Const (List.nth (rep_names, i), T --> U) $
   1.247 @@ -1036,7 +1000,7 @@
   1.248      val indrule_lemma' = cterm_instantiate
   1.249        (map (cterm_of thy8) Ps ~~ map (cterm_of thy8) frees) indrule_lemma;
   1.250  
   1.251 -    val Abs_inverse_thms' = List.concat (map mk_funs_inv Abs_inverse_thms);
   1.252 +    val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms;
   1.253  
   1.254      val dt_induct_prop = DatatypeProp.make_ind descr' sorts';
   1.255      val dt_induct = standard (Goal.prove thy8 []