author | wenzelm |
Tue, 29 Mar 2011 17:47:11 +0200 | |
changeset 42151 | 4da4fc77664b |
parent 40774 | 0437dbc127b3 |
child 58880 | 0baae4311a9f |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Tutorial/New_Domain.thy |
33813 | 2 |
Author: Brian Huffman |
3 |
*) |
|
4 |
||
5 |
header {* Definitional domain package *} |
|
6 |
||
7 |
theory New_Domain |
|
8 |
imports HOLCF |
|
9 |
begin |
|
10 |
||
11 |
text {* |
|
40329
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
39986
diff
changeset
|
12 |
UPDATE: The definitional back-end is now the default mode of the domain |
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
39986
diff
changeset
|
13 |
package. This file should be merged with @{text Domain_ex.thy}. |
33813 | 14 |
*} |
15 |
||
16 |
text {* |
|
40497 | 17 |
Provided that @{text domain} is the default sort, the @{text new_domain} |
33813 | 18 |
package should work with any type definition supported by the old |
19 |
domain package. |
|
20 |
*} |
|
21 |
||
40329
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
39986
diff
changeset
|
22 |
domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist") |
33813 | 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 |
||
40329
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
39986
diff
changeset
|
39 |
domain 'a ltree = Leaf (lazy 'a) | Branch (lazy "'a ltree llist") |
33813 | 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 {* |
|
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
52 |
The definition of the take function uses map functions associated with |
33813 | 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 |
||
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
57 |
thm ltree.take_rews |
33813 | 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 - |
|
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
68 |
have "P (\<Squnion>i. ltree_take i\<cdot>x)" |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
69 |
using adm |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
70 |
proof (rule admD) |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
71 |
fix i |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
72 |
show "P (ltree_take i\<cdot>x)" |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
73 |
proof (induct i arbitrary: x) |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
74 |
case (0 x) |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
75 |
show "P (ltree_take 0\<cdot>x)" by (simp add: bot) |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
76 |
next |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
77 |
case (Suc n x) |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
78 |
show "P (ltree_take (Suc n)\<cdot>x)" |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
79 |
apply (cases x) |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
80 |
apply (simp add: bot) |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
81 |
apply (simp add: Leaf) |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
82 |
apply (simp add: Branch Suc) |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
83 |
done |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
84 |
qed |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
33813
diff
changeset
|
85 |
qed (simp add: ltree.chain_take) |
33813 | 86 |
thus ?thesis |
87 |
by (simp add: ltree.reach) |
|
88 |
qed |
|
89 |
||
90 |
end |