# HG changeset patch
# User huffman
# Date 1269323001 25200
# Node ID cd1b0166481037bc96c4ef630aa17bbba2c12386
# Parent  9ef9a20cfba13c056c460a9dad815e2a0b1b1abf
convert lemma fix_cprod to use Pair, fst, snd

diff -r 9ef9a20cfba1 -r cd1b01664810 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Mon Mar 22 22:42:34 2010 -0700
+++ b/src/HOLCF/Fix.thy	Mon Mar 22 22:43:21 2010 -0700
@@ -236,29 +236,31 @@
 
 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>")
+   (\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))),
+    \<mu> y. snd (F\<cdot>(\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))), y)))"
+  (is "fix\<cdot>F = (?x, ?y)")
 proof (rule fix_eqI)
-  have 1: "cfst\<cdot>(F\<cdot>\<langle>?x, ?y\<rangle>) = ?x"
+  have 1: "fst (F\<cdot>(?x, ?y)) = ?x"
     by (rule trans [symmetric, OF fix_eq], simp)
-  have 2: "csnd\<cdot>(F\<cdot>\<langle>?x, ?y\<rangle>) = ?y"
+  have 2: "snd (F\<cdot>(?x, ?y)) = ?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)
+  from 1 2 show "F\<cdot>(?x, ?y) = (?x, ?y)" by (simp add: Pair_fst_snd_eq)
 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>)"
+  obtain x y where z: "z = (x,y)" by (rule prod.exhaust)
+  from F_z z have F_x: "fst (F\<cdot>(x, y)) = x" by simp
+  from F_z z have F_y: "snd (F\<cdot>(x, y)) = y" by simp
+  let ?y1 = "\<mu> y. snd (F\<cdot>(x, y))"
   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 "fst (F\<cdot>(x, ?y1)) \<sqsubseteq> fst (F\<cdot>(x, y))"
+    by (simp add: fst_monofun monofun_cfun)
+  hence "fst (F\<cdot>(x, ?y1)) \<sqsubseteq> x" using F_x by simp
   hence 1: "?x \<sqsubseteq> x" by (simp add: fix_least_below)
-  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 "snd (F\<cdot>(?x, y)) \<sqsubseteq> snd (F\<cdot>(x, y))"
+    by (simp add: snd_monofun monofun_cfun)
+  hence "snd (F\<cdot>(?x, y)) \<sqsubseteq> y" using F_y by simp
   hence 2: "?y \<sqsubseteq> y" by (simp add: fix_least_below)
-  show "\<langle>?x, ?y\<rangle> \<sqsubseteq> z" using z 1 2 by simp
+  show "(?x, ?y) \<sqsubseteq> z" using z 1 2 by simp
 qed
 
 end