# HG changeset patch
# User huffman
# Date 1242425543 25200
# Node ID f550c4cf3f3af09d731292bee589bba9e22b6e4b
# Parent  19c2f68ae23d957c8c26cadceb4f1e351d51b143
continuity proofs for approx function on deflations; lemma cast_below_imp_below

diff -r 19c2f68ae23d -r f550c4cf3f3a src/HOLCF/Algebraic.thy
--- a/src/HOLCF/Algebraic.thy	Tue May 12 12:16:33 2009 -0700
+++ b/src/HOLCF/Algebraic.thy	Fri May 15 15:12:23 2009 -0700
@@ -29,6 +29,11 @@
   thus "P i j" using step trans by (rule less_Suc_induct)
 qed
 
+definition
+  eventual_iterate :: "('a \<rightarrow> 'a::cpo) \<Rightarrow> ('a \<rightarrow> 'a)"
+where
+  "eventual_iterate f = eventual (\<lambda>n. iterate n\<cdot>f)"
+
 text {* A pre-deflation is like a deflation, but not idempotent. *}
 
 locale pre_deflation =
@@ -103,9 +108,10 @@
 abbreviation
   d :: "'a \<rightarrow> 'a"
 where
-  "d \<equiv> eventual (\<lambda>n. iterate n\<cdot>f)"
+  "d \<equiv> eventual_iterate f"
 
 lemma MOST_d: "MOST n. P (iterate n\<cdot>f) \<Longrightarrow> P d"
+unfolding eventual_iterate_def
 using eventually_constant_iterate by (rule MOST_eventual)
 
 lemma f_d: "f\<cdot>(d\<cdot>x) = d\<cdot>x"
@@ -134,6 +140,7 @@
 proof
   fix x :: 'a
   have "d \<in> range (\<lambda>n. iterate n\<cdot>f)"
+    unfolding eventual_iterate_def
     using eventually_constant_iterate
     by (rule eventual_mem_range)
   then obtain n where n: "d = iterate n\<cdot>f" ..
@@ -153,9 +160,17 @@
     by (simp add: d_fixed_iff)
 qed
 
+lemma deflation_d: "deflation d"
+using finite_deflation_d
+by (rule finite_deflation_imp_deflation)
+
 end
 
-lemma pre_deflation_d_f:
+lemma finite_deflation_eventual_iterate:
+  "pre_deflation d \<Longrightarrow> finite_deflation (eventual_iterate d)"
+by (rule pre_deflation.finite_deflation_d)
+
+lemma pre_deflation_oo:
   assumes "finite_deflation d"
   assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
   shows "pre_deflation (d oo f)"
@@ -171,13 +186,13 @@
 lemma eventual_iterate_oo_fixed_iff:
   assumes "finite_deflation d"
   assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
-  shows "eventual (\<lambda>n. iterate n\<cdot>(d oo f))\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x"
+  shows "eventual_iterate (d oo f)\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x"
 proof -
   interpret d: finite_deflation d by fact
   let ?e = "d oo f"
   interpret e: pre_deflation "d oo f"
     using `finite_deflation d` f
-    by (rule pre_deflation_d_f)
+    by (rule pre_deflation_oo)
   let ?g = "eventual (\<lambda>n. iterate n\<cdot>?e)"
   show ?thesis
     apply (subst e.d_fixed_iff)
@@ -192,6 +207,94 @@
     done
 qed
 
+lemma eventual_mono:
+  assumes A: "eventually_constant A"
+  assumes B: "eventually_constant B"
+  assumes below: "\<And>n. A n \<sqsubseteq> B n"
+  shows "eventual A \<sqsubseteq> eventual B"
+proof -
+  from A have "MOST n. A n = eventual A"
+    by (rule MOST_eq_eventual)
+  then have "MOST n. eventual A \<sqsubseteq> B n"
+    by (rule MOST_mono) (erule subst, rule below)
+  with B show "eventual A \<sqsubseteq> eventual B"
+    by (rule MOST_eventual)
+qed
+
+lemma eventual_iterate_mono:
+  assumes f: "pre_deflation f" and g: "pre_deflation g" and "f \<sqsubseteq> g"
+  shows "eventual_iterate f \<sqsubseteq> eventual_iterate g"
+unfolding eventual_iterate_def
+apply (rule eventual_mono)
+apply (rule pre_deflation.eventually_constant_iterate [OF f])
+apply (rule pre_deflation.eventually_constant_iterate [OF g])
+apply (rule monofun_cfun_arg [OF `f \<sqsubseteq> g`])
+done
+
+lemma cont2cont_eventual_iterate_oo:
+  assumes d: "finite_deflation d"
+  assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
+  shows "cont (\<lambda>x. eventual_iterate (d oo f x))"
+    (is "cont ?e")
+proof (rule contI2)
+  show "monofun ?e"
+    apply (rule monofunI)
+    apply (rule eventual_iterate_mono)
+    apply (rule pre_deflation_oo [OF d below])
+    apply (rule pre_deflation_oo [OF d below])
+    apply (rule monofun_cfun_arg)
+    apply (erule cont2monofunE [OF cont])
+    done
+next
+  fix Y :: "nat \<Rightarrow> 'b"
+  assume Y: "chain Y"
+  with cont have fY: "chain (\<lambda>i. f (Y i))"
+    by (rule ch2ch_cont)
+  assume eY: "chain (\<lambda>i. ?e (Y i))"
+  have lub_below: "\<And>x. f (\<Squnion>i. Y i)\<cdot>x \<sqsubseteq> x"
+    by (rule admD [OF _ Y], simp add: cont, rule below)
+  have "deflation (?e (\<Squnion>i. Y i))"
+    apply (rule pre_deflation.deflation_d)
+    apply (rule pre_deflation_oo [OF d lub_below])
+    done
+  then show "?e (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. ?e (Y i))"
+  proof (rule deflation.belowI)
+    fix x :: 'a
+    assume "?e (\<Squnion>i. Y i)\<cdot>x = x"
+    hence "d\<cdot>x = x" and "f (\<Squnion>i. Y i)\<cdot>x = x"
+      by (simp_all add: eventual_iterate_oo_fixed_iff [OF d lub_below])
+    hence "(\<Squnion>i. f (Y i)\<cdot>x) = x"
+      apply (simp only: cont2contlubE [OF cont Y])
+      apply (simp only: contlub_cfun_fun [OF fY])
+      done
+    have "compact (d\<cdot>x)"
+      using d by (rule finite_deflation.compact)
+    then have "compact x"
+      using `d\<cdot>x = x` by simp
+    then have "compact (\<Squnion>i. f (Y i)\<cdot>x)"
+      using `(\<Squnion>i. f (Y i)\<cdot>x) = x` by simp
+    then have "\<exists>n. max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)"
+      by - (rule compact_imp_max_in_chain, simp add: fY, assumption)
+    then obtain n where n: "max_in_chain n (\<lambda>i. f (Y i)\<cdot>x)" ..
+    then have "f (Y n)\<cdot>x = x"
+      using `(\<Squnion>i. f (Y i)\<cdot>x) = x` fY by (simp add: maxinch_is_thelub)
+    with `d\<cdot>x = x` have "?e (Y n)\<cdot>x = x"
+      by (simp add: eventual_iterate_oo_fixed_iff [OF d below])
+    moreover have "?e (Y n)\<cdot>x \<sqsubseteq> (\<Squnion>i. ?e (Y i)\<cdot>x)"
+      by (rule is_ub_thelub, simp add: eY)
+    ultimately have "x \<sqsubseteq> (\<Squnion>i. ?e (Y i))\<cdot>x"
+      by (simp add: contlub_cfun_fun eY)
+    also have "(\<Squnion>i. ?e (Y i))\<cdot>x \<sqsubseteq> x"
+      apply (rule deflation.below)
+      apply (rule admD [OF adm_deflation eY])
+      apply (rule pre_deflation.deflation_d)
+      apply (rule pre_deflation_oo [OF d below])
+      done
+    finally show "(\<Squnion>i. ?e (Y i))\<cdot>x = x" ..
+  qed
+qed
+
+
 subsection {* Type constructor for finite deflations *}
 
 defaultsort profinite
@@ -214,6 +317,10 @@
 lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
 using Rep_fin_defl by simp
 
+lemma deflation_Rep_fin_defl: "deflation (Rep_fin_defl d)"
+using finite_deflation_Rep_fin_defl
+by (rule finite_deflation_imp_deflation)
+
 interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
 by (rule finite_deflation_Rep_fin_defl)
 
@@ -244,27 +351,69 @@
 subsection {* Take function for finite deflations *}
 
 definition
+  defl_approx :: "nat \<Rightarrow> ('a \<rightarrow> 'a) \<Rightarrow> ('a \<rightarrow> 'a)"
+where
+  "defl_approx i d = eventual_iterate (approx i oo d)"
+
+lemma finite_deflation_defl_approx:
+  "deflation d \<Longrightarrow> finite_deflation (defl_approx i d)"
+unfolding defl_approx_def
+apply (rule pre_deflation.finite_deflation_d)
+apply (rule pre_deflation_oo)
+apply (rule finite_deflation_approx)
+apply (erule deflation.below)
+done
+
+lemma deflation_defl_approx:
+  "deflation d \<Longrightarrow> deflation (defl_approx i d)"
+apply (rule finite_deflation_imp_deflation)
+apply (erule finite_deflation_defl_approx)
+done
+
+lemma defl_approx_fixed_iff:
+  "deflation d \<Longrightarrow> defl_approx i d\<cdot>x = x \<longleftrightarrow> approx i\<cdot>x = x \<and> d\<cdot>x = x"
+unfolding defl_approx_def
+apply (rule eventual_iterate_oo_fixed_iff)
+apply (rule finite_deflation_approx)
+apply (erule deflation.below)
+done
+
+lemma defl_approx_below:
+  "\<lbrakk>a \<sqsubseteq> b; deflation a; deflation b\<rbrakk> \<Longrightarrow> defl_approx i a \<sqsubseteq> defl_approx i b"
+apply (rule deflation.belowI)
+apply (erule deflation_defl_approx)
+apply (simp add: defl_approx_fixed_iff)
+apply (erule (1) deflation.belowD)
+apply (erule conjunct2)
+done
+
+lemma cont2cont_defl_approx:
+  assumes cont: "cont f" and below: "\<And>x y. f x\<cdot>y \<sqsubseteq> y"
+  shows "cont (\<lambda>x. defl_approx i (f x))"
+unfolding defl_approx_def
+using finite_deflation_approx assms
+by (rule cont2cont_eventual_iterate_oo)
+
+definition
   fd_take :: "nat \<Rightarrow> 'a fin_defl \<Rightarrow> 'a fin_defl"
 where
-  "fd_take i d = Abs_fin_defl (eventual (\<lambda>n. iterate n\<cdot>(approx i oo Rep_fin_defl d)))"
+  "fd_take i d = Abs_fin_defl (defl_approx i (Rep_fin_defl d))"
 
 lemma Rep_fin_defl_fd_take:
-  "Rep_fin_defl (fd_take i d) =
-    eventual (\<lambda>n. iterate n\<cdot>(approx i oo Rep_fin_defl d))"
+  "Rep_fin_defl (fd_take i d) = defl_approx i (Rep_fin_defl d)"
 unfolding fd_take_def
 apply (rule Abs_fin_defl_inverse [unfolded mem_Collect_eq])
-apply (rule pre_deflation.finite_deflation_d)
-apply (rule pre_deflation_d_f)
-apply (rule finite_deflation_approx)
-apply (rule Rep_fin_defl.below)
+apply (rule finite_deflation_defl_approx)
+apply (rule deflation_Rep_fin_defl)
 done
 
 lemma fd_take_fixed_iff:
   "Rep_fin_defl (fd_take i d)\<cdot>x = x \<longleftrightarrow>
     approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
 unfolding Rep_fin_defl_fd_take
-by (rule eventual_iterate_oo_fixed_iff
-    [OF finite_deflation_approx Rep_fin_defl.below])
+apply (rule defl_approx_fixed_iff)
+apply (rule deflation_Rep_fin_defl)
+done
 
 lemma fd_take_below: "fd_take n d \<sqsubseteq> d"
 apply (rule fin_defl_belowI)
@@ -463,6 +612,41 @@
 interpretation cast: deflation "cast\<cdot>d"
 by (rule deflation_cast)
 
+lemma cast_approx: "cast\<cdot>(approx n\<cdot>A) = defl_approx n (cast\<cdot>A)"
+apply (rule alg_defl.principal_induct)
+apply (rule adm_eq)
+apply simp
+apply (simp add: cont2cont_defl_approx cast.below)
+apply (simp only: approx_alg_defl_principal)
+apply (simp only: cast_alg_defl_principal)
+apply (simp only: Rep_fin_defl_fd_take)
+done
+
+lemma cast_approx_fixed_iff:
+  "cast\<cdot>(approx i\<cdot>A)\<cdot>x = x \<longleftrightarrow> approx i\<cdot>x = x \<and> cast\<cdot>A\<cdot>x = x"
+apply (simp only: cast_approx)
+apply (rule defl_approx_fixed_iff)
+apply (rule deflation_cast)
+done
+
+lemma defl_approx_cast: "defl_approx i (cast\<cdot>A) = cast\<cdot>(approx i\<cdot>A)"
+by (rule cast_approx [symmetric])
+
+lemma cast_below_imp_below: "cast\<cdot>A \<sqsubseteq> cast\<cdot>B \<Longrightarrow> A \<sqsubseteq> B"
+apply (rule profinite_below_ext)
+apply (drule_tac i=i in defl_approx_below)
+apply (rule deflation_cast)
+apply (rule deflation_cast)
+apply (simp only: defl_approx_cast)
+apply (cut_tac x="approx i\<cdot>A" in alg_defl.compact_imp_principal)
+apply (rule compact_approx)
+apply (cut_tac x="approx i\<cdot>B" in alg_defl.compact_imp_principal)
+apply (rule compact_approx)
+apply clarsimp
+apply (simp add: cast_alg_defl_principal)
+apply (simp add: below_fin_defl_def)
+done
+
 lemma "cast\<cdot>(\<Squnion>i. alg_defl_principal (Abs_fin_defl (approx i)))\<cdot>x = x"
 apply (subst contlub_cfun_arg)
 apply (rule chainI)