1(* Title: HOL/HOLCF/Library/Bool_Discrete.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Discrete cpo instance for booleans\<close> 6 7theory Bool_Discrete 8imports HOLCF 9begin 10 11text \<open>Discrete cpo instance for @{typ bool}.\<close> 12 13instantiation bool :: discrete_cpo 14begin 15 16definition below_bool_def: 17 "(x::bool) \<sqsubseteq> y \<longleftrightarrow> x = y" 18 19instance proof 20qed (rule below_bool_def) 21 22end 23 24text \<open> 25 TODO: implement a command to automate discrete predomain instances. 26\<close> 27 28instantiation bool :: predomain 29begin 30 31definition 32 "(liftemb :: bool u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)" 33 34definition 35 "(liftprj :: udom u \<rightarrow> bool u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj" 36 37definition 38 "liftdefl \<equiv> (\<lambda>(t::bool itself). LIFTDEFL(bool discr))" 39 40instance proof 41 show "ep_pair liftemb (liftprj :: udom u \<rightarrow> bool u)" 42 unfolding liftemb_bool_def liftprj_bool_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(bool) = liftemb oo (liftprj :: udom u \<rightarrow> bool u)" 49 unfolding liftemb_bool_def liftprj_bool_def liftdefl_bool_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 57lemma cont2cont_if [simp, cont2cont]: 58 assumes b: "cont b" and f: "cont f" and g: "cont g" 59 shows "cont (\<lambda>x. if b x then f x else g x)" 60by (rule cont_apply [OF b cont_discrete_cpo], simp add: f g) 61 62lemma cont2cont_eq [simp, cont2cont]: 63 fixes f g :: "'a::cpo \<Rightarrow> 'b::discrete_cpo" 64 assumes f: "cont f" and g: "cont g" 65 shows "cont (\<lambda>x. f x = g x)" 66apply (rule cont_apply [OF f cont_discrete_cpo]) 67apply (rule cont_apply [OF g cont_discrete_cpo]) 68apply (rule cont_const) 69done 70 71end 72