src/HOL/Transitive_Closure_lemmas.ML
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10996 74e970389def
child 11327 cd2c27a23df1
permissions -rw-r--r--
improved theory reference in comment
wenzelm@10980
     1
(*  Title:      HOL/Transitive_Closure_lemmas.ML
wenzelm@10980
     2
    ID:         $Id$
wenzelm@10980
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@10980
     4
    Copyright   1992  University of Cambridge
wenzelm@10980
     5
wenzelm@10980
     6
Theorems about the transitive closure of a relation
wenzelm@10980
     7
*)
wenzelm@10980
     8
wenzelm@10980
     9
val rtrancl_def = thm "rtrancl_def";
wenzelm@10980
    10
val trancl_def = thm "trancl_def";
wenzelm@10980
    11
wenzelm@10980
    12
wenzelm@10980
    13
(** The relation rtrancl **)
wenzelm@10980
    14
wenzelm@10980
    15
section "^*";
wenzelm@10980
    16
wenzelm@10980
    17
Goal "mono(%s. Id Un (r O s))";
wenzelm@10980
    18
by (rtac monoI 1);
wenzelm@10980
    19
by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1));
wenzelm@10980
    20
qed "rtrancl_fun_mono";
wenzelm@10980
    21
wenzelm@10980
    22
bind_thm ("rtrancl_unfold", rtrancl_fun_mono RS (rtrancl_def RS def_lfp_unfold));
wenzelm@10980
    23
wenzelm@10980
    24
(*Reflexivity of rtrancl*)
wenzelm@10980
    25
Goal "(a,a) : r^*";
wenzelm@10980
    26
by (stac rtrancl_unfold 1);
wenzelm@10980
    27
by (Blast_tac 1);
wenzelm@10980
    28
qed "rtrancl_refl";
wenzelm@10980
    29
wenzelm@10980
    30
Addsimps [rtrancl_refl];
wenzelm@10980
    31
AddSIs   [rtrancl_refl];
wenzelm@10980
    32
wenzelm@10980
    33
wenzelm@10980
    34
(*Closure under composition with r*)
wenzelm@10980
    35
Goal "[| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
wenzelm@10980
    36
by (stac rtrancl_unfold 1);
wenzelm@10980
    37
by (Blast_tac 1);
wenzelm@10980
    38
qed "rtrancl_into_rtrancl";
wenzelm@10980
    39
wenzelm@10980
    40
(*rtrancl of r contains r*)
wenzelm@10980
    41
Goal "!!p. p : r ==> p : r^*";
wenzelm@10980
    42
by (split_all_tac 1);
wenzelm@10980
    43
by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
wenzelm@10980
    44
qed "r_into_rtrancl";
wenzelm@10980
    45
wenzelm@10980
    46
AddIs [r_into_rtrancl];
wenzelm@10980
    47
wenzelm@10980
    48
(*monotonicity of rtrancl*)
wenzelm@10980
    49
Goalw [rtrancl_def] "r <= s ==> r^* <= s^*";
wenzelm@10980
    50
by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
wenzelm@10980
    51
qed "rtrancl_mono";
wenzelm@10980
    52
wenzelm@10980
    53
(** standard induction rule **)
wenzelm@10980
    54
wenzelm@10980
    55
val major::prems = Goal 
wenzelm@10980
    56
  "[| (a,b) : r^*; \
wenzelm@10980
    57
\     !!x. P(x,x); \
wenzelm@10980
    58
\     !!x y z.[| P(x,y); (x,y): r^*; (y,z): r |]  ==>  P(x,z) |] \
wenzelm@10980
    59
\  ==>  P(a,b)";
wenzelm@10980
    60
by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_lfp_induct) 1);
wenzelm@10980
    61
by (blast_tac (claset() addIs prems) 1);
wenzelm@10980
    62
qed "rtrancl_full_induct";
wenzelm@10980
    63
wenzelm@10980
    64
(*nice induction rule*)
wenzelm@10980
    65
val major::prems = Goal
wenzelm@10980
    66
    "[| (a::'a,b) : r^*;    \
wenzelm@10980
    67
\       P(a); \
wenzelm@10980
    68
\       !!y z.[| (a,y) : r^*;  (y,z) : r;  P(y) |] ==> P(z) |]  \
wenzelm@10980
    69
\     ==> P(b)";
wenzelm@10980
    70
(*by induction on this formula*)
wenzelm@10980
    71
by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1);
wenzelm@10980
    72
(*now solve first subgoal: this formula is sufficient*)
wenzelm@10980
    73
by (Blast_tac 1);
wenzelm@10980
    74
(*now do the induction*)
wenzelm@10980
    75
by (resolve_tac [major RS rtrancl_full_induct] 1);
wenzelm@10980
    76
by (blast_tac (claset() addIs prems) 1);
wenzelm@10980
    77
by (blast_tac (claset() addIs prems) 1);
wenzelm@10980
    78
qed "rtrancl_induct";
wenzelm@10980
    79
wenzelm@10980
    80
bind_thm ("rtrancl_induct2", split_rule
wenzelm@10980
    81
  (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] rtrancl_induct));
wenzelm@10980
    82
wenzelm@10980
    83
(*transitivity of transitive closure!! -- by induction.*)
wenzelm@10980
    84
Goalw [trans_def] "trans(r^*)";
wenzelm@10980
    85
by Safe_tac;
wenzelm@10980
    86
by (eres_inst_tac [("b","z")] rtrancl_induct 1);
wenzelm@10980
    87
by (ALLGOALS(blast_tac (claset() addIs [rtrancl_into_rtrancl])));
wenzelm@10980
    88
qed "trans_rtrancl";
wenzelm@10980
    89
wenzelm@10980
    90
bind_thm ("rtrancl_trans", trans_rtrancl RS transD);
wenzelm@10980
    91
wenzelm@10980
    92
wenzelm@10980
    93
(*elimination of rtrancl -- by induction on a special formula*)
wenzelm@10980
    94
val major::prems = Goal
wenzelm@10980
    95
    "[| (a::'a,b) : r^*;  (a = b) ==> P;        \
wenzelm@10980
    96
\       !!y.[| (a,y) : r^*; (y,b) : r |] ==> P  \
wenzelm@10980
    97
\    |] ==> P";
wenzelm@10980
    98
by (subgoal_tac "(a::'a) = b  | (? y. (a,y) : r^* & (y,b) : r)" 1);
wenzelm@10980
    99
by (rtac (major RS rtrancl_induct) 2);
wenzelm@10980
   100
by (blast_tac (claset() addIs prems) 2);
wenzelm@10980
   101
by (blast_tac (claset() addIs prems) 2);
wenzelm@10980
   102
by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
wenzelm@10980
   103
qed "rtranclE";
wenzelm@10980
   104
wenzelm@10980
   105
bind_thm ("rtrancl_into_rtrancl2", r_into_rtrancl RS rtrancl_trans);
wenzelm@10980
   106
wenzelm@10980
   107
(*** More r^* equations and inclusions ***)
wenzelm@10980
   108
wenzelm@10980
   109
Goal "(r^*)^* = r^*";
wenzelm@10980
   110
by Auto_tac;
wenzelm@10980
   111
by (etac rtrancl_induct 1);
wenzelm@10980
   112
by (rtac rtrancl_refl 1);
wenzelm@10980
   113
by (blast_tac (claset() addIs [rtrancl_trans]) 1);
wenzelm@10980
   114
qed "rtrancl_idemp";
wenzelm@10980
   115
Addsimps [rtrancl_idemp];
wenzelm@10980
   116
wenzelm@10980
   117
Goal "R^* O R^* = R^*";
wenzelm@10980
   118
by (rtac set_ext 1);
wenzelm@10980
   119
by (split_all_tac 1);
wenzelm@10980
   120
by (blast_tac (claset() addIs [rtrancl_trans]) 1);
wenzelm@10980
   121
qed "rtrancl_idemp_self_comp";
wenzelm@10980
   122
Addsimps [rtrancl_idemp_self_comp];
wenzelm@10980
   123
wenzelm@10980
   124
Goal "r <= s^* ==> r^* <= s^*";
wenzelm@10980
   125
by (dtac rtrancl_mono 1);
wenzelm@10980
   126
by (Asm_full_simp_tac 1);
wenzelm@10980
   127
qed "rtrancl_subset_rtrancl";
wenzelm@10980
   128
wenzelm@10980
   129
Goal "[| R <= S; S <= R^* |] ==> S^* = R^*";
wenzelm@10980
   130
by (dtac rtrancl_mono 1);
wenzelm@10980
   131
by (dtac rtrancl_mono 1);
wenzelm@10980
   132
by (Asm_full_simp_tac 1);
wenzelm@10980
   133
by (Blast_tac 1);
wenzelm@10980
   134
qed "rtrancl_subset";
wenzelm@10980
   135
wenzelm@10980
   136
Goal "(R^* Un S^*)^* = (R Un S)^*";
wenzelm@10980
   137
by (blast_tac (claset() addSIs [rtrancl_subset]
wenzelm@10980
   138
                        addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1);
wenzelm@10980
   139
qed "rtrancl_Un_rtrancl";
wenzelm@10980
   140
wenzelm@10980
   141
Goal "(R^=)^* = R^*";
wenzelm@10980
   142
by (blast_tac (claset() addSIs [rtrancl_subset] addIs [r_into_rtrancl]) 1);
wenzelm@10980
   143
qed "rtrancl_reflcl";
wenzelm@10980
   144
Addsimps [rtrancl_reflcl];
wenzelm@10980
   145
wenzelm@10980
   146
Goal "(r - Id)^* = r^*";
wenzelm@10980
   147
by (rtac sym 1);
wenzelm@10980
   148
by (rtac rtrancl_subset 1);
wenzelm@10980
   149
 by (Blast_tac 1);
wenzelm@10980
   150
by (Clarify_tac 1);
wenzelm@10980
   151
by (rename_tac "a b" 1);
wenzelm@10980
   152
by (case_tac "a=b" 1);
wenzelm@10980
   153
 by (Blast_tac 1);
wenzelm@10980
   154
by (blast_tac (claset() addSIs [r_into_rtrancl]) 1);
wenzelm@10980
   155
qed "rtrancl_r_diff_Id";
wenzelm@10980
   156
wenzelm@10980
   157
Goal "(x,y) : (r^-1)^* ==> (y,x) : r^*";
wenzelm@10980
   158
by (etac rtrancl_induct 1);
wenzelm@10980
   159
by (rtac rtrancl_refl 1);
wenzelm@10980
   160
by (blast_tac (claset() addIs [rtrancl_trans]) 1);
wenzelm@10980
   161
qed "rtrancl_converseD";
wenzelm@10980
   162
wenzelm@10980
   163
Goal "(y,x) : r^* ==> (x,y) : (r^-1)^*";
wenzelm@10980
   164
by (etac rtrancl_induct 1);
wenzelm@10980
   165
by (rtac rtrancl_refl 1);
wenzelm@10980
   166
by (blast_tac (claset() addIs [rtrancl_trans]) 1);
wenzelm@10980
   167
qed "rtrancl_converseI";
wenzelm@10980
   168
wenzelm@10980
   169
Goal "(r^-1)^* = (r^*)^-1";
wenzelm@10980
   170
(*blast_tac fails: the split_all_tac wrapper must be called to convert
wenzelm@10980
   171
  the set element to a pair*)
wenzelm@10980
   172
by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
wenzelm@10980
   173
qed "rtrancl_converse";
wenzelm@10980
   174
wenzelm@10980
   175
val major::prems = Goal
wenzelm@10980
   176
    "[| (a,b) : r^*; P(b); \
wenzelm@10980
   177
\       !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]  \
wenzelm@10980
   178
\     ==> P(a)";
wenzelm@10980
   179
by (rtac (major RS rtrancl_converseI RS rtrancl_induct) 1);
wenzelm@10980
   180
by (resolve_tac prems 1);
wenzelm@10980
   181
by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1);
wenzelm@10980
   182
qed "converse_rtrancl_induct";
wenzelm@10980
   183
wenzelm@10980
   184
bind_thm ("converse_rtrancl_induct2", split_rule
wenzelm@10980
   185
  (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")]converse_rtrancl_induct));
wenzelm@10980
   186
wenzelm@10980
   187
val major::prems = Goal
wenzelm@10980
   188
 "[| (x,z):r^*; \
wenzelm@10980
   189
\    x=z ==> P; \
wenzelm@10980
   190
\    !!y. [| (x,y):r; (y,z):r^* |] ==> P \
wenzelm@10980
   191
\ |] ==> P";
wenzelm@10980
   192
by (subgoal_tac "x = z  | (? y. (x,y) : r & (y,z) : r^*)" 1);
wenzelm@10980
   193
by (rtac (major RS converse_rtrancl_induct) 2);
wenzelm@10980
   194
by (blast_tac (claset() addIs prems) 2);
wenzelm@10980
   195
by (blast_tac (claset() addIs prems) 2);
wenzelm@10980
   196
by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
wenzelm@10980
   197
qed "converse_rtranclE";
wenzelm@10980
   198
wenzelm@10980
   199
bind_thm ("converse_rtranclE2", split_rule
wenzelm@10980
   200
  (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] converse_rtranclE));
wenzelm@10980
   201
wenzelm@10980
   202
Goal "r O r^* = r^* O r";
wenzelm@10980
   203
by (blast_tac (claset() addEs [rtranclE, converse_rtranclE] 
wenzelm@10980
   204
	               addIs [rtrancl_into_rtrancl, rtrancl_into_rtrancl2]) 1);
wenzelm@10980
   205
qed "r_comp_rtrancl_eq";
wenzelm@10980
   206
wenzelm@10980
   207
wenzelm@10980
   208
(**** The relation trancl ****)
wenzelm@10980
   209
wenzelm@10980
   210
section "^+";
wenzelm@10980
   211
wenzelm@10980
   212
Goalw [trancl_def] "[| p:r^+; r <= s |] ==> p:s^+";
wenzelm@10980
   213
by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1);
wenzelm@10980
   214
qed "trancl_mono";
wenzelm@10980
   215
wenzelm@10980
   216
(** Conversions between trancl and rtrancl **)
wenzelm@10980
   217
wenzelm@10980
   218
Goalw [trancl_def]
wenzelm@10980
   219
    "!!p. p : r^+ ==> p : r^*";
wenzelm@10980
   220
by (split_all_tac 1);
wenzelm@10980
   221
by (etac compEpair 1);
wenzelm@10980
   222
by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
wenzelm@10980
   223
qed "trancl_into_rtrancl";
wenzelm@10980
   224
wenzelm@10980
   225
(*r^+ contains r*)
wenzelm@10980
   226
Goalw [trancl_def]
wenzelm@10980
   227
   "!!p. p : r ==> p : r^+";
wenzelm@10980
   228
by (split_all_tac 1);
wenzelm@10980
   229
by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
wenzelm@10980
   230
qed "r_into_trancl";
wenzelm@10980
   231
AddIs [r_into_trancl];
wenzelm@10980
   232
wenzelm@10980
   233
(*intro rule by definition: from rtrancl and r*)
wenzelm@10980
   234
Goalw [trancl_def] "[| (a,b) : r^*;  (b,c) : r |]   ==>  (a,c) : r^+";
wenzelm@10980
   235
by Auto_tac;
wenzelm@10980
   236
qed "rtrancl_into_trancl1";
wenzelm@10980
   237
wenzelm@10980
   238
(*intro rule from r and rtrancl*)
wenzelm@10980
   239
Goal "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+";
wenzelm@10980
   240
by (etac rtranclE 1);
wenzelm@10980
   241
by (blast_tac (claset() addIs [r_into_trancl]) 1);
wenzelm@10980
   242
by (rtac (rtrancl_trans RS rtrancl_into_trancl1) 1);
wenzelm@10980
   243
by (REPEAT (ares_tac [r_into_rtrancl] 1));
wenzelm@10980
   244
qed "rtrancl_into_trancl2";
wenzelm@10980
   245
wenzelm@10980
   246
(*Nice induction rule for trancl*)
wenzelm@10980
   247
val major::prems = Goal
wenzelm@10980
   248
  "[| (a,b) : r^+;                                      \
wenzelm@10980
   249
\     !!y.  [| (a,y) : r |] ==> P(y);                   \
wenzelm@10980
   250
\     !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)       \
wenzelm@10980
   251
\  |] ==> P(b)";
wenzelm@10980
   252
by (rtac (rewrite_rule [trancl_def] major  RS  compEpair) 1);
wenzelm@10980
   253
(*by induction on this formula*)
wenzelm@10980
   254
by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
wenzelm@10980
   255
(*now solve first subgoal: this formula is sufficient*)
wenzelm@10980
   256
by (Blast_tac 1);
wenzelm@10980
   257
by (etac rtrancl_induct 1);
wenzelm@10980
   258
by (ALLGOALS (blast_tac (claset() addIs (rtrancl_into_trancl1::prems))));
wenzelm@10980
   259
qed "trancl_induct";
wenzelm@10980
   260
wenzelm@10980
   261
(*Another induction rule for trancl, incorporating transitivity.*)
wenzelm@10980
   262
val major::prems = Goal
wenzelm@10980
   263
 "[| (x,y) : r^+; \
wenzelm@10980
   264
\    !!x y. (x,y) : r ==> P x y; \
wenzelm@10980
   265
\    !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z \
wenzelm@10980
   266
\ |] ==> P x y";
wenzelm@10980
   267
by (blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1);
wenzelm@10980
   268
qed "trancl_trans_induct";
wenzelm@10980
   269
wenzelm@10980
   270
(*elimination of r^+ -- NOT an induction rule*)
wenzelm@10980
   271
val major::prems = Goal
wenzelm@10980
   272
    "[| (a::'a,b) : r^+;  \
wenzelm@10980
   273
\       (a,b) : r ==> P; \
wenzelm@10980
   274
\       !!y.[| (a,y) : r^+;  (y,b) : r |] ==> P  \
wenzelm@10980
   275
\    |] ==> P";
wenzelm@10980
   276
by (subgoal_tac "(a::'a,b) : r | (? y. (a,y) : r^+  &  (y,b) : r)" 1);
wenzelm@10980
   277
by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
wenzelm@10980
   278
by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
wenzelm@10980
   279
by (etac rtranclE 1);
wenzelm@10980
   280
by (Blast_tac 1);
wenzelm@10980
   281
by (blast_tac (claset() addSIs [rtrancl_into_trancl1]) 1);
wenzelm@10980
   282
qed "tranclE";
wenzelm@10980
   283
wenzelm@10980
   284
(*Transitivity of r^+.
wenzelm@10980
   285
  Proved by unfolding since it uses transitivity of rtrancl. *)
wenzelm@10980
   286
Goalw [trancl_def] "trans(r^+)";
wenzelm@10980
   287
by (rtac transI 1);
wenzelm@10980
   288
by (REPEAT (etac compEpair 1));
wenzelm@10980
   289
by (rtac (rtrancl_into_rtrancl RS (rtrancl_trans RS compI)) 1);
wenzelm@10980
   290
by (REPEAT (assume_tac 1));
wenzelm@10980
   291
qed "trans_trancl";
wenzelm@10980
   292
wenzelm@10980
   293
bind_thm ("trancl_trans", trans_trancl RS transD);
wenzelm@10980
   294
wenzelm@10980
   295
Goalw [trancl_def] "[| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
wenzelm@10980
   296
by (blast_tac (claset() addIs [rtrancl_trans]) 1);
wenzelm@10980
   297
qed "rtrancl_trancl_trancl";
wenzelm@10980
   298
wenzelm@10980
   299
(* "[| (a,b) : r;  (b,c) : r^+ |]   ==>  (a,c) : r^+" *)
wenzelm@10980
   300
bind_thm ("trancl_into_trancl2", [trans_trancl, r_into_trancl] MRS transD);
wenzelm@10980
   301
wenzelm@10980
   302
(* primitive recursion for trancl over finite relations: *)
wenzelm@10980
   303
Goal "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}";
wenzelm@10980
   304
by (rtac equalityI 1);
wenzelm@10980
   305
 by (rtac subsetI 1);
wenzelm@10980
   306
 by (split_all_tac 1);
wenzelm@10980
   307
 by (etac trancl_induct 1);
wenzelm@10980
   308
  by (blast_tac (claset() addIs [r_into_trancl]) 1);
wenzelm@10980
   309
 by (blast_tac (claset() addIs
wenzelm@10980
   310
     [rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1);
wenzelm@10980
   311
by (rtac subsetI 1);
wenzelm@10980
   312
by (blast_tac (claset() addIs
wenzelm@10980
   313
     [rtrancl_into_trancl2, rtrancl_trancl_trancl,
wenzelm@10980
   314
      impOfSubs rtrancl_mono, trancl_mono]) 1);
wenzelm@10980
   315
qed "trancl_insert";
wenzelm@10980
   316
wenzelm@10980
   317
Goalw [trancl_def] "(r^-1)^+ = (r^+)^-1";
wenzelm@10980
   318
by (simp_tac (simpset() addsimps [rtrancl_converse,converse_comp]) 1);
wenzelm@10980
   319
by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,
wenzelm@10980
   320
				  r_comp_rtrancl_eq]) 1);
wenzelm@10980
   321
qed "trancl_converse";
wenzelm@10980
   322
wenzelm@10980
   323
Goal "(x,y) : (r^+)^-1 ==> (x,y) : (r^-1)^+";
wenzelm@10980
   324
by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
wenzelm@10980
   325
qed "trancl_converseI";
wenzelm@10980
   326
wenzelm@10980
   327
Goal "(x,y) : (r^-1)^+ ==> (x,y) : (r^+)^-1";
wenzelm@10980
   328
by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1);
wenzelm@10980
   329
qed "trancl_converseD";
wenzelm@10980
   330
wenzelm@10980
   331
val major::prems = Goal
wenzelm@10980
   332
    "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y); \
wenzelm@10980
   333
\       !!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y) |]  \
wenzelm@10980
   334
\     ==> P(a)";
wenzelm@10980
   335
by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1);
wenzelm@10980
   336
 by (resolve_tac prems 1);
wenzelm@10980
   337
 by (etac converseD 1);
wenzelm@10980
   338
by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1);
wenzelm@10980
   339
qed "converse_trancl_induct";
wenzelm@10980
   340
wenzelm@10980
   341
Goal "(x,y):R^+ ==> ? z. (x,z):R & (z,y):R^*";
wenzelm@10980
   342
be converse_trancl_induct 1;
wenzelm@10980
   343
by Auto_tac;
wenzelm@10980
   344
by (blast_tac (claset() addIs [rtrancl_trans]) 1);
wenzelm@10980
   345
qed "tranclD";
wenzelm@10980
   346
wenzelm@10980
   347
(*Unused*)
wenzelm@10980
   348
Goal "r^-1 Int r^+ = {} ==> (x, x) ~: r^+";
wenzelm@10980
   349
by (subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1);
wenzelm@10980
   350
by (Fast_tac 1);
wenzelm@10980
   351
by (strip_tac 1);
wenzelm@10980
   352
by (etac trancl_induct 1);
wenzelm@10980
   353
by (auto_tac (claset() addIs [r_into_trancl], simpset()));
wenzelm@10980
   354
qed "irrefl_tranclI";
wenzelm@10980
   355
wenzelm@10980
   356
Goal "!!X. [| !x. (x, x) ~: r^+; (x,y) : r |] ==> x ~= y";
wenzelm@10980
   357
by (blast_tac (claset() addDs [r_into_trancl]) 1);
wenzelm@10980
   358
qed "irrefl_trancl_rD";
wenzelm@10980
   359
wenzelm@10980
   360
Goal "[| (a,b) : r^*;  r <= A <*> A |] ==> a=b | a:A";
wenzelm@10980
   361
by (etac rtrancl_induct 1);
wenzelm@10980
   362
by Auto_tac;
wenzelm@10980
   363
val lemma = result();
wenzelm@10980
   364
wenzelm@10980
   365
Goalw [trancl_def] "r <= A <*> A ==> r^+ <= A <*> A";
wenzelm@10980
   366
by (blast_tac (claset() addSDs [lemma]) 1);
wenzelm@10980
   367
qed "trancl_subset_Sigma";