1.1 --- a/src/HOL/Nominal/nominal_package.ML	Mon Oct 17 17:40:34 2005 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Mon Oct 17 17:42:24 2005 +0200
     1.3 @@ -1721,11 +1721,73 @@
     1.4          end) (constrs ~~ constr_rep_thms)
     1.5        end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
     1.6  
     1.7 +    (** equations for support and freshness **)
     1.8 +
     1.9 +    val Un_assoc = PureThy.get_thm thy8 (Name "Un_assoc");
    1.10 +    val de_Morgan_conj = PureThy.get_thm thy8 (Name "de_Morgan_conj");
    1.11 +    val Collect_disj_eq = PureThy.get_thm thy8 (Name "Collect_disj_eq");
    1.12 +    val finite_Un = PureThy.get_thm thy8 (Name "finite_Un");
    1.13 +
    1.14 +    val (supp_thms, fresh_thms) = ListPair.unzip (map ListPair.unzip
    1.15 +      (map (fn ((((i, (_, _, constrs)), tname), inject_thms'), perm_thms') =>
    1.16 +      let val T = replace_types' (nth_dtyp i)
    1.17 +      in List.concat (map (fn (cname, dts) => map (fn atom =>
    1.18 +        let
    1.19 +          val cname = Sign.intern_const thy8
    1.20 +            (NameSpace.append tname (Sign.base_name cname));
    1.21 +          val atomT = Type (atom, []);
    1.22 +
    1.23 +          fun process_constr (dt, (j, args1, args2)) =
    1.24 +            let
    1.25 +              val x' = mk_Free "x" (typ_of_dtyp' dt) j;
    1.26 +              val (dts, dt') = strip_option dt;
    1.27 +              val Ts_idx = map typ_of_dtyp' dts ~~ (j upto j + length dts - 1);
    1.28 +              val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
    1.29 +              val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
    1.30 +              val (dts', dt'') = strip_dtyp dt';
    1.31 +            in case dt'' of
    1.32 +                DtRec k => if k < length new_type_names then
    1.33 +                    (j + length dts + 1,
    1.34 +                     xs @ (x :: args1), foldr mk_abs_fun x xs :: args2)
    1.35 +                  else error "nested recursion not (yet) supported"
    1.36 +              | _ => (j + 1, x' :: args1, x' :: args2)
    1.37 +            end;
    1.38 +
    1.39 +          val (_, args1, args2) = foldr process_constr (1, [], []) dts;
    1.40 +          val Ts = map fastype_of args1;
    1.41 +          val c = list_comb (Const (cname, Ts ---> T), args1);
    1.42 +          fun supp t =
    1.43 +            Const ("nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
    1.44 +          fun fresh t =
    1.45 +            Const ("nominal.fresh", atomT --> fastype_of t --> HOLogic.boolT) $
    1.46 +              Free ("a", atomT) $ t;
    1.47 +          val supp_thm = prove_goalw_cterm [] (cterm_of thy8
    1.48 +              (HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.49 +                (supp c,
    1.50 +                 if null dts then Const ("{}", HOLogic.mk_setT atomT)
    1.51 +                 else foldr1 (HOLogic.mk_binop "op Un") (map supp args2)))))
    1.52 +            (fn _ =>
    1.53 +              [simp_tac (HOL_basic_ss addsimps (supp_def ::
    1.54 +                 Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
    1.55 +                 abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1])
    1.56 +        in
    1.57 +          (supp_thm,
    1.58 +           prove_goalw_cterm [] (cterm_of thy8 (HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.59 +              (fresh c,
    1.60 +               if null dts then HOLogic.true_const
    1.61 +               else foldr1 HOLogic.mk_conj (map fresh args2)))))
    1.62 +             (fn _ =>
    1.63 +               [simp_tac (simpset_of thy8 addsimps [fresh_def, supp_thm]) 1]))
    1.64 +        end) atoms) constrs)
    1.65 +      end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
    1.66 +
    1.67      val (thy9, _) = thy8 |>
    1.68        DatatypeAux.store_thmss "distinct" new_type_names distinct_thms |>>>
    1.69        DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss |>>>
    1.70        DatatypeAux.store_thmss "perm" new_type_names perm_simps' |>>>
    1.71 -      DatatypeAux.store_thmss "inject" new_type_names inject_thms;
    1.72 +      DatatypeAux.store_thmss "inject" new_type_names inject_thms |>>>
    1.73 +      DatatypeAux.store_thmss "supp" new_type_names supp_thms |>>>
    1.74 +      DatatypeAux.store_thmss "fresh" new_type_names fresh_thms;
    1.75  
    1.76    in
    1.77      (thy9, perm_eq_thms)