src/HOL/BNF/BNF_LFP.thy
changeset 54841 af71b753c459
parent 54246 8fdb4dc08ed1
child 55023 38db7814481d
--- a/src/HOL/BNF/BNF_LFP.thy	Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/BNF_LFP.thy	Wed Dec 18 11:03:40 2013 +0100
@@ -224,6 +224,10 @@
   shows "PROP P x y"
 by (rule `(\<And>x y. PROP P x y)`)
 
+lemma nchotomy_relcomppE:
+  "\<lbrakk>\<And>y. \<exists>x. y = f x; (r OO s) a c; (\<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
+  by (metis relcompp.cases)
+
 lemma vimage2p_fun_rel: "(fun_rel (vimage2p f g R) R) f g"
   unfolding fun_rel_def vimage2p_def by auto