--- a/src/HOL/Finite.ML Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/Finite.ML Mon Mar 16 16:50:50 1998 +0100
@@ -191,15 +191,15 @@
by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1);
by (simp_tac (simpset() addsplits [expand_split]) 1);
by (etac finite_imageI 1);
-by (simp_tac (simpset() addsimps [inverse_def,image_def]) 1);
+by (simp_tac (simpset() addsimps [converse_def,image_def]) 1);
by Auto_tac;
by (rtac bexI 1);
by (assume_tac 2);
by (Simp_tac 1);
by (split_all_tac 1);
by (Asm_full_simp_tac 1);
-qed "finite_inverse";
-AddIffs [finite_inverse];
+qed "finite_converse";
+AddIffs [finite_converse];
section "Finite cardinality -- 'card'";
--- a/src/HOL/IMP/Transition.ML Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/IMP/Transition.ML Mon Mar 16 16:50:50 1998 +0100
@@ -127,7 +127,7 @@
goal Transition.thy
"!!c1. (c1,s1) -*-> (SKIP,s2) ==> \
\ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
-by (etac inverse_rtrancl_induct2 1);
+by (etac converse_rtrancl_induct2 1);
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
qed_spec_mp "my_lemma1";
--- a/src/HOL/Integ/Equiv.ML Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/Integ/Equiv.ML Mon Mar 16 16:50:50 1998 +0100
@@ -16,9 +16,9 @@
(** first half: equiv A r ==> r^-1 O r = r **)
-goalw Equiv.thy [trans_def,sym_def,inverse_def]
+goalw Equiv.thy [trans_def,sym_def,converse_def]
"!!r. [| sym(r); trans(r) |] ==> r^-1 O r <= r";
-by (blast_tac (claset() addSEs [inverseD]) 1);
+by (Blast_tac 1);
qed "sym_trans_comp_subset";
goalw Equiv.thy [refl_def]
--- a/src/HOL/Lambda/Commutation.ML Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/Lambda/Commutation.ML Mon Mar 16 16:50:50 1998 +0100
@@ -91,7 +91,7 @@
by (safe_tac HOL_cs);
by (blast_tac (HOL_cs addIs
[Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
- rtrancl_inverseI, inverseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
+ rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
by (etac rtrancl_induct 1);
by (Blast_tac 1);
by (blast_tac (claset() delrules [rtrancl_refl]
--- a/src/HOL/Relation.ML Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/Relation.ML Mon Mar 16 16:50:50 1998 +0100
@@ -87,22 +87,22 @@
(** Natural deduction for r^-1 **)
-goalw thy [inverse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
+goalw thy [converse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
by (Simp_tac 1);
-qed "inverse_iff";
+qed "converse_iff";
-AddIffs [inverse_iff];
+AddIffs [converse_iff];
-goalw thy [inverse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
+goalw thy [converse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
by (Simp_tac 1);
-qed "inverseI";
+qed "converseI";
-goalw thy [inverse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
+goalw thy [converse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
by (Blast_tac 1);
-qed "inverseD";
+qed "converseD";
-(*More general than inverseD, as it "splits" the member of the relation*)
-qed_goalw "inverseE" thy [inverse_def]
+(*More general than converseD, as it "splits" the member of the relation*)
+qed_goalw "converseE" thy [converse_def]
"[| yx : r^-1; \
\ !!x y. [| yx=(y,x); (x,y):r |] ==> P \
\ |] ==> P"
@@ -111,21 +111,21 @@
(REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
(assume_tac 1) ]);
-AddSEs [inverseE];
+AddSEs [converseE];
-goalw thy [inverse_def] "(r^-1)^-1 = r";
+goalw thy [converse_def] "(r^-1)^-1 = r";
by (Blast_tac 1);
-qed "inverse_inverse";
-Addsimps [inverse_inverse];
+qed "converse_converse";
+Addsimps [converse_converse];
goal thy "(r O s)^-1 = s^-1 O r^-1";
by (Blast_tac 1);
-qed "inverse_comp";
+qed "converse_comp";
goal thy "id^-1 = id";
by (Blast_tac 1);
-qed "inverse_id";
-Addsimps [inverse_id];
+qed "converse_id";
+Addsimps [converse_id];
(** Domain **)
@@ -153,14 +153,14 @@
(** Range **)
qed_goalw "RangeI" thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
- (fn _ => [ (etac (inverseI RS DomainI) 1) ]);
+ (fn _ => [ (etac (converseI RS DomainI) 1) ]);
qed_goalw "RangeE" thy [Range_def]
"[| b : Range(r); !!x. (x,b): r ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS DomainE) 1),
(resolve_tac prems 1),
- (etac inverseD 1) ]);
+ (etac converseD 1) ]);
AddIs [RangeI];
AddSEs [RangeE];
--- a/src/HOL/Relation.thy Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/Relation.thy Mon Mar 16 16:50:50 1998 +0100
@@ -8,7 +8,7 @@
consts
id :: "('a * 'a)set" (*the identity relation*)
O :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
- inverse :: "('a*'b) set => ('b*'a) set" ("(_^-1)" [1000] 999)
+ converse :: "('a*'b) set => ('b*'a) set" ("(_^-1)" [1000] 999)
"^^" :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
Domain :: "('a*'b) set => 'a set"
Range :: "('a*'b) set => 'b set"
@@ -17,7 +17,7 @@
defs
id_def "id == {p. ? x. p = (x,x)}"
comp_def "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
- inverse_def "r^-1 == {(y,x). (x,y):r}"
+ converse_def "r^-1 == {(y,x). (x,y):r}"
Domain_def "Domain(r) == {x. ? y. (x,y):r}"
Range_def "Range(r) == Domain(r^-1)"
Image_def "r ^^ s == {y. ? x:s. (x,y):r}"
--- a/src/HOL/Trancl.ML Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/Trancl.ML Mon Mar 16 16:50:50 1998 +0100
@@ -139,48 +139,48 @@
Addsimps [rtrancl_reflcl];
goal Trancl.thy "!!r. (x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1";
-by (rtac inverseI 1);
+by (rtac converseI 1);
by (etac rtrancl_induct 1);
by (rtac rtrancl_refl 1);
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
-qed "rtrancl_inverseD";
+qed "rtrancl_converseD";
goal Trancl.thy "!!r. (x,y) : (r^*)^-1 ==> (x,y) : (r^-1)^*";
-by (dtac inverseD 1);
+by (dtac converseD 1);
by (etac rtrancl_induct 1);
by (rtac rtrancl_refl 1);
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
-qed "rtrancl_inverseI";
+qed "rtrancl_converseI";
goal Trancl.thy "(r^-1)^* = (r^*)^-1";
-by (safe_tac (claset() addSIs [rtrancl_inverseI]));
+by (safe_tac (claset() addSIs [rtrancl_converseI]));
by (res_inst_tac [("p","x")] PairE 1);
by (hyp_subst_tac 1);
-by (etac rtrancl_inverseD 1);
-qed "rtrancl_inverse";
+by (etac rtrancl_converseD 1);
+qed "rtrancl_converse";
val major::prems = goal Trancl.thy
"[| (a,b) : r^*; P(b); \
\ !!y z.[| (y,z) : r; (z,b) : r^*; P(z) |] ==> P(y) |] \
\ ==> P(a)";
-by (rtac ((major RS inverseI RS rtrancl_inverseI) RS rtrancl_induct) 1);
+by (rtac ((major RS converseI RS rtrancl_converseI) RS rtrancl_induct) 1);
by (resolve_tac prems 1);
-by (blast_tac (claset() addIs prems addSDs[rtrancl_inverseD])1);
-qed "inverse_rtrancl_induct";
+by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1);
+qed "converse_rtrancl_induct";
val prems = goal Trancl.thy
"[| ((a,b),(c,d)) : r^*; P c d; \
\ !!x y z u.[| ((x,y),(z,u)) : r; ((z,u),(c,d)) : r^*; P z u |] ==> P x y\
\ |] ==> P a b";
by (res_inst_tac[("R","P")]splitD 1);
-by (res_inst_tac[("P","split P")]inverse_rtrancl_induct 1);
+by (res_inst_tac[("P","split P")]converse_rtrancl_induct 1);
by (resolve_tac prems 1);
by (Simp_tac 1);
by (resolve_tac prems 1);
by (split_all_tac 1);
by (Asm_full_simp_tac 1);
by (REPEAT(ares_tac prems 1));
-qed "inverse_rtrancl_induct2";
+qed "converse_rtrancl_induct2";
val major::prems = goal Trancl.thy
"[| (x,z):r^*; \
@@ -188,7 +188,7 @@
\ !!y. [| (x,y):r; (y,z):r^* |] ==> P \
\ |] ==> P";
by (subgoal_tac "x = z | (? y. (x,y) : r & (y,z) : r^*)" 1);
-by (rtac (major RS inverse_rtrancl_induct) 2);
+by (rtac (major RS converse_rtrancl_induct) 2);
by (blast_tac (claset() addIs prems) 2);
by (blast_tac (claset() addIs prems) 2);
by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
@@ -304,9 +304,9 @@
qed "trancl_insert";
goalw Trancl.thy [trancl_def] "(r^-1)^+ = (r^+)^-1";
-by (simp_tac (simpset() addsimps [rtrancl_inverse,inverse_comp]) 1);
-by (simp_tac (simpset() addsimps [rtrancl_inverse RS sym,r_comp_rtrancl_eq]) 1);
-qed "trancl_inverse";
+by (simp_tac (simpset() addsimps [rtrancl_converse,converse_comp]) 1);
+by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,r_comp_rtrancl_eq]) 1);
+qed "trancl_converse";
val major::prems = goal Trancl.thy
--- a/src/HOL/WF.ML Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/WF.ML Mon Mar 16 16:50:50 1998 +0100
@@ -144,8 +144,8 @@
AddIffs [acyclic_insert];
goalw WF.thy [acyclic_def] "acyclic(r^-1) = acyclic r";
-by (simp_tac (simpset() addsimps [trancl_inverse]) 1);
-qed "acyclic_inverse";
+by (simp_tac (simpset() addsimps [trancl_converse]) 1);
+qed "acyclic_converse";
(** cut **)