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