src/HOL/Library/Order_Continuity.thy
changeset 60427 b4b672f09270
parent 60172 423273355b55
child 60500 903bb1495239
equal deleted inserted replaced
60426:eb3094c6576c 60427:b4b672f09270
    89       by (fast intro: SUP_least SUP_upper)
    89       by (fast intro: SUP_least SUP_upper)
    90     finally show "F ?U \<le> ?U" .
    90     finally show "F ?U \<le> ?U" .
    91   qed
    91   qed
    92 qed
    92 qed
    93 
    93 
       
    94 lemma lfp_transfer:
       
    95   assumes \<alpha>: "sup_continuous \<alpha>" and f: "sup_continuous f" and g: "sup_continuous g"
       
    96   assumes [simp]: "\<alpha> bot = bot" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
       
    97   shows "\<alpha> (lfp f) = lfp g"
       
    98 proof -
       
    99   have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
       
   100     unfolding sup_continuous_lfp[OF f] by (intro f \<alpha> sup_continuousD mono_funpow sup_continuous_mono)
       
   101   moreover have "\<alpha> ((f^^i) bot) = (g^^i) bot" for i
       
   102     by (induction i; simp)
       
   103   ultimately show ?thesis
       
   104     unfolding sup_continuous_lfp[OF g] by simp
       
   105 qed
       
   106 
    94 definition
   107 definition
    95   inf_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
   108   inf_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    96   "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
   109   "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
    97 
   110 
    98 lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
   111 lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
   144       by (simp add: inf_continuousD `inf_continuous F` *)
   157       by (simp add: inf_continuousD `inf_continuous F` *)
   145     finally show "?U \<le> F ?U" .
   158     finally show "?U \<le> F ?U" .
   146   qed
   159   qed
   147 qed
   160 qed
   148 
   161 
       
   162 lemma gfp_transfer:
       
   163   assumes \<alpha>: "inf_continuous \<alpha>" and f: "inf_continuous f" and g: "inf_continuous g"
       
   164   assumes [simp]: "\<alpha> top = top" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
       
   165   shows "\<alpha> (gfp f) = gfp g"
       
   166 proof -
       
   167   have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) top))"
       
   168     unfolding inf_continuous_gfp[OF f] by (intro f \<alpha> inf_continuousD antimono_funpow inf_continuous_mono)
       
   169   moreover have "\<alpha> ((f^^i) top) = (g^^i) top" for i
       
   170     by (induction i; simp)
       
   171   ultimately show ?thesis
       
   172     unfolding inf_continuous_gfp[OF g] by simp
       
   173 qed
       
   174 
   149 end
   175 end