--- 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
--- 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])";
--- 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);
--- 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)
--- 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);
--- 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";