author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8703  816d8f6513be 
child 9022  a389be05c06f 
permissions  rwrr 
4764
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

1 
(* Title: HOL/Trancl 
923  2 
ID: $Id$ 
1465  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
923  4 
Copyright 1992 University of Cambridge 
5 

5316  6 
Theorems about the transitive closure of a relation 
923  7 
*) 
8 

5771  9 
(** The relation rtrancl **) 
923  10 

5771  11 
section "^*"; 
923  12 

5608  13 
Goal "mono(%s. Id Un (r O s))"; 
923  14 
by (rtac monoI 1); 
15 
by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1)); 

16 
qed "rtrancl_fun_mono"; 

17 

18 
val rtrancl_unfold = rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski); 

19 

20 
(*Reflexivity of rtrancl*) 

5069  21 
Goal "(a,a) : r^*"; 
923  22 
by (stac rtrancl_unfold 1); 
2891  23 
by (Blast_tac 1); 
923  24 
qed "rtrancl_refl"; 
25 

1921  26 
Addsimps [rtrancl_refl]; 
27 
AddSIs [rtrancl_refl]; 

28 

29 

923  30 
(*Closure under composition with r*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

31 
Goal "[ (a,b) : r^*; (b,c) : r ] ==> (a,c) : r^*"; 
923  32 
by (stac rtrancl_unfold 1); 
2891  33 
by (Blast_tac 1); 
923  34 
qed "rtrancl_into_rtrancl"; 
35 

36 
(*rtrancl of r contains r*) 

5069  37 
Goal "!!p. p : r ==> p : r^*"; 
1552  38 
by (split_all_tac 1); 
1301  39 
by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1); 
923  40 
qed "r_into_rtrancl"; 
41 

42 
(*monotonicity of rtrancl*) 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

43 
Goalw [rtrancl_def] "r <= s ==> r^* <= s^*"; 
1552  44 
by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1)); 
923  45 
qed "rtrancl_mono"; 
46 

47 
(** standard induction rule **) 

48 

5316  49 
val major::prems = Goal 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

50 
"[ (a,b) : r^*; \ 
8114  51 
\ !!x. P(x,x); \ 
52 
\ !!x y z.[ P(x,y); (x,y): r^*; (y,z): r ] ==> P(x,z) ] \ 

53 
\ ==> P(a,b)"; 

923  54 
by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1); 
4089  55 
by (blast_tac (claset() addIs prems) 1); 
923  56 
qed "rtrancl_full_induct"; 
57 

58 
(*nice induction rule*) 

5316  59 
val major::prems = Goal 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

60 
"[ (a::'a,b) : r^*; \ 
923  61 
\ P(a); \ 
1465  62 
\ !!y z.[ (a,y) : r^*; (y,z) : r; P(y) ] ==> P(z) ] \ 
923  63 
\ ==> P(b)"; 
64 
(*by induction on this formula*) 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

65 
by (subgoal_tac "! y. (a::'a,b) = (a,y) > P(y)" 1); 
923  66 
(*now solve first subgoal: this formula is sufficient*) 
2891  67 
by (Blast_tac 1); 
923  68 
(*now do the induction*) 
69 
by (resolve_tac [major RS rtrancl_full_induct] 1); 

4089  70 
by (blast_tac (claset() addIs prems) 1); 
71 
by (blast_tac (claset() addIs prems) 1); 

923  72 
qed "rtrancl_induct"; 
73 

5098  74 
bind_thm ("rtrancl_induct2", split_rule 
75 
(read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] rtrancl_induct)); 

1706
4e0d5c7f57fa
Added backwards rtrancl_induct and special versions for pairs.
nipkow
parents:
1642
diff
changeset

76 

923  77 
(*transitivity of transitive closure!!  by induction.*) 
5069  78 
Goalw [trans_def] "trans(r^*)"; 
4153  79 
by Safe_tac; 
1642  80 
by (eres_inst_tac [("b","z")] rtrancl_induct 1); 
4089  81 
by (ALLGOALS(blast_tac (claset() addIs [rtrancl_into_rtrancl]))); 
1642  82 
qed "trans_rtrancl"; 
83 

84 
bind_thm ("rtrancl_trans", trans_rtrancl RS transD); 

85 

923  86 

87 
(*elimination of rtrancl  by induction on a special formula*) 

5316  88 
val major::prems = Goal 
1465  89 
"[ (a::'a,b) : r^*; (a = b) ==> P; \ 
90 
\ !!y.[ (a,y) : r^*; (y,b) : r ] ==> P \ 

923  91 
\ ] ==> P"; 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

92 
by (subgoal_tac "(a::'a) = b  (? y. (a,y) : r^* & (y,b) : r)" 1); 
923  93 
by (rtac (major RS rtrancl_induct) 2); 
4089  94 
by (blast_tac (claset() addIs prems) 2); 
95 
by (blast_tac (claset() addIs prems) 2); 

923  96 
by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1)); 
97 
qed "rtranclE"; 

98 

1642  99 
bind_thm ("rtrancl_into_rtrancl2", r_into_rtrancl RS rtrancl_trans); 
100 

101 

102 
(*** More r^* equations and inclusions ***) 

103 

5069  104 
Goal "(r^*)^* = r^*"; 
8320  105 
by Auto_tac; 
106 
by (etac r_into_rtrancl 2); 

1552  107 
by (etac rtrancl_induct 1); 
1642  108 
by (rtac rtrancl_refl 1); 
4089  109 
by (blast_tac (claset() addIs [rtrancl_trans]) 1); 
1642  110 
qed "rtrancl_idemp"; 
111 
Addsimps [rtrancl_idemp]; 

112 

5069  113 
Goal "R^* O R^* = R^*"; 
5132  114 
by (rtac set_ext 1); 
115 
by (split_all_tac 1); 

116 
by (blast_tac (claset() addIs [rtrancl_trans]) 1); 

4830  117 
qed "rtrancl_idemp_self_comp"; 
118 
Addsimps [rtrancl_idemp_self_comp]; 

119 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

120 
Goal "r <= s^* ==> r^* <= s^*"; 
2031  121 
by (dtac rtrancl_mono 1); 
1642  122 
by (Asm_full_simp_tac 1); 
123 
qed "rtrancl_subset_rtrancl"; 

124 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

125 
Goal "[ R <= S; S <= R^* ] ==> S^* = R^*"; 
1642  126 
by (dtac rtrancl_mono 1); 
127 
by (dtac rtrancl_mono 1); 

128 
by (Asm_full_simp_tac 1); 

2891  129 
by (Blast_tac 1); 
1642  130 
qed "rtrancl_subset"; 
131 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

132 
Goal "(R^* Un S^*)^* = (R Un S)^*"; 
5479  133 
by (blast_tac (claset() addSIs [rtrancl_subset] 
134 
addIs [r_into_rtrancl, rtrancl_mono RS subsetD]) 1); 

1642  135 
qed "rtrancl_Un_rtrancl"; 
1496  136 

5069  137 
Goal "(R^=)^* = R^*"; 
5281  138 
by (blast_tac (claset() addSIs [rtrancl_subset] addIs [r_into_rtrancl]) 1); 
1642  139 
qed "rtrancl_reflcl"; 
140 
Addsimps [rtrancl_reflcl]; 

141 

8265  142 
Goal "(r  Id)^* = r^*"; 
8320  143 
by (rtac sym 1); 
144 
by (rtac rtrancl_subset 1); 

8265  145 
by (Blast_tac 1); 
146 
by (Clarify_tac 1); 

8320  147 
by (rename_tac "a b" 1); 
148 
by (case_tac "a=b" 1); 

8265  149 
by (Blast_tac 1); 
8320  150 
by (blast_tac (claset() addSIs [r_into_rtrancl]) 1); 
8265  151 
qed "rtrancl_r_diff_Id"; 
152 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

153 
Goal "(x,y) : (r^1)^* ==> (x,y) : (r^*)^1"; 
4746  154 
by (rtac converseI 1); 
1642  155 
by (etac rtrancl_induct 1); 
156 
by (rtac rtrancl_refl 1); 

4089  157 
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1); 
4746  158 
qed "rtrancl_converseD"; 
1642  159 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

160 
Goal "(x,y) : (r^*)^1 ==> (x,y) : (r^1)^*"; 
4746  161 
by (dtac converseD 1); 
1642  162 
by (etac rtrancl_induct 1); 
163 
by (rtac rtrancl_refl 1); 

4089  164 
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1); 
4746  165 
qed "rtrancl_converseI"; 
1642  166 

5069  167 
Goal "(r^1)^* = (r^*)^1"; 
4838  168 
by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI])); 
4746  169 
qed "rtrancl_converse"; 
1642  170 

5316  171 
val major::prems = Goal 
1706
4e0d5c7f57fa
Added backwards rtrancl_induct and special versions for pairs.
nipkow
parents:
1642
diff
changeset

172 
"[ (a,b) : r^*; P(b); \ 
4e0d5c7f57fa
Added backwards rtrancl_induct and special versions for pairs.
nipkow
parents:
1642
diff
changeset

173 
\ !!y z.[ (y,z) : r; (z,b) : r^*; P(z) ] ==> P(y) ] \ 
4e0d5c7f57fa
Added backwards rtrancl_induct and special versions for pairs.
nipkow
parents:
1642
diff
changeset

174 
\ ==> P(a)"; 
4746  175 
by (rtac ((major RS converseI RS rtrancl_converseI) RS rtrancl_induct) 1); 
2031  176 
by (resolve_tac prems 1); 
4746  177 
by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1); 
178 
qed "converse_rtrancl_induct"; 

1706
4e0d5c7f57fa
Added backwards rtrancl_induct and special versions for pairs.
nipkow
parents:
1642
diff
changeset

179 

5347  180 
bind_thm ("converse_rtrancl_induct2", split_rule 
181 
(read_instantiate [("a","(ax,ay)"),("b","(bx,by)")]converse_rtrancl_induct)); 

1496  182 

5316  183 
val major::prems = Goal 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

184 
"[ (x,z):r^*; \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

185 
\ x=z ==> P; \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

186 
\ !!y. [ (x,y):r; (y,z):r^* ] ==> P \ 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

187 
\ ] ==> P"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

188 
by (subgoal_tac "x = z  (? y. (x,y) : r & (y,z) : r^*)" 1); 
4746  189 
by (rtac (major RS converse_rtrancl_induct) 2); 
4089  190 
by (blast_tac (claset() addIs prems) 2); 
191 
by (blast_tac (claset() addIs prems) 2); 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

192 
by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1)); 
5347  193 
qed "converse_rtranclE"; 
194 

195 
bind_thm ("converse_rtranclE2", split_rule 

196 
(read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] converse_rtranclE)); 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

197 

5069  198 
Goal "r O r^* = r^* O r"; 
5347  199 
by (blast_tac (claset() addEs [rtranclE, converse_rtranclE] 
3723  200 
addIs [rtrancl_into_rtrancl, rtrancl_into_rtrancl2]) 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

201 
qed "r_comp_rtrancl_eq"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

202 

923  203 

204 
(**** The relation trancl ****) 

205 

5771  206 
section "^+"; 
207 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset

208 
Goalw [trancl_def] "[ p:r^+; r <= s ] ==> p:s^+"; 
4089  209 
by (blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

210 
qed "trancl_mono"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

211 

923  212 
(** Conversions between trancl and rtrancl **) 
213 

5069  214 
Goalw [trancl_def] 
4764
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

215 
"!!p. p : r^+ ==> p : r^*"; 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

216 
by (split_all_tac 1); 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

217 
by (etac compEpair 1); 
923  218 
by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1)); 
219 
qed "trancl_into_rtrancl"; 

220 

221 
(*r^+ contains r*) 

5069  222 
Goalw [trancl_def] 
4764
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

223 
"!!p. p : r ==> p : r^+"; 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

224 
by (split_all_tac 1); 
923  225 
by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1)); 
226 
qed "r_into_trancl"; 

227 

228 
(*intro rule by definition: from rtrancl and r*) 

5255  229 
Goalw [trancl_def] "[ (a,b) : r^*; (b,c) : r ] ==> (a,c) : r^+"; 
230 
by Auto_tac; 

923  231 
qed "rtrancl_into_trancl1"; 
232 

233 
(*intro rule from r and rtrancl*) 

5255  234 
Goal "[ (a,b) : r; (b,c) : r^* ] ==> (a,c) : r^+"; 
235 
by (etac rtranclE 1); 

236 
by (blast_tac (claset() addIs [r_into_trancl]) 1); 

1122
20b708827030
renamed trans_rtrancl to rtrancl_trans and modified it by expanding trans.
nipkow
parents:
1121
diff
changeset

237 
by (rtac (rtrancl_trans RS rtrancl_into_trancl1) 1); 
5255  238 
by (REPEAT (ares_tac [r_into_rtrancl] 1)); 
923  239 
qed "rtrancl_into_trancl2"; 
240 

1642  241 
(*Nice induction rule for trancl*) 
5316  242 
val major::prems = Goal 
1642  243 
"[ (a,b) : r^+; \ 
244 
\ !!y. [ (a,y) : r ] ==> P(y); \ 

245 
\ !!y z.[ (a,y) : r^+; (y,z) : r; P(y) ] ==> P(z) \ 

246 
\ ] ==> P(b)"; 

247 
by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1); 

248 
(*by induction on this formula*) 

249 
by (subgoal_tac "ALL z. (y,z) : r > P(z)" 1); 

250 
(*now solve first subgoal: this formula is sufficient*) 

2891  251 
by (Blast_tac 1); 
1642  252 
by (etac rtrancl_induct 1); 
4089  253 
by (ALLGOALS (blast_tac (claset() addIs (rtrancl_into_trancl1::prems)))); 
1642  254 
qed "trancl_induct"; 
255 

6856  256 
(*Another induction rule for trancl, incorporating transitivity.*) 
257 
val major::prems = goal thy 

258 
"[ (x,y) : r^+; \ 

259 
\ !!x y. (x,y) : r ==> P x y; \ 

260 
\ !!x y z. [ (x,y) : r^+; P x y; (y,z) : r^+; P y z ] ==> P x z \ 

261 
\ ] ==> P x y"; 

7007  262 
by (blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1); 
6856  263 
qed "trancl_trans_induct"; 
264 

923  265 
(*elimination of r^+  NOT an induction rule*) 
5316  266 
val major::prems = Goal 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

267 
"[ (a::'a,b) : r^+; \ 
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

268 
\ (a,b) : r ==> P; \ 
1465  269 
\ !!y.[ (a,y) : r^+; (y,b) : r ] ==> P \ 
923  270 
\ ] ==> P"; 
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
923
diff
changeset

271 
by (subgoal_tac "(a::'a,b) : r  (? y. (a,y) : r^+ & (y,b) : r)" 1); 
923  272 
by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1)); 
273 
by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1); 

274 
by (etac rtranclE 1); 

2891  275 
by (Blast_tac 1); 
4089  276 
by (blast_tac (claset() addSIs [rtrancl_into_trancl1]) 1); 
923  277 
qed "tranclE"; 
278 

279 
(*Transitivity of r^+. 

280 
Proved by unfolding since it uses transitivity of rtrancl. *) 

5069  281 
Goalw [trancl_def] "trans(r^+)"; 
923  282 
by (rtac transI 1); 
283 
by (REPEAT (etac compEpair 1)); 

1122
20b708827030
renamed trans_rtrancl to rtrancl_trans and modified it by expanding trans.
nipkow
parents:
1121
diff
changeset

284 
by (rtac (rtrancl_into_rtrancl RS (rtrancl_trans RS compI)) 1); 
923  285 
by (REPEAT (assume_tac 1)); 
286 
qed "trans_trancl"; 

287 

1642  288 
bind_thm ("trancl_trans", trans_trancl RS transD); 
289 

5255  290 
Goalw [trancl_def] "[ (x,y):r^*; (y,z):r^+ ] ==> (x,z):r^+"; 
4089  291 
by (blast_tac (claset() addIs [rtrancl_trans,r_into_rtrancl]) 1); 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

292 
qed "rtrancl_trancl_trancl"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

293 

5255  294 
(* "[ (a,b) : r; (b,c) : r^+ ] ==> (a,c) : r^+" *) 
295 
bind_thm ("trancl_into_trancl2", [trans_trancl, r_into_trancl] MRS transD); 

923  296 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

297 
(* primitive recursion for trancl over finite relations: *) 
5069  298 
Goal "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}"; 
3457  299 
by (rtac equalityI 1); 
300 
by (rtac subsetI 1); 

301 
by (split_all_tac 1); 

302 
by (etac trancl_induct 1); 

4089  303 
by (blast_tac (claset() addIs [r_into_trancl]) 1); 
304 
by (blast_tac (claset() addIs 

3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

305 
[rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1); 
3457  306 
by (rtac subsetI 1); 
4089  307 
by (blast_tac (claset() addIs 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

308 
[rtrancl_into_trancl2, rtrancl_trancl_trancl, 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

309 
impOfSubs rtrancl_mono, trancl_mono]) 1); 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

310 
qed "trancl_insert"; 
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

311 

5069  312 
Goalw [trancl_def] "(r^1)^+ = (r^+)^1"; 
4746  313 
by (simp_tac (simpset() addsimps [rtrancl_converse,converse_comp]) 1); 
5451  314 
by (simp_tac (simpset() addsimps [rtrancl_converse RS sym, 
315 
r_comp_rtrancl_eq]) 1); 

4746  316 
qed "trancl_converse"; 
3413
c1f63cc3a768
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
nipkow
parents:
2935
diff
changeset

317 

5771  318 
Goal "(x,y) : (r^+)^1 ==> (x,y) : (r^1)^+"; 
319 
by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1); 

320 
qed "trancl_converseI"; 

321 

322 
Goal "(x,y) : (r^1)^+ ==> (x,y) : (r^+)^1"; 

323 
by (asm_full_simp_tac (simpset() addsimps [trancl_converse]) 1); 

324 
qed "trancl_converseD"; 

325 

326 
val major::prems = Goal 

327 
"[ (a,b) : r^+; !!y. (y,b) : r ==> P(y); \ 

328 
\ !!y z.[ (y,z) : r; (z,b) : r^+; P(z) ] ==> P(y) ] \ 

329 
\ ==> P(a)"; 

330 
by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1); 

331 
by (resolve_tac prems 1); 

6162  332 
by (etac converseD 1); 
5771  333 
by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1); 
334 
qed "converse_trancl_induct"; 

335 

5451  336 
(*Unused*) 
7007  337 
Goal "r^1 Int r^+ = {} ==> (x, x) ~: r^+"; 
338 
by (subgoal_tac "!y. (x, y) : r^+ > x~=y" 1); 

339 
by (Fast_tac 1); 

340 
by (strip_tac 1); 

341 
by (etac trancl_induct 1); 

342 
by (auto_tac (claset() addIs [r_into_trancl], simpset())); 

343 
qed "irrefl_tranclI"; 

1130  344 

8703  345 
Goal "[ (a,b) : r^*; r <= A <*> A ] ==> a=b  a:A"; 
5255  346 
by (etac rtrancl_induct 1); 
347 
by Auto_tac; 

1642  348 
val lemma = result(); 
923  349 

8703  350 
Goalw [trancl_def] "r <= A <*> A ==> r^+ <= A <*> A"; 
4089  351 
by (blast_tac (claset() addSDs [lemma]) 1); 
923  352 
qed "trancl_subset_Sigma"; 
1130  353 

4764
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

354 

5069  355 
Goal "(r^+)^= = r^*"; 
4838  356 
by Safe_tac; 
4764
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

357 
by (etac trancl_into_rtrancl 1); 
8265  358 
by (blast_tac (claset() addEs [rtranclE] addDs [rtrancl_into_trancl1]) 1); 
4764
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

359 
qed "reflcl_trancl"; 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

360 
Addsimps[reflcl_trancl]; 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

361 

5069  362 
Goal "(r^=)^+ = r^*"; 
4838  363 
by Safe_tac; 
4764
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

364 
by (dtac trancl_into_rtrancl 1); 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

365 
by (Asm_full_simp_tac 1); 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

366 
by (etac rtranclE 1); 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

367 
by Safe_tac; 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

368 
by (rtac r_into_trancl 1); 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

369 
by (Simp_tac 1); 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

370 
by (rtac rtrancl_into_trancl1 1); 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

371 
by (etac (rtrancl_reflcl RS equalityD2 RS subsetD) 1); 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

372 
by (Fast_tac 1); 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

373 
qed "trancl_reflcl"; 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

374 
Addsimps[trancl_reflcl]; 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

375 

7007  376 
Goal "{}^+ = {}"; 
377 
by (auto_tac (claset() addEs [trancl_induct], simpset())); 

378 
qed "trancl_empty"; 

4764
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

379 
Addsimps[trancl_empty]; 
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

380 

7007  381 
Goal "{}^* = Id"; 
382 
by (rtac (reflcl_trancl RS subst) 1); 

383 
by (Simp_tac 1); 

384 
qed "rtrancl_empty"; 

4764
9b3293646b5d
generalized appearance of trancl_into_rtrancl and r_into_trancl
oheimb
parents:
4746
diff
changeset

385 
Addsimps[rtrancl_empty]; 