--- a/src/HOL/HOLCF/Fix.thy Mon Dec 20 09:48:16 2010 -0800
+++ b/src/HOL/HOLCF/Fix.thy Mon Dec 20 10:48:01 2010 -0800
@@ -148,6 +148,10 @@
apply (rule nat_induct, simp_all)
done
+lemma cont_fix_ind:
+ "\<lbrakk>cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>(Abs_cfun F))"
+by (simp add: fix_ind)
+
lemma def_fix_ind:
"\<lbrakk>f \<equiv> fix\<cdot>F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P f"
by (simp add: fix_ind)
@@ -190,6 +194,14 @@
by (simp add: fix_def2)
qed
+lemma cont_parallel_fix_ind:
+ assumes "cont F" and "cont G"
+ assumes "adm (\<lambda>x. P (fst x) (snd x))"
+ assumes "P \<bottom> \<bottom>"
+ assumes "\<And>x y. P x y \<Longrightarrow> P (F x) (G y)"
+ shows "P (fix\<cdot>(Abs_cfun F)) (fix\<cdot>(Abs_cfun G))"
+by (rule parallel_fix_ind, simp_all add: assms)
+
subsection {* Fixed-points on product types *}
text {*