src/HOL/Relation.ML
changeset 1754 852093aeb0ab
parent 1694 3452958f85a8
child 1761 29e08d527ba1
     1.1 --- a/src/HOL/Relation.ML	Tue May 21 10:52:26 1996 +0200
     1.2 +++ b/src/HOL/Relation.ML	Tue May 21 13:39:31 1996 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  qed "idE";
     1.5  
     1.6  goalw Relation.thy [id_def] "(a,b):id = (a=b)";
     1.7 -by (fast_tac prod_cs 1);
     1.8 +by (Fast_tac 1);
     1.9  qed "pair_in_id_conv";
    1.10  Addsimps [pair_in_id_conv];
    1.11  
    1.12 @@ -36,7 +36,7 @@
    1.13  
    1.14  val prems = goalw Relation.thy [comp_def]
    1.15      "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
    1.16 -by (fast_tac (prod_cs addIs prems) 1);
    1.17 +by (fast_tac (!claset addIs prems) 1);
    1.18  qed "compI";
    1.19  
    1.20  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
    1.21 @@ -56,16 +56,19 @@
    1.22  by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1));
    1.23  qed "compEpair";
    1.24  
    1.25 +AddIs [compI, idI];
    1.26 +AddSEs [compE, idE];
    1.27 +
    1.28  val comp_cs = prod_cs addIs [compI, idI] addSEs [compE, idE];
    1.29  
    1.30  goal Relation.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    1.31 -by (fast_tac comp_cs 1);
    1.32 +by (Fast_tac 1);
    1.33  qed "comp_mono";
    1.34  
    1.35  goal Relation.thy
    1.36      "!!r s. [| s <= A Times B;  r <= B Times C |] ==> \
    1.37  \           (r O s) <= A Times C";
    1.38 -by (fast_tac comp_cs 1);
    1.39 +by (Fast_tac 1);
    1.40  qed "comp_subset_Sigma";
    1.41  
    1.42  (** Natural deduction for trans(r) **)
    1.43 @@ -78,7 +81,7 @@
    1.44  val major::prems = goalw Relation.thy [trans_def]
    1.45      "[| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
    1.46  by (cut_facts_tac [major] 1);
    1.47 -by (fast_tac (HOL_cs addIs prems) 1);
    1.48 +by (fast_tac (!claset addIs prems) 1);
    1.49  qed "transD";
    1.50  
    1.51  (** Natural deduction for converse(r) **)
    1.52 @@ -88,7 +91,7 @@
    1.53  qed "converseI";
    1.54  
    1.55  goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r";
    1.56 -by (fast_tac comp_cs 1);
    1.57 +by (Fast_tac 1);
    1.58  qed "converseD";
    1.59  
    1.60  qed_goalw "converseE" Relation.thy [converse_def]
    1.61 @@ -100,18 +103,21 @@
    1.62      (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
    1.63      (assume_tac 1) ]);
    1.64  
    1.65 -val converse_cs = comp_cs addSIs [converseI] 
    1.66 +AddSIs [converseI];
    1.67 +AddSEs [converseD,converseE];
    1.68 +
    1.69 +val converse_cs = comp_cs addSIs [converseI]
    1.70                            addSEs [converseD,converseE];
    1.71  
    1.72  goalw Relation.thy [converse_def] "converse(converse R) = R";
    1.73 -by(fast_tac (prod_cs addSIs [equalityI]) 1);
    1.74 +by(fast_tac (!claset addSIs [equalityI]) 1);
    1.75  qed "converse_converse";
    1.76  
    1.77  (** Domain **)
    1.78  
    1.79  qed_goalw "Domain_iff" Relation.thy [Domain_def]
    1.80      "a: Domain(r) = (EX y. (a,y): r)"
    1.81 - (fn _=> [ (fast_tac comp_cs 1) ]);
    1.82 + (fn _=> [ (Fast_tac 1) ]);
    1.83  
    1.84  qed_goal "DomainI" Relation.thy "!!a b r. (a,b): r ==> a: Domain(r)"
    1.85   (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]);
    1.86 @@ -138,19 +144,19 @@
    1.87  
    1.88  qed_goalw "Image_iff" Relation.thy [Image_def]
    1.89      "b : r^^A = (? x:A. (x,b):r)"
    1.90 - (fn _ => [ fast_tac (comp_cs addIs [RangeI]) 1 ]);
    1.91 + (fn _ => [ fast_tac (!claset addIs [RangeI]) 1 ]);
    1.92  
    1.93  qed_goal "Image_singleton_iff" Relation.thy
    1.94      "(b : r^^{a}) = ((a,b):r)"
    1.95   (fn _ => [ rtac (Image_iff RS trans) 1,
    1.96 -            fast_tac comp_cs 1 ]);
    1.97 +            Fast_tac 1 ]);
    1.98  
    1.99  qed_goalw "ImageI" Relation.thy [Image_def]
   1.100      "!!a b r. [| (a,b): r;  a:A |] ==> b : r^^A"
   1.101   (fn _ => [ (REPEAT (ares_tac [CollectI,RangeI,bexI] 1)),
   1.102              (resolve_tac [conjI ] 1),
   1.103              (rtac RangeI 1),
   1.104 -            (REPEAT (fast_tac set_cs 1))]);
   1.105 +            (REPEAT (Fast_tac 1))]);
   1.106  
   1.107  qed_goalw "ImageE" Relation.thy [Image_def]
   1.108      "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
   1.109 @@ -167,18 +173,24 @@
   1.110    [ (rtac subsetI 1),
   1.111      (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
   1.112  
   1.113 +AddSIs [converseI]; 
   1.114 +AddIs  [ImageI, DomainI, RangeI];
   1.115 +AddSEs [ImageE, DomainE, RangeE];
   1.116 +
   1.117  val rel_cs = converse_cs addSIs [converseI] 
   1.118                           addIs  [ImageI, DomainI, RangeI]
   1.119                           addSEs [ImageE, DomainE, RangeE];
   1.120  
   1.121 +AddSIs [equalityI];
   1.122 +
   1.123  val rel_eq_cs = rel_cs addSIs [equalityI];
   1.124  
   1.125  goal Relation.thy "R O id = R";
   1.126 -by(fast_tac (rel_cs addIs [set_ext] addbefore (split_all_tac 1)) 1);
   1.127 +by(fast_tac (!claset addIs [set_ext] addbefore (split_all_tac 1)) 1);
   1.128  qed "R_O_id";
   1.129  
   1.130  goal Relation.thy "id O R = R";
   1.131 -by(fast_tac (rel_cs addIs [set_ext] addbefore (split_all_tac 1)) 1);
   1.132 +by(fast_tac (!claset addIs [set_ext] addbefore (split_all_tac 1)) 1);
   1.133  qed "id_O_R";
   1.134  
   1.135  Addsimps [R_O_id,id_O_R];