# HG changeset patch
# User huffman
# Date 1292131673 28800
# Node ID 866148b762470e4eaeb8fa6824a29845a70038da
# Parent  b497cc48e5638498bb5ad4ec1a1fe358bb2977a6
add HOLCF library theories with cpo/predomain instances for HOL types

diff -r b497cc48e563 -r 866148b76247 src/HOL/HOLCF/IsaMakefile
--- a/src/HOL/HOLCF/IsaMakefile	Sat Dec 11 11:26:37 2010 -0800
+++ b/src/HOL/HOLCF/IsaMakefile	Sat Dec 11 21:27:53 2010 -0800
@@ -104,7 +104,14 @@
 
 $(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
   Library/Defl_Bifinite.thy \
+  Library/Bool_Discrete.thy \
+  Library/Char_Discrete.thy \
+  Library/HOL_Cpo.thy \
+  Library/Int_Discrete.thy \
   Library/List_Cpo.thy \
+  Library/List_Predomain.thy \
+  Library/Nat_Discrete.thy \
+  Library/Option_Cpo.thy \
   Library/Stream.thy \
   Library/Sum_Cpo.thy \
   Library/HOLCF_Library.thy \
diff -r b497cc48e563 -r 866148b76247 src/HOL/HOLCF/Library/Bool_Discrete.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/Library/Bool_Discrete.thy	Sat Dec 11 21:27:53 2010 -0800
@@ -0,0 +1,71 @@
+(*  Title:      HOLCF/Library/Bool_Discrete.thy
+    Author:     Brian Huffman
+*)
+
+header {* Discrete cpo instance for booleans *}
+
+theory Bool_Discrete
+imports HOLCF
+begin
+
+text {* Discrete cpo instance for @{typ bool}. *}
+
+instantiation bool :: discrete_cpo
+begin
+
+definition below_bool_def:
+  "(x::bool) \<sqsubseteq> y \<longleftrightarrow> x = y"
+
+instance proof
+qed (rule below_bool_def)
+
+end
+
+text {*
+  TODO: implement a command to automate discrete predomain instances.
+*}
+
+instantiation bool :: predomain
+begin
+
+definition
+  "(liftemb :: bool u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
+
+definition
+  "(liftprj :: udom \<rightarrow> bool u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
+
+definition
+  "liftdefl \<equiv> (\<lambda>(t::bool itself). LIFTDEFL(bool discr))"
+
+instance proof
+  show "ep_pair liftemb (liftprj :: udom \<rightarrow> bool u)"
+    unfolding liftemb_bool_def liftprj_bool_def
+    apply (rule ep_pair_comp)
+    apply (rule ep_pair_u_map)
+    apply (simp add: ep_pair.intro)
+    apply (rule predomain_ep)
+    done
+  show "cast\<cdot>LIFTDEFL(bool) = liftemb oo (liftprj :: udom \<rightarrow> bool u)"
+    unfolding liftemb_bool_def liftprj_bool_def liftdefl_bool_def
+    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
+    apply (simp add: ID_def [symmetric] u_map_ID)
+    done
+qed
+
+end
+
+lemma cont2cont_if [simp, cont2cont]:
+  assumes b: "cont b" and f: "cont f" and g: "cont g"
+  shows "cont (\<lambda>x. if b x then f x else g x)"
+by (rule cont_apply [OF b cont_discrete_cpo], simp add: f g)
+
+lemma cont2cont_eq [simp, cont2cont]:
+  fixes f g :: "'a::cpo \<Rightarrow> 'b::discrete_cpo"
+  assumes f: "cont f" and g: "cont g"
+  shows "cont (\<lambda>x. f x = g x)"
+apply (rule cont_apply [OF f cont_discrete_cpo])
+apply (rule cont_apply [OF g cont_discrete_cpo])
+apply (rule cont_const)
+done
+
+end
diff -r b497cc48e563 -r 866148b76247 src/HOL/HOLCF/Library/Char_Discrete.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/Library/Char_Discrete.thy	Sat Dec 11 21:27:53 2010 -0800
@@ -0,0 +1,245 @@
+(*  Title:      HOLCF/Library/Char_Discrete.thy
+    Author:     Brian Huffman
+*)
+
+header {* Discrete cpo instance for 8-bit char type *}
+
+theory Char_Discrete
+imports HOLCF
+begin
+
+subsection {* Discrete cpo instance for @{typ nibble}. *}
+
+instantiation nibble :: discrete_cpo
+begin
+
+definition below_nibble_def:
+  "(x::nibble) \<sqsubseteq> y \<longleftrightarrow> x = y"
+
+instance proof
+qed (rule below_nibble_def)
+
+end
+
+text {*
+  TODO: implement a command to automate discrete predomain instances.
+*}
+
+instantiation nibble :: predomain
+begin
+
+definition
+  "(liftemb :: nibble u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
+
+definition
+  "(liftprj :: udom \<rightarrow> nibble u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
+
+definition
+  "liftdefl \<equiv> (\<lambda>(t::nibble itself). LIFTDEFL(nibble discr))"
+
+instance proof
+  show "ep_pair liftemb (liftprj :: udom \<rightarrow> nibble u)"
+    unfolding liftemb_nibble_def liftprj_nibble_def
+    apply (rule ep_pair_comp)
+    apply (rule ep_pair_u_map)
+    apply (simp add: ep_pair.intro)
+    apply (rule predomain_ep)
+    done
+  show "cast\<cdot>LIFTDEFL(nibble) = liftemb oo (liftprj :: udom \<rightarrow> nibble u)"
+    unfolding liftemb_nibble_def liftprj_nibble_def liftdefl_nibble_def
+    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
+    apply (simp add: ID_def [symmetric] u_map_ID)
+    done
+qed
+
+end
+
+subsection {* Discrete cpo instance for @{typ char}. *}
+
+instantiation char :: discrete_cpo
+begin
+
+definition below_char_def:
+  "(x::char) \<sqsubseteq> y \<longleftrightarrow> x = y"
+
+instance proof
+qed (rule below_char_def)
+
+end
+
+text {*
+  TODO: implement a command to automate discrete predomain instances.
+*}
+
+instantiation char :: predomain
+begin
+
+definition
+  "(liftemb :: char u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
+
+definition
+  "(liftprj :: udom \<rightarrow> char u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
+
+definition
+  "liftdefl \<equiv> (\<lambda>(t::char itself). LIFTDEFL(char discr))"
+
+instance proof
+  show "ep_pair liftemb (liftprj :: udom \<rightarrow> char u)"
+    unfolding liftemb_char_def liftprj_char_def
+    apply (rule ep_pair_comp)
+    apply (rule ep_pair_u_map)
+    apply (simp add: ep_pair.intro)
+    apply (rule predomain_ep)
+    done
+  show "cast\<cdot>LIFTDEFL(char) = liftemb oo (liftprj :: udom \<rightarrow> char u)"
+    unfolding liftemb_char_def liftprj_char_def liftdefl_char_def
+    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
+    apply (simp add: ID_def [symmetric] u_map_ID)
+    done
+qed
+
+end
+
+subsection {* Using chars with Fixrec *}
+
+definition match_Char :: "char \<rightarrow> (nibble \<rightarrow> nibble \<rightarrow> 'a match) \<rightarrow> 'a match"
+  where "match_Char = (\<Lambda> c k. case c of Char a b \<Rightarrow> k\<cdot>a\<cdot>b)"
+
+lemma match_Char_simps [simp]:
+  "match_Char\<cdot>(Char a b)\<cdot>k = k\<cdot>a\<cdot>b"
+by (simp add: match_Char_def)
+
+definition match_Nibble0 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_Nibble0 = (\<Lambda> c k. if c = Nibble0 then k else Fixrec.fail)"
+
+definition match_Nibble1 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_Nibble1 = (\<Lambda> c k. if c = Nibble1 then k else Fixrec.fail)"
+
+definition match_Nibble2 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_Nibble2 = (\<Lambda> c k. if c = Nibble2 then k else Fixrec.fail)"
+
+definition match_Nibble3 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_Nibble3 = (\<Lambda> c k. if c = Nibble3 then k else Fixrec.fail)"
+
+definition match_Nibble4 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_Nibble4 = (\<Lambda> c k. if c = Nibble4 then k else Fixrec.fail)"
+
+definition match_Nibble5 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_Nibble5 = (\<Lambda> c k. if c = Nibble5 then k else Fixrec.fail)"
+
+definition match_Nibble6 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_Nibble6 = (\<Lambda> c k. if c = Nibble6 then k else Fixrec.fail)"
+
+definition match_Nibble7 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_Nibble7 = (\<Lambda> c k. if c = Nibble7 then k else Fixrec.fail)"
+
+definition match_Nibble8 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_Nibble8 = (\<Lambda> c k. if c = Nibble8 then k else Fixrec.fail)"
+
+definition match_Nibble9 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_Nibble9 = (\<Lambda> c k. if c = Nibble9 then k else Fixrec.fail)"
+
+definition match_NibbleA :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_NibbleA = (\<Lambda> c k. if c = NibbleA then k else Fixrec.fail)"
+
+definition match_NibbleB :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_NibbleB = (\<Lambda> c k. if c = NibbleB then k else Fixrec.fail)"
+
+definition match_NibbleC :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_NibbleC = (\<Lambda> c k. if c = NibbleC then k else Fixrec.fail)"
+
+definition match_NibbleD :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_NibbleD = (\<Lambda> c k. if c = NibbleD then k else Fixrec.fail)"
+
+definition match_NibbleE :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_NibbleE = (\<Lambda> c k. if c = NibbleE then k else Fixrec.fail)"
+
+definition match_NibbleF :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
+  where "match_NibbleF = (\<Lambda> c k. if c = NibbleF then k else Fixrec.fail)"
+
+lemma match_Nibble0_simps [simp]:
+  "match_Nibble0\<cdot>c\<cdot>k = (if c = Nibble0 then k else Fixrec.fail)"
+by (simp add: match_Nibble0_def)
+
+lemma match_Nibble1_simps [simp]:
+  "match_Nibble1\<cdot>c\<cdot>k = (if c = Nibble1 then k else Fixrec.fail)"
+by (simp add: match_Nibble1_def)
+
+lemma match_Nibble2_simps [simp]:
+  "match_Nibble2\<cdot>c\<cdot>k = (if c = Nibble2 then k else Fixrec.fail)"
+by (simp add: match_Nibble2_def)
+
+lemma match_Nibble3_simps [simp]:
+  "match_Nibble3\<cdot>c\<cdot>k = (if c = Nibble3 then k else Fixrec.fail)"
+by (simp add: match_Nibble3_def)
+
+lemma match_Nibble4_simps [simp]:
+  "match_Nibble4\<cdot>c\<cdot>k = (if c = Nibble4 then k else Fixrec.fail)"
+by (simp add: match_Nibble4_def)
+
+lemma match_Nibble5_simps [simp]:
+  "match_Nibble5\<cdot>c\<cdot>k = (if c = Nibble5 then k else Fixrec.fail)"
+by (simp add: match_Nibble5_def)
+
+lemma match_Nibble6_simps [simp]:
+  "match_Nibble6\<cdot>c\<cdot>k = (if c = Nibble6 then k else Fixrec.fail)"
+by (simp add: match_Nibble6_def)
+
+lemma match_Nibble7_simps [simp]:
+  "match_Nibble7\<cdot>c\<cdot>k = (if c = Nibble7 then k else Fixrec.fail)"
+by (simp add: match_Nibble7_def)
+
+lemma match_Nibble8_simps [simp]:
+  "match_Nibble8\<cdot>c\<cdot>k = (if c = Nibble8 then k else Fixrec.fail)"
+by (simp add: match_Nibble8_def)
+
+lemma match_Nibble9_simps [simp]:
+  "match_Nibble9\<cdot>c\<cdot>k = (if c = Nibble9 then k else Fixrec.fail)"
+by (simp add: match_Nibble9_def)
+
+lemma match_NibbleA_simps [simp]:
+  "match_NibbleA\<cdot>c\<cdot>k = (if c = NibbleA then k else Fixrec.fail)"
+by (simp add: match_NibbleA_def)
+
+lemma match_NibbleB_simps [simp]:
+  "match_NibbleB\<cdot>c\<cdot>k = (if c = NibbleB then k else Fixrec.fail)"
+by (simp add: match_NibbleB_def)
+
+lemma match_NibbleC_simps [simp]:
+  "match_NibbleC\<cdot>c\<cdot>k = (if c = NibbleC then k else Fixrec.fail)"
+by (simp add: match_NibbleC_def)
+
+lemma match_NibbleD_simps [simp]:
+  "match_NibbleD\<cdot>c\<cdot>k = (if c = NibbleD then k else Fixrec.fail)"
+by (simp add: match_NibbleD_def)
+
+lemma match_NibbleE_simps [simp]:
+  "match_NibbleE\<cdot>c\<cdot>k = (if c = NibbleE then k else Fixrec.fail)"
+by (simp add: match_NibbleE_def)
+
+lemma match_NibbleF_simps [simp]:
+  "match_NibbleF\<cdot>c\<cdot>k = (if c = NibbleF then k else Fixrec.fail)"
+by (simp add: match_NibbleF_def)
+
+setup {*
+  Fixrec.add_matchers
+    [ (@{const_name Char}, @{const_name match_Char}),
+      (@{const_name Nibble0}, @{const_name match_Nibble0}),
+      (@{const_name Nibble1}, @{const_name match_Nibble1}),
+      (@{const_name Nibble2}, @{const_name match_Nibble2}),
+      (@{const_name Nibble3}, @{const_name match_Nibble3}),
+      (@{const_name Nibble4}, @{const_name match_Nibble4}),
+      (@{const_name Nibble5}, @{const_name match_Nibble5}),
+      (@{const_name Nibble6}, @{const_name match_Nibble6}),
+      (@{const_name Nibble7}, @{const_name match_Nibble7}),
+      (@{const_name Nibble8}, @{const_name match_Nibble8}),
+      (@{const_name Nibble9}, @{const_name match_Nibble9}),
+      (@{const_name NibbleA}, @{const_name match_NibbleA}),
+      (@{const_name NibbleB}, @{const_name match_NibbleB}),
+      (@{const_name NibbleC}, @{const_name match_NibbleC}),
+      (@{const_name NibbleD}, @{const_name match_NibbleD}),
+      (@{const_name NibbleE}, @{const_name match_NibbleE}),
+      (@{const_name NibbleF}, @{const_name match_NibbleF}) ]
+*}
+
+end
diff -r b497cc48e563 -r 866148b76247 src/HOL/HOLCF/Library/HOLCF_Library.thy
--- a/src/HOL/HOLCF/Library/HOLCF_Library.thy	Sat Dec 11 11:26:37 2010 -0800
+++ b/src/HOL/HOLCF/Library/HOLCF_Library.thy	Sat Dec 11 21:27:53 2010 -0800
@@ -1,7 +1,13 @@
 theory HOLCF_Library
 imports
+  Bool_Discrete
+  Char_Discrete
   Defl_Bifinite
+  Int_Discrete
   List_Cpo
+  List_Predomain
+  Nat_Discrete
+  Option_Cpo
   Stream
   Sum_Cpo
 begin
diff -r b497cc48e563 -r 866148b76247 src/HOL/HOLCF/Library/HOL_Cpo.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/Library/HOL_Cpo.thy	Sat Dec 11 21:27:53 2010 -0800
@@ -0,0 +1,18 @@
+(*  Title:      HOLCF/HOL_Cpo.thy
+    Author:     Brian Huffman
+*)
+
+header {* Cpo class instances for all HOL types *}
+
+theory HOL_Cpo
+imports
+  Bool_Discrete
+  Nat_Discrete
+  Int_Discrete
+  Char_Discrete
+  Sum_Cpo
+  Option_Cpo
+  List_Predomain
+begin
+
+end
diff -r b497cc48e563 -r 866148b76247 src/HOL/HOLCF/Library/Int_Discrete.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/Library/Int_Discrete.thy	Sat Dec 11 21:27:53 2010 -0800
@@ -0,0 +1,57 @@
+(*  Title:      HOLCF/Library/Int_Discrete.thy
+    Author:     Brian Huffman
+*)
+
+header {* Discrete cpo instance for integers *}
+
+theory Int_Discrete
+imports HOLCF
+begin
+
+text {* Discrete cpo instance for @{typ int}. *}
+
+instantiation int :: discrete_cpo
+begin
+
+definition below_int_def:
+  "(x::int) \<sqsubseteq> y \<longleftrightarrow> x = y"
+
+instance proof
+qed (rule below_int_def)
+
+end
+
+text {*
+  TODO: implement a command to automate discrete predomain instances.
+*}
+
+instantiation int :: predomain
+begin
+
+definition
+  "(liftemb :: int u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
+
+definition
+  "(liftprj :: udom \<rightarrow> int u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
+
+definition
+  "liftdefl \<equiv> (\<lambda>(t::int itself). LIFTDEFL(int discr))"
+
+instance proof
+  show "ep_pair liftemb (liftprj :: udom \<rightarrow> int u)"
+    unfolding liftemb_int_def liftprj_int_def
+    apply (rule ep_pair_comp)
+    apply (rule ep_pair_u_map)
+    apply (simp add: ep_pair.intro)
+    apply (rule predomain_ep)
+    done
+  show "cast\<cdot>LIFTDEFL(int) = liftemb oo (liftprj :: udom \<rightarrow> int u)"
+    unfolding liftemb_int_def liftprj_int_def liftdefl_int_def
+    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
+    apply (simp add: ID_def [symmetric] u_map_ID)
+    done
+qed
+
+end
+
+end
diff -r b497cc48e563 -r 866148b76247 src/HOL/HOLCF/Library/List_Predomain.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/Library/List_Predomain.thy	Sat Dec 11 21:27:53 2010 -0800
@@ -0,0 +1,128 @@
+(*  Title:      HOLCF/Library/List_Predomain.thy
+    Author:     Brian Huffman
+*)
+
+header {* Predomain class instance for HOL list type *}
+
+theory List_Predomain
+imports List_Cpo
+begin
+
+subsection {* Strict list type *}
+
+domain 'a slist = SNil | SCons "'a" "'a slist"
+
+text {*
+  Types @{typ "'a list u"}. and @{typ "'a u slist"} are isomorphic.
+*}
+
+fixrec encode_list_u where
+  "encode_list_u\<cdot>(up\<cdot>[]) = SNil" |
+  "encode_list_u\<cdot>(up\<cdot>(x # xs)) = SCons\<cdot>(up\<cdot>x)\<cdot>(encode_list_u\<cdot>(up\<cdot>xs))"
+
+lemma encode_list_u_strict [simp]: "encode_list_u\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
+
+lemma encode_list_u_bottom_iff [simp]:
+  "encode_list_u\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
+apply (induct x, simp_all)
+apply (rename_tac xs, induct_tac xs, simp_all)
+done
+
+fixrec decode_list_u where
+  "decode_list_u\<cdot>SNil = up\<cdot>[]" |
+  "ys \<noteq> \<bottom> \<Longrightarrow> decode_list_u\<cdot>(SCons\<cdot>(up\<cdot>x)\<cdot>ys) =
+    (case decode_list_u\<cdot>ys of up\<cdot>xs \<Rightarrow> up\<cdot>(x # xs))"
+
+lemma decode_list_u_strict [simp]: "decode_list_u\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
+
+lemma decode_encode_list_u [simp]: "decode_list_u\<cdot>(encode_list_u\<cdot>x) = x"
+by (induct x, simp, rename_tac xs, induct_tac xs, simp_all)
+
+lemma encode_decode_list_u [simp]: "encode_list_u\<cdot>(decode_list_u\<cdot>y) = y"
+apply (induct y, simp, simp)
+apply (case_tac a, simp)
+apply (case_tac "decode_list_u\<cdot>y", simp, simp)
+done
+
+subsection {* Lists are a predomain *}
+
+instantiation list :: (predomain) predomain
+begin
+
+definition
+  "liftemb = emb oo encode_list_u"
+
+definition
+  "liftprj = decode_list_u oo prj"
+
+definition
+  "liftdefl (t::('a list) itself) = DEFL(('a\<^sub>\<bottom>) slist)"
+
+instance proof
+  have "ep_pair encode_list_u decode_list_u"
+    by (rule ep_pair.intro, simp_all)
+  thus "ep_pair liftemb (liftprj :: udom \<rightarrow> ('a list) u)"
+    unfolding liftemb_list_def liftprj_list_def
+    using ep_pair_emb_prj by (rule ep_pair_comp)
+  show "cast\<cdot>LIFTDEFL('a list) = liftemb oo (liftprj :: udom \<rightarrow> ('a list) u)"
+    unfolding liftemb_list_def liftprj_list_def liftdefl_list_def
+    by (simp add: cfcomp1 cast_DEFL)
+qed
+
+end
+
+lemma liftdefl_list [domain_defl_simps]:
+  "LIFTDEFL('a::predomain list) = slist_defl\<cdot>LIFTDEFL('a)"
+unfolding liftdefl_list_def by (simp add: domain_defl_simps)
+
+subsection {* Continuous map operation for lists *}
+
+definition
+  list_map :: "('a::predomain \<rightarrow> 'b::predomain) \<rightarrow> 'a list \<rightarrow> 'b list"
+where
+  "list_map = (\<Lambda> f xs. map (\<lambda>x. f\<cdot>x) xs)"
+
+lemma list_map_simps [simp]:
+  "list_map\<cdot>f\<cdot>[] = []"
+  "list_map\<cdot>f\<cdot>(x # xs) = f\<cdot>x # list_map\<cdot>f\<cdot>xs"
+unfolding list_map_def by simp_all
+
+lemma list_map_ID [domain_map_ID]: "list_map\<cdot>ID = ID"
+unfolding list_map_def ID_def
+by (simp add: Abs_cfun_inverse cfun_def)
+
+lemma deflation_list_map [domain_deflation]:
+  "deflation d \<Longrightarrow> deflation (list_map\<cdot>d)"
+apply default
+apply (induct_tac x, simp_all add: deflation.idem)
+apply (induct_tac x, simp_all add: deflation.below)
+done
+
+subsection {* Configuring list type to work with domain package *}
+
+lemma encode_list_u_map:
+  "encode_list_u\<cdot>(u_map\<cdot>(list_map\<cdot>f)\<cdot>(decode_list_u\<cdot>xs))
+    = slist_map\<cdot>(u_map\<cdot>f)\<cdot>xs"
+apply (induct xs)
+apply (simp, subst slist_map_unfold, simp)
+apply (simp, subst slist_map_unfold, simp add: SNil_def)
+apply (case_tac a, simp, rename_tac b)
+apply (case_tac "decode_list_u\<cdot>xs")
+apply (drule_tac f="encode_list_u" in cfun_arg_cong, simp)
+by (simp, subst slist_map_unfold, simp add: SCons_def)
+
+lemma isodefl_list_u [domain_isodefl]:
+  fixes d :: "'a::predomain \<rightarrow> 'a"
+  assumes "isodefl (u_map\<cdot>d) t"
+  shows "isodefl (u_map\<cdot>(list_map\<cdot>d)) (slist_defl\<cdot>t)"
+using assms [THEN isodefl_slist] unfolding isodefl_def
+unfolding emb_u_def prj_u_def liftemb_list_def liftprj_list_def
+by (simp add: cfcomp1 encode_list_u_map)
+
+setup {*
+  Domain_Take_Proofs.add_rec_type (@{type_name "list"}, [true])
+*}
+
+end
diff -r b497cc48e563 -r 866148b76247 src/HOL/HOLCF/Library/Nat_Discrete.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/Library/Nat_Discrete.thy	Sat Dec 11 21:27:53 2010 -0800
@@ -0,0 +1,57 @@
+(*  Title:      HOLCF/Library/Nat_Discrete.thy
+    Author:     Brian Huffman
+*)
+
+header {* Discrete cpo instance for naturals *}
+
+theory Nat_Discrete
+imports HOLCF
+begin
+
+text {* Discrete cpo instance for @{typ nat}. *}
+
+instantiation nat :: discrete_cpo
+begin
+
+definition below_nat_def:
+  "(x::nat) \<sqsubseteq> y \<longleftrightarrow> x = y"
+
+instance proof
+qed (rule below_nat_def)
+
+end
+
+text {*
+  TODO: implement a command to automate discrete predomain instances.
+*}
+
+instantiation nat :: predomain
+begin
+
+definition
+  "(liftemb :: nat u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
+
+definition
+  "(liftprj :: udom \<rightarrow> nat u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
+
+definition
+  "liftdefl \<equiv> (\<lambda>(t::nat itself). LIFTDEFL(nat discr))"
+
+instance proof
+  show "ep_pair liftemb (liftprj :: udom \<rightarrow> nat u)"
+    unfolding liftemb_nat_def liftprj_nat_def
+    apply (rule ep_pair_comp)
+    apply (rule ep_pair_u_map)
+    apply (simp add: ep_pair.intro)
+    apply (rule predomain_ep)
+    done
+  show "cast\<cdot>LIFTDEFL(nat) = liftemb oo (liftprj :: udom \<rightarrow> nat u)"
+    unfolding liftemb_nat_def liftprj_nat_def liftdefl_nat_def
+    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
+    apply (simp add: ID_def [symmetric] u_map_ID)
+    done
+qed
+
+end
+
+end
diff -r b497cc48e563 -r 866148b76247 src/HOL/HOLCF/Library/Option_Cpo.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/Library/Option_Cpo.thy	Sat Dec 11 21:27:53 2010 -0800
@@ -0,0 +1,255 @@
+(*  Title:      HOLCF/Option_Cpo.thy
+    Author:     Brian Huffman
+*)
+
+header {* Cpo class instance for HOL option type *}
+
+theory Option_Cpo
+imports HOLCF
+begin
+
+subsection {* Ordering on option type *}
+
+instantiation option :: (below) below
+begin
+
+definition below_option_def:
+  "x \<sqsubseteq> y \<equiv> case x of
+         None \<Rightarrow> (case y of None \<Rightarrow> True | Some b \<Rightarrow> False) |
+         Some a \<Rightarrow> (case y of None \<Rightarrow> False | Some b \<Rightarrow> a \<sqsubseteq> b)"
+
+instance ..
+end
+
+lemma None_below_None [simp]: "None \<sqsubseteq> None"
+unfolding below_option_def by simp
+
+lemma Some_below_Some [simp]: "Some x \<sqsubseteq> Some y \<longleftrightarrow> x \<sqsubseteq> y"
+unfolding below_option_def by simp
+
+lemma Some_below_None [simp]: "\<not> Some x \<sqsubseteq> None"
+unfolding below_option_def by simp
+
+lemma None_below_Some [simp]: "\<not> None \<sqsubseteq> Some y"
+unfolding below_option_def by simp
+
+lemma Some_mono: "x \<sqsubseteq> y \<Longrightarrow> Some x \<sqsubseteq> Some y"
+by simp
+
+lemma None_below_iff [simp]: "None \<sqsubseteq> x \<longleftrightarrow> x = None"
+by (cases x, simp_all)
+
+lemma below_None_iff [simp]: "x \<sqsubseteq> None \<longleftrightarrow> x = None"
+by (cases x, simp_all)
+
+lemma option_below_cases:
+  assumes "x \<sqsubseteq> y"
+  obtains "x = None" and "y = None"
+  | a b where "x = Some a" and "y = Some b" and "a \<sqsubseteq> b"
+using assms unfolding below_option_def
+by (simp split: option.split_asm)
+
+subsection {* Option type is a complete partial order *}
+
+instance option :: (po) po
+proof
+  fix x :: "'a option"
+  show "x \<sqsubseteq> x"
+    unfolding below_option_def
+    by (simp split: option.split)
+next
+  fix x y :: "'a option"
+  assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
+    unfolding below_option_def
+    by (auto split: option.split_asm intro: below_antisym)
+next
+  fix x y z :: "'a option"
+  assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
+    unfolding below_option_def
+    by (auto split: option.split_asm intro: below_trans)
+qed
+
+lemma monofun_the: "monofun the"
+by (rule monofunI, erule option_below_cases, simp_all)
+
+lemma option_chain_cases:
+  assumes Y: "chain Y"
+  obtains "Y = (\<lambda>i. None)" | A where "chain A" and "Y = (\<lambda>i. Some (A i))"
+ apply (cases "Y 0")
+  apply (rule that(1))
+  apply (rule ext)
+  apply (cut_tac j=i in chain_mono [OF Y le0], simp)
+ apply (rule that(2))
+  apply (rule ch2ch_monofun [OF monofun_the Y])
+ apply (rule ext)
+ apply (cut_tac j=i in chain_mono [OF Y le0], simp)
+ apply (case_tac "Y i", simp_all)
+done
+
+lemma is_lub_Some: "range S <<| x \<Longrightarrow> range (\<lambda>i. Some (S i)) <<| Some x"
+ apply (rule is_lubI)
+  apply (rule ub_rangeI)
+  apply (simp add: is_lub_rangeD1)
+ apply (frule ub_rangeD [where i=arbitrary])
+ apply (case_tac u, simp_all)
+ apply (erule is_lubD2)
+ apply (rule ub_rangeI)
+ apply (drule ub_rangeD, simp)
+done
+
+instance option :: (cpo) cpo
+ apply intro_classes
+ apply (erule option_chain_cases, safe)
+  apply (rule exI, rule is_lub_const)
+ apply (rule exI)
+ apply (rule is_lub_Some)
+ apply (erule cpo_lubI)
+done
+
+subsection {* Continuity of Some and case function *}
+
+lemma cont_Some: "cont Some"
+by (intro contI is_lub_Some cpo_lubI)
+
+lemmas cont2cont_Some [simp, cont2cont] = cont_compose [OF cont_Some]
+
+lemmas ch2ch_Some [simp] = ch2ch_cont [OF cont_Some]
+
+lemmas lub_Some = cont2contlubE [OF cont_Some, symmetric]
+
+lemma cont2cont_option_case:
+  assumes f: "cont (\<lambda>x. f x)"
+  assumes g: "cont (\<lambda>x. g x)"
+  assumes h1: "\<And>a. cont (\<lambda>x. h x a)"
+  assumes h2: "\<And>x. cont (\<lambda>a. h x a)"
+  shows "cont (\<lambda>x. case f x of None \<Rightarrow> g x | Some a \<Rightarrow> h x a)"
+apply (rule cont_apply [OF f])
+apply (rule contI)
+apply (erule option_chain_cases)
+apply (simp add: is_lub_const)
+apply (simp add: lub_Some)
+apply (simp add: cont2contlubE [OF h2])
+apply (rule cpo_lubI, rule chainI)
+apply (erule cont2monofunE [OF h2 chainE])
+apply (case_tac y, simp_all add: g h1)
+done
+
+lemma cont2cont_option_case' [simp, cont2cont]:
+  assumes f: "cont (\<lambda>x. f x)"
+  assumes g: "cont (\<lambda>x. g x)"
+  assumes h: "cont (\<lambda>p. h (fst p) (snd p))"
+  shows "cont (\<lambda>x. case f x of None \<Rightarrow> g x | Some a \<Rightarrow> h x a)"
+using assms by (simp add: cont2cont_option_case prod_cont_iff)
+
+text {* Simple version for when the element type is not a cpo. *}
+
+lemma cont2cont_option_case_simple [simp, cont2cont]:
+  assumes "cont (\<lambda>x. f x)"
+  assumes "\<And>a. cont (\<lambda>x. g x a)"
+  shows "cont (\<lambda>x. case z of None \<Rightarrow> f x | Some a \<Rightarrow> g x a)"
+using assms by (cases z) auto
+
+subsection {* Compactness and chain-finiteness *}
+
+lemma compact_None [simp]: "compact None"
+apply (rule compactI2)
+apply (erule option_chain_cases, safe)
+apply simp
+apply (simp add: lub_Some)
+done
+
+lemma compact_Some: "compact a \<Longrightarrow> compact (Some a)"
+apply (rule compactI2)
+apply (erule option_chain_cases, safe)
+apply simp
+apply (simp add: lub_Some)
+apply (erule (2) compactD2)
+done
+
+lemma compact_Some_rev: "compact (Some a) \<Longrightarrow> compact a"
+unfolding compact_def
+by (drule adm_subst [OF cont_Some], simp)
+
+lemma compact_Some_iff [simp]: "compact (Some a) = compact a"
+by (safe elim!: compact_Some compact_Some_rev)
+
+instance option :: (chfin) chfin
+apply intro_classes
+apply (erule compact_imp_max_in_chain)
+apply (case_tac "\<Squnion>i. Y i", simp_all)
+done
+
+instance option :: (discrete_cpo) discrete_cpo
+by intro_classes (simp add: below_option_def split: option.split)
+
+subsection {* Using option types with fixrec *}
+
+definition
+  "match_None = (\<Lambda> x k. case x of None \<Rightarrow> k | Some a \<Rightarrow> Fixrec.fail)"
+
+definition
+  "match_Some = (\<Lambda> x k. case x of None \<Rightarrow> Fixrec.fail | Some a \<Rightarrow> k\<cdot>a)"
+
+lemma match_None_simps [simp]:
+  "match_None\<cdot>None\<cdot>k = k"
+  "match_None\<cdot>(Some a)\<cdot>k = Fixrec.fail"
+unfolding match_None_def by simp_all
+
+lemma match_Some_simps [simp]:
+  "match_Some\<cdot>None\<cdot>k = Fixrec.fail"
+  "match_Some\<cdot>(Some a)\<cdot>k = k\<cdot>a"
+unfolding match_Some_def by simp_all
+
+setup {*
+  Fixrec.add_matchers
+    [ (@{const_name None}, @{const_name match_None}),
+      (@{const_name Some}, @{const_name match_Some}) ]
+*}
+
+subsection {* Option type is a predomain *}
+
+definition
+  "encode_option_u =
+    (\<Lambda>(up\<cdot>x). case x of None \<Rightarrow> sinl\<cdot>ONE | Some a \<Rightarrow> sinr\<cdot>(up\<cdot>a))"
+
+definition
+  "decode_option_u = sscase\<cdot>(\<Lambda> ONE. up\<cdot>None)\<cdot>(\<Lambda>(up\<cdot>a). up\<cdot>(Some a))"
+
+lemma decode_encode_option_u [simp]: "decode_option_u\<cdot>(encode_option_u\<cdot>x) = x"
+unfolding decode_option_u_def encode_option_u_def
+by (case_tac x, simp, rename_tac y, case_tac y, simp_all)
+
+lemma encode_decode_option_u [simp]: "encode_option_u\<cdot>(decode_option_u\<cdot>x) = x"
+unfolding decode_option_u_def encode_option_u_def
+apply (case_tac x, simp)
+apply (rename_tac a, case_tac a rule: oneE, simp, simp)
+apply (rename_tac b, case_tac b, simp, simp)
+done
+
+instantiation option :: (predomain) predomain
+begin
+
+definition
+  "liftemb = emb oo encode_option_u"
+
+definition
+  "liftprj = decode_option_u oo prj"
+
+definition
+  "liftdefl (t::('a option) itself) = DEFL(one \<oplus> 'a u)"
+
+instance proof
+  show "ep_pair liftemb (liftprj :: udom \<rightarrow> ('a option) u)"
+    unfolding liftemb_option_def liftprj_option_def
+    apply (rule ep_pair_comp)
+    apply (rule ep_pair.intro, simp, simp)
+    apply (rule ep_pair_emb_prj)
+    done
+  show "cast\<cdot>LIFTDEFL('a option) = liftemb oo (liftprj :: udom \<rightarrow> ('a option) u)"
+    unfolding liftemb_option_def liftprj_option_def liftdefl_option_def
+    by (simp add: cast_DEFL cfcomp1)
+qed
+
+end
+
+end
diff -r b497cc48e563 -r 866148b76247 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat Dec 11 11:26:37 2010 -0800
+++ b/src/HOL/IsaMakefile	Sat Dec 11 21:27:53 2010 -0800
@@ -1471,7 +1471,14 @@
 
 $(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
   HOLCF/Library/Defl_Bifinite.thy \
+  HOLCF/Library/Bool_Discrete.thy \
+  HOLCF/Library/Char_Discrete.thy \
+  HOLCF/Library/HOL_Cpo.thy \
+  HOLCF/Library/Int_Discrete.thy \
   HOLCF/Library/List_Cpo.thy \
+  HOLCF/Library/List_Predomain.thy \
+  HOLCF/Library/Nat_Discrete.thy \
+  HOLCF/Library/Option_Cpo.thy \
   HOLCF/Library/Stream.thy \
   HOLCF/Library/Sum_Cpo.thy \
   HOLCF/Library/HOLCF_Library.thy \