src/HOL/Datatype_Examples/Compat.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58442 039b54d9b5c4
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 (*  Title:      HOL/Datatype_Examples/Compat.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2014
     4 
     5 Tests for compatibility with the old datatype package.
     6 *)
     7 
     8 header {* Tests for Compatibility with the Old Datatype Package *}
     9 
    10 theory Compat
    11 imports "~~/src/HOL/Library/Old_Datatype"
    12 begin
    13 
    14 subsection {* Viewing and Registering New-Style Datatypes as Old-Style Ones *}
    15 
    16 ML {*
    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)),
    25    these (Option.map #descr (BNF_LFP_Compat.get_info thy [] T_name)),
    26    these (Option.map #descr (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] T_name)))
    27   |> tap (check_lens lens);
    28 *}
    29 
    30 old_datatype 'a old_lst = Old_Nl | Old_Cns 'a "'a old_lst"
    31 
    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"
    43   nitpick (* [expect = genuine] *)
    44   quickcheck [exhaustive, expect = counterexample]
    45   quickcheck [random, expect = counterexample]
    46   quickcheck [narrowing (* , expect = counterexample *)]
    47   oops
    48 
    49 lemma "old_len xs = size xs"
    50   by (induct xs) auto
    51 
    52 ML {* get_descrs @{theory} (1, 1, 1) @{type_name old_lst} *}
    53 
    54 datatype 'a lst = Nl | Cns 'a "'a lst"
    55 
    56 ML {* get_descrs @{theory} (0, 1, 1) @{type_name lst} *}
    57 
    58 datatype_compat lst
    59 
    60 ML {* get_descrs @{theory} (1, 1, 1) @{type_name lst} *}
    61 
    62 datatype 'b w = W | W' "'b w \<times> 'b list"
    63 
    64 ML {* get_descrs @{theory} (0, 1, 1) @{type_name w} *}
    65 
    66 datatype_compat w
    67 
    68 ML {* get_descrs @{theory} (2, 2, 1) @{type_name w} *}
    69 
    70 datatype ('c, 'b) s = L 'c | R 'b
    71 
    72 ML {* get_descrs @{theory} (0, 1, 1) @{type_name s} *}
    73 
    74 datatype 'd x = X | X' "('d x lst, 'd list) s"
    75 
    76 ML {* get_descrs @{theory} (0, 1, 1) @{type_name x} *}
    77 
    78 datatype_compat s
    79 
    80 ML {* get_descrs @{theory} (1, 1, 1) @{type_name s} *}
    81 ML {* get_descrs @{theory} (0, 1, 1) @{type_name x} *}
    82 
    83 datatype_compat x
    84 
    85 ML {* get_descrs @{theory} (3, 3, 1) @{type_name x} *}
    86 
    87 thm x.induct x.rec
    88 thm compat_x.induct compat_x.rec
    89 
    90 datatype 'a tttre = TTTre 'a "'a tttre lst lst lst"
    91 
    92 ML {* get_descrs @{theory} (0, 1, 1) @{type_name tttre} *}
    93 
    94 datatype_compat tttre
    95 
    96 ML {* get_descrs @{theory} (4, 4, 1) @{type_name tttre} *}
    97 
    98 thm tttre.induct tttre.rec
    99 thm compat_tttre.induct compat_tttre.rec
   100 
   101 datatype 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre lst"
   102 
   103 ML {* get_descrs @{theory} (0, 1, 1) @{type_name ftre} *}
   104 
   105 datatype_compat ftre
   106 
   107 ML {* get_descrs @{theory} (2, 2, 1) @{type_name ftre} *}
   108 
   109 thm ftre.induct ftre.rec
   110 thm compat_ftre.induct compat_ftre.rec
   111 
   112 datatype 'a btre = BTre 'a "'a btre lst" "'a btre lst"
   113 
   114 ML {* get_descrs @{theory} (0, 1, 1) @{type_name btre} *}
   115 
   116 datatype_compat btre
   117 
   118 ML {* get_descrs @{theory} (3, 3, 1) @{type_name btre} *}
   119 
   120 thm btre.induct btre.rec
   121 thm compat_btre.induct compat_btre.rec
   122 
   123 datatype 'a foo = Foo | Foo' 'a "'a bar" and 'a bar = Bar | Bar' 'a "'a foo"
   124 
   125 ML {* get_descrs @{theory} (0, 2, 2) @{type_name foo} *}
   126 ML {* get_descrs @{theory} (0, 2, 2) @{type_name bar} *}
   127 
   128 datatype_compat foo bar
   129 
   130 ML {* get_descrs @{theory} (2, 2, 2) @{type_name foo} *}
   131 ML {* get_descrs @{theory} (2, 2, 2) @{type_name bar} *}
   132 
   133 datatype 'a tre = Tre 'a "'a tre lst"
   134 
   135 ML {* get_descrs @{theory} (0, 1, 1) @{type_name tre} *}
   136 
   137 datatype_compat tre
   138 
   139 ML {* get_descrs @{theory} (2, 2, 1) @{type_name tre} *}
   140 
   141 thm tre.induct tre.rec
   142 thm compat_tre.induct compat_tre.rec
   143 
   144 datatype 'a f = F 'a and 'a g = G 'a
   145 
   146 ML {* get_descrs @{theory} (0, 2, 2) @{type_name f} *}
   147 ML {* get_descrs @{theory} (0, 2, 2) @{type_name g} *}
   148 
   149 datatype h = H "h f" | H'
   150 
   151 ML {* get_descrs @{theory} (0, 1, 1) @{type_name h} *}
   152 
   153 datatype_compat f g
   154 
   155 ML {* get_descrs @{theory} (2, 2, 2) @{type_name f} *}
   156 ML {* get_descrs @{theory} (2, 2, 2) @{type_name g} *}
   157 ML {* get_descrs @{theory} (0, 1, 1) @{type_name h} *}
   158 
   159 datatype_compat h
   160 
   161 ML {* get_descrs @{theory} (3, 3, 1) @{type_name h} *}
   162 
   163 thm h.induct h.rec
   164 thm compat_h.induct compat_h.rec
   165 
   166 datatype myunit = MyUnity
   167 
   168 ML {* get_descrs @{theory} (0, 1, 1) @{type_name myunit} *}
   169 
   170 datatype_compat myunit
   171 
   172 ML {* get_descrs @{theory} (1, 1, 1) @{type_name myunit} *}
   173 
   174 datatype mylist = MyNil | MyCons nat mylist
   175 
   176 ML {* get_descrs @{theory} (0, 1, 1) @{type_name mylist} *}
   177 
   178 datatype_compat mylist
   179 
   180 ML {* get_descrs @{theory} (1, 1, 1) @{type_name mylist} *}
   181 
   182 datatype foo' = FooNil | FooCons bar' foo' and bar' = Bar
   183 
   184 ML {* get_descrs @{theory} (0, 2, 2) @{type_name foo'} *}
   185 ML {* get_descrs @{theory} (0, 2, 2) @{type_name bar'} *}
   186 
   187 datatype_compat bar' foo'
   188 
   189 ML {* get_descrs @{theory} (2, 2, 2) @{type_name foo'} *}
   190 ML {* get_descrs @{theory} (2, 2, 2) @{type_name bar'} *}
   191 
   192 old_datatype funky = Funky "funky tre" | Funky'
   193 
   194 ML {* get_descrs @{theory} (3, 3, 3) @{type_name funky} *}
   195 
   196 old_datatype fnky = Fnky "nat tre"
   197 
   198 ML {* get_descrs @{theory} (1, 1, 1) @{type_name fnky} *}
   199 
   200 datatype tree = Tree "tree foo"
   201 
   202 ML {* get_descrs @{theory} (0, 1, 1) @{type_name tree} *}
   203 
   204 datatype_compat tree
   205 
   206 ML {* get_descrs @{theory} (3, 3, 1) @{type_name tree} *}
   207 
   208 thm tree.induct tree.rec
   209 thm compat_tree.induct compat_tree.rec
   210 
   211 
   212 subsection {* Creating New-Style Datatypes Using Old-Style Interfaces *}
   213 
   214 ML {*
   215 val l_specs =
   216   [((@{binding l}, [("'a", @{sort type})], NoSyn),
   217    [(@{binding N}, [], NoSyn),
   218     (@{binding C}, [@{typ 'a}, Type (Sign.full_name @{theory} @{binding l}, [@{typ 'a}])],
   219      NoSyn)])];
   220 *}
   221 
   222 setup {* snd o BNF_LFP_Compat.add_datatype [] l_specs *}
   223 
   224 ML {* get_descrs @{theory} (1, 1, 1) @{type_name l} *}
   225 
   226 thm l.exhaust l.map l.induct l.rec l.size
   227 
   228 ML {*
   229 val t_specs =
   230   [((@{binding t}, [("'b", @{sort type})], NoSyn),
   231    [(@{binding T}, [@{typ 'b},
   232        Type (@{type_name l}, [Type (Sign.full_name @{theory} @{binding t}, [@{typ 'b}])])],
   233      NoSyn)])];
   234 *}
   235 
   236 setup {* snd o BNF_LFP_Compat.add_datatype [] t_specs *}
   237 
   238 ML {* get_descrs @{theory} (2, 2, 1) @{type_name t} *}
   239 
   240 thm t.exhaust t.map t.induct t.rec t.size
   241 thm compat_t.induct compat_t.rec
   242 
   243 ML {*
   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)])];
   249 *}
   250 
   251 setup {* snd o BNF_LFP_Compat.add_datatype [] ft_specs *}
   252 
   253 ML {* get_descrs @{theory} (1, 1, 1) @{type_name ft} *}
   254 
   255 thm ft.exhaust ft.induct ft.rec ft.size
   256 thm compat_ft.induct compat_ft.rec
   257 
   258 end