# Theory Powerdomain_ex

theory Powerdomain_ex
imports HOLCF
```(*  Title:      HOL/HOLCF/ex/Powerdomain_ex.thy
Author:     Brian Huffman
*)

section ‹Powerdomain examples›

theory Powerdomain_ex
imports HOLCF
begin

domain ordering = LT | EQ | GT

definition
compare :: "int lift → int lift → ordering" where
"compare = (FLIFT x y. if x < y then LT else if x = y then EQ else GT)"

definition
is_le :: "int lift → int lift → tr" where
"is_le = (Λ x y. case compare⋅x⋅y of LT ⇒ TT | EQ ⇒ TT | GT ⇒ FF)"

definition
is_less :: "int lift → int lift → tr" where
"is_less = (Λ x y. case compare⋅x⋅y of LT ⇒ TT | EQ ⇒ FF | GT ⇒ FF)"

definition
r1 :: "(int lift × 'a) → (int lift × 'a) → tr convex_pd" where
"r1 = (Λ (x,_) (y,_). case compare⋅x⋅y of
LT ⇒ {TT}♮ |
EQ ⇒ {TT, FF}♮ |
GT ⇒ {FF}♮)"

definition
r2 :: "(int lift × 'a) → (int lift × 'a) → tr convex_pd" where
"r2 = (Λ (x,_) (y,_). {is_le⋅x⋅y, is_less⋅x⋅y}♮)"

lemma r1_r2: "r1⋅(x,a)⋅(y,b) = (r2⋅(x,a)⋅(y,b) :: tr convex_pd)"
apply (cases "compare⋅x⋅y")
apply simp_all
done

subsection ‹Picking a leaf from a tree›

domain 'a tree =
Node (lazy "'a tree") (lazy "'a tree") |
Leaf (lazy "'a")

fixrec
mirror :: "'a tree → 'a tree"
where
mirror_Leaf: "mirror⋅(Leaf⋅a) = Leaf⋅a"
| mirror_Node: "mirror⋅(Node⋅l⋅r) = Node⋅(mirror⋅r)⋅(mirror⋅l)"

lemma mirror_strict [simp]: "mirror⋅⊥ = ⊥"
by fixrec_simp

fixrec
pick :: "'a tree → 'a convex_pd"
where
pick_Leaf: "pick⋅(Leaf⋅a) = {a}♮"
| pick_Node: "pick⋅(Node⋅l⋅r) = pick⋅l ∪♮ pick⋅r"

lemma pick_strict [simp]: "pick⋅⊥ = ⊥"
by fixrec_simp

lemma pick_mirror: "pick⋅(mirror⋅t) = pick⋅t"
by (induct t) (simp_all add: convex_plus_ac)

fixrec tree1 :: "int lift tree"
where "tree1 = Node⋅(Node⋅(Leaf⋅(Def 1))⋅(Leaf⋅(Def 2)))
⋅(Node⋅(Leaf⋅(Def 3))⋅(Leaf⋅(Def 4)))"

fixrec tree2 :: "int lift tree"
where "tree2 = Node⋅(Node⋅(Leaf⋅(Def 1))⋅(Leaf⋅(Def 2)))
⋅(Node⋅⊥⋅(Leaf⋅(Def 4)))"

fixrec tree3 :: "int lift tree"
where "tree3 = Node⋅(Node⋅(Leaf⋅(Def 1))⋅tree3)
⋅(Node⋅(Leaf⋅(Def 3))⋅(Leaf⋅(Def 4)))"

declare tree1.simps tree2.simps tree3.simps [simp del]

lemma pick_tree1:
"pick⋅tree1 = {Def 1, Def 2, Def 3, Def 4}♮"
apply (subst tree1.simps)
apply simp
done

lemma pick_tree2:
"pick⋅tree2 = {Def 1, Def 2, ⊥, Def 4}♮"
apply (subst tree2.simps)
apply simp
done

lemma pick_tree3:
"pick⋅tree3 = {Def 1, ⊥, Def 3, Def 4}♮"
apply (subst tree3.simps)
apply simp
apply (induct rule: tree3.induct)
apply simp
apply simp