src/HOL/Library/Order_Continuity.thy
changeset 56020 f92479477c52
parent 54257 5c7a3b6b05a9
child 58881 b9556a055632
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Order_Continuity.thy	Mon Mar 10 20:04:40 2014 +0100
     1.3 @@ -0,0 +1,141 @@
     1.4 +(*  Title:      HOL/Library/Order_Continuity.thy
     1.5 +    Author:     David von Oheimb, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* Continuity and iterations (of set transformers) *}
     1.9 +
    1.10 +theory Order_Continuity
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +(* TODO: Generalize theory to chain-complete partial orders *)
    1.15 +
    1.16 +lemma SUP_nat_binary:
    1.17 +  "(SUP n::nat. if n = 0 then A else B) = (sup A B::'a::complete_lattice)"
    1.18 +  apply (auto intro!: antisym SUP_least)
    1.19 +  apply (rule SUP_upper2[where i=0])
    1.20 +  apply simp_all
    1.21 +  apply (rule SUP_upper2[where i=1])
    1.22 +  apply simp_all
    1.23 +  done
    1.24 +
    1.25 +lemma INF_nat_binary:
    1.26 +  "(INF n::nat. if n = 0 then A else B) = (inf A B::'a::complete_lattice)"
    1.27 +  apply (auto intro!: antisym INF_greatest)
    1.28 +  apply (rule INF_lower2[where i=0])
    1.29 +  apply simp_all
    1.30 +  apply (rule INF_lower2[where i=1])
    1.31 +  apply simp_all
    1.32 +  done
    1.33 +
    1.34 +subsection {* Continuity for complete lattices *}
    1.35 +
    1.36 +definition
    1.37 +  continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    1.38 +  "continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    1.39 +
    1.40 +lemma continuousD: "continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
    1.41 +  by (auto simp: continuous_def)
    1.42 +
    1.43 +lemma continuous_mono:
    1.44 +  fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    1.45 +  assumes [simp]: "continuous F" shows "mono F"
    1.46 +proof
    1.47 +  fix A B :: "'a" assume [simp]: "A \<le> B"
    1.48 +  have "F B = F (SUP n::nat. if n = 0 then A else B)"
    1.49 +    by (simp add: sup_absorb2 SUP_nat_binary)
    1.50 +  also have "\<dots> = (SUP n::nat. if n = 0 then F A else F B)"
    1.51 +    by (auto simp: continuousD mono_def intro!: SUP_cong)
    1.52 +  finally show "F A \<le> F B"
    1.53 +    by (simp add: SUP_nat_binary le_iff_sup)
    1.54 +qed
    1.55 +
    1.56 +lemma continuous_lfp:
    1.57 +  assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
    1.58 +proof (rule antisym)
    1.59 +  note mono = continuous_mono[OF `continuous F`]
    1.60 +  show "?U \<le> lfp F"
    1.61 +  proof (rule SUP_least)
    1.62 +    fix i show "(F ^^ i) bot \<le> lfp F"
    1.63 +    proof (induct i)
    1.64 +      case (Suc i)
    1.65 +      have "(F ^^ Suc i) bot = F ((F ^^ i) bot)" by simp
    1.66 +      also have "\<dots> \<le> F (lfp F)" by (rule monoD[OF mono Suc])
    1.67 +      also have "\<dots> = lfp F" by (simp add: lfp_unfold[OF mono, symmetric])
    1.68 +      finally show ?case .
    1.69 +    qed simp
    1.70 +  qed
    1.71 +  show "lfp F \<le> ?U"
    1.72 +  proof (rule lfp_lowerbound)
    1.73 +    have "mono (\<lambda>i::nat. (F ^^ i) bot)"
    1.74 +    proof -
    1.75 +      { fix i::nat have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
    1.76 +        proof (induct i)
    1.77 +          case 0 show ?case by simp
    1.78 +        next
    1.79 +          case Suc thus ?case using monoD[OF mono Suc] by auto
    1.80 +        qed }
    1.81 +      thus ?thesis by (auto simp add: mono_iff_le_Suc)
    1.82 +    qed
    1.83 +    hence "F ?U = (SUP i. (F ^^ Suc i) bot)" using `continuous F` by (simp add: continuous_def)
    1.84 +    also have "\<dots> \<le> ?U" by (fast intro: SUP_least SUP_upper)
    1.85 +    finally show "F ?U \<le> ?U" .
    1.86 +  qed
    1.87 +qed
    1.88 +
    1.89 +definition
    1.90 +  down_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    1.91 +  "down_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
    1.92 +
    1.93 +lemma down_continuousD: "down_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
    1.94 +  by (auto simp: down_continuous_def)
    1.95 +
    1.96 +lemma down_continuous_mono:
    1.97 +  fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    1.98 +  assumes [simp]: "down_continuous F" shows "mono F"
    1.99 +proof
   1.100 +  fix A B :: "'a" assume [simp]: "A \<le> B"
   1.101 +  have "F A = F (INF n::nat. if n = 0 then B else A)"
   1.102 +    by (simp add: inf_absorb2 INF_nat_binary)
   1.103 +  also have "\<dots> = (INF n::nat. if n = 0 then F B else F A)"
   1.104 +    by (auto simp: down_continuousD antimono_def intro!: INF_cong)
   1.105 +  finally show "F A \<le> F B"
   1.106 +    by (simp add: INF_nat_binary le_iff_inf inf_commute)
   1.107 +qed
   1.108 +
   1.109 +lemma down_continuous_gfp:
   1.110 +  assumes "down_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
   1.111 +proof (rule antisym)
   1.112 +  note mono = down_continuous_mono[OF `down_continuous F`]
   1.113 +  show "gfp F \<le> ?U"
   1.114 +  proof (rule INF_greatest)
   1.115 +    fix i show "gfp F \<le> (F ^^ i) top"
   1.116 +    proof (induct i)
   1.117 +      case (Suc i)
   1.118 +      have "gfp F = F (gfp F)" by (simp add: gfp_unfold[OF mono, symmetric])
   1.119 +      also have "\<dots> \<le> F ((F ^^ i) top)" by (rule monoD[OF mono Suc])
   1.120 +      also have "\<dots> = (F ^^ Suc i) top" by simp
   1.121 +      finally show ?case .
   1.122 +    qed simp
   1.123 +  qed
   1.124 +  show "?U \<le> gfp F"
   1.125 +  proof (rule gfp_upperbound)
   1.126 +    have *: "antimono (\<lambda>i::nat. (F ^^ i) top)"
   1.127 +    proof -
   1.128 +      { fix i::nat have "(F ^^ Suc i) top \<le> (F ^^ i) top"
   1.129 +        proof (induct i)
   1.130 +          case 0 show ?case by simp
   1.131 +        next
   1.132 +          case Suc thus ?case using monoD[OF mono Suc] by auto
   1.133 +        qed }
   1.134 +      thus ?thesis by (auto simp add: antimono_iff_le_Suc)
   1.135 +    qed
   1.136 +    have "?U \<le> (INF i. (F ^^ Suc i) top)"
   1.137 +      by (fast intro: INF_greatest INF_lower)
   1.138 +    also have "\<dots> \<le> F ?U"
   1.139 +      by (simp add: down_continuousD `down_continuous F` *)
   1.140 +    finally show "?U \<le> F ?U" .
   1.141 +  qed
   1.142 +qed
   1.143 +
   1.144 +end