--- 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 \
--- 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]
--- 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];
--- 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;