src/HOL/HOL.ML
changeset 3646 a11338a5d2d4
parent 3621 d3e248853428
child 3842 b55686a7b22c
     1.1 --- a/src/HOL/HOL.ML	Fri Aug 08 11:22:59 1997 +0200
     1.2 +++ b/src/HOL/HOL.ML	Sun Aug 10 12:28:34 1997 +0200
     1.3 @@ -257,15 +257,24 @@
     1.4                  rtac selectI 1, 
     1.5                  resolve_tac prems 1 ]);
     1.6  
     1.7 +(*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
     1.8 +qed_goal "selectI2EX" HOL.thy
     1.9 +  "[| ? a.P a; !!x. P x ==> Q x |] ==> Q(Eps P)"
    1.10 +(fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
    1.11 +
    1.12  qed_goal "select_equality" HOL.thy
    1.13      "[| P(a);  !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a"
    1.14   (fn prems => [ rtac selectI2 1, 
    1.15                  REPEAT (ares_tac prems 1) ]);
    1.16  
    1.17 -(*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
    1.18 -qed_goal "selectI2EX" HOL.thy
    1.19 -  "[| ? a.P a; !!x. P x ==> Q x |] ==> Q(Eps P)"
    1.20 -(fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
    1.21 +qed_goalw "select1_equality" HOL.thy [Ex1_def]
    1.22 +  "!!P. [| ?!x.P(x); P(a) |] ==> (@x.P(x)) = a"
    1.23 +(fn _ => [rtac select_equality 1, atac 1,
    1.24 +          etac exE 1, etac conjE 1,
    1.25 +          rtac allE 1, atac 1,
    1.26 +          etac impE 1, atac 1, etac ssubst 1,
    1.27 +          etac allE 1, etac impE 1, atac 1, etac ssubst 1,
    1.28 +          rtac refl 1]);
    1.29  
    1.30  qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) =  (? x. P x)" (fn prems => [
    1.31          rtac iffI 1,