# HG changeset patch
# User huffman
# Date 1257863419 28800
# Node ID 1806f58a365156372a44f26763d2c30b87d03e3c
# Parent  e7ba88cdf3a2477c1fa081355d23fefdedef52ff
add lemma parallel_fix_ind

diff -r e7ba88cdf3a2 -r 1806f58a3651 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Tue Nov 10 06:30:08 2009 -0800
+++ b/src/HOLCF/Fix.thy	Tue Nov 10 06:30:19 2009 -0800
@@ -179,6 +179,28 @@
 apply (simp add: step)
 done
 
+lemma parallel_fix_ind:
+  assumes adm: "adm (\<lambda>x. P (fst x) (snd x))"
+  assumes base: "P \<bottom> \<bottom>"
+  assumes step: "\<And>x y. P x y \<Longrightarrow> P (F\<cdot>x) (G\<cdot>y)"
+  shows "P (fix\<cdot>F) (fix\<cdot>G)"
+proof -
+  from adm have adm': "adm (split P)"
+    unfolding split_def .
+  have "\<And>i. P (iterate i\<cdot>F\<cdot>\<bottom>) (iterate i\<cdot>G\<cdot>\<bottom>)"
+    by (induct_tac i, simp add: base, simp add: step)
+  hence "\<And>i. split P (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>)"
+    by simp
+  hence "split P (\<Squnion>i. (iterate i\<cdot>F\<cdot>\<bottom>, iterate i\<cdot>G\<cdot>\<bottom>))"
+    by - (rule admD [OF adm'], simp, assumption)
+  hence "split P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>, \<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
+    by (simp add: thelub_Pair)
+  hence "P (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>)"
+    by simp
+  thus "P (fix\<cdot>F) (fix\<cdot>G)"
+    by (simp add: fix_def2)
+qed
+
 subsection {* Recursive let bindings *}
 
 definition