equal
deleted
inserted
replaced
69 "chain S = (\<forall>i. S i \<subseteq> S(Suc i))" |
69 "chain S = (\<forall>i. S i \<subseteq> S(Suc i))" |
70 |
70 |
71 lemma chain_total: "chain S \<Longrightarrow> S i \<le> S j \<or> S j \<le> S i" |
71 lemma chain_total: "chain S \<Longrightarrow> S i \<le> S j \<or> S j \<le> S i" |
72 by (metis chain_def le_cases lift_Suc_mono_le) |
72 by (metis chain_def le_cases lift_Suc_mono_le) |
73 |
73 |
74 definition cont :: "('a set \<Rightarrow> 'a set) \<Rightarrow> bool" where |
74 definition cont :: "('a set \<Rightarrow> 'b set) \<Rightarrow> bool" where |
75 "cont f = (\<forall>S. chain S \<longrightarrow> f(UN n. S n) = (UN n. f(S n)))" |
75 "cont f = (\<forall>S. chain S \<longrightarrow> f(UN n. S n) = (UN n. f(S n)))" |
76 |
76 |
77 lemma mono_if_cont: fixes f :: "'a set \<Rightarrow> 'a set" |
77 lemma mono_if_cont: fixes f :: "'a set \<Rightarrow> 'b set" |
78 assumes "cont f" shows "mono f" |
78 assumes "cont f" shows "mono f" |
79 proof |
79 proof |
80 fix a b :: "'a set" assume "a \<subseteq> b" |
80 fix a b :: "'a set" assume "a \<subseteq> b" |
81 let ?S = "\<lambda>n::nat. if n=0 then a else b" |
81 let ?S = "\<lambda>n::nat. if n=0 then a else b" |
82 have "chain ?S" using `a \<subseteq> b` by(auto simp: chain_def) |
82 have "chain ?S" using `a \<subseteq> b` by(auto simp: chain_def) |