# HG changeset patch
# User oheimb
# Date 991318648 -7200
# Node ID c150861633da510994f7103996f18f8ee2b5f612
# Parent  a16eaf2a1edd9b9b085ea06b4f6a1a9facfe32f5
added weak_coinduct_image

diff -r a16eaf2a1edd -r c150861633da src/HOL/Gfp.ML
--- a/src/HOL/Gfp.ML	Thu May 31 16:07:35 2001 +0200
+++ b/src/HOL/Gfp.ML	Thu May 31 16:17:28 2001 +0200
@@ -42,6 +42,11 @@
 by Auto_tac;
 qed "weak_coinduct";
 
+Goal "!!X. [| a : X; g`X <= f (g`X) |] ==> g a : gfp f";
+by (etac (gfp_upperbound RS subsetD) 1);
+by (etac imageI 1);
+qed "weak_coinduct_image";
+
 Goal "[| X <= f(X Un gfp(f));  mono(f) |] ==>  \
 \    X Un gfp(f) <= f(X Un gfp(f))";
 by (blast_tac (claset() addDs [gfp_lemma2, mono_Un]) 1);