1(*  Title:      HOL/HOLCF/Library/Char_Discrete.thy
2    Author:     Brian Huffman
3*)
4
5section \<open>Discrete cpo instance for 8-bit char type\<close>
6
7theory Char_Discrete
8imports HOLCF
9begin
10
11subsection \<open>Discrete cpo instance for @{typ char}.\<close>
12
13instantiation char :: discrete_cpo
14begin
15
16definition below_char_def:
17  "(x::char) \<sqsubseteq> y \<longleftrightarrow> x = y"
18
19instance proof
20qed (rule below_char_def)
21
22end
23
24text \<open>
25  TODO: implement a command to automate discrete predomain instances.
26\<close>
27
28instantiation char :: predomain
29begin
30
31definition
32  "(liftemb :: char u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)"
33
34definition
35  "(liftprj :: udom u \<rightarrow> char u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj"
36
37definition
38  "liftdefl \<equiv> (\<lambda>(t::char itself). LIFTDEFL(char discr))"
39
40instance proof
41  show "ep_pair liftemb (liftprj :: udom u \<rightarrow> char u)"
42    unfolding liftemb_char_def liftprj_char_def
43    apply (rule ep_pair_comp)
44    apply (rule ep_pair_u_map)
45    apply (simp add: ep_pair.intro)
46    apply (rule predomain_ep)
47    done
48  show "cast\<cdot>LIFTDEFL(char) = liftemb oo (liftprj :: udom u \<rightarrow> char u)"
49    unfolding liftemb_char_def liftprj_char_def liftdefl_char_def
50    apply (simp add: cast_liftdefl cfcomp1 u_map_map)
51    apply (simp add: ID_def [symmetric] u_map_ID)
52    done
53qed
54
55end
56
57end
58