src/HOL/Library/Continuity.thy
author nipkow
Sun Nov 12 19:22:10 2006 +0100 (2006-11-12)
changeset 21312 1d39091a3208
parent 19736 d8d0f8f51d69
child 21404 eb85850d3eb7
permissions -rw-r--r--
started reorgnization of lattice theories
     1 (*  Title:      HOL/Library/Continuity.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb, TU Muenchen
     4 *)
     5 
     6 header {* Continuity and iterations (of set transformers) *}
     7 
     8 theory Continuity
     9 imports Main
    10 begin
    11 
    12 subsection{*Continuity for complete lattices*}
    13 
    14 constdefs
    15  chain :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool"
    16 "chain M == !i. M i \<le> M(Suc i)"
    17  continuous :: "('a::order \<Rightarrow> 'a::order) \<Rightarrow> bool"
    18 "continuous F == !M. chain M \<longrightarrow> F(SUP i. M i) = (SUP i. F(M i))"
    19 
    20 abbreviation
    21  bot :: "'a::order"
    22 "bot == Sup {}"
    23 
    24 lemma SUP_nat_conv:
    25  "(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))"
    26 apply(rule order_antisym)
    27  apply(rule SUP_leI)
    28  apply(case_tac n)
    29   apply simp
    30  apply (blast intro:le_SUPI le_joinI2)
    31 apply(simp)
    32 apply (blast intro:SUP_leI le_SUPI)
    33 done
    34 
    35 lemma continuous_mono: fixes F :: "'a::comp_lat \<Rightarrow> 'a::comp_lat"
    36   assumes "continuous F" shows "mono F"
    37 proof
    38   fix A B :: "'a" assume "A <= B"
    39   let ?C = "%i::nat. if i=0 then A else B"
    40   have "chain ?C" using `A <= B` by(simp add:chain_def)
    41   have "F B = join (F A) (F B)"
    42   proof -
    43     have "join A B = B" using `A <= B` by (simp add:join_absorp2)
    44     hence "F B = F(SUP i. ?C i)" by(simp add: SUP_nat_conv)
    45     also have "\<dots> = (SUP i. F(?C i))"
    46       using `chain ?C` `continuous F` by(simp add:continuous_def)
    47     also have "\<dots> = join (F A) (F B)" by(simp add: SUP_nat_conv)
    48     finally show ?thesis .
    49   qed
    50   thus "F A \<le> F B" by(subst le_def_join, simp)
    51 qed
    52 
    53 lemma continuous_lfp:
    54  assumes "continuous F" shows "lfp F = (SUP i. (F^i) bot)"
    55 proof -
    56   note mono = continuous_mono[OF `continuous F`]
    57   { fix i have "(F^i) bot \<le> lfp F"
    58     proof (induct i)
    59       show "(F^0) bot \<le> lfp F" by simp
    60     next
    61       case (Suc i)
    62       have "(F^(Suc i)) bot = F((F^i) bot)" by simp
    63       also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc])
    64       also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
    65       finally show ?case .
    66     qed }
    67   hence "(SUP i. (F^i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
    68   moreover have "lfp F \<le> (SUP i. (F^i) bot)" (is "_ \<le> ?U")
    69   proof (rule lfp_lowerbound)
    70     have "chain(%i. (F^i) bot)"
    71     proof -
    72       { fix i have "(F^i) bot \<le> (F^(Suc i)) bot"
    73 	proof (induct i)
    74 	  case 0 show ?case by simp
    75 	next
    76 	  case Suc thus ?case using monoD[OF mono Suc] by auto
    77 	qed }
    78       thus ?thesis by(auto simp add:chain_def)
    79     qed
    80     hence "F ?U = (SUP i. (F^(i+1)) bot)" using `continuous F` by (simp add:continuous_def)
    81     also have "\<dots> \<le> ?U" by(blast intro:SUP_leI le_SUPI)
    82     finally show "F ?U \<le> ?U" .
    83   qed
    84   ultimately show ?thesis by (blast intro:order_antisym)
    85 qed
    86 
    87 text{* The following development is just for sets but presents an up
    88 and a down version of chains and continuity and covers @{const gfp}. *}
    89 
    90 
    91 subsection "Chains"
    92 
    93 definition
    94   up_chain :: "(nat => 'a set) => bool"
    95   "up_chain F = (\<forall>i. F i \<subseteq> F (Suc i))"
    96 
    97 lemma up_chainI: "(!!i. F i \<subseteq> F (Suc i)) ==> up_chain F"
    98   by (simp add: up_chain_def)
    99 
   100 lemma up_chainD: "up_chain F ==> F i \<subseteq> F (Suc i)"
   101   by (simp add: up_chain_def)
   102 
   103 lemma up_chain_less_mono:
   104     "up_chain F ==> x < y ==> F x \<subseteq> F y"
   105   apply (induct y)
   106    apply (blast dest: up_chainD elim: less_SucE)+
   107   done
   108 
   109 lemma up_chain_mono: "up_chain F ==> x \<le> y ==> F x \<subseteq> F y"
   110   apply (drule le_imp_less_or_eq)
   111   apply (blast dest: up_chain_less_mono)
   112   done
   113 
   114 
   115 definition
   116   down_chain :: "(nat => 'a set) => bool"
   117   "down_chain F = (\<forall>i. F (Suc i) \<subseteq> F i)"
   118 
   119 lemma down_chainI: "(!!i. F (Suc i) \<subseteq> F i) ==> down_chain F"
   120   by (simp add: down_chain_def)
   121 
   122 lemma down_chainD: "down_chain F ==> F (Suc i) \<subseteq> F i"
   123   by (simp add: down_chain_def)
   124 
   125 lemma down_chain_less_mono:
   126     "down_chain F ==> x < y ==> F y \<subseteq> F x"
   127   apply (induct y)
   128    apply (blast dest: down_chainD elim: less_SucE)+
   129   done
   130 
   131 lemma down_chain_mono: "down_chain F ==> x \<le> y ==> F y \<subseteq> F x"
   132   apply (drule le_imp_less_or_eq)
   133   apply (blast dest: down_chain_less_mono)
   134   done
   135 
   136 
   137 subsection "Continuity"
   138 
   139 definition
   140   up_cont :: "('a set => 'a set) => bool"
   141   "up_cont f = (\<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F))"
   142 
   143 lemma up_contI:
   144     "(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f"
   145   apply (unfold up_cont_def)
   146   apply blast
   147   done
   148 
   149 lemma up_contD:
   150     "up_cont f ==> up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)"
   151   apply (unfold up_cont_def)
   152   apply auto
   153   done
   154 
   155 
   156 lemma up_cont_mono: "up_cont f ==> mono f"
   157   apply (rule monoI)
   158   apply (drule_tac F = "\<lambda>i. if i = 0 then A else B" in up_contD)
   159    apply (rule up_chainI)
   160    apply  simp+
   161   apply (drule Un_absorb1)
   162   apply (auto simp add: nat_not_singleton)
   163   done
   164 
   165 
   166 definition
   167   down_cont :: "('a set => 'a set) => bool"
   168   "down_cont f =
   169     (\<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F))"
   170 
   171 lemma down_contI:
   172   "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f ` range F)) ==>
   173     down_cont f"
   174   apply (unfold down_cont_def)
   175   apply blast
   176   done
   177 
   178 lemma down_contD: "down_cont f ==> down_chain F ==>
   179     f (Inter (range F)) = Inter (f ` range F)"
   180   apply (unfold down_cont_def)
   181   apply auto
   182   done
   183 
   184 lemma down_cont_mono: "down_cont f ==> mono f"
   185   apply (rule monoI)
   186   apply (drule_tac F = "\<lambda>i. if i = 0 then B else A" in down_contD)
   187    apply (rule down_chainI)
   188    apply simp+
   189   apply (drule Int_absorb1)
   190   apply (auto simp add: nat_not_singleton)
   191   done
   192 
   193 
   194 subsection "Iteration"
   195 
   196 definition
   197   up_iterate :: "('a set => 'a set) => nat => 'a set"
   198   "up_iterate f n = (f^n) {}"
   199 
   200 lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
   201   by (simp add: up_iterate_def)
   202 
   203 lemma up_iterate_Suc [simp]: "up_iterate f (Suc i) = f (up_iterate f i)"
   204   by (simp add: up_iterate_def)
   205 
   206 lemma up_iterate_chain: "mono F ==> up_chain (up_iterate F)"
   207   apply (rule up_chainI)
   208   apply (induct_tac i)
   209    apply simp+
   210   apply (erule (1) monoD)
   211   done
   212 
   213 lemma UNION_up_iterate_is_fp:
   214   "up_cont F ==>
   215     F (UNION UNIV (up_iterate F)) = UNION UNIV (up_iterate F)"
   216   apply (frule up_cont_mono [THEN up_iterate_chain])
   217   apply (drule (1) up_contD)
   218   apply simp
   219   apply (auto simp del: up_iterate_Suc simp add: up_iterate_Suc [symmetric])
   220   apply (case_tac xa)
   221    apply auto
   222   done
   223 
   224 lemma UNION_up_iterate_lowerbound:
   225     "mono F ==> F P = P ==> UNION UNIV (up_iterate F) \<subseteq> P"
   226   apply (subgoal_tac "(!!i. up_iterate F i \<subseteq> P)")
   227    apply fast
   228   apply (induct_tac i)
   229   prefer 2 apply (drule (1) monoD)
   230    apply auto
   231   done
   232 
   233 lemma UNION_up_iterate_is_lfp:
   234     "up_cont F ==> lfp F = UNION UNIV (up_iterate F)"
   235   apply (rule set_eq_subset [THEN iffD2])
   236   apply (rule conjI)
   237    prefer 2
   238    apply (drule up_cont_mono)
   239    apply (rule UNION_up_iterate_lowerbound)
   240     apply assumption
   241    apply (erule lfp_unfold [symmetric])
   242   apply (rule lfp_lowerbound)
   243   apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
   244   apply (erule UNION_up_iterate_is_fp [symmetric])
   245   done
   246 
   247 
   248 definition
   249   down_iterate :: "('a set => 'a set) => nat => 'a set"
   250   "down_iterate f n = (f^n) UNIV"
   251 
   252 lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
   253   by (simp add: down_iterate_def)
   254 
   255 lemma down_iterate_Suc [simp]:
   256     "down_iterate f (Suc i) = f (down_iterate f i)"
   257   by (simp add: down_iterate_def)
   258 
   259 lemma down_iterate_chain: "mono F ==> down_chain (down_iterate F)"
   260   apply (rule down_chainI)
   261   apply (induct_tac i)
   262    apply simp+
   263   apply (erule (1) monoD)
   264   done
   265 
   266 lemma INTER_down_iterate_is_fp:
   267   "down_cont F ==>
   268     F (INTER UNIV (down_iterate F)) = INTER UNIV (down_iterate F)"
   269   apply (frule down_cont_mono [THEN down_iterate_chain])
   270   apply (drule (1) down_contD)
   271   apply simp
   272   apply (auto simp del: down_iterate_Suc simp add: down_iterate_Suc [symmetric])
   273   apply (case_tac xa)
   274    apply auto
   275   done
   276 
   277 lemma INTER_down_iterate_upperbound:
   278     "mono F ==> F P = P ==> P \<subseteq> INTER UNIV (down_iterate F)"
   279   apply (subgoal_tac "(!!i. P \<subseteq> down_iterate F i)")
   280    apply fast
   281   apply (induct_tac i)
   282   prefer 2 apply (drule (1) monoD)
   283    apply auto
   284   done
   285 
   286 lemma INTER_down_iterate_is_gfp:
   287     "down_cont F ==> gfp F = INTER UNIV (down_iterate F)"
   288   apply (rule set_eq_subset [THEN iffD2])
   289   apply (rule conjI)
   290    apply (drule down_cont_mono)
   291    apply (rule INTER_down_iterate_upperbound)
   292     apply assumption
   293    apply (erule gfp_unfold [symmetric])
   294   apply (rule gfp_upperbound)
   295   apply (rule set_eq_subset [THEN iffD1, THEN conjunct2])
   296   apply (erule INTER_down_iterate_is_fp)
   297   done
   298 
   299 end