# HG changeset patch
# User huffman
# Date 1235065189 28800
# Node ID 5deee36e33c420579453ef0df0bc6983be0e3b41
# Parent  c60ace776315c6245bc9fc12912c7de05ffedc3f
add Powerdomain_ex.thy

diff -r c60ace776315 -r 5deee36e33c4 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Thu Feb 19 08:07:52 2009 -0800
+++ b/src/HOLCF/IsaMakefile	Thu Feb 19 09:39:49 2009 -0800
@@ -89,6 +89,7 @@
 
 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Stream.thy ex/Dagstuhl.thy \
   ex/Dnat.thy ex/Fix2.thy ex/Focus_ex.thy ex/Hoare.thy ex/Loop.thy \
+  ex/Powerdomain_ex.thy \
   ex/ROOT.ML ex/Fixrec_ex.thy ../HOL/Library/Nat_Infinity.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
 
diff -r c60ace776315 -r 5deee36e33c4 src/HOLCF/ex/Powerdomain_ex.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Powerdomain_ex.thy	Thu Feb 19 09:39:49 2009 -0800
@@ -0,0 +1,123 @@
+(*  Title:      HOLCF/ex/Powerdomain_ex.thy
+    Author:     Brian Huffman
+*)
+
+header {* Powerdomain examples *}
+
+theory Powerdomain_ex
+imports HOLCF
+begin
+
+defaultsort bifinite
+
+subsection {* Monadic sorting example *}
+
+domain ordering = LT | EQ | GT
+
+declare ordering.rews [simp]
+
+definition
+  compare :: "int lift \<rightarrow> int lift \<rightarrow> ordering" where
+  "compare = (FLIFT x y. if x < y then LT else if x = y then EQ else GT)"
+
+definition
+  is_le :: "int lift \<rightarrow> int lift \<rightarrow> tr" where
+  "is_le = (\<Lambda> x y. case compare\<cdot>x\<cdot>y of LT \<Rightarrow> TT | EQ \<Rightarrow> TT | GT \<Rightarrow> FF)"
+
+definition
+  is_less :: "int lift \<rightarrow> int lift \<rightarrow> tr" where
+  "is_less = (\<Lambda> x y. case compare\<cdot>x\<cdot>y of LT \<Rightarrow> TT | EQ \<Rightarrow> FF | GT \<Rightarrow> FF)"
+
+definition
+  r1 :: "(int lift \<times> 'a) \<rightarrow> (int lift \<times> 'a) \<rightarrow> tr convex_pd" where
+  "r1 = (\<Lambda> \<langle>x,_\<rangle> \<langle>y,_\<rangle>. case compare\<cdot>x\<cdot>y of
+          LT \<Rightarrow> {TT}\<natural> |
+          EQ \<Rightarrow> {TT, FF}\<natural> |
+          GT \<Rightarrow> {FF}\<natural>)"
+
+definition
+  r2 :: "(int lift \<times> 'a) \<rightarrow> (int lift \<times> 'a) \<rightarrow> tr convex_pd" where
+  "r2 = (\<Lambda> \<langle>x,_\<rangle> \<langle>y,_\<rangle>. {is_le\<cdot>x\<cdot>y, is_less\<cdot>x\<cdot>y}\<natural>)"
+
+lemma r1_r2: "r1\<cdot>\<langle>x,a\<rangle>\<cdot>\<langle>y,b\<rangle> = (r2\<cdot>\<langle>x,a\<rangle>\<cdot>\<langle>y,b\<rangle> :: tr convex_pd)"
+apply (simp add: r1_def r2_def)
+apply (simp add: is_le_def is_less_def)
+apply (cases "compare\<cdot>x\<cdot>y" rule: ordering.casedist)
+apply simp_all
+done
+
+
+subsection {* Picking a leaf from a tree *}
+
+domain 'a tree =
+  Node (lazy "'a tree") (lazy "'a tree") |
+  Leaf (lazy "'a")
+
+consts
+  mirror :: "'a tree \<rightarrow> 'a tree"
+  pick :: "'a tree \<rightarrow> 'a convex_pd"
+
+fixrec
+  mirror_Leaf: "mirror\<cdot>(Leaf\<cdot>a) = Leaf\<cdot>a"
+  mirror_Node: "mirror\<cdot>(Node\<cdot>l\<cdot>r) = Node\<cdot>(mirror\<cdot>r)\<cdot>(mirror\<cdot>l)"
+
+fixpat
+  mirror_strict [simp]: "mirror\<cdot>\<bottom>"
+
+fixrec
+  pick_Leaf: "pick\<cdot>(Leaf\<cdot>a) = {a}\<natural>"
+  pick_Node: "pick\<cdot>(Node\<cdot>l\<cdot>r) = pick\<cdot>l +\<natural> pick\<cdot>r"
+
+fixpat
+  pick_strict [simp]: "pick\<cdot>\<bottom>"
+
+lemma pick_mirror: "pick\<cdot>(mirror\<cdot>t) = pick\<cdot>t"
+by (induct t rule: tree.ind)
+   (simp_all add: convex_plus_ac)
+
+consts
+  tree1 :: "int lift tree"
+  tree2 :: "int lift tree"
+  tree3 :: "int lift tree"
+
+fixrec
+  "tree1 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>(Leaf\<cdot>(Def 2)))
+               \<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))"
+
+fixrec
+  "tree2 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>(Leaf\<cdot>(Def 2)))
+               \<cdot>(Node\<cdot>\<bottom>\<cdot>(Leaf\<cdot>(Def 4)))"
+
+fixrec
+  "tree3 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>tree3)
+               \<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))"
+
+declare tree1_simps tree2_simps tree3_simps [simp del]
+
+lemma pick_tree1:
+  "pick\<cdot>tree1 = {Def 1, Def 2, Def 3, Def 4}\<natural>"
+apply (subst tree1_simps)
+apply simp
+apply (simp add: convex_plus_ac)
+done
+
+lemma pick_tree2:
+  "pick\<cdot>tree2 = {Def 1, Def 2, \<bottom>, Def 4}\<natural>"
+apply (subst tree2_simps)
+apply simp
+apply (simp add: convex_plus_ac)
+done
+
+lemma pick_tree3:
+  "pick\<cdot>tree3 = {Def 1, \<bottom>, Def 3, Def 4}\<natural>"
+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
diff -r c60ace776315 -r 5deee36e33c4 src/HOLCF/ex/ROOT.ML
--- a/src/HOLCF/ex/ROOT.ML	Thu Feb 19 08:07:52 2009 -0800
+++ b/src/HOLCF/ex/ROOT.ML	Thu Feb 19 09:39:49 2009 -0800
@@ -1,8 +1,7 @@
 (*  Title:      HOLCF/ex/ROOT.ML
-    ID:         $Id$
 
 Misc HOLCF examples.
 *)
 
 use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
-  "Loop", "Fixrec_ex"];
+  "Loop", "Fixrec_ex", "Powerdomain_ex"];