# HG changeset patch
# User paulson
# Date 962181542 -7200
# Node ID 902ea754eee21a90cfdb9f970b451a6269d96110
# Parent  084abf3d0eff230ca5a299d3db43255f8e249b81
rev_notE now makes strong elim rules;
tidied the file

diff -r 084abf3d0eff -r 902ea754eee2 src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Wed Jun 28 10:37:52 2000 +0200
+++ b/src/HOL/HOL_lemmas.ML	Wed Jun 28 10:39:02 2000 +0200
@@ -131,21 +131,21 @@
 (** Universal quantifier **)
 section "!";
 
-val prems = Goalw [All_def] "(!!x::'a. P(x)) ==> ! x. P(x)";
+val prems = Goalw [All_def] "(!!x::'a. P(x)) ==> ALL x. P(x)";
 by (resolve_tac (prems RL [eqTrueI RS ext]) 1);
 qed "allI";
 
-Goalw [All_def] "! x::'a. P(x) ==> P(x)";
+Goalw [All_def] "ALL x::'a. P(x) ==> P(x)";
 by (rtac eqTrueE 1);
 by (etac fun_cong 1);
 qed "spec";
 
-val major::prems= goal (the_context ()) "[| ! x. P(x);  P(x) ==> R |] ==> R";
+val major::prems= goal (the_context ()) "[| ALL x. P(x);  P(x) ==> R |] ==> R";
 by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ;
 qed "allE";
 
 val prems = goal (the_context ()) 
-    "[| ! x. P(x);  [| P(x); ! x. P(x) |] ==> R |] ==> R";
+    "[| ALL x. P(x);  [| P(x); ALL x. P(x) |] ==> R |] ==> R";
 by (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ;
 qed "all_dupE";
 
@@ -187,12 +187,8 @@
 by (assume_tac 1);
 qed "notE";
 
-bind_thm ("classical2", notE RS notI);
-
-Goal "[| P; ~P |] ==> R";
-by (etac notE 1);
-by (assume_tac 1);
-qed "rev_notE";
+(* Alternative ~ introduction rule: [| P ==> ~ Pa; P ==> Pa |] ==> ~ P *)
+bind_thm ("notI2", notE RS notI);
 
 
 (** Implication **)
@@ -217,19 +213,19 @@
 by (etac major 1) ;
 qed "rev_contrapos";
 
-(* ~(?t = ?s) ==> ~(?s = ?t) *)
+(* t ~= s ==> s ~= t *)
 bind_thm("not_sym", sym COMP rev_contrapos);
 
 
 (** Existential quantifier **)
-section "?";
+section "EX ";
 
-Goalw [Ex_def] "P x ==> ? x::'a. P x";
+Goalw [Ex_def] "P x ==> EX x::'a. P x";
 by (etac selectI 1) ;
 qed "exI";
 
 val [major,minor] = 
-Goalw [Ex_def] "[| ? x::'a. P(x); !!x. P(x) ==> Q |] ==> Q";
+Goalw [Ex_def] "[| EX x::'a. P(x); !!x. P(x) ==> Q |] ==> Q";
 by (rtac (major RS minor) 1);
 qed "exE";
 
@@ -301,6 +297,13 @@
 
 bind_thm ("ccontr", FalseE RS classical);
 
+(*notE with premises exchanged; it discharges ~R so that it can be used to
+  make elimination rules*)
+val [premp,premnot] = Goal "[| P; ~R ==> ~P |] ==> R";
+by (rtac ccontr 1);
+by (etac ([premnot,premp] MRS notE) 1);
+qed "rev_notE";
+
 (*Double negation law*)
 Goal "~~P ==> P";
 by (rtac classical 1);
@@ -323,26 +326,26 @@
 qed "swap2";
 
 (** Unique existence **)
-section "?!";
+section "EX!";
 
-val prems = Goalw [Ex1_def] "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)";
+val prems = Goalw [Ex1_def] "[| P(a);  !!x. P(x) ==> x=a |] ==> EX! x. P(x)";
 by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1));
 qed "ex1I";
 
 (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
 val [ex_prem,eq] = Goal
-    "[| ? x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)";
+    "[| EX x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)";
 by (rtac (ex_prem RS exE) 1);
 by (REPEAT (ares_tac [ex1I,eq] 1)) ;
 qed "ex_ex1I";
 
 val major::prems = Goalw [Ex1_def]
-    "[| ?! x. P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R";
+    "[| EX! x. P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R";
 by (rtac (major RS exE) 1);
 by (REPEAT (etac conjE 1 ORELSE ares_tac prems 1));
 qed "ex1E";
 
-Goal "?! x. P x ==> ? x. P x";
+Goal "EX! x. P x ==> EX x. P x";
 by (etac ex1E 1);
 by (rtac exI 1);
 by (assume_tac 1);
@@ -361,7 +364,7 @@
 qed "selectI2";
 
 (*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
-val [major,minor] = Goal "[| ? a. P a;  !!x. P x ==> Q x |] ==> Q (Eps P)";
+val [major,minor] = Goal "[| EX a. P a;  !!x. P x ==> Q x |] ==> Q (Eps P)";
 by (rtac (major RS exE) 1);
 by (etac selectI2 1 THEN etac minor 1);
 qed "selectI2EX";
@@ -372,7 +375,7 @@
 by (REPEAT (ares_tac prems 1)) ;
 qed "select_equality";
 
-Goalw [Ex1_def] "[| ?!x. P x; P a |] ==> (@x. P x) = a";
+Goalw [Ex1_def] "[| EX!x. P x; P a |] ==> (@x. P x) = a";
 by (rtac select_equality 1);
 by (atac 1);
 by (etac exE 1);
@@ -387,7 +390,7 @@
 by (atac 1);
 qed "select1_equality";
 
-Goal "P (@ x. P x) =  (? x. P x)";
+Goal "P (@ x. P x) =  (EX x. P x)";
 by (rtac iffI 1);
 by (etac exI 1);
 by (etac exE 1);
@@ -446,7 +449,7 @@
 	    (eresolve_tac ([asm_rl,impCE,notE]@prems) 1)));
 qed "iffCE";
 
-val prems = Goal "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)";
+val prems = Goal "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)";
 by (rtac ccontr 1);
 by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ;
 qed "exCI";
@@ -500,7 +503,7 @@
 
 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
 
-(** strip ! and --> from proved goal while preserving !-bound var names **)
+(** strip ALL and --> from proved goal while preserving ALL-bound var names **)
 
 (** THIS CODE IS A MESS!!! **)