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.

# Homework 14

## Resources

### Definitions File

```theory Defs
imports Main
begin

end```

### Template File

```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```

### Check File

```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```

Terms and Conditions