src/HOL/Relation.ML
changeset 5608 a82a038a3e7a
parent 5335 07fb8999de62
child 5649 1bac26652f45
     1.1 --- a/src/HOL/Relation.ML	Fri Oct 02 10:44:20 1998 +0200
     1.2 +++ b/src/HOL/Relation.ML	Fri Oct 02 14:28:39 1998 +0200
     1.3 @@ -8,22 +8,22 @@
     1.4  
     1.5  (** Identity relation **)
     1.6  
     1.7 -Goalw [id_def] "(a,a) : id";  
     1.8 +Goalw [Id_def] "(a,a) : Id";  
     1.9  by (Blast_tac 1);
    1.10 -qed "idI";
    1.11 +qed "IdI";
    1.12  
    1.13 -val major::prems = Goalw [id_def]
    1.14 -    "[| p: id;  !!x.[| p = (x,x) |] ==> P  \
    1.15 +val major::prems = Goalw [Id_def]
    1.16 +    "[| p: Id;  !!x.[| p = (x,x) |] ==> P  \
    1.17  \    |] ==>  P";  
    1.18  by (rtac (major RS CollectE) 1);
    1.19  by (etac exE 1);
    1.20  by (eresolve_tac prems 1);
    1.21 -qed "idE";
    1.22 +qed "IdE";
    1.23  
    1.24 -Goalw [id_def] "(a,b):id = (a=b)";
    1.25 +Goalw [Id_def] "(a,b):Id = (a=b)";
    1.26  by (Blast_tac 1);
    1.27 -qed "pair_in_id_conv";
    1.28 -Addsimps [pair_in_id_conv];
    1.29 +qed "pair_in_Id_conv";
    1.30 +Addsimps [pair_in_Id_conv];
    1.31  
    1.32  
    1.33  (** Composition of two relations **)
    1.34 @@ -51,18 +51,18 @@
    1.35  by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1));
    1.36  qed "compEpair";
    1.37  
    1.38 -AddIs [compI, idI];
    1.39 -AddSEs [compE, idE];
    1.40 +AddIs [compI, IdI];
    1.41 +AddSEs [compE, IdE];
    1.42  
    1.43 -Goal "R O id = R";
    1.44 +Goal "R O Id = R";
    1.45  by (Fast_tac 1);
    1.46 -qed "R_O_id";
    1.47 +qed "R_O_Id";
    1.48  
    1.49 -Goal "id O R = R";
    1.50 +Goal "Id O R = R";
    1.51  by (Fast_tac 1);
    1.52 -qed "id_O_R";
    1.53 +qed "Id_O_R";
    1.54  
    1.55 -Addsimps [R_O_id,id_O_R];
    1.56 +Addsimps [R_O_Id,Id_O_R];
    1.57  
    1.58  Goal "(R O S) O T = R O (S O T)";
    1.59  by (Blast_tac 1);
    1.60 @@ -124,10 +124,10 @@
    1.61  by (Blast_tac 1);
    1.62  qed "converse_comp";
    1.63  
    1.64 -Goal "id^-1 = id";
    1.65 +Goal "Id^-1 = Id";
    1.66  by (Blast_tac 1);
    1.67 -qed "converse_id";
    1.68 -Addsimps [converse_id];
    1.69 +qed "converse_Id";
    1.70 +Addsimps [converse_Id];
    1.71  
    1.72  (** Domain **)
    1.73  
    1.74 @@ -147,10 +147,10 @@
    1.75  AddIs  [DomainI];
    1.76  AddSEs [DomainE];
    1.77  
    1.78 -Goal "Domain id = UNIV";
    1.79 +Goal "Domain Id = UNIV";
    1.80  by (Blast_tac 1);
    1.81 -qed "Domain_id";
    1.82 -Addsimps [Domain_id];
    1.83 +qed "Domain_Id";
    1.84 +Addsimps [Domain_Id];
    1.85  
    1.86  (** Range **)
    1.87  
    1.88 @@ -167,10 +167,10 @@
    1.89  AddIs  [RangeI];
    1.90  AddSEs [RangeE];
    1.91  
    1.92 -Goal "Range id = UNIV";
    1.93 +Goal "Range Id = UNIV";
    1.94  by (Blast_tac 1);
    1.95 -qed "Range_id";
    1.96 -Addsimps [Range_id];
    1.97 +qed "Range_Id";
    1.98 +Addsimps [Range_Id];
    1.99  
   1.100  (*** Image of a set under a relation ***)
   1.101  
   1.102 @@ -213,11 +213,11 @@
   1.103  
   1.104  Addsimps [Image_empty];
   1.105  
   1.106 -Goal "id ^^ A = A";
   1.107 +Goal "Id ^^ A = A";
   1.108  by (Blast_tac 1);
   1.109 -qed "Image_id";
   1.110 +qed "Image_Id";
   1.111  
   1.112 -Addsimps [Image_id];
   1.113 +Addsimps [Image_Id];
   1.114  
   1.115  qed_goal "Image_Int_subset" thy
   1.116      "R ^^ (A Int B) <= R ^^ A Int R ^^ B"