src/HOL/Library/Order_Continuity.thy
changeset 60427 b4b672f09270
parent 60172 423273355b55
child 60500 903bb1495239
--- 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 \<alpha>: "sup_continuous \<alpha>" and f: "sup_continuous f" and g: "sup_continuous g"
+  assumes [simp]: "\<alpha> bot = bot" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
+  shows "\<alpha> (lfp f) = lfp g"
+proof -
+  have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
+    unfolding sup_continuous_lfp[OF f] by (intro f \<alpha> sup_continuousD mono_funpow sup_continuous_mono)
+  moreover have "\<alpha> ((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 \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
   "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
@@ -146,4 +159,17 @@
   qed
 qed
 
+lemma gfp_transfer:
+  assumes \<alpha>: "inf_continuous \<alpha>" and f: "inf_continuous f" and g: "inf_continuous g"
+  assumes [simp]: "\<alpha> top = top" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
+  shows "\<alpha> (gfp f) = gfp g"
+proof -
+  have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) top))"
+    unfolding inf_continuous_gfp[OF f] by (intro f \<alpha> inf_continuousD antimono_funpow inf_continuous_mono)
+  moreover have "\<alpha> ((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