Theory Powerdomain_ex

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

section ‹Powerdomain examples›

theory Powerdomain_ex
imports HOLCF
begin

subsection ‹Monadic sorting example›

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 comparexy of LT  TT | EQ  TT | GT  FF)"

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

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

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

lemma r1_r2: "r1(x,a)(y,b) = (r2(x,a)(y,b) :: tr convex_pd)"
apply (simp add: r1_def r2_def)
apply (simp add: is_le_def is_less_def)
apply (cases "comparexy")
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(Leafa) = Leafa"
| mirror_Node: "mirror(Nodelr) = Node(mirrorr)(mirrorl)"

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

fixrec
  pick :: "'a tree  'a convex_pd"
where
  pick_Leaf: "pick(Leafa) = {a}♮"
| pick_Node: "pick(Nodelr) = pickl ∪♮ pickr"

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

lemma pick_mirror: "pick(mirrort) = pickt"
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:
  "picktree1 = {Def 1, Def 2, Def 3, Def 4}♮"
apply (subst tree1.simps)
apply simp
apply (simp add: convex_plus_ac)
done

lemma pick_tree2:
  "picktree2 = {Def 1, Def 2, , Def 4}♮"
apply (subst tree2.simps)
apply simp
apply (simp add: convex_plus_ac)
done

lemma pick_tree3:
  "picktree3 = {Def 1, , Def 3, Def 4}♮"
apply (subst tree3.simps)
apply simp
apply (induct rule: tree3.induct)
apply simp
apply simp
apply (simp add: convex_plus_ac)
apply simp
apply (simp add: convex_plus_ac)
done

end