author | immler |
Sun, 27 Oct 2019 21:51:14 -0400 | |
changeset 71035 | 6fe5a0e1fa8e |
parent 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Library/Bool_Discrete.thy |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
2 |
Author: Brian Huffman |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
3 |
*) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
4 |
|
62175 | 5 |
section \<open>Discrete cpo instance for booleans\<close> |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
6 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
7 |
theory Bool_Discrete |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
8 |
imports HOLCF |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
9 |
begin |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
10 |
|
69597 | 11 |
text \<open>Discrete cpo instance for \<^typ>\<open>bool\<close>.\<close> |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
12 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
13 |
instantiation bool :: discrete_cpo |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
14 |
begin |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
15 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
16 |
definition below_bool_def: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
17 |
"(x::bool) \<sqsubseteq> y \<longleftrightarrow> x = y" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
18 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
19 |
instance proof |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
20 |
qed (rule below_bool_def) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
21 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
22 |
end |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
23 |
|
62175 | 24 |
text \<open> |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
25 |
TODO: implement a command to automate discrete predomain instances. |
62175 | 26 |
\<close> |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
27 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
28 |
instantiation bool :: predomain |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
29 |
begin |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
30 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
31 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41112
diff
changeset
|
32 |
"(liftemb :: bool u \<rightarrow> udom u) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)" |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
33 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
34 |
definition |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41112
diff
changeset
|
35 |
"(liftprj :: udom u \<rightarrow> bool u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj" |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
36 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
37 |
definition |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
38 |
"liftdefl \<equiv> (\<lambda>(t::bool itself). LIFTDEFL(bool discr))" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
39 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
40 |
instance proof |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41112
diff
changeset
|
41 |
show "ep_pair liftemb (liftprj :: udom u \<rightarrow> bool u)" |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
42 |
unfolding liftemb_bool_def liftprj_bool_def |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
43 |
apply (rule ep_pair_comp) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
44 |
apply (rule ep_pair_u_map) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
45 |
apply (simp add: ep_pair.intro) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
46 |
apply (rule predomain_ep) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
47 |
done |
41292
2b7bc8d9fd6e
use deflations over type 'udom u' to represent predomains;
huffman
parents:
41112
diff
changeset
|
48 |
show "cast\<cdot>LIFTDEFL(bool) = liftemb oo (liftprj :: udom u \<rightarrow> bool u)" |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
49 |
unfolding liftemb_bool_def liftprj_bool_def liftdefl_bool_def |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
50 |
apply (simp add: cast_liftdefl cfcomp1 u_map_map) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
51 |
apply (simp add: ID_def [symmetric] u_map_ID) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
52 |
done |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
53 |
qed |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
54 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
55 |
end |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
56 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
57 |
lemma cont2cont_if [simp, cont2cont]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
58 |
assumes b: "cont b" and f: "cont f" and g: "cont g" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
59 |
shows "cont (\<lambda>x. if b x then f x else g x)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
60 |
by (rule cont_apply [OF b cont_discrete_cpo], simp add: f g) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
61 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
62 |
lemma cont2cont_eq [simp, cont2cont]: |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
63 |
fixes f g :: "'a::cpo \<Rightarrow> 'b::discrete_cpo" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
64 |
assumes f: "cont f" and g: "cont g" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
65 |
shows "cont (\<lambda>x. f x = g x)" |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
66 |
apply (rule cont_apply [OF f cont_discrete_cpo]) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
67 |
apply (rule cont_apply [OF g cont_discrete_cpo]) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
68 |
apply (rule cont_const) |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
69 |
done |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
70 |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
71 |
end |