1 (* Title: HOLCF/ex/Domain_ex.thy |
|
2 Author: Brian Huffman |
|
3 *) |
|
4 |
|
5 header {* Domain package examples *} |
|
6 |
|
7 theory Domain_ex |
|
8 imports HOLCF |
|
9 begin |
|
10 |
|
11 text {* Domain constructors are strict by default. *} |
|
12 |
|
13 domain d1 = d1a | d1b "d1" "d1" |
|
14 |
|
15 lemma "d1b\<cdot>\<bottom>\<cdot>y = \<bottom>" by simp |
|
16 |
|
17 text {* Constructors can be made lazy using the @{text "lazy"} keyword. *} |
|
18 |
|
19 domain d2 = d2a | d2b (lazy "d2") |
|
20 |
|
21 lemma "d2b\<cdot>x \<noteq> \<bottom>" by simp |
|
22 |
|
23 text {* Strict and lazy arguments may be mixed arbitrarily. *} |
|
24 |
|
25 domain d3 = d3a | d3b (lazy "d2") "d2" |
|
26 |
|
27 lemma "P (d3b\<cdot>x\<cdot>y = \<bottom>) \<longleftrightarrow> P (y = \<bottom>)" by simp |
|
28 |
|
29 text {* Selectors can be used with strict or lazy constructor arguments. *} |
|
30 |
|
31 domain d4 = d4a | d4b (lazy d4b_left :: "d2") (d4b_right :: "d2") |
|
32 |
|
33 lemma "y \<noteq> \<bottom> \<Longrightarrow> d4b_left\<cdot>(d4b\<cdot>x\<cdot>y) = x" by simp |
|
34 |
|
35 text {* Mixfix declarations can be given for data constructors. *} |
|
36 |
|
37 domain d5 = d5a | d5b (lazy "d5") "d5" (infixl ":#:" 70) |
|
38 |
|
39 lemma "d5a \<noteq> x :#: y :#: z" by simp |
|
40 |
|
41 text {* Mixfix declarations can also be given for type constructors. *} |
|
42 |
|
43 domain ('a, 'b) lazypair (infixl ":*:" 25) = |
|
44 lpair (lazy lfst :: 'a) (lazy lsnd :: 'b) (infixl ":*:" 75) |
|
45 |
|
46 lemma "\<forall>p::('a :*: 'b). p \<sqsubseteq> lfst\<cdot>p :*: lsnd\<cdot>p" |
|
47 by (rule allI, case_tac p, simp_all) |
|
48 |
|
49 text {* Non-recursive constructor arguments can have arbitrary types. *} |
|
50 |
|
51 domain ('a, 'b) d6 = d6 "int lift" "'a \<oplus> 'b u" (lazy "('a :*: 'b) \<times> ('b \<rightarrow> 'a)") |
|
52 |
|
53 text {* |
|
54 Indirect recusion is allowed for sums, products, lifting, and the |
|
55 continuous function space. However, the domain package does not |
|
56 generate an induction rule in terms of the constructors. |
|
57 *} |
|
58 |
|
59 domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a") |
|
60 -- "Indirect recursion detected, skipping proofs of (co)induction rules" |
|
61 (* d7.induct is absent *) |
|
62 |
|
63 text {* |
|
64 Indirect recursion is also allowed using previously-defined datatypes. |
|
65 *} |
|
66 |
|
67 domain 'a slist = SNil | SCons 'a "'a slist" |
|
68 |
|
69 domain 'a stree = STip | SBranch "'a stree slist" |
|
70 |
|
71 text {* Mutually-recursive datatypes can be defined using the @{text "and"} keyword. *} |
|
72 |
|
73 domain d8 = d8a | d8b "d9" and d9 = d9a | d9b (lazy "d8") |
|
74 |
|
75 text {* Non-regular recursion is not allowed. *} |
|
76 (* |
|
77 domain ('a, 'b) altlist = ANil | ACons 'a "('b, 'a) altlist" |
|
78 -- "illegal direct recursion with different arguments" |
|
79 domain 'a nest = Nest1 'a | Nest2 "'a nest nest" |
|
80 -- "illegal direct recursion with different arguments" |
|
81 *) |
|
82 |
|
83 text {* |
|
84 Mutually-recursive datatypes must have all the same type arguments, |
|
85 not necessarily in the same order. |
|
86 *} |
|
87 |
|
88 domain ('a, 'b) list1 = Nil1 | Cons1 'a "('b, 'a) list2" |
|
89 and ('b, 'a) list2 = Nil2 | Cons2 'b "('a, 'b) list1" |
|
90 |
|
91 text {* Induction rules for flat datatypes have no admissibility side-condition. *} |
|
92 |
|
93 domain 'a flattree = Tip | Branch "'a flattree" "'a flattree" |
|
94 |
|
95 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" |
|
96 by (rule flattree.induct) -- "no admissibility requirement" |
|
97 |
|
98 text {* Trivial datatypes will produce a warning message. *} |
|
99 |
|
100 domain triv = Triv triv triv |
|
101 -- "domain Domain_ex.triv is empty!" |
|
102 |
|
103 lemma "(x::triv) = \<bottom>" by (induct x, simp_all) |
|
104 |
|
105 text {* Lazy constructor arguments may have unpointed types. *} |
|
106 |
|
107 domain natlist = nnil | ncons (lazy "nat discr") natlist |
|
108 |
|
109 text {* Class constraints may be given for type parameters on the LHS. *} |
|
110 |
|
111 domain ('a::cpo) box = Box (lazy 'a) |
|
112 |
|
113 |
|
114 subsection {* Generated constants and theorems *} |
|
115 |
|
116 domain 'a tree = Leaf (lazy 'a) | Node (left :: "'a tree") (right :: "'a tree") |
|
117 |
|
118 lemmas tree_abs_defined_iff = |
|
119 iso.abs_defined_iff [OF iso.intro [OF tree.abs_iso tree.rep_iso]] |
|
120 |
|
121 text {* Rules about ismorphism *} |
|
122 term tree_rep |
|
123 term tree_abs |
|
124 thm tree.rep_iso |
|
125 thm tree.abs_iso |
|
126 thm tree.iso_rews |
|
127 |
|
128 text {* Rules about constructors *} |
|
129 term Leaf |
|
130 term Node |
|
131 thm Leaf_def Node_def |
|
132 thm tree.nchotomy |
|
133 thm tree.exhaust |
|
134 thm tree.compacts |
|
135 thm tree.con_rews |
|
136 thm tree.dist_les |
|
137 thm tree.dist_eqs |
|
138 thm tree.inverts |
|
139 thm tree.injects |
|
140 |
|
141 text {* Rules about case combinator *} |
|
142 term tree_when |
|
143 thm tree.tree_when_def |
|
144 thm tree.when_rews |
|
145 |
|
146 text {* Rules about selectors *} |
|
147 term left |
|
148 term right |
|
149 thm tree.sel_rews |
|
150 |
|
151 text {* Rules about discriminators *} |
|
152 term is_Leaf |
|
153 term is_Node |
|
154 thm tree.dis_rews |
|
155 |
|
156 text {* Rules about pattern match combinators *} |
|
157 term Leaf_pat |
|
158 term Node_pat |
|
159 thm tree.pat_rews |
|
160 |
|
161 text {* Rules about monadic pattern match combinators *} |
|
162 term match_Leaf |
|
163 term match_Node |
|
164 thm tree.match_rews |
|
165 |
|
166 text {* Rules about take function *} |
|
167 term tree_take |
|
168 thm tree.take_def |
|
169 thm tree.take_0 |
|
170 thm tree.take_Suc |
|
171 thm tree.take_rews |
|
172 thm tree.chain_take |
|
173 thm tree.take_take |
|
174 thm tree.deflation_take |
|
175 thm tree.take_below |
|
176 thm tree.take_lemma |
|
177 thm tree.lub_take |
|
178 thm tree.reach |
|
179 thm tree.finite_induct |
|
180 |
|
181 text {* Rules about finiteness predicate *} |
|
182 term tree_finite |
|
183 thm tree.finite_def |
|
184 thm tree.finite (* only generated for flat datatypes *) |
|
185 |
|
186 text {* Rules about bisimulation predicate *} |
|
187 term tree_bisim |
|
188 thm tree.bisim_def |
|
189 thm tree.coinduct |
|
190 |
|
191 text {* Induction rule *} |
|
192 thm tree.induct |
|
193 |
|
194 |
|
195 subsection {* Known bugs *} |
|
196 |
|
197 text {* Declaring a mixfix with spaces causes some strange parse errors. *} |
|
198 (* |
|
199 domain xx = xx ("x y") |
|
200 -- "Inner syntax error: unexpected end of input" |
|
201 *) |
|
202 |
|
203 text {* |
|
204 Non-cpo type parameters currently do not work. |
|
205 *} |
|
206 (* |
|
207 domain ('a::type) stream = snil | scons (lazy "'a discr") "'a stream" |
|
208 *) |
|
209 |
|
210 end |
|