author | huffman |
Wed, 10 Nov 2010 14:59:52 -0800 | |
changeset 40501 | 2ed71459136e |
parent 40329 | 73f2b99b549d |
permissions | -rw-r--r-- |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
1 |
(* Title: HOLCF/ex/Domain_ex.thy |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
2 |
Author: Brian Huffman |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
3 |
*) |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
4 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
5 |
header {* Domain package examples *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
6 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
7 |
theory Domain_ex |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
8 |
imports HOLCF |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
9 |
begin |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
10 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
11 |
text {* Domain constructors are strict by default. *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
12 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
13 |
domain d1 = d1a | d1b "d1" "d1" |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
14 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
15 |
lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
16 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
17 |
text {* Constructors can be made lazy using the @{text "lazy"} keyword. *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
18 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
19 |
domain d2 = d2a | d2b (lazy "d2") |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
20 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
21 |
lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
22 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
23 |
text {* Strict and lazy arguments may be mixed arbitrarily. *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
24 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
25 |
domain d3 = d3a | d3b (lazy "d2") "d2" |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
26 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
27 |
lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
28 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
29 |
text {* Selectors can be used with strict or lazy constructor arguments. *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
30 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
31 |
domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2") |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
32 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
33 |
lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
34 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
35 |
text {* Mixfix declarations can be given for data constructors. *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
36 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
37 |
domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70) |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
38 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
39 |
lemma "d5a \<noteq> x :#: y :#: z" by simp |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
40 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
41 |
text {* Mixfix declarations can also be given for type constructors. *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
42 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
43 |
domain ('a, 'b) lazypair (infixl ":*:" 25) = |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
44 |
lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75) |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
45 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
46 |
lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p" |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
47 |
by (rule allI, case_tac p, simp_all) |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
48 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
49 |
text {* Non-recursive constructor arguments can have arbitrary types. *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
50 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
51 |
domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)") |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
52 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
53 |
text {* |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
54 |
Indirect recusion is allowed for sums, products, lifting, and the |
35585
555f26f00e47
skip proof of induction rule for indirect-recursive domain definitions
huffman
parents:
35497
diff
changeset
|
55 |
continuous function space. However, the domain package does not |
555f26f00e47
skip proof of induction rule for indirect-recursive domain definitions
huffman
parents:
35497
diff
changeset
|
56 |
generate an induction rule in terms of the constructors. |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
57 |
*} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
58 |
|
31232
689aa7da48cc
define copy functions using combinators; add checking for failed proofs of induction rules
huffman
parents:
30922
diff
changeset
|
59 |
domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a") |
36120 | 60 |
-- "Indirect recursion detected, skipping proofs of (co)induction rules" |
37000
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
36120
diff
changeset
|
61 |
|
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
36120
diff
changeset
|
62 |
text {* Note that @{text d7.induct} is absent. *} |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
63 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
64 |
text {* |
36120 | 65 |
Indirect recursion is also allowed using previously-defined datatypes. |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
66 |
*} |
36120 | 67 |
|
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
68 |
domain 'a slist = SNil | SCons 'a "'a slist" |
36120 | 69 |
|
70 |
domain 'a stree = STip | SBranch "'a stree slist" |
|
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
71 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
72 |
text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
73 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
74 |
domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8") |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
75 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
76 |
text {* Non-regular recursion is not allowed. *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
77 |
(* |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
78 |
domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist" |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
79 |
-- "illegal direct recursion with different arguments" |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
80 |
domain 'a nest = Nest1 'a | Nest2 "'a nest nest" |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
81 |
-- "illegal direct recursion with different arguments" |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
82 |
*) |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
83 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
84 |
text {* |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
85 |
Mutually-recursive datatypes must have all the same type arguments, |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
86 |
not necessarily in the same order. |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
87 |
*} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
88 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
89 |
domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2" |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
90 |
and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1" |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
91 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
92 |
text {* Induction rules for flat datatypes have no admissibility side-condition. *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
93 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
94 |
domain 'a flattree = Tip | Branch "'a flattree" "'a flattree" |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
95 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
96 |
lemma "\<lbrakk>P \<bottom>; P Tip; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; P x; P y\<rbrakk> \<Longrightarrow> P (Branch\<cdot>x\<cdot>y)\<rbrakk> \<Longrightarrow> P x" |
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35661
diff
changeset
|
97 |
by (rule flattree.induct) -- "no admissibility requirement" |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
98 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
99 |
text {* Trivial datatypes will produce a warning message. *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
100 |
|
35443
2e0f9516947e
change domain package's treatment of variable names in theorems to be like datatype package
huffman
parents:
31232
diff
changeset
|
101 |
domain triv = Triv triv triv |
37000
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
36120
diff
changeset
|
102 |
-- "domain @{text Domain_ex.triv} is empty!" |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
103 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
104 |
lemma "(x::triv) = \<bottom>" by (induct x, simp_all) |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
105 |
|
36120 | 106 |
text {* Lazy constructor arguments may have unpointed types. *} |
107 |
||
40501
2ed71459136e
allow unpointed lazy arguments for definitional domain package
huffman
parents:
40329
diff
changeset
|
108 |
domain natlist = nnil | ncons (lazy "nat discr") natlist |
36120 | 109 |
|
110 |
text {* Class constraints may be given for type parameters on the LHS. *} |
|
111 |
||
40501
2ed71459136e
allow unpointed lazy arguments for definitional domain package
huffman
parents:
40329
diff
changeset
|
112 |
domain ('a::predomain) box = Box (lazy 'a) |
40329
73f2b99b549d
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents:
40321
diff
changeset
|
113 |
|
40501
2ed71459136e
allow unpointed lazy arguments for definitional domain package
huffman
parents:
40329
diff
changeset
|
114 |
domain ('a::countable) stream = snil | scons (lazy "'a discr") "'a stream" |
36120 | 115 |
|
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
116 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
117 |
subsection {* Generated constants and theorems *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
118 |
|
35661
ede27eb8e94b
don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule
huffman
parents:
35642
diff
changeset
|
119 |
domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree") |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
120 |
|
40321
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40213
diff
changeset
|
121 |
lemmas tree_abs_bottom_iff = |
d065b195ec89
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
huffman
parents:
40213
diff
changeset
|
122 |
iso.abs_bottom_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]] |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
123 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
124 |
text {* Rules about ismorphism *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
125 |
term tree_rep |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
126 |
term tree_abs |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
127 |
thm tree.rep_iso |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
128 |
thm tree.abs_iso |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
129 |
thm tree.iso_rews |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
130 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
131 |
text {* Rules about constructors *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
132 |
term Leaf |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
133 |
term Node |
35444 | 134 |
thm Leaf_def Node_def |
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35661
diff
changeset
|
135 |
thm tree.nchotomy |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
136 |
thm tree.exhaust |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
137 |
thm tree.compacts |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
138 |
thm tree.con_rews |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
139 |
thm tree.dist_les |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
140 |
thm tree.dist_eqs |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
141 |
thm tree.inverts |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
142 |
thm tree.injects |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
143 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
144 |
text {* Rules about case combinator *} |
40213
b63e966564da
rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
huffman
parents:
37109
diff
changeset
|
145 |
term tree_case |
b63e966564da
rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
huffman
parents:
37109
diff
changeset
|
146 |
thm tree.tree_case_def |
b63e966564da
rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
huffman
parents:
37109
diff
changeset
|
147 |
thm tree.case_rews |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
148 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
149 |
text {* Rules about selectors *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
150 |
term left |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
151 |
term right |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
152 |
thm tree.sel_rews |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
153 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
154 |
text {* Rules about discriminators *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
155 |
term is_Leaf |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
156 |
term is_Node |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
157 |
thm tree.dis_rews |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
158 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
159 |
text {* Rules about monadic pattern match combinators *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
160 |
term match_Leaf |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
161 |
term match_Node |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
162 |
thm tree.match_rews |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
163 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
164 |
text {* Rules about take function *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
165 |
term tree_take |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
166 |
thm tree.take_def |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35444
diff
changeset
|
167 |
thm tree.take_0 |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35444
diff
changeset
|
168 |
thm tree.take_Suc |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
169 |
thm tree.take_rews |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35444
diff
changeset
|
170 |
thm tree.chain_take |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35444
diff
changeset
|
171 |
thm tree.take_take |
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35444
diff
changeset
|
172 |
thm tree.deflation_take |
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35661
diff
changeset
|
173 |
thm tree.take_below |
35642
f478d5a9d238
generate separate qualified theorem name for each type's reach and take_lemma
huffman
parents:
35585
diff
changeset
|
174 |
thm tree.take_lemma |
35585
555f26f00e47
skip proof of induction rule for indirect-recursive domain definitions
huffman
parents:
35497
diff
changeset
|
175 |
thm tree.lub_take |
35494
45c9a8278faf
domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents:
35444
diff
changeset
|
176 |
thm tree.reach |
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35661
diff
changeset
|
177 |
thm tree.finite_induct |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
178 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
179 |
text {* Rules about finiteness predicate *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
180 |
term tree_finite |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
181 |
thm tree.finite_def |
35661
ede27eb8e94b
don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule
huffman
parents:
35642
diff
changeset
|
182 |
thm tree.finite (* only generated for flat datatypes *) |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
183 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
184 |
text {* Rules about bisimulation predicate *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
185 |
term tree_bisim |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
186 |
thm tree.bisim_def |
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35661
diff
changeset
|
187 |
thm tree.coinduct |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
188 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
189 |
text {* Induction rule *} |
35781
b7738ab762b1
renamed some lemmas generated by the domain package
huffman
parents:
35661
diff
changeset
|
190 |
thm tree.induct |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
191 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
192 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
193 |
subsection {* Known bugs *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
194 |
|
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
195 |
text {* Declaring a mixfix with spaces causes some strange parse errors. *} |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
196 |
(* |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
197 |
domain xx = xx ("x y") |
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
198 |
-- "Inner syntax error: unexpected end of input" |
30922 | 199 |
*) |
200 |
||
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
diff
changeset
|
201 |
end |