src/HOL/Library/Order_Continuity.thy
changeset 60172 423273355b55
parent 58881 b9556a055632
child 60427 b4b672f09270
     1.1 --- a/src/HOL/Library/Order_Continuity.thy	Mon May 04 16:01:36 2015 +0200
     1.2 +++ b/src/HOL/Library/Order_Continuity.thy	Mon May 04 17:35:31 2015 +0200
     1.3 @@ -28,32 +28,38 @@
     1.4    apply simp_all
     1.5    done
     1.6  
     1.7 +text \<open>
     1.8 +  The name @{text continuous} is already taken in @{text "Complex_Main"}, so we use
     1.9 +  @{text "sup_continuous"} and @{text "inf_continuous"}. These names appear sometimes in literature
    1.10 +  and have the advantage that these names are duals.
    1.11 +\<close>
    1.12 +
    1.13  subsection {* Continuity for complete lattices *}
    1.14  
    1.15  definition
    1.16 -  continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    1.17 -  "continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    1.18 +  sup_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    1.19 +  "sup_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    1.20  
    1.21 -lemma continuousD: "continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
    1.22 -  by (auto simp: continuous_def)
    1.23 +lemma sup_continuousD: "sup_continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
    1.24 +  by (auto simp: sup_continuous_def)
    1.25  
    1.26 -lemma continuous_mono:
    1.27 +lemma sup_continuous_mono:
    1.28    fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    1.29 -  assumes [simp]: "continuous F" shows "mono F"
    1.30 +  assumes [simp]: "sup_continuous F" shows "mono F"
    1.31  proof
    1.32    fix A B :: "'a" assume [simp]: "A \<le> B"
    1.33    have "F B = F (SUP n::nat. if n = 0 then A else B)"
    1.34      by (simp add: sup_absorb2 SUP_nat_binary)
    1.35    also have "\<dots> = (SUP n::nat. if n = 0 then F A else F B)"
    1.36 -    by (auto simp: continuousD mono_def intro!: SUP_cong)
    1.37 +    by (auto simp: sup_continuousD mono_def intro!: SUP_cong)
    1.38    finally show "F A \<le> F B"
    1.39      by (simp add: SUP_nat_binary le_iff_sup)
    1.40  qed
    1.41  
    1.42 -lemma continuous_lfp:
    1.43 -  assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
    1.44 +lemma sup_continuous_lfp:
    1.45 +  assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
    1.46  proof (rule antisym)
    1.47 -  note mono = continuous_mono[OF `continuous F`]
    1.48 +  note mono = sup_continuous_mono[OF `sup_continuous F`]
    1.49    show "?U \<le> lfp F"
    1.50    proof (rule SUP_least)
    1.51      fix i show "(F ^^ i) bot \<le> lfp F"
    1.52 @@ -77,36 +83,38 @@
    1.53          qed }
    1.54        thus ?thesis by (auto simp add: mono_iff_le_Suc)
    1.55      qed
    1.56 -    hence "F ?U = (SUP i. (F ^^ Suc i) bot)" using `continuous F` by (simp add: continuous_def)
    1.57 -    also have "\<dots> \<le> ?U" by (fast intro: SUP_least SUP_upper)
    1.58 +    hence "F ?U = (SUP i. (F ^^ Suc i) bot)"
    1.59 +      using `sup_continuous F` by (simp add: sup_continuous_def)
    1.60 +    also have "\<dots> \<le> ?U"
    1.61 +      by (fast intro: SUP_least SUP_upper)
    1.62      finally show "F ?U \<le> ?U" .
    1.63    qed
    1.64  qed
    1.65  
    1.66  definition
    1.67 -  down_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    1.68 -  "down_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
    1.69 +  inf_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    1.70 +  "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
    1.71  
    1.72 -lemma down_continuousD: "down_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
    1.73 -  by (auto simp: down_continuous_def)
    1.74 +lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
    1.75 +  by (auto simp: inf_continuous_def)
    1.76  
    1.77 -lemma down_continuous_mono:
    1.78 +lemma inf_continuous_mono:
    1.79    fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    1.80 -  assumes [simp]: "down_continuous F" shows "mono F"
    1.81 +  assumes [simp]: "inf_continuous F" shows "mono F"
    1.82  proof
    1.83    fix A B :: "'a" assume [simp]: "A \<le> B"
    1.84    have "F A = F (INF n::nat. if n = 0 then B else A)"
    1.85      by (simp add: inf_absorb2 INF_nat_binary)
    1.86    also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)"
    1.87 -    by (auto simp: down_continuousD antimono_def intro!: INF_cong)
    1.88 +    by (auto simp: inf_continuousD antimono_def intro!: INF_cong)
    1.89    finally show "F A \<le> F B"
    1.90      by (simp add: INF_nat_binary le_iff_inf inf_commute)
    1.91  qed
    1.92  
    1.93 -lemma down_continuous_gfp:
    1.94 -  assumes "down_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
    1.95 +lemma inf_continuous_gfp:
    1.96 +  assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
    1.97  proof (rule antisym)
    1.98 -  note mono = down_continuous_mono[OF `down_continuous F`]
    1.99 +  note mono = inf_continuous_mono[OF `inf_continuous F`]
   1.100    show "gfp F \<le> ?U"
   1.101    proof (rule INF_greatest)
   1.102      fix i show "gfp F \<le> (F ^^ i) top"
   1.103 @@ -133,7 +141,7 @@
   1.104      have "?U \<le> (INF i. (F ^^ Suc i) top)"
   1.105        by (fast intro: INF_greatest INF_lower)
   1.106      also have "\<dots> \<le> F ?U"
   1.107 -      by (simp add: down_continuousD `down_continuous F` *)
   1.108 +      by (simp add: inf_continuousD `inf_continuous F` *)
   1.109      finally show "?U \<le> F ?U" .
   1.110    qed
   1.111  qed