src/HOL/Relation.ML

 
 open Relation;
 
 (** Identity relation **)
 
-Goalw [id_def] "(a,a) : id";  
-by (Blast_tac 1);
-qed "idI";
-
-val major::prems = Goalw [id_def]
-    "[| p: id;  !!x.[| p = (x,x) |] ==> P  \
+Goalw [Id_def] "(a,a) : Id";  
+by (Blast_tac 1);
+qed "IdI";
+
+val major::prems = Goalw [Id_def]
+    "[| p: Id;  !!x.[| p = (x,x) |] ==> P  \
 \    |] ==>  P";  
 by (rtac (major RS CollectE) 1);
 by (etac exE 1);
 by (eresolve_tac prems 1);
-qed "idE";
-
-Goalw [id_def] "(a,b):id = (a=b)";
-by (Blast_tac 1);
-qed "pair_in_id_conv";
-Addsimps [pair_in_id_conv];
+qed "IdE";
+
+Goalw [Id_def] "(a,b):Id = (a=b)";
+by (Blast_tac 1);
+qed "pair_in_Id_conv";
+Addsimps [pair_in_Id_conv];
 
 
 (** Composition of two relations **)
 
 Goalw [comp_def]

 \    |] ==> P";
 by (rtac compE 1);
 by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1));
 qed "compEpair";
 
-AddIs [compI, idI];
-AddSEs [compE, idE];
-
-Goal "R O id = R";
+AddIs [compI, IdI];
+AddSEs [compE, IdE];
+
+Goal "R O Id = R";
 by (Fast_tac 1);
-qed "R_O_id";
-
-Goal "id O R = R";
+qed "R_O_Id";
+
+Goal "Id O R = R";
 by (Fast_tac 1);
-qed "id_O_R";
-
-Addsimps [R_O_id,id_O_R];
+qed "Id_O_R";
+
+Addsimps [R_O_Id,Id_O_R];
 
 Goal "(R O S) O T = R O (S O T)";
 by (Blast_tac 1);
 qed "O_assoc";
 

 
 Goal "(r O s)^-1 = s^-1 O r^-1";
 by (Blast_tac 1);
 qed "converse_comp";
 
-Goal "id^-1 = id";
-by (Blast_tac 1);
-qed "converse_id";
-Addsimps [converse_id];
+Goal "Id^-1 = Id";
+by (Blast_tac 1);
+qed "converse_Id";
+Addsimps [converse_Id];
 
 (** Domain **)
 
 qed_goalw "Domain_iff" thy [Domain_def]
     "a: Domain(r) = (EX y. (a,y): r)"

     (REPEAT (ares_tac prems 1)) ]);
 
 AddIs  [DomainI];
 AddSEs [DomainE];
 
-Goal "Domain id = UNIV";
-by (Blast_tac 1);
-qed "Domain_id";
-Addsimps [Domain_id];
+Goal "Domain Id = UNIV";
+by (Blast_tac 1);
+qed "Domain_Id";
+Addsimps [Domain_Id];
 
 (** Range **)
 
 qed_goalw "RangeI" thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
  (fn _ => [ (etac (converseI RS DomainI) 1) ]);

     (etac converseD 1) ]);
 
 AddIs  [RangeI];
 AddSEs [RangeE];
 
-Goal "Range id = UNIV";
-by (Blast_tac 1);
-qed "Range_id";
-Addsimps [Range_id];
+Goal "Range Id = UNIV";
+by (Blast_tac 1);
+qed "Range_Id";
+Addsimps [Range_Id];
 
 (*** Image of a set under a relation ***)
 
 Blast.overloaded ("Relation.op ^^", HOLogic.dest_setT o domain_type);
 

     "R^^{} = {}"
  (fn _ => [ Blast_tac 1 ]);
 
 Addsimps [Image_empty];
 
-Goal "id ^^ A = A";
-by (Blast_tac 1);
-qed "Image_id";
-
-Addsimps [Image_id];
+Goal "Id ^^ A = A";
+by (Blast_tac 1);
+qed "Image_Id";
+
+Addsimps [Image_Id];
 
 qed_goal "Image_Int_subset" thy
     "R ^^ (A Int B) <= R ^^ A Int R ^^ B"
  (fn _ => [ Blast_tac 1 ]);