src/HOL/HOLCF/ex/Powerdomain_ex.thy
 author wenzelm Sun Nov 02 17:16:01 2014 +0100 (2014-11-02) changeset 58880 0baae4311a9f parent 42151 4da4fc77664b child 62175 8ffc4d0e652d permissions -rw-r--r--
```     1 (*  Title:      HOL/HOLCF/ex/Powerdomain_ex.thy
```
```     2     Author:     Brian Huffman
```
```     3 *)
```
```     4
```
```     5 section {* Powerdomain examples *}
```
```     6
```
```     7 theory Powerdomain_ex
```
```     8 imports HOLCF
```
```     9 begin
```
```    10
```
```    11 subsection {* Monadic sorting example *}
```
```    12
```
```    13 domain ordering = LT | EQ | GT
```
```    14
```
```    15 definition
```
```    16   compare :: "int lift \<rightarrow> int lift \<rightarrow> ordering" where
```
```    17   "compare = (FLIFT x y. if x < y then LT else if x = y then EQ else GT)"
```
```    18
```
```    19 definition
```
```    20   is_le :: "int lift \<rightarrow> int lift \<rightarrow> tr" where
```
```    21   "is_le = (\<Lambda> x y. case compare\<cdot>x\<cdot>y of LT \<Rightarrow> TT | EQ \<Rightarrow> TT | GT \<Rightarrow> FF)"
```
```    22
```
```    23 definition
```
```    24   is_less :: "int lift \<rightarrow> int lift \<rightarrow> tr" where
```
```    25   "is_less = (\<Lambda> x y. case compare\<cdot>x\<cdot>y of LT \<Rightarrow> TT | EQ \<Rightarrow> FF | GT \<Rightarrow> FF)"
```
```    26
```
```    27 definition
```
```    28   r1 :: "(int lift \<times> 'a) \<rightarrow> (int lift \<times> 'a) \<rightarrow> tr convex_pd" where
```
```    29   "r1 = (\<Lambda> (x,_) (y,_). case compare\<cdot>x\<cdot>y of
```
```    30           LT \<Rightarrow> {TT}\<natural> |
```
```    31           EQ \<Rightarrow> {TT, FF}\<natural> |
```
```    32           GT \<Rightarrow> {FF}\<natural>)"
```
```    33
```
```    34 definition
```
```    35   r2 :: "(int lift \<times> 'a) \<rightarrow> (int lift \<times> 'a) \<rightarrow> tr convex_pd" where
```
```    36   "r2 = (\<Lambda> (x,_) (y,_). {is_le\<cdot>x\<cdot>y, is_less\<cdot>x\<cdot>y}\<natural>)"
```
```    37
```
```    38 lemma r1_r2: "r1\<cdot>(x,a)\<cdot>(y,b) = (r2\<cdot>(x,a)\<cdot>(y,b) :: tr convex_pd)"
```
```    39 apply (simp add: r1_def r2_def)
```
```    40 apply (simp add: is_le_def is_less_def)
```
```    41 apply (cases "compare\<cdot>x\<cdot>y")
```
```    42 apply simp_all
```
```    43 done
```
```    44
```
```    45
```
```    46 subsection {* Picking a leaf from a tree *}
```
```    47
```
```    48 domain 'a tree =
```
```    49   Node (lazy "'a tree") (lazy "'a tree") |
```
```    50   Leaf (lazy "'a")
```
```    51
```
```    52 fixrec
```
```    53   mirror :: "'a tree \<rightarrow> 'a tree"
```
```    54 where
```
```    55   mirror_Leaf: "mirror\<cdot>(Leaf\<cdot>a) = Leaf\<cdot>a"
```
```    56 | mirror_Node: "mirror\<cdot>(Node\<cdot>l\<cdot>r) = Node\<cdot>(mirror\<cdot>r)\<cdot>(mirror\<cdot>l)"
```
```    57
```
```    58 lemma mirror_strict [simp]: "mirror\<cdot>\<bottom> = \<bottom>"
```
```    59 by fixrec_simp
```
```    60
```
```    61 fixrec
```
```    62   pick :: "'a tree \<rightarrow> 'a convex_pd"
```
```    63 where
```
```    64   pick_Leaf: "pick\<cdot>(Leaf\<cdot>a) = {a}\<natural>"
```
```    65 | pick_Node: "pick\<cdot>(Node\<cdot>l\<cdot>r) = pick\<cdot>l \<union>\<natural> pick\<cdot>r"
```
```    66
```
```    67 lemma pick_strict [simp]: "pick\<cdot>\<bottom> = \<bottom>"
```
```    68 by fixrec_simp
```
```    69
```
```    70 lemma pick_mirror: "pick\<cdot>(mirror\<cdot>t) = pick\<cdot>t"
```
```    71 by (induct t) (simp_all add: convex_plus_ac)
```
```    72
```
```    73 fixrec tree1 :: "int lift tree"
```
```    74 where "tree1 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>(Leaf\<cdot>(Def 2)))
```
```    75                    \<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))"
```
```    76
```
```    77 fixrec tree2 :: "int lift tree"
```
```    78 where "tree2 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>(Leaf\<cdot>(Def 2)))
```
```    79                    \<cdot>(Node\<cdot>\<bottom>\<cdot>(Leaf\<cdot>(Def 4)))"
```
```    80
```
```    81 fixrec tree3 :: "int lift tree"
```
```    82 where "tree3 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>tree3)
```
```    83                    \<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))"
```
```    84
```
```    85 declare tree1.simps tree2.simps tree3.simps [simp del]
```
```    86
```
```    87 lemma pick_tree1:
```
```    88   "pick\<cdot>tree1 = {Def 1, Def 2, Def 3, Def 4}\<natural>"
```
```    89 apply (subst tree1.simps)
```
```    90 apply simp
```
```    91 apply (simp add: convex_plus_ac)
```
```    92 done
```
```    93
```
```    94 lemma pick_tree2:
```
```    95   "pick\<cdot>tree2 = {Def 1, Def 2, \<bottom>, Def 4}\<natural>"
```
```    96 apply (subst tree2.simps)
```
```    97 apply simp
```
```    98 apply (simp add: convex_plus_ac)
```
```    99 done
```
```   100
```
```   101 lemma pick_tree3:
```
```   102   "pick\<cdot>tree3 = {Def 1, \<bottom>, Def 3, Def 4}\<natural>"
```
```   103 apply (subst tree3.simps)
```
```   104 apply simp
```
```   105 apply (induct rule: tree3.induct)
```
```   106 apply simp
```
```   107 apply simp
```
```   108 apply (simp add: convex_plus_ac)
```
```   109 apply simp
```
```   110 apply (simp add: convex_plus_ac)
```
```   111 done
```
```   112
```
```   113 end
```