src/HOL/Relation.ML
changeset 11451 8abfb4f7bd02
parent 11136 e34e7f6d9b57
child 11655 923e4d0d36d5
     1.1 --- a/src/HOL/Relation.ML	Tue Jul 24 11:25:54 2001 +0200
     1.2 +++ b/src/HOL/Relation.ML	Wed Jul 25 13:13:01 2001 +0200
     1.3 @@ -333,7 +333,7 @@
     1.4  
     1.5  overload_1st_set "Relation.Image";
     1.6  
     1.7 -Goalw [Image_def] "b : r``A = (? x:A. (x,b):r)";
     1.8 +Goalw [Image_def] "b : r``A = (EX x:A. (x,b):r)";
     1.9  by (Blast_tac 1);
    1.10  qed "Image_iff";
    1.11  
    1.12 @@ -422,7 +422,7 @@
    1.13  section "single_valued";
    1.14  
    1.15  Goalw [single_valued_def]
    1.16 -     "!x y. (x,y):r --> (!z. (x,z):r --> y=z) ==> single_valued r";
    1.17 +     "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r";
    1.18  by (assume_tac 1);
    1.19  qed "single_valuedI";
    1.20  
    1.21 @@ -454,26 +454,18 @@
    1.22  by (Fast_tac 1);
    1.23  qed "fun_rel_comp_mono";
    1.24  
    1.25 -Goalw [fun_rel_comp_def] "! x. ?! y. (f x, y) : R ==> ?! g. g : fun_rel_comp f R";
    1.26 -by (res_inst_tac [("a","%x. @y. (f x, y) : R")] ex1I 1);
    1.27 -by (rtac CollectI 1);
    1.28 -by (rtac allI 1);
    1.29 -by (etac allE 1);
    1.30 -by (rtac (some_eq_ex RS iffD2) 1);
    1.31 -by (etac ex1_implies_ex 1);
    1.32 -by (rtac ext 1);
    1.33 -by (etac CollectE 1);
    1.34 -by (REPEAT (etac allE 1));
    1.35 -by (rtac (some1_equality RS sym) 1);
    1.36 -by (atac 1);
    1.37 -by (atac 1);
    1.38 +Goalw [fun_rel_comp_def]
    1.39 +     "ALL x. EX! y. (f x, y) : R ==> EX! g. g : fun_rel_comp f R";
    1.40 +by (res_inst_tac [("a","%x. THE y. (f x, y) : R")] ex1I 1);
    1.41 +by (fast_tac (claset() addSDs [theI']) 1); 
    1.42 +by (fast_tac (claset() addIs [ext, the1_equality RS sym]) 1);
    1.43  qed "fun_rel_comp_unique";
    1.44  
    1.45  
    1.46  section "inverse image";
    1.47  
    1.48  Goalw [trans_def,inv_image_def]
    1.49 -    "!!r. trans r ==> trans (inv_image r f)";
    1.50 +    "trans r ==> trans (inv_image r f)";
    1.51  by (Simp_tac 1);
    1.52  by (Blast_tac 1);
    1.53  qed "trans_inv_image";