# Theory SetPcpo

Up to index of Isabelle/HOLCF

theory SetPcpo
begin

```(*  Title:      HOLCF/SetPcpo.thy
ID:         \$Id: SetPcpo.thy,v 1.5 2008/05/16 19:41:07 huffman Exp \$
Author:     Brian Huffman
*)

header {* Set as a pointed cpo *}

theory SetPcpo
begin

instantiation bool :: po
begin

definition
less_bool_def: "(op \<sqsubseteq>) = (op -->)"

instance
by (intro_classes, unfold less_bool_def, safe)

end

lemma less_set_eq: "(op \<sqsubseteq>) = (op ⊆)"
by (simp add: less_fun_def less_bool_def le_fun_def le_bool_def expand_fun_eq)

instance bool :: finite_po ..

lemma Union_is_lub: "A <<| Union A"
unfolding is_lub_def is_ub_def less_set_eq by fast

instance bool :: cpo ..

lemma lub_eq_Union: "lub = Union"
by (rule ext, rule thelubI [OF Union_is_lub])

instance bool :: pcpo
proof
have "∀y::bool. False \<sqsubseteq> y" unfolding less_bool_def by simp
thus "∃x::bool. ∀y. x \<sqsubseteq> y" ..
qed

lemma UU_eq_empty: "⊥ = {}"
by (rule UU_I [symmetric], simp add: less_set_eq)

lemmas set_cpo_simps = less_set_eq lub_eq_Union UU_eq_empty

subsection {* Admissibility of set predicates *}

subsection {* Compactness *}

lemma compact_empty: "compact {}"
by (fold UU_eq_empty, simp)

lemma compact_insert: "compact A ==> compact (insert x A)"
unfolding compact_def set_cpo_simps

lemma finite_imp_compact: "finite A ==> compact A"
by (induct A set: finite, rule compact_empty, erule compact_insert)

end
```

lemma less_set_eq:

`  op << = op ⊆`

lemma Union_is_lub:

`  A <<| Union A`

lemma lub_eq_Union:

`  lub = Union`

lemma UU_eq_empty:

`  UU = {}`

lemma set_cpo_simps:

`  op << = op ⊆`
`  lub = Union`
`  UU = {}`

`  adm (λA. ∃x. x ∈ A)`

`  adm (op ∈ x)`

`  adm (op ∉ x)`

`  (!!x. adm (λA. P A x)) ==> adm (λA. ∀x∈A. P A x)`

`  adm (λA. Bex A P)`

`  adm (λA. A ⊆ B)`

`  adm (op ⊆ B)`

`  adm (λA. ∃x. x ∈ A)`
`  adm (op ∈ x)`
`  adm (op ∉ x)`
`  adm (λA. Bex A P)`
`  (!!x. adm (λA. P A x)) ==> adm (λA. ∀x∈A. P A x)`
`  adm (λA. A ⊆ B)`
`  adm (op ⊆ B)`

### Compactness

lemma compact_empty:

`  compact {}`

lemma compact_insert:

`  compact A ==> compact (insert x A)`

lemma finite_imp_compact:

`  finite A ==> compact A`