src/HOL/HOLCF/ex/Powerdomain_ex.thy
changeset 40774 0437dbc127b3
parent 40497 d2e876d6da8c
child 41399 ad093e4638e2
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,113 @@
     1.4 +(*  Title:      HOLCF/ex/Powerdomain_ex.thy
     1.5 +    Author:     Brian Huffman
     1.6 +*)
     1.7 +
     1.8 +header {* Powerdomain examples *}
     1.9 +
    1.10 +theory Powerdomain_ex
    1.11 +imports HOLCF
    1.12 +begin
    1.13 +
    1.14 +subsection {* Monadic sorting example *}
    1.15 +
    1.16 +domain ordering = LT | EQ | GT
    1.17 +
    1.18 +definition
    1.19 +  compare :: "int lift \<rightarrow> int lift \<rightarrow> ordering" where
    1.20 +  "compare = (FLIFT x y. if x < y then LT else if x = y then EQ else GT)"
    1.21 +
    1.22 +definition
    1.23 +  is_le :: "int lift \<rightarrow> int lift \<rightarrow> tr" where
    1.24 +  "is_le = (\<Lambda> x y. case compare\<cdot>x\<cdot>y of LT \<Rightarrow> TT | EQ \<Rightarrow> TT | GT \<Rightarrow> FF)"
    1.25 +
    1.26 +definition
    1.27 +  is_less :: "int lift \<rightarrow> int lift \<rightarrow> tr" where
    1.28 +  "is_less = (\<Lambda> x y. case compare\<cdot>x\<cdot>y of LT \<Rightarrow> TT | EQ \<Rightarrow> FF | GT \<Rightarrow> FF)"
    1.29 +
    1.30 +definition
    1.31 +  r1 :: "(int lift \<times> 'a) \<rightarrow> (int lift \<times> 'a) \<rightarrow> tr convex_pd" where
    1.32 +  "r1 = (\<Lambda> (x,_) (y,_). case compare\<cdot>x\<cdot>y of
    1.33 +          LT \<Rightarrow> {TT}\<natural> |
    1.34 +          EQ \<Rightarrow> {TT, FF}\<natural> |
    1.35 +          GT \<Rightarrow> {FF}\<natural>)"
    1.36 +
    1.37 +definition
    1.38 +  r2 :: "(int lift \<times> 'a) \<rightarrow> (int lift \<times> 'a) \<rightarrow> tr convex_pd" where
    1.39 +  "r2 = (\<Lambda> (x,_) (y,_). {is_le\<cdot>x\<cdot>y, is_less\<cdot>x\<cdot>y}\<natural>)"
    1.40 +
    1.41 +lemma r1_r2: "r1\<cdot>(x,a)\<cdot>(y,b) = (r2\<cdot>(x,a)\<cdot>(y,b) :: tr convex_pd)"
    1.42 +apply (simp add: r1_def r2_def)
    1.43 +apply (simp add: is_le_def is_less_def)
    1.44 +apply (cases "compare\<cdot>x\<cdot>y")
    1.45 +apply simp_all
    1.46 +done
    1.47 +
    1.48 +
    1.49 +subsection {* Picking a leaf from a tree *}
    1.50 +
    1.51 +domain 'a tree =
    1.52 +  Node (lazy "'a tree") (lazy "'a tree") |
    1.53 +  Leaf (lazy "'a")
    1.54 +
    1.55 +fixrec
    1.56 +  mirror :: "'a tree \<rightarrow> 'a tree"
    1.57 +where
    1.58 +  mirror_Leaf: "mirror\<cdot>(Leaf\<cdot>a) = Leaf\<cdot>a"
    1.59 +| mirror_Node: "mirror\<cdot>(Node\<cdot>l\<cdot>r) = Node\<cdot>(mirror\<cdot>r)\<cdot>(mirror\<cdot>l)"
    1.60 +
    1.61 +lemma mirror_strict [simp]: "mirror\<cdot>\<bottom> = \<bottom>"
    1.62 +by fixrec_simp
    1.63 +
    1.64 +fixrec
    1.65 +  pick :: "'a tree \<rightarrow> 'a convex_pd"
    1.66 +where
    1.67 +  pick_Leaf: "pick\<cdot>(Leaf\<cdot>a) = {a}\<natural>"
    1.68 +| pick_Node: "pick\<cdot>(Node\<cdot>l\<cdot>r) = pick\<cdot>l +\<natural> pick\<cdot>r"
    1.69 +
    1.70 +lemma pick_strict [simp]: "pick\<cdot>\<bottom> = \<bottom>"
    1.71 +by fixrec_simp
    1.72 +
    1.73 +lemma pick_mirror: "pick\<cdot>(mirror\<cdot>t) = pick\<cdot>t"
    1.74 +by (induct t) (simp_all add: convex_plus_ac)
    1.75 +
    1.76 +fixrec tree1 :: "int lift tree"
    1.77 +where "tree1 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>(Leaf\<cdot>(Def 2)))
    1.78 +                   \<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))"
    1.79 +
    1.80 +fixrec tree2 :: "int lift tree"
    1.81 +where "tree2 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>(Leaf\<cdot>(Def 2)))
    1.82 +                   \<cdot>(Node\<cdot>\<bottom>\<cdot>(Leaf\<cdot>(Def 4)))"
    1.83 +
    1.84 +fixrec tree3 :: "int lift tree"
    1.85 +where "tree3 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>tree3)
    1.86 +                   \<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))"
    1.87 +
    1.88 +declare tree1.simps tree2.simps tree3.simps [simp del]
    1.89 +
    1.90 +lemma pick_tree1:
    1.91 +  "pick\<cdot>tree1 = {Def 1, Def 2, Def 3, Def 4}\<natural>"
    1.92 +apply (subst tree1.simps)
    1.93 +apply simp
    1.94 +apply (simp add: convex_plus_ac)
    1.95 +done
    1.96 +
    1.97 +lemma pick_tree2:
    1.98 +  "pick\<cdot>tree2 = {Def 1, Def 2, \<bottom>, Def 4}\<natural>"
    1.99 +apply (subst tree2.simps)
   1.100 +apply simp
   1.101 +apply (simp add: convex_plus_ac)
   1.102 +done
   1.103 +
   1.104 +lemma pick_tree3:
   1.105 +  "pick\<cdot>tree3 = {Def 1, \<bottom>, Def 3, Def 4}\<natural>"
   1.106 +apply (subst tree3.simps)
   1.107 +apply simp
   1.108 +apply (induct rule: tree3.induct)
   1.109 +apply simp
   1.110 +apply simp
   1.111 +apply (simp add: convex_plus_ac)
   1.112 +apply simp
   1.113 +apply (simp add: convex_plus_ac)
   1.114 +done
   1.115 +
   1.116 +end