add transfer theorems for fixed points
authorhoelzl
Thu Jun 11 18:24:44 2015 +0200 (2015-06-11)
changeset 60427b4b672f09270
parent 60426 eb3094c6576c
child 60428 5e9de4faef98
add transfer theorems for fixed points
src/HOL/Library/Order_Continuity.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Library/Order_Continuity.thy	Thu Jun 11 00:13:25 2015 +0100
     1.2 +++ b/src/HOL/Library/Order_Continuity.thy	Thu Jun 11 18:24:44 2015 +0200
     1.3 @@ -91,6 +91,19 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma lfp_transfer:
     1.8 +  assumes \<alpha>: "sup_continuous \<alpha>" and f: "sup_continuous f" and g: "sup_continuous g"
     1.9 +  assumes [simp]: "\<alpha> bot = bot" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
    1.10 +  shows "\<alpha> (lfp f) = lfp g"
    1.11 +proof -
    1.12 +  have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
    1.13 +    unfolding sup_continuous_lfp[OF f] by (intro f \<alpha> sup_continuousD mono_funpow sup_continuous_mono)
    1.14 +  moreover have "\<alpha> ((f^^i) bot) = (g^^i) bot" for i
    1.15 +    by (induction i; simp)
    1.16 +  ultimately show ?thesis
    1.17 +    unfolding sup_continuous_lfp[OF g] by simp
    1.18 +qed
    1.19 +
    1.20  definition
    1.21    inf_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    1.22    "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
    1.23 @@ -146,4 +159,17 @@
    1.24    qed
    1.25  qed
    1.26  
    1.27 +lemma gfp_transfer:
    1.28 +  assumes \<alpha>: "inf_continuous \<alpha>" and f: "inf_continuous f" and g: "inf_continuous g"
    1.29 +  assumes [simp]: "\<alpha> top = top" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
    1.30 +  shows "\<alpha> (gfp f) = gfp g"
    1.31 +proof -
    1.32 +  have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) top))"
    1.33 +    unfolding inf_continuous_gfp[OF f] by (intro f \<alpha> inf_continuousD antimono_funpow inf_continuous_mono)
    1.34 +  moreover have "\<alpha> ((f^^i) top) = (g^^i) top" for i
    1.35 +    by (induction i; simp)
    1.36 +  ultimately show ?thesis
    1.37 +    unfolding inf_continuous_gfp[OF g] by simp
    1.38 +qed
    1.39 +
    1.40  end
     2.1 --- a/src/HOL/Nat.thy	Thu Jun 11 00:13:25 2015 +0100
     2.2 +++ b/src/HOL/Nat.thy	Thu Jun 11 18:24:44 2015 +0200
     2.3 @@ -1881,12 +1881,12 @@
     2.4             intro: order_trans[OF _ funpow_mono])
     2.5  
     2.6  lemma mono_funpow:
     2.7 -  fixes Q :: "('i \<Rightarrow> 'a::{lattice, order_bot}) \<Rightarrow> ('i \<Rightarrow> 'a)"
     2.8 +  fixes Q :: "'a::{lattice, order_bot} \<Rightarrow> 'a"
     2.9    shows "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
    2.10    by (auto intro!: funpow_decreasing simp: mono_def)
    2.11  
    2.12  lemma antimono_funpow:
    2.13 -  fixes Q :: "('i \<Rightarrow> 'a::{lattice, order_top}) \<Rightarrow> ('i \<Rightarrow> 'a)"
    2.14 +  fixes Q :: "'a::{lattice, order_top} \<Rightarrow> 'a"
    2.15    shows "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)"
    2.16    by (auto intro!: funpow_increasing simp: antimono_def)
    2.17