inverse -> converse
authorpaulson
Mon Mar 16 16:50:50 1998 +0100 (1998-03-16)
changeset 4746a5dcd7e4a37d
parent 4745 b855a7094195
child 4747 bbe14a54deb3
inverse -> converse
[It is standard terminology and also used in ZF]
src/HOL/Finite.ML
src/HOL/IMP/Transition.ML
src/HOL/Integ/Equiv.ML
src/HOL/Lambda/Commutation.ML
src/HOL/Relation.ML
src/HOL/Relation.thy
src/HOL/Trancl.ML
src/HOL/WF.ML
     1.1 --- a/src/HOL/Finite.ML	Mon Mar 16 16:47:57 1998 +0100
     1.2 +++ b/src/HOL/Finite.ML	Mon Mar 16 16:50:50 1998 +0100
     1.3 @@ -191,15 +191,15 @@
     1.4    by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1);
     1.5    by (simp_tac (simpset() addsplits [expand_split]) 1);
     1.6   by (etac finite_imageI 1);
     1.7 -by (simp_tac (simpset() addsimps [inverse_def,image_def]) 1);
     1.8 +by (simp_tac (simpset() addsimps [converse_def,image_def]) 1);
     1.9  by Auto_tac;
    1.10   by (rtac bexI 1);
    1.11   by (assume_tac 2);
    1.12   by (Simp_tac 1);
    1.13  by (split_all_tac 1);
    1.14  by (Asm_full_simp_tac 1);
    1.15 -qed "finite_inverse";
    1.16 -AddIffs [finite_inverse];
    1.17 +qed "finite_converse";
    1.18 +AddIffs [finite_converse];
    1.19  
    1.20  section "Finite cardinality -- 'card'";
    1.21  
     2.1 --- a/src/HOL/IMP/Transition.ML	Mon Mar 16 16:47:57 1998 +0100
     2.2 +++ b/src/HOL/IMP/Transition.ML	Mon Mar 16 16:50:50 1998 +0100
     2.3 @@ -127,7 +127,7 @@
     2.4  goal Transition.thy
     2.5   "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \
     2.6  \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
     2.7 -by (etac inverse_rtrancl_induct2 1);
     2.8 +by (etac converse_rtrancl_induct2 1);
     2.9  by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
    2.10  by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
    2.11  qed_spec_mp "my_lemma1";
     3.1 --- a/src/HOL/Integ/Equiv.ML	Mon Mar 16 16:47:57 1998 +0100
     3.2 +++ b/src/HOL/Integ/Equiv.ML	Mon Mar 16 16:50:50 1998 +0100
     3.3 @@ -16,9 +16,9 @@
     3.4  
     3.5  (** first half: equiv A r ==> r^-1 O r = r **)
     3.6  
     3.7 -goalw Equiv.thy [trans_def,sym_def,inverse_def]
     3.8 +goalw Equiv.thy [trans_def,sym_def,converse_def]
     3.9      "!!r. [| sym(r); trans(r) |] ==> r^-1 O r <= r";
    3.10 -by (blast_tac (claset() addSEs [inverseD]) 1);
    3.11 +by (Blast_tac 1);
    3.12  qed "sym_trans_comp_subset";
    3.13  
    3.14  goalw Equiv.thy [refl_def]
     4.1 --- a/src/HOL/Lambda/Commutation.ML	Mon Mar 16 16:47:57 1998 +0100
     4.2 +++ b/src/HOL/Lambda/Commutation.ML	Mon Mar 16 16:50:50 1998 +0100
     4.3 @@ -91,7 +91,7 @@
     4.4  by (safe_tac HOL_cs);
     4.5   by (blast_tac (HOL_cs addIs
     4.6        [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
     4.7 -       rtrancl_inverseI, inverseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
     4.8 +       rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
     4.9  by (etac rtrancl_induct 1);
    4.10   by (Blast_tac 1);
    4.11  by (blast_tac (claset() delrules [rtrancl_refl] 
     5.1 --- a/src/HOL/Relation.ML	Mon Mar 16 16:47:57 1998 +0100
     5.2 +++ b/src/HOL/Relation.ML	Mon Mar 16 16:50:50 1998 +0100
     5.3 @@ -87,22 +87,22 @@
     5.4  
     5.5  (** Natural deduction for r^-1 **)
     5.6  
     5.7 -goalw thy [inverse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
     5.8 +goalw thy [converse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
     5.9  by (Simp_tac 1);
    5.10 -qed "inverse_iff";
    5.11 +qed "converse_iff";
    5.12  
    5.13 -AddIffs [inverse_iff];
    5.14 +AddIffs [converse_iff];
    5.15  
    5.16 -goalw thy [inverse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
    5.17 +goalw thy [converse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
    5.18  by (Simp_tac 1);
    5.19 -qed "inverseI";
    5.20 +qed "converseI";
    5.21  
    5.22 -goalw thy [inverse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
    5.23 +goalw thy [converse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
    5.24  by (Blast_tac 1);
    5.25 -qed "inverseD";
    5.26 +qed "converseD";
    5.27  
    5.28 -(*More general than inverseD, as it "splits" the member of the relation*)
    5.29 -qed_goalw "inverseE" thy [inverse_def]
    5.30 +(*More general than converseD, as it "splits" the member of the relation*)
    5.31 +qed_goalw "converseE" thy [converse_def]
    5.32      "[| yx : r^-1;  \
    5.33  \       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
    5.34  \    |] ==> P"
    5.35 @@ -111,21 +111,21 @@
    5.36      (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
    5.37      (assume_tac 1) ]);
    5.38  
    5.39 -AddSEs [inverseE];
    5.40 +AddSEs [converseE];
    5.41  
    5.42 -goalw thy [inverse_def] "(r^-1)^-1 = r";
    5.43 +goalw thy [converse_def] "(r^-1)^-1 = r";
    5.44  by (Blast_tac 1);
    5.45 -qed "inverse_inverse";
    5.46 -Addsimps [inverse_inverse];
    5.47 +qed "converse_converse";
    5.48 +Addsimps [converse_converse];
    5.49  
    5.50  goal thy "(r O s)^-1 = s^-1 O r^-1";
    5.51  by (Blast_tac 1);
    5.52 -qed "inverse_comp";
    5.53 +qed "converse_comp";
    5.54  
    5.55  goal thy "id^-1 = id";
    5.56  by (Blast_tac 1);
    5.57 -qed "inverse_id";
    5.58 -Addsimps [inverse_id];
    5.59 +qed "converse_id";
    5.60 +Addsimps [converse_id];
    5.61  
    5.62  (** Domain **)
    5.63  
    5.64 @@ -153,14 +153,14 @@
    5.65  (** Range **)
    5.66  
    5.67  qed_goalw "RangeI" thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
    5.68 - (fn _ => [ (etac (inverseI RS DomainI) 1) ]);
    5.69 + (fn _ => [ (etac (converseI RS DomainI) 1) ]);
    5.70  
    5.71  qed_goalw "RangeE" thy [Range_def]
    5.72      "[| b : Range(r);  !!x. (x,b): r ==> P |] ==> P"
    5.73   (fn major::prems=>
    5.74    [ (rtac (major RS DomainE) 1),
    5.75      (resolve_tac prems 1),
    5.76 -    (etac inverseD 1) ]);
    5.77 +    (etac converseD 1) ]);
    5.78  
    5.79  AddIs  [RangeI];
    5.80  AddSEs [RangeE];
     6.1 --- a/src/HOL/Relation.thy	Mon Mar 16 16:47:57 1998 +0100
     6.2 +++ b/src/HOL/Relation.thy	Mon Mar 16 16:50:50 1998 +0100
     6.3 @@ -8,7 +8,7 @@
     6.4  consts
     6.5      id          :: "('a * 'a)set"               (*the identity relation*)
     6.6      O           :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
     6.7 -    inverse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 999)
     6.8 +    converse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 999)
     6.9      "^^"        :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
    6.10      Domain      :: "('a*'b) set => 'a set"
    6.11      Range       :: "('a*'b) set => 'b set"
    6.12 @@ -17,7 +17,7 @@
    6.13  defs
    6.14      id_def        "id == {p. ? x. p = (x,x)}"
    6.15      comp_def      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
    6.16 -    inverse_def   "r^-1 == {(y,x). (x,y):r}"
    6.17 +    converse_def   "r^-1 == {(y,x). (x,y):r}"
    6.18      Domain_def    "Domain(r) == {x. ? y. (x,y):r}"
    6.19      Range_def     "Range(r) == Domain(r^-1)"
    6.20      Image_def     "r ^^ s == {y. ? x:s. (x,y):r}"
     7.1 --- a/src/HOL/Trancl.ML	Mon Mar 16 16:47:57 1998 +0100
     7.2 +++ b/src/HOL/Trancl.ML	Mon Mar 16 16:50:50 1998 +0100
     7.3 @@ -139,48 +139,48 @@
     7.4  Addsimps [rtrancl_reflcl];
     7.5  
     7.6  goal Trancl.thy "!!r. (x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1";
     7.7 -by (rtac inverseI 1);
     7.8 +by (rtac converseI 1);
     7.9  by (etac rtrancl_induct 1);
    7.10  by (rtac rtrancl_refl 1);
    7.11  by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
    7.12 -qed "rtrancl_inverseD";
    7.13 +qed "rtrancl_converseD";
    7.14  
    7.15  goal Trancl.thy "!!r. (x,y) : (r^*)^-1 ==> (x,y) : (r^-1)^*";
    7.16 -by (dtac inverseD 1);
    7.17 +by (dtac converseD 1);
    7.18  by (etac rtrancl_induct 1);
    7.19  by (rtac rtrancl_refl 1);
    7.20  by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
    7.21 -qed "rtrancl_inverseI";
    7.22 +qed "rtrancl_converseI";
    7.23  
    7.24  goal Trancl.thy "(r^-1)^* = (r^*)^-1";
    7.25 -by (safe_tac (claset() addSIs [rtrancl_inverseI]));
    7.26 +by (safe_tac (claset() addSIs [rtrancl_converseI]));
    7.27  by (res_inst_tac [("p","x")] PairE 1);
    7.28  by (hyp_subst_tac 1);
    7.29 -by (etac rtrancl_inverseD 1);
    7.30 -qed "rtrancl_inverse";
    7.31 +by (etac rtrancl_converseD 1);
    7.32 +qed "rtrancl_converse";
    7.33  
    7.34  val major::prems = goal Trancl.thy
    7.35      "[| (a,b) : r^*; P(b); \
    7.36  \       !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]  \
    7.37  \     ==> P(a)";
    7.38 -by (rtac ((major RS inverseI RS rtrancl_inverseI) RS rtrancl_induct) 1);
    7.39 +by (rtac ((major RS converseI RS rtrancl_converseI) RS rtrancl_induct) 1);
    7.40  by (resolve_tac prems 1);
    7.41 -by (blast_tac (claset() addIs prems addSDs[rtrancl_inverseD])1);
    7.42 -qed "inverse_rtrancl_induct";
    7.43 +by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1);
    7.44 +qed "converse_rtrancl_induct";
    7.45  
    7.46  val prems = goal Trancl.thy
    7.47   "[| ((a,b),(c,d)) : r^*; P c d; \
    7.48  \    !!x y z u.[| ((x,y),(z,u)) : r;  ((z,u),(c,d)) : r^*;  P z u |] ==> P x y\
    7.49  \ |] ==> P a b";
    7.50  by (res_inst_tac[("R","P")]splitD 1);
    7.51 -by (res_inst_tac[("P","split P")]inverse_rtrancl_induct 1);
    7.52 +by (res_inst_tac[("P","split P")]converse_rtrancl_induct 1);
    7.53  by (resolve_tac prems 1);
    7.54  by (Simp_tac 1);
    7.55  by (resolve_tac prems 1);
    7.56  by (split_all_tac 1);
    7.57  by (Asm_full_simp_tac 1);
    7.58  by (REPEAT(ares_tac prems 1));
    7.59 -qed "inverse_rtrancl_induct2";
    7.60 +qed "converse_rtrancl_induct2";
    7.61  
    7.62  val major::prems = goal Trancl.thy
    7.63   "[| (x,z):r^*; \
    7.64 @@ -188,7 +188,7 @@
    7.65  \    !!y. [| (x,y):r; (y,z):r^* |] ==> P \
    7.66  \ |] ==> P";
    7.67  by (subgoal_tac "x = z  | (? y. (x,y) : r & (y,z) : r^*)" 1);
    7.68 -by (rtac (major RS inverse_rtrancl_induct) 2);
    7.69 +by (rtac (major RS converse_rtrancl_induct) 2);
    7.70  by (blast_tac (claset() addIs prems) 2);
    7.71  by (blast_tac (claset() addIs prems) 2);
    7.72  by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
    7.73 @@ -304,9 +304,9 @@
    7.74  qed "trancl_insert";
    7.75  
    7.76  goalw Trancl.thy [trancl_def] "(r^-1)^+ = (r^+)^-1";
    7.77 -by (simp_tac (simpset() addsimps [rtrancl_inverse,inverse_comp]) 1);
    7.78 -by (simp_tac (simpset() addsimps [rtrancl_inverse RS sym,r_comp_rtrancl_eq]) 1);
    7.79 -qed "trancl_inverse";
    7.80 +by (simp_tac (simpset() addsimps [rtrancl_converse,converse_comp]) 1);
    7.81 +by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,r_comp_rtrancl_eq]) 1);
    7.82 +qed "trancl_converse";
    7.83  
    7.84  
    7.85  val major::prems = goal Trancl.thy
     8.1 --- a/src/HOL/WF.ML	Mon Mar 16 16:47:57 1998 +0100
     8.2 +++ b/src/HOL/WF.ML	Mon Mar 16 16:50:50 1998 +0100
     8.3 @@ -144,8 +144,8 @@
     8.4  AddIffs [acyclic_insert];
     8.5  
     8.6  goalw WF.thy [acyclic_def] "acyclic(r^-1) = acyclic r";
     8.7 -by (simp_tac (simpset() addsimps [trancl_inverse]) 1);
     8.8 -qed "acyclic_inverse";
     8.9 +by (simp_tac (simpset() addsimps [trancl_converse]) 1);
    8.10 +qed "acyclic_converse";
    8.11  
    8.12  (** cut **)
    8.13