src/HOL/Product_Type.thy
changeset 51717 9e7d1c139569
parent 51703 f2e92fc0c8aa
child 52143 36ffe23b25f8
     1.1 --- a/src/HOL/Product_Type.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -415,16 +415,21 @@
     1.4        | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u
     1.5        | exists_paired_all (Abs (_, _, t)) = exists_paired_all t
     1.6        | exists_paired_all _ = false;
     1.7 -    val ss = HOL_basic_ss
     1.8 -      addsimps [@{thm split_paired_all}, @{thm unit_all_eq2}, @{thm unit_abs_eta_conv}]
     1.9 -      addsimprocs [@{simproc unit_eq}];
    1.10 +    val ss =
    1.11 +      simpset_of
    1.12 +       (put_simpset HOL_basic_ss @{context}
    1.13 +        addsimps [@{thm split_paired_all}, @{thm unit_all_eq2}, @{thm unit_abs_eta_conv}]
    1.14 +        addsimprocs [@{simproc unit_eq}]);
    1.15    in
    1.16 -    val split_all_tac = SUBGOAL (fn (t, i) =>
    1.17 -      if exists_paired_all t then safe_full_simp_tac ss i else no_tac);
    1.18 -    val unsafe_split_all_tac = SUBGOAL (fn (t, i) =>
    1.19 -      if exists_paired_all t then full_simp_tac ss i else no_tac);
    1.20 -    fun split_all th =
    1.21 -      if exists_paired_all (Thm.prop_of th) then full_simplify ss th else th;
    1.22 +    fun split_all_tac ctxt = SUBGOAL (fn (t, i) =>
    1.23 +      if exists_paired_all t then safe_full_simp_tac (put_simpset ss ctxt) i else no_tac);
    1.24 +
    1.25 +    fun unsafe_split_all_tac ctxt = SUBGOAL (fn (t, i) =>
    1.26 +      if exists_paired_all t then full_simp_tac (put_simpset ss ctxt) i else no_tac);
    1.27 +
    1.28 +    fun split_all ctxt th =
    1.29 +      if exists_paired_all (Thm.prop_of th)
    1.30 +      then full_simplify (put_simpset ss ctxt) th else th;
    1.31    end;
    1.32  *}
    1.33  
    1.34 @@ -451,7 +456,8 @@
    1.35  
    1.36  ML {*
    1.37  local
    1.38 -  val cond_split_eta_ss = HOL_basic_ss addsimps @{thms cond_split_eta};
    1.39 +  val cond_split_eta_ss =
    1.40 +    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms cond_split_eta});
    1.41    fun Pair_pat k 0 (Bound m) = (m = k)
    1.42      | Pair_pat k i (Const (@{const_name Pair},  _) $ Bound m $ t) =
    1.43          i > 0 andalso m = k + i andalso Pair_pat k (i - 1) t
    1.44 @@ -463,9 +469,9 @@
    1.45    fun split_pat tp i (Abs  (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE
    1.46      | split_pat tp i (Const (@{const_name prod_case}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
    1.47      | split_pat tp i _ = NONE;
    1.48 -  fun metaeq ss lhs rhs = mk_meta_eq (Goal.prove (Simplifier.the_context ss) [] []
    1.49 +  fun metaeq ctxt lhs rhs = mk_meta_eq (Goal.prove ctxt [] []
    1.50          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
    1.51 -        (K (simp_tac (Simplifier.inherit_context ss cond_split_eta_ss) 1)));
    1.52 +        (K (simp_tac (put_simpset cond_split_eta_ss ctxt) 1)));
    1.53  
    1.54    fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k + 1) i t
    1.55      | beta_term_pat k i (t $ u) =
    1.56 @@ -479,20 +485,20 @@
    1.57          else (subst arg k i t $ subst arg k i u)
    1.58      | subst arg k i t = t;
    1.59  in
    1.60 -  fun beta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t) $ arg) =
    1.61 +  fun beta_proc ctxt (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t) $ arg) =
    1.62          (case split_pat beta_term_pat 1 t of
    1.63 -          SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f))
    1.64 +          SOME (i, f) => SOME (metaeq ctxt s (subst arg 0 i f))
    1.65          | NONE => NONE)
    1.66      | beta_proc _ _ = NONE;
    1.67 -  fun eta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t)) =
    1.68 +  fun eta_proc ctxt (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t)) =
    1.69          (case split_pat eta_term_pat 1 t of
    1.70 -          SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
    1.71 +          SOME (_, ft) => SOME (metaeq ctxt s (let val (f $ arg) = ft in f end))
    1.72          | NONE => NONE)
    1.73      | eta_proc _ _ = NONE;
    1.74  end;
    1.75  *}
    1.76 -simproc_setup split_beta ("split f z") = {* fn _ => fn ss => fn ct => beta_proc ss (term_of ct) *}
    1.77 -simproc_setup split_eta ("split f") = {* fn _ => fn ss => fn ct => eta_proc ss (term_of ct) *}
    1.78 +simproc_setup split_beta ("split f z") = {* fn _ => fn ctxt => fn ct => beta_proc ctxt (term_of ct) *}
    1.79 +simproc_setup split_eta ("split f") = {* fn _ => fn ctxt => fn ct => eta_proc ctxt (term_of ct) *}
    1.80  
    1.81  lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
    1.82    by (subst surjective_pairing, rule split_conv)
    1.83 @@ -572,10 +578,11 @@
    1.84      | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
    1.85      | exists_p_split (Abs (_, _, t)) = exists_p_split t
    1.86      | exists_p_split _ = false;
    1.87 -  val ss = HOL_basic_ss addsimps @{thms split_conv};
    1.88  in
    1.89 -val split_conv_tac = SUBGOAL (fn (t, i) =>
    1.90 -    if exists_p_split t then safe_full_simp_tac ss i else no_tac);
    1.91 +fun split_conv_tac ctxt = SUBGOAL (fn (t, i) =>
    1.92 +  if exists_p_split t
    1.93 +  then safe_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_conv}) i
    1.94 +  else no_tac);
    1.95  end;
    1.96  *}
    1.97  
    1.98 @@ -1154,7 +1161,7 @@
    1.99  ML_file "Tools/set_comprehension_pointfree.ML"
   1.100  
   1.101  setup {*
   1.102 -  Code_Preproc.map_pre (fn ss => ss addsimprocs
   1.103 +  Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs
   1.104      [Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}],
   1.105      proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}])
   1.106  *}