# HG changeset patch
# User huffman
# Date 1131232923 -3600
# Node ID 4328356ab7e67e53a72483dce320ccf3f6da98d2
# Parent  404f298220afe08e628f13d1624da69852052cfd
add proof of Bekic's theorem: fix_cprod

diff -r 404f298220af -r 4328356ab7e6 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Sat Nov 05 21:56:45 2005 +0100
+++ b/src/HOLCF/Fix.thy	Sun Nov 06 00:22:03 2005 +0100
@@ -108,9 +108,7 @@
 
 lemma fix_eqI: "\<lbrakk>F\<cdot>x = x; \<forall>z. F\<cdot>z = z \<longrightarrow> x \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x = fix\<cdot>F"
 apply (rule antisym_less)
-apply (erule allE)
-apply (erule mp)
-apply (rule fix_eq [symmetric])
+apply (simp add: fix_eq [symmetric])
 apply (erule fix_least)
 done
 
@@ -190,6 +188,38 @@
   "Letrec xs = a in \<langle>e,es\<rangle>"    == "CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e,es\<rangle>)"
   "Letrec xs = a in e"         == "CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e\<rangle>)"
 
+text {*
+  Bekic's Theorem: Simultaneous fixed points over pairs
+  can be written in terms of separate fixed points.
+*}
+
+lemma fix_cprod:
+  "fix\<cdot>(F::'a \<times> 'b \<rightarrow> 'a \<times> 'b) =
+   \<langle>\<mu> x. cfst\<cdot>(F\<cdot>\<langle>x, \<mu> y. csnd\<cdot>(F\<cdot>\<langle>x, y\<rangle>)\<rangle>),
+    \<mu> y. csnd\<cdot>(F\<cdot>\<langle>\<mu> x. cfst\<cdot>(F\<cdot>\<langle>x, \<mu> y. csnd\<cdot>(F\<cdot>\<langle>x, y\<rangle>)\<rangle>), y\<rangle>)\<rangle>"
+  (is "fix\<cdot>F = \<langle>?x, ?y\<rangle>")
+proof (rule fix_eqI [rule_format, symmetric])
+  have 1: "cfst\<cdot>(F\<cdot>\<langle>?x, ?y\<rangle>) = ?x"
+    by (rule trans [symmetric, OF fix_eq], simp)
+  have 2: "csnd\<cdot>(F\<cdot>\<langle>?x, ?y\<rangle>) = ?y"
+    by (rule trans [symmetric, OF fix_eq], simp)
+  from 1 2 show "F\<cdot>\<langle>?x, ?y\<rangle> = \<langle>?x, ?y\<rangle>" by (simp add: eq_cprod)
+next
+  fix z assume F_z: "F\<cdot>z = z"
+  then obtain x y where z: "z = \<langle>x,y\<rangle>" by (rule_tac p=z in cprodE)
+  from F_z z have F_x: "cfst\<cdot>(F\<cdot>\<langle>x, y\<rangle>) = x" by simp
+  from F_z z have F_y: "csnd\<cdot>(F\<cdot>\<langle>x, y\<rangle>) = y" by simp
+  let ?y1 = "\<mu> y. csnd\<cdot>(F\<cdot>\<langle>x, y\<rangle>)"
+  have "?y1 \<sqsubseteq> y" by (rule fix_least, simp add: F_y)
+  hence "cfst\<cdot>(F\<cdot>\<langle>x, ?y1\<rangle>) \<sqsubseteq> cfst\<cdot>(F\<cdot>\<langle>x, y\<rangle>)" by (simp add: monofun_cfun)
+  hence "cfst\<cdot>(F\<cdot>\<langle>x, ?y1\<rangle>) \<sqsubseteq> x" using F_x by simp
+  hence 1: "?x \<sqsubseteq> x" by (simp add: fix_least_less)
+  hence "csnd\<cdot>(F\<cdot>\<langle>?x, y\<rangle>) \<sqsubseteq> csnd\<cdot>(F\<cdot>\<langle>x, y\<rangle>)" by (simp add: monofun_cfun)
+  hence "csnd\<cdot>(F\<cdot>\<langle>?x, y\<rangle>) \<sqsubseteq> y" using F_y by simp
+  hence 2: "?y \<sqsubseteq> y" by (simp add: fix_least_less)
+  show "\<langle>?x, ?y\<rangle> \<sqsubseteq> z" using z 1 2 by simp
+qed
+
 subsection {* Weak admissibility *}
 
 constdefs