|
1 (* Title: HOLCF/ex/New_Domain.thy |
|
2 Author: Brian Huffman |
|
3 *) |
|
4 |
|
5 header {* Definitional domain package *} |
|
6 |
|
7 theory New_Domain |
|
8 imports HOLCF |
|
9 begin |
|
10 |
|
11 text {* |
|
12 UPDATE: The definitional back-end is now the default mode of the domain |
|
13 package. This file should be merged with @{text Domain_ex.thy}. |
|
14 *} |
|
15 |
|
16 text {* |
|
17 Provided that @{text domain} is the default sort, the @{text new_domain} |
|
18 package should work with any type definition supported by the old |
|
19 domain package. |
|
20 *} |
|
21 |
|
22 domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist") |
|
23 |
|
24 text {* |
|
25 The difference is that the new domain package is completely |
|
26 definitional, and does not generate any axioms. The following type |
|
27 and constant definitions are not produced by the old domain package. |
|
28 *} |
|
29 |
|
30 thm type_definition_llist |
|
31 thm llist_abs_def llist_rep_def |
|
32 |
|
33 text {* |
|
34 The new domain package also adds support for indirect recursion with |
|
35 user-defined datatypes. This definition of a tree datatype uses |
|
36 indirect recursion through the lazy list type constructor. |
|
37 *} |
|
38 |
|
39 domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist") |
|
40 |
|
41 text {* |
|
42 For indirect-recursive definitions, the domain package is not able to |
|
43 generate a high-level induction rule. (It produces a warning |
|
44 message instead.) The low-level reach lemma (now proved as a |
|
45 theorem, no longer generated as an axiom) can be used to derive |
|
46 other induction rules. |
|
47 *} |
|
48 |
|
49 thm ltree.reach |
|
50 |
|
51 text {* |
|
52 The definition of the take function uses map functions associated with |
|
53 each type constructor involved in the definition. A map function |
|
54 for the lazy list type has been generated by the new domain package. |
|
55 *} |
|
56 |
|
57 thm ltree.take_rews |
|
58 thm llist_map_def |
|
59 |
|
60 lemma ltree_induct: |
|
61 fixes P :: "'a ltree \<Rightarrow> bool" |
|
62 assumes adm: "adm P" |
|
63 assumes bot: "P \<bottom>" |
|
64 assumes Leaf: "\<And>x. P (Leaf\<cdot>x)" |
|
65 assumes Branch: "\<And>f l. \<forall>x. P (f\<cdot>x) \<Longrightarrow> P (Branch\<cdot>(llist_map\<cdot>f\<cdot>l))" |
|
66 shows "P x" |
|
67 proof - |
|
68 have "P (\<Squnion>i. ltree_take i\<cdot>x)" |
|
69 using adm |
|
70 proof (rule admD) |
|
71 fix i |
|
72 show "P (ltree_take i\<cdot>x)" |
|
73 proof (induct i arbitrary: x) |
|
74 case (0 x) |
|
75 show "P (ltree_take 0\<cdot>x)" by (simp add: bot) |
|
76 next |
|
77 case (Suc n x) |
|
78 show "P (ltree_take (Suc n)\<cdot>x)" |
|
79 apply (cases x) |
|
80 apply (simp add: bot) |
|
81 apply (simp add: Leaf) |
|
82 apply (simp add: Branch Suc) |
|
83 done |
|
84 qed |
|
85 qed (simp add: ltree.chain_take) |
|
86 thus ?thesis |
|
87 by (simp add: ltree.reach) |
|
88 qed |
|
89 |
|
90 end |