# HG changeset patch
# User wenzelm
# Date 1389533542 -3600
# Node ID 8601434fa33401a9ff25cb4a58f5cbcb6054cbfd
# Parent  811c35e81ac555e2b97c58616e06f0b92ae30d54
tuned signature;
clarified context;

diff -r 811c35e81ac5 -r 8601434fa334 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Sun Jan 12 13:16:00 2014 +0100
+++ b/src/FOL/simpdata.ML	Sun Jan 12 14:32:22 2014 +0100
@@ -123,7 +123,7 @@
   |> Simplifier.set_mkcong mk_meta_cong
   |> simpset_of;
 
-fun unfold_tac ths ctxt =
+fun unfold_tac ctxt ths =
   ALLGOALS (full_simp_tac (clear_simpset (put_simpset FOL_basic_ss ctxt) addsimps ths));
 
 
diff -r 811c35e81ac5 -r 8601434fa334 src/HOL/BNF/Tools/bnf_def_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Sun Jan 12 13:16:00 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Sun Jan 12 14:32:22 2014 +0100
@@ -186,10 +186,10 @@
 fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} =
   if null set_maps then atac 1
   else
-    unfold_tac [in_rel] ctxt THEN
+    unfold_tac ctxt [in_rel] THEN
     REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN
     hyp_subst_tac ctxt 1 THEN
-    unfold_tac set_maps ctxt THEN
+    unfold_tac ctxt set_maps THEN
     EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]},
       CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1;
 
diff -r 811c35e81ac5 -r 8601434fa334 src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sun Jan 12 13:16:00 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Sun Jan 12 14:32:22 2014 +0100
@@ -782,7 +782,7 @@
 fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = IHs} =
   let val n = length ks;
   in
-    unfold_tac @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} ctxt THEN
+    unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
     EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2,
       EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong =>
         EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp),
diff -r 811c35e81ac5 -r 8601434fa334 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Jan 12 13:16:00 2014 +0100
+++ b/src/HOL/Set.thy	Sun Jan 12 14:32:22 2014 +0100
@@ -69,9 +69,9 @@
 *}
 
 simproc_setup defined_Collect ("{x. P x & Q x}") = {*
-  fn _ =>
-    Quantifier1.rearrange_Collect
-     (rtac @{thm Collect_cong} 1 THEN
+  fn _ => Quantifier1.rearrange_Collect
+    (fn _ =>
+      rtac @{thm Collect_cong} 1 THEN
       rtac @{thm iffI} 1 THEN
       ALLGOALS
         (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
@@ -355,17 +355,17 @@
 *}
 
 simproc_setup defined_Bex ("EX x:A. P x & Q x") = {*
-  let
-    val unfold_bex_tac = unfold_tac @{thms Bex_def};
-    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
-  in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end
+  fn _ => Quantifier1.rearrange_bex
+    (fn ctxt =>
+      unfold_tac ctxt @{thms Bex_def} THEN
+      Quantifier1.prove_one_point_ex_tac)
 *}
 
 simproc_setup defined_All ("ALL x:A. P x --> Q x") = {*
-  let
-    val unfold_ball_tac = unfold_tac @{thms Ball_def};
-    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
-  in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end
+  fn _ => Quantifier1.rearrange_ball
+    (fn ctxt =>
+      unfold_tac ctxt @{thms Ball_def} THEN
+      Quantifier1.prove_one_point_all_tac)
 *}
 
 lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
diff -r 811c35e81ac5 -r 8601434fa334 src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Sun Jan 12 13:16:00 2014 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Sun Jan 12 14:32:22 2014 +0100
@@ -122,19 +122,14 @@
 
 (* General reduction pair application *)
 fun rem_inv_img ctxt =
-  let
-    val unfold_tac = Local_Defs.unfold_tac ctxt
-  in
-    rtac @{thm subsetI} 1
-    THEN etac @{thm CollectE} 1
-    THEN REPEAT (etac @{thm exE} 1)
-    THEN unfold_tac @{thms inv_image_def}
-    THEN rtac @{thm CollectI} 1
-    THEN etac @{thm conjE} 1
-    THEN etac @{thm ssubst} 1
-    THEN unfold_tac (@{thms split_conv} @ @{thms triv_forall_equality}
-                     @ @{thms sum.cases})
-  end
+  rtac @{thm subsetI} 1
+  THEN etac @{thm CollectE} 1
+  THEN REPEAT (etac @{thm exE} 1)
+  THEN Local_Defs.unfold_tac ctxt @{thms inv_image_def}
+  THEN rtac @{thm CollectI} 1
+  THEN etac @{thm conjE} 1
+  THEN etac @{thm ssubst} 1
+  THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.cases}
 
 (* Sets *)
 
@@ -289,9 +284,8 @@
          THEN (rtac @{thm rp_inv_image_rp} 1)
          THEN (rtac (order_rpair ms_rp label) 1)
          THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
-         THEN unfold_tac @{thms rp_inv_image_def} ctxt
-         THEN Local_Defs.unfold_tac ctxt
-           (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
+         THEN unfold_tac ctxt @{thms rp_inv_image_def}
+         THEN Local_Defs.unfold_tac ctxt @{thms split_conv fst_conv snd_conv}
          THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
          THEN EVERY (map (prove_lev true) sl)
          THEN EVERY (map (prove_lev false) (subtract (op =) sl (0 upto length cs - 1))))
diff -r 811c35e81ac5 -r 8601434fa334 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Sun Jan 12 13:16:00 2014 +0100
+++ b/src/HOL/Tools/simpdata.ML	Sun Jan 12 14:32:22 2014 +0100
@@ -178,7 +178,7 @@
 fun hol_simplify ctxt rews =
   Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps rews);
 
-fun unfold_tac ths ctxt =
+fun unfold_tac ctxt ths =
   ALLGOALS (full_simp_tac (clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps ths));
 
 end;
diff -r 811c35e81ac5 -r 8601434fa334 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Sun Jan 12 13:16:00 2014 +0100
+++ b/src/Provers/quantifier1.ML	Sun Jan 12 14:32:22 2014 +0100
@@ -68,9 +68,9 @@
   val prove_one_point_ex_tac: tactic
   val rearrange_all: Proof.context -> cterm -> thm option
   val rearrange_ex: Proof.context -> cterm -> thm option
-  val rearrange_ball: tactic -> Proof.context -> cterm -> thm option
-  val rearrange_bex: tactic -> Proof.context -> cterm -> thm option
-  val rearrange_Collect: tactic -> Proof.context -> cterm -> thm option
+  val rearrange_ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
+  val rearrange_bex: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
+  val rearrange_Collect: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
 end;
 
 functor Quantifier1(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
@@ -120,12 +120,13 @@
       | exqu xs P = extract (null xs) xs P
   in exqu [] end;
 
-fun prove_conv tac ctxt tu =
+fun prove_conv ctxt tu tac =
   let
     val (goal, ctxt') =
       yield_singleton (Variable.import_terms true) (Logic.mk_equals tu) ctxt;
     val thm =
-      Goal.prove ctxt' [] [] goal (K (rtac Data.iff_reflection 1 THEN tac));
+      Goal.prove ctxt' [] [] goal
+        (fn {context = ctxt'', ...} => rtac Data.iff_reflection 1 THEN tac ctxt'');
   in singleton (Variable.export ctxt' ctxt) thm end;
 
 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i);
@@ -178,7 +179,7 @@
         NONE => NONE
       | SOME (xs, eq, Q) =>
           let val R = quantify all x T xs (Data.imp $ eq $ Q)
-          in SOME (prove_conv prove_one_point_all_tac ctxt (F, R)) end)
+          in SOME (prove_conv ctxt (F, R) (K prove_one_point_all_tac)) end)
   | _ => NONE);
 
 fun rearrange_ball tac ctxt ct =
@@ -190,7 +191,7 @@
           if not (null xs) then NONE
           else
             let val R = Data.imp $ eq $ Q
-            in SOME (prove_conv tac ctxt (F, Ball $ A $ Abs (x, T, R))) end)
+            in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) tac) end)
   | _ => NONE);
 
 fun rearrange_ex ctxt ct =
@@ -200,7 +201,7 @@
         NONE => NONE
       | SOME (xs, eq, Q) =>
           let val R = quantify ex x T xs (Data.conj $ eq $ Q)
-          in SOME (prove_conv prove_one_point_ex_tac ctxt (F, R)) end)
+          in SOME (prove_conv ctxt (F, R) (K prove_one_point_ex_tac)) end)
   | _ => NONE);
 
 fun rearrange_bex tac ctxt ct =
@@ -210,7 +211,7 @@
         NONE => NONE
       | SOME (xs, eq, Q) =>
           if not (null xs) then NONE
-          else SOME (prove_conv tac ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q))))
+          else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) tac))
   | _ => NONE);
 
 fun rearrange_Collect tac ctxt ct =
@@ -220,7 +221,7 @@
         NONE => NONE
       | SOME (_, eq, Q) =>
           let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q)
-          in SOME (prove_conv tac ctxt (F, R)) end)
+          in SOME (prove_conv ctxt (F, R) tac) end)
   | _ => NONE);
 
 end;
diff -r 811c35e81ac5 -r 8601434fa334 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Sun Jan 12 13:16:00 2014 +0100
+++ b/src/ZF/OrdQuant.thy	Sun Jan 12 14:32:22 2014 +0100
@@ -368,17 +368,17 @@
 text {* Setting up the one-point-rule simproc *}
 
 simproc_setup defined_rex ("\<exists>x[M]. P(x) & Q(x)") = {*
-  let
-    val unfold_rex_tac = unfold_tac @{thms rex_def};
-    fun prove_rex_tac ctxt = unfold_rex_tac ctxt THEN Quantifier1.prove_one_point_ex_tac;
-  in fn _ => fn ctxt => Quantifier1.rearrange_bex (prove_rex_tac ctxt) ctxt end
+  fn _ => Quantifier1.rearrange_bex
+    (fn ctxt =>
+      unfold_tac ctxt @{thms rex_def} THEN
+      Quantifier1.prove_one_point_ex_tac)
 *}
 
 simproc_setup defined_rall ("\<forall>x[M]. P(x) \<longrightarrow> Q(x)") = {*
-  let
-    val unfold_rall_tac = unfold_tac @{thms rall_def};
-    fun prove_rall_tac ctxt = unfold_rall_tac ctxt THEN Quantifier1.prove_one_point_all_tac;
-  in fn _ => fn ctxt => Quantifier1.rearrange_ball (prove_rall_tac ctxt) ctxt end
+  fn _ => Quantifier1.rearrange_ball
+    (fn ctxt =>
+      unfold_tac ctxt @{thms rall_def} THEN
+      Quantifier1.prove_one_point_all_tac)
 *}
 
 end
diff -r 811c35e81ac5 -r 8601434fa334 src/ZF/pair.thy
--- a/src/ZF/pair.thy	Sun Jan 12 13:16:00 2014 +0100
+++ b/src/ZF/pair.thy	Sun Jan 12 14:32:22 2014 +0100
@@ -19,17 +19,17 @@
 ML {* val ZF_ss = simpset_of @{context} *}
 
 simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = {*
-  let
-    val unfold_bex_tac = unfold_tac @{thms Bex_def};
-    fun prove_bex_tac ctxt = unfold_bex_tac ctxt THEN Quantifier1.prove_one_point_ex_tac;
-  in fn _ => fn ctxt => Quantifier1.rearrange_bex (prove_bex_tac ctxt) ctxt end
+  fn _ => Quantifier1.rearrange_bex
+    (fn ctxt =>
+      unfold_tac ctxt @{thms Bex_def} THEN
+      Quantifier1.prove_one_point_ex_tac)
 *}
 
 simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = {*
-  let
-    val unfold_ball_tac = unfold_tac @{thms Ball_def};
-    fun prove_ball_tac ctxt = unfold_ball_tac ctxt THEN Quantifier1.prove_one_point_all_tac;
-  in fn _ => fn ctxt => Quantifier1.rearrange_ball (prove_ball_tac ctxt) ctxt end
+  fn _ => Quantifier1.rearrange_ball
+    (fn ctxt =>
+      unfold_tac ctxt @{thms Ball_def} THEN
+      Quantifier1.prove_one_point_all_tac)
 *}