added finite_acyclic_wf_converse
authoroheimb
Tue, 24 Mar 1998 15:46:08 +0100
changeset 4749 35b47e36e615
parent 4748 2b8ead8e9393
child 4750 f83cd6a06676
added finite_acyclic_wf_converse
src/HOL/WF_Rel.ML
--- a/src/HOL/WF_Rel.ML	Mon Mar 23 13:56:53 1998 +0100
+++ b/src/HOL/WF_Rel.ML	Tue Mar 24 15:46:08 1998 +0100
@@ -117,6 +117,11 @@
 by (Asm_full_simp_tac 1);
 qed_spec_mp "finite_acyclic_wf";
 
+qed_goal "finite_acyclic_wf_converse" thy 
+ "X. finite r; acyclic r  wf (r^-1)" (K [
+	etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1,
+	etac (acyclic_converse RS iffD2) 1]);
+
 goal thy "!!r. finite r ==> wf r = acyclic r";
 by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
 qed "wf_iff_acyclic_if_finite";