# HG changeset patch
# User nipkow
# Date 985338653 -3600
# Node ID db536a42dfc5f6df4133af2284761de4a9e2ba60
# Parent  c4c210e7c89cc2616556cbf0d7bfc1e772ea8982
added one point simprocs for bounded quantifiers

diff -r c4c210e7c89c -r db536a42dfc5 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Mar 22 10:29:26 2001 +0100
+++ b/src/HOL/IsaMakefile	Fri Mar 23 10:10:53 2001 +0100
@@ -59,7 +59,8 @@
 Pure:
 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
-$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
+$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/quantifier1.ML \
+  $(SRC)/Provers/Arith/abel_cancel.ML \
   $(SRC)/Provers/Arith/assoc_fold.ML \
   $(SRC)/Provers/Arith/cancel_numerals.ML \
   $(SRC)/Provers/Arith/cancel_sums.ML \
diff -r c4c210e7c89c -r db536a42dfc5 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Mar 22 10:29:26 2001 +0100
+++ b/src/HOL/Set.ML	Fri Mar 23 10:10:53 2001 +0100
@@ -100,6 +100,45 @@
 
 Addsimps [ball_triv, bex_triv];
 
+Goalw [Bex_def] "(ALL x:A. x=a --> P x) = (a:A --> P a)";
+by(Blast_tac 1);
+qed "ball_one_point";
+
+Goal "(EX x:A. x=a & P x) = (a:A & P a)";
+by(Blast_tac 1);
+qed "bex_one_point";
+
+Addsimps [ball_one_point,bex_one_point];
+
+let
+val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
+    ("EX x:A. P(x) & Q(x)",HOLogic.boolT)
+
+val prove_bex_tac = rewrite_goals_tac [Bex_def] THEN
+                    Quantifier1.prove_one_point_ex_tac;
+
+val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
+
+val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
+    ("ALL x:A. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
+
+val swap = prove_goal thy
+  "((!x. Q x --> P x --> R x) = S) ==> ((!x. P x --> Q x --> R x) = S)"
+  (fn ths => [cut_facts_tac ths 1, Blast_tac 1]);
+
+val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN rtac swap 1 THEN
+                     Quantifier1.prove_one_point_all_tac;
+
+val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
+
+val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex;
+val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball;
+in
+
+Addsimprocs [defBALL_regroup,defBEX_regroup]
+
+end;
+
 (** Congruence rules **)
 
 val prems = Goalw [Ball_def]
diff -r c4c210e7c89c -r db536a42dfc5 src/HOL/UNITY/PPROD.ML
--- a/src/HOL/UNITY/PPROD.ML	Thu Mar 22 10:29:26 2001 +0100
+++ b/src/HOL/UNITY/PPROD.ML	Fri Mar 23 10:10:53 2001 +0100
@@ -103,7 +103,6 @@
 \     ==> (PLam I F : preserves (v o sub j o fst)) = \
 \         (if j: I then F j : preserves (v o fst) else True)";
 by (asm_simp_tac (simpset() addsimps [PLam_def, lift_preserves_sub]) 1);
-by (Blast_tac 1);
 qed "PLam_preserves_fst";
 Addsimps [PLam_preserves_fst];
 
diff -r c4c210e7c89c -r db536a42dfc5 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Mar 22 10:29:26 2001 +0100
+++ b/src/HOL/simpdata.ML	Fri Mar 23 10:10:53 2001 +0100
@@ -284,17 +284,15 @@
 end);
 
 local
-val ex_pattern =
-  Thm.read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)",HOLogic.boolT)
-
-val all_pattern =
-  Thm.read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
-
+val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
+    ("EX x. P(x) & Q(x)",HOLogic.boolT)
+val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
+    ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
 in
-val defEX_regroup =
-  mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
-val defALL_regroup =
-  mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
+val defEX_regroup = mk_simproc "defined EX" [ex_pattern]
+      Quantifier1.rearrange_ex
+val defALL_regroup = mk_simproc "defined ALL" [all_pattern]
+      Quantifier1.rearrange_all
 end;