# HG changeset patch
# User hoelzl
# Date 1434039884 -7200
# Node ID b4b672f09270cb293e901b314dd5e6a61b6eb453
# Parent  eb3094c6576c756f1c6f1cac6e3da0a76159e70d
add transfer theorems for fixed points

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 \<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
diff -r eb3094c6576c -r b4b672f09270 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Jun 11 00:13:25 2015 +0100
+++ b/src/HOL/Nat.thy	Thu Jun 11 18:24:44 2015 +0200
@@ -1881,12 +1881,12 @@
            intro: order_trans[OF _ funpow_mono])
 
 lemma mono_funpow:
-  fixes Q :: "('i \<Rightarrow> 'a::{lattice, order_bot}) \<Rightarrow> ('i \<Rightarrow> 'a)"
+  fixes Q :: "'a::{lattice, order_bot} \<Rightarrow> 'a"
   shows "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
   by (auto intro!: funpow_decreasing simp: mono_def)
 
 lemma antimono_funpow:
-  fixes Q :: "('i \<Rightarrow> 'a::{lattice, order_top}) \<Rightarrow> ('i \<Rightarrow> 'a)"
+  fixes Q :: "'a::{lattice, order_top} \<Rightarrow> 'a"
   shows "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)"
   by (auto intro!: funpow_increasing simp: antimono_def)