equal
deleted
inserted
replaced
7 theory New_Domain |
7 theory New_Domain |
8 imports HOLCF |
8 imports HOLCF |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text {* |
12 The definitional domain package only works with bifinite domains, |
12 UPDATE: The definitional back-end is now the default mode of the domain |
13 i.e. types in class @{text bifinite}. |
13 package. This file should be merged with @{text Domain_ex.thy}. |
14 *} |
14 *} |
15 |
15 |
16 default_sort bifinite |
16 default_sort bifinite |
17 |
17 |
18 text {* |
18 text {* |
19 Provided that @{text bifinite} is the default sort, the @{text new_domain} |
19 Provided that @{text bifinite} is the default sort, the @{text new_domain} |
20 package should work with any type definition supported by the old |
20 package should work with any type definition supported by the old |
21 domain package. |
21 domain package. |
22 *} |
22 *} |
23 |
23 |
24 new_domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist") |
24 domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist") |
25 |
25 |
26 text {* |
26 text {* |
27 The difference is that the new domain package is completely |
27 The difference is that the new domain package is completely |
28 definitional, and does not generate any axioms. The following type |
28 definitional, and does not generate any axioms. The following type |
29 and constant definitions are not produced by the old domain package. |
29 and constant definitions are not produced by the old domain package. |
36 The new domain package also adds support for indirect recursion with |
36 The new domain package also adds support for indirect recursion with |
37 user-defined datatypes. This definition of a tree datatype uses |
37 user-defined datatypes. This definition of a tree datatype uses |
38 indirect recursion through the lazy list type constructor. |
38 indirect recursion through the lazy list type constructor. |
39 *} |
39 *} |
40 |
40 |
41 new_domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist") |
41 domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist") |
42 |
42 |
43 text {* |
43 text {* |
44 For indirect-recursive definitions, the domain package is not able to |
44 For indirect-recursive definitions, the domain package is not able to |
45 generate a high-level induction rule. (It produces a warning |
45 generate a high-level induction rule. (It produces a warning |
46 message instead.) The low-level reach lemma (now proved as a |
46 message instead.) The low-level reach lemma (now proved as a |