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 11

This is the task corresponding to homework 11.

## Resources

### Definitions File

```theory Defs
imports "HOL-IMP.Big_Step"
begin

datatype entry = Unchanged ("'_'_'_'_'_'_'_'_") | V "(int\<times>int) set"

unbundle lattice_syntax

definition chain :: "(nat \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool"
where "chain C \<longleftrightarrow> (\<forall>n. C n \<le> C (Suc n))"

definition continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool"
where "continuous f \<longleftrightarrow> (\<forall>C. chain C \<longrightarrow> f (\<Squnion> (range C)) = \<Squnion> (f ` range C))"

lemma continuousD: "\<lbrakk>continuous f; chain C\<rbrakk> \<Longrightarrow> f (\<Squnion> (range C)) = \<Squnion> (f ` range C)"
unfolding continuous_def by auto

consts A\<^sub>0 :: "entry list"

consts A\<^sub>1 :: "entry list"

consts A\<^sub>2 :: "entry list"

consts A\<^sub>3 :: "entry list"

consts A\<^sub>4 :: "entry list"

consts A\<^sub>5 :: "entry list"

consts A\<^sub>6 :: "entry list"

end```

### Template File

```theory Submission
imports Defs
begin

definition A\<^sub>0 :: "entry list"  where
"A\<^sub>0 _ = undefined"

definition A\<^sub>1 :: "entry list"  where
"A\<^sub>1 _ = undefined"

definition A\<^sub>2 :: "entry list"  where
"A\<^sub>2 _ = undefined"

definition A\<^sub>3 :: "entry list"  where
"A\<^sub>3 _ = undefined"

definition A\<^sub>4 :: "entry list"  where
"A\<^sub>4 _ = undefined"

definition A\<^sub>5 :: "entry list"  where
"A\<^sub>5 _ = undefined"

definition A\<^sub>6 :: "entry list"  where
"A\<^sub>6 _ = undefined"

lemma cont_imp_mono:
fixes f :: "'a::complete_lattice \<Rightarrow> 'b::complete_lattice"
assumes "continuous f"
shows "mono f"
sorry

thm mono_def monoI monoD

theorem kleene_lfp:
fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
assumes CONT: "continuous f"
shows "lfp f = \<Squnion> (range (\<lambda>i. (f^^i) \<bottom>))"
proof -
txt \<open> We propose a proof structure here, however, you may deviate from this
and use your own proof structure: \<close>
let ?C = "\<lambda>i. (f^^i) \<bottom>"
note MONO=cont_imp_mono[OF CONT]
have CHAIN: "chain ?C"
sorry
qed

show ?thesis
proof (rule antisym)
show "\<Squnion> (range ?C) \<le> lfp f"
next
show "lfp f \<le> Sup (range ?C)"
qed
qed

thm lfp_unfold lfp_lowerbound Sup_subset_mono range_eqI

end```

### Check File

```theory Check
imports Submission
begin

lemma cont_imp_mono: "\<And> f :: 'a::complete_lattice \<Rightarrow> 'b::complete_lattice. (continuous f) \<Longrightarrow> mono f"
by (rule Submission.cont_imp_mono)

theorem kleene_lfp: "\<And> f :: 'a::complete_lattice \<Rightarrow> 'a. (continuous f) \<Longrightarrow> lfp f = \<Squnion> (range (\<lambda>i. (f^^i) \<bottom>))"
by (rule Submission.kleene_lfp)

end```

Terms and Conditions