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