removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
authoroheimb
Thu Jan 08 17:47:22 1998 +0100 (1998-01-08)
changeset 45274878fb3d0ac5
parent 4526 6be35399125a
child 4528 ff22e16c5f2f
removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
src/HOL/HOL.ML
     1.1 --- a/src/HOL/HOL.ML	Thu Jan 08 17:44:50 1998 +0100
     1.2 +++ b/src/HOL/HOL.ML	Thu Jan 08 17:47:22 1998 +0100
     1.3 @@ -159,7 +159,7 @@
     1.4  (** Existential quantifier **)
     1.5  section "?";
     1.6  
     1.7 -qed_goalw "exI" HOL.thy [Ex_def] "P(x) ==> ? x::'a. P(x)"
     1.8 +qed_goalw "exI" HOL.thy [Ex_def] "P x ==> ? x::'a. P x"
     1.9   (fn prems => [rtac selectI 1, resolve_tac prems 1]);
    1.10  
    1.11  qed_goalw "exE" HOL.thy [Ex_def]
    1.12 @@ -256,23 +256,23 @@
    1.13  
    1.14  (*Easier to apply than selectI: conclusion has only one occurrence of P*)
    1.15  qed_goal "selectI2" HOL.thy
    1.16 -    "[| P(a);  !!x. P(x) ==> Q(x) |] ==> Q(@x. P(x))"
    1.17 +    "[| P a;  !!x. P x ==> Q x |] ==> Q (@x. P x)"
    1.18   (fn prems => [ resolve_tac prems 1, 
    1.19                  rtac selectI 1, 
    1.20                  resolve_tac prems 1 ]);
    1.21  
    1.22  (*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
    1.23  qed_goal "selectI2EX" HOL.thy
    1.24 -  "[| ? a. P a; !!x. P x ==> Q x |] ==> Q(Eps P)"
    1.25 +  "[| ? a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"
    1.26  (fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
    1.27  
    1.28  qed_goal "select_equality" HOL.thy
    1.29 -    "[| P(a);  !!x. P(x) ==> x=a |] ==> (@x. P(x)) = a"
    1.30 +    "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a"
    1.31   (fn prems => [ rtac selectI2 1, 
    1.32                  REPEAT (ares_tac prems 1) ]);
    1.33  
    1.34  qed_goalw "select1_equality" HOL.thy [Ex1_def]
    1.35 -  "!!P. [| ?!x. P(x); P(a) |] ==> (@x. P(x)) = a" (K [
    1.36 +  "!!P. [| ?!x. P x; P a |] ==> (@x. P x) = a" (K [
    1.37  	  rtac select_equality 1, atac 1,
    1.38            etac exE 1, etac conjE 1,
    1.39            rtac allE 1, atac 1,
    1.40 @@ -286,22 +286,6 @@
    1.41          etac exE 1,
    1.42          etac selectI 1]);
    1.43  
    1.44 -val Eps_eq = prove_goal HOL.thy "Eps (op = x) = x" (K [
    1.45 -	rtac select_equality 1, rtac refl 1, etac sym 1]);
    1.46 -
    1.47 -val ex1_Eps_eq = prove_goal HOL.thy "!!X. [|?!x. P x; P y|] ==> Eps P = y" (K [
    1.48 -	rtac select_equality 1,
    1.49 -	 atac 1,
    1.50 -	etac ex1E 1,
    1.51 -	etac all_dupE 1,
    1.52 -	etac impE 1,
    1.53 -	 atac 1,
    1.54 -	rtac trans 1,
    1.55 -	 etac sym 2,
    1.56 -	dtac spec 1,
    1.57 -	etac impE 1,
    1.58 -	 ALLGOALS atac]);
    1.59 -
    1.60  
    1.61  (** Classical intro rules for disjunction and existential quantifiers *)
    1.62  section "classical intro rules";