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