src/HOL/Tools/inductive_set.ML
changeset 32287 65d5c5b30747
parent 32135 f645b51e8e54
child 32306 19f55947d4d5
child 32342 3fabf5b5fc83
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Jul 29 16:43:02 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Jul 29 16:48:34 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_split t
     1.8 +         let val (u, Ts, ps) = HOLogic.strip_splits 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.dest_tuple 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.ap_split' (HOLogic.prod_factors p) U HOLogic.boolT t
    1.21 +          HOLogic.mk_splits (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.prodT_factors' ps U ---> HOLogic.boolT)) x
    1.30 +      val x' = map_type (K (HOLogic.strip_tupleT 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.ap_split' ps U HOLogic.boolT x'))
    1.35 +         HOLogic.mk_splits 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.prodT_factors' fs' U;
    1.44 +            val Ts = HOLogic.strip_tupleT 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.ap_split' fs' U
    1.53 +                HOLogic.Collect_const U $ HOLogic.mk_splits fs' U
    1.54                    HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
    1.55            end)
    1.56    in
    1.57 @@ -270,7 +270,7 @@
    1.58               fun factors_of t fs = case strip_abs_body t of
    1.59                   Const ("op :", _) $ u $ S =>
    1.60                     if is_Free S orelse is_Var S then
    1.61 -                     let val ps = HOLogic.prod_factors u
    1.62 +                     let val ps = HOLogic.flat_tuple_paths u
    1.63                       in (SOME ps, (S, ps) :: fs) end
    1.64                     else (NONE, fs)
    1.65                 | _ => (NONE, fs);
    1.66 @@ -279,7 +279,7 @@
    1.67               val ((h', ts'), fs') = (case rhs of
    1.68                   Abs _ => (case strip_abs_body rhs of
    1.69                       Const ("op :", _) $ u $ S =>
    1.70 -                       (strip_comb S, SOME (HOLogic.prod_factors u))
    1.71 +                       (strip_comb S, SOME (HOLogic.flat_tuple_paths u))
    1.72                     | _ => error "member symbol on right-hand side expected")
    1.73                 | _ => (strip_comb rhs, NONE))
    1.74             in
    1.75 @@ -366,7 +366,7 @@
    1.76        in
    1.77          (cterm_of thy x,
    1.78           cterm_of thy (list_abs (map (pair "x") Ts, HOLogic.mk_mem
    1.79 -           (HOLogic.mk_tuple' ps T (map Bound (length ps downto 0)), x'))))
    1.80 +           (HOLogic.mk_tuple ps T (map Bound (length ps downto 0)), x'))))
    1.81        end) fs
    1.82    in
    1.83      thm |>
    1.84 @@ -412,7 +412,7 @@
    1.85        PredSetConvData.get (Context.Proof ctxt);
    1.86      fun infer (Abs (_, _, t)) = infer t
    1.87        | infer (Const ("op :", _) $ t $ u) =
    1.88 -          infer_arities thy set_arities (SOME (HOLogic.prod_factors t), u)
    1.89 +          infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
    1.90        | infer (t $ u) = infer t #> infer u
    1.91        | infer _ = I;
    1.92      val new_arities = filter_out
    1.93 @@ -422,14 +422,14 @@
    1.94          SOME fs =>
    1.95            let
    1.96              val T = HOLogic.dest_setT (fastype_of x);
    1.97 -            val Ts = HOLogic.prodT_factors' fs T;
    1.98 +            val Ts = HOLogic.strip_tupleT fs T;
    1.99              val x' = map_type (K (Ts ---> HOLogic.boolT)) x
   1.100            in
   1.101              (x, (x',
   1.102                (HOLogic.Collect_const T $
   1.103 -                 HOLogic.ap_split' fs T HOLogic.boolT x',
   1.104 +                 HOLogic.mk_splits fs T HOLogic.boolT x',
   1.105                 list_abs (map (pair "x") Ts, HOLogic.mk_mem
   1.106 -                 (HOLogic.mk_tuple' fs T (map Bound (length fs downto 0)),
   1.107 +                 (HOLogic.mk_tuple fs T (map Bound (length fs downto 0)),
   1.108                    x)))))
   1.109            end
   1.110         | NONE => (x, (x, (x, x))))) params;
   1.111 @@ -448,13 +448,13 @@
   1.112             Pretty.str ("of " ^ s ^ " do not agree with types"),
   1.113             Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) paramTs)),
   1.114             Pretty.str "of declared parameters"]));
   1.115 -        val Ts = HOLogic.prodT_factors' fs U;
   1.116 +        val Ts = HOLogic.strip_tupleT fs U;
   1.117          val c' = Free (s ^ "p",
   1.118            map fastype_of params1 @ Ts ---> HOLogic.boolT)
   1.119        in
   1.120          ((c', (fs, U, Ts)),
   1.121           (list_comb (c, params2),
   1.122 -          HOLogic.Collect_const U $ HOLogic.ap_split' fs U HOLogic.boolT
   1.123 +          HOLogic.Collect_const U $ HOLogic.mk_splits fs U HOLogic.boolT
   1.124              (list_comb (c', params1))))
   1.125        end) |> split_list |>> split_list;
   1.126      val eqns' = eqns @
   1.127 @@ -484,7 +484,7 @@
   1.128      val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
   1.129        (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
   1.130           fold_rev lambda params (HOLogic.Collect_const U $
   1.131 -           HOLogic.ap_split' fs U HOLogic.boolT (list_comb (p, params3))))))
   1.132 +           HOLogic.mk_splits fs U HOLogic.boolT (list_comb (p, params3))))))
   1.133           (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
   1.134  
   1.135      (* prove theorems for converting predicate to set notation *)
   1.136 @@ -495,7 +495,7 @@
   1.137              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.138                (list_comb (p, params3),
   1.139                 list_abs (map (pair "x") Ts, HOLogic.mk_mem
   1.140 -                 (HOLogic.mk_tuple' fs U (map Bound (length fs downto 0)),
   1.141 +                 (HOLogic.mk_tuple fs U (map Bound (length fs downto 0)),
   1.142                    list_comb (c, params))))))
   1.143              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
   1.144                [def, mem_Collect_eq, split_conv]) 1))