equal
deleted
inserted
replaced
|
1 (* Title: HOLCF/Library/Nat_Discrete.thy |
|
2 Author: Brian Huffman |
|
3 *) |
|
4 |
|
5 header {* Discrete cpo instance for naturals *} |
|
6 |
|
7 theory Nat_Discrete |
|
8 imports HOLCF |
|
9 begin |
|
10 |
|
11 text {* Discrete cpo instance for @{typ nat}. *} |
|
12 |
|
13 instantiation nat :: discrete_cpo |
|
14 begin |
|
15 |
|
16 definition below_nat_def: |
|
17 "(x::nat) \<sqsubseteq> y \<longleftrightarrow> x = y" |
|
18 |
|
19 instance proof |
|
20 qed (rule below_nat_def) |
|
21 |
|
22 end |
|
23 |
|
24 text {* |
|
25 TODO: implement a command to automate discrete predomain instances. |
|
26 *} |
|
27 |
|
28 instantiation nat :: predomain |
|
29 begin |
|
30 |
|
31 definition |
|
32 "(liftemb :: nat u \<rightarrow> udom) \<equiv> liftemb oo u_map\<cdot>(\<Lambda> x. Discr x)" |
|
33 |
|
34 definition |
|
35 "(liftprj :: udom \<rightarrow> nat u) \<equiv> u_map\<cdot>(\<Lambda> y. undiscr y) oo liftprj" |
|
36 |
|
37 definition |
|
38 "liftdefl \<equiv> (\<lambda>(t::nat itself). LIFTDEFL(nat discr))" |
|
39 |
|
40 instance proof |
|
41 show "ep_pair liftemb (liftprj :: udom \<rightarrow> nat u)" |
|
42 unfolding liftemb_nat_def liftprj_nat_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(nat) = liftemb oo (liftprj :: udom \<rightarrow> nat u)" |
|
49 unfolding liftemb_nat_def liftprj_nat_def liftdefl_nat_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 end |