oheimb@11351: (* Title: HOL/Library/Continuity.thy wenzelm@11355: Author: David von Oheimb, TU Muenchen oheimb@11351: *) oheimb@11351: wenzelm@14706: header {* Continuity and iterations (of set transformers) *} oheimb@11351: nipkow@15131: theory Continuity wenzelm@46508: imports Main nipkow@15131: begin oheimb@11351: wenzelm@22367: subsection {* Continuity for complete lattices *} nipkow@21312: wenzelm@22367: definition haftmann@22452: chain :: "(nat \ 'a::complete_lattice) \ bool" where wenzelm@22367: "chain M \ (\i. M i \ M (Suc i))" wenzelm@22367: wenzelm@22367: definition haftmann@22452: continuous :: "('a::complete_lattice \ 'a::complete_lattice) \ bool" where wenzelm@22367: "continuous F \ (\M. chain M \ F (SUP i. M i) = (SUP i. F (M i)))" nipkow@21312: nipkow@21312: lemma SUP_nat_conv: berghofe@22431: "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))" nipkow@21312: apply(rule order_antisym) hoelzl@44928: apply(rule SUP_least) nipkow@21312: apply(case_tac n) nipkow@21312: apply simp hoelzl@44928: apply (fast intro:SUP_upper le_supI2) nipkow@21312: apply(simp) hoelzl@44928: apply (blast intro:SUP_least SUP_upper) nipkow@21312: done nipkow@21312: haftmann@22452: lemma continuous_mono: fixes F :: "'a::complete_lattice \ 'a::complete_lattice" nipkow@21312: assumes "continuous F" shows "mono F" nipkow@21312: proof nipkow@21312: fix A B :: "'a" assume "A <= B" nipkow@21312: let ?C = "%i::nat. if i=0 then A else B" nipkow@21312: have "chain ?C" using `A <= B` by(simp add:chain_def) haftmann@22422: have "F B = sup (F A) (F B)" nipkow@21312: proof - haftmann@22422: have "sup A B = B" using `A <= B` by (simp add:sup_absorb2) berghofe@22431: hence "F B = F(SUP i. ?C i)" by (subst SUP_nat_conv) simp nipkow@21312: also have "\ = (SUP i. F(?C i))" nipkow@21312: using `chain ?C` `continuous F` by(simp add:continuous_def) berghofe@22431: also have "\ = sup (F A) (F B)" by (subst SUP_nat_conv) simp nipkow@21312: finally show ?thesis . nipkow@21312: qed haftmann@22422: thus "F A \ F B" by(subst le_iff_sup, simp) nipkow@21312: qed nipkow@21312: nipkow@21312: lemma continuous_lfp: haftmann@30971: assumes "continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" nipkow@21312: proof - nipkow@21312: note mono = continuous_mono[OF `continuous F`] haftmann@30971: { fix i have "(F ^^ i) bot \ lfp F" nipkow@21312: proof (induct i) haftmann@30971: show "(F ^^ 0) bot \ lfp F" by simp nipkow@21312: next nipkow@21312: case (Suc i) haftmann@30971: have "(F ^^ Suc i) bot = F((F ^^ i) bot)" by simp nipkow@21312: also have "\ \ F(lfp F)" by(rule monoD[OF mono Suc]) nipkow@21312: also have "\ = lfp F" by(simp add:lfp_unfold[OF mono, symmetric]) nipkow@21312: finally show ?case . nipkow@21312: qed } hoelzl@44928: hence "(SUP i. (F ^^ i) bot) \ lfp F" by (blast intro!:SUP_least) haftmann@30971: moreover have "lfp F \ (SUP i. (F ^^ i) bot)" (is "_ \ ?U") nipkow@21312: proof (rule lfp_lowerbound) haftmann@30971: have "chain(%i. (F ^^ i) bot)" nipkow@21312: proof - haftmann@30971: { fix i have "(F ^^ i) bot \ (F ^^ (Suc i)) bot" wenzelm@32960: proof (induct i) wenzelm@32960: case 0 show ?case by simp wenzelm@32960: next wenzelm@32960: case Suc thus ?case using monoD[OF mono Suc] by auto wenzelm@32960: qed } nipkow@21312: thus ?thesis by(auto simp add:chain_def) nipkow@21312: qed haftmann@30971: hence "F ?U = (SUP i. (F ^^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def) hoelzl@44928: also have "\ \ ?U" by(fast intro:SUP_least SUP_upper) nipkow@21312: finally show "F ?U \ ?U" . nipkow@21312: qed nipkow@21312: ultimately show ?thesis by (blast intro:order_antisym) nipkow@21312: qed nipkow@21312: nipkow@21312: text{* The following development is just for sets but presents an up nipkow@21312: and a down version of chains and continuity and covers @{const gfp}. *} nipkow@21312: nipkow@21312: oheimb@11351: subsection "Chains" oheimb@11351: wenzelm@19736: definition wenzelm@21404: up_chain :: "(nat => 'a set) => bool" where wenzelm@19736: "up_chain F = (\i. F i \ F (Suc i))" oheimb@11351: wenzelm@11355: lemma up_chainI: "(!!i. F i \ F (Suc i)) ==> up_chain F" wenzelm@11355: by (simp add: up_chain_def) oheimb@11351: wenzelm@11355: lemma up_chainD: "up_chain F ==> F i \ F (Suc i)" wenzelm@11355: by (simp add: up_chain_def) oheimb@11351: wenzelm@19736: lemma up_chain_less_mono: wenzelm@19736: "up_chain F ==> x < y ==> F x \ F y" wenzelm@19736: apply (induct y) wenzelm@19736: apply (blast dest: up_chainD elim: less_SucE)+ wenzelm@11355: done oheimb@11351: wenzelm@11355: lemma up_chain_mono: "up_chain F ==> x \ y ==> F x \ F y" wenzelm@11355: apply (drule le_imp_less_or_eq) wenzelm@11355: apply (blast dest: up_chain_less_mono) wenzelm@11355: done oheimb@11351: oheimb@11351: wenzelm@19736: definition wenzelm@21404: down_chain :: "(nat => 'a set) => bool" where wenzelm@19736: "down_chain F = (\i. F (Suc i) \ F i)" oheimb@11351: wenzelm@11355: lemma down_chainI: "(!!i. F (Suc i) \ F i) ==> down_chain F" wenzelm@11355: by (simp add: down_chain_def) oheimb@11351: wenzelm@11355: lemma down_chainD: "down_chain F ==> F (Suc i) \ F i" wenzelm@11355: by (simp add: down_chain_def) oheimb@11351: wenzelm@19736: lemma down_chain_less_mono: wenzelm@19736: "down_chain F ==> x < y ==> F y \ F x" wenzelm@19736: apply (induct y) wenzelm@19736: apply (blast dest: down_chainD elim: less_SucE)+ wenzelm@11355: done oheimb@11351: wenzelm@11355: lemma down_chain_mono: "down_chain F ==> x \ y ==> F y \ F x" wenzelm@11355: apply (drule le_imp_less_or_eq) wenzelm@11355: apply (blast dest: down_chain_less_mono) wenzelm@11355: done oheimb@11351: oheimb@11351: oheimb@11351: subsection "Continuity" oheimb@11351: wenzelm@19736: definition wenzelm@21404: up_cont :: "('a set => 'a set) => bool" where wenzelm@19736: "up_cont f = (\F. up_chain F --> f (\(range F)) = \(f ` range F))" oheimb@11351: wenzelm@11355: lemma up_contI: nipkow@24331: "(!!F. up_chain F ==> f (\(range F)) = \(f ` range F)) ==> up_cont f" nipkow@24331: apply (unfold up_cont_def) nipkow@24331: apply blast nipkow@24331: done oheimb@11351: wenzelm@11355: lemma up_contD: nipkow@24331: "up_cont f ==> up_chain F ==> f (\(range F)) = \(f ` range F)" nipkow@24331: apply (unfold up_cont_def) nipkow@24331: apply auto nipkow@24331: done oheimb@11351: oheimb@11351: oheimb@11351: lemma up_cont_mono: "up_cont f ==> mono f" nipkow@24331: apply (rule monoI) haftmann@25076: apply (drule_tac F = "\i. if i = 0 then x else y" in up_contD) nipkow@24331: apply (rule up_chainI) nipkow@24331: apply simp nipkow@24331: apply (drule Un_absorb1) nipkow@32456: apply (auto split:split_if_asm) nipkow@24331: done oheimb@11351: oheimb@11351: wenzelm@19736: definition wenzelm@21404: down_cont :: "('a set => 'a set) => bool" where wenzelm@19736: "down_cont f = wenzelm@19736: (\F. down_chain F --> f (Inter (range F)) = Inter (f ` range F))" oheimb@11351: wenzelm@11355: lemma down_contI: wenzelm@11355: "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f ` range F)) ==> wenzelm@11355: down_cont f" wenzelm@11355: apply (unfold down_cont_def) wenzelm@11355: apply blast wenzelm@11355: done oheimb@11351: wenzelm@11355: lemma down_contD: "down_cont f ==> down_chain F ==> wenzelm@11355: f (Inter (range F)) = Inter (f ` range F)" wenzelm@11355: apply (unfold down_cont_def) wenzelm@11355: apply auto wenzelm@11355: done oheimb@11351: oheimb@11351: lemma down_cont_mono: "down_cont f ==> mono f" nipkow@24331: apply (rule monoI) haftmann@25076: apply (drule_tac F = "\i. if i = 0 then y else x" in down_contD) nipkow@24331: apply (rule down_chainI) nipkow@24331: apply simp nipkow@24331: apply (drule Int_absorb1) nipkow@32456: apply (auto split:split_if_asm) nipkow@24331: done oheimb@11351: oheimb@11351: oheimb@11351: subsection "Iteration" oheimb@11351: wenzelm@19736: definition wenzelm@21404: up_iterate :: "('a set => 'a set) => nat => 'a set" where haftmann@30971: "up_iterate f n = (f ^^ n) {}" oheimb@11351: oheimb@11351: lemma up_iterate_0 [simp]: "up_iterate f 0 = {}" wenzelm@11355: by (simp add: up_iterate_def) oheimb@11351: wenzelm@11355: lemma up_iterate_Suc [simp]: "up_iterate f (Suc i) = f (up_iterate f i)" wenzelm@11355: by (simp add: up_iterate_def) oheimb@11351: oheimb@11351: lemma up_iterate_chain: "mono F ==> up_chain (up_iterate F)" wenzelm@11355: apply (rule up_chainI) wenzelm@11355: apply (induct_tac i) wenzelm@11355: apply simp+ wenzelm@11355: apply (erule (1) monoD) wenzelm@11355: done oheimb@11351: wenzelm@11355: lemma UNION_up_iterate_is_fp: wenzelm@11355: "up_cont F ==> wenzelm@11355: F (UNION UNIV (up_iterate F)) = UNION UNIV (up_iterate F)" wenzelm@11355: apply (frule up_cont_mono [THEN up_iterate_chain]) wenzelm@11355: apply (drule (1) up_contD) wenzelm@11355: apply simp wenzelm@11355: apply (auto simp del: up_iterate_Suc simp add: up_iterate_Suc [symmetric]) wenzelm@11355: apply (case_tac xa) wenzelm@11355: apply auto wenzelm@11355: done oheimb@11351: wenzelm@11355: lemma UNION_up_iterate_lowerbound: wenzelm@11355: "mono F ==> F P = P ==> UNION UNIV (up_iterate F) \ P" wenzelm@11355: apply (subgoal_tac "(!!i. up_iterate F i \ P)") wenzelm@11355: apply fast wenzelm@11355: apply (induct_tac i) wenzelm@11355: prefer 2 apply (drule (1) monoD) wenzelm@11355: apply auto wenzelm@11355: done oheimb@11351: wenzelm@11355: lemma UNION_up_iterate_is_lfp: wenzelm@11355: "up_cont F ==> lfp F = UNION UNIV (up_iterate F)" wenzelm@11355: apply (rule set_eq_subset [THEN iffD2]) wenzelm@11355: apply (rule conjI) wenzelm@11355: prefer 2 wenzelm@11355: apply (drule up_cont_mono) wenzelm@11355: apply (rule UNION_up_iterate_lowerbound) wenzelm@11355: apply assumption wenzelm@11355: apply (erule lfp_unfold [symmetric]) wenzelm@11355: apply (rule lfp_lowerbound) wenzelm@11355: apply (rule set_eq_subset [THEN iffD1, THEN conjunct2]) wenzelm@11355: apply (erule UNION_up_iterate_is_fp [symmetric]) wenzelm@11355: done oheimb@11351: oheimb@11351: wenzelm@19736: definition wenzelm@21404: down_iterate :: "('a set => 'a set) => nat => 'a set" where haftmann@30971: "down_iterate f n = (f ^^ n) UNIV" oheimb@11351: oheimb@11351: lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV" wenzelm@11355: by (simp add: down_iterate_def) oheimb@11351: wenzelm@11355: lemma down_iterate_Suc [simp]: wenzelm@11355: "down_iterate f (Suc i) = f (down_iterate f i)" wenzelm@11355: by (simp add: down_iterate_def) oheimb@11351: oheimb@11351: lemma down_iterate_chain: "mono F ==> down_chain (down_iterate F)" wenzelm@11355: apply (rule down_chainI) wenzelm@11355: apply (induct_tac i) wenzelm@11355: apply simp+ wenzelm@11355: apply (erule (1) monoD) wenzelm@11355: done oheimb@11351: wenzelm@11355: lemma INTER_down_iterate_is_fp: wenzelm@11355: "down_cont F ==> wenzelm@11355: F (INTER UNIV (down_iterate F)) = INTER UNIV (down_iterate F)" wenzelm@11355: apply (frule down_cont_mono [THEN down_iterate_chain]) wenzelm@11355: apply (drule (1) down_contD) wenzelm@11355: apply simp wenzelm@11355: apply (auto simp del: down_iterate_Suc simp add: down_iterate_Suc [symmetric]) wenzelm@11355: apply (case_tac xa) wenzelm@11355: apply auto wenzelm@11355: done oheimb@11351: wenzelm@11355: lemma INTER_down_iterate_upperbound: wenzelm@11355: "mono F ==> F P = P ==> P \ INTER UNIV (down_iterate F)" wenzelm@11355: apply (subgoal_tac "(!!i. P \ down_iterate F i)") wenzelm@11355: apply fast wenzelm@11355: apply (induct_tac i) wenzelm@11355: prefer 2 apply (drule (1) monoD) wenzelm@11355: apply auto wenzelm@11355: done oheimb@11351: wenzelm@11355: lemma INTER_down_iterate_is_gfp: wenzelm@11355: "down_cont F ==> gfp F = INTER UNIV (down_iterate F)" wenzelm@11355: apply (rule set_eq_subset [THEN iffD2]) wenzelm@11355: apply (rule conjI) wenzelm@11355: apply (drule down_cont_mono) wenzelm@11355: apply (rule INTER_down_iterate_upperbound) wenzelm@11355: apply assumption wenzelm@11355: apply (erule gfp_unfold [symmetric]) wenzelm@11355: apply (rule gfp_upperbound) wenzelm@11355: apply (rule set_eq_subset [THEN iffD1, THEN conjunct2]) wenzelm@11355: apply (erule INTER_down_iterate_is_fp) wenzelm@11355: done oheimb@11351: oheimb@11351: end