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