src/HOL/Tools/inductive_set.ML
changeset 32342 3fabf5b5fc83
parent 32287 65d5c5b30747
child 32351 96f9e6402403
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Jul 30 13:52:18 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Jul 30 15:20:57 2009 +0200
     1.3 @@ -33,10 +33,10 @@
     1.4  val collect_mem_simproc =
     1.5    Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
     1.6      fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
     1.7 -         let val (u, Ts, ps) = HOLogic.strip_splits t
     1.8 +         let val (u, Ts, ps) = HOLogic.strip_psplits t
     1.9           in case u of
    1.10             (c as Const ("op :", _)) $ q $ S' =>
    1.11 -             (case try (HOLogic.dest_tuple ps) q of
    1.12 +             (case try (HOLogic.strip_ptuple ps) q of
    1.13                  NONE => NONE
    1.14                | SOME ts =>
    1.15                    if not (loose_bvar (S', 0)) andalso
    1.16 @@ -79,7 +79,7 @@
    1.17        fun mk_collect p T t =
    1.18          let val U = HOLogic.dest_setT T
    1.19          in HOLogic.Collect_const U $
    1.20 -          HOLogic.mk_splits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
    1.21 +          HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
    1.22          end;
    1.23        fun decomp (Const (s, _) $ ((m as Const ("op :",
    1.24              Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
    1.25 @@ -223,11 +223,11 @@
    1.26    map (fn (x, ps) =>
    1.27      let
    1.28        val U = HOLogic.dest_setT (fastype_of x);
    1.29 -      val x' = map_type (K (HOLogic.strip_tupleT ps U ---> HOLogic.boolT)) x
    1.30 +      val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x
    1.31      in
    1.32        (cterm_of thy x,
    1.33         cterm_of thy (HOLogic.Collect_const U $
    1.34 -         HOLogic.mk_splits ps U HOLogic.boolT x'))
    1.35 +         HOLogic.mk_psplits ps U HOLogic.boolT x'))
    1.36      end) fs;
    1.37  
    1.38  fun mk_to_pred_eq p fs optfs' T thm =
    1.39 @@ -240,7 +240,7 @@
    1.40        | SOME fs' =>
    1.41            let
    1.42              val (_, U) = split_last (binder_types T);
    1.43 -            val Ts = HOLogic.strip_tupleT fs' U;
    1.44 +            val Ts = HOLogic.strip_ptupleT fs' U;
    1.45              (* FIXME: should cterm_instantiate increment indexes? *)
    1.46              val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
    1.47              val (arg_cong_f, _) = arg_cong' |> cprop_of |> Drule.strip_imp_concl |>
    1.48 @@ -248,7 +248,7 @@
    1.49            in
    1.50              thm' RS (Drule.cterm_instantiate [(arg_cong_f,
    1.51                cterm_of thy (Abs ("P", Ts ---> HOLogic.boolT,
    1.52 -                HOLogic.Collect_const U $ HOLogic.mk_splits fs' U
    1.53 +                HOLogic.Collect_const U $ HOLogic.mk_psplits fs' U
    1.54                    HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
    1.55            end)
    1.56    in
    1.57 @@ -361,12 +361,12 @@
    1.58      val insts = map (fn (x, ps) =>
    1.59        let
    1.60          val Ts = binder_types (fastype_of x);
    1.61 -        val T = HOLogic.mk_tupleT ps Ts;
    1.62 +        val T = HOLogic.mk_ptupleT ps Ts;
    1.63          val x' = map_type (K (HOLogic.mk_setT T)) x
    1.64        in
    1.65          (cterm_of thy x,
    1.66           cterm_of thy (list_abs (map (pair "x") Ts, HOLogic.mk_mem
    1.67 -           (HOLogic.mk_tuple ps T (map Bound (length ps downto 0)), x'))))
    1.68 +           (HOLogic.mk_ptuple ps T (map Bound (length ps downto 0)), x'))))
    1.69        end) fs
    1.70    in
    1.71      thm |>
    1.72 @@ -422,14 +422,14 @@
    1.73          SOME fs =>
    1.74            let
    1.75              val T = HOLogic.dest_setT (fastype_of x);
    1.76 -            val Ts = HOLogic.strip_tupleT fs T;
    1.77 +            val Ts = HOLogic.strip_ptupleT fs T;
    1.78              val x' = map_type (K (Ts ---> HOLogic.boolT)) x
    1.79            in
    1.80              (x, (x',
    1.81                (HOLogic.Collect_const T $
    1.82 -                 HOLogic.mk_splits fs T HOLogic.boolT x',
    1.83 +                 HOLogic.mk_psplits fs T HOLogic.boolT x',
    1.84                 list_abs (map (pair "x") Ts, HOLogic.mk_mem
    1.85 -                 (HOLogic.mk_tuple fs T (map Bound (length fs downto 0)),
    1.86 +                 (HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)),
    1.87                    x)))))
    1.88            end
    1.89         | NONE => (x, (x, (x, x))))) params;
    1.90 @@ -448,13 +448,13 @@
    1.91             Pretty.str ("of " ^ s ^ " do not agree with types"),
    1.92             Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) paramTs)),
    1.93             Pretty.str "of declared parameters"]));
    1.94 -        val Ts = HOLogic.strip_tupleT fs U;
    1.95 +        val Ts = HOLogic.strip_ptupleT fs U;
    1.96          val c' = Free (s ^ "p",
    1.97            map fastype_of params1 @ Ts ---> HOLogic.boolT)
    1.98        in
    1.99          ((c', (fs, U, Ts)),
   1.100           (list_comb (c, params2),
   1.101 -          HOLogic.Collect_const U $ HOLogic.mk_splits fs U HOLogic.boolT
   1.102 +          HOLogic.Collect_const U $ HOLogic.mk_psplits fs U HOLogic.boolT
   1.103              (list_comb (c', params1))))
   1.104        end) |> split_list |>> split_list;
   1.105      val eqns' = eqns @
   1.106 @@ -484,7 +484,7 @@
   1.107      val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
   1.108        (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
   1.109           fold_rev lambda params (HOLogic.Collect_const U $
   1.110 -           HOLogic.mk_splits fs U HOLogic.boolT (list_comb (p, params3))))))
   1.111 +           HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
   1.112           (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
   1.113  
   1.114      (* prove theorems for converting predicate to set notation *)
   1.115 @@ -495,7 +495,7 @@
   1.116              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.117                (list_comb (p, params3),
   1.118                 list_abs (map (pair "x") Ts, HOLogic.mk_mem
   1.119 -                 (HOLogic.mk_tuple fs U (map Bound (length fs downto 0)),
   1.120 +                 (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
   1.121                    list_comb (c, params))))))
   1.122              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
   1.123                [def, mem_Collect_eq, split_conv]) 1))