author | wenzelm |
Sat, 24 Mar 2018 20:51:42 +0100 | |
changeset 67945 | 984c3dc46cc0 |
parent 62175 | 8ffc4d0e652d |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Tutorial/New_Domain.thy |
33813 | 2 |
Author: Brian Huffman |
3 |
*) |
|
4 |
||
62175 | 5 |
section \<open>Definitional domain package\<close> |
33813 | 6 |
|
7 |
theory New_Domain |
|
8 |
imports HOLCF |
|
9 |
begin |
|
10 |
||
62175 | 11 |
text \<open> |
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 |
62175 | 13 |
package. This file should be merged with \<open>Domain_ex.thy\<close>. |
14 |
\<close> |
|
33813 | 15 |
|
62175 | 16 |
text \<open> |
17 |
Provided that \<open>domain\<close> is the default sort, the \<open>new_domain\<close> |
|
33813 | 18 |
package should work with any type definition supported by the old |
19 |
domain package. |
|
62175 | 20 |
\<close> |
33813 | 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 |
|
62175 | 24 |
text \<open> |
33813 | 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. |
|
62175 | 28 |
\<close> |
33813 | 29 |
|
30 |
thm type_definition_llist |
|
31 |
thm llist_abs_def llist_rep_def |
|
32 |
||
62175 | 33 |
text \<open> |
33813 | 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. |
|
62175 | 37 |
\<close> |
33813 | 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 |
|
62175 | 41 |
text \<open> |
33813 | 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. |
|
62175 | 47 |
\<close> |
33813 | 48 |
|
49 |
thm ltree.reach |
|
50 |
||
62175 | 51 |
text \<open> |
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. |
|
62175 | 55 |
\<close> |
33813 | 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 |