Cookies disclaimer

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.

Homework 11

This is the task corresponding to homework 11.


Download Files

Definitions File

theory Defs
  imports "HOL-IMP.Big_Step"

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"


Template File

theory Submission
  imports Defs

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"

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"

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

thm lfp_unfold lfp_lowerbound Sup_subset_mono range_eqI


Check File

theory Check
  imports Submission

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)


Terms and Conditions