author berghofe Mon Oct 17 17:42:24 2005 +0200 (2005-10-17) changeset 17872 f08fc98a164a parent 17871 67ffbfcd6fef child 17873 09236f6a6a19
Implemented proofs for support and freshness theorems.
```     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)
```