I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.
theory Defs imports Main begin end
theory Submission
imports Defs
begin
context
fixes f :: "'a set \<Rightarrow> 'a set" and x\<^sub>0 :: "'a set"
assumes "mono f" and post_fixpoint: "x\<^sub>0 \<subseteq> f x\<^sub>0"
begin
theorem postfix_step: "\<Union> {(f^^i)(x\<^sub>0) | i :: nat. True} \<subseteq> \<Union> {(f^^(Suc i))(x\<^sub>0) | i :: nat. True}"
sorry
end
context
fixes f :: "'a set \<Rightarrow> 'a set"
assumes continuous: "\<And>X. X\<noteq>{} \<Longrightarrow> f (\<Union>X) = \<Union>(f ` X)"
begin
theorem mono: "x \<subseteq> y \<Longrightarrow> f x \<subseteq> f y"
sorry
lemma lfp_fold: "f (lfp f) = lfp f"
using lfp_unfold mono unfolding mono_def by blast
theorem lfp_ge: "\<Union>{(f^^i) {} | i. True} \<subseteq> lfp f"
sorry
theorem lfp_le: "lfp f \<subseteq> \<Union>{(f^^i) {} | i. True}" (is "_ \<subseteq> \<Union>?S")
sorry
corollary
"lfp f = \<Union>{(f^^i) {} | i. True}"
using lfp_le lfp_ge ..
end
end
theory Check
imports Submission
begin
context
fixes f :: "'a set \<Rightarrow> 'a set" and x\<^sub>0 :: "'a set"
assumes "mono f" and post_fixpoint: "x\<^sub>0 \<subseteq> f x\<^sub>0"
begin
theorem postfix_step: "\<Union> {(f^^i)(x\<^sub>0) | i :: nat. True} \<subseteq> \<Union> {(f^^(Suc i))(x\<^sub>0) | i :: nat. True}"
using \<open>mono f\<close> post_fixpoint by (rule Submission.postfix_step)
end
context
fixes f :: "'a set \<Rightarrow> 'a set"
assumes continuous: "\<And>X. X\<noteq>{} \<Longrightarrow> f (\<Union>X) = \<Union>(f ` X)"
begin
theorem mono: "x \<subseteq> y \<Longrightarrow> f x \<subseteq> f y"
using continuous by (rule Submission.mono)
theorem lfp_ge: "\<Union>{(f^^i) {} | i. True} \<subseteq> lfp f"
using continuous by (rule Submission.lfp_ge)
theorem lfp_le: "lfp f \<subseteq> \<Union>{(f^^i) {} | i. True}" (is "_ \<subseteq> \<Union>?S")
using continuous by (rule Submission.lfp_le)
end
end