src/HOL/Relation.ML
changeset 12487 bbd564190c9b
parent 11655 923e4d0d36d5
child 12905 bbbae3f359e6
     1.1 --- a/src/HOL/Relation.ML	Thu Dec 13 15:45:03 2001 +0100
     1.2 +++ b/src/HOL/Relation.ML	Thu Dec 13 16:47:35 2001 +0100
     1.3 @@ -71,31 +71,31 @@
     1.4  
     1.5  (** Composition of two relations **)
     1.6  
     1.7 -Goalw [comp_def]
     1.8 +Goalw [rel_comp_def]
     1.9      "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
    1.10  by (Blast_tac 1);
    1.11 -qed "compI";
    1.12 +qed "rel_compI";
    1.13  
    1.14  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
    1.15 -val prems = Goalw [comp_def]
    1.16 +val prems = Goalw [rel_comp_def]
    1.17      "[| xz : r O s;  \
    1.18  \       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
    1.19  \    |] ==> P";
    1.20  by (cut_facts_tac prems 1);
    1.21  by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 
    1.22       ORELSE ares_tac prems 1));
    1.23 -qed "compE";
    1.24 +qed "rel_compE";
    1.25  
    1.26  val prems = Goal
    1.27      "[| (a,c) : r O s;  \
    1.28  \       !!y. [| (a,y):s;  (y,c):r |] ==> P \
    1.29  \    |] ==> P";
    1.30 -by (rtac compE 1);
    1.31 +by (rtac rel_compE 1);
    1.32  by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1));
    1.33 -qed "compEpair";
    1.34 +qed "rel_compEpair";
    1.35  
    1.36 -AddIs [compI, IdI];
    1.37 -AddSEs [compE, IdE];
    1.38 +AddIs [rel_compI, IdI];
    1.39 +AddSEs [rel_compE, IdE];
    1.40  
    1.41  Goal "R O Id = R";
    1.42  by (Fast_tac 1);
    1.43 @@ -117,11 +117,11 @@
    1.44  
    1.45  Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    1.46  by (Blast_tac 1);
    1.47 -qed "comp_mono";
    1.48 +qed "rel_comp_mono";
    1.49  
    1.50  Goal "[| s <= A <*> B;  r <= B <*> C |] ==> (r O s) <= A <*> C";
    1.51  by (Blast_tac 1);
    1.52 -qed "comp_subset_Sigma";
    1.53 +qed "rel_comp_subset_Sigma";
    1.54  
    1.55  (** Natural deduction for refl(r) **)
    1.56  
    1.57 @@ -191,7 +191,7 @@
    1.58  
    1.59  Goal "(r O s)^-1 = s^-1 O r^-1";
    1.60  by (Blast_tac 1);
    1.61 -qed "converse_comp";
    1.62 +qed "converse_rel_comp";
    1.63  
    1.64  Goal "Id^-1 = Id";
    1.65  by (Blast_tac 1);