--- a/src/HOL/WF.ML Sun Feb 20 09:32:06 2000 +0100
+++ b/src/HOL/WF.ML Mon Feb 21 10:20:38 2000 +0100
@@ -230,6 +230,19 @@
Goalw [acyclic_def] "acyclic(r^-1) = acyclic r";
by (simp_tac (simpset() addsimps [trancl_converse]) 1);
qed "acyclic_converse";
+AddIffs [acyclic_converse];
+
+Goalw [acyclic_def,antisym_def] "acyclic r ==> antisym(r^*)";
+by(blast_tac (claset() addEs [rtranclE]
+ addIs [rtrancl_into_trancl1,rtrancl_trancl_trancl]) 1);
+qed "acyclic_impl_antisym_rtrancl";
+
+(* Other direction:
+acyclic = no loops
+antisym = only self loops
+Goalw [acyclic_def,antisym_def] "antisym(r^* ) ==> acyclic(r - Id)";
+==> "antisym(r^* ) = acyclic(r - Id)";
+*)
Goalw [acyclic_def] "[| acyclic s; r <= s |] ==> acyclic r";
by (blast_tac (claset() addIs [trancl_mono]) 1);