--- 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));
--- 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;
--- 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),
--- 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"
--- 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))))
--- 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;
--- 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;
--- 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
--- 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)
*}