added theorems for Eps
authoroheimb
Tue Nov 04 20:46:56 1997 +0100 (1997-11-04)
changeset 4131916641b59219
parent 4130 9fac2370a2f4
child 4132 daff3c9987cc
added theorems for Eps
src/HOL/HOL.ML
     1.1 --- a/src/HOL/HOL.ML	Tue Nov 04 17:16:26 1997 +0100
     1.2 +++ b/src/HOL/HOL.ML	Tue Nov 04 20:46:56 1997 +0100
     1.3 @@ -268,20 +268,36 @@
     1.4                  REPEAT (ares_tac prems 1) ]);
     1.5  
     1.6  qed_goalw "select1_equality" HOL.thy [Ex1_def]
     1.7 -  "!!P. [| ?!x. P(x); P(a) |] ==> (@x. P(x)) = a"
     1.8 -(fn _ => [rtac select_equality 1, atac 1,
     1.9 +  "!!P. [| ?!x. P(x); P(a) |] ==> (@x. P(x)) = a" (K [
    1.10 +	  rtac select_equality 1, atac 1,
    1.11            etac exE 1, etac conjE 1,
    1.12            rtac allE 1, atac 1,
    1.13            etac impE 1, atac 1, etac ssubst 1,
    1.14            etac allE 1, etac impE 1, atac 1, etac ssubst 1,
    1.15            rtac refl 1]);
    1.16  
    1.17 -qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) =  (? x. P x)" (fn prems => [
    1.18 +qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) =  (? x. P x)" (K [
    1.19          rtac iffI 1,
    1.20          etac exI 1,
    1.21          etac exE 1,
    1.22          etac selectI 1]);
    1.23  
    1.24 +val Eps_eq = prove_goal HOL.thy "Eps (op = x) = x" (K [
    1.25 +	rtac select_equality 1, rtac refl 1, etac sym 1]);
    1.26 +
    1.27 +val ex1_Eps_eq = prove_goal HOL.thy "!!X. [|?!x. P x; P y|] ==> Eps P = y" (K [
    1.28 +	rtac select_equality 1,
    1.29 +	 atac 1,
    1.30 +	etac ex1E 1,
    1.31 +	etac all_dupE 1,
    1.32 +	etac impE 1,
    1.33 +	 atac 1,
    1.34 +	rtac trans 1,
    1.35 +	 etac sym 2,
    1.36 +	dtac spec 1,
    1.37 +	etac impE 1,
    1.38 +	 ALLGOALS atac]);
    1.39 +
    1.40  
    1.41  (** Classical intro rules for disjunction and existential quantifiers *)
    1.42  section "classical intro rules";