--- 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 \
--- /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
--- /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
--- 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
--- /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
--- /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
--- /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
--- /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
--- /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
--- 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 \