theory "Env-HOLCF" imports Env "HOLCF-Utils" begin subsubsection {* Continuity and pcpo-valued functions *} lemma override_on_belowI: assumes "⋀ a. a ∈ S ⟹ y a ⊑ z a" and "⋀ a. a ∉ S ⟹ x a ⊑ z a" shows "x ++⇘S⇙ y ⊑ z" using assms apply - apply (rule fun_belowI) apply (case_tac "xa ∈ S") apply auto done lemma override_on_cont1: "cont (λ x. x ++⇘S⇙ m)" by (rule cont2cont_lambda) (auto simp add: override_on_def) lemma override_on_cont2: "cont (λ x. m ++⇘S⇙ x)" by (rule cont2cont_lambda) (auto simp add: override_on_def) lemma override_on_cont2cont[simp, cont2cont]: assumes "cont f" assumes "cont g" shows "cont (λ x. f x ++⇘S⇙ g x)" by (rule cont_apply[OF assms(1) override_on_cont1 cont_compose[OF override_on_cont2 assms(2)]]) lemma override_on_mono: assumes "x1 ⊑ (x2 :: 'a::type ⇒ 'b::cpo)" assumes "y1 ⊑ y2" shows "x1 ++⇘S⇙ y1 ⊑ x2 ++⇘S⇙ y2" by (rule below_trans[OF cont2monofunE[OF override_on_cont1 assms(1)] cont2monofunE[OF override_on_cont2 assms(2)]]) lemma fun_upd_below_env_deleteI: assumes "env_delete x ρ ⊑ env_delete x ρ'" assumes "y ⊑ ρ' x" shows "ρ(x := y) ⊑ ρ'" using assms apply (auto intro!: fun_upd_belowI simp add: env_delete_def) by (metis fun_belowD fun_upd_other) lemma fun_upd_belowI2: assumes "⋀ z . z ≠ x ⟹ ρ z ⊑ ρ' z" assumes "ρ x ⊑ y" shows "ρ ⊑ ρ'(x := y)" apply (rule fun_belowI) using assms by auto lemma env_restr_belowI: assumes "⋀ x. x ∈ S ⟹ (m1 f|` S) x ⊑ (m2 f|` S) x" shows "m1 f|` S ⊑ m2 f|` S" apply (rule fun_belowI) by (metis assms below_bottom_iff lookup_env_restr_not_there) lemma env_restr_belowI2: assumes "⋀ x. x ∈ S ⟹ m1 x ⊑ m2 x" shows "m1 f|` S ⊑ m2" by (rule fun_belowI) (simp add: assms env_restr_def) lemma env_restr_below_itself: shows "m f|` S ⊑ m" apply (rule fun_belowI) apply (case_tac "x ∈ S") apply auto done lemma env_restr_cont: "cont (env_restr S)" apply (rule cont2cont_lambda) apply (case_tac "y ∈ S") apply auto done lemma env_restr_belowD: assumes "m1 f|` S ⊑ m2 f|` S" assumes "x ∈ S" shows "m1 x ⊑ m2 x" using fun_belowD[OF assms(1), where x = x] assms(2) by simp lemma env_restr_eqD: assumes "m1 f|` S = m2 f|` S" assumes "x ∈ S" shows "m1 x = m2 x" by (metis assms(1) assms(2) lookup_env_restr) lemma env_restr_below_subset: assumes "S ⊆ S'" and "m1 f|` S' ⊑ m2 f|` S'" shows "m1 f|` S ⊑ m2 f|` S" using assms by (auto intro!: env_restr_belowI dest: env_restr_belowD) lemma override_on_below_restrI: assumes " x f|` (-S) ⊑ z f|` (-S)" and "y f|` S ⊑ z f|` S" shows "x ++⇘S⇙ y ⊑ z" using assms by (auto intro: override_on_belowI dest:env_restr_belowD) lemma fmap_below_add_restrI: assumes "x f|` (-S) ⊑ y f|` (-S)" and "x f|` S ⊑ z f|` S" shows "x ⊑ y ++⇘S⇙ z" using assms by (auto intro!: fun_belowI dest:env_restr_belowD simp add: lookup_override_on_eq) lemmas env_restr_cont2cont[simp,cont2cont] = cont_compose[OF env_restr_cont] lemma env_delete_cont: "cont (env_delete x)" apply (rule cont2cont_lambda) apply (case_tac "y = x") apply auto done lemmas env_delete_cont2cont[simp,cont2cont] = cont_compose[OF env_delete_cont] end