# HG changeset patch
# User nipkow
# Date 1008258455 -3600
# Node ID bbd564190c9bb2a5a94aaeeab72a85897bb790f2
# Parent  0ed8bdd883e0792283a4a93029d7b5b734fca023
comp -> rel_comp

diff -r 0ed8bdd883e0 -r bbd564190c9b src/HOL/Lex/RegExp2NA.ML
--- a/src/HOL/Lex/RegExp2NA.ML	Thu Dec 13 15:45:03 2001 +0100
+++ b/src/HOL/Lex/RegExp2NA.ML	Thu Dec 13 16:47:35 2001 +0100
@@ -26,7 +26,7 @@
  "([False],[False]) : steps (atom a) w = (w = [])";
 by (induct_tac "w" 1);
  by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [comp_def]) 1);
+by (asm_simp_tac (simpset() addsimps [rel_comp_def]) 1);
 qed "False_False_in_steps_atom";
 
 Goal
@@ -34,7 +34,7 @@
 by (induct_tac "w" 1);
  by (asm_simp_tac (simpset() addsimps [start_atom]) 1);
 by (asm_full_simp_tac (simpset()
-     addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
+     addsimps [False_False_in_steps_atom,rel_comp_def,start_atom]) 1);
 qed "start_fin_in_steps_atom";
 
 Goal
diff -r 0ed8bdd883e0 -r bbd564190c9b src/HOL/Lex/RegExp2NAe.ML
--- a/src/HOL/Lex/RegExp2NAe.ML	Thu Dec 13 15:45:03 2001 +0100
+++ b/src/HOL/Lex/RegExp2NAe.ML	Thu Dec 13 16:47:35 2001 +0100
@@ -33,14 +33,14 @@
 Goal "([False],[False]) : steps (atom a) w = (w = [])";
 by (induct_tac "w" 1);
  by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [comp_def]) 1);
+by (asm_simp_tac (simpset() addsimps [rel_comp_def]) 1);
 qed "False_False_in_steps_atom";
 
 Goal "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
 by (induct_tac "w" 1);
  by (asm_simp_tac (simpset() addsimps [start_atom,thm"rtrancl_empty"]) 1);
 by (asm_full_simp_tac (simpset()
-     addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
+     addsimps [False_False_in_steps_atom,rel_comp_def,start_atom]) 1);
 qed "start_fin_in_steps_atom";
 
 Goal "accepts (atom a) w = (w = [a])";
diff -r 0ed8bdd883e0 -r bbd564190c9b src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Thu Dec 13 15:45:03 2001 +0100
+++ b/src/HOL/Relation.ML	Thu Dec 13 16:47:35 2001 +0100
@@ -71,31 +71,31 @@
 
 (** Composition of two relations **)
 
-Goalw [comp_def]
+Goalw [rel_comp_def]
     "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
 by (Blast_tac 1);
-qed "compI";
+qed "rel_compI";
 
 (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
-val prems = Goalw [comp_def]
+val prems = Goalw [rel_comp_def]
     "[| xz : r O s;  \
 \       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
 \    |] ==> P";
 by (cut_facts_tac prems 1);
 by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 
      ORELSE ares_tac prems 1));
-qed "compE";
+qed "rel_compE";
 
 val prems = Goal
     "[| (a,c) : r O s;  \
 \       !!y. [| (a,y):s;  (y,c):r |] ==> P \
 \    |] ==> P";
-by (rtac compE 1);
+by (rtac rel_compE 1);
 by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1));
-qed "compEpair";
+qed "rel_compEpair";
 
-AddIs [compI, IdI];
-AddSEs [compE, IdE];
+AddIs [rel_compI, IdI];
+AddSEs [rel_compE, IdE];
 
 Goal "R O Id = R";
 by (Fast_tac 1);
@@ -117,11 +117,11 @@
 
 Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
 by (Blast_tac 1);
-qed "comp_mono";
+qed "rel_comp_mono";
 
 Goal "[| s <= A <*> B;  r <= B <*> C |] ==> (r O s) <= A <*> C";
 by (Blast_tac 1);
-qed "comp_subset_Sigma";
+qed "rel_comp_subset_Sigma";
 
 (** Natural deduction for refl(r) **)
 
@@ -191,7 +191,7 @@
 
 Goal "(r O s)^-1 = s^-1 O r^-1";
 by (Blast_tac 1);
-qed "converse_comp";
+qed "converse_rel_comp";
 
 Goal "Id^-1 = Id";
 by (Blast_tac 1);
diff -r 0ed8bdd883e0 -r bbd564190c9b src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Dec 13 15:45:03 2001 +0100
+++ b/src/HOL/Relation.thy	Thu Dec 13 16:47:35 2001 +0100
@@ -13,7 +13,7 @@
   converse :: "('a * 'b) set => ('b * 'a) set"    ("(_\\<inverse>)" [1000] 999)
 
 constdefs
-  comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
+  rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
     "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
 
   Image :: "[('a * 'b) set, 'a set] => 'b set"                (infixl "``" 90)
diff -r 0ed8bdd883e0 -r bbd564190c9b src/HOL/Relation_Power.ML
--- a/src/HOL/Relation_Power.ML	Thu Dec 13 15:45:03 2001 +0100
+++ b/src/HOL/Relation_Power.ML	Thu Dec 13 16:47:35 2001 +0100
@@ -44,7 +44,7 @@
 by (case_tac "n" 1);
 by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
 by (Asm_full_simp_tac 1);
-by (etac compEpair 1);
+by (etac rel_compEpair 1);
 by (REPEAT(ares_tac [p3] 1));
 qed "rel_pow_E";
 
@@ -71,7 +71,7 @@
 by (case_tac "n" 1);
 by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
 by (Asm_full_simp_tac 1);
-by (etac compEpair 1);
+by (etac rel_compEpair 1);
 by (dtac (conjI RS rel_pow_Suc_D2') 1);
 by (assume_tac 1);
 by (etac exE 1);
diff -r 0ed8bdd883e0 -r bbd564190c9b src/HOL/Transitive_Closure_lemmas.ML
--- a/src/HOL/Transitive_Closure_lemmas.ML	Thu Dec 13 15:45:03 2001 +0100
+++ b/src/HOL/Transitive_Closure_lemmas.ML	Thu Dec 13 16:47:35 2001 +0100
@@ -184,7 +184,7 @@
 Goalw [trancl_def]
     "!!p. p : r^+ ==> p : r^*";
 by (split_all_tac 1);
-by (etac compEpair 1);
+by (etac rel_compEpair 1);
 by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
 qed "trancl_into_rtrancl";
 
@@ -192,7 +192,7 @@
 Goalw [trancl_def]
    "!!p. p : r ==> p : r^+";
 by (split_all_tac 1);
-by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
+by (REPEAT (ares_tac [prem,rel_compI,rtrancl_refl] 1));
 qed "r_into_trancl";
 AddIs [r_into_trancl];
 
@@ -215,7 +215,7 @@
 \     !!y.  [| (a,y) : r |] ==> P(y);                   \
 \     !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)       \
 \  |] ==> P(b)";
-by (rtac (rewrite_rule [trancl_def] major  RS  compEpair) 1);
+by (rtac (rewrite_rule [trancl_def] major  RS  rel_compEpair) 1);
 (*by induction on this formula*)
 by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
 (*now solve first subgoal: this formula is sufficient*)
@@ -241,7 +241,7 @@
 \    |] ==> P";
 by (subgoal_tac "(a::'a,b) : r | (? y. (a,y) : r^+  &  (y,b) : r)" 1);
 by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
-by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
+by (rtac (rewrite_rule [trancl_def] major RS rel_compEpair) 1);
 by (etac rtranclE 1);
 by (Blast_tac 1);
 by (blast_tac (claset() addSIs [rtrancl_into_trancl1]) 1);
@@ -251,8 +251,8 @@
   Proved by unfolding since it uses transitivity of rtrancl. *)
 Goalw [trancl_def] "trans(r^+)";
 by (rtac transI 1);
-by (REPEAT (etac compEpair 1));
-by (rtac (rtrancl_into_rtrancl RS (rtrancl_trans RS compI)) 1);
+by (REPEAT (etac rel_compEpair 1));
+by (rtac (rtrancl_into_rtrancl RS (rtrancl_trans RS rel_compI)) 1);
 by (REPEAT (assume_tac 1));
 qed "trans_trancl";
 
@@ -281,7 +281,7 @@
 qed "trancl_insert";
 
 Goalw [trancl_def] "(r^-1)^+ = (r^+)^-1";
-by (simp_tac (simpset() addsimps [rtrancl_converse,converse_comp]) 1);
+by (simp_tac (simpset() addsimps [rtrancl_converse,converse_rel_comp]) 1);
 by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,
 				  r_comp_rtrancl_eq]) 1);
 qed "trancl_converse";