author | wenzelm |
Sun, 02 Nov 2014 18:21:45 +0100 | |
changeset 58889 | 5b7a9633cfa8 |
parent 58442 | 039b54d9b5c4 |
child 63167 | 0909deb8059b |
permissions | -rw-r--r-- |
58309
a09ec6daaa19
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
blanchet
parents:
58305
diff
changeset
|
1 |
(* Title: HOL/Datatype_Examples/Compat.thy |
57634 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
Copyright 2014 |
|
4 |
||
5 |
Tests for compatibility with the old datatype package. |
|
6 |
*) |
|
7 |
||
58889 | 8 |
section {* Tests for Compatibility with the Old Datatype Package *} |
57634 | 9 |
|
56454 | 10 |
theory Compat |
58372
bfd497f2f4c2
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents:
58358
diff
changeset
|
11 |
imports "~~/src/HOL/Library/Old_Datatype" |
56454 | 12 |
begin |
13 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
14 |
subsection {* Viewing and Registering New-Style Datatypes as Old-Style Ones *} |
58125 | 15 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
16 |
ML {* |
58124 | 17 |
fun check_len n xs label = |
18 |
length xs = n orelse error ("Expected length " ^ string_of_int (length xs) ^ " for " ^ label); |
|
19 |
||
20 |
fun check_lens (n1, n2, n3) (xs1, xs2, xs3) = |
|
21 |
check_len n1 xs1 "old" andalso check_len n2 xs2 "unfold" andalso check_len n3 xs3 "keep"; |
|
22 |
||
23 |
fun get_descrs thy lens T_name = |
|
24 |
(these (Option.map #descr (Old_Datatype_Data.get_info thy T_name)), |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
25 |
these (Option.map #descr (BNF_LFP_Compat.get_info thy [] T_name)), |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
26 |
these (Option.map #descr (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] T_name))) |
58124 | 27 |
|> tap (check_lens lens); |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
28 |
*} |
58124 | 29 |
|
58305
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
58216
diff
changeset
|
30 |
old_datatype 'a old_lst = Old_Nl | Old_Cns 'a "'a old_lst" |
58124 | 31 |
|
58392 | 32 |
text {* |
33 |
A few tests to make sure that @{text old_datatype} works as expected: |
|
34 |
*} |
|
35 |
||
36 |
primrec old_len :: "'a old_lst \<Rightarrow> nat" where |
|
37 |
"old_len Old_Nl = 0" |
|
38 |
| "old_len (Old_Cns _ xs) = Suc (old_len xs)" |
|
39 |
||
40 |
export_code old_len checking SML OCaml? Haskell? Scala |
|
41 |
||
42 |
lemma "Old_Nl = Old_Cns x xs" |
|
58442
039b54d9b5c4
commented out some tests that require external tools (e.g. ghc)
blanchet
parents:
58392
diff
changeset
|
43 |
nitpick (* [expect = genuine] *) |
58392 | 44 |
quickcheck [exhaustive, expect = counterexample] |
45 |
quickcheck [random, expect = counterexample] |
|
58442
039b54d9b5c4
commented out some tests that require external tools (e.g. ghc)
blanchet
parents:
58392
diff
changeset
|
46 |
quickcheck [narrowing (* , expect = counterexample *)] |
58392 | 47 |
oops |
48 |
||
49 |
lemma "old_len xs = size xs" |
|
50 |
by (induct xs) auto |
|
51 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
52 |
ML {* get_descrs @{theory} (1, 1, 1) @{type_name old_lst} *} |
58124 | 53 |
|
58310 | 54 |
datatype 'a lst = Nl | Cns 'a "'a lst" |
58124 | 55 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
56 |
ML {* get_descrs @{theory} (0, 1, 1) @{type_name lst} *} |
58124 | 57 |
|
56454 | 58 |
datatype_compat lst |
59 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
60 |
ML {* get_descrs @{theory} (1, 1, 1) @{type_name lst} *} |
58124 | 61 |
|
58310 | 62 |
datatype 'b w = W | W' "'b w \<times> 'b list" |
58124 | 63 |
|
58358 | 64 |
ML {* get_descrs @{theory} (0, 1, 1) @{type_name w} *} |
65 |
||
56454 | 66 |
datatype_compat w |
67 |
||
58358 | 68 |
ML {* get_descrs @{theory} (2, 2, 1) @{type_name w} *} |
58124 | 69 |
|
58310 | 70 |
datatype ('c, 'b) s = L 'c | R 'b |
58124 | 71 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
72 |
ML {* get_descrs @{theory} (0, 1, 1) @{type_name s} *} |
58124 | 73 |
|
58310 | 74 |
datatype 'd x = X | X' "('d x lst, 'd list) s" |
58124 | 75 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
76 |
ML {* get_descrs @{theory} (0, 1, 1) @{type_name x} *} |
58124 | 77 |
|
56454 | 78 |
datatype_compat s |
58124 | 79 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
80 |
ML {* get_descrs @{theory} (1, 1, 1) @{type_name s} *} |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
81 |
ML {* get_descrs @{theory} (0, 1, 1) @{type_name x} *} |
58124 | 82 |
|
56454 | 83 |
datatype_compat x |
84 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
85 |
ML {* get_descrs @{theory} (3, 3, 1) @{type_name x} *} |
58124 | 86 |
|
58216 | 87 |
thm x.induct x.rec |
88 |
thm compat_x.induct compat_x.rec |
|
89 |
||
58310 | 90 |
datatype 'a tttre = TTTre 'a "'a tttre lst lst lst" |
58124 | 91 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
92 |
ML {* get_descrs @{theory} (0, 1, 1) @{type_name tttre} *} |
58124 | 93 |
|
56454 | 94 |
datatype_compat tttre |
95 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
96 |
ML {* get_descrs @{theory} (4, 4, 1) @{type_name tttre} *} |
58124 | 97 |
|
58216 | 98 |
thm tttre.induct tttre.rec |
99 |
thm compat_tttre.induct compat_tttre.rec |
|
100 |
||
58310 | 101 |
datatype 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre lst" |
58124 | 102 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
103 |
ML {* get_descrs @{theory} (0, 1, 1) @{type_name ftre} *} |
58124 | 104 |
|
56454 | 105 |
datatype_compat ftre |
106 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
107 |
ML {* get_descrs @{theory} (2, 2, 1) @{type_name ftre} *} |
58124 | 108 |
|
58216 | 109 |
thm ftre.induct ftre.rec |
110 |
thm compat_ftre.induct compat_ftre.rec |
|
111 |
||
58310 | 112 |
datatype 'a btre = BTre 'a "'a btre lst" "'a btre lst" |
58124 | 113 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
114 |
ML {* get_descrs @{theory} (0, 1, 1) @{type_name btre} *} |
58124 | 115 |
|
56454 | 116 |
datatype_compat btre |
117 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
118 |
ML {* get_descrs @{theory} (3, 3, 1) @{type_name btre} *} |
58124 | 119 |
|
58216 | 120 |
thm btre.induct btre.rec |
121 |
thm compat_btre.induct compat_btre.rec |
|
122 |
||
58310 | 123 |
datatype 'a foo = Foo | Foo' 'a "'a bar" and 'a bar = Bar | Bar' 'a "'a foo" |
58124 | 124 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
125 |
ML {* get_descrs @{theory} (0, 2, 2) @{type_name foo} *} |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
126 |
ML {* get_descrs @{theory} (0, 2, 2) @{type_name bar} *} |
58124 | 127 |
|
56454 | 128 |
datatype_compat foo bar |
129 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
130 |
ML {* get_descrs @{theory} (2, 2, 2) @{type_name foo} *} |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
131 |
ML {* get_descrs @{theory} (2, 2, 2) @{type_name bar} *} |
58124 | 132 |
|
58310 | 133 |
datatype 'a tre = Tre 'a "'a tre lst" |
58124 | 134 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
135 |
ML {* get_descrs @{theory} (0, 1, 1) @{type_name tre} *} |
58124 | 136 |
|
56454 | 137 |
datatype_compat tre |
138 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
139 |
ML {* get_descrs @{theory} (2, 2, 1) @{type_name tre} *} |
58124 | 140 |
|
58216 | 141 |
thm tre.induct tre.rec |
142 |
thm compat_tre.induct compat_tre.rec |
|
56454 | 143 |
|
58310 | 144 |
datatype 'a f = F 'a and 'a g = G 'a |
58124 | 145 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
146 |
ML {* get_descrs @{theory} (0, 2, 2) @{type_name f} *} |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
147 |
ML {* get_descrs @{theory} (0, 2, 2) @{type_name g} *} |
58124 | 148 |
|
58310 | 149 |
datatype h = H "h f" | H' |
58124 | 150 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
151 |
ML {* get_descrs @{theory} (0, 1, 1) @{type_name h} *} |
58124 | 152 |
|
56454 | 153 |
datatype_compat f g |
58124 | 154 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
155 |
ML {* get_descrs @{theory} (2, 2, 2) @{type_name f} *} |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
156 |
ML {* get_descrs @{theory} (2, 2, 2) @{type_name g} *} |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
157 |
ML {* get_descrs @{theory} (0, 1, 1) @{type_name h} *} |
58124 | 158 |
|
56454 | 159 |
datatype_compat h |
160 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
161 |
ML {* get_descrs @{theory} (3, 3, 1) @{type_name h} *} |
58124 | 162 |
|
58216 | 163 |
thm h.induct h.rec |
164 |
thm compat_h.induct compat_h.rec |
|
165 |
||
58310 | 166 |
datatype myunit = MyUnity |
58124 | 167 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
168 |
ML {* get_descrs @{theory} (0, 1, 1) @{type_name myunit} *} |
58124 | 169 |
|
56454 | 170 |
datatype_compat myunit |
171 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
172 |
ML {* get_descrs @{theory} (1, 1, 1) @{type_name myunit} *} |
58124 | 173 |
|
58310 | 174 |
datatype mylist = MyNil | MyCons nat mylist |
58124 | 175 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
176 |
ML {* get_descrs @{theory} (0, 1, 1) @{type_name mylist} *} |
58124 | 177 |
|
56454 | 178 |
datatype_compat mylist |
179 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
180 |
ML {* get_descrs @{theory} (1, 1, 1) @{type_name mylist} *} |
58124 | 181 |
|
58310 | 182 |
datatype foo' = FooNil | FooCons bar' foo' and bar' = Bar |
58124 | 183 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
184 |
ML {* get_descrs @{theory} (0, 2, 2) @{type_name foo'} *} |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
185 |
ML {* get_descrs @{theory} (0, 2, 2) @{type_name bar'} *} |
58124 | 186 |
|
56454 | 187 |
datatype_compat bar' foo' |
188 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
189 |
ML {* get_descrs @{theory} (2, 2, 2) @{type_name foo'} *} |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
190 |
ML {* get_descrs @{theory} (2, 2, 2) @{type_name bar'} *} |
58124 | 191 |
|
58305
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
58216
diff
changeset
|
192 |
old_datatype funky = Funky "funky tre" | Funky' |
58124 | 193 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
194 |
ML {* get_descrs @{theory} (3, 3, 3) @{type_name funky} *} |
58124 | 195 |
|
58305
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
58216
diff
changeset
|
196 |
old_datatype fnky = Fnky "nat tre" |
56454 | 197 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
198 |
ML {* get_descrs @{theory} (1, 1, 1) @{type_name fnky} *} |
58124 | 199 |
|
58310 | 200 |
datatype tree = Tree "tree foo" |
58124 | 201 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
202 |
ML {* get_descrs @{theory} (0, 1, 1) @{type_name tree} *} |
58124 | 203 |
|
56488 | 204 |
datatype_compat tree |
56454 | 205 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
206 |
ML {* get_descrs @{theory} (3, 3, 1) @{type_name tree} *} |
58125 | 207 |
|
58216 | 208 |
thm tree.induct tree.rec |
209 |
thm compat_tree.induct compat_tree.rec |
|
58125 | 210 |
|
58216 | 211 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
212 |
subsection {* Creating New-Style Datatypes Using Old-Style Interfaces *} |
58125 | 213 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
214 |
ML {* |
58125 | 215 |
val l_specs = |
216 |
[((@{binding l}, [("'a", @{sort type})], NoSyn), |
|
217 |
[(@{binding N}, [], NoSyn), |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
218 |
(@{binding C}, [@{typ 'a}, Type (Sign.full_name @{theory} @{binding l}, [@{typ 'a}])], |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
219 |
NoSyn)])]; |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
220 |
*} |
58125 | 221 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
222 |
setup {* snd o BNF_LFP_Compat.add_datatype [] l_specs *} |
58125 | 223 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
224 |
ML {* get_descrs @{theory} (1, 1, 1) @{type_name l} *} |
58125 | 225 |
|
226 |
thm l.exhaust l.map l.induct l.rec l.size |
|
227 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
228 |
ML {* |
58125 | 229 |
val t_specs = |
230 |
[((@{binding t}, [("'b", @{sort type})], NoSyn), |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
231 |
[(@{binding T}, [@{typ 'b}, |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
232 |
Type (@{type_name l}, [Type (Sign.full_name @{theory} @{binding t}, [@{typ 'b}])])], |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
233 |
NoSyn)])]; |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
234 |
*} |
58125 | 235 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
236 |
setup {* snd o BNF_LFP_Compat.add_datatype [] t_specs *} |
58125 | 237 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
238 |
ML {* get_descrs @{theory} (2, 2, 1) @{type_name t} *} |
58125 | 239 |
|
240 |
thm t.exhaust t.map t.induct t.rec t.size |
|
58216 | 241 |
thm compat_t.induct compat_t.rec |
242 |
||
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
243 |
ML {* |
58216 | 244 |
val ft_specs = |
245 |
[((@{binding ft}, [("'a", @{sort type})], NoSyn), |
|
246 |
[(@{binding FT0}, [], NoSyn), |
|
247 |
(@{binding FT}, [@{typ 'a} --> Type (Sign.full_name @{theory} @{binding ft}, [@{typ 'a}])], |
|
248 |
NoSyn)])]; |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
249 |
*} |
58216 | 250 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
251 |
setup {* snd o BNF_LFP_Compat.add_datatype [] ft_specs *} |
58216 | 252 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58310
diff
changeset
|
253 |
ML {* get_descrs @{theory} (1, 1, 1) @{type_name ft} *} |
58216 | 254 |
|
255 |
thm ft.exhaust ft.induct ft.rec ft.size |
|
256 |
thm compat_ft.induct compat_ft.rec |
|
56454 | 257 |
|
258 |
end |