--- a/src/FOL/FOL.thy Sun May 24 21:11:23 2020 +0200
+++ b/src/FOL/FOL.thy Sun May 24 19:57:13 2020 +0000
@@ -337,8 +337,8 @@
ML_file \<open>simpdata.ML\<close>
-simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_ex\<close>
-simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_all\<close>
+simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_Ex\<close>
+simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_All\<close>
ML \<open>
(*intuitionistic simprules only*)
--- a/src/HOL/HOL.thy Sun May 24 21:11:23 2020 +0200
+++ b/src/HOL/HOL.thy Sun May 24 19:57:13 2020 +0000
@@ -1198,8 +1198,8 @@
Simplifier.method_setup Splitter.split_modifiers
\<close>
-simproc_setup defined_Ex ("\<exists>x. P x") = \<open>K Quantifier1.rearrange_ex\<close>
-simproc_setup defined_All ("\<forall>x. P x") = \<open>K Quantifier1.rearrange_all\<close>
+simproc_setup defined_Ex ("\<exists>x. P x") = \<open>K Quantifier1.rearrange_Ex\<close>
+simproc_setup defined_All ("\<forall>x. P x") = \<open>K Quantifier1.rearrange_All\<close>
text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
--- a/src/HOL/Library/Quantified_Premise_Simproc.thy Sun May 24 21:11:23 2020 +0200
+++ b/src/HOL/Library/Quantified_Premise_Simproc.thy Sun May 24 19:57:13 2020 +0000
@@ -4,6 +4,6 @@
imports Main
begin
-simproc_setup defined_forall ("\<And>x. PROP P x") = \<open>K Quantifier1.rearrange_All\<close>
+simproc_setup defined_all ("\<And>x. PROP P x") = \<open>K Quantifier1.rearrange_all\<close>
end
--- a/src/HOL/Set.thy Sun May 24 21:11:23 2020 +0200
+++ b/src/HOL/Set.thy Sun May 24 19:57:13 2020 +0000
@@ -330,17 +330,13 @@
\<close>
simproc_setup defined_Bex ("\<exists>x\<in>A. P x \<and> Q x") = \<open>
- fn _ => Quantifier1.rearrange_bex
- (fn ctxt =>
- unfold_tac ctxt @{thms Bex_def} THEN
- Quantifier1.prove_one_point_ex_tac ctxt)
+ fn _ => Quantifier1.rearrange_Bex
+ (fn ctxt => unfold_tac ctxt @{thms Bex_def})
\<close>
simproc_setup defined_All ("\<forall>x\<in>A. P x \<longrightarrow> Q x") = \<open>
- fn _ => Quantifier1.rearrange_ball
- (fn ctxt =>
- unfold_tac ctxt @{thms Ball_def} THEN
- Quantifier1.prove_one_point_all_tac ctxt)
+ fn _ => Quantifier1.rearrange_Ball
+ (fn ctxt => unfold_tac ctxt @{thms Ball_def})
\<close>
lemma ballI [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> P x) \<Longrightarrow> \<forall>x\<in>A. P x"
--- a/src/Provers/quantifier1.ML Sun May 24 21:11:23 2020 +0200
+++ b/src/Provers/quantifier1.ML Sun May 24 19:57:13 2020 +0000
@@ -64,13 +64,11 @@
signature QUANTIFIER1 =
sig
- val prove_one_point_all_tac: Proof.context -> tactic
- val prove_one_point_ex_tac: Proof.context -> tactic
val rearrange_all: Proof.context -> cterm -> thm option
val rearrange_All: Proof.context -> cterm -> thm option
- val rearrange_ex: 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_Ball: (Proof.context -> tactic) -> Proof.context -> cterm -> thm option
+ val rearrange_Ex: 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;
@@ -158,7 +156,7 @@
local
val excomm = Data.ex_comm RS Data.iff_trans;
in
- fun prove_one_point_ex_tac ctxt =
+ fun prove_one_point_Ex_tac ctxt =
qcomm_tac ctxt excomm Data.iff_exI 1 THEN resolve_tac ctxt [Data.iffI] 1 THEN
ALLGOALS
(EVERY' [eresolve_tac ctxt [Data.exE], REPEAT_DETERM o eresolve_tac ctxt [Data.conjE],
@@ -180,13 +178,13 @@
val all_comm = Data.all_comm RS Data.iff_trans;
val All_comm = @{thm swap_params [THEN transitive]};
in
- fun prove_one_point_all_tac ctxt =
+ fun prove_one_point_All_tac ctxt =
EVERY1 [qcomm_tac ctxt all_comm Data.iff_allI,
resolve_tac ctxt [Data.iff_allI],
resolve_tac ctxt [Data.iffI],
tac ctxt,
tac ctxt];
- fun prove_one_point_All_tac ctxt =
+ fun prove_one_point_all_tac ctxt =
EVERY1 [qcomm_tac ctxt All_comm @{thm equal_allI},
resolve_tac ctxt [@{thm equal_allI}],
resolve_tac ctxt [@{thm equal_intr_rule}],
@@ -222,24 +220,24 @@
fun rearrange_all ctxt ct =
(case Thm.term_of ct of
F as (all as Const (q, _)) $ Abs (x, T, P) =>
- (case extract_quant ctxt (K extract_imp) q P of
+ (case extract_quant ctxt extract_implies q P of
NONE => NONE
| SOME (xs, eq, Q) =>
- let val R = quantify all x T xs (Data.imp $ eq $ Q)
- in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_all_tac)) end)
+ let val R = quantify all x T xs (Logic.implies $ eq $ Q)
+ in SOME (prove_conv ctxt (F, R) prove_one_point_all_tac) end)
| _ => NONE);
fun rearrange_All ctxt ct =
(case Thm.term_of ct of
F as (all as Const (q, _)) $ Abs (x, T, P) =>
- (case extract_quant ctxt extract_implies q P of
+ (case extract_quant ctxt (K extract_imp) q P of
NONE => NONE
| SOME (xs, eq, Q) =>
- let val R = quantify all x T xs (Logic.implies $ eq $ Q)
- in SOME (prove_conv ctxt (F, R) prove_one_point_All_tac) end)
+ let val R = quantify all x T xs (Data.imp $ eq $ Q)
+ in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_All_tac)) end)
| _ => NONE);
-fun rearrange_ball tac ctxt ct =
+fun rearrange_Ball tac ctxt ct =
(case Thm.term_of ct of
F as Ball $ A $ Abs (x, T, P) =>
(case extract_imp true [] P of
@@ -248,27 +246,29 @@
if not (null xs) then NONE
else
let val R = Data.imp $ eq $ Q
- in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) (iff_reflection_tac THEN' tac)) end)
+ in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R))
+ (iff_reflection_tac THEN' tac THEN' prove_one_point_All_tac)) end)
| _ => NONE);
-fun rearrange_ex ctxt ct =
+fun rearrange_Ex ctxt ct =
(case Thm.term_of ct of
F as (ex as Const (q, _)) $ Abs (x, T, P) =>
(case extract_quant ctxt (K extract_conj) q P of
NONE => NONE
| SOME (xs, eq, Q) =>
let val R = quantify ex x T xs (Data.conj $ eq $ Q)
- in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_ex_tac)) end)
+ in SOME (prove_conv ctxt (F, R) (iff_reflection_tac THEN' prove_one_point_Ex_tac)) end)
| _ => NONE);
-fun rearrange_bex tac ctxt ct =
+fun rearrange_Bex tac ctxt ct =
(case Thm.term_of ct of
F as Bex $ A $ Abs (x, T, P) =>
(case extract_conj true [] P of
NONE => NONE
| SOME (xs, eq, Q) =>
if not (null xs) then NONE
- else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) (iff_reflection_tac THEN' tac)))
+ else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q))
+ (iff_reflection_tac THEN' tac THEN' prove_one_point_Ex_tac)))
| _ => NONE);
fun rearrange_Collect tac ctxt ct =
--- a/src/ZF/OrdQuant.thy Sun May 24 21:11:23 2020 +0200
+++ b/src/ZF/OrdQuant.thy Sun May 24 19:57:13 2020 +0000
@@ -350,17 +350,13 @@
text \<open>Setting up the one-point-rule simproc\<close>
simproc_setup defined_rex ("\<exists>x[M]. P(x) & Q(x)") = \<open>
- fn _ => Quantifier1.rearrange_bex
- (fn ctxt =>
- unfold_tac ctxt @{thms rex_def} THEN
- Quantifier1.prove_one_point_ex_tac ctxt)
+ fn _ => Quantifier1.rearrange_Bex
+ (fn ctxt => unfold_tac ctxt @{thms rex_def})
\<close>
simproc_setup defined_rall ("\<forall>x[M]. P(x) \<longrightarrow> Q(x)") = \<open>
- fn _ => Quantifier1.rearrange_ball
- (fn ctxt =>
- unfold_tac ctxt @{thms rall_def} THEN
- Quantifier1.prove_one_point_all_tac ctxt)
+ fn _ => Quantifier1.rearrange_Ball
+ (fn ctxt => unfold_tac ctxt @{thms rall_def})
\<close>
end
--- a/src/ZF/pair.thy Sun May 24 21:11:23 2020 +0200
+++ b/src/ZF/pair.thy Sun May 24 19:57:13 2020 +0000
@@ -19,17 +19,13 @@
ML \<open>val ZF_ss = simpset_of \<^context>\<close>
simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = \<open>
- fn _ => Quantifier1.rearrange_bex
- (fn ctxt =>
- unfold_tac ctxt @{thms Bex_def} THEN
- Quantifier1.prove_one_point_ex_tac ctxt)
+ fn _ => Quantifier1.rearrange_Bex
+ (fn ctxt => unfold_tac ctxt @{thms Bex_def})
\<close>
simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = \<open>
- fn _ => Quantifier1.rearrange_ball
- (fn ctxt =>
- unfold_tac ctxt @{thms Ball_def} THEN
- Quantifier1.prove_one_point_all_tac ctxt)
+ fn _ => Quantifier1.rearrange_Ball
+ (fn ctxt => unfold_tac ctxt @{thms Ball_def})
\<close>