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