src/HOL/Library/Continuity.thy
changeset 21312 1d39091a3208
parent 19736 d8d0f8f51d69
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/Library/Continuity.thy	Sat Nov 11 23:58:46 2006 +0100
     1.2 +++ b/src/HOL/Library/Continuity.thy	Sun Nov 12 19:22:10 2006 +0100
     1.3 @@ -9,6 +9,85 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 +subsection{*Continuity for complete lattices*}
     1.8 +
     1.9 +constdefs
    1.10 + chain :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool"
    1.11 +"chain M == !i. M i \<le> M(Suc i)"
    1.12 + continuous :: "('a::order \<Rightarrow> 'a::order) \<Rightarrow> bool"
    1.13 +"continuous F == !M. chain M \<longrightarrow> F(SUP i. M i) = (SUP i. F(M i))"
    1.14 +
    1.15 +abbreviation
    1.16 + bot :: "'a::order"
    1.17 +"bot == Sup {}"
    1.18 +
    1.19 +lemma SUP_nat_conv:
    1.20 + "(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))"
    1.21 +apply(rule order_antisym)
    1.22 + apply(rule SUP_leI)
    1.23 + apply(case_tac n)
    1.24 +  apply simp
    1.25 + apply (blast intro:le_SUPI le_joinI2)
    1.26 +apply(simp)
    1.27 +apply (blast intro:SUP_leI le_SUPI)
    1.28 +done
    1.29 +
    1.30 +lemma continuous_mono: fixes F :: "'a::comp_lat \<Rightarrow> 'a::comp_lat"
    1.31 +  assumes "continuous F" shows "mono F"
    1.32 +proof
    1.33 +  fix A B :: "'a" assume "A <= B"
    1.34 +  let ?C = "%i::nat. if i=0 then A else B"
    1.35 +  have "chain ?C" using `A <= B` by(simp add:chain_def)
    1.36 +  have "F B = join (F A) (F B)"
    1.37 +  proof -
    1.38 +    have "join A B = B" using `A <= B` by (simp add:join_absorp2)
    1.39 +    hence "F B = F(SUP i. ?C i)" by(simp add: SUP_nat_conv)
    1.40 +    also have "\<dots> = (SUP i. F(?C i))"
    1.41 +      using `chain ?C` `continuous F` by(simp add:continuous_def)
    1.42 +    also have "\<dots> = join (F A) (F B)" by(simp add: SUP_nat_conv)
    1.43 +    finally show ?thesis .
    1.44 +  qed
    1.45 +  thus "F A \<le> F B" by(subst le_def_join, simp)
    1.46 +qed
    1.47 +
    1.48 +lemma continuous_lfp:
    1.49 + assumes "continuous F" shows "lfp F = (SUP i. (F^i) bot)"
    1.50 +proof -
    1.51 +  note mono = continuous_mono[OF `continuous F`]
    1.52 +  { fix i have "(F^i) bot \<le> lfp F"
    1.53 +    proof (induct i)
    1.54 +      show "(F^0) bot \<le> lfp F" by simp
    1.55 +    next
    1.56 +      case (Suc i)
    1.57 +      have "(F^(Suc i)) bot = F((F^i) bot)" by simp
    1.58 +      also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc])
    1.59 +      also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
    1.60 +      finally show ?case .
    1.61 +    qed }
    1.62 +  hence "(SUP i. (F^i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
    1.63 +  moreover have "lfp F \<le> (SUP i. (F^i) bot)" (is "_ \<le> ?U")
    1.64 +  proof (rule lfp_lowerbound)
    1.65 +    have "chain(%i. (F^i) bot)"
    1.66 +    proof -
    1.67 +      { fix i have "(F^i) bot \<le> (F^(Suc i)) bot"
    1.68 +	proof (induct i)
    1.69 +	  case 0 show ?case by simp
    1.70 +	next
    1.71 +	  case Suc thus ?case using monoD[OF mono Suc] by auto
    1.72 +	qed }
    1.73 +      thus ?thesis by(auto simp add:chain_def)
    1.74 +    qed
    1.75 +    hence "F ?U = (SUP i. (F^(i+1)) bot)" using `continuous F` by (simp add:continuous_def)
    1.76 +    also have "\<dots> \<le> ?U" by(blast intro:SUP_leI le_SUPI)
    1.77 +    finally show "F ?U \<le> ?U" .
    1.78 +  qed
    1.79 +  ultimately show ?thesis by (blast intro:order_antisym)
    1.80 +qed
    1.81 +
    1.82 +text{* The following development is just for sets but presents an up
    1.83 +and a down version of chains and continuity and covers @{const gfp}. *}
    1.84 +
    1.85 +
    1.86  subsection "Chains"
    1.87  
    1.88  definition