diff -r eb3094c6576c -r b4b672f09270 src/HOL/Library/Order_Continuity.thy
--- a/src/HOL/Library/Order_Continuity.thy Thu Jun 11 00:13:25 2015 +0100
+++ b/src/HOL/Library/Order_Continuity.thy Thu Jun 11 18:24:44 2015 +0200
@@ -91,6 +91,19 @@
qed
qed
+lemma lfp_transfer:
+ assumes \: "sup_continuous \" and f: "sup_continuous f" and g: "sup_continuous g"
+ assumes [simp]: "\ bot = bot" "\x. \ (f x) = g (\ x)"
+ shows "\ (lfp f) = lfp g"
+proof -
+ have "\ (lfp f) = (SUP i. \ ((f^^i) bot))"
+ unfolding sup_continuous_lfp[OF f] by (intro f \ sup_continuousD mono_funpow sup_continuous_mono)
+ moreover have "\ ((f^^i) bot) = (g^^i) bot" for i
+ by (induction i; simp)
+ ultimately show ?thesis
+ unfolding sup_continuous_lfp[OF g] by simp
+qed
+
definition
inf_continuous :: "('a::complete_lattice \ 'a::complete_lattice) \ bool" where
"inf_continuous F \ (\M::nat \ 'a. antimono M \ F (INF i. M i) = (INF i. F (M i)))"
@@ -146,4 +159,17 @@
qed
qed
+lemma gfp_transfer:
+ assumes \: "inf_continuous \" and f: "inf_continuous f" and g: "inf_continuous g"
+ assumes [simp]: "\ top = top" "\x. \ (f x) = g (\ x)"
+ shows "\ (gfp f) = gfp g"
+proof -
+ have "\ (gfp f) = (INF i. \ ((f^^i) top))"
+ unfolding inf_continuous_gfp[OF f] by (intro f \ inf_continuousD antimono_funpow inf_continuous_mono)
+ moreover have "\ ((f^^i) top) = (g^^i) top" for i
+ by (induction i; simp)
+ ultimately show ?thesis
+ unfolding inf_continuous_gfp[OF g] by simp
+qed
+
end