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