tuned signature;
authorwenzelm
Sun Jan 12 14:32:22 2014 +0100 (2014-01-12)
changeset 549988601434fa334
parent 54997 811c35e81ac5
child 54999 7859ed58c041
tuned signature;
clarified context;
src/FOL/simpdata.ML
src/HOL/BNF/Tools/bnf_def_tactics.ML
src/HOL/BNF/Tools/bnf_lfp_tactics.ML
src/HOL/Set.thy
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/simpdata.ML
src/Provers/quantifier1.ML
src/ZF/OrdQuant.thy
src/ZF/pair.thy
     1.1 --- a/src/FOL/simpdata.ML	Sun Jan 12 13:16:00 2014 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Sun Jan 12 14:32:22 2014 +0100
     1.3 @@ -123,7 +123,7 @@
     1.4    |> Simplifier.set_mkcong mk_meta_cong
     1.5    |> simpset_of;
     1.6  
     1.7 -fun unfold_tac ths ctxt =
     1.8 +fun unfold_tac ctxt ths =
     1.9    ALLGOALS (full_simp_tac (clear_simpset (put_simpset FOL_basic_ss ctxt) addsimps ths));
    1.10  
    1.11  
     2.1 --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Sun Jan 12 13:16:00 2014 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Sun Jan 12 14:32:22 2014 +0100
     2.3 @@ -186,10 +186,10 @@
     2.4  fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} =
     2.5    if null set_maps then atac 1
     2.6    else
     2.7 -    unfold_tac [in_rel] ctxt THEN
     2.8 +    unfold_tac ctxt [in_rel] THEN
     2.9      REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN
    2.10      hyp_subst_tac ctxt 1 THEN
    2.11 -    unfold_tac set_maps ctxt THEN
    2.12 +    unfold_tac ctxt set_maps THEN
    2.13      EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]},
    2.14        CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1;
    2.15  
     3.1 --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sun Jan 12 13:16:00 2014 +0100
     3.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sun Jan 12 14:32:22 2014 +0100
     3.3 @@ -782,7 +782,7 @@
     3.4  fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = IHs} =
     3.5    let val n = length ks;
     3.6    in
     3.7 -    unfold_tac @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} ctxt THEN
     3.8 +    unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
     3.9      EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2,
    3.10        EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong =>
    3.11          EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp),
     4.1 --- a/src/HOL/Set.thy	Sun Jan 12 13:16:00 2014 +0100
     4.2 +++ b/src/HOL/Set.thy	Sun Jan 12 14:32:22 2014 +0100
     4.3 @@ -69,9 +69,9 @@
     4.4  *}
     4.5  
     4.6  simproc_setup defined_Collect ("{x. P x & Q x}") = {*
     4.7 -  fn _ =>
     4.8 -    Quantifier1.rearrange_Collect
     4.9 -     (rtac @{thm Collect_cong} 1 THEN
    4.10 +  fn _ => Quantifier1.rearrange_Collect
    4.11 +    (fn _ =>
    4.12 +      rtac @{thm Collect_cong} 1 THEN
    4.13        rtac @{thm iffI} 1 THEN
    4.14        ALLGOALS
    4.15          (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
    4.16 @@ -355,17 +355,17 @@
    4.17  *}
    4.18  
    4.19  simproc_setup defined_Bex ("EX x:A. P x & Q x") = {*
    4.20 -  let
    4.21 -    val unfold_bex_tac = unfold_tac @{thms Bex_def};
    4.22 -    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    4.23 -  in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end
    4.24 +  fn _ => Quantifier1.rearrange_bex
    4.25 +    (fn ctxt =>
    4.26 +      unfold_tac ctxt @{thms Bex_def} THEN
    4.27 +      Quantifier1.prove_one_point_ex_tac)
    4.28  *}
    4.29  
    4.30  simproc_setup defined_All ("ALL x:A. P x --> Q x") = {*
    4.31 -  let
    4.32 -    val unfold_ball_tac = unfold_tac @{thms Ball_def};
    4.33 -    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    4.34 -  in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end
    4.35 +  fn _ => Quantifier1.rearrange_ball
    4.36 +    (fn ctxt =>
    4.37 +      unfold_tac ctxt @{thms Ball_def} THEN
    4.38 +      Quantifier1.prove_one_point_all_tac)
    4.39  *}
    4.40  
    4.41  lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
     5.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Sun Jan 12 13:16:00 2014 +0100
     5.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Sun Jan 12 14:32:22 2014 +0100
     5.3 @@ -122,19 +122,14 @@
     5.4  
     5.5  (* General reduction pair application *)
     5.6  fun rem_inv_img ctxt =
     5.7 -  let
     5.8 -    val unfold_tac = Local_Defs.unfold_tac ctxt
     5.9 -  in
    5.10 -    rtac @{thm subsetI} 1
    5.11 -    THEN etac @{thm CollectE} 1
    5.12 -    THEN REPEAT (etac @{thm exE} 1)
    5.13 -    THEN unfold_tac @{thms inv_image_def}
    5.14 -    THEN rtac @{thm CollectI} 1
    5.15 -    THEN etac @{thm conjE} 1
    5.16 -    THEN etac @{thm ssubst} 1
    5.17 -    THEN unfold_tac (@{thms split_conv} @ @{thms triv_forall_equality}
    5.18 -                     @ @{thms sum.cases})
    5.19 -  end
    5.20 +  rtac @{thm subsetI} 1
    5.21 +  THEN etac @{thm CollectE} 1
    5.22 +  THEN REPEAT (etac @{thm exE} 1)
    5.23 +  THEN Local_Defs.unfold_tac ctxt @{thms inv_image_def}
    5.24 +  THEN rtac @{thm CollectI} 1
    5.25 +  THEN etac @{thm conjE} 1
    5.26 +  THEN etac @{thm ssubst} 1
    5.27 +  THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.cases}
    5.28  
    5.29  (* Sets *)
    5.30  
    5.31 @@ -289,9 +284,8 @@
    5.32           THEN (rtac @{thm rp_inv_image_rp} 1)
    5.33           THEN (rtac (order_rpair ms_rp label) 1)
    5.34           THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
    5.35 -         THEN unfold_tac @{thms rp_inv_image_def} ctxt
    5.36 -         THEN Local_Defs.unfold_tac ctxt
    5.37 -           (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
    5.38 +         THEN unfold_tac ctxt @{thms rp_inv_image_def}
    5.39 +         THEN Local_Defs.unfold_tac ctxt @{thms split_conv fst_conv snd_conv}
    5.40           THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
    5.41           THEN EVERY (map (prove_lev true) sl)
    5.42           THEN EVERY (map (prove_lev false) (subtract (op =) sl (0 upto length cs - 1))))
     6.1 --- a/src/HOL/Tools/simpdata.ML	Sun Jan 12 13:16:00 2014 +0100
     6.2 +++ b/src/HOL/Tools/simpdata.ML	Sun Jan 12 14:32:22 2014 +0100
     6.3 @@ -178,7 +178,7 @@
     6.4  fun hol_simplify ctxt rews =
     6.5    Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps rews);
     6.6  
     6.7 -fun unfold_tac ths ctxt =
     6.8 +fun unfold_tac ctxt ths =
     6.9    ALLGOALS (full_simp_tac (clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths));
    6.10  
    6.11  end;
     7.1 --- a/src/Provers/quantifier1.ML	Sun Jan 12 13:16:00 2014 +0100
     7.2 +++ b/src/Provers/quantifier1.ML	Sun Jan 12 14:32:22 2014 +0100
     7.3 @@ -68,9 +68,9 @@
     7.4    val prove_one_point_ex_tac: tactic
     7.5    val rearrange_all: Proof.context -> cterm -> thm option
     7.6    val rearrange_ex: Proof.context -> cterm -> thm option
     7.7 -  val rearrange_ball: tactic -> Proof.context -> cterm -> thm option
     7.8 -  val rearrange_bex: tactic -> Proof.context -> cterm -> thm option
     7.9 -  val rearrange_Collect: tactic -> Proof.context -> cterm -> thm option
    7.10 +  val rearrange_ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
    7.11 +  val rearrange_bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
    7.12 +  val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
    7.13  end;
    7.14  
    7.15  functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
    7.16 @@ -120,12 +120,13 @@
    7.17        | exqu xs P = extract (null xs) xs P
    7.18    in exqu [] end;
    7.19  
    7.20 -fun prove_conv tac ctxt tu =
    7.21 +fun prove_conv ctxt tu tac =
    7.22    let
    7.23      val (goal, ctxt') =
    7.24        yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
    7.25      val thm =
    7.26 -      Goal.prove ctxt' [] [] goal (K (rtac Data.iff_reflection 1 THEN tac));
    7.27 +      Goal.prove ctxt' [] [] goal
    7.28 +        (fn {context = ctxt'', ...} => rtac Data.iff_reflection 1 THEN tac ctxt'');
    7.29    in singleton (Variable.export ctxt' ctxt) thm end;
    7.30  
    7.31  fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i);
    7.32 @@ -178,7 +179,7 @@
    7.33          NONE => NONE
    7.34        | SOME (xs, eq, Q) =>
    7.35            let val R = quantify all x T xs (Data.imp $ eq $ Q)
    7.36 -          in SOME (prove_conv prove_one_point_all_tac ctxt (F, R)) end)
    7.37 +          in SOME (prove_conv ctxt (F, R) (K prove_one_point_all_tac)) end)
    7.38    | _ => NONE);
    7.39  
    7.40  fun rearrange_ball tac ctxt ct =
    7.41 @@ -190,7 +191,7 @@
    7.42            if not (null xs) then NONE
    7.43            else
    7.44              let val R = Data.imp $ eq $ Q
    7.45 -            in SOME (prove_conv tac ctxt (F, Ball $ A $ Abs (x, T, R))) end)
    7.46 +            in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) tac) end)
    7.47    | _ => NONE);
    7.48  
    7.49  fun rearrange_ex ctxt ct =
    7.50 @@ -200,7 +201,7 @@
    7.51          NONE => NONE
    7.52        | SOME (xs, eq, Q) =>
    7.53            let val R = quantify ex x T xs (Data.conj $ eq $ Q)
    7.54 -          in SOME (prove_conv prove_one_point_ex_tac ctxt (F, R)) end)
    7.55 +          in SOME (prove_conv ctxt (F, R) (K prove_one_point_ex_tac)) end)
    7.56    | _ => NONE);
    7.57  
    7.58  fun rearrange_bex tac ctxt ct =
    7.59 @@ -210,7 +211,7 @@
    7.60          NONE => NONE
    7.61        | SOME (xs, eq, Q) =>
    7.62            if not (null xs) then NONE
    7.63 -          else SOME (prove_conv tac ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q))))
    7.64 +          else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) tac))
    7.65    | _ => NONE);
    7.66  
    7.67  fun rearrange_Collect tac ctxt ct =
    7.68 @@ -220,7 +221,7 @@
    7.69          NONE => NONE
    7.70        | SOME (_, eq, Q) =>
    7.71            let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q)
    7.72 -          in SOME (prove_conv tac ctxt (F, R)) end)
    7.73 +          in SOME (prove_conv ctxt (F, R) tac) end)
    7.74    | _ => NONE);
    7.75  
    7.76  end;
     8.1 --- a/src/ZF/OrdQuant.thy	Sun Jan 12 13:16:00 2014 +0100
     8.2 +++ b/src/ZF/OrdQuant.thy	Sun Jan 12 14:32:22 2014 +0100
     8.3 @@ -368,17 +368,17 @@
     8.4  text {* Setting up the one-point-rule simproc *}
     8.5  
     8.6  simproc_setup defined_rex ("\<exists>x[M]. P(x) & Q(x)") = {*
     8.7 -  let
     8.8 -    val unfold_rex_tac = unfold_tac @{thms rex_def};
     8.9 -    fun prove_rex_tac ctxt = unfold_rex_tac ctxt THEN Quantifier1.prove_one_point_ex_tac;
    8.10 -  in fn _ => fn ctxt => Quantifier1.rearrange_bex (prove_rex_tac ctxt) ctxt end
    8.11 +  fn _ => Quantifier1.rearrange_bex
    8.12 +    (fn ctxt =>
    8.13 +      unfold_tac ctxt @{thms rex_def} THEN
    8.14 +      Quantifier1.prove_one_point_ex_tac)
    8.15  *}
    8.16  
    8.17  simproc_setup defined_rall ("\<forall>x[M]. P(x) \<longrightarrow> Q(x)") = {*
    8.18 -  let
    8.19 -    val unfold_rall_tac = unfold_tac @{thms rall_def};
    8.20 -    fun prove_rall_tac ctxt = unfold_rall_tac ctxt THEN Quantifier1.prove_one_point_all_tac;
    8.21 -  in fn _ => fn ctxt => Quantifier1.rearrange_ball (prove_rall_tac ctxt) ctxt end
    8.22 +  fn _ => Quantifier1.rearrange_ball
    8.23 +    (fn ctxt =>
    8.24 +      unfold_tac ctxt @{thms rall_def} THEN
    8.25 +      Quantifier1.prove_one_point_all_tac)
    8.26  *}
    8.27  
    8.28  end
     9.1 --- a/src/ZF/pair.thy	Sun Jan 12 13:16:00 2014 +0100
     9.2 +++ b/src/ZF/pair.thy	Sun Jan 12 14:32:22 2014 +0100
     9.3 @@ -19,17 +19,17 @@
     9.4  ML {* val ZF_ss = simpset_of @{context} *}
     9.5  
     9.6  simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = {*
     9.7 -  let
     9.8 -    val unfold_bex_tac = unfold_tac @{thms Bex_def};
     9.9 -    fun prove_bex_tac ctxt = unfold_bex_tac ctxt THEN Quantifier1.prove_one_point_ex_tac;
    9.10 -  in fn _ => fn ctxt => Quantifier1.rearrange_bex (prove_bex_tac ctxt) ctxt end
    9.11 +  fn _ => Quantifier1.rearrange_bex
    9.12 +    (fn ctxt =>
    9.13 +      unfold_tac ctxt @{thms Bex_def} THEN
    9.14 +      Quantifier1.prove_one_point_ex_tac)
    9.15  *}
    9.16  
    9.17  simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = {*
    9.18 -  let
    9.19 -    val unfold_ball_tac = unfold_tac @{thms Ball_def};
    9.20 -    fun prove_ball_tac ctxt = unfold_ball_tac ctxt THEN Quantifier1.prove_one_point_all_tac;
    9.21 -  in fn _ => fn ctxt => Quantifier1.rearrange_ball (prove_ball_tac ctxt) ctxt end
    9.22 +  fn _ => Quantifier1.rearrange_ball
    9.23 +    (fn ctxt =>
    9.24 +      unfold_tac ctxt @{thms Ball_def} THEN
    9.25 +      Quantifier1.prove_one_point_all_tac)
    9.26  *}
    9.27  
    9.28