--- a/src/HOL/Trancl.ML Thu Jun 05 14:06:23 1997 +0200
+++ b/src/HOL/Trancl.ML Thu Jun 05 14:39:22 1997 +0200
@@ -182,9 +182,31 @@
by (REPEAT(ares_tac prems 1));
qed "converse_rtrancl_induct2";
+val major::prems = goal Trancl.thy
+ "[| (x,z):r^*; \
+\ x=z ==> P; \
+\ !!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 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));
+qed "rtranclE2";
+
+goal Trancl.thy "r O r^* = r^* O r";
+by(Step_tac 1);
+ by(blast_tac (!claset addEs [rtranclE2] addIs [rtrancl_into_rtrancl]) 1);
+by(blast_tac (!claset addEs [rtranclE] addIs [rtrancl_into_rtrancl2]) 1);
+qed "r_comp_rtrancl_eq";
+
(**** The relation trancl ****)
+goalw Trancl.thy [trancl_def] "!!p.[| p:r^+; r <= s |] ==> p:s^+";
+by(blast_tac (!claset addIs [rtrancl_mono RS subsetD]) 1);
+qed "trancl_mono";
+
(** Conversions between trancl and rtrancl **)
val [major] = goalw Trancl.thy [trancl_def]
@@ -255,6 +277,11 @@
bind_thm ("trancl_trans", trans_trancl RS transD);
+goalw Trancl.thy [trancl_def]
+ "!!r. [| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
+by(blast_tac (!claset addIs [rtrancl_trans,r_into_rtrancl]) 1);
+qed "rtrancl_trancl_trancl";
+
val prems = goal Trancl.thy
"[| (a,b) : r; (b,c) : r^+ |] ==> (a,c) : r^+";
by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1);
@@ -262,6 +289,26 @@
by (resolve_tac prems 1);
qed "trancl_into_trancl2";
+(* primitive recursion for trancl over finite relations: *)
+goal Trancl.thy "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}";
+br equalityI 1;
+ br subsetI 1;
+ by(split_all_tac 1);
+ be trancl_induct 1;
+ by(blast_tac (!claset addIs [r_into_trancl]) 1);
+ by(blast_tac (!claset addIs
+ [rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1);
+br subsetI 1;
+by(blast_tac (!claset addIs
+ [rtrancl_into_trancl2, rtrancl_trancl_trancl,
+ impOfSubs rtrancl_mono, trancl_mono]) 1);
+qed "trancl_insert";
+
+goalw Trancl.thy [trancl_def] "(converse r)^+ = converse(r^+)";
+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,b) : r^*; r <= A Times A |] ==> a=b | a:A";