Eliminated dependency of Funs_rangeE on SOME.
authorberghofe
Tue Aug 07 19:26:42 2001 +0200 (2001-08-07)
changeset 11470d3a3be6660f9
parent 11469 57b072f00626
child 11471 ba2c252b55ad
Eliminated dependency of Funs_rangeE on SOME.
src/HOL/Datatype_Universe.ML
     1.1 --- a/src/HOL/Datatype_Universe.ML	Tue Aug 07 17:21:58 2001 +0200
     1.2 +++ b/src/HOL/Datatype_Universe.ML	Tue Aug 07 19:26:42 2001 +0200
     1.3 @@ -402,12 +402,16 @@
     1.4  by (rtac (p1 RS FunsD) 1);
     1.5  qed "Funs_inv";
     1.6  
     1.7 -val [p1, p2] = Goalw [o_def]
     1.8 -     "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
     1.9 -by (res_inst_tac [("h", "%x. @y. (f::'a=>'b) x = g y")] p2 1);
    1.10 +val [p1, p2, p3] = Goalw [o_def]
    1.11 +     "[| inj g; f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
    1.12 +by (res_inst_tac [("h", "%x. THE y. (f::'c=>'b) x = g y")] p3 1);
    1.13  by (rtac ext 1);
    1.14 -by (rtac (p1 RS FunsD RS rangeE) 1);
    1.15 -by (etac (exI RS (some_eq_ex RS iffD2)) 1);
    1.16 +by (rtac (p2 RS FunsD RS rangeE) 1);
    1.17 +by (rtac theI 1);
    1.18 +by (atac 1);
    1.19 +by (rtac (p1 RS injD) 1);
    1.20 +by (etac (sym RS trans) 1);
    1.21 +by (atac 1);
    1.22  qed "Funs_rangeE";
    1.23  
    1.24  Goal "a : S ==> (%x. a) : Funs S";