equal
deleted
inserted
replaced
1 (* Title: HOL/HOLCF/Library/Int_Discrete.thy |
1 (* Title: HOL/HOLCF/Library/Int_Discrete.thy |
2 Author: Brian Huffman |
2 Author: Brian Huffman |
3 *) |
3 *) |
4 |
4 |
5 section {* Discrete cpo instance for integers *} |
5 section \<open>Discrete cpo instance for integers\<close> |
6 |
6 |
7 theory Int_Discrete |
7 theory Int_Discrete |
8 imports HOLCF |
8 imports HOLCF |
9 begin |
9 begin |
10 |
10 |
11 text {* Discrete cpo instance for @{typ int}. *} |
11 text \<open>Discrete cpo instance for @{typ int}.\<close> |
12 |
12 |
13 instantiation int :: discrete_cpo |
13 instantiation int :: discrete_cpo |
14 begin |
14 begin |
15 |
15 |
16 definition below_int_def: |
16 definition below_int_def: |
19 instance proof |
19 instance proof |
20 qed (rule below_int_def) |
20 qed (rule below_int_def) |
21 |
21 |
22 end |
22 end |
23 |
23 |
24 text {* |
24 text \<open> |
25 TODO: implement a command to automate discrete predomain instances. |
25 TODO: implement a command to automate discrete predomain instances. |
26 *} |
26 \<close> |
27 |
27 |
28 instantiation int :: predomain |
28 instantiation int :: predomain |
29 begin |
29 begin |
30 |
30 |
31 definition |
31 definition |