src/HOL/Tools/inductive_set.ML
changeset 61424 c3658c18b7bc
parent 61268 abe08fb15a12
child 61853 fb7756087101
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4          fun mk_collect p T t =
     1.5            let val U = HOLogic.dest_setT T
     1.6            in HOLogic.Collect_const U $
     1.7 -            HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
     1.8 +            HOLogic.mk_ptupleabs (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
     1.9            end;
    1.10          fun decomp (Const (s, _) $ ((m as Const (@{const_name Set.member},
    1.11                Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
    1.12 @@ -66,7 +66,7 @@
    1.13            | decomp _ = NONE;
    1.14          val simp =
    1.15            full_simp_tac
    1.16 -            (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]) 1;
    1.17 +            (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm case_prod_conv}]) 1;
    1.18          fun mk_rew t = (case strip_abs_vars t of
    1.19              [] => NONE
    1.20            | xs => (case decomp (strip_abs_body t) of
    1.21 @@ -211,7 +211,7 @@
    1.22        (dest_Var x,
    1.23         Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
    1.24           (HOLogic.Collect_const U $
    1.25 -            HOLogic.mk_psplits ps U HOLogic.boolT
    1.26 +            HOLogic.mk_ptupleabs ps U HOLogic.boolT
    1.27                (list_comb (x', map Bound (length Ts - 1 downto 0))))))
    1.28      end) fs;
    1.29  
    1.30 @@ -232,11 +232,11 @@
    1.31            in
    1.32              thm' RS (infer_instantiate ctxt [(arg_cong_f,
    1.33                Thm.cterm_of ctxt (Abs ("P", Ts ---> HOLogic.boolT,
    1.34 -                HOLogic.Collect_const U $ HOLogic.mk_psplits fs' U
    1.35 +                HOLogic.Collect_const U $ HOLogic.mk_ptupleabs fs' U
    1.36                    HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
    1.37            end)
    1.38    in
    1.39 -    Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]
    1.40 +    Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm case_prod_conv}]
    1.41        addsimprocs [@{simproc Collect_mem}]) thm'' |>
    1.42          zero_var_indexes |> eta_contract_thm ctxt (equal p)
    1.43    end;
    1.44 @@ -344,7 +344,7 @@
    1.45      thm |>
    1.46      Thm.instantiate ([], insts) |>
    1.47      Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs
    1.48 -      [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |>
    1.49 +      [to_pred_simproc (mem_Collect_eq :: @{thm case_prod_conv} :: to_pred_simps)]) |>
    1.50      eta_contract_thm ctxt (is_pred pred_arities) |>
    1.51      Rule_Cases.save thm
    1.52    end;
    1.53 @@ -415,7 +415,7 @@
    1.54            in
    1.55              (x, (x',
    1.56                (HOLogic.Collect_const T $
    1.57 -                 HOLogic.mk_psplits fs T HOLogic.boolT x',
    1.58 +                 HOLogic.mk_ptupleabs fs T HOLogic.boolT x',
    1.59                 fold_rev (Term.abs o pair "x") Ts
    1.60                   (HOLogic.mk_mem
    1.61                     (HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)), x)))))
    1.62 @@ -442,12 +442,12 @@
    1.63        in
    1.64          ((c', (fs, U, Ts)),
    1.65           (list_comb (c, params2),
    1.66 -          HOLogic.Collect_const U $ HOLogic.mk_psplits fs U HOLogic.boolT
    1.67 +          HOLogic.Collect_const U $ HOLogic.mk_ptupleabs fs U HOLogic.boolT
    1.68              (list_comb (c', params1))))
    1.69        end) |> split_list |>> split_list;
    1.70      val eqns' = eqns @
    1.71        map (Thm.prop_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq)
    1.72 -        (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps);
    1.73 +        (mem_Collect_eq :: @{thm case_prod_conv} :: to_pred_simps);
    1.74  
    1.75      (* predicate version of the introduction rules *)
    1.76      val intros' =
    1.77 @@ -472,7 +472,7 @@
    1.78        |> fold_map Local_Theory.define
    1.79          (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []),
    1.80             fold_rev lambda params (HOLogic.Collect_const U $
    1.81 -             HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
    1.82 +             HOLogic.mk_ptupleabs fs U HOLogic.boolT (list_comb (p, params3))))))
    1.83             (cnames_syn ~~ cs_info ~~ preds));
    1.84  
    1.85      (* prove theorems for converting predicate to set notation *)
    1.86 @@ -487,7 +487,7 @@
    1.87                    list_comb (c, params))))))
    1.88              (K (REPEAT (resolve_tac lthy @{thms ext} 1) THEN
    1.89                simp_tac (put_simpset HOL_basic_ss lthy addsimps
    1.90 -                [def, mem_Collect_eq, @{thm split_conv}]) 1))
    1.91 +                [def, mem_Collect_eq, @{thm case_prod_conv}]) 1))
    1.92          in
    1.93            lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
    1.94              [Attrib.internal (K pred_set_conv_att)]),
    1.95 @@ -542,7 +542,7 @@
    1.96        "declare of monotonicity rule for set operators");
    1.97  
    1.98  
    1.99 -(* commands *)
   1.100 +(* commands *)                           
   1.101  
   1.102  val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
   1.103