# HG changeset patch
# User paulson
# Date 960372396 -7200
# Node ID 3730ae0f513a28a1e475eb44050d685e8c4457ea
# Parent  249c135057d773c680e1effb86fed0895ed4eb3a
tidied

diff -r 249c135057d7 -r 3730ae0f513a src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Tue Jun 06 20:32:10 2000 +0200
+++ b/src/HOL/Arith.ML	Wed Jun 07 12:06:36 2000 +0200
@@ -150,7 +150,7 @@
 (**** Additional theorems about "less than" ****)
 
 (*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
-Goal "m<n --> (? k. n=Suc(m+k))";
+Goal "m<n --> (EX k. n=Suc(m+k))";
 by (induct_tac "n" 1);
 by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less])));
 by (blast_tac (claset() addSEs [less_SucE] 
@@ -171,7 +171,7 @@
 bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
 bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
 
-Goal "(m<n) = (? k. n=Suc(m+k))";
+Goal "(m<n) = (EX k. n=Suc(m+k))";
 by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1);
 qed "less_iff_Suc_add";
 
@@ -449,12 +449,12 @@
 qed "zero_less_diff";
 Addsimps [zero_less_diff];
 
-Goal "i < j  ==> ? k::nat. 0<k & i+k = j";
+Goal "i < j  ==> EX k::nat. 0<k & i+k = j";
 by (res_inst_tac [("x","j - i")] exI 1);
 by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1);
 qed "less_imp_add_positive";
 
-Goal "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
+Goal "P(k) --> (ALL n. P(Suc(n))--> P(n)) --> P(k-i)";
 by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
 by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
 qed "zero_induct_lemma";
@@ -1002,8 +1002,6 @@
 by (auto_tac (claset(), simpset() addsimps [diff_is_0_eq RS iffD2]));
 qed "nat_diff_split";
 
-val nat_diff_split = nat_diff_split;
-
 (* FIXME: K true should be replaced by a sensible test to speed things up
    in case there are lots of irrelevant terms involved;
    elimination of min/max can be optimized:
diff -r 249c135057d7 -r 3730ae0f513a src/HOL/Set.ML
--- a/src/HOL/Set.ML	Tue Jun 06 20:32:10 2000 +0200
+++ b/src/HOL/Set.ML	Wed Jun 07 12:06:36 2000 +0200
@@ -40,23 +40,23 @@
 section "Bounded quantifiers";
 
 val prems = Goalw [Ball_def]
-    "[| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)";
+    "[| !!x. x:A ==> P(x) |] ==> ALL x:A. P(x)";
 by (REPEAT (ares_tac (prems @ [allI,impI]) 1));
 qed "ballI";
 
 bind_thms ("strip", [impI, allI, ballI]);
 
-Goalw [Ball_def] "[| ! x:A. P(x);  x:A |] ==> P(x)";
+Goalw [Ball_def] "[| ALL x:A. P(x);  x:A |] ==> P(x)";
 by (Blast_tac 1);
 qed "bspec";
 
 val major::prems = Goalw [Ball_def]
-    "[| ! x:A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q";
+    "[| ALL x:A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q";
 by (rtac (major RS spec RS impCE) 1);
 by (REPEAT (eresolve_tac prems 1));
 qed "ballE";
 
-(*Takes assumptions ! x:A.P(x) and a:A; creates assumption P(a)*)
+(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
 fun ball_tac i = etac ballE i THEN contr_tac (i+1);
 
 AddSIs [ballI];
@@ -67,23 +67,23 @@
 			 (dtac bspec THEN' atac) APPEND' tac2);
 
 (*Normally the best argument order: P(x) constrains the choice of x:A*)
-Goalw [Bex_def] "[| P(x);  x:A |] ==> ? x:A. P(x)";
+Goalw [Bex_def] "[| P(x);  x:A |] ==> EX x:A. P(x)";
 by (Blast_tac 1);
 qed "bexI";
 
 (*The best argument order when there is only one x:A*)
-Goalw [Bex_def] "[| x:A;  P(x) |] ==> ? x:A. P(x)";
+Goalw [Bex_def] "[| x:A;  P(x) |] ==> EX x:A. P(x)";
 by (Blast_tac 1);
 qed "rev_bexI";
 
 val prems = Goal 
-   "[| ! x:A. ~P(x) ==> P(a);  a:A |] ==> ? x:A. P(x)";
+   "[| ALL x:A. ~P(x) ==> P(a);  a:A |] ==> EX x:A. P(x)";
 by (rtac classical 1);
 by (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1))  ;
 qed "bexCI";
 
 val major::prems = Goalw [Bex_def]
-    "[| ? x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q";
+    "[| EX x:A. P(x);  !!x. [| x:A; P(x) |] ==> Q  |] ==> Q";
 by (rtac (major RS exE) 1);
 by (REPEAT (eresolve_tac (prems @ [asm_rl,conjE]) 1));
 qed "bexE";
@@ -92,12 +92,12 @@
 AddSEs [bexE];
 
 (*Trival rewrite rule*)
-Goal "(! x:A. P) = ((? x. x:A) --> P)";
+Goal "(ALL x:A. P) = ((EX x. x:A) --> P)";
 by (simp_tac (simpset() addsimps [Ball_def]) 1);
 qed "ball_triv";
 
 (*Dual form for existentials*)
-Goal "(? x:A. P) = ((? x. x:A) & P)";
+Goal "(EX x:A. P) = ((EX x. x:A) & P)";
 by (simp_tac (simpset() addsimps [Bex_def]) 1);
 qed "bex_triv";
 
@@ -107,13 +107,13 @@
 
 val prems = Goalw [Ball_def]
     "[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
-\    (! x:A. P(x)) = (! x:B. Q(x))";
+\    (ALL x:A. P(x)) = (ALL x:B. Q(x))";
 by (asm_simp_tac (simpset() addsimps prems) 1);
 qed "ball_cong";
 
 val prems = Goalw [Bex_def]
     "[| A=B;  !!x. x:B ==> P(x) = Q(x) |] ==> \
-\    (? x:A. P(x)) = (? x:B. Q(x))";
+\    (EX x:A. P(x)) = (EX x:B. Q(x))";
 by (asm_simp_tac (simpset() addcongs [conj_cong] addsimps prems) 1);
 qed "bex_cong";
 
@@ -212,6 +212,11 @@
 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
 qed "equalityE";
 
+(*This could be tried.  Most things build fine with it.  However, some proofs
+  become very slow or even fail.
+  AddEs [equalityE];
+*)
+
 val major::prems = Goal
     "[| A = B;  [| c:A; c:B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P";
 by (rtac (major RS equalityE) 1);
@@ -290,6 +295,7 @@
 by (Blast_tac 1) ;
 qed "equals0D";
 
+(* [| A = {};  a : A |] ==> R *)
 AddDs [equals0D, sym RS equals0D];
 
 Goalw [Ball_def] "Ball {} P = True";
@@ -473,7 +479,7 @@
 AddSIs [insertCI]; 
 AddSEs [insertE];
 
-Goal "A <= insert x B ==> A <= B & x ~: A | (? B'. A = insert x B' & B' <= B)";
+Goal "A <= insert x B ==> A <= B & x ~: A | (EX B'. A = insert x B' & B' <= B)";
 by (case_tac "x:A" 1);
 by  (Fast_tac 2);
 by (rtac disjI2 1);
@@ -732,7 +738,16 @@
 val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
                  mem_Collect_eq, UN_iff, Union_iff, INT_iff, Inter_iff];
 
-val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
+(*Would like to add these, but the existing code only searches for the 
+  outer-level constant, which in this case is just "op :"; we instead need
+  to use term-nets to associate patterns with rules.  Also, if a rule fails to
+  apply, then the formula should be kept.
+  [("uminus", Compl_iff RS iffD1), ("op -", [Diff_iff RS iffD1]), 
+   ("op Int", [IntD1,IntD2]),
+   ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
+ *)
+val mksimps_pairs =
+  [("Ball",[bspec])] @ mksimps_pairs;
 
 simpset_ref() := simpset() setmksimps (mksimps mksimps_pairs);