# Theory HOLCFUtils

Up to index of Isabelle/HOL/HOLCF/Shivers-CFA

theory HOLCFUtils
imports HOLCF
`header {* HOLCF Utility lemmas *}theory HOLCFUtilsimports HOLCFbegintext {*We use @{theory HOLCF} to define the denotational semantics. By default, HOLCF does not turn the regular @{text set} type into a partial order, so this is done here. Some of the lemmas here are contributed by Brian Huffman.We start by making the type @{text bool} a pointed chain-complete partial order.*}instantiation bool :: pobegindefinition  "x \<sqsubseteq> y <-> (x --> y)"instance by (default, unfold below_bool_def, fast+)endinstance bool :: chfinapply defaultapply (drule finite_range_imp_finch)apply (rule finite)apply (simp add: finite_chain_def)doneinstance bool :: pcpoproof  have "∀y. False \<sqsubseteq> y" by (simp add: below_bool_def)  thus "∃x::bool. ∀y. x \<sqsubseteq> y" ..qedlemma is_lub_bool: "S <<| (True ∈ S)"  unfolding is_lub_def is_ub_def below_bool_def by autolemma lub_bool: "lub S = (True ∈ S)"  using is_lub_bool by (rule lub_eqI)lemma bottom_eq_False[simp]: "⊥ = False"by (rule below_antisym [OF minimal], simp add: below_bool_def)text {*To convert between the squared syntax used by @{theory HOLCF} and the regular, round syntax for sets, we state some of the equivalencies.*}instantiation set :: (type) pobegindefinition  "A \<sqsubseteq> B <-> A ⊆ B"instance by (default, unfold below_set_def, fast+)endlemma sqsubset_is_subset: "A \<sqsubseteq> B <-> A ⊆ B"  by (fact below_set_def)lemma is_lub_set: "S <<| \<Union>S"  unfolding is_lub_def is_ub_def below_set_def by fastlemma lub_is_union: "lub S = \<Union>S"  using is_lub_set by (rule lub_eqI)instance set :: (type) cpo  by (default, fast intro: is_lub_set)lemma emptyset_is_bot[simp]: "{} \<sqsubseteq> S"  by (simp add:sqsubset_is_subset)instance set :: (type) pcpo  by (default, fast intro: emptyset_is_bot)lemma bot_bool_is_emptyset[simp]: "⊥ = {}"  using emptyset_is_bot by (rule bottomI [symmetric])text {*To actually use these instance in @{text fixrec} definitions or fixed-point inductions, we need continuity requrements for various boolean and set operations.*}lemma cont2cont_disj [simp, cont2cont]:  assumes f: "cont (λx. f x)" and g: "cont (λx. g x)"  shows "cont (λx. f x ∨ g x)"apply (rule cont_apply [OF f])apply (rule chfindom_monofun2cont)apply (rule monofunI, simp add: below_bool_def)apply (rule cont_compose [OF _ g])apply (rule chfindom_monofun2cont)apply (rule monofunI, simp add: below_bool_def)donelemma cont2cont_imp[simp, cont2cont]:  assumes f: "cont (λx. ¬ f x)" and g: "cont (λx. g x)"  shows "cont (λx. f x --> g x)"unfolding imp_conv_disj by (rule cont2cont_disj[OF f g])lemma cont2cont_Collect [simp, cont2cont]:  assumes "!!y. cont (λx. f x y)"  shows "cont (λx. {y. f x y})"apply (rule contI)apply (subst cont2contlubE [OF assms], assumption)apply (auto simp add: is_lub_def is_ub_def below_set_def lub_bool)donelemma cont2cont_mem [simp, cont2cont]:  assumes "cont (λx. f x)"  shows "cont (λx. y ∈ f x)"apply (rule cont_compose [OF _ assms])apply (rule contI)apply (auto simp add: is_lub_def is_ub_def below_bool_def lub_is_union)donelemma cont2cont_union [simp, cont2cont]:  "cont (λx. f x) ==> cont (λx. g x)==> cont (λx. f x ∪ g x)"unfolding Un_def by simplemma cont2cont_insert [simp, cont2cont]:  assumes "cont (λx. f x)"  shows "cont (λx. insert y (f x))"unfolding insert_def using assmsby (intro cont2cont)lemmas adm_subset = adm_below[where ?'b = "'a::type set", unfolded sqsubset_is_subset]lemma cont2cont_UNION[cont2cont,simp]:  assumes "cont f"      and "!! y. cont (λx. g x y)"  shows "cont (λx. \<Union>y∈ f x. g x y)"proof(induct rule: contI2[case_names Mono Limit])case Mono  show "monofun (λx. \<Union>y∈f x. g x y)"    by (rule monofunI)(auto iff:sqsubset_is_subset dest: monofunE[OF assms(1)[THEN cont2mono]] monofunE[OF assms(2)[THEN cont2mono]])nextcase (Limit Y)  have "(\<Union>y∈f (\<Squnion> i. Y i). g (\<Squnion> j. Y j) y) ⊆ (\<Squnion> k. \<Union>y∈f (Y k). g (Y k) y)"  proof    fix x assume "x ∈ (\<Union>y∈f (\<Squnion> i. Y i). g (\<Squnion> j. Y j) y)"    then obtain y where "y∈f (\<Squnion> i. Y i)" and "x∈ g (\<Squnion> j. Y j) y" by auto    hence "y ∈ (\<Squnion> i. f (Y i))" and "x∈ (\<Squnion> j. g (Y j) y)" by (auto simp add: cont2contlubE[OF assms(1) Limit(1)] cont2contlubE[OF assms(2) Limit(1)])    then obtain i and j where yi: "y∈ f (Y i)" and xj: "x∈ g (Y j) y" by (auto simp add:lub_is_union)    obtain k where "i≤k" and "j≤k" by (erule_tac x = "max i j" in meta_allE)auto    from yi and xj have "y ∈ f (Y k)" and "x∈ g (Y k) y"      using monofunE[OF assms(1)[THEN cont2mono], OF chain_mono[OF Limit(1) `i≤k`]]        and monofunE[OF assms(2)[THEN cont2mono], OF chain_mono[OF Limit(1) `j≤k`]]      by (auto simp add:sqsubset_is_subset)    hence "x∈ (\<Union>y∈ f (Y k). g (Y k) y)" by auto    thus "x∈ (\<Squnion> k. \<Union>y∈f (Y k). g (Y k) y)" by (auto simp add:lub_is_union)  qed  thus ?case by (simp add:sqsubset_is_subset)qedlemma cont2cont_Let_simple[simp,cont2cont]:  assumes "cont (λx. g x t)"  shows "cont (λx. let y = t in g x y)"unfolding Let_def using assms .lemma cont2cont_list_case [simp, cont2cont]:  assumes "!!y. cont (λx. f1 x)"     and  "!!y z. cont (λx. f2 x y z)"  shows "cont (λx. list_case (f1 x) (f2 x) l)"using assmsby (cases l) autotext {* As with the continuity lemmas, we need admissibility lemmas. *}lemma adm_not_mem:  assumes "cont (λx. f x)"  shows "adm (λx. y ∉ f x)"using assmsapply (erule_tac t = f in adm_subst)proof (rule admI)fix Y :: "nat => 'b set"assume chain: "chain Y"assume "∀i. y ∉ Y i" hence  "(\<Squnion> i. y ∈ Y i) = False"  by autothus "y ∉ (\<Squnion> i. Y i)"  using chain unfolding lub_bool lub_is_union by autoqedlemma adm_id[simp]: "adm (λx . x)"by (rule adm_chfin)lemma adm_Not[simp]: "adm Not"by (rule adm_chfin)lemma adm_prod_split:  assumes "adm (λp. f (fst p) (snd p))"  shows "adm (λ(x,y). f x y)"using assms unfolding split_def .lemma adm_ball':  assumes "!! y. adm (λx. y ∈ A x --> P x y)"  shows "adm (λx. ∀y ∈ A x . P x y)"by (subst Ball_def, rule adm_all[OF assms])lemma adm_not_conj:  "[|adm (λx. ¬ P x); adm (λx. ¬ Q x)|] ==> adm (λx. ¬ (P x ∧ Q x))"by simplemma adm_single_valued: assumes "cont (λx. f x)" shows "adm (λx. single_valued (f x))"using assmsunfolding single_valued_defby (intro adm_lemmas adm_not_mem cont2cont adm_subst[of f])text {*To match Shivers' syntax we introduce the power-syntax for iterated function application.*}abbreviation niceiterate ("(_⇗_⇖)" [1000] 1000)  where "niceiterate f i ≡ iterate i·f"end`