src/HOL/Relation.ML
changeset 2891 d8f254ad1ab9
parent 2637 e9b203f854ae
child 3413 c1f63cc3a768
     1.1 --- a/src/HOL/Relation.ML	Fri Apr 04 11:18:19 1997 +0200
     1.2 +++ b/src/HOL/Relation.ML	Fri Apr 04 11:18:52 1997 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  (** Identity relation **)
     1.5  
     1.6  goalw Relation.thy [id_def] "(a,a) : id";  
     1.7 -by (Fast_tac 1);
     1.8 +by (Blast_tac 1);
     1.9  qed "idI";
    1.10  
    1.11  val major::prems = goalw Relation.thy [id_def]
    1.12 @@ -21,7 +21,7 @@
    1.13  qed "idE";
    1.14  
    1.15  goalw Relation.thy [id_def] "(a,b):id = (a=b)";
    1.16 -by (Fast_tac 1);
    1.17 +by (Blast_tac 1);
    1.18  qed "pair_in_id_conv";
    1.19  Addsimps [pair_in_id_conv];
    1.20  
    1.21 @@ -30,7 +30,7 @@
    1.22  
    1.23  goalw Relation.thy [comp_def]
    1.24      "!!r s. [| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
    1.25 -by (Fast_tac 1);
    1.26 +by (Blast_tac 1);
    1.27  qed "compI";
    1.28  
    1.29  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
    1.30 @@ -55,12 +55,12 @@
    1.31  AddSEs [compE, idE];
    1.32  
    1.33  goal Relation.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    1.34 -by (Fast_tac 1);
    1.35 +by (Blast_tac 1);
    1.36  qed "comp_mono";
    1.37  
    1.38  goal Relation.thy
    1.39      "!!r s. [| s <= A Times B;  r <= B Times C |] ==> (r O s) <= A Times C";
    1.40 -by (Fast_tac 1);
    1.41 +by (Blast_tac 1);
    1.42  qed "comp_subset_Sigma";
    1.43  
    1.44  (** Natural deduction for trans(r) **)
    1.45 @@ -72,7 +72,7 @@
    1.46  
    1.47  goalw Relation.thy [trans_def]
    1.48      "!!r. [| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
    1.49 -by (Fast_tac 1);
    1.50 +by (Blast_tac 1);
    1.51  qed "transD";
    1.52  
    1.53  (** Natural deduction for converse(r) **)
    1.54 @@ -88,7 +88,7 @@
    1.55  qed "converseI";
    1.56  
    1.57  goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r";
    1.58 -by (Fast_tac 1);
    1.59 +by (Blast_tac 1);
    1.60  qed "converseD";
    1.61  
    1.62  (*More general than converseD, as it "splits" the member of the relation*)
    1.63 @@ -104,14 +104,14 @@
    1.64  AddSEs [converseE];
    1.65  
    1.66  goalw Relation.thy [converse_def] "converse(converse R) = R";
    1.67 -by (Fast_tac 1);
    1.68 +by (Blast_tac 1);
    1.69  qed "converse_converse";
    1.70  
    1.71  (** Domain **)
    1.72  
    1.73  qed_goalw "Domain_iff" Relation.thy [Domain_def]
    1.74      "a: Domain(r) = (EX y. (a,y): r)"
    1.75 - (fn _=> [ (Fast_tac 1) ]);
    1.76 + (fn _=> [ (Blast_tac 1) ]);
    1.77  
    1.78  qed_goal "DomainI" Relation.thy "!!a b r. (a,b): r ==> a: Domain(r)"
    1.79   (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]);
    1.80 @@ -144,16 +144,16 @@
    1.81  
    1.82  qed_goalw "Image_iff" Relation.thy [Image_def]
    1.83      "b : r^^A = (? x:A. (x,b):r)"
    1.84 - (fn _ => [ Fast_tac 1 ]);
    1.85 + (fn _ => [ Blast_tac 1 ]);
    1.86  
    1.87  qed_goal "Image_singleton_iff" Relation.thy
    1.88      "(b : r^^{a}) = ((a,b):r)"
    1.89   (fn _ => [ rtac (Image_iff RS trans) 1,
    1.90 -            Fast_tac 1 ]);
    1.91 +            Blast_tac 1 ]);
    1.92  
    1.93  qed_goalw "ImageI" Relation.thy [Image_def]
    1.94      "!!a b r. [| (a,b): r;  a:A |] ==> b : r^^A"
    1.95 - (fn _ => [ (Fast_tac 1)]);
    1.96 + (fn _ => [ (Blast_tac 1)]);
    1.97  
    1.98  qed_goalw "ImageE" Relation.thy [Image_def]
    1.99      "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"