add HOLCF library theories with cpo/predomain instances for HOL types
authorhuffman
Sat Dec 11 21:27:53 2010 -0800 (2010-12-11)
changeset 41112866148b76247
parent 41111 b497cc48e563
child 41113 b223fa19af3c
add HOLCF library theories with cpo/predomain instances for HOL types
src/HOL/HOLCF/IsaMakefile
src/HOL/HOLCF/Library/Bool_Discrete.thy
src/HOL/HOLCF/Library/Char_Discrete.thy
src/HOL/HOLCF/Library/HOLCF_Library.thy
src/HOL/HOLCF/Library/HOL_Cpo.thy
src/HOL/HOLCF/Library/Int_Discrete.thy
src/HOL/HOLCF/Library/List_Predomain.thy
src/HOL/HOLCF/Library/Nat_Discrete.thy
src/HOL/HOLCF/Library/Option_Cpo.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/HOLCF/IsaMakefile	Sat Dec 11 11:26:37 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/IsaMakefile	Sat Dec 11 21:27:53 2010 -0800
     1.3 @@ -104,7 +104,14 @@
     1.4  
     1.5  $(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
     1.6    Library/Defl_Bifinite.thy \
     1.7 +  Library/Bool_Discrete.thy \
     1.8 +  Library/Char_Discrete.thy \
     1.9 +  Library/HOL_Cpo.thy \
    1.10 +  Library/Int_Discrete.thy \
    1.11    Library/List_Cpo.thy \
    1.12 +  Library/List_Predomain.thy \
    1.13 +  Library/Nat_Discrete.thy \
    1.14 +  Library/Option_Cpo.thy \
    1.15    Library/Stream.thy \
    1.16    Library/Sum_Cpo.thy \
    1.17    Library/HOLCF_Library.thy \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/HOLCF/Library/Bool_Discrete.thy	Sat Dec 11 21:27:53 2010 -0800
     2.3 @@ -0,0 +1,71 @@
     2.4 +(*  Title:      HOLCF/Library/Bool_Discrete.thy
     2.5 +    Author:     Brian Huffman
     2.6 +*)
     2.7 +
     2.8 +header {* Discrete cpo instance for booleans *}
     2.9 +
    2.10 +theory Bool_Discrete
    2.11 +imports HOLCF
    2.12 +begin
    2.13 +
    2.14 +text {* Discrete cpo instance for @{typ bool}. *}
    2.15 +
    2.16 +instantiation bool :: discrete_cpo
    2.17 +begin
    2.18 +
    2.19 +definition below_bool_def:
    2.20 +  "(x::bool) \<sqsubseteq> y \<longleftrightarrow> x = y"
    2.21 +
    2.22 +instance proof
    2.23 +qed (rule below_bool_def)
    2.24 +
    2.25 +end
    2.26 +
    2.27 +text {*
    2.28 +  TODO: implement a command to automate discrete predomain instances.
    2.29 +*}
    2.30 +
    2.31 +instantiation bool :: predomain
    2.32 +begin
    2.33 +
    2.34 +definition
    2.35 +  "(liftemb :: bool u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
    2.36 +
    2.37 +definition
    2.38 +  "(liftprj :: udom \<rightarrow> bool u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
    2.39 +
    2.40 +definition
    2.41 +  "liftdefl \<equiv> (\<lambda>(t::bool itself). LIFTDEFL(bool discr))"
    2.42 +
    2.43 +instance proof
    2.44 +  show "ep_pair liftemb (liftprj :: udom \<rightarrow> bool u)"
    2.45 +    unfolding liftemb_bool_def liftprj_bool_def
    2.46 +    apply (rule ep_pair_comp)
    2.47 +    apply (rule ep_pair_u_map)
    2.48 +    apply (simp add: ep_pair.intro)
    2.49 +    apply (rule predomain_ep)
    2.50 +    done
    2.51 +  show "cast\<cdot>LIFTDEFL(bool) = liftemb oo (liftprj :: udom \<rightarrow> bool u)"
    2.52 +    unfolding liftemb_bool_def liftprj_bool_def liftdefl_bool_def
    2.53 +    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
    2.54 +    apply (simp add: ID_def [symmetric] u_map_ID)
    2.55 +    done
    2.56 +qed
    2.57 +
    2.58 +end
    2.59 +
    2.60 +lemma cont2cont_if [simp, cont2cont]:
    2.61 +  assumes b: "cont b" and f: "cont f" and g: "cont g"
    2.62 +  shows "cont (\<lambda>x. if b x then f x else g x)"
    2.63 +by (rule cont_apply [OF b cont_discrete_cpo], simp add: f g)
    2.64 +
    2.65 +lemma cont2cont_eq [simp, cont2cont]:
    2.66 +  fixes f g :: "'a::cpo \<Rightarrow> 'b::discrete_cpo"
    2.67 +  assumes f: "cont f" and g: "cont g"
    2.68 +  shows "cont (\<lambda>x. f x = g x)"
    2.69 +apply (rule cont_apply [OF f cont_discrete_cpo])
    2.70 +apply (rule cont_apply [OF g cont_discrete_cpo])
    2.71 +apply (rule cont_const)
    2.72 +done
    2.73 +
    2.74 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/HOLCF/Library/Char_Discrete.thy	Sat Dec 11 21:27:53 2010 -0800
     3.3 @@ -0,0 +1,245 @@
     3.4 +(*  Title:      HOLCF/Library/Char_Discrete.thy
     3.5 +    Author:     Brian Huffman
     3.6 +*)
     3.7 +
     3.8 +header {* Discrete cpo instance for 8-bit char type *}
     3.9 +
    3.10 +theory Char_Discrete
    3.11 +imports HOLCF
    3.12 +begin
    3.13 +
    3.14 +subsection {* Discrete cpo instance for @{typ nibble}. *}
    3.15 +
    3.16 +instantiation nibble :: discrete_cpo
    3.17 +begin
    3.18 +
    3.19 +definition below_nibble_def:
    3.20 +  "(x::nibble) \<sqsubseteq> y \<longleftrightarrow> x = y"
    3.21 +
    3.22 +instance proof
    3.23 +qed (rule below_nibble_def)
    3.24 +
    3.25 +end
    3.26 +
    3.27 +text {*
    3.28 +  TODO: implement a command to automate discrete predomain instances.
    3.29 +*}
    3.30 +
    3.31 +instantiation nibble :: predomain
    3.32 +begin
    3.33 +
    3.34 +definition
    3.35 +  "(liftemb :: nibble u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
    3.36 +
    3.37 +definition
    3.38 +  "(liftprj :: udom \<rightarrow> nibble u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
    3.39 +
    3.40 +definition
    3.41 +  "liftdefl \<equiv> (\<lambda>(t::nibble itself). LIFTDEFL(nibble discr))"
    3.42 +
    3.43 +instance proof
    3.44 +  show "ep_pair liftemb (liftprj :: udom \<rightarrow> nibble u)"
    3.45 +    unfolding liftemb_nibble_def liftprj_nibble_def
    3.46 +    apply (rule ep_pair_comp)
    3.47 +    apply (rule ep_pair_u_map)
    3.48 +    apply (simp add: ep_pair.intro)
    3.49 +    apply (rule predomain_ep)
    3.50 +    done
    3.51 +  show "cast\<cdot>LIFTDEFL(nibble) = liftemb oo (liftprj :: udom \<rightarrow> nibble u)"
    3.52 +    unfolding liftemb_nibble_def liftprj_nibble_def liftdefl_nibble_def
    3.53 +    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
    3.54 +    apply (simp add: ID_def [symmetric] u_map_ID)
    3.55 +    done
    3.56 +qed
    3.57 +
    3.58 +end
    3.59 +
    3.60 +subsection {* Discrete cpo instance for @{typ char}. *}
    3.61 +
    3.62 +instantiation char :: discrete_cpo
    3.63 +begin
    3.64 +
    3.65 +definition below_char_def:
    3.66 +  "(x::char) \<sqsubseteq> y \<longleftrightarrow> x = y"
    3.67 +
    3.68 +instance proof
    3.69 +qed (rule below_char_def)
    3.70 +
    3.71 +end
    3.72 +
    3.73 +text {*
    3.74 +  TODO: implement a command to automate discrete predomain instances.
    3.75 +*}
    3.76 +
    3.77 +instantiation char :: predomain
    3.78 +begin
    3.79 +
    3.80 +definition
    3.81 +  "(liftemb :: char u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
    3.82 +
    3.83 +definition
    3.84 +  "(liftprj :: udom \<rightarrow> char u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
    3.85 +
    3.86 +definition
    3.87 +  "liftdefl \<equiv> (\<lambda>(t::char itself). LIFTDEFL(char discr))"
    3.88 +
    3.89 +instance proof
    3.90 +  show "ep_pair liftemb (liftprj :: udom \<rightarrow> char u)"
    3.91 +    unfolding liftemb_char_def liftprj_char_def
    3.92 +    apply (rule ep_pair_comp)
    3.93 +    apply (rule ep_pair_u_map)
    3.94 +    apply (simp add: ep_pair.intro)
    3.95 +    apply (rule predomain_ep)
    3.96 +    done
    3.97 +  show "cast\<cdot>LIFTDEFL(char) = liftemb oo (liftprj :: udom \<rightarrow> char u)"
    3.98 +    unfolding liftemb_char_def liftprj_char_def liftdefl_char_def
    3.99 +    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
   3.100 +    apply (simp add: ID_def [symmetric] u_map_ID)
   3.101 +    done
   3.102 +qed
   3.103 +
   3.104 +end
   3.105 +
   3.106 +subsection {* Using chars with Fixrec *}
   3.107 +
   3.108 +definition match_Char :: "char \<rightarrow> (nibble \<rightarrow> nibble \<rightarrow> 'a match) \<rightarrow> 'a match"
   3.109 +  where "match_Char = (\<Lambda> c k. case c of Char a b \<Rightarrow> k\<cdot>a\<cdot>b)"
   3.110 +
   3.111 +lemma match_Char_simps [simp]:
   3.112 +  "match_Char\<cdot>(Char a b)\<cdot>k = k\<cdot>a\<cdot>b"
   3.113 +by (simp add: match_Char_def)
   3.114 +
   3.115 +definition match_Nibble0 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.116 +  where "match_Nibble0 = (\<Lambda> c k. if c = Nibble0 then k else Fixrec.fail)"
   3.117 +
   3.118 +definition match_Nibble1 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.119 +  where "match_Nibble1 = (\<Lambda> c k. if c = Nibble1 then k else Fixrec.fail)"
   3.120 +
   3.121 +definition match_Nibble2 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.122 +  where "match_Nibble2 = (\<Lambda> c k. if c = Nibble2 then k else Fixrec.fail)"
   3.123 +
   3.124 +definition match_Nibble3 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.125 +  where "match_Nibble3 = (\<Lambda> c k. if c = Nibble3 then k else Fixrec.fail)"
   3.126 +
   3.127 +definition match_Nibble4 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.128 +  where "match_Nibble4 = (\<Lambda> c k. if c = Nibble4 then k else Fixrec.fail)"
   3.129 +
   3.130 +definition match_Nibble5 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.131 +  where "match_Nibble5 = (\<Lambda> c k. if c = Nibble5 then k else Fixrec.fail)"
   3.132 +
   3.133 +definition match_Nibble6 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.134 +  where "match_Nibble6 = (\<Lambda> c k. if c = Nibble6 then k else Fixrec.fail)"
   3.135 +
   3.136 +definition match_Nibble7 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.137 +  where "match_Nibble7 = (\<Lambda> c k. if c = Nibble7 then k else Fixrec.fail)"
   3.138 +
   3.139 +definition match_Nibble8 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.140 +  where "match_Nibble8 = (\<Lambda> c k. if c = Nibble8 then k else Fixrec.fail)"
   3.141 +
   3.142 +definition match_Nibble9 :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.143 +  where "match_Nibble9 = (\<Lambda> c k. if c = Nibble9 then k else Fixrec.fail)"
   3.144 +
   3.145 +definition match_NibbleA :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.146 +  where "match_NibbleA = (\<Lambda> c k. if c = NibbleA then k else Fixrec.fail)"
   3.147 +
   3.148 +definition match_NibbleB :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.149 +  where "match_NibbleB = (\<Lambda> c k. if c = NibbleB then k else Fixrec.fail)"
   3.150 +
   3.151 +definition match_NibbleC :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.152 +  where "match_NibbleC = (\<Lambda> c k. if c = NibbleC then k else Fixrec.fail)"
   3.153 +
   3.154 +definition match_NibbleD :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.155 +  where "match_NibbleD = (\<Lambda> c k. if c = NibbleD then k else Fixrec.fail)"
   3.156 +
   3.157 +definition match_NibbleE :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.158 +  where "match_NibbleE = (\<Lambda> c k. if c = NibbleE then k else Fixrec.fail)"
   3.159 +
   3.160 +definition match_NibbleF :: "nibble \<rightarrow> 'a match \<rightarrow> 'a match"
   3.161 +  where "match_NibbleF = (\<Lambda> c k. if c = NibbleF then k else Fixrec.fail)"
   3.162 +
   3.163 +lemma match_Nibble0_simps [simp]:
   3.164 +  "match_Nibble0\<cdot>c\<cdot>k = (if c = Nibble0 then k else Fixrec.fail)"
   3.165 +by (simp add: match_Nibble0_def)
   3.166 +
   3.167 +lemma match_Nibble1_simps [simp]:
   3.168 +  "match_Nibble1\<cdot>c\<cdot>k = (if c = Nibble1 then k else Fixrec.fail)"
   3.169 +by (simp add: match_Nibble1_def)
   3.170 +
   3.171 +lemma match_Nibble2_simps [simp]:
   3.172 +  "match_Nibble2\<cdot>c\<cdot>k = (if c = Nibble2 then k else Fixrec.fail)"
   3.173 +by (simp add: match_Nibble2_def)
   3.174 +
   3.175 +lemma match_Nibble3_simps [simp]:
   3.176 +  "match_Nibble3\<cdot>c\<cdot>k = (if c = Nibble3 then k else Fixrec.fail)"
   3.177 +by (simp add: match_Nibble3_def)
   3.178 +
   3.179 +lemma match_Nibble4_simps [simp]:
   3.180 +  "match_Nibble4\<cdot>c\<cdot>k = (if c = Nibble4 then k else Fixrec.fail)"
   3.181 +by (simp add: match_Nibble4_def)
   3.182 +
   3.183 +lemma match_Nibble5_simps [simp]:
   3.184 +  "match_Nibble5\<cdot>c\<cdot>k = (if c = Nibble5 then k else Fixrec.fail)"
   3.185 +by (simp add: match_Nibble5_def)
   3.186 +
   3.187 +lemma match_Nibble6_simps [simp]:
   3.188 +  "match_Nibble6\<cdot>c\<cdot>k = (if c = Nibble6 then k else Fixrec.fail)"
   3.189 +by (simp add: match_Nibble6_def)
   3.190 +
   3.191 +lemma match_Nibble7_simps [simp]:
   3.192 +  "match_Nibble7\<cdot>c\<cdot>k = (if c = Nibble7 then k else Fixrec.fail)"
   3.193 +by (simp add: match_Nibble7_def)
   3.194 +
   3.195 +lemma match_Nibble8_simps [simp]:
   3.196 +  "match_Nibble8\<cdot>c\<cdot>k = (if c = Nibble8 then k else Fixrec.fail)"
   3.197 +by (simp add: match_Nibble8_def)
   3.198 +
   3.199 +lemma match_Nibble9_simps [simp]:
   3.200 +  "match_Nibble9\<cdot>c\<cdot>k = (if c = Nibble9 then k else Fixrec.fail)"
   3.201 +by (simp add: match_Nibble9_def)
   3.202 +
   3.203 +lemma match_NibbleA_simps [simp]:
   3.204 +  "match_NibbleA\<cdot>c\<cdot>k = (if c = NibbleA then k else Fixrec.fail)"
   3.205 +by (simp add: match_NibbleA_def)
   3.206 +
   3.207 +lemma match_NibbleB_simps [simp]:
   3.208 +  "match_NibbleB\<cdot>c\<cdot>k = (if c = NibbleB then k else Fixrec.fail)"
   3.209 +by (simp add: match_NibbleB_def)
   3.210 +
   3.211 +lemma match_NibbleC_simps [simp]:
   3.212 +  "match_NibbleC\<cdot>c\<cdot>k = (if c = NibbleC then k else Fixrec.fail)"
   3.213 +by (simp add: match_NibbleC_def)
   3.214 +
   3.215 +lemma match_NibbleD_simps [simp]:
   3.216 +  "match_NibbleD\<cdot>c\<cdot>k = (if c = NibbleD then k else Fixrec.fail)"
   3.217 +by (simp add: match_NibbleD_def)
   3.218 +
   3.219 +lemma match_NibbleE_simps [simp]:
   3.220 +  "match_NibbleE\<cdot>c\<cdot>k = (if c = NibbleE then k else Fixrec.fail)"
   3.221 +by (simp add: match_NibbleE_def)
   3.222 +
   3.223 +lemma match_NibbleF_simps [simp]:
   3.224 +  "match_NibbleF\<cdot>c\<cdot>k = (if c = NibbleF then k else Fixrec.fail)"
   3.225 +by (simp add: match_NibbleF_def)
   3.226 +
   3.227 +setup {*
   3.228 +  Fixrec.add_matchers
   3.229 +    [ (@{const_name Char}, @{const_name match_Char}),
   3.230 +      (@{const_name Nibble0}, @{const_name match_Nibble0}),
   3.231 +      (@{const_name Nibble1}, @{const_name match_Nibble1}),
   3.232 +      (@{const_name Nibble2}, @{const_name match_Nibble2}),
   3.233 +      (@{const_name Nibble3}, @{const_name match_Nibble3}),
   3.234 +      (@{const_name Nibble4}, @{const_name match_Nibble4}),
   3.235 +      (@{const_name Nibble5}, @{const_name match_Nibble5}),
   3.236 +      (@{const_name Nibble6}, @{const_name match_Nibble6}),
   3.237 +      (@{const_name Nibble7}, @{const_name match_Nibble7}),
   3.238 +      (@{const_name Nibble8}, @{const_name match_Nibble8}),
   3.239 +      (@{const_name Nibble9}, @{const_name match_Nibble9}),
   3.240 +      (@{const_name NibbleA}, @{const_name match_NibbleA}),
   3.241 +      (@{const_name NibbleB}, @{const_name match_NibbleB}),
   3.242 +      (@{const_name NibbleC}, @{const_name match_NibbleC}),
   3.243 +      (@{const_name NibbleD}, @{const_name match_NibbleD}),
   3.244 +      (@{const_name NibbleE}, @{const_name match_NibbleE}),
   3.245 +      (@{const_name NibbleF}, @{const_name match_NibbleF}) ]
   3.246 +*}
   3.247 +
   3.248 +end
     4.1 --- a/src/HOL/HOLCF/Library/HOLCF_Library.thy	Sat Dec 11 11:26:37 2010 -0800
     4.2 +++ b/src/HOL/HOLCF/Library/HOLCF_Library.thy	Sat Dec 11 21:27:53 2010 -0800
     4.3 @@ -1,7 +1,13 @@
     4.4  theory HOLCF_Library
     4.5  imports
     4.6 +  Bool_Discrete
     4.7 +  Char_Discrete
     4.8    Defl_Bifinite
     4.9 +  Int_Discrete
    4.10    List_Cpo
    4.11 +  List_Predomain
    4.12 +  Nat_Discrete
    4.13 +  Option_Cpo
    4.14    Stream
    4.15    Sum_Cpo
    4.16  begin
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/HOLCF/Library/HOL_Cpo.thy	Sat Dec 11 21:27:53 2010 -0800
     5.3 @@ -0,0 +1,18 @@
     5.4 +(*  Title:      HOLCF/HOL_Cpo.thy
     5.5 +    Author:     Brian Huffman
     5.6 +*)
     5.7 +
     5.8 +header {* Cpo class instances for all HOL types *}
     5.9 +
    5.10 +theory HOL_Cpo
    5.11 +imports
    5.12 +  Bool_Discrete
    5.13 +  Nat_Discrete
    5.14 +  Int_Discrete
    5.15 +  Char_Discrete
    5.16 +  Sum_Cpo
    5.17 +  Option_Cpo
    5.18 +  List_Predomain
    5.19 +begin
    5.20 +
    5.21 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/HOLCF/Library/Int_Discrete.thy	Sat Dec 11 21:27:53 2010 -0800
     6.3 @@ -0,0 +1,57 @@
     6.4 +(*  Title:      HOLCF/Library/Int_Discrete.thy
     6.5 +    Author:     Brian Huffman
     6.6 +*)
     6.7 +
     6.8 +header {* Discrete cpo instance for integers *}
     6.9 +
    6.10 +theory Int_Discrete
    6.11 +imports HOLCF
    6.12 +begin
    6.13 +
    6.14 +text {* Discrete cpo instance for @{typ int}. *}
    6.15 +
    6.16 +instantiation int :: discrete_cpo
    6.17 +begin
    6.18 +
    6.19 +definition below_int_def:
    6.20 +  "(x::int) \<sqsubseteq> y \<longleftrightarrow> x = y"
    6.21 +
    6.22 +instance proof
    6.23 +qed (rule below_int_def)
    6.24 +
    6.25 +end
    6.26 +
    6.27 +text {*
    6.28 +  TODO: implement a command to automate discrete predomain instances.
    6.29 +*}
    6.30 +
    6.31 +instantiation int :: predomain
    6.32 +begin
    6.33 +
    6.34 +definition
    6.35 +  "(liftemb :: int u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
    6.36 +
    6.37 +definition
    6.38 +  "(liftprj :: udom \<rightarrow> int u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
    6.39 +
    6.40 +definition
    6.41 +  "liftdefl \<equiv> (\<lambda>(t::int itself). LIFTDEFL(int discr))"
    6.42 +
    6.43 +instance proof
    6.44 +  show "ep_pair liftemb (liftprj :: udom \<rightarrow> int u)"
    6.45 +    unfolding liftemb_int_def liftprj_int_def
    6.46 +    apply (rule ep_pair_comp)
    6.47 +    apply (rule ep_pair_u_map)
    6.48 +    apply (simp add: ep_pair.intro)
    6.49 +    apply (rule predomain_ep)
    6.50 +    done
    6.51 +  show "cast\<cdot>LIFTDEFL(int) = liftemb oo (liftprj :: udom \<rightarrow> int u)"
    6.52 +    unfolding liftemb_int_def liftprj_int_def liftdefl_int_def
    6.53 +    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
    6.54 +    apply (simp add: ID_def [symmetric] u_map_ID)
    6.55 +    done
    6.56 +qed
    6.57 +
    6.58 +end
    6.59 +
    6.60 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/HOLCF/Library/List_Predomain.thy	Sat Dec 11 21:27:53 2010 -0800
     7.3 @@ -0,0 +1,128 @@
     7.4 +(*  Title:      HOLCF/Library/List_Predomain.thy
     7.5 +    Author:     Brian Huffman
     7.6 +*)
     7.7 +
     7.8 +header {* Predomain class instance for HOL list type *}
     7.9 +
    7.10 +theory List_Predomain
    7.11 +imports List_Cpo
    7.12 +begin
    7.13 +
    7.14 +subsection {* Strict list type *}
    7.15 +
    7.16 +domain 'a slist = SNil | SCons "'a" "'a slist"
    7.17 +
    7.18 +text {*
    7.19 +  Types @{typ "'a list u"}. and @{typ "'a u slist"} are isomorphic.
    7.20 +*}
    7.21 +
    7.22 +fixrec encode_list_u where
    7.23 +  "encode_list_u\<cdot>(up\<cdot>[]) = SNil" |
    7.24 +  "encode_list_u\<cdot>(up\<cdot>(x # xs)) = SCons\<cdot>(up\<cdot>x)\<cdot>(encode_list_u\<cdot>(up\<cdot>xs))"
    7.25 +
    7.26 +lemma encode_list_u_strict [simp]: "encode_list_u\<cdot>\<bottom> = \<bottom>"
    7.27 +by fixrec_simp
    7.28 +
    7.29 +lemma encode_list_u_bottom_iff [simp]:
    7.30 +  "encode_list_u\<cdot>x = \<bottom> \<longleftrightarrow> x = \<bottom>"
    7.31 +apply (induct x, simp_all)
    7.32 +apply (rename_tac xs, induct_tac xs, simp_all)
    7.33 +done
    7.34 +
    7.35 +fixrec decode_list_u where
    7.36 +  "decode_list_u\<cdot>SNil = up\<cdot>[]" |
    7.37 +  "ys \<noteq> \<bottom> \<Longrightarrow> decode_list_u\<cdot>(SCons\<cdot>(up\<cdot>x)\<cdot>ys) =
    7.38 +    (case decode_list_u\<cdot>ys of up\<cdot>xs \<Rightarrow> up\<cdot>(x # xs))"
    7.39 +
    7.40 +lemma decode_list_u_strict [simp]: "decode_list_u\<cdot>\<bottom> = \<bottom>"
    7.41 +by fixrec_simp
    7.42 +
    7.43 +lemma decode_encode_list_u [simp]: "decode_list_u\<cdot>(encode_list_u\<cdot>x) = x"
    7.44 +by (induct x, simp, rename_tac xs, induct_tac xs, simp_all)
    7.45 +
    7.46 +lemma encode_decode_list_u [simp]: "encode_list_u\<cdot>(decode_list_u\<cdot>y) = y"
    7.47 +apply (induct y, simp, simp)
    7.48 +apply (case_tac a, simp)
    7.49 +apply (case_tac "decode_list_u\<cdot>y", simp, simp)
    7.50 +done
    7.51 +
    7.52 +subsection {* Lists are a predomain *}
    7.53 +
    7.54 +instantiation list :: (predomain) predomain
    7.55 +begin
    7.56 +
    7.57 +definition
    7.58 +  "liftemb = emb oo encode_list_u"
    7.59 +
    7.60 +definition
    7.61 +  "liftprj = decode_list_u oo prj"
    7.62 +
    7.63 +definition
    7.64 +  "liftdefl (t::('a list) itself) = DEFL(('a\<^sub>\<bottom>) slist)"
    7.65 +
    7.66 +instance proof
    7.67 +  have "ep_pair encode_list_u decode_list_u"
    7.68 +    by (rule ep_pair.intro, simp_all)
    7.69 +  thus "ep_pair liftemb (liftprj :: udom \<rightarrow> ('a list) u)"
    7.70 +    unfolding liftemb_list_def liftprj_list_def
    7.71 +    using ep_pair_emb_prj by (rule ep_pair_comp)
    7.72 +  show "cast\<cdot>LIFTDEFL('a list) = liftemb oo (liftprj :: udom \<rightarrow> ('a list) u)"
    7.73 +    unfolding liftemb_list_def liftprj_list_def liftdefl_list_def
    7.74 +    by (simp add: cfcomp1 cast_DEFL)
    7.75 +qed
    7.76 +
    7.77 +end
    7.78 +
    7.79 +lemma liftdefl_list [domain_defl_simps]:
    7.80 +  "LIFTDEFL('a::predomain list) = slist_defl\<cdot>LIFTDEFL('a)"
    7.81 +unfolding liftdefl_list_def by (simp add: domain_defl_simps)
    7.82 +
    7.83 +subsection {* Continuous map operation for lists *}
    7.84 +
    7.85 +definition
    7.86 +  list_map :: "('a::predomain \<rightarrow> 'b::predomain) \<rightarrow> 'a list \<rightarrow> 'b list"
    7.87 +where
    7.88 +  "list_map = (\<Lambda> f xs. map (\<lambda>x. f\<cdot>x) xs)"
    7.89 +
    7.90 +lemma list_map_simps [simp]:
    7.91 +  "list_map\<cdot>f\<cdot>[] = []"
    7.92 +  "list_map\<cdot>f\<cdot>(x # xs) = f\<cdot>x # list_map\<cdot>f\<cdot>xs"
    7.93 +unfolding list_map_def by simp_all
    7.94 +
    7.95 +lemma list_map_ID [domain_map_ID]: "list_map\<cdot>ID = ID"
    7.96 +unfolding list_map_def ID_def
    7.97 +by (simp add: Abs_cfun_inverse cfun_def)
    7.98 +
    7.99 +lemma deflation_list_map [domain_deflation]:
   7.100 +  "deflation d \<Longrightarrow> deflation (list_map\<cdot>d)"
   7.101 +apply default
   7.102 +apply (induct_tac x, simp_all add: deflation.idem)
   7.103 +apply (induct_tac x, simp_all add: deflation.below)
   7.104 +done
   7.105 +
   7.106 +subsection {* Configuring list type to work with domain package *}
   7.107 +
   7.108 +lemma encode_list_u_map:
   7.109 +  "encode_list_u\<cdot>(u_map\<cdot>(list_map\<cdot>f)\<cdot>(decode_list_u\<cdot>xs))
   7.110 +    = slist_map\<cdot>(u_map\<cdot>f)\<cdot>xs"
   7.111 +apply (induct xs)
   7.112 +apply (simp, subst slist_map_unfold, simp)
   7.113 +apply (simp, subst slist_map_unfold, simp add: SNil_def)
   7.114 +apply (case_tac a, simp, rename_tac b)
   7.115 +apply (case_tac "decode_list_u\<cdot>xs")
   7.116 +apply (drule_tac f="encode_list_u" in cfun_arg_cong, simp)
   7.117 +by (simp, subst slist_map_unfold, simp add: SCons_def)
   7.118 +
   7.119 +lemma isodefl_list_u [domain_isodefl]:
   7.120 +  fixes d :: "'a::predomain \<rightarrow> 'a"
   7.121 +  assumes "isodefl (u_map\<cdot>d) t"
   7.122 +  shows "isodefl (u_map\<cdot>(list_map\<cdot>d)) (slist_defl\<cdot>t)"
   7.123 +using assms [THEN isodefl_slist] unfolding isodefl_def
   7.124 +unfolding emb_u_def prj_u_def liftemb_list_def liftprj_list_def
   7.125 +by (simp add: cfcomp1 encode_list_u_map)
   7.126 +
   7.127 +setup {*
   7.128 +  Domain_Take_Proofs.add_rec_type (@{type_name "list"}, [true])
   7.129 +*}
   7.130 +
   7.131 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/HOLCF/Library/Nat_Discrete.thy	Sat Dec 11 21:27:53 2010 -0800
     8.3 @@ -0,0 +1,57 @@
     8.4 +(*  Title:      HOLCF/Library/Nat_Discrete.thy
     8.5 +    Author:     Brian Huffman
     8.6 +*)
     8.7 +
     8.8 +header {* Discrete cpo instance for naturals *}
     8.9 +
    8.10 +theory Nat_Discrete
    8.11 +imports HOLCF
    8.12 +begin
    8.13 +
    8.14 +text {* Discrete cpo instance for @{typ nat}. *}
    8.15 +
    8.16 +instantiation nat :: discrete_cpo
    8.17 +begin
    8.18 +
    8.19 +definition below_nat_def:
    8.20 +  "(x::nat) \<sqsubseteq> y \<longleftrightarrow> x = y"
    8.21 +
    8.22 +instance proof
    8.23 +qed (rule below_nat_def)
    8.24 +
    8.25 +end
    8.26 +
    8.27 +text {*
    8.28 +  TODO: implement a command to automate discrete predomain instances.
    8.29 +*}
    8.30 +
    8.31 +instantiation nat :: predomain
    8.32 +begin
    8.33 +
    8.34 +definition
    8.35 +  "(liftemb :: nat u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
    8.36 +
    8.37 +definition
    8.38 +  "(liftprj :: udom \<rightarrow> nat u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
    8.39 +
    8.40 +definition
    8.41 +  "liftdefl \<equiv> (\<lambda>(t::nat itself). LIFTDEFL(nat discr))"
    8.42 +
    8.43 +instance proof
    8.44 +  show "ep_pair liftemb (liftprj :: udom \<rightarrow> nat u)"
    8.45 +    unfolding liftemb_nat_def liftprj_nat_def
    8.46 +    apply (rule ep_pair_comp)
    8.47 +    apply (rule ep_pair_u_map)
    8.48 +    apply (simp add: ep_pair.intro)
    8.49 +    apply (rule predomain_ep)
    8.50 +    done
    8.51 +  show "cast\<cdot>LIFTDEFL(nat) = liftemb oo (liftprj :: udom \<rightarrow> nat u)"
    8.52 +    unfolding liftemb_nat_def liftprj_nat_def liftdefl_nat_def
    8.53 +    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
    8.54 +    apply (simp add: ID_def [symmetric] u_map_ID)
    8.55 +    done
    8.56 +qed
    8.57 +
    8.58 +end
    8.59 +
    8.60 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/HOLCF/Library/Option_Cpo.thy	Sat Dec 11 21:27:53 2010 -0800
     9.3 @@ -0,0 +1,255 @@
     9.4 +(*  Title:      HOLCF/Option_Cpo.thy
     9.5 +    Author:     Brian Huffman
     9.6 +*)
     9.7 +
     9.8 +header {* Cpo class instance for HOL option type *}
     9.9 +
    9.10 +theory Option_Cpo
    9.11 +imports HOLCF
    9.12 +begin
    9.13 +
    9.14 +subsection {* Ordering on option type *}
    9.15 +
    9.16 +instantiation option :: (below) below
    9.17 +begin
    9.18 +
    9.19 +definition below_option_def:
    9.20 +  "x \<sqsubseteq> y \<equiv> case x of
    9.21 +         None \<Rightarrow> (case y of None \<Rightarrow> True | Some b \<Rightarrow> False) |
    9.22 +         Some a \<Rightarrow> (case y of None \<Rightarrow> False | Some b \<Rightarrow> a \<sqsubseteq> b)"
    9.23 +
    9.24 +instance ..
    9.25 +end
    9.26 +
    9.27 +lemma None_below_None [simp]: "None \<sqsubseteq> None"
    9.28 +unfolding below_option_def by simp
    9.29 +
    9.30 +lemma Some_below_Some [simp]: "Some x \<sqsubseteq> Some y \<longleftrightarrow> x \<sqsubseteq> y"
    9.31 +unfolding below_option_def by simp
    9.32 +
    9.33 +lemma Some_below_None [simp]: "\<not> Some x \<sqsubseteq> None"
    9.34 +unfolding below_option_def by simp
    9.35 +
    9.36 +lemma None_below_Some [simp]: "\<not> None \<sqsubseteq> Some y"
    9.37 +unfolding below_option_def by simp
    9.38 +
    9.39 +lemma Some_mono: "x \<sqsubseteq> y \<Longrightarrow> Some x \<sqsubseteq> Some y"
    9.40 +by simp
    9.41 +
    9.42 +lemma None_below_iff [simp]: "None \<sqsubseteq> x \<longleftrightarrow> x = None"
    9.43 +by (cases x, simp_all)
    9.44 +
    9.45 +lemma below_None_iff [simp]: "x \<sqsubseteq> None \<longleftrightarrow> x = None"
    9.46 +by (cases x, simp_all)
    9.47 +
    9.48 +lemma option_below_cases:
    9.49 +  assumes "x \<sqsubseteq> y"
    9.50 +  obtains "x = None" and "y = None"
    9.51 +  | a b where "x = Some a" and "y = Some b" and "a \<sqsubseteq> b"
    9.52 +using assms unfolding below_option_def
    9.53 +by (simp split: option.split_asm)
    9.54 +
    9.55 +subsection {* Option type is a complete partial order *}
    9.56 +
    9.57 +instance option :: (po) po
    9.58 +proof
    9.59 +  fix x :: "'a option"
    9.60 +  show "x \<sqsubseteq> x"
    9.61 +    unfolding below_option_def
    9.62 +    by (simp split: option.split)
    9.63 +next
    9.64 +  fix x y :: "'a option"
    9.65 +  assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
    9.66 +    unfolding below_option_def
    9.67 +    by (auto split: option.split_asm intro: below_antisym)
    9.68 +next
    9.69 +  fix x y z :: "'a option"
    9.70 +  assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    9.71 +    unfolding below_option_def
    9.72 +    by (auto split: option.split_asm intro: below_trans)
    9.73 +qed
    9.74 +
    9.75 +lemma monofun_the: "monofun the"
    9.76 +by (rule monofunI, erule option_below_cases, simp_all)
    9.77 +
    9.78 +lemma option_chain_cases:
    9.79 +  assumes Y: "chain Y"
    9.80 +  obtains "Y = (\<lambda>i. None)" | A where "chain A" and "Y = (\<lambda>i. Some (A i))"
    9.81 + apply (cases "Y 0")
    9.82 +  apply (rule that(1))
    9.83 +  apply (rule ext)
    9.84 +  apply (cut_tac j=i in chain_mono [OF Y le0], simp)
    9.85 + apply (rule that(2))
    9.86 +  apply (rule ch2ch_monofun [OF monofun_the Y])
    9.87 + apply (rule ext)
    9.88 + apply (cut_tac j=i in chain_mono [OF Y le0], simp)
    9.89 + apply (case_tac "Y i", simp_all)
    9.90 +done
    9.91 +
    9.92 +lemma is_lub_Some: "range S <<| x \<Longrightarrow> range (\<lambda>i. Some (S i)) <<| Some x"
    9.93 + apply (rule is_lubI)
    9.94 +  apply (rule ub_rangeI)
    9.95 +  apply (simp add: is_lub_rangeD1)
    9.96 + apply (frule ub_rangeD [where i=arbitrary])
    9.97 + apply (case_tac u, simp_all)
    9.98 + apply (erule is_lubD2)
    9.99 + apply (rule ub_rangeI)
   9.100 + apply (drule ub_rangeD, simp)
   9.101 +done
   9.102 +
   9.103 +instance option :: (cpo) cpo
   9.104 + apply intro_classes
   9.105 + apply (erule option_chain_cases, safe)
   9.106 +  apply (rule exI, rule is_lub_const)
   9.107 + apply (rule exI)
   9.108 + apply (rule is_lub_Some)
   9.109 + apply (erule cpo_lubI)
   9.110 +done
   9.111 +
   9.112 +subsection {* Continuity of Some and case function *}
   9.113 +
   9.114 +lemma cont_Some: "cont Some"
   9.115 +by (intro contI is_lub_Some cpo_lubI)
   9.116 +
   9.117 +lemmas cont2cont_Some [simp, cont2cont] = cont_compose [OF cont_Some]
   9.118 +
   9.119 +lemmas ch2ch_Some [simp] = ch2ch_cont [OF cont_Some]
   9.120 +
   9.121 +lemmas lub_Some = cont2contlubE [OF cont_Some, symmetric]
   9.122 +
   9.123 +lemma cont2cont_option_case:
   9.124 +  assumes f: "cont (\<lambda>x. f x)"
   9.125 +  assumes g: "cont (\<lambda>x. g x)"
   9.126 +  assumes h1: "\<And>a. cont (\<lambda>x. h x a)"
   9.127 +  assumes h2: "\<And>x. cont (\<lambda>a. h x a)"
   9.128 +  shows "cont (\<lambda>x. case f x of None \<Rightarrow> g x | Some a \<Rightarrow> h x a)"
   9.129 +apply (rule cont_apply [OF f])
   9.130 +apply (rule contI)
   9.131 +apply (erule option_chain_cases)
   9.132 +apply (simp add: is_lub_const)
   9.133 +apply (simp add: lub_Some)
   9.134 +apply (simp add: cont2contlubE [OF h2])
   9.135 +apply (rule cpo_lubI, rule chainI)
   9.136 +apply (erule cont2monofunE [OF h2 chainE])
   9.137 +apply (case_tac y, simp_all add: g h1)
   9.138 +done
   9.139 +
   9.140 +lemma cont2cont_option_case' [simp, cont2cont]:
   9.141 +  assumes f: "cont (\<lambda>x. f x)"
   9.142 +  assumes g: "cont (\<lambda>x. g x)"
   9.143 +  assumes h: "cont (\<lambda>p. h (fst p) (snd p))"
   9.144 +  shows "cont (\<lambda>x. case f x of None \<Rightarrow> g x | Some a \<Rightarrow> h x a)"
   9.145 +using assms by (simp add: cont2cont_option_case prod_cont_iff)
   9.146 +
   9.147 +text {* Simple version for when the element type is not a cpo. *}
   9.148 +
   9.149 +lemma cont2cont_option_case_simple [simp, cont2cont]:
   9.150 +  assumes "cont (\<lambda>x. f x)"
   9.151 +  assumes "\<And>a. cont (\<lambda>x. g x a)"
   9.152 +  shows "cont (\<lambda>x. case z of None \<Rightarrow> f x | Some a \<Rightarrow> g x a)"
   9.153 +using assms by (cases z) auto
   9.154 +
   9.155 +subsection {* Compactness and chain-finiteness *}
   9.156 +
   9.157 +lemma compact_None [simp]: "compact None"
   9.158 +apply (rule compactI2)
   9.159 +apply (erule option_chain_cases, safe)
   9.160 +apply simp
   9.161 +apply (simp add: lub_Some)
   9.162 +done
   9.163 +
   9.164 +lemma compact_Some: "compact a \<Longrightarrow> compact (Some a)"
   9.165 +apply (rule compactI2)
   9.166 +apply (erule option_chain_cases, safe)
   9.167 +apply simp
   9.168 +apply (simp add: lub_Some)
   9.169 +apply (erule (2) compactD2)
   9.170 +done
   9.171 +
   9.172 +lemma compact_Some_rev: "compact (Some a) \<Longrightarrow> compact a"
   9.173 +unfolding compact_def
   9.174 +by (drule adm_subst [OF cont_Some], simp)
   9.175 +
   9.176 +lemma compact_Some_iff [simp]: "compact (Some a) = compact a"
   9.177 +by (safe elim!: compact_Some compact_Some_rev)
   9.178 +
   9.179 +instance option :: (chfin) chfin
   9.180 +apply intro_classes
   9.181 +apply (erule compact_imp_max_in_chain)
   9.182 +apply (case_tac "\<Squnion>i. Y i", simp_all)
   9.183 +done
   9.184 +
   9.185 +instance option :: (discrete_cpo) discrete_cpo
   9.186 +by intro_classes (simp add: below_option_def split: option.split)
   9.187 +
   9.188 +subsection {* Using option types with fixrec *}
   9.189 +
   9.190 +definition
   9.191 +  "match_None = (\<Lambda> x k. case x of None \<Rightarrow> k | Some a \<Rightarrow> Fixrec.fail)"
   9.192 +
   9.193 +definition
   9.194 +  "match_Some = (\<Lambda> x k. case x of None \<Rightarrow> Fixrec.fail | Some a \<Rightarrow> k\<cdot>a)"
   9.195 +
   9.196 +lemma match_None_simps [simp]:
   9.197 +  "match_None\<cdot>None\<cdot>k = k"
   9.198 +  "match_None\<cdot>(Some a)\<cdot>k = Fixrec.fail"
   9.199 +unfolding match_None_def by simp_all
   9.200 +
   9.201 +lemma match_Some_simps [simp]:
   9.202 +  "match_Some\<cdot>None\<cdot>k = Fixrec.fail"
   9.203 +  "match_Some\<cdot>(Some a)\<cdot>k = k\<cdot>a"
   9.204 +unfolding match_Some_def by simp_all
   9.205 +
   9.206 +setup {*
   9.207 +  Fixrec.add_matchers
   9.208 +    [ (@{const_name None}, @{const_name match_None}),
   9.209 +      (@{const_name Some}, @{const_name match_Some}) ]
   9.210 +*}
   9.211 +
   9.212 +subsection {* Option type is a predomain *}
   9.213 +
   9.214 +definition
   9.215 +  "encode_option_u =
   9.216 +    (\<Lambda>(up\<cdot>x). case x of None \<Rightarrow> sinl\<cdot>ONE | Some a \<Rightarrow> sinr\<cdot>(up\<cdot>a))"
   9.217 +
   9.218 +definition
   9.219 +  "decode_option_u = sscase\<cdot>(\<Lambda> ONE. up\<cdot>None)\<cdot>(\<Lambda>(up\<cdot>a). up\<cdot>(Some a))"
   9.220 +
   9.221 +lemma decode_encode_option_u [simp]: "decode_option_u\<cdot>(encode_option_u\<cdot>x) = x"
   9.222 +unfolding decode_option_u_def encode_option_u_def
   9.223 +by (case_tac x, simp, rename_tac y, case_tac y, simp_all)
   9.224 +
   9.225 +lemma encode_decode_option_u [simp]: "encode_option_u\<cdot>(decode_option_u\<cdot>x) = x"
   9.226 +unfolding decode_option_u_def encode_option_u_def
   9.227 +apply (case_tac x, simp)
   9.228 +apply (rename_tac a, case_tac a rule: oneE, simp, simp)
   9.229 +apply (rename_tac b, case_tac b, simp, simp)
   9.230 +done
   9.231 +
   9.232 +instantiation option :: (predomain) predomain
   9.233 +begin
   9.234 +
   9.235 +definition
   9.236 +  "liftemb = emb oo encode_option_u"
   9.237 +
   9.238 +definition
   9.239 +  "liftprj = decode_option_u oo prj"
   9.240 +
   9.241 +definition
   9.242 +  "liftdefl (t::('a option) itself) = DEFL(one \<oplus> 'a u)"
   9.243 +
   9.244 +instance proof
   9.245 +  show "ep_pair liftemb (liftprj :: udom \<rightarrow> ('a option) u)"
   9.246 +    unfolding liftemb_option_def liftprj_option_def
   9.247 +    apply (rule ep_pair_comp)
   9.248 +    apply (rule ep_pair.intro, simp, simp)
   9.249 +    apply (rule ep_pair_emb_prj)
   9.250 +    done
   9.251 +  show "cast\<cdot>LIFTDEFL('a option) = liftemb oo (liftprj :: udom \<rightarrow> ('a option) u)"
   9.252 +    unfolding liftemb_option_def liftprj_option_def liftdefl_option_def
   9.253 +    by (simp add: cast_DEFL cfcomp1)
   9.254 +qed
   9.255 +
   9.256 +end
   9.257 +
   9.258 +end
    10.1 --- a/src/HOL/IsaMakefile	Sat Dec 11 11:26:37 2010 -0800
    10.2 +++ b/src/HOL/IsaMakefile	Sat Dec 11 21:27:53 2010 -0800
    10.3 @@ -1471,7 +1471,14 @@
    10.4  
    10.5  $(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
    10.6    HOLCF/Library/Defl_Bifinite.thy \
    10.7 +  HOLCF/Library/Bool_Discrete.thy \
    10.8 +  HOLCF/Library/Char_Discrete.thy \
    10.9 +  HOLCF/Library/HOL_Cpo.thy \
   10.10 +  HOLCF/Library/Int_Discrete.thy \
   10.11    HOLCF/Library/List_Cpo.thy \
   10.12 +  HOLCF/Library/List_Predomain.thy \
   10.13 +  HOLCF/Library/Nat_Discrete.thy \
   10.14 +  HOLCF/Library/Option_Cpo.thy \
   10.15    HOLCF/Library/Stream.thy \
   10.16    HOLCF/Library/Sum_Cpo.thy \
   10.17    HOLCF/Library/HOLCF_Library.thy \