src/HOL/Library/Order_Continuity.thy
 changeset 60427 b4b672f09270 parent 60172 423273355b55 child 60500 903bb1495239
equal 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`