# HG changeset patch
# User haftmann
# Date 1590350233 0
# Node ID 4f46957579804f677dff030e5c595b8af3e25011
# Parent  45f85e283ce075981e52f02f612dbcd796e96d27
better closeup and more consistent terminology

diff -r 45f85e283ce0 -r 4f4695757980 src/FOL/FOL.thy
--- 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*)
diff -r 45f85e283ce0 -r 4f4695757980 src/HOL/HOL.thy
--- 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>
 
diff -r 45f85e283ce0 -r 4f4695757980 src/HOL/Library/Quantified_Premise_Simproc.thy
--- 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
diff -r 45f85e283ce0 -r 4f4695757980 src/HOL/Set.thy
--- 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"
diff -r 45f85e283ce0 -r 4f4695757980 src/Provers/quantifier1.ML
--- 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 =
diff -r 45f85e283ce0 -r 4f4695757980 src/ZF/OrdQuant.thy
--- 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
diff -r 45f85e283ce0 -r 4f4695757980 src/ZF/pair.thy
--- 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>