96 qed |
96 qed |
97 |
97 |
98 theorem lfp_if_cont: |
98 theorem lfp_if_cont: |
99 assumes "cont f" shows "lfp f = (UN n. (f^^n) {})" (is "_ = ?U") |
99 assumes "cont f" shows "lfp f = (UN n. (f^^n) {})" (is "_ = ?U") |
100 proof |
100 proof |
|
101 from assms mono_if_cont |
|
102 have mono: "(f ^^ n) {} \<subseteq> (f ^^ Suc n) {}" for n |
|
103 using funpow_decreasing [of n "Suc n"] by auto |
101 show "lfp f \<subseteq> ?U" |
104 show "lfp f \<subseteq> ?U" |
102 proof (rule lfp_lowerbound) |
105 proof (rule lfp_lowerbound) |
103 have "f ?U = (UN n. (f^^Suc n){})" |
106 have "f ?U = (UN n. (f^^Suc n){})" |
104 using chain_iterates[OF mono_if_cont[OF assms]] assms |
107 using chain_iterates[OF mono_if_cont[OF assms]] assms |
105 by(simp add: cont_def) |
108 by(simp add: cont_def) |
106 also have "\<dots> = (f^^0){} \<union> \<dots>" by simp |
109 also have "\<dots> = (f^^0){} \<union> \<dots>" by simp |
107 also have "\<dots> = ?U" |
110 also have "\<dots> = ?U" |
108 using assms funpow_decreasing le_SucI mono_if_cont by blast |
111 using mono by auto (metis funpow_simps_right(2) funpow_swap1 o_apply) |
109 finally show "f ?U \<subseteq> ?U" by simp |
112 finally show "f ?U \<subseteq> ?U" by simp |
110 qed |
113 qed |
111 next |
114 next |
112 { fix n p assume "f p \<subseteq> p" |
115 { fix n p assume "f p \<subseteq> p" |
113 have "(f^^n){} \<subseteq> p" |
116 have "(f^^n){} \<subseteq> p" |